Uset : Type.
Uprop : Type.
Utype : Type.

eprop : x : Uprop -> Type.
eset : x : Uset -> Type.
etype : x : Utype -> Type.

dotset : Utype.
dotprop : Utype.

dotpipp : x : Uprop -> y : (eprop x -> Uprop) -> Uprop.
dotpips : x : Uprop -> y : (eprop x -> Uset)  -> Uset.
dotpipt : x : Uprop -> y : (eprop x -> Utype) -> Utype.
dotpisp : x : Uset  -> y : (eset x  -> Uprop) -> Uprop.
dotpitp : x : Utype -> y : (etype x -> Uprop) -> Uprop.
dotpist : x : Uset  -> y : (eset  x -> Utype) -> Utype.
dotpits : x : Utype -> y : (etype x -> Uset)  -> Uset.
dotpiss : x : Uset  -> y : (eset x  -> Uset)  -> Uset.
dotpitt : x : Utype -> y : (etype x -> Utype) -> Utype.


[x:Uprop, y : eprop x -> Uprop]
              eprop (dotpipp x y) --> w : eprop x -> eprop (y w).

[x:Uset, y : eset x -> Uprop]
              eprop (dotpisp x y) --> w : eset x -> eprop (y w).

[x:Utype, y : etype x -> Uprop]
              eprop (dotpitp x y) --> w : etype x -> eprop (y w).

[x:Uprop, y : eprop x -> Uset]
              eset (dotpips x y) --> w : eprop x -> eset (y w).

[x:Utype, y : etype x -> Uset]
              eset (dotpits x y) --> w : etype x -> eset (y w).

[x:Uset, y : eset x -> Uset]
              eset (dotpiss x y) --> w : eset x -> eset (y w).

[x:Uset, y : eset x -> Utype]
              etype (dotpist x y) --> w : eset x -> etype (y w).

[x:Utype, y : etype x -> Utype]
              etype (dotpitt x y) --> w : etype x -> etype (y w).

[x:Uprop, y : eprop x -> Utype]
              etype (dotpipt x y) --> w : eprop x -> etype (y w).


[] (etype dotset)  --> Uset.
[] (etype dotprop) --> Uprop.
simple :  (P : Uprop ->  (_ :  (eprop P)  ->  (eprop P) ) ) .
[] simple -->  (P :  (etype dotprop)  =>  (H :  (eprop P)  => H) ) .
K :  (P : Uprop ->  (Q : Uprop ->  (_ :  (eprop P)  ->  (_ :  (eprop Q)  ->  (eprop P) ) ) ) ) .
[] K -->  (P :  (etype dotprop)  =>  (Q :  (etype dotprop)  =>  (H :  (eprop P)  =>  (H0 :  (eprop Q)  =>  ( (simple P)  H) ) ) ) ) .
S :  (P : Uprop ->  (Q : Uprop ->  (R : Uprop ->  (_ :  (_ :  (eprop P)  ->  (_ :  (eprop Q)  ->  (eprop R) ) )  ->  (_ :  (_ :  (eprop P)  ->  (eprop Q) )  ->  (_ :  (eprop P)  ->  (eprop R) ) ) ) ) ) ) .
[] S -->  (P :  (etype dotprop)  =>  (Q :  (etype dotprop)  =>  (R :  (etype dotprop)  =>  (H :  (eprop  ( (dotpipp P)   (_ :  (eprop P)  =>  ( (dotpipp Q)   (_ :  (eprop Q)  => R) ) ) ) )  =>  (H0 :  (eprop  ( (dotpipp P)   (_ :  (eprop P)  => Q) ) )  =>  (H1 :  (eprop P)  =>  ( (H H1)   (H0 H1) ) ) ) ) ) ) ) .
I :  (P : Uprop ->  (_ :  (eprop P)  ->  (eprop P) ) ) .
[] I -->  (P :  (etype dotprop)  =>  ( ( ( ( (S P)   ( (dotpipp P)   (_ :  (eprop P)  => P) ) )  P)   ( (K P)   ( (dotpipp P)   (_ :  (eprop P)  => P) ) ) )   ( (K P)  P) ) ) .