Voevodsky describes sets as "well-founded trees with no automorphisms".
We can formalize  well-founded trees with W-types.
This is what Aczel did when interpreting CZF into type theory.
We can follow Aczel's interpretation and define "CZF" in Nuprl.

Aczel also studied non-wellfounded sets.
The non-wellfounded trees are the coW-types, and W-type is just the
well-founded subtype of the corresponding coW-type.

We define ⌜Set{i:l}⌝ to be ⌜W(Type;x.x)⌝ and 
 ⌜coSet{i:l}⌝ to be ⌜coW(Type;x.x)⌝
so set (or co-set) is
Wsup(T;f)⌝  where ⌜T ∈ Type⌝ and 
f ∈ T ⟶ Set{i:l}⌝ (or ⌜f ∈ T ⟶ coSet{i:l}⌝).

Now we need to deal with the "no automorphisms" part.
For that we need an equivalence relation on sets that corresponds to
"s1 and s2" have the same members.

Aczel defined set equality using the recursive definition: 
seteq(s1;s2) ==  let T,f s1 in let X,g s2 in (∀t:T. ∃x:X. seteq(f t;g x)) ∧ (∀x:X. ∃t:T. seteq(f t;g x))⌝
This is well-defined for ⌜Set{i:l}⌝ because sets are well-founded.
But it won't work for the type ⌜coSet{i:l}⌝.

If we want one definition of set equality that works for both Set and cSet
we need to use the definition that works for coSet.
That is the bisimulation relation on coW-types
which for coSet becomes
 ⌜seteq(s1;s2) ==  coW-equiv(T.T;s1;s2)⌝

This is indeed an equivalence relation on both 
coSet{i:l}⌝ and on ⌜Set{i:l}⌝ (see seteq_equiv).
So we would be tempted to 
use the quotient type ⌜s1,s2:Set{i:l}//seteq(s1;s2)⌝ for the type of sets.
That would probably not work well for reasons similar to the
constructive reals (there is no canonical member of each equivalence class
so it won't be possible to compute with such quotiented sets).

So we just interpret in CZF as seteq.

Now set is member of ⌜Wsup(T;f)⌝ if ⌜∃t:T. seteq(x;f t)⌝,
so that gives the interpretation of ⌜(x ∈ s)⌝.

Now one wants to verify the axioms of CZF as much as possible.
We have versions of restricted separation 
sub-set_wf  and setmem-sub-set
(restricted to propositions in universe i).
Notice that we don't need the concept of class of sets defined
by formula. Instead we can just use propositions about sets 
(and relations on sets, rather than classes of ordered pairs)
that respect the `seteq` relation.  We can call these `extensional`
propositions and relations.

The `restricted` classes correspond to propositions in universe i
and unrestricted classes to propositions in universe i+1  (or higher).

The "union-replacement" is (setunionfun_wfsetmem-setunionfun)
Again, the function can be any extensional function from sets to sets.
(Members of the function type ⌜Set{i:l} ⟶ Set{i:l}⌝ are what Bishop
call `operations` on Sets, while those that are extensional 
(i.e respect `seteq`) are called `set functions`). .

Of course, pair is easy setmem-pairset
The foundation axiom is replaced by the induction principle:

The "exponentiation" axiom seems to be the same as the
existence of the set Πa:A.B[a]  (see setmem-Piset)
and we also have the set Σa:A.B[a]  (see setmem-sigmaset).

We define the transitive closure of set
and the TC-induction principle setTC-induction.

Aczel proves that the type-theoric interpretation of CZF also satisfies the
REA ("Regular Extension Axiom").
We prove that in Nuprl:  RegularExtension.

Aczel uses that to prove the existence of inductively defined sets
where the inductive definition is "bounded".
See Error :bounded-inductive-definition

Definition: coSet
coSet{i:l} ==  coW(Type;x.x)

Lemma: coSet_wf
coSet{i:l} ∈ 𝕌'

Lemma: coSet_subtype
coSet{i:l} ⊆(T:Type × (T ⟶ coSet{i:l}))

Lemma: subtype_coSet
(T:Type × (T ⟶ coSet{i:l})) ⊆coSet{i:l}

Lemma: coSet-subtype-corec
coSet{i:l} ⊆corec(T.a:Type × (a ⟶ T))

Lemma: corec-subtype-coSet
corec(T.a:Type × (a ⟶ T)) ⊆coSet{i:l}

Lemma: coSet-corec
coSet{i:l} ≡ corec(T.a:Type × (a ⟶ T))

Definition: mk-coset
mk-coset(T;f) ==  <T, f>

Lemma: mk-coset_wf
[T:Type]. ∀[f:T ⟶ coSet{i:l}].  (mk-coset(T;f) ∈ coSet{i:l})

Definition: set-dom
set-dom(s) ==  fst(s)

Lemma: set-dom_wf
[s:coSet{i:l}]. (set-dom(s) ∈ Type)

Definition: set-item
set-item(s;x) ==  (snd(s)) x

Lemma: set-item_wf
[s:coSet{i:l}]. ∀[x:set-dom(s)].  (set-item(s;x) ∈ coSet{i:l})

Definition: set-eq
set-eq(s;s') ==
  νR.λs,s'. ((∀i:set-dom(s). ∃j:set-dom(s'). (R set-item(s;i) set-item(s';j)))
           ∧ (∀j:set-dom(s'). ∃i:set-dom(s). (R set-item(s;i) set-item(s';j)))) 

Lemma: set-eq_wf
[s,s':coSet{i:l}].  (set-eq(s;s') ∈ ℙ)

Definition: seteq
seteq(s1;s2) ==  coW-equiv(T.T;s1;s2)

Lemma: seteq_wf
[s1,s2:coSet{i:l}].  (seteq(s1;s2) ∈ ℙ)

Lemma: seteq-equiv

Definition: coSet-bisimulation

coSet-bisimulation{i:l}(x,y.R[x; y]) ==
    ((((a:Type × (a ⟶ T)) ⊆T) ∧ (coSet{i:l} ⊆T))
     (∀x,y:coSet{i:l}.  (R[x; y]  (x y ∈ T)))
     (∀x,y:coSet{i:l}.  (R[x; y]  (x y ∈ (a:Type × (a ⟶ T))))))

