Next: Sum Types Up: The LEGO library - Previous: Boolean Theorems

# Product Types

There is one library file in the directory lib_prod with the definition of (non-dependent) cross-product. As well as the basic definitions there are also theorems giving the -rule for pairs and the fact that pairing is extensional.

 ** Module lib_prod Imports lib_eq_basics
$prod : (Type)->(Type)->Type(prod)$Pair : {A|Type}{B|Type}A->B->prod A B
\$prod_elim :
{A|Type}{B|Type}{C_prod:(prod A B)->Type}
({a:A}{b:B}C_prod (Pair a b))->{z:prod A B}C_prod z
** Label (!prod!) prod
** Label (!prod elim!) prod_elim
** Label (!prod Pair!) Pair
[[A|Type][B|Type][C_prod:(prod A B)->Type]
[f_Pair:{a:A}{b:B}C_prod (Pair a b)][a:A][b:B]
prod_elim C_prod f_Pair (Pair a b)  ==>  f_Pair a b]

Gen (!prod is Pair!) as prod_is_Pair = ... :
{A|Type}{B|Type}(prod A B)->Type
Gen (!prod Pair injective!) as prod_Pair_injective = ... :
{A|Type}{B|Type}{ix0,iy0|A}{ix1,iy1|B}
(Eq (Pair ix0 ix1) (Pair iy0 iy1))->{P|Type}
((Eq ix0 iy0)->(Eq ix1 iy1)->P)->P
pair1 = ... : {A:Type}{B:Type}A->B->prod A B
prod_rec = ... : {s|Type}{t|Type}{u|Type}(s->t->u)->(prod s t)->u
prod_ind = ... :
{s|Type}{t|Type}{P:(prod s t)->Prop}({a:s}{b:t}P (Pair a b))->
{p:prod s t}P p
Fst = ... : {s|Type}{t|Type}(prod s t)->s
Snd = ... : {s|Type}{t|Type}(prod s t)->t
prod_eta = ... :
{s|Type}{t|Type}{p:prod s t}Eq p (Pair (Fst p) (Snd p))
prod_ext = ... :
{s|Type}{t|Type}{p,q:prod s t}(Eq (Fst p) (Fst q))->
(Eq (Snd p) (Snd q))->Eq p q


Conor McBride
11/13/1998