Next: The Natural Numbers Up: The LEGO library - Previous: Sum Types

# 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)
```

Conor McBride
11/13/1998