Lemma: coSet-bisimulation_wf
[R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ']. (coSet-bisimulation{i:l}(x,y.R[x;y]) ∈ ℙ{i''})

Lemma: coSet-equality
  (x y ∈ coSet{i:l} ⇐⇒ ∃R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'. (coSet-bisimulation{i:l}(x,y.R[x;y]) ∧ R[x;y]))

Lemma: coSet-equality2
  ((∀T:𝕌'. ((((a:Type × (a ⟶ T)) ⊆T) ∧ (coSet{i:l} ⊆T))  (x y ∈ T)  (x y ∈ (a:Type × (a ⟶ T)))))
   (x y ∈ coSet{i:l}))

Definition: setmem
(x ∈ s) ==  coWmem(T.T;x;s)

Lemma: setmem_wf
[x,s:coSet{i:l}].  ((x ∈ s) ∈ ℙ)

Lemma: setmem-iff
x,s:coSet{i:l}.  ((x ∈ s) ⇐⇒ ∃t:set-dom(s). seteq(x;set-item(s;t)))

Lemma: set-item-mem
s:coSet{i:l}. ∀x:set-dom(s).  (set-item(s;x) ∈ s)

Lemma: co-seteq-iff
x,y:coSet{i:l}.  (seteq(x;y) ⇐⇒ ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ (z ∈ y)))

Lemma: setmem-mk-coset
[T,f,x:Top].  ((x ∈ mk-coset(T;f)) ~ ∃t:T. seteq(x;f t))

Definition: comem
comem{i:l}(x;s) ==  ∃t:set-dom(s). (x set-item(s;t) ∈ coSet{i:l})

Lemma: comem_wf
[s,x:coSet{i:l}].  (comem{i:l}(x;s) ∈ ℙ')

Lemma: fix_wf_coSet
[G:⋂W:𝕌'. (W ⟶ (T:Type × (T ⟶ W)))]. (fix(G) ∈ coSet{i:l})

Lemma: fix_wf_coSet_system
[I:𝕌']. ∀[G:⋂C:{C:𝕌'| ((T:Type × (T ⟶ C)) ⊆C) ∧ (coSet{i:l} ⊆C)} ((I ⟶ C) ⟶ I ⟶ (T:Type × (T ⟶ C)))].
  (fix(G) ∈ I ⟶ coSet{i:l})

Lemma: fix_wf_coSet_system_weak
[I:𝕌']. ∀[G:⋂C:𝕌'. ((I ⟶ C) ⟶ I ⟶ (T:Type × (T ⟶ C)))].  (fix(G) ∈ I ⟶ coSet{i:l})

Definition: graph-cosets
graph-cosets(I;i,j.E[i; j]) ==  fix((λS,i. <j:I × E[i; j], λp.(S (fst(p)))>))

Lemma: graph-cosets_wf
[I:Type]. ∀[E:I ⟶ I ⟶ ℙ].  (graph-cosets(I;i,j.E[i;j]) ∈ I ⟶ coSet{i:l})

Lemma: comem-graph-cosets
[I:Type]. ∀[E:I ⟶ I ⟶ ℙ].
  ∀i:I. ∀x:coSet{i:l}.
    (comem{i:l}(x;graph-cosets(I;i,j.E[i;j]) i) ⇐⇒ ∃j:I. (E[i;j] ∧ (x (graph-cosets(I;i,j.E[i;j]) j) ∈ coSet{i:l})))

Definition: loopset
loopset() ==  fix((λS.<Unit, λp.S>))

Lemma: loopset_wf
loopset() ∈ coSet{i:l}

Lemma: loopset-sq
loopset() mk-coset(Unit;λp.loopset())

Definition: Set
Set{i:l} ==  W(Type;x.x)

Lemma: Set_wf
Set{i:l} ∈ 𝕌'

Lemma: set-ext
Set{i:l} ≡ T:Type × (T ⟶ Set{i:l})

Lemma: subtype-set
(T:Type × (T ⟶ Set{i:l})) ⊆Set{i:l}

Lemma: set-subtype
Set{i:l} ⊆(T:Type × (T ⟶ Set{i:l}))

Lemma: set-subtype-coSet
Set{i:l} ⊆coSet{i:l}

Definition: mkset
{f[t] t ∈ T} ==  <T, λt.f[t]>

Lemma: mkset_wf
[T:Type]. ∀[f:T ⟶ Set{i:l}].  ({f[t] t ∈ T} ∈ Set{i:l})

Definition: mk-set
f"(T) ==  Wsup(T;f)

Lemma: mk-set_wf
[T:Type]. ∀[f:T ⟶ Set{i:l}].  (f"(T) ∈ Set{i:l})

Lemma: dom_mk_set_lemma
f,T:Top.  (set-dom(f"(T)) T)

Lemma: item_mk_set_lemma
x,f,T:Top.  (set-item(f"(T);x) x)

Lemma: set-induction-1
[P:Set{i:l} ⟶ ℙ']. ((∀T:Type. ∀f:T ⟶ Set{i:l}.  ((∀t:T. P[f[t]])  P[f"(T)]))  (∀s:Set{i:l}. P[s]))

Lemma: set-induction-1-ext
[P:Set{i:l} ⟶ ℙ']. ((∀T:Type. ∀f:T ⟶ Set{i:l}.  ((∀t:T. P[f[t]])  P[f"(T)]))  (∀s:Set{i:l}. P[s]))

Definition: Set-ind
Set-ind() ==  λh,s. W_ind(λa,f,x. (h x);s)

Lemma: Set-ind_wf
Set-ind() ∈ ∀[P:Set{i:l} ⟶ ℙ']. ((∀T:Type. ∀f:T ⟶ Set{i:l}.  ((∀t:T. P[f[t]])  P[f"(T)]))  (∀s:Set{i:l}. P[s]))

Lemma: set-induction
[P:Set{i:l} ⟶ ℙ']. ((∀T:Type. ∀f:T ⟶ Set{i:l}.  ((∀t:T. P[f[t]])  P[f"(T)]))  (∀s:Set{i:l}. P[s]))

Definition: isSet
isSet(w) ==  coW-wfdd(x.x;w)

Lemma: isSet_wf
[a:coSet{i:l}]. (isSet(a) ∈ ℙ)

Lemma: isSet_functionality
a1,a2:coSet{i:l}.  (seteq(a1;a2)  (isSet(a1) ⇐⇒ isSet(a2)))

Lemma: coSet-is-Set
[a:coSet{i:l}]. a ∈ Set{i:l} supposing isSet(a)

Lemma: Set-isSet
[a:Set{i:l}]. isSet(a)

Lemma: coSet-seteq-Set
[s:Set{i:l}]. ∀[z:coSet{i:l}].  z ∈ Set{i:l} supposing seteq(z;s)

Lemma: set-item_wf2
[s:Set{i:l}]. ∀[t:set-dom(s)].  (set-item(s;t) ∈ Set{i:l})

Lemma: seteqweaken1
s1,s2:coSet{i:l}.  ((s1 s2 ∈ coSet{i:l})  seteq(s1;s2))

Lemma: seteqweaken1_ext
s1,s2:coSet{i:l}.  ((s1 s2 ∈ coSet{i:l})  seteq(s1;s2))

Definition: seteqweaken
seteqweaken(s2) ==
  λ_,moves. let u,v moves[||moves|| 2] 
            in let u',v' moves[||moves|| 1] 
               in if copath-length(u) <copath-length(u') then <u', u'> else <v', v'> fi 

Lemma: seteqweaken_wf
s1,s2:coSet{i:l}.  (seteqweaken(s2) ∈ (s1 s2 ∈ coSet{i:l})  seteq(s1;s2))

Lemma: seteq_weakening
s1,s2:coSet{i:l}.  ((s1 s2 ∈ coSet{i:l})  seteq(s1;s2))

Lemma: seteqinv1
s1,s2:coSet{i:l}.  (seteq(s1;s2)  seteq(s2;s1))

Lemma: seteqinv1_ext
s1,s2:coSet{i:l}.  (seteq(s1;s2)  seteq(s2;s1))

Definition: seteqinv
seteqinv() ==  λ_,f,eq,moves. let u,v eq λp.let u,v in <v, u> moves in <v, u>

Lemma: seteqinv_wf
seteqinv() ∈ ∀s1,s2:coSet{i:l}.  (seteq(s1;s2)  seteq(s2;s1))

Lemma: seteq_inversion
s1,s2:coSet{i:l}.  (seteq(s1;s2)  seteq(s2;s1))

Lemma: seteqtrans1
s1,s2,s3:coSet{i:l}.  (seteq(s1;s2)  seteq(s2;s3)  seteq(s1;s3))

Lemma: seteqtrans1_ext
s1,s2,s3:coSet{i:l}.  (seteq(s1;s2)  seteq(s2;s3)  seteq(s1;s3))

Definition: seteqtrans
seteqtrans() ==  λ_,_,_,eq1,eq2. coW-trans(eq1; eq2)

Lemma: seteqtrans_wf
seteqtrans() ∈ ∀s1,s2,s3:coSet{i:l}.  (seteq(s1;s2)  seteq(s2;s3)  seteq(s1;s3))

Lemma: seteq_transitivity
s1,s2,s3:coSet{i:l}.  (seteq(s1;s2)  seteq(s2;s3)  seteq(s1;s3))

Lemma: seteq_equiv

Lemma: seteq_functionality
x1,x2,y1,y2:coSet{i:l}.  (seteq(x1;x2)  seteq(y1;y2)  (seteq(x1;y1) ⇐⇒ seteq(x2;y2)))

Lemma: setmemfunclemma
x1,s1,x2,s2:coSet{i:l}.  (seteq(x1;x2)  seteq(s1;s2)  {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})

Lemma: setmemfunclemma_ext
x1,s1,x2,s2:coSet{i:l}.  (seteq(x1;x2)  seteq(s1;s2)  {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})

Definition: setmemfunc
setmemfunc(x1; s1; x2; s2) ==
  λ%,%1. <λ%5.let x,y s2 
              in let b,y1 %5 
                 in let q1,y2 %1 
                                , λi.if i=0
                                     then <(), ()>
                                     else if 1=0 then <copath-cons(b;()), ()> else (⋅ (i 1))
                    in <copath-hd(y2)
                       seteqtrans() x2 x1 (y copath-hd(y2)) (seteqinv() x1 x2 %) 
                                   λmoves.let u,v %1 
                                                    let k,g moves 
                                                    in <(k 1) 1
                                                       , λi.if i=0
                                                            then <(), ()>
                                                            else if 1=0
                                                                 then <copath-cons(b;()), ()>
                                                                 else let u,v (i 1) 
                                                                      in <copath-cons(b;u)
                                          in <copath-tl(u), copath-tl(v)>)
         , λ%5.let x,y s1 
               in let b,y1 %5 
                  in let u,y2 %1 
                                , λi.if i=0
                                     then <(), ()>
                                     else if 1=0 then <(), copath-cons(b;())> else let u,v = ⋅ (i 1) in <v, u>
                     in <copath-hd(u)
                        seteqtrans() x1 x2 (y copath-hd(u)) 
                                    λmoves.let u,v %1 
                                                     let k,g moves 
                                                     in <(k 1) 1
                                                        , λi.if i=0
                                                             then <(), ()>
                                                             else if 1=0
                                                                  then <(), copath-cons(b;())>
                                                                  else let u@0,v (i 1) 
                                                                       in <copath-cons(copath-hd(u);v)
                                           in <copath-tl(v), copath-tl(u)>)

Lemma: setmemfunc_wf
[x1,s1,x2,s2:coSet{i:l}].  (setmemfunc(x1; s1; x2; s2) ∈ seteq(x1;x2)  seteq(s1;s2)  {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})

Lemma: setmem_functionality
x1,s1,x2,s2:coSet{i:l}.  (seteq(x1;x2)  seteq(s1;s2)  {(x1 ∈ s1) ⇐⇒ (x2 ∈ s2)})

Lemma: setmem_functionality_1
s,x1,x2:coSet{i:l}.  (seteq(x1;x2)  ((x1 ∈ s) ⇐⇒ (x2 ∈ s)))

Lemma: coSet-mem-Set-implies-Set
[z:coSet{i:l}]. z ∈ Set{i:l} supposing ∃s:Set{i:l}. (z ∈ s)

Lemma: coSet-subtype-Set
B:Set{i:l}. ({u:coSet{i:l}| (u ∈ B)}  ⊆Set{i:l})

Lemma: seteq-iff
s1,s2:Set{i:l}.  (seteq(s1;s2) ⇐⇒ ∀x:Set{i:l}. ((x ∈ s1) ⇐⇒ (x ∈ s2)))

Lemma: setmem-irreflexive
s:Set{i:l}. (s ∈ s))

Lemma: setmem-mk-set-sq
[T,f,x:Top].  ((x ∈ f"(T)) ~ ∃b:T. seteq(x;f b))

Lemma: setmem-mkset-sq
[T,f,x:Top].  ((x ∈ {f[b] b ∈ T}) ~ ∃b:T. seteq(x;f[b]))

Lemma: setmem-mk-set
T:Type. ∀f:T ⟶ Set{i:l}. ∀t:T.  (f t ∈ f"(T))

Lemma: setmem-coset
T:Type. ∀f:T ⟶ coSet{i:l}. ∀t:T.  (f t ∈ mk-coset(T;f))

Lemma: setmem-loopset
z:coSet{i:l}. ((z ∈ loopset()) ⇐⇒ seteq(z;loopset()))

Definition: set-predicate
set-predicate{i:l}(s;a.P[a]) ==  ∀a1,a2:coSet{i:l}.  ((a1 ∈ s)  (a2 ∈ s)  seteq(a1;a2)  P[a1]  P[a2])

Lemma: set-predicate_wf
[s:coSet{i:l}]. ∀[P:{x:coSet{i:l}| (x ∈ s)}  ⟶ ℙ'].  (set-predicate{i:l}(s;x.P[x]) ∈ ℙ')

Lemma: set-predicate_wf2
[s:Set{i:l}]. ∀[P:{x:Set{i:l}| (x ∈ s)}  ⟶ ℙ'].  (set-predicate{i:l}(s;x.P[x]) ∈ ℙ')

Lemma: set-predicate-iff
[s:Set{i:l}]. ∀[P:{x:Set{i:l}| (x ∈ s)}  ⟶ ℙ'].
  (set-predicate{i:l}(s;x.P[x]) ⇐⇒ ∀a1,a2:Set{i:l}.  ((a1 ∈ s)  (a2 ∈ s)  seteq(a1;a2)  P[a1]  P[a2]))

Lemma: isSet-set-predicate
s:coSet{i:l}. set-predicate{i:l}(s;x.isSet(x))

Definition: sub-set
{a ∈ P[a]} ==  let T,f in <t:T × P[f t], λp.(f (fst(p)))>

Lemma: sub-set_wf
[s:coSet{i:l}]. ∀[P:{a:coSet{i:l}| (a ∈ s)}  ⟶ ℙ].  ({a ∈ P[a]} ∈ coSet{i:l})

Lemma: sub-set_wf2
[s:Set{i:l}]. ∀[P:{a:Set{i:l}| (a ∈ s)}  ⟶ ℙ].  ({a ∈ P[a]} ∈ Set{i:l})

Lemma: setmem-sub-set
  ∀[P:{a:Set{i:l}| (a ∈ s)}  ⟶ ℙ]
    (set-predicate{i:l}(s;a.P[a])  (∀a:Set{i:l}. ((a ∈ {a ∈ P[a]}) ⇐⇒ (a ∈ s) ∧ P[a])))

Lemma: setmem-sub-coset
  ∀[P:{a:coSet{i:l}| (a ∈ s)}  ⟶ ℙ]
    (set-predicate{i:l}(s;a.P[a])  (∀a:coSet{i:l}. ((a ∈ {a ∈ P[a]}) ⇐⇒ (a ∈ s) ∧ P[a])))

Definition: set-function
set-function{i:l}(s; x.f[x]) ==  ∀x,y:coSet{i:l}.  ((x ∈ s)  (y ∈ s)  seteq(x;y)  seteq(f[x];f[y]))

Lemma: set-function_wf
[s:coSet{i:l}]. ∀[f:{x:coSet{i:l}| (x ∈ s)}  ⟶ coSet{i:l}].  (set-function{i:l}(s; x.f[x]) ∈ ℙ')

Definition: set-part
set-part(s) ==  {x ∈ isSet(x)}

Lemma: set-part_wf
[s:coSet{i:l}]. (set-part(s) ∈ Set{i:l})

Lemma: setmem-set-part
s,x:coSet{i:l}.  ((x ∈ set-part(s)) ⇐⇒ (x ∈ s) ∧ isSet(x))

Definition: setunionfun
 ⋃x∈s.f[x] ==  let T,g in <t:T × set-dom(f[g t]), λp.let t,d in set-item(f[g t];d)>

Lemma: setunionfun_wf
[s:coSet{i:l}]. ∀[f:{x:coSet{i:l}| (x ∈ s)}  ⟶ coSet{i:l}].  ( ⋃x∈s.f[x] ∈ coSet{i:l})

Lemma: setunionfun_wf2
[s:Set{i:l}]. ∀[f:{x:Set{i:l}| (x ∈ s)}  ⟶ Set{i:l}].  ( ⋃x∈s.f[x] ∈ Set{i:l})

Lemma: setmem-unionfun-implies
s:coSet{i:l}. ∀f:{x:coSet{i:l}| (x ∈ s)}  ⟶ coSet{i:l}. ∀y:coSet{i:l}.
  ((y ∈  ⋃x∈s.f[x])  (∃x:coSet{i:l}. ((x ∈ s) ∧ (y ∈ f[x]))))

Lemma: setmem-setunionfun
s:coSet{i:l}. ∀f:{x:coSet{i:l}| (x ∈ s)}  ⟶ coSet{i:l}.
  (set-function{i:l}(s; x.f[x])  (∀y:coSet{i:l}. ((y ∈  ⋃x∈s.f[x]) ⇐⇒ ∃x:coSet{i:l}. ((x ∈ s) ∧ (y ∈ f[x])))))

Definition: unionset
(s) ==   ⋃x∈s.x

Lemma: unionset_wf
[s:coSet{i:l}]. (⋃(s) ∈ coSet{i:l})

Lemma: unionset_wf2
[s:Set{i:l}]. (⋃(s) ∈ Set{i:l})

Lemma: setmem-unionset
s,x:coSet{i:l}.  ((x ∈ ⋃(s)) ⇐⇒ ∃a:coSet{i:l}. ((a ∈ s) ∧ (x ∈ a)))

Lemma: unionset_functionality
a,b:coSet{i:l}.  (seteq(a;b)  seteq(⋃(a);⋃(b)))

Lemma: setmem-mkset
T:Type. ∀f:T ⟶ Set{i:l}. ∀x:Set{i:l}.  ((x ∈ {f[t] t ∈ T}) ⇐⇒ ∃t:T. seteq(x;f[t]))

Definition: emptyset
{} ==  {⋅ x ∈ Void}

Lemma: emptyset_wf
{} ∈ Set{i:l}

Lemma: setmem-emptyset
x:coSet{i:l}. ((x ∈ {}) ⇐⇒ False)

Definition: singleset
{a} ==  <Unit, λx.a>

Lemma: singleset_wf
[a:coSet{i:l}]. ({a} ∈ coSet{i:l})

Lemma: singleset_wf2
[a:Set{i:l}]. ({a} ∈ Set{i:l})

Lemma: setmem-singleset
a,x:coSet{i:l}.  ((x ∈ {a}) ⇐⇒ seteq(x;a))

Lemma: singleset_functionality
a,b:coSet{i:l}.  (seteq(a;b)  seteq({a};{b}))

Definition: singleitem
singleitem(s) ==  ⋃(s)

Lemma: singleitem_wf
[s:coSet{i:l}]. (singleitem(s) ∈ coSet{i:l})

Lemma: singleitem_wf2
[s:Set{i:l}]. (singleitem(s) ∈ Set{i:l})

Lemma: singleitem_functionality
a,b:coSet{i:l}.  (seteq(a;b)  seteq(singleitem(a);singleitem(b)))

Lemma: singleitem-singleset
a:coSet{i:l}. seteq(singleitem({a});a)

Definition: pairset
{a,b} ==  <𝔹, λx.if then else fi >

Lemma: pairset_wf
[a,b:coSet{i:l}].  ({a,b} ∈ coSet{i:l})

Lemma: pairset_wf2
[a,b:Set{i:l}].  ({a,b} ∈ Set{i:l})

Lemma: setmem-pairset
a,b,x:coSet{i:l}.  ((x ∈ {a,b}) ⇐⇒ seteq(x;a) ∨ seteq(x;b))

Lemma: pairset_functionality
a,b,a',b':coSet{i:l}.  (seteq(a;a')  seteq(b;b')  seteq({a,b};{a',b'}))

Definition: orderedpairset
(a,b) ==  {{a},{a,b}}

Lemma: orderedpairset_wf
[a,b:coSet{i:l}].  ((a,b) ∈ coSet{i:l})

Lemma: orderedpairset_wf2
[a,b:Set{i:l}].  ((a,b) ∈ Set{i:l})

Lemma: seteq-orderedpairs-iff
a,b,a',b':coSet{i:l}.  (seteq((a,b);(a',b')) ⇐⇒ seteq(a;a') ∧ seteq(b;b'))

Lemma: orderedpairset_functionality
a,b,a',b':coSet{i:l}.  (seteq(a;a')  seteq(b;b')  seteq((a,b);(a',b')))

Definition: set-add
==  let T,f in let S,g in <S, λx.case of inl(t) => inr(s) => s>

Lemma: set-add_wf
[a,b:coSet{i:l}].  (a b ∈ coSet{i:l})

Lemma: set-add_wf2
[a,b:Set{i:l}].  (a b ∈ Set{i:l})

Lemma: setmem-set-add
a,b,x:coSet{i:l}.  ((x ∈ b) ⇐⇒ (x ∈ a) ∨ (x ∈ b))

Lemma: set-add_functionality
a,b,a',b':coSet{i:l}.  (seteq(a;a')  seteq(b;b')  seteq(a b;a' b'))

Definition: plus-set
(a)+ ==  {a} a

Lemma: plus-set_wf
[a:coSet{i:l}]. ((a)+ ∈ coSet{i:l})

Lemma: plus-set_wf2
[a:Set{i:l}]. ((a)+ ∈ Set{i:l})

Lemma: setmem-plus-set
a,x:coSet{i:l}.  ((x ∈ (a)+) ⇐⇒ (x ∈ a) ∨ seteq(x;a))

Lemma: plus-set_functionality
a,a':coSet{i:l}.  (seteq(a;a')  seteq((a)+;(a')+))

Definition: cosetTC
cosetTC(a) ==  mk-coset({p:copath(T.T;a)| 0 < copath-length(p)} p.copath-at(a;p))

Lemma: cosetTC_wf
[a:coSet{i:l}]. (cosetTC(a) ∈ coSet{i:l})

Lemma: cosetTC_wf2
[a:Set{i:l}]. (cosetTC(a) ∈ Set{i:l})

Definition: setTC
setTC(a) ==  +  ⋃x∈a.setTC(x)

Lemma: setTC_wf
[a:Set{i:l}]. (setTC(a) ∈ Set{i:l})

Definition: allsetmem
a∈A.P[a] ==  ∀i:set-dom(A). P[set-item(A;i)]

Lemma: allsetmem_wf
[A:coSet{i:l}]. ∀[P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ].  (∀a∈A.P[a] ∈ ℙ)

Lemma: implies-allsetmem
A:coSet{i:l}. ∀[P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ]. ((∀a:coSet{i:l}. ((a ∈ A)  P[a]))  ∀a∈A.P[a])

Lemma: allsetmem-iff
  ∀[P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ]. (set-predicate{i:l}(A;a.P[a])  (∀a∈A.P[a] ⇐⇒ ∀a:coSet{i:l}. ((a ∈ A)  P[a])))

Lemma: allsetmem_functionality
A:coSet{i:l}. ∀P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ. ∀B:coSet{i:l}.
  (set-predicate{i:l}(A;a.P[a])  seteq(A;B)  (∀a∈A.P[a] ⇐⇒ ∀a∈B.P[a]))

Definition: existssetmem
a∈A.P[a] ==  ∃i:set-dom(A). P[set-item(A;i)]

Lemma: existssetmem_wf
[A:coSet{i:l}]. ∀[P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ].  (∃a∈A.P[a] ∈ ℙ)

Lemma: existssetmem-implies
A:coSet{i:l}. ∀[P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ]. (∃a∈A.P[a]  (∃a:coSet{i:l}. ((a ∈ A) ∧ P[a])))

Lemma: existssetmem-iff
  ∀[P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ]. (set-predicate{i:l}(A;a.P[a])  (∃a∈A.P[a] ⇐⇒ ∃a:coSet{i:l}. ((a ∈ A) ∧ P[a])))

Lemma: existssetmem_functionality
A:coSet{i:l}. ∀P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ. ∀B:coSet{i:l}.
  (set-predicate{i:l}(A;a.P[a])  seteq(A;B)  (∃a∈A.P[a] ⇐⇒ ∃a∈B.P[a]))

Definition: intersectionset
(s) ==  {x ∈ ⋃(s) | ∀z∈s.(x ∈ z)}

Lemma: intersectionset_wf
[s:coSet{i:l}]. (⋂(s) ∈ coSet{i:l})

Lemma: intersectionset_wf2
[s:Set{i:l}]. (⋂(s) ∈ Set{i:l})

Lemma: setmem-intersectionset
s,x:coSet{i:l}.  ((∃a:coSet{i:l}. (a ∈ s))  ((x ∈ ⋂(s)) ⇐⇒ ∀z:coSet{i:l}. ((z ∈ s)  (x ∈ z))))

Lemma: intersectionset_functionality
a,b:coSet{i:l}.  (seteq(a;b)  seteq(⋂(a);⋂(b)))

Definition: setsubset
(a ⊆ b) ==  ∀x∈a.(x ∈ b)

Lemma: setsubset_wf
[a,b:coSet{i:l}].  ((a ⊆ b) ∈ ℙ)

Lemma: setsubset-iff
a,b:coSet{i:l}.  ((a ⊆ b) ⇐⇒ ∀x:coSet{i:l}. ((x ∈ a)  (x ∈ b)))

Lemma: setsubset-iff2
a:Set{i:l}. ∀b:coSet{i:l}.  ((a ⊆ b) ⇐⇒ ∀x:Set{i:l}. ((x ∈ a)  (x ∈ b)))

Lemma: setsubset_functionality
a,b,a',b':coSet{i:l}.  (seteq(a;a')  seteq(b;b')  ((a ⊆ b) ⇐⇒ (a' ⊆ b')))

Lemma: seteq-iff-setsubset
a,b:coSet{i:l}.  (seteq(a;b) ⇐⇒ (a ⊆ b) ∧ (b ⊆ a))

Lemma: setsubset_transitivity
a,b,c:coSet{i:l}.  ((a ⊆ b)  (b ⊆ c)  (a ⊆ c))

Lemma: set-part-greatest
s:coSet{i:l}. ((set-part(s) ⊆ s) ∧ (∀x:Set{i:l}. ((x ⊆ s)  (x ⊆ set-part(s)))))

Lemma: cosetTC_functionality_subset
a,b:coSet{i:l}.  ((a ⊆ b)  (cosetTC(a) ⊆ cosetTC(b)))

Lemma: cosetTC_functionality
a,b:coSet{i:l}.  (seteq(a;b)  seteq(cosetTC(a);cosetTC(b)))

Lemma: cosetTC-set-function
s:coSet{i:l}. set-function{i:l}(s; a.cosetTC(a))

Lemma: cosetTC-contains
a:coSet{i:l}. (a ⊆ cosetTC(a))

Definition: orderedpair-fsts
orderedpair-fsts(pr) ==  ⋂(pr)

Lemma: orderedpair-fsts_wf
[pr:coSet{i:l}]. (orderedpair-fsts(pr) ∈ coSet{i:l})

Lemma: orderedpair-fsts_wf2
[pr:Set{i:l}]. (orderedpair-fsts(pr) ∈ Set{i:l})

Lemma: orderedpair-fsts_functionality
a,b:coSet{i:l}.  (seteq(a;b)  seteq(orderedpair-fsts(a);orderedpair-fsts(b)))

Lemma: orderedpair-first
a,b:coSet{i:l}.  seteq(orderedpair-fsts((a,b));{a})

Definition: orderedpair-fst
fst(pr) ==  singleitem(orderedpair-fsts(pr))

Lemma: orderedpair-fst_wf
[pr:coSet{i:l}]. (fst(pr) ∈ coSet{i:l})

Lemma: orderedpair-fst_wf2
[pr:Set{i:l}]. (fst(pr) ∈ Set{i:l})

Lemma: orderedpair-fst_functionality
a,b:coSet{i:l}.  (seteq(a;b)  seteq(fst(a);fst(b)))

Lemma: fst-orderedpairset
a,b:coSet{i:l}.  seteq(fst((a,b));a)

Definition: orderedpair-snds
snds(pr) ==  {x ∈ ⋃(pr) seteq(pr;(fst(pr),x))}

Lemma: orderedpair-snds_wf
[pr:coSet{i:l}]. (snds(pr) ∈ coSet{i:l})

Lemma: orderedpair-snds_wf2
[pr:Set{i:l}]. (snds(pr) ∈ Set{i:l})

Lemma: orderedpair-snds_functionality
a,b:coSet{i:l}.  (seteq(a;b)  seteq(snds(a);snds(b)))

Lemma: orderedpair-second
a,b:coSet{i:l}.  seteq(snds((a,b));{b})

Definition: orderedpair-snd
snd(pr) ==  singleitem(snds(pr))

Lemma: orderedpair-snd_wf
[pr:coSet{i:l}]. (snd(pr) ∈ coSet{i:l})

Lemma: orderedpair-snd_wf2
[pr:Set{i:l}]. (snd(pr) ∈ Set{i:l})

Lemma: orderedpair-snd_functionality
a,b:coSet{i:l}.  (seteq(a;b)  seteq(snd(a);snd(b)))

Lemma: snd-orderedpairset
a,b:coSet{i:l}.  seteq(snd((a,b));b)

Definition: transitive-set
We define ⌜transitive-set(s)⌝ using the ∀x∈s..... so that it will have
type ⌜ℙ⌝ rather than ⌜ℙ'⌝ (universe i+1) 
if had been defined: ∀x:Set{i:l}. ((x ∈ s)  (x ⊆ s)).
But these are equivalent. See transitive-set-iff.⋅

transitive-set(s) ==  ∀x∈s.(x ⊆ s)

Lemma: transitive-set_wf
[s:coSet{i:l}]. (transitive-set(s) ∈ ℙ)

Lemma: transitive-set-iff
s:coSet{i:l}. (transitive-set(s) ⇐⇒ ∀x:coSet{i:l}. ((x ∈ s)  (x ⊆ s)))

Lemma: transitive-set-iff2
s:Set{i:l}. (transitive-set(s) ⇐⇒ ∀x:Set{i:l}. ((x ∈ s)  (x ⊆ s)))

Lemma: transitive-set_functionality
s1,s2:coSet{i:l}.  (seteq(s1;s2)  (transitive-set(s1) ⇐⇒ transitive-set(s2)))

Lemma: plus-set-transitive
a:coSet{i:l}. (transitive-set(a)  transitive-set((a)+))

Lemma: emptyset-transitive

Lemma: loopset-transitive

Definition: natset
natset(n) ==  primrec(n;{};λi,r. (r)+)

Lemma: natset_wf
[n:ℕ]. (natset(n) ∈ Set{i:l})

Lemma: natset-transitive

Lemma: setmem-natset
n:ℕ. ∀x:Set{i:l}.  ((x ∈ natset(n)) ⇐⇒ ∃i:ℕn. seteq(x;natset(i)))

Lemma: natset-setmem-natset
n,m:ℕ.  ((natset(n) ∈ natset(m)) ⇐⇒ n < m)

Lemma: natset-subset-natset
n,m:ℕ.  ((natset(n) ⊆ natset(m)) ⇐⇒ n ≤ m)

Lemma: natset-seteq-natset
n,m:ℕ.  (seteq(natset(n);natset(m)) ⇐⇒ m ∈ ℤ)

Definition: omegaset
omegaset() ==  {natset(n) n ∈ ℕ}

Lemma: omegaset_wf
omegaset() ∈ Set{i:l}

Lemma: cosetTC-transitive
a:coSet{i:l}. transitive-set(cosetTC(a))

Lemma: cosetTC-least
a,s:coSet{i:l}.  ((a ⊆ s)  transitive-set(s)  (cosetTC(a) ⊆ s))

Lemma: cosetTC-contained
s:coSet{i:l}. (transitive-set(s)  (cosetTC(s) ⊆ s))

Lemma: cosetTC-unique
  ((a ⊆ s)
   (∀s':coSet{i:l}. ((a ⊆ s')  transitive-set(s')  (s ⊆ s')))

Definition: transmem
(x ∈∈ y) ==  TC(λx,y. (x ∈ y)) y

Lemma: transmem_wf
[x,y:coSet{i:l}].  ((x ∈∈ y) ∈ ℙ')

Lemma: setmem-transmem
x,y:coSet{i:l}.  ((x ∈ y)  (x ∈∈ y))

Lemma: transmem_transitivity
Trans(coSet{i:l};x,y.(x ∈∈ y))

Lemma: setTC_functionality_subset
b,a:Set{i:l}.  ((a ⊆ b)  (setTC(a) ⊆ setTC(b)))

Lemma: setTC_functionality
a,b:Set{i:l}.  (seteq(a;b)  seteq(setTC(a);setTC(b)))

Lemma: setTC-set-function
s:Set{i:l}. set-function{i:l}(s; a.setTC(a))

Lemma: setTC-contains
a:Set{i:l}. (a ⊆ setTC(a))

Lemma: setTC-transitive
a:Set{i:l}. transitive-set(setTC(a))

Lemma: setTC-least
a:Set{i:l}. ∀s:coSet{i:l}.  ((a ⊆ s)  transitive-set(s)  (setTC(a) ⊆ s))

Lemma: setTC-unique
  ((a ⊆ s)  transitive-set(s)  (∀s':Set{i:l}. ((a ⊆ s')  transitive-set(s')  (s ⊆ s')))  seteq(s;setTC(a)))

Lemma: setTC-cosetTC
a:Set{i:l}. seteq(setTC(a);cosetTC(a))

Lemma: setTC-induction
[P:Set{i:l} ⟶ ℙ']. ((∀a:Set{i:l}. ((∀x:Set{i:l}. ((x ∈ setTC(a))  P[x]))  P[a]))  (∀s:Set{i:l}. P[s]))

Definition: productset
==  let A,f in let B,g in <A × B, λp.let x,y in (f x,g y)>

Lemma: productset_wf
[a,b:coSet{i:l}].  (a b ∈ coSet{i:l})

Lemma: productset_wf2
[a,b:Set{i:l}].  (a b ∈ Set{i:l})

Lemma: setmem-productset
a,b,p:coSet{i:l}.  ((p ∈ b) ⇐⇒ ∃u,v:coSet{i:l}. ((u ∈ a) ∧ (v ∈ b) ∧ seteq(p;(u,v))))

Definition: sigmaset
Σa:A.B[a] ==  let T,f in <t:T × set-dom(B[f t]), λp.let t,s in (f t,set-item(B[f t];s))>

Lemma: sigmaset_wf
[A:coSet{i:l}]. ∀[B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}].  a:A.B[a] ∈ coSet{i:l})

Lemma: sigmaset_wf2
[A:Set{i:l}]. ∀[B:{a:Set{i:l}| (a ∈ A)}  ⟶ Set{i:l}].  a:A.B[a] ∈ Set{i:l})

Lemma: setmem-sigmaset
A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A)  (a2 ∈ A)  seteq(a1;a2)  seteq(B[a1];B[a2])))
   (∀x:coSet{i:l}. ((x ∈ Σa:A.B[a]) ⇐⇒ ∃a:coSet{i:l}. ((a ∈ A) ∧ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ seteq(x;(a,b))))))))

Definition: piset
piset(A;a.B[a]) ==  let T,f in <t:T ⟶ set-dom(B[f t]), λg.<T, λt.(f t,set-item(B[f t];g t))>>

Lemma: piset_wf
[A:coSet{i:l}]. ∀[B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}].  (piset(A;a.B[a]) ∈ coSet{i:l})

Lemma: piset_wf2
[A:Set{i:l}]. ∀[B:{a:Set{i:l}| (a ∈ A)}  ⟶ Set{i:l}].  (piset(A;a.B[a]) ∈ Set{i:l})

Lemma: setmem-piset-1
A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}. ∀x:coSet{i:l}.
  ((x ∈ piset(A;a.B[a]))
  ⇐⇒ ∃f:t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
       ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃t:set-dom(A). seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];f t)))))

