( sum : Type -> Type -> Type )

( left : {S,T | Type } S -> (sum S T) )

( right : {S,T | Type} T -> (sum S T) )

( sum_ind : {S,T : Type}{C : (sum S T) -> Prop}
             ({x : S} (C (left x))) -> ({y : T} (C (right y))) -> 
             ({z : (sum S T)} (C z)) )

( sum_elim : {S,T | Type}{C | (sum S T) -> Type}
             ({x : S} (C (left x))) -> ({y : T} (C (right y))) -> 
             ({z : (sum S T)} (C z)) )

( sum_left : !! {S,T : Type}{C : (sum S T) -> Type}
  {f : {x : S} (C (left x))}{g : {y : T} (C (right y))}
  {x : S} ((sum_elim f g (left x)) = (f x)) )

( sum_right : !! {S,T : Type}{C : (sum S T) -> Type}
  {f : {x : S} (C (left x))}{g : {y : T} (C (right y))}
  {y : T} ((sum_elim f g (right y)) = (g y)) )

( case : {S,T | Type}{U | Type} (S -> U) -> (T -> U) -> (sum S T) -> U )

( case_eq : !! {S,T : Type}{U : Type}{f : (S -> U)}{g : (T -> U)}{z : (sum S T)} 
  ((case f g z) = (sum_elim | S | T | ([_ : (sum S T)] U) f g z)) )

( done )