Definition: uand
uand(A;B) == ⋂x:Base. ⋂p:(x)↓. if x = Ax then A otherwise B
Lemma: uand_wf
∀[A,B:Type]. (uand(A;B) ∈ Type)
Lemma: uand-subtype1
∀[A,B:Type]. ∀[z:uand(A;B)]. (z ∈ A)
Lemma: uand-subtype2
∀[A,B:Type]. (uand(A;B) ⊆r B)
Definition: per-int
per-int() == pertype(λa,b. uand(a ~ b;isint(a) ~ tt))
Lemma: per-int_wf
per-int() ∈ Type
Definition: per-void
per-void() == pertype(λa,b. (tt ≤ ff))
Lemma: per-void_wf
per-void() ∈ Type
Lemma: if-per-void
∀[t:Top]. (per-void() ⇒ t)
Definition: base-type-family
base-type-family{i:l}(A;a.B[a]) == ∀[a,a':Base]. B[a] = B[a'] ∈ Type supposing a = a' ∈ A
Lemma: base-type-family_wf
∀[A:Type]. ∀[B:Base]. (base-type-family{i:l}(A;a.B[a]) ∈ ℙ')
Lemma: base-type-family-implies
∀[A:Type]. ∀[B:Base]. ∀a:A. (B[a] ∈ Type) supposing base-type-family{i:l}(A;a.B[a])
Definition: function-eq
function-eq(A;a.B[a];f;g) == ∀[a,b:Base]. (f a) = (g b) ∈ B[a] supposing a = b ∈ A
Lemma: function-eq_wf
∀[A:Type]. ∀[B:Base]. ∀[f,g:Base]. (function-eq(A;a.B[a];f;g) ∈ Type) supposing base-type-family{i:l}(A;a.B[a])
Lemma: function-eq-symmetry
∀[A:Type]. ∀[B:Base].
∀[f,g:Base]. (function-eq(A;a.B[a];f;g) ⇒ function-eq(A;a.B[a];g;f)) supposing base-type-family{i:l}(A;a.B[a])
Lemma: function-eq-transitivity
∀[A:Type]. ∀[B:Base].
∀[f,g,h:Base]. (function-eq(A;a.B[a];f;g) ⇒ function-eq(A;a.B[a];g;h) ⇒ function-eq(A;a.B[a];f;h))
supposing base-type-family{i:l}(A;a.B[a])
Lemma: function-eq-implies
∀[A:Type]. ∀[B:Base].
∀[f,g:Base]. (function-eq(A;a.B[a];f;g) ⇒ {∀[a:A]. ((f a) = (g a) ∈ B[a])})
supposing base-type-family{i:l}(A;a.B[a])
Definition: per-function
per-function(A;a.B[a]) == pertype(λf,g. function-eq(A;a.B[a];f;g))
Lemma: per-function_wf_base_family
∀[A:Type]. ∀[B:Base]. per-function(A;a.B[a]) ∈ Type supposing base-type-family{i:l}(A;a.B[a])
Definition: type-function
type-function{i:l}(A) == per-function(A;a.Type)
Lemma: type-function_wf
∀[A:Type]. (type-function{i:l}(A) ∈ 𝕌')
Lemma: per-function_wf_type
∀[A:Type]. (per-function(A;a.Type) ∈ 𝕌')
Definition: per-type-family
per-type-family(B) == λx.B
Lemma: per-type-family_wf
∀[A:Type]. ∀[B:Type supposing A]. (per-type-family(B) ∈ per-function(A;a.Type))
Definition: per-or-family
per-or-family(A;B) == λx.if x = Ax then A otherwise B
Definition: tf-apply
tf-apply(f;x) == f x
Lemma: tf-apply_wf
∀[A:Type]. ∀[a:A]. ∀[B:type-function{i:l}(A)]. (tf-apply(B;a) ∈ Type)
Lemma: apply_wf_type-function
∀[A:Type]. ∀[a:A]. ∀[B:type-function{i:l}(A)]. (B a ∈ Type)
Lemma: type-function-eta
∀[A:Type]. ∀[B,C:type-function{i:l}(A)].
((B = C ∈ type-function{i:l}(A)) ⇒ ((λx.(B x)) = (λx.(C x)) ∈ type-function{i:l}(A)))
Lemma: per-function-type-apply
∀[A:Type]. ∀[B:type-function{i:l}(A)]. ∀[a:A]. (B[a] ∈ Type)
Lemma: function-eq_wf_type_function
∀A:Type. ∀B:type-function{i:l}(A). ∀f,g:Base. (function-eq(A;a.B[a];f;g) ∈ Type)
Lemma: function-eq-symmetry-type-function
∀A:Type. ∀B:type-function{i:l}(A). ∀f,g:Base. (function-eq(A;a.B[a];f;g) ⇒ function-eq(A;a.B[a];g;f))
Lemma: function-eq-transitivity-type-function
∀A:Type. ∀B:type-function{i:l}(A). ∀f,g,h:Base.
(function-eq(A;a.B[a];f;g) ⇒ function-eq(A;a.B[a];g;h) ⇒ function-eq(A;a.B[a];f;h))
Lemma: per-function_wf
∀[A:Type]. ∀[B:type-function{i:l}(A)]. (per-function(A;a.B[a]) ∈ Type)
Lemma: apply-wf-per
∀[A:Type]. ∀[B:type-function{i:l}(A)]. ∀[f:per-function(A;a.B[a])]. ∀[a:A]. (f[a] ∈ B[a])
Definition: per-apply
per-apply(f;x) == f x
Lemma: per-apply_wf
∀[A:Type]. ∀[B:type-function{i:l}(A)]. ∀[f:per-function(A;a.B[a])]. ∀[a:A]. (per-apply(f;a) ∈ tf-apply(B;a))
Lemma: base-member-per-function
∀[A:Type]. ∀[B:per-function(A;x.Type)]. ∀[f:Base].
f ∈ per-function(A;x.B[x]) supposing ∀[a,a':Base]. (f a) = (f a') ∈ B[a] supposing a = a' ∈ A
Lemma: per-function-ext
∀[A:Type]. ∀[B:per-function(A;x.Type)]. ∀[f,g:per-function(A;x.B[x])].
f = g ∈ per-function(A;x.B[x]) supposing ∀[a:A]. ((f a) = (g a) ∈ B[a])
Definition: per-all
per-all(A;a.B[a]) == per-function(A;a.B[a])
Lemma: per-all_wf
∀[A:Type]. ∀[B:type-function{i:l}(A)]. (per-all(A;a.B[a]) ∈ ℙ)
Definition: per-product
per-product(A;a.B[a]) ==
pertype(λa,b. uand(ispair(a) ~ tt;uand(ispair(b) ~ tt;uand((fst(a)) = (fst(b)) ∈ A;(snd(a)) = (snd(b)) ∈ B[fst(a)]
supposing (fst(a))
= (fst(b))
∈ A))))
Lemma: per-product_wf
∀[A:Type]. ∀[B:per-function(A;a.Type)]. (per-product(A;a.B[a]) ∈ Type)
Lemma: per-product-elim
∀[A:Type]. ∀[B:per-function(A;a.Type)]. ∀[p:per-product(A;a.B[a])].
uand(p ~ <fst(p), snd(p)>;uand(fst(p) ∈ A;snd(p) ∈ B[fst(p)]))
Lemma: member-per-product
∀[A:Type]. ∀[B:per-function(A;a.Type)]. ∀[a:A]. ∀[b:B[a]]. (<a, b> ∈ per-product(A;a.B[a]))
Definition: per-exists
per-exists(A;a.B[a]) == per-product(A;a.B[a])
Lemma: per-exists_wf
∀[A:Type]. ∀[B:type-function{i:l}(A)]. (per-exists(A;a.B[a]) ∈ Type)
Definition: per-and
per-and(A;B) == per-product(A;null_var.B)
Lemma: per-and_wf
∀[A:Type]. ∀[B:Type supposing A]. (per-and(A;B) ∈ Type)
Lemma: member-per-and
∀[A:Type]. ∀[B:Type supposing A]. ∀[a:A]. ∀[b:B]. (<a, b> ∈ per-and(A;B))
Definition: per-set
per-set(A;a.B[a]) == pertype(λa,b. ((a = b ∈ A) ∧ B[a]))
Lemma: per-set_wf
∀[A:Type]. ∀[B:A ⟶ Type]. (per-set(A;a.B[a]) ∈ Type)
Lemma: subtype_rel-per-set
∀[A:Type]. ∀[B:A ⟶ Type]. (per-set(A;a.B[a]) ⊆r A)
Lemma: per-set-equality
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[a1,a2:A]. (a1 = a2 ∈ per-set(A;a.B[a])) supposing ((a1 = a2 ∈ A) and B[a1])
Lemma: per-set-intro
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[a:A]. a ∈ per-set(A;a.B[a]) supposing B[a]
Definition: per-value
per-value() == per-set(Base;x.(x)↓)
Lemma: per-value_wf
per-value() ∈ Type
Lemma: per-value-property
∀[x:per-value()]. uand(x ∈ Base;(x)↓)
Lemma: per-value_subtype_base
per-value() ⊆r Base
Lemma: member-per-value
∀[x:Base]. x ∈ per-value() supposing (x)↓
Lemma: per-or-family_wf
∀[A,B:Type]. (per-or-family(A;B) ∈ per-function(per-value();a.Type))
Definition: per-or
per-or(A;B) == per-exists(per-value();x.if x = Ax then A otherwise B)
Lemma: per-or_wf
∀[A,B:Type]. (per-or(A;B) ∈ Type)
Lemma: per-or-equal
∀[A1,B1,A2,B2:Type]. (per-or(A1;B1) = per-or(A2;B2) ∈ Type) supposing (A1 ≡ A2 and B1 ≡ B2)
Lemma: member-per-or-left
∀[A,B:Type]. ∀[a:A]. (<Ax, a> ∈ per-or(A;B))
Lemma: member-per-or-right
∀[A,B:Type]. ∀[b:B]. (<0, b> ∈ per-or(A;B))
Definition: per-union
per-union(A;B) ==
pertype(λa,b. uand(uand((a)↓;(b)↓);if a is inl then if b is inl then outl(a) = outl(b) ∈ A
else per-void()
else if a is inr then if b is inr then outr(a) = outr(b) ∈ B
else per-void()
else per-void()
supposing uand((a)↓;(b)↓)))
Lemma: per-union_wf
∀[A,B:Type]. (per-union(A;B) ∈ Type)
Lemma: per-union-implies-wf1
∀[A,B:Type]. ∀[x:per-union(A;B)]. (x ~ inl outl(x) ∈ ℙ)
Lemma: per-union-implies-wf2
∀[A,B:Type]. ∀[x:per-union(A;B)]. (x ~ inr outr(x) ∈ ℙ)
Lemma: per-union-elim1
∀[A,B:Type]. ∀x:per-union(A;B). per-or(x ~ inl outl(x);x ~ inr outr(x) )
Lemma: per-union-elim
∀[A,B:Type].
∀x:per-union(A;B)
per-or(uand(x ~ inl outl(x);outl(x) ∈ A supposing x ~ inl outl(x));uand(x ~ inr outr(x) ;outr(x) ∈ B
supposing x
~ inr outr(x) ))
Lemma: member-per-union-left
∀[A,B:Type]. ∀[x:A]. (inl x ∈ per-union(A;B))
Lemma: member-per-union-right
∀[A,B:Type]. ∀[x:B]. (inr x ∈ per-union(A;B))
Home
Index