Lemma: implies-setmem-piset
A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}. ∀x:coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A)  (a2 ∈ A)  seteq(a1;a2)  seteq(B[a1];B[a2])))
   ((x ⊆ Σa:A.B[a])
     ∧ (∀a:coSet{i:l}. ((a ∈ A)  (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ x)))))
     ∧ (∀a,b1,b2:coSet{i:l}.  ((a ∈ A)  (b1 ∈ B[a])  (b2 ∈ B[a])  ((a,b1) ∈ x)  ((a,b2) ∈ x)  seteq(b1;b2))))
   (x ∈ piset(A;a.B[a])))

Lemma: setmem-piset-implies
A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}. ∀x:coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A)  (a2 ∈ A)  seteq(a1;a2)  seteq(B[a1];B[a2])))
   (x ∈ piset(A;a.B[a]))
   ((x ⊆ Σa:A.B[a]) ∧ (∀a:coSet{i:l}. ((a ∈ A)  (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ x)))))))

Definition: singlevalued-graph
singlevalued-graph(A;a.B[a];grph) ==  ∀a∈A.∀b1∈B[a].∀b2∈B[a].((a,b1) ∈ grph)  ((a,b2) ∈ grph)  seteq(b1;b2)

Lemma: singlevalued-graph_wf
A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}. ∀x:coSet{i:l}.  (singlevalued-graph(A;a.B[a];x) ∈ ℙ)

