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)