Inductive Sigma

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
 ** Label (!sigma!) sigma
 ** Label (!sigma elim!) sigma_elim
 ** Label (!sigma dep_pair!) dep_pair
[[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)