Lemma: singlevalued-graph-iff
A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A)  (a2 ∈ A)  seteq(a1;a2)  seteq(B[a1];B[a2])))
        ⇐⇒ ∀a,b1,b2:coSet{i:l}.
              ((a ∈ A)  (b1 ∈ B[a])  (b2 ∈ B[a])  ((a,b1) ∈ x)  ((a,b2) ∈ x)  seteq(b1;b2)))))

Lemma: singlevalued-graph_functionality
A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A)  (a2 ∈ A)  seteq(a1;a2)  seteq(B[a1];B[a2])))
   (∀g1,g2:coSet{i:l}.  (seteq(g1;g2)  (singlevalued-graph(A;a.B[a];g1) ⇐⇒ singlevalued-graph(A;a.B[a];g2)))))

Definition: Piset
Πa:A.B[a] ==  {g ∈ piset(A;a.B[a]) singlevalued-graph(A;a.B[a];g)}

Lemma: Piset_wf
[A:coSet{i:l}]. ∀[B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}].  a:A.B[a] ∈ coSet{i:l})

Lemma: Piset_wf2
[A:Set{i:l}]. ∀[B:{a:Set{i:l}| (a ∈ A)}  ⟶ Set{i:l}].  a:A.B[a] ∈ Set{i:l})

