Comment: union_summary
Non canonical functions (isl, outl, outr) for union type. 

Definition: isl
isl(x) ==  case of inl(y) => tt inr(z) => ff

Lemma: isl_wf
[A,B:Type]. ∀[x:A B].  (isl(x) ∈ 𝔹)

Definition: isr
isr(x) ==  case of inl(y) => ff inr(z) => tt

Lemma: isr_wf
[A,B:Type]. ∀[x:A B].  (isr(x) ∈ 𝔹)

Lemma: inr-one-one
[A,B:Type]. ∀[x,y:B].  uiff((inr (inr ) ∈ (A B);x y ∈ B)

Lemma: inr-one-one'
[A,B:Type]. ∀[x,y:B].  y ∈ supposing (inr (inr ) ∈ (A B)

Lemma: inl-one-one
[A,B:Type]. ∀[x,y:A].  uiff((inl x) (inl y) ∈ (A B);x y ∈ A)

Lemma: inl-one-one'
[A,B:Type]. ∀[x,y:A].  y ∈ supposing (inl x) (inl y) ∈ (A B)

Lemma: inl-inr-disjoint
[A,B:Type]. ∀[x:A]. ∀[y:B].  uiff((inl x) (inr ) ∈ (A B);False)

Lemma: inr-inl-disjoint
[A,B:Type]. ∀[x:B]. ∀[y:A].  uiff((inr (inl y) ∈ (A B);False)

Definition: ifthenelse
if then else fi  ==  case of inl() => inr() => f

Lemma: ifthenelse_wf
[b:𝔹]. ∀[A:Type]. ∀[p,q:A].  (if then else fi  ∈ A)

Definition: ifunion
ifunion(b; t) ==  if then else fi 

Lemma: subtype_rel_ifthenelse
[b:𝔹]. ∀[A1,A2,B1,B2:Type].
  (if then A1 else B1 fi  ⊆if then A2 else B2 fi supposing ((A1 ⊆A2) and (B1 ⊆B2))

Definition: assert
==  if then True else False fi 

Lemma: assert_wf
[b:𝔹]. (↑b ∈ ℙ)

Lemma: istype-assert
[b:𝔹]. istype(↑b)

Definition: bnot
¬b==  if then ff else tt fi 

Lemma: bnot_wf
[b:𝔹]. bb ∈ 𝔹)

Definition: le_int
i ≤==  ¬bj <i

Lemma: le_int_wf
[i,j:ℤ].  (i ≤j ∈ 𝔹)

Definition: outl
outl(x) ==  case of inl(y) => inr(z) => ⊥

Lemma: outl_wf
[A,B:Type]. ∀[x:A B].  outl(x) ∈ supposing ↑isl(x)

Definition: outr
outr(x) ==  case of inl(y) => ⊥ inr(z) => z

Lemma: outr_wf
[A,B:Type]. ∀[x:A B].  outr(x) ∈ supposing ↑¬bisl(x)

Lemma: isr-not-isl
x:Top Top. ((↑isr(x))  (isl(x) ff))

Lemma: isl-not-isr
x:Top Top. ((↑isl(x))  (isr(x) ff))

Lemma: not-isr-isl
x:Top Top. ((¬↑isr(x))  (isl(x) tt))

Lemma: not-isr-assert-isl
x:Top Top. ((¬↑isr(x))  (↑isl(x)))

Lemma: not-isl-isr
x:Top Top. ((¬↑isl(x))  (isr(x) tt))

Lemma: not-isl-assert-isr
x:Top Top. ((¬↑isl(x))  (↑isr(x)))

Lemma: injection-eta
d:Top Top. if isl(d) then inl outl(d) else inr outr(d)  fi 

Lemma: inl-eta
[x:Top]. ∀d:Top Top. inl outl(d) supposing (inl x) ∈ (Top Top)

Lemma: inr-eta
[x:Top]. ∀d:Top Top. inr outr(d)  supposing (inr ) ∈ (Top Top)

Lemma: not-inl-sqeq-inr
[a,b:Base].  (inl inr ))

Lemma: istype-inl-sqeq-inr
[a,b:Top].  istype(inl inr )

Lemma: istype-inr-sqeq-inl
[a,b:Top].  istype(inr b  inl a)

Lemma: union-eta
d:Top Top. ((d inl outl(d)) ∨ (d inr outr(d) ))

Lemma: respects-equality-union
[T1,T2,S1,S2:Type].  (respects-equality(S1;T1)  respects-equality(S2;T2)  respects-equality(S1 S2;T1 T2))

Lemma: not-btrue-sqeq-bfalse
¬(ff tt)

Comment: assert_com

Lemma: assert_of_tt

Lemma: assert_of_ff

Lemma: assert_elim
[b:𝔹]. tt supposing ↑b

Lemma: not_assert_elim
[b:𝔹]. ff supposing ¬↑b

Lemma: sqeqtt_to_assert
[b:𝔹]. uiff(b tt;↑b)

Lemma: sqeqff_to_assert
[b:𝔹]. uiff(b ff;↑¬bb)

Lemma: eqtt_to_assert
[b:𝔹]. uiff(b tt;↑b)

Lemma: eqff_to_assert
[b:𝔹]. uiff(b ff;↑¬bb)

Lemma: decidable__assert

Lemma: assert_of_bnot
[p:𝔹]. uiff(↑¬bp;¬↑p)

Lemma: assert_of_eq_int
[x,y:ℤ].  uiff(↑(x =z y);x y ∈ ℤ)

Lemma: assert_of_lt_int
[x,y:ℤ].  uiff(↑x <y;x < y)

Definition: b-union
The union of two types is special case of the union of family of types,
where we use the booleans to index the family.⋅

A ⋃ ==  ⋃x:𝔹.if then else fi 

Lemma: b-union_wf
[A,B:Type].  (A ⋃ B ∈ Type)

Lemma: decide-spread-sq1
[x:Top × Top]. ∀[f,g,h:Top].  (case let a,b in inl f[a;b] of inl(z) => g[z] inr(z) => h[z] g[f[fst(x);snd(x)]])

Lemma: decide-spread-sq2
[x:Top × Top]. ∀[f,g,h:Top].
  (case let a,b in inr f[a;b]  of inl(z) => g[z] inr(z) => h[z] h[f[fst(x);snd(x)]])

Lemma: decide-decide
[x:Top Top]. ∀[f1,f2,g,h:Top].
  (case case of inl(z) => f1[z] inr(z) => f2[z] of inl(z) => g[z] inr(z) => h[z] case x
   of inl(z) =>
   case f1[z] of inl(z) => g[z] inr(z) => h[z]
   inr(z) =>
   case f2[z] of inl(z) => g[z] inr(z) => h[z])

Lemma: decide-decide2
[x:Top Top]. ∀[f1,f2,h:Top].
  (case of inl(z) => case of inl(z) => f1[z] inr(z) => f2[z] inr(z) => h[z] case x
   of inl(z) =>
   inr(z) =>

Lemma: decide-decide3
[x:Top Top]. ∀[f1,f2,h:Top].
  (case of inl(z) => h[z] inr(z) => case of inl(z) => f1[z] inr(z) => f2[z] case x
   of inl(z) =>
   inr(z) =>

Lemma: spread-spread
[t:Top × Top]. ∀[P,Q:Top].  (let x,y let a,b in P[a;b] in Q[x;y] let a,b in let x,y P[a;b] in Q[x;y])

Lemma: spread-ifthenelse
[b:𝔹]. ∀[f1,f2,x,y:Top].
  (let u,v 
   in if then f1[u;v] else f2[u;v] fi  if then let u,v in f1[u;v] else let u,v in f2[u;v] fi )

Lemma: trivial-ifthenelse
[b:𝔹]. ∀[f:Top].  (if then else fi  f)

Lemma: decidable__equal_union
[A,B:Type].  ((∀x,y:A.  Dec(x y ∈ A))  (∀u,v:B.  Dec(u v ∈ B))  (∀x,y:A B.  Dec(x y ∈ (A B))))

Home Index