Next: The Integers Up: The LEGO library - Previous: Relation closures

# Set theory

The one file currently in this section contains the version of set theory developed for the work described in ##jonesrationals (##jonesrationals). It defines a ``set'' to be the sigma type consisting of a type plus an equivalence relation over that type. Similarly a ``function'' between two sets is an arrow between the base types and a proof that the function respects equality. Also defined are (two-place) relations, two-place functions, and subsets (defined as predicates over the base types).

``` ** Module lib_sets_ccmj Imports lib_logic
eq_refl = ... : {A|Type}(A->A->Prop)->Prop
eq_sym = ... : {A|Type}(A->A->Prop)->Prop
eq_trans = ... : {A|Type}(A->A->Prop)->Prop
eq_rel = ... : (Type)->Type
set = ... : Type
eq = ... : {A|set}A.1->A.1->Prop
eq_refl_ax = ... : {A|set}eq_refl|A.1|A.2.1
eq_sym_ax = ... : {A|set}{x,y|A.1}(eq x y)->eq y x
eq_trans_ax = ... : {A|set}{x,y,z|A.1}(eq x y)->(eq y z)->eq x z
pres_eq = ... : {A,B|set}(A.1->B.1)->Prop
function = ... : set->set->Type
pres_eq_ax = ... : {A,B|set}{f|function A B}[f'4=f.1]pres_eq|A|B f'4
pr = ... : {A,B|set}A.1->B.1->A.1#B.1
cross_prod = ... : set->set->set
curry = ... : {A,B,C:set}(function|(cross_prod A B)|C)->A.1->B.1->C.1
comp = ... : {A,B,C|set}(function A B)->(function B C)->function A C
pres_l = ... : {A:set}(A.1->A.1->Prop)->Prop
pres_r = ... : {A:set}(A.1->A.1->Prop)->Prop
relation = ... : set->Type
rel_pres_eq_l = ... : {A|set}{R|relation A}pres_l A R.1
rel_pres_eq_r = ... : {A|set}{R|relation A}pres_r A R.1
subset = ... : set->Type
pres_eq2 = ... : {A,B:set}(A.1->A.1->B.1)->Prop
function2 = ... : set->set->Type
pres_eq_l = ... :
{A,B|set}{f|function2 A B}{x,y,z:A.1}(eq x y)->
eq (f.1 x z) (f.1 y z)
pres_eq_r = ... :
{A,B|set}{f|function2 A B}{x,y,z:A.1}(eq x y)->
eq (f.1 z x) (f.1 z y)
```

Conor McBride
11/13/1998