Definition: function-graph
function-graph{i:l}(A;a.B[a];grph) ==
  (grph ⊆ Σa:A.B[a])
  ∧ (∀a:coSet{i:l}. ((a ∈ A)  (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ grph)))))
  ∧ (∀a,b1,b2:coSet{i:l}.
       ((a ∈ A)  (b1 ∈ B[a])  (b2 ∈ B[a])  ((a,b1) ∈ grph)  ((a,b2) ∈ grph)  seteq(b1;b2)))

Lemma: function-graph_wf
[A:coSet{i:l}]. ∀[B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}]. ∀[grph:coSet{i:l}].
  (function-graph{i:l}(A;a.B[a];grph) ∈ ℙ')

Lemma: setmem-Piset
A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}. ∀x:coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A)  (a2 ∈ A)  seteq(a1;a2)  seteq(B[a1];B[a2])))
   ((x ∈ Πa:A.B[a]) ⇐⇒ function-graph{i:l}(A;a.B[a];x)))

Definition: funset
A ⟶ ==  Πa:A.B

Lemma: funset_wf
[A,B:coSet{i:l}].  (A ⟶ B ∈ coSet{i:l})

Lemma: funset_wf2
[A,B:Set{i:l}].  (A ⟶ B ∈ Set{i:l})

