---

Lemma: subtype_rel_dep_function_iff
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  (uiff(∀[a:C]. (B[a] ⊆r D[a]);(a:A ⟶ B[a]) ⊆r (c:C ⟶ D[c]))) supposing 
     ((∀x,y:A.  Dec(x = y ∈ A)) and 
     (a:A ⟶ B[a]) and 
     (C ⊆r A))

Definition: type-continuous
Continuous(T.F[T]) ==  ∀[X:ℕ ⟶ Type]. ((⋂n:ℕ. F[X n]) ⊆r F[⋂n:ℕ. (X n)])

Lemma: type-continuous_wf
∀[F:Type ⟶ Type]. (Continuous(t.F[t]) ∈ ℙ')

Definition: strong-type-continuous
Continuous+(T.F[T]) ==  ∀[X:ℕ ⟶ Type]. ⋂n:ℕ. F[X n] ≡ F[⋂n:ℕ. (X n)]

Lemma: strong-type-continuous_wf
∀[F:Type ⟶ Type]. (Continuous+(t.F[t]) ∈ ℙ')

Definition: type-monotone
Monotone(T.F[T]) ==  ∀[A,B:Type].  F[A] ⊆r F[B] supposing A ⊆r B

Lemma: type-monotone_wf
∀[F:Type ⟶ Type]. (Monotone(T.F[T]) ∈ ℙ')

Lemma: strong-continuous-isect2
∀[F,G:Type ⟶ Type].  (Continuous+(T.F[T] ⋂ G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))

Definition: continuous-monotone
ContinuousMonotone(T.F[T]) ==  Monotone(T.F[T]) ∧ Continuous(T.F[T])

Lemma: continuous-monotone_wf
∀[F:Type ⟶ Type]. (ContinuousMonotone(T.F[T]) ∈ ℙ')

Lemma: continuous-monotone-depfunction
∀[A:Type]. ∀[F:Type ⟶ A ⟶ Type].  ContinuousMonotone(T.a:A ⟶ F[T;a]) supposing ∀a:A. ContinuousMonotone(T.F[T;a])

Lemma: continuous-function
∀[A,B:Type ⟶ Type].  (Continuous(T.A[T] ⟶ B[T])) supposing (Continuous(T.B[T]) and Continuous+(T.A[T]))

Lemma: strong-continuous-function
∀[F:Type ⟶ Type]. ∀[A:Type].  Continuous+(T.A ⟶ F[T]) supposing Continuous+(T.F[T])

Lemma: continuous-monotone-function
∀[F:Type ⟶ Type]. ∀[A:Type]. ContinuousMonotone(T.A ⟶ F[T]) supposing ContinuousMonotone(T.F[T])

Lemma: strong-continuous-product
∀[F,G:Type ⟶ Type].  (Continuous+(T.F[T] × G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))

Lemma: continuous-monotone-product
∀[F,G:Type ⟶ Type].
  (ContinuousMonotone(T.F[T] × G[T])) supposing (ContinuousMonotone(T.G[T]) and ContinuousMonotone(T.F[T]))

Lemma: continuous-monotone-depproduct
∀[F:Type ⟶ Type]. ∀[G:T:Type ⟶ F[T] ⟶ Type].
  (ContinuousMonotone(T.x:F[T] × G[T;x])) supposing 
     ((∀X:ℕ ⟶ Type. ∀x:⋂n:ℕ. F[X n].  ((⋂n:ℕ. G[X n;x]) ⊆r G[⋂n:ℕ. (X n);x])) and 
     (∀A,B:Type.  ((A ⊆r B) ⇒ (∀x:F[A]. (G[A;x] ⊆r G[B;x])))) and 
     ContinuousMonotone(T.F[T]))

Lemma: strong-continuous-depproduct
∀[A:Type]. ∀[G:T:Type ⟶ A ⟶ Type].  Continuous+(T.x:A × G[T;x]) supposing ∀a:A. Continuous+(T.G[T;a])

Lemma: continuous-monotone-set
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[F:Type ⟶ Type].
  (ContinuousMonotone(T.{x:F[T]| P[x]} )) supposing ((∀T:Type. (F[T] ⊆r A)) and ContinuousMonotone(T.F[T]))

Lemma: strong-continuous-set
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[F:Type ⟶ Type].
  (Continuous+(T.{x:F[T]| P[x]} )) supposing (Continuous+(T.F[T]) and (∀T:Type. (F[T] ⊆r A)))

Lemma: strong-continuous-union
∀[F,G:Type ⟶ Type].  (Continuous+(T.F[T] + G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))

Lemma: b-union-void
∀[V,T:Type].  ((V ⋃ T) ⊆r T) ∧ ((T ⋃ V) ⊆r T) supposing ¬V

Lemma: continuous-monotone-union
∀F,G:Type ⟶ Type.  (ContinuousMonotone(T.F[T]) ⇒ ContinuousMonotone(T.G[T]) ⇒ ContinuousMonotone(T.F[T] + G[T]))

Lemma: continuous-monotone-isect
∀[A:Type]. ∀[F:A ⟶ Type ⟶ Type].  ContinuousMonotone(T.⋂a:A. F[a;T]) supposing ∀a:A. ContinuousMonotone(T.F[a;T])

Lemma: continuous-constant
∀[G:Type]. Continuous+(T.G)

Lemma: continuous-monotone-constant
∀[G:Type]. ContinuousMonotone(T.G)

Lemma: continuous-id
Continuous+(T.T)

Lemma: continuous-monotone-id
ContinuousMonotone(T.T)

Definition: union-continuous
union-continuous{i:l}(T.F[T]) ==  ∀[I:Type]. ∀[X:I ⟶ Type].  (⋃n:I.F[X n] ⊆r F[⋃n:I.(X n)])

Lemma: union-continuous_wf
∀[F:Type ⟶ Type]. (union-continuous{i:l}(T.F[T]) ∈ ℙ')

Lemma: type-monotone-union-continuous
∀[F:Type ⟶ Type]. union-continuous{i:l}(T.F[T]) supposing Monotone(T.F[T])

Lemma: union-continuous-type-monotone
∀[F:Type ⟶ Type]. (Monotone(T.F[T])) supposing (union-continuous{i:l}(T.F[T]) and (∀A,B:Type.  (A ≡ B ⇒ F[A] ≡ F[B])))

Lemma: int_sq
SQType(ℤ)

Lemma: nat_sq
SQType(ℕ)

Lemma: atom_sq
SQType(Atom)

Lemma: eq_atom_eq_false_elim_sqequal
∀[x,y:Atom].  ¬(x = y ∈ Atom) supposing x =a y ~ ff

Lemma: eq_atom_eq_true_elim_sqequal
∀[x,y:Atom].  x = y ∈ Atom supposing x =a y ~ tt

Lemma: lt_int_eq_false_elim_sqequal
∀[i,j:ℤ].  ¬i < j supposing i <z j ~ ff

Lemma: lt_int_eq_true_elim_sqequal
∀[i,j:ℤ].  i < j supposing i <z j ~ tt

Lemma: eq_int_eq_false_elim_sqequal
∀[i,j:ℤ].  i ≠ j supposing (i =z j) ~ ff

Lemma: eq_int_eq_true_elim_sqequal
∀[i,j:ℤ].  i = j ∈ ℤ supposing (i =z j) ~ tt

Lemma: uimplies_subtype
∀[A,B:Type]. ∀[P:ℙ].  (A supposing P ⊆r B) supposing ((A ⊆r B) and P)

Lemma: isect_subtype
∀[A1:Type]. ∀[B1:A1 ⟶ ℙ]. ∀[A2:Type]. ∀[B2:A2 ⟶ ℙ].
  ((⋂x:A1. B1[x]) ⊆r (⋂x:A2. B2[x])) supposing ((∀x:A2. (B1[x] ⊆r B2[x])) and (A2 ⊆r A1))

Lemma: equal_subtype
∀[A,B:Type]. ∀[a1,a2:A]. ∀[b1,b2:B].  (a1 = a2 ∈ A) ⊆r (b1 = b2 ∈ B) supposing (a1 = a2 ∈ A) ⇒ (b1 = b2 ∈ B)

Lemma: bunion-value-type
∀[A,B:Type].  (value-type(A ⋃ B)) supposing (value-type(B) and value-type(A))

Lemma: bunion-valueall-type
∀[A,B:Type].  (valueall-type(A ⋃ B)) supposing (valueall-type(B) and valueall-type(A))

Lemma: isect2_functionality_wrt_subtype_rel
∀[A1,B1,A2,B2:Type].  (A1 ⋂ B1 ⊆r A2 ⋂ B2) supposing ((A1 ⊆r A2) and (B1 ⊆r B2))

Lemma: equal-in-subtype-implies
∀[A,B:Type]. ∀[x,y:A].  (x = y ∈ B) supposing ((x = y ∈ A) and (A ⊆r B))

Lemma: function-subtype-top
∀[A,B:Type].  ((A ⟶ B) ⊆r Top)

Lemma: top-subtype-function
∀[A,B:Type].  Top ⊆r (A ⟶ B) supposing ¬A

Definition: strong-subtype
strong-subtype(A;B) ==  (A ⊆r B) c∧ ({b:B| ∃a:A. (b = a ∈ B)}  ⊆r A)

Lemma: strong-subtype_wf
∀[A,B:Type].  (strong-subtype(A;B) ∈ ℙ)

Lemma: strong-subtype-iff-respects-equality
∀[A,B:Type].  uiff(strong-subtype(A;B);(A ⊆r B) ∧ respects-equality(B;A))

Lemma: strong-subtype-iff-preserves-singleton
∀[A,B:Type].  uiff(strong-subtype(A;B);(A ⊆r B) ∧ (∀a:A. ({a:B} ⊆r {a:A})))

Lemma: strong-subtype-implies
∀[A,B:Type].  (strong-subtype(A;B) ⇒ {∀b:B. ∀a:A.  ((b = a ∈ B) ⇒ (b = a ∈ A))})

Lemma: strong-subtype_witness
∀[A,B:Type].  (strong-subtype(A;B) ⇒ (<Ax, Ax> ∈ strong-subtype(A;B)))

Lemma: strong-subtype-self
∀[A:Type]. strong-subtype(A;A)

Lemma: strong-subtype-equal
∀[A,B:Type].  strong-subtype(A;B) supposing A = B ∈ Type

Lemma: strong-subtype-ext-equal
∀[A,B:Type].  (strong-subtype(A;B)) supposing ((A ⊆r B) and (B ⊆r A))

Lemma: strong-subtype_transitivity
∀[A,B,C:Type].  (strong-subtype(A;C)) supposing (strong-subtype(B;C) and strong-subtype(A;B))

Lemma: strong-subtype_functionality
∀[A1,B1,A2,B2:Type].  (A1 ≡ A2 ⇒ B1 ≡ B2 ⇒ strong-subtype(A1;B1) ⇒ strong-subtype(A2;B2))

Lemma: strong-subtype-void
∀[T:Type]. strong-subtype(Void;T)

Lemma: strong-subtype-set
∀[A,B:Type].  ∀[P:A ⟶ ℙ]. ∀[Q:B ⟶ ℙ].  strong-subtype({x:A| P[x]} ;{x:B| Q[x]} ) supposing ∀x:A. (P[x] ⇒ Q[x]) suppos\000Cing strong-subtype(A;B)

Lemma: strong-subtype-set1
∀[A:Type]. ∀[P,Q:A ⟶ ℙ].  strong-subtype({x:A| P[x]} ;{x:A| Q[x]} ) supposing ∀x:A. (P[x] ⇒ Q[x])

Lemma: strong-subtype-set2
∀[A:Type]. ∀[P:A ⟶ ℙ].  strong-subtype({x:A| P[x]} ;A)

Lemma: strong-subtype-set3
∀[A,B:Type]. ∀[P:A ⟶ ℙ].  strong-subtype({x:A| P[x]} ;B) supposing strong-subtype(A;B)

Lemma: strong-subtype-product
∀[A,B,C,D:Type].  (strong-subtype(A × B;C × D)) supposing (strong-subtype(B;D) and strong-subtype(A;C))

Lemma: strong-subtype-dep-product
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  (strong-subtype(a:A × B[a];c:C × D[c])) supposing ((∀a:A. strong-subtype(B[a];D[a])) and strong-subtype(A;C))

Lemma: strong-subtype-union
∀[A,B,C,D:Type].  (strong-subtype(A + B;C + D)) supposing (strong-subtype(B;D) and strong-subtype(A;C))

Lemma: strong-subtype-eq1
∀[A,B:Type]. ∀[b:B]. ∀[a:A].  ((b ∈ A) c∧ (b = a ∈ A)) supposing ((b = a ∈ B) and strong-subtype(A;B))

Lemma: strong-subtype-eq2
∀[A,B:Type]. ∀[b:B]. ∀[a:A].  (b = a ∈ A) supposing ((b = a ∈ B) and strong-subtype(A;B))

Lemma: strong-subtype-eq3
∀[A,B:Type]. ∀[b:B]. ∀[a:A].  {b = a ∈ A supposing b = a ∈ B} supposing strong-subtype(A;B)

Lemma: strong-subtype-eq4
∀[A,B:Type]. ∀[b:B]. ∀[a:A].  {b = a ∈ B supposing b = a ∈ A} supposing strong-subtype(B;A)

Lemma: strong-subtype-member
∀[A,B:Type]. ∀[b:B]. ∀[a:A].  {b ∈ A supposing b = a ∈ B} supposing strong-subtype(A;B)

Lemma: singleton-subtype
∀[A,B:Type].  ∀[a:A]. ({z:B| z = a ∈ B}  ⊆r A) supposing strong-subtype(A;B)

Lemma: inject-subtype
∀[C,A:Type].  ∀[B:Type]. ∀[f:A ⟶ B].  Inj(C;B;f) supposing Inj(A;B;f) supposing strong-subtype(C;A)

Lemma: b-union-equality-disjoint
∀A,B:Type. ∀a:A. ∀b:B.  ((¬A ⋂ B) ⇒ (¬(a = b ∈ (A ⋃ B))))

Lemma: b-union-equality-disjoint2
∀A,B:Type. ∀a:A. ∀b:B.  ((a = b ∈ (A ⋃ B)) ⇒ (¬¬A ⋂ B))

Lemma: strong-subtype-b-union-better
∀[A,B:Type].  strong-subtype(A;A ⋃ B) supposing strong-subtype(A ⋂ B;B)

Lemma: strong-subtype-isect-base
∀[A:Type]. (strong-subtype(A ⋂ Base;Base) ∧ strong-subtype(Base ⋂ A;Base))

Lemma: strong-subtype-union-base
∀[A:Type]. (strong-subtype(A;A ⋃ Base) ∧ strong-subtype(A;Base ⋃ A))

Lemma: b-union-base-equality
∀A:Type. ∀a,b:Base.  ((a = b ∈ (Base ⋃ A)) ⇒ (b ∈ A) ⇒ (a = b ∈ A))

Lemma: strong-subtype-b-union
∀[A,B:Type].  strong-subtype(A;A ⋃ B) ∧ strong-subtype(B;A ⋃ B) supposing ¬A ⋂ B

Lemma: isect2-b-union-subtype
∀[A,B,C:Type].  A ⋂ B ⋃ C ⊆r (A ⋂ B ⋃ A ⋂ C) supposing ¬B ⋂ C

Lemma: strong-continuous-b-union
∀[F,G:Type ⟶ Type].
  (Continuous+(T.F[T] ⋃ G[T])) supposing ((∀T,S:Type.  (¬F[T] ⋂ G[S])) and Continuous+(T.G[T]) and Continuous+(T.F[T]))

Lemma: inject_functionality
∀[A,B,C:Type]. ∀[f:B ⟶ C].  (Inj(A;C;f)) supposing (Inj(B;C;f) and strong-subtype(A;B))

Lemma: sq_stable__strong-subtype
∀[A,B:Type].  SqStable(strong-subtype(A;B))

Lemma: id-fun-subtype
∀[A,B:Type].  id-fun(B) ⊆r id-fun(A) supposing strong-subtype(A;B)

Lemma: id-fun-set
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[f:id-fun(A)].  (f ∈ id-fun({a:A| P[a]} ))

Lemma: subtype_by_equality
∀[A,B:Type].  ((∀x,y:Base.  ((x = y ∈ A) ⇒ (x = y ∈ B))) ⇒ (A ⊆r B))

Definition: per-class
per-class(T;a) ==  {x:Base| x = a ∈ T} 

Lemma: per-class_wf
∀[T:Type]. ∀[a:Base ⋃ T].  (per-class(T;a) ∈ Type)

Lemma: trivial-per-class
∀[T:Type]. ∀[a:T ⋂ Base].  (a ∈ per-class(T;a))

Lemma: squash-per-class
∀[T:Type]. ∀[a:T].  (↓per-class(T;a))

Lemma: subtype_rel_per-class
∀[A,B:Type].  ∀[a:A]. (per-class(A;a) ⊆r per-class(B;a)) supposing A ⊆r B

Lemma: per-class-subtype-singleton
∀[T:Type]. ∀[a:T].  (per-class(T;a) ⊆r {x:T| x = a ∈ T} )

Lemma: per-class-base-singleton
∀[T:Type]. ∀[a:T].  per-class(T;a) ≡ Base ⋂ {x:T| x = a ∈ T} 

Lemma: per-class-base
∀[T:Type]. ∀[a:T]. ∀[b:per-class(T;a)].  (b ~ a) supposing T ⊆r Base

Definition: t-sqle
t-sqle(T;a;b) ==  ↓∃a':per-class(T;a). ∃b':per-class(T;b). (a' ≤ b')

Lemma: t-sqle_wf
∀[T:Type]. ∀[a,b:T].  (t-sqle(T;a;b) ∈ ℙ)

Lemma: sq_stable__t-sqle
∀[T:Type]. ∀[a,b:T].  SqStable(t-sqle(T;a;b))

Lemma: t-sqle_reflexive
∀[T:Type]. ∀a:T. t-sqle(T;a;a)

Lemma: t-sqle-subtype
∀[A,B:Type].  ∀[a,b:A].  (t-sqle(A;a;b) ⇒ t-sqle(B;a;b)) supposing A ⊆r B

Lemma: t-sqle-apply
∀[A,B:Type].  ∀a1,a2:A. ∀f1,f2:a:A ⟶ B.  (t-sqle(a:A ⟶ B;f1;f2) ⇒ t-sqle(A;a1;a2) ⇒ t-sqle(B;f1 a1;f2 a2))

Lemma: t-sqle-base
∀[T:Type]. ∀a,b:T.  (t-sqle(T;a;b) ⇒ (a ≤ b)) supposing T ⊆r Base

Definition: is-above
is-above(T;a;z) ==  ∃y:Base. ((y = a ∈ T) ∧ (y ≤ z))

Lemma: is-above_wf
∀[T:Type]. ∀[a:T]. ∀[z:Base].  (is-above(T;a;z) ∈ ℙ)

Lemma: is-above-subtype
∀[A,B:Type].  ∀[a:A]. ∀[z:Base].  (is-above(A;a;z) ⇒ is-above(B;a;z)) supposing A ⊆r B

Lemma: is-above-singleton-subtype
∀[A:Type]. ∀[a:A]. ∀[B:Type].  ∀[z:Base]. (is-above(A;a;z) ⇒ is-above(B;a;z)) supposing {x:A| x = a ∈ A}  ⊆r B

Lemma: is-above-int
∀[n:ℤ]. ∀[z:Base].  z = n ∈ ℤ supposing is-above(ℤ;n;z)

Lemma: is-above-axiom-general
∀[T:Type]. ∀[z:Base]. z ~ Ax supposing is-above(T;Ax;z) supposing T ⊆r Base

Lemma: is-above-axiom
∀[z:Base]. z ~ Ax supposing is-above(Unit;Ax;z)

Lemma: is-above-pair
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[a:A]. ∀[b:B[a]].
  ∀z:Base. (is-above(a:A × B[a];<a, b>;z) ⇒ (∃c,d:Base. ((z ~ <c, d>) ∧ is-above(A;a;c) ∧ is-above(B[a];b;d))))

Lemma: is-above-inl
∀[A,B:Type]. ∀[a:A].  ∀z:Base. (is-above(A + B;inl a;z) ⇒ (∃c:Base. ((z ~ inl c) ∧ is-above(A;a;c))))

Lemma: is-above-inr
∀[A,B:Type]. ∀[a:B].  ∀z:Base. (is-above(A + B;inr a ;z) ⇒ (∃c:Base. ((z ~ inr c ) ∧ is-above(B;a;c))))

Definition: mono
mono(T) ==  ∀a:T. ∀b:Base.  (is-above(T;a;b) ⇒ (a = b ∈ T))

Lemma: mono_wf
∀[T:Type]. (mono(T) ∈ ℙ)

Lemma: t-sqle-apply-dependent
∀[A:Type]
  ∀[B:A ⟶ Type]
    ∀a1,a2:A. ∀f1,f2:a:A ⟶ B[a].  (t-sqle(a:A ⟶ B[a];f1;f2) ⇒ t-sqle(A;a1;a2) ⇒ t-sqle(B[a1];f1 a1;f2 a2)) 
  supposing mono(A)

Lemma: int-mono
mono(ℤ)

Lemma: unit-mono
mono(Unit)

Lemma: void-mono
mono(Void)

Lemma: subtype-mono
∀[A,B:Type].  (mono(A)) supposing (mono(B) and strong-subtype(A;B))

Lemma: set-mono
∀A:Type. ∀P:A ⟶ ℙ.  (mono(A) ⇒ mono({a:A| P[a]} ))

Lemma: nat-mono
mono(ℕ)

Lemma: pair-mono
∀A:Type. ∀B:A ⟶ Type.  ((mono(A) ∧ (∀a:A. mono(B[a]))) ⇒ mono(a:A × B[a]))

Lemma: function-mono
∀A:Type. ∀B:A ⟶ Type.  (((A ⊆r Base) ∧ (∀a:A. mono(B[a])) ∧ (↓∃a:A. value-type(B[a]))) ⇒ mono(a:A ⟶ B[a]))

Lemma: isect-mono
∀A:Type. ∀B:A ⟶ Type.  ((∀a:A. mono(B[a])) ⇒ mono(⋂a:A. B[a]))

Lemma: union-mono
∀A,B:Type.  ((mono(A) ∧ mono(B)) ⇒ mono(A + B))

Lemma: bool-mono
mono(𝔹)

Lemma: sqle-mono-implies-equal
∀[T:Type]. ∀[x,y:Base].  (x = y ∈ T) supposing ((x ∈ T) and (x ≤ y)) supposing mono(T)

Lemma: squash-exists-is-union-squash
∀[T:Type]. ∀[P:T ⟶ ℙ].  ↓∃x:T. P[x] ≡ ⋃x:T.(↓P[x])

Lemma: squash-product
∀[A,B:Type].  uiff(↓A × B;↓A × (↓B))

Lemma: union-set-is-set-exists
∀[A,B:Type]. ∀[P:A ⟶ B ⟶ ℙ].  ⋃x:A.{y:B| P[x;y]}  ≡ {y:B| ∃x:A. P[x;y]} 

Lemma: prod-image-is-image
∀[A:Type]. ∀[f:Base]. ∀[B:Image(A,f) ⟶ Type]. ∀[g:Base].
  y:Image(A,f) × Image(B[y],g) ≡ Image((z:A × B[f z]),(λp.let a,b = p 
                                                          in <f a, g b>))

Lemma: squash-union-is-union-squash
∀[A:Type]. ∀[P:A ⟶ Type].  ↓⋃a:A.P[a] ≡ ⋃a:A.(↓P[a])

Lemma: subtype-iff-id-mem-fun
∀[A,B:Type].  uiff(A ⊆r B;λx.x ∈ A ⟶ B)

Lemma: type-monotone_fun_exp_top
∀[F:Type ⟶ Type]. ∀[n,m:ℕ].  (F^n Top) ⊆r (F^m Top) supposing m ≤ n supposing Monotone(T.F[T])

Lemma: type-monotone-fun_exp
∀[F:Type ⟶ Type]. ∀[n,m:ℕ].  (F^n Void) ⊆r (F^m Void) supposing n ≤ m supposing Monotone(T.F[T])

Definition: exception-name
exception-name(e;n) ==  isaxiom(e?n:x.Ax) ∧b isint(e?n:x.2)

Lemma: exception-name_wf
∀[n:Atom2]. ∀[t:Value() ⋃ Exception(n;Top)].  (exception-name(t;n) ∈ 𝔹)

Lemma: assert-exception-name
∀[n:Atom2]. ∀[t:Value() ⋃ Exception(n;Top)].
  (t ∈ Exception(n;Top) supposing ↑exception-name(t;n) ∧ t ∈ Value() supposing ¬↑exception-name(t;n))

Definition: set-axiom-of-choice
If we think of "sets" as types, then a family of non-empty sets is
given by an "index set" T and a function S ∈ T ⟶ Type such that
∀x:T. (S x).  The condition ∀x:T. (S x) says that each "set" S x is inhabited.

Now, the constructive interpretation of ∀x:T. (S x) is a function of type ⌜x:T ⟶ (S x)⌝
, so one version of the axiom of choice is necessarily true.

But, if we require a "function" from the family of sets S x to members of those
sets, then the function must be extensional. That would mean that
when two sets S x and S y are extensionally the same set then the function
must choose the same value for S y that it chooses for S x.

We define here the statement of an axiom of choice that says that such
an extensional choice function exists. Instead of extensional equality of sets
we use extensional equality of types.

Following Diaconescu (or Goodman-Myhill) we can prove that this
version of AC implies the law of excluded middle
 (set-axiom-of-choice-implies-xmiddle).
And therefore, it is proveably false in Nuprl
(Error :set-axiom-of-choice-is-false).⋅

Set-AC ==  ∀T:Type. ∀S:T ⟶ Type.  ((∀x:T. (S x)) ⇒ (∃f:x:T ⟶ (S x). ∀x,y:T.  (S x ≡ S y ⇒ ((f x) = (f y) ∈ (S x)))))

Lemma: set-axiom-of-choice_wf
Set-AC ∈ ℙ'

Lemma: set-axiom-of-choice-implies-xmiddle
Set-AC ⇒ (∀P:ℙ. ((↓P) ∨ (¬P)))

Lemma: subtype-TYPE
Type ⊆r TYPE



Home Index