In the directory lib_sigma we define the inductive sigma type, with its projections, a proof that the first projection is injective and the eta-rule for the dependent pairs. Products can then be defined as a non-dependent sigma type.
** Module lib_sigma Imports lib_eq_basics $sigma : {A|Type}(A->Type)->Type(sigma) $dep_pair : {A|Type}{B|A->Type}{a:A}(B a)->sigma|A|B $sigma_elim : {A|Type}{B|A->Type}{C_sigma:(sigma|A|B)->Type} ({a:A}{b:B a}C_sigma (dep_pair a b))->{z:sigma|A|B}C_sigma z [[A|Type][B|A->Type][C_sigma:(sigma|A|B)->Type] [f_dep_pair:{a:A}{b:B a}C_sigma (dep_pair a b)][a:A][b:B a] sigma_elim C_sigma f_dep_pair (dep_pair a b) ==> f_dep_pair a b] sigma_rec = ... : {A|Type}{B|A->Type}{T|Type}({a:A}(B a)->T)->(sigma|A|B)->T sigma_ind = ... : {A|Type}{B|A->Type}{P:(sigma|A|B)->Prop} ({a:A}{b:B a}P (dep_pair a b))->{z:sigma|A|B}P z sig_pi1 = ... : {A|Type}{B|A->Type}(sigma|A|B)->A sig_pi2 = ... : {A|Type}{B|A->Type}{z:sigma|A|B}B (sig_pi1 z) dep_pair_eta = ... : {A|Type}{B|A->Type}{x:sigma|A|B} Eq x (dep_pair (sig_pi1 x) (sig_pi2 x)) sig_pi1_inj = ... : {A|Type}{B|A->Type}{x,y:sigma|A|B}(Eq x y)-> Eq (sig_pi1 x) (sig_pi1 y) Sigma = ... : {A:Type}(A->Type)->Type(sigma) Prod = ... : (Type)->(Type)->Type(sigma) Pr = ... : {A|Type}{B|Type}A->B->sigma|A|([_:A]B)