Lemma: setmem-funset
A,B,x:coSet{i:l}.  ((x ∈ A ⟶ B) ⇐⇒ function-graph{i:l}(A;_.B;x))

Definition: imageset
imageset(B;f) ==  {b ∈ | ∃pr∈f.seteq(b;snd(pr))}

Lemma: imageset_wf
[B,f:coSet{i:l}].  (imageset(B;f) ∈ coSet{i:l})

Lemma: imageset_wf2
[B,f:Set{i:l}].  (imageset(B;f) ∈ Set{i:l})

Lemma: setmem-imageset
B,f,x:coSet{i:l}.  ((x ∈ imageset(B;f)) ⇐⇒ (x ∈ B) ∧ (∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(x;snd(pr)))))

Lemma: imageset_functionality
B1,B2,f1,f2:coSet{i:l}.  (seteq(B1;B2)  seteq(f1;f2)  seteq(imageset(B1;f1);imageset(B2;f2)))

Definition: setimages
setimages(A;B) ==   ⋃f∈A ⟶ B.{imageset(B;f)}

Lemma: setimages_wf
[A,B:coSet{i:l}].  (setimages(A;B) ∈ coSet{i:l})

Lemma: setimages_wf2
[A,B:Set{i:l}].  (setimages(A;B) ∈ Set{i:l})

Lemma: setmem-setimages
  ((x ∈ setimages(A;B))
  ⇐⇒ ∃f:coSet{i:l}
       (function-graph{i:l}(A;_.B;f) ∧ (∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr)))))))

Definition: itersetfun
itersetfun(s.G[s];a) ==  G[ ⋃x∈a.itersetfun(s.G[s];x)]

Lemma: itersetfun_wf
[G:Set{i:l} ⟶ Set{i:l}]. ∀[a:Set{i:l}].  (itersetfun(x.G[x];a) ∈ Set{i:l})

Lemma: itersetfun_functionality_subset
G:Set{i:l} ⟶ Set{i:l}
  ((∀a,b:Set{i:l}.  ((a ⊆ b)  (G[a] ⊆ G[b])))
   (∀b,a:Set{i:l}.  ((a ⊆ b)  (itersetfun(x.G[x];a) ⊆ itersetfun(x.G[x];b)))))

Lemma: itersetfun_functionality
G:Set{i:l} ⟶ Set{i:l}
  ((∀a,b:Set{i:l}.  ((a ⊆ b)  (G[a] ⊆ G[b])))
   (∀b,a:Set{i:l}.  (seteq(a;b)  seteq(itersetfun(x.G[x];a);itersetfun(x.G[x];b)))))

Lemma: itersetfun-subset-fixpoint
G:Set{i:l} ⟶ Set{i:l}
  ((∀a,b:Set{i:l}.  ((a ⊆ b)  (G[a] ⊆ G[b])))
   (∀X:Set{i:l}. ((G[X] ⊆ X)  (∀a:Set{i:l}. (itersetfun(x.G[x];a) ⊆ X)))))

Definition: coset-relation
coSetRelation(R) ==  ∀x,x',y,y':coSet{i:l}.  (seteq(x;x')  seteq(y;y')  (R y)  (R x' y'))

Lemma: coset-relation_wf
[R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ']. (coSetRelation(R) ∈ ℙ')

Definition: set-relation
This says that the relation respects the extensional equality ⌜seteq(x;y)⌝.⋅

SetRelation(R) ==  ∀x,x',y,y':Set{i:l}.  (seteq(x;x')  seteq(y;y')  (R y)  (R x' y'))

Lemma: set-relation_wf
[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. (SetRelation(R) ∈ ℙ')

Definition: set-relation-on
SetRelationOn(A;R) ==  ∀x,x',y,y':{u:Set{i:l}| (u ∈ A)} .  (seteq(x;x')  seteq(y;y')  (R y)  (R x' y'))

Lemma: set-relation-on_wf
[A:Set{i:l}]. ∀[R:{u:Set{i:l}| (u ∈ A)}  ⟶ {u:Set{i:l}| (u ∈ A)}  ⟶ ℙ'].  (SetRelationOn(A;R) ∈ ℙ')

Definition: mv-map
This says that the relation relates every member of 
to at least one member of B. So it is "multi-valued map" from to B.⋅

 R:(A  B) ==  ∀x:coSet{i:l}. ((x ∈ A)  (∃y:coSet{i:l}. ((y ∈ B) ∧ (R y))))

Lemma: mv-map_wf
[A,B:coSet{i:l}]. ∀[R:{u:coSet{i:l}| (u ∈ A)}  ⟶ {v:coSet{i:l}| (v ∈ B)}  ⟶ ℙ'].  R:(A  B) ∈ ℙ')

Definition: onto-map
This says that relation maps onto B. ⋅

R:(A ─>> B) ==  ∀y:coSet{i:l}. ((y ∈ B)  (∃x:coSet{i:l}. ((x ∈ A) ∧ (R y))))

Lemma: onto-map_wf
[A,B:coSet{i:l}]. ∀[R:{u:coSet{i:l}| (u ∈ A)}  ⟶ {v:coSet{i:l}| (v ∈ B)}  ⟶ ℙ'].  (R:(A ─>> B) ∈ ℙ')

Definition: setrel
Any set determines relation on sets.
It is extensional (i.e. set-relation-setrel).⋅

setrel(R) ==  λx,y. ((x,y) ∈ R)

Lemma: setrel_wf
[R:coSet{i:l}]. (setrel(R) ∈ coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ)

Lemma: set-relation-setrel
R:coSet{i:l}. SetRelation(setrel(R))

Lemma: coset-relation-setrel
R:coSet{i:l}. coSetRelation(setrel(R))

Lemma: set-relation-on-setrel
R,A:Set{i:l}.  SetRelationOn(A;setrel(R))

Definition: regularset
transitive set is regular if for every set that is multi-valued
map from member, B, to the whole set A, the range of the map R
is set  in A. ⋅

regular(A) ==
  ∧ (∀B:coSet{i:l}
       ((B ∈ A)
             setrel(R):(B  A)  (∃b:coSet{i:l}. ((b ∈ A) ∧  setrel(R):(B  b) ∧ setrel(R):(B ─>> b)))))))

Lemma: regularset_wf
[A:coSet{i:l}]. (regular(A) ∈ ℙ')

Definition: Regularcoset
cRegular(A) ==
  ∧ (∀B:coSet{i:l}
       ((B ∈ A)
        (∀R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
             (coSetRelation(R)   R:(B  A)  (∃b:coSet{i:l}. ((b ∈ A) ∧  R:(B  b) ∧ R:(B ─>> b)))))))

Lemma: Regularcoset_wf
[A:coSet{i:l}]. (cRegular(A) ∈ ℙ{i''})

Definition: Regularset
Regular(A) is generalization of regular(A) where the relation R
can be any extensional relation (not necessarily given by set).

So, Regular(A)  regular(A) (see Regularset-regularset).
Aczel's "regular extension axiom" is that every set is subset of
regular set (in fact of Regular set).

see RegularExtension ⋅

Regular(A) ==
  ∧ (∀B:Set{i:l}
       ((B ∈ A)
        (∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
             (SetRelation(R)   R:(B  A)  (∃b:Set{i:l}. ((b ∈ A) ∧  R:(B  b) ∧ R:(B ─>> b)))))))

Lemma: Regularset_wf
[A:Set{i:l}]. (Regular(A) ∈ ℙ{i''})

Lemma: Regularset-regularset
A:Set{i:l}. (Regular(A)  regular(A))

Lemma: Regularcoset-regularset
A:coSet{i:l}. (cRegular(A)  regular(A))

Definition: regextfun
regextfun(f;w)==r let t,g in λu.regextfun(f;g u)"(set-dom(f t))

Lemma: regextfun_wf
[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[w:coW(T;x.set-dom(f x))].  (regextfun(f;w) ∈ coSet{i:l})

Lemma: regextfun_wf2
[T:Type]. ∀[f:T ⟶ Set{i:l}]. ∀[w:W(T;x.set-dom(f x))].  (regextfun(f;w) ∈ Set{i:l})

Definition: regext
By forming set indexed by suitable type, we get Regular set for which
(a ⊆ r) provided that set is transitive.
See subset-regext and regext-Regularset.⋅

regext(a) ==  let T,f in λw.regextfun(f;w)"(W(T;x.set-dom(f x)))

Lemma: regext_wf
[a:coSet{i:l}]. (regext(a) ∈ coSet{i:l})

Lemma: regext_wf2
[a:Set{i:l}]. (regext(a) ∈ Set{i:l})

Lemma: regext-transitive
a:coSet{i:l}. transitive-set(regext(a))

Lemma: regext-lemma1
T:Type. ∀f:T ⟶ coSet{i:l}. ∀B:coSet{i:l}.
  ((∃t:T. ∃g:set-dom(f t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(f t);g)))
   (∀R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
          R:(B  regext(mk-coset(T;f)))
         (∃b:coSet{i:l}. ((b ∈ regext(mk-coset(T;f))) ∧  R:(B  b) ∧ R:(B ─>> b))))))

Lemma: regext-lemma
T:Type. ∀f:T ⟶ Set{i:l}. ∀B:Set{i:l}.
  ((∃t:T. ∃g:set-dom(f t) ⟶ Set{i:l}. seteq(B;g"(set-dom(f t))))
   (∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
          R:(B  regext(f"(T)))
         (∃b:Set{i:l}. ((b ∈ regext(f"(T))) ∧  R:(B  b) ∧ R:(B ─>> b))))))

Lemma: regext-Regularcoset
a:coSet{i:l}. cRegular(regext(a))

Lemma: regext-Regularset
a:Set{i:l}. Regular(regext(a))

Lemma: subset-regext
a:Set{i:l}. (transitive-set(a)  (a ⊆ regext(a)))

Lemma: RegularExtension
a:Set{i:l}. ∃r:Set{i:l}. ((a ⊆ r) ∧ Regular(r))

Lemma: regularExtension
a:Set{i:l}. ∃r:Set{i:l}. ((a ⊆ r) ∧ regular(r))

Lemma: regext-loopset-empty
Now we do get ⌜(loopset() ⊆ co-regext(loopset()))⌝because the type
coW(Unit;x.Unit)⌝ has single member (while the corresponding type
W(Unit;x.Unit)⌝ is empty).  So the needed property
⌜∀a:coSet{i:l}. (transitive-set(a)  (a ⊆ co-regext(a)))⌝ could be true??..⋅


Definition: co-regext
co-regext(a) ==  let T,f in mk-coset(coW(T;x.set-dom(f x));λw.regextfun(f;w))

Lemma: co-regext_wf
[a:coSet{i:l}]. (co-regext(a) ∈ coSet{i:l})

Lemma: co-regext-transitive
a:coSet{i:l}. transitive-set(co-regext(a))

Lemma: co-regext-lemma
T:Type. ∀f:T ⟶ coSet{i:l}. ∀B:coSet{i:l}.
  ((∃t:T. ∃g:set-dom(f t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(f t);g)))
   (∀R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
          R:(B  co-regext(mk-coset(T;f)))
         (∃b:coSet{i:l}. ((b ∈ co-regext(mk-coset(T;f))) ∧  R:(B  b) ∧ R:(B ─>> b))))))

Lemma: co-regext-Regularcoset
The proof that ⌜co-regext(a)⌝ is regular goes through as before, just
using co- versions of everything.⋅

a:coSet{i:l}. cRegular(co-regext(a))

Lemma: co-regext-loopset
Now we do get ⌜(loopset() ⊆ co-regext(loopset()))⌝because the type
coW(Unit;x.Unit)⌝ has single member (while the corresponding type
W(Unit;x.Unit)⌝ is empty).  So the needed property
⌜∀a:coSet{i:l}. (transitive-set(a)  (a ⊆ co-regext(a)))⌝ could be true??..⋅


Lemma: subset-co-regext-1
a:coSet{i:l}. (transitive-set(a)  (∀x:Set{i:l}. ((x ∈ a)  (x ∈ co-regext(a)))))

Definition: regextW
regextW(G;t)==r Wsup(t;λi.regextW(G;G i))

Lemma: regextW_wf
[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[G:i:T ⟶ j:set-dom(f i) ⟶ T]. ∀[t:T].  (regextW(G;t) ∈ coW(T;x.set-dom(f x)))

Lemma: subset-co-regext
a:coSet{i:l}. (transitive-set(a)  (a ⊆ co-regext(a)))

Definition: relclosed-set
closed(x,a.R[x; a])s ==  ∀x,a:Set{i:l}.  ((x ⊆ s)  R[x; a]  (a ∈ s))

Lemma: relclosed-set_wf
[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀[s:Set{i:l}].  (closed(x,a.R[x;a])s ∈ ℙ')

Definition: mem-mk-set
mem-mk-set(f;t) ==  <t, seteqweaken(f t) Ax>

Lemma: mem-mk-set_wf
[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[t:T].  (mem-mk-set(f;t) ∈ (f t ∈ mk-coset(T;f)))

Lemma: mem-mk-set_wf2
[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[t:T].  (mem-mk-set(f;t) ∈ (f t ∈ f"(T)))

Definition: setimage
setimage{i:l}(x;b) ==
  ∃f:(z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
   ((∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2))  seteq(f z1;f z2)))
   ∧ (∀y:coSet{i:l}. ((y ∈ x) ⇐⇒ ∃z:z:coSet{i:l} × (z ∈ b). seteq(y;f z))))

Lemma: setimage_wf
[x,b:coSet{i:l}].  (setimage{i:l}(x;b) ∈ ℙ')

Definition: set-image
set-image(f;b) ==  let T,g in <T, λt.(f <t, mem-mk-set(g;t)>)>

Lemma: set-image_wf
[b:coSet{i:l}]. ∀[f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}].  (set-image(f;b) ∈ coSet{i:l})

Lemma: set-image_wf2
[b:coSet{i:l}]. ∀[f:(x:coSet{i:l} × (x ∈ b)) ⟶ Set{i:l}].  (set-image(f;b) ∈ Set{i:l})

Lemma: setmem-image
b:coSet{i:l}. ∀f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}.
  ((∀z1,z2:x:coSet{i:l} × (x ∈ b).  (seteq(fst(z1);fst(z2))  seteq(f z1;f z2)))
   (∀y:coSet{i:l}. ((y ∈ set-image(f;b)) ⇐⇒ ∃x:x:coSet{i:l} × (x ∈ b). seteq(y;f x))))

Lemma: setimage-iff
  ⇐⇒ ∃f:(z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
       ((∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2))  seteq(f z1;f z2))) ∧ seteq(x;set-image(f;b))))

Definition: fun-graph
fun-graph(b;f) ==  let T,g in <T, λt.(g t,f <t, mem-mk-set(g;t)>)>

Lemma: fun-graph_wf
[b:coSet{i:l}]. ∀[f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}].  (fun-graph(b;f) ∈ coSet{i:l})

Lemma: fun-graph_wf2
[b:Set{i:l}]. ∀[f:(x:Set{i:l} × (x ∈ b)) ⟶ Set{i:l}].  (fun-graph(b;f) ∈ Set{i:l})

Lemma: setmem-fun-graph
b:coSet{i:l}. ∀f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}.
  ((∀z1,z2:x:coSet{i:l} × (x ∈ b).  (seteq(fst(z1);fst(z2))  seteq(f z1;f z2)))
   (∀y:coSet{i:l}. ((y ∈ fun-graph(b;f)) ⇐⇒ ∃p:x:coSet{i:l} × (x ∈ b). seteq(y;(fst(p),f p)))))

Lemma: function-graph-fun-graph
b:coSet{i:l}. ∀f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}.
  ((∀z1,z2:x:coSet{i:l} × (x ∈ b).  (seteq(fst(z1);fst(z2))  seteq(f z1;f z2)))
   (∀x:coSet{i:l}. ((set-image(f;b) ⊆ x)  function-graph{i:l}(b;_.x;fun-graph(b;f)))))

Lemma: setmem-setimages-2
A,b,x:coSet{i:l}.  ((A ∈ setimages(b;x)) ⇐⇒ setimage{i:l}(A;b) ∧ (A ⊆ x))

Lemma: setimages_functionality
b1,b2,x1,x2:coSet{i:l}.  (seteq(b1;b2)  seteq(x1;x2)  seteq(setimages(b1;x1);setimages(b2;x2)))

Definition: bounded-relation
Bounded(x,a.R[x; a]) ==
  (∀x1,x2,a1,a2:Set{i:l}.  (seteq(x1;x2)  seteq(a1;a2)  R[x1; a1]  R[x2; a2]))
  ∧ (∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x; a] ⇐⇒ (a ∈ y)))
  ∧ (∃B:Set{i:l}. ∀x,a:Set{i:l}.  (R[x; a]  (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))

Lemma: bounded-relation_wf
[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. (Bounded(x,a.R[x;a]) ∈ ℙ')

Definition: inductively-defined
inductively-defined{i:l}(x,a.R[x; a];s) ==  closed(x,a.R[x; a])s ∧ (∀s':Set{i:l}. (closed(x,a.R[x; a])s'  (s ⊆ s')))

Lemma: inductively-defined_wf
[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀[s:Set{i:l}].  (inductively-defined{i:l}(x,a.R[x;a];s) ∈ ℙ')

Lemma: inductively-defined-unique
R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'. ∀s1,s2:Set{i:l}.
  (inductively-defined{i:l}(x,a.R[x;a];s1)  inductively-defined{i:l}(x,a.R[x;a];s2)  seteq(s1;s2))

Definition: least-closed-set
By iterating over all the members of regular set containg the transitive
closure of set we can form the least set closed under function G,
provided that is bound for in suitable sense.
(Spelled out in the lemma least-closed-set-inductively-defined).⋅

least-closed-set(B;G) ==   ⋃a∈regext(setTC(B)).itersetfun(x.G x;a)

Lemma: least-closed-set_wf
[B:Set{i:l}]. ∀[G:Set{i:l} ⟶ Set{i:l}].  (least-closed-set(B;G) ∈ Set{i:l})

Lemma: least-closed-set-inductively-defined
[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']
  ∀B:Set{i:l}. ∀G:Set{i:l} ⟶ Set{i:l}.
    ((∀x,a:Set{i:l}.  (R[x;a]  (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))
     (∀x,z:Set{i:l}.  ((z ∈ x) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ R[A;z])))

Definition: closure-set
closure-set(B;Y;x) is the set of things we need to add to set x
(iteratively) to eventually close under function Y.
The bound makes this possible.⋅

closure-set(B;Y;x) ==   ⋃b∈B. ⋃A∈setimages(b;x).Y A

Lemma: closure-set_wf
[B:Set{i:l}]. ∀[Y:Set{i:l} ⟶ Set{i:l}]. ∀[x:Set{i:l}].  (closure-set(B;Y;x) ∈ Set{i:l})

Lemma: setmem-closure-set
B:Set{i:l}. ∀Y:Set{i:l} ⟶ Set{i:l}. ∀x:Set{i:l}.
  ((∀b:Set{i:l}. ((b ∈ B)  set-function{i:l}(setimages(b;x); A.Y A)))
        ((z ∈ closure-set(B;Y;x)) ⇐⇒ ∃b:coSet{i:l}. ((b ∈ B) ∧ (∃A:coSet{i:l}. ((A ∈ setimages(b;x)) ∧ (z ∈ A)))))))

Lemma: closure-set-property
B,x:Set{i:l}. ∀Y:x1:Set{i:l} ⟶ Set{i:l}.
  ((∀x1,x2,a1,a2:Set{i:l}.  (seteq(x1;x2)  seteq(a1;a2)  (a1 ∈ x1)  (a2 ∈ x2)))
   (∀x,a:Set{i:l}.  ((a ∈ x)  (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))
   (∀z:Set{i:l}. ((z ∈ closure-set(B;Y;x)) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ (z ∈ A)))))

Definition: inductive-set
If bdd witnesses ⌜Bounded(A,a.R[A;a])⌝ then 
for _,S,B,_ bdd,  is bound on the "cardinality" of the A's
and ⌜λA.(fst((S A)))⌝ is the set {a R[A;a]}.

For any set x, the set ⌜closure-set(B;λA.(fst((S A)));x)⌝ will contain
all the sets for which R[A;a] for some ⌜(A ⊆ x)⌝.

So, the set defined inductively by is the closure of the
function ⌜λx.closure-set(B;λA.(fst((S A)));x)⌝.

This is proved in inductive-set-property.⋅

inductive-set(bdd) ==  let _,S,B,_ bdd in least-closed-set(B;λx.closure-set(B;λz.(fst((S z)));x))  

Lemma: inductive-set_wf
[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀[bdd:Bounded(x,a.R[x;a])].  (inductive-set(bdd) ∈ Set{i:l})

Lemma: inductive-set-property
[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀bdd:Bounded(x,a.R[x;a]). inductively-defined{i:l}(x,a.R[x;a];inductive-set(bdd))

Definition: funclosed-set
f-closed(s) ==  ∀x:Set{i:l}. ((x ⊆ s)  (f x ⊆ s))

Lemma: funclosed-set_wf
[f:Set{i:l} ⟶ Set{i:l}]. ∀[s:Set{i:l}].  (f-closed(s) ∈ ℙ')

Lemma: relclosed-iff-funclosed
R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ
  ((∀x:Set{i:l}. ∃y:Set{i:l}. ∀a:Set{i:l}. (R[x;a] ⇐⇒ (a ∈ y)))
   (∃f:Set{i:l} ⟶ Set{i:l}. ∀s:Set{i:l}. (closed(x,a.R[x;a])s ⇐⇒ f-closed(s))))

Definition: injectively-presented
InjectivelyPresented(s) ==  Inj(set-dom(s);Set{i:l};λx.set-item(s;x))

Lemma: injectively-presented_wf
[s:Set{i:l}]. (InjectivelyPresented(s) ∈ ℙ')

Lemma: injectively-presented-emptyset

Lemma: injectively-presented-singleset
a:Set{i:l}. InjectivelyPresented({a})

Definition: injectively-presentable
InjectivelyPresentable(a) ==  ∃b:Set{i:l}. (InjectivelyPresented(b) ∧ seteq(a;b))

Lemma: injectively-presentable_wf
[a:Set{i:l}]. (InjectivelyPresentable(a) ∈ ℙ')

Lemma: injectively-presented-presentable
a:Set{i:l}. (InjectivelyPresented(a)  InjectivelyPresentable(a))

Definition: WtoSet
WtoSet(a.B[a];x) ==  let a,f in λb.WtoSet(a.B[a];f b)"(B[a])

Lemma: WtoSet_wf
[A:Type]. ∀[B:A ⟶ Type]. ∀[x:W(A;a.B[a])].  (WtoSet(a.B[a];x) ∈ Set{i:l})

Lemma: WtoSet-order-preserving
[A:Type]. ∀[B:A ⟶ Type].
  ∀x,y:W(A;a.B[a]). ∀b:𝔹.  ((x Wcmp(A;a.B[a];b) y)  (WtoSet(a.B[a];x) Wcmp(Type;a.a;b) WtoSet(a.B[a];y)))

Home Index