Definition: lattice-structure
LatticeStructure ==
  "Point":Type
  "meet":self."Point" ⟶ self."Point" ⟶ self."Point"
  "join":self."Point" ⟶ self."Point" ⟶ self."Point"

Lemma: lattice-structure_wf
LatticeStructure ∈ 𝕌'

Definition: lattice-point
Point(l) ==  l."Point"

Lemma: lattice-point_wf
[l:LatticeStructure]. (Point(l) ∈ Type)

Definition: lattice-meet
a ∧ ==  l."meet" b

Lemma: lattice-meet_wf
[l:LatticeStructure]. ∀[a,b:Point(l)].  (a ∧ b ∈ Point(l))

Definition: lattice-join
a ∨ ==  l."join" b

Lemma: lattice-join_wf
[l:LatticeStructure]. ∀[a,b:Point(l)].  (a ∨ b ∈ Point(l))

Definition: lattice-axioms
lattice-axioms(l) ==
  (∀[a,b:Point(l)].  (a ∧ b ∧ a ∈ Point(l)))
  ∧ (∀[a,b:Point(l)].  (a ∨ b ∨ a ∈ Point(l)))
  ∧ (∀[a,b,c:Point(l)].  (a ∧ b ∧ a ∧ b ∧ c ∈ Point(l)))
  ∧ (∀[a,b,c:Point(l)].  (a ∨ b ∨ a ∨ b ∨ c ∈ Point(l)))
  ∧ (∀[a,b:Point(l)].  (a ∨ a ∧ a ∈ Point(l)))
  ∧ (∀[a,b:Point(l)].  (a ∧ a ∨ a ∈ Point(l)))

Lemma: lattice-axioms_wf
[l:LatticeStructure]. (lattice-axioms(l) ∈ ℙ)

Lemma: lattice-axioms-from-order
[l:LatticeStructure]
  lattice-axioms(l) 
  supposing ∃R:Point(l) ⟶ Point(l) ⟶ ℙ
             (((∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b))
             ∧ (∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)))
             ∧ Order(Point(l);x,y.R[x;y]))

Definition: lattice
Lattice ==  {l:LatticeStructure| lattice-axioms(l)} 

Lemma: lattice_wf
Lattice ∈ 𝕌'

Lemma: lattice_properties
[l:Lattice]
  ((∀[a,b:Point(l)].  (a ∧ b ∧ a ∈ Point(l)))
  ∧ (∀[a,b:Point(l)].  (a ∨ b ∨ a ∈ Point(l)))
  ∧ (∀[a,b,c:Point(l)].  (a ∧ b ∧ a ∧ b ∧ c ∈ Point(l)))
  ∧ (∀[a,b,c:Point(l)].  (a ∨ b ∨ a ∨ b ∨ c ∈ Point(l)))
  ∧ (∀[a,b:Point(l)].  (a ∨ a ∧ a ∈ Point(l)))
  ∧ (∀[a,b:Point(l)].  (a ∧ a ∨ a ∈ Point(l))))

Definition: lattice-le
a ≤ ==  a ∧ b ∈ Point(l)

Lemma: lattice-le_wf
[l:LatticeStructure]. ∀[a,b:Point(l)].  (a ≤ b ∈ Type)

Definition: lattice-hom
Hom(l1;l2) ==
  {f:Point(l1) ⟶ Point(l2)| 
   ∀[a,b:Point(l1)].  ((f a ∧ (f a ∧ b) ∈ Point(l2)) ∧ (f a ∨ (f a ∨ b) ∈ Point(l2)))} 

Lemma: lattice-hom_wf
[l1,l2:LatticeStructure].  (Hom(l1;l2) ∈ Type)

Lemma: id-is-lattice-hom
[l:LatticeStructure]. x.x ∈ Hom(l;l))

Lemma: compose-lattice-hom
[l1,l2,l3:Lattice]. ∀[f:Hom(l1;l2)]. ∀[g:Hom(l2;l3)].  (g f ∈ Hom(l1;l3))

Definition: mk-lattice
mk-lattice(T;m;j) ==  λx.x["Point" := T]["meet" := m]["join" := j]

Lemma: mk-lattice_wf
[T:Type]. ∀[m,j:T ⟶ T ⟶ T].
  mk-lattice(T;m;j) ∈ Lattice 
  supposing (∀[a,b:T].  (m[a;b] m[b;a] ∈ T))
  ∧ (∀[a,b:T].  (j[a;b] j[b;a] ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;m[b;c]] m[m[a;b];c] ∈ T))
  ∧ (∀[a,b,c:T].  (j[a;j[b;c]] j[j[a;b];c] ∈ T))
  ∧ (∀[a,b:T].  (j[a;m[a;b]] a ∈ T))
  ∧ (∀[a,b:T].  (m[a;j[a;b]] a ∈ T))

Definition: divisibility-lattice
divisibility-lattice() ==  mk-lattice(ℕa,b. gcd(a;b);λa,b. lcm(a;b))

Lemma: divisibility-lattice_wf
divisibility-lattice() ∈ Lattice

Definition: bounded-lattice-structure
BoundedLatticeStructure ==
  "Point":Type
  "meet":self."Point" ⟶ self."Point" ⟶ self."Point"
  "join":self."Point" ⟶ self."Point" ⟶ self."Point"
  "1":self."Point"
  "0":self."Point"

Lemma: bounded-lattice-structure_wf
BoundedLatticeStructure ∈ 𝕌'

Lemma: bounded-lattice-structure-subtype
BoundedLatticeStructure ⊆LatticeStructure

Definition: mk-bounded-lattice
mk-bounded-lattice(T;m;j;z;o) ==  λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o]

Definition: lattice-1
==  l."1"

Lemma: lattice-1_wf
[l:BoundedLatticeStructure]. (1 ∈ Point(l))

Definition: lattice-0
==  l."0"

Lemma: lattice-0_wf
[l:BoundedLatticeStructure]. (0 ∈ Point(l))

Definition: bounded-lattice-axioms
bounded-lattice-axioms(l) ==  (∀[a:Point(l)]. (a ∨ a ∈ Point(l))) ∧ (∀[a:Point(l)]. (a ∧ a ∈ Point(l)))

Lemma: bounded-lattice-axioms_wf
[l:BoundedLatticeStructure]. (bounded-lattice-axioms(l) ∈ ℙ)

Definition: bdd-lattice
BoundedLattice ==  {l:BoundedLatticeStructure| lattice-axioms(l) ∧ bounded-lattice-axioms(l)} 

Lemma: bdd-lattice_wf
BoundedLattice ∈ 𝕌'

Lemma: bdd-lattice-subtype-lattice
BoundedLattice ⊆Lattice

Lemma: mk-bounded-lattice_wf
[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T].
  mk-bounded-lattice(T;m;j;z;o) ∈ BoundedLattice 
  supposing (∀[a,b:T].  (m[a;b] m[b;a] ∈ T))
  ∧ (∀[a,b:T].  (j[a;b] j[b;a] ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;m[b;c]] m[m[a;b];c] ∈ T))
  ∧ (∀[a,b,c:T].  (j[a;j[b;c]] j[j[a;b];c] ∈ T))
  ∧ (∀[a,b:T].  (j[a;m[a;b]] a ∈ T))
  ∧ (∀[a,b:T].  (m[a;j[a;b]] a ∈ T))
  ∧ (∀[a:T]. (m[a;o] a ∈ T))
  ∧ (∀[a:T]. (j[a;z] a ∈ T))

Lemma: ext-eq-equiv
EquivRel(Type;A,B.A ≡ B)

Definition: e-type
EType ==  A,B:Type//A ≡ B

Lemma: e-type_wf
EType ∈ 𝕌'

Definition: p-type
PType ==  A,B:Type//(A ⇐⇒ B)

Lemma: p-type_wf
PType ∈ 𝕌'

Definition: e-isect
e-isect(A;B) ==  A ⋂ B

Lemma: e-isect_wf
[A,B:EType].  (e-isect(A;B) ∈ EType)

Definition: p-and
p-and(A;B) ==  A ∧ B

Lemma: p-and_wf
[A,B:PType].  (p-and(A;B) ∈ PType)

Definition: e-union
e-union(A;B) ==  A ⋃ B

Lemma: e-union_wf
[A,B:EType].  (e-union(A;B) ∈ EType)

Definition: p-or
p-or(A;B) ==  A ∨ B

Lemma: p-or_wf
[A,B:PType].  (p-or(A;B) ∈ PType)

Definition: type-lattice
type-lattice{i:l}() ==  mk-bounded-lattice(EType;λ2B.e-isect(A;B);λ2B.e-union(A;B);Void;Top)

Lemma: type-lattice_wf
type-lattice{i:l}() ∈ bdd-lattice{i':l}

Definition: iff-type-lattice
iff-type-lattice{i:l}() ==  mk-bounded-lattice(PType;λ2B.p-and(A;B);λ2B.p-or(A;B);False;True)

Definition: bounded-lattice-hom
Hom(l1;l2) ==  {f:Hom(l1;l2)| ((f 0) 0 ∈ Point(l2)) ∧ ((f 1) 1 ∈ Point(l2))} 

Lemma: bounded-lattice-hom_wf
[l1,l2:BoundedLatticeStructure].  (Hom(l1;l2) ∈ Type)

Lemma: bounded-lattice-hom-equal
[l1,l2:BoundedLatticeStructure]. ∀[f,g:Hom(l1;l2)].
  g ∈ Hom(l1;l2) supposing ∀x:Point(l1). ((f x) (g x) ∈ Point(l2))

Lemma: compose-bounded-lattice-hom
[l1,l2,l3:BoundedLattice]. ∀[f:Hom(l1;l2)]. ∀[g:Hom(l2;l3)].  (g f ∈ Hom(l1;l3))

Lemma: id-is-bounded-lattice-hom
[l:BoundedLattice]. x.x ∈ Hom(l;l))

Definition: distributive-lattice
DistributiveLattice ==
  {l:LatticeStructure| lattice-axioms(l) ∧ (∀[a,b,c:Point(l)].  (a ∧ b ∨ a ∧ b ∨ a ∧ c ∈ Point(l)))} 

Lemma: distributive-lattice_wf
DistributiveLattice ∈ 𝕌'

Definition: mk-distributive-lattice
mk-distributive-lattice(T; m; j) ==  mk-lattice(T;m;j)

Lemma: mk-distributive-lattice_wf
[T:Type]. ∀[m,j:T ⟶ T ⟶ T].
  mk-distributive-lattice(T; m; j) ∈ DistributiveLattice 
  supposing (∀[a,b:T].  (m[a;b] m[b;a] ∈ T))
  ∧ (∀[a,b:T].  (j[a;b] j[b;a] ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;m[b;c]] m[m[a;b];c] ∈ T))
  ∧ (∀[a,b,c:T].  (j[a;j[b;c]] j[j[a;b];c] ∈ T))
  ∧ (∀[a,b:T].  (j[a;m[a;b]] a ∈ T))
  ∧ (∀[a,b:T].  (m[a;j[a;b]] a ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;j[b;c]] j[m[a;b];m[a;c]] ∈ T))

Definition: bdd-distributive-lattice
BoundedDistributiveLattice ==
  {l:BoundedLatticeStructure| 
   (lattice-axioms(l) ∧ bounded-lattice-axioms(l)) ∧ (∀[a,b,c:Point(l)].  (a ∧ b ∨ a ∧ b ∨ a ∧ c ∈ Point(l)))} 

Lemma: bdd-distributive-lattice_wf
BoundedDistributiveLattice ∈ 𝕌'

Lemma: bdd-distributive-lattice-subtype-lattice
BoundedDistributiveLattice ⊆Lattice

Lemma: bdd-distributive-lattice-subtype-bdd-lattice
BoundedDistributiveLattice ⊆BoundedLattice

Lemma: bdd-distributive-lattice-subtype-distributive-lattice
BoundedDistributiveLattice ⊆DistributiveLattice

Definition: mk-bounded-distributive-lattice
{points=T;meet=m;join=j;0=z;1=o} ==  mk-bounded-lattice(T;m;j;z;o)

Lemma: mk-bounded-distributive-lattice_wf
[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T].
  {points=T;
   meet=m;
   join=j;
   0=z;
   1=o} ∈ BoundedDistributiveLattice 
  supposing (∀[a,b:T].  (m[a;b] m[b;a] ∈ T))
  ∧ (∀[a,b:T].  (j[a;b] j[b;a] ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;m[b;c]] m[m[a;b];c] ∈ T))
  ∧ (∀[a,b,c:T].  (j[a;j[b;c]] j[j[a;b];c] ∈ T))
  ∧ (∀[a,b:T].  (j[a;m[a;b]] a ∈ T))
  ∧ (∀[a,b:T].  (m[a;j[a;b]] a ∈ T))
  ∧ (∀[a:T]. (m[a;o] a ∈ T))
  ∧ (∀[a:T]. (j[a;z] a ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;j[b;c]] j[m[a;b];m[a;c]] ∈ T))

Lemma: mk-bounded-distributive-lattice-from-order
[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T]. ∀[R:T ⟶ T ⟶ ℙ].
  {points=T;
   meet=m;
   join=j;
   0=z;
   1=o} ∈ BoundedDistributiveLattice 
  supposing Order(T;x,y.R[x;y])
  ∧ (∀[a,b:T].  least-upper-bound(T;x,y.R[x;y];a;b;j[a;b]))
  ∧ (∀[a,b:T].  greatest-lower-bound(T;x,y.R[x;y];a;b;m[a;b]))
  ∧ (∀[a:T]. R[a;o])
  ∧ (∀[a:T]. R[z;a])
  ∧ (∀[a,b,c:T].  (m[a;j[b;c]] j[m[a;b];m[a;c]] ∈ T))

Lemma: lattice-join-idempotent
[l:Lattice]. ∀[u:Point(l)].  (u ∨ u ∈ Point(l))

Lemma: lattice-meet-idempotent
[l:Lattice]. ∀[u:Point(l)].  (u ∧ u ∈ Point(l))

Lemma: lattice-le_weakening
[l:Lattice]. ∀[a,b:Point(l)].  a ≤ supposing b ∈ Point(l)

Lemma: lattice-le_transitivity
[l:Lattice]. ∀[a,b,c:Point(l)].  (a ≤ c) supposing (a ≤ and b ≤ c)

Lemma: lattice-le-order
l:Lattice. Order(Point(l);x,y.x ≤ y)

Lemma: lattice-le-iff
[l:Lattice]. ∀[a,b:Point(l)].  uiff(a ≤ b;b a ∨ b ∈ Point(l))

Lemma: lattice-join-is-lub
l:Lattice. ∀a,b:Point(l).  least-upper-bound(Point(l);x,y.x ≤ y;a;b;a ∨ b)

Lemma: lattice-meet-is-glb
l:Lattice. ∀a,b:Point(l).  greatest-lower-bound(Point(l);x,y.x ≤ y;a;b;a ∧ b)

Lemma: lattice-le-meet
l:Lattice. ∀a,b,c:Point(l).  (c ≤ a ∧ ⇐⇒ c ≤ a ∧ c ≤ b)

Lemma: lattice-meet-le
l:Lattice. ∀a,b:Point(l).  (a ∧ b ≤ a ∧ a ∧ b ≤ b)

Lemma: lattice-join-le
l:Lattice. ∀a,b,c:Point(l).  (a ∨ b ≤ ⇐⇒ a ≤ c ∧ b ≤ c)

Lemma: lattice-axioms-iff-order
l:LatticeStructure
  (∃R:Point(l) ⟶ Point(l) ⟶ ℙ
    (((∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b))
    ∧ (∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)))
    ∧ Order(Point(l);x,y.R[x;y]))
  ⇐⇒ lattice-axioms(l))

Lemma: distributive-lattice-dual-distrib
[L:DistributiveLattice]. ∀[a,b,c:Point(L)].  (a ∨ b ∧ a ∨ b ∧ a ∨ c ∈ Point(L))

Lemma: distributive-lattice-distrib
[L:DistributiveLattice]. ∀[a,b,c:Point(L)].
  ((a ∧ b ∨ a ∧ b ∨ a ∧ c ∈ Point(L)) ∧ (b ∨ c ∧ b ∧ a ∨ c ∧ a ∈ Point(L)))

Lemma: distributive-lattice-dual-distrib2
[L:DistributiveLattice]. ∀[a,b,c:Point(L)].  (b ∧ c ∨ b ∨ a ∧ c ∨ a ∈ Point(L))

Lemma: lattice-0-le
[l:BoundedLattice]. ∀[x:Point(l)].  0 ≤ x

Lemma: lattice-meet-0
[l:BoundedLattice]. ∀[x:Point(l)].  (0 ∧ 0 ∈ Point(l))

Lemma: lattice-0-meet
[l:BoundedLattice]. ∀[x:Point(l)].  (x ∧ 0 ∈ Point(l))

Lemma: lattice-join-0
[l:BoundedLattice]. ∀[x:Point(l)].  ((0 ∨ x ∈ Point(l)) ∧ (x ∨ x ∈ Point(l)))

Lemma: lattice-meet-1
[l:BoundedLattice]. ∀[x:Point(l)].  (x ∧ x ∈ Point(l))

Lemma: lattice-1-meet
[l:BoundedLattice]. ∀[x:Point(l)].  (1 ∧ x ∈ Point(l))

Lemma: le-lattice-1
[l:BoundedLattice]. ∀[x:Point(l)].  x ≤ 1

Lemma: lattice-join-1
[l:BoundedLattice]. ∀[x:Point(l)].  (1 ∨ 1 ∈ Point(l))

Lemma: lattice-1-join
[l:BoundedLattice]. ∀[x:Point(l)].  (x ∨ 1 ∈ Point(l))

Lemma: lattice-meet-eq-1
[l:BoundedLattice]. ∀[x,y:Point(l)].  uiff(x ∧ 1 ∈ Point(l);(x 1 ∈ Point(l)) ∧ (y 1 ∈ Point(l)))

Lemma: lattice-1-le-iff
[l:BoundedLattice]. ∀[b:Point(l)].  uiff(1 ≤ b;b 1 ∈ Point(l))

Lemma: lattice-0-equal-lattice-1-implies
L:BoundedLattice. ((1 0 ∈ Point(L))  (∀x:Point(L). (0 x ∈ Point(L))))

Lemma: order-preserving-map-lattice-lemma
[l1,l2:Lattice]. ∀[f:Point(l1) ⟶ Point(l2)].
  (∀a,b:Point(l1).  a ∧ b ≤ a ∧ b) ∧ (∀a,b:Point(l1).  a ∨ b ≤ a ∨ b) 
  supposing ∀x,y:Point(l1).  (x ≤  x ≤ y)

Lemma: order-preserving-map-is-lattice-hom
[l1,l2:Lattice]. ∀[f:Point(l1) ⟶ Point(l2)].
  f ∈ Hom(l1;l2) 
  supposing (∀x,y:Point(l1).  (x ≤  x ≤ y))
  ∧ (∀a,b:Point(l1).  a ∧ b ≤ a ∧ b)
  ∧ (∀a,b:Point(l1).  a ∨ b ≤ a ∨ b)

Lemma: order-preserving-map-is-bounded-lattice-hom
[l1,l2:BoundedLattice]. ∀[f:Point(l1) ⟶ Point(l2)].
  f ∈ Hom(l1;l2) 
  supposing ((∀x,y:Point(l1).  (x ≤  x ≤ y))
            ∧ (∀a,b:Point(l1).  a ∧ b ≤ a ∧ b)
            ∧ (∀a,b:Point(l1).  a ∨ b ≤ a ∨ b))
  ∧ ((f 0) 0 ∈ Point(l2))
  ∧ ((f 1) 1 ∈ Point(l2))

Comment: free distributive lattices using quotient doc
In order to construct free distributive lattice on any type of generators
(without assuming decidable equality or finiteness) we can use a
quotient type.⋅

Definition: dlattice-order
as  bs ==  (∀b∈bs.(∃a∈as. a ⊆ b))

Lemma: dlattice-order_wf
[X:Type]. ∀[as,bs:X List List].  (as  bs ∈ ℙ)

Lemma: dlattice-order-iff
[X:Type]. ∀as,bs:X List List.  (as  bs ⇐⇒ ∀x:X List. ((x ∈ bs)  (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))

Lemma: dlattice-order_transitivity
[X:Type]. ∀as,bs,cs:X List List.  (as  bs  bs  cs  as  cs)

Lemma: dlattice-order_weakening
[X:Type]. ∀as,bs:X List List.  ((as bs ∈ (X List List))  as  bs)

Lemma: dlattice-order-append
X:Type. ∀a1,b1,a2,b2:X List List.  (a1  b1  a2  b2  a1 a2  b1 b2)

Definition: dlattice-eq
dlattice-eq(X;as;bs) ==  as  bs ∧ bs  as

Lemma: dlattice-eq_wf
[X:Type]. ∀[as,bs:X List List].  (dlattice-eq(X;as;bs) ∈ ℙ)

Lemma: dlattice-eq-equiv
[X:Type]. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))

Definition: free-dl-type
free-dl-type(X) ==  as,bs:X List List//dlattice-eq(X;as;bs)

Lemma: free-dl-type_wf
[X:Type]. (free-dl-type(X) ∈ Type)

Definition: free-dl-join
free-dl-join(as;bs) ==  as bs

Lemma: free-dl-join_wf
[X:Type]. ∀[as,bs:free-dl-type(X)].  (free-dl-join(as;bs) ∈ free-dl-type(X))

Definition: free-dl-meet
free-dl-meet(as;bs) ==
  accumulate (with value cs and list item a):
   cs map(λb.(a b);bs)
  over list:
    as
  with starting value:
   [])

Lemma: free-dl-meet_wf_list
[X:Type]. ∀[as,bs:X List List].  (free-dl-meet(as;bs) ∈ List List)

Lemma: member-free-dl-meet
[X:Type]
  ∀as,bs:X List List. ∀x:X List.
    ((x ∈ free-dl-meet(as;bs)) ⇐⇒ ∃u,v:X List. ((u ∈ as) ∧ (v ∈ bs) ∧ (x (u v) ∈ (X List))))

Lemma: dlattice-order-free-dl-meet
X:Type. ∀a1,b1,as,b2:X List List.  (a1  b1  as  b2  free-dl-meet(a1;as)  free-dl-meet(b1;b2))

Lemma: free-dl-meet_wf
[X:Type]. ∀[as,bs:free-dl-type(X)].  (free-dl-meet(as;bs) ∈ free-dl-type(X))

Definition: free-dl
free-dl(X) ==  {points=free-dl-type(X);meet=λ2y.free-dl-meet(x;y);join=λ2y.free-dl-join(x;y);0=[];1=[[]]}

Lemma: free-dl_wf
[X:Type]. (free-dl(X) ∈ BoundedDistributiveLattice)

Definition: free-dl-generator
free-dl-generator(x) ==  [[x]]

Lemma: free-dl-generator_wf
[X:Type]. ∀[x:X].  (free-dl-generator(x) ∈ free-dl-type(X))

Lemma: free-dl-generators
[X:Type]
  ∀L:BoundedDistributiveLattice
    ∀[f,g:Hom(free-dl(X);L)].
      g ∈ Hom(free-dl(X);L) supposing ∀x:X. ((f free-dl-generator(x)) (g free-dl-generator(x)) ∈ Point(L))

Definition: fdl-hom
fdl-hom(L;f) ==
  λz.accumulate (with value and list item xs):
      a ∨ accumulate (with value and list item x):
           b ∧ x
          over list:
            xs
          with starting value:
           1)
     over list:
       z
     with starting value:
      0)

Lemma: fdl-hom_wf1
[X:Type]. ∀[L:BoundedDistributiveLattice]. ∀[f:X ⟶ Point(L)].  (fdl-hom(L;f) ∈ (X List List) ⟶ Point(L))

Lemma: fdl-hom_wf
[X:Type]. ∀[L:BoundedDistributiveLattice]. ∀[f:X ⟶ Point(L)].  (fdl-hom(L;f) ∈ Hom(free-dl(X);L))

Lemma: fdl-hom-agrees
[X:Type]. ∀[L:BoundedDistributiveLattice]. ∀[f:X ⟶ Point(L)].
  ∀x:X. ((fdl-hom(L;f) free-dl-generator(x)) (f x) ∈ Point(L))

Definition: fdl-is-1
fdl-is-1(x) ==  (∃a∈x.isaxiom(a))_b

Lemma: fdl-is-1_wf
[X:Type]. ∀[x:Point(free-dl(X))].  (fdl-is-1(x) ∈ 𝔹)

Lemma: fdl-eq-1
[X:Type]. ∀x:Point(free-dl(X)). (x 1 ∈ Point(free-dl(X)) ⇐⇒ ↑fdl-is-1(x))

Lemma: fdl-0-not-1
[X:Type]. (0 1 ∈ Point(free-dl(X))))

Lemma: fdl-1-join-irreducible
[X:Type]
  ∀x,y:Point(free-dl(X)).  (x ∨ 1 ∈ Point(free-dl(X)) ⇐⇒ (x 1 ∈ Point(free-dl(X))) ∨ (y 1 ∈ Point(free-dl(X))))

Definition: lattice-less
a < ==  a ≤ b ∧ (a b ∈ Point(l)))

Lemma: lattice-less_wf
[l:LatticeStructure]. ∀[a,b:Point(l)].  (a < b ∈ ℙ)

Comment: distributive lattice with decidable equality doc
If the "points" of the lattice have decidable equality, then
we can implement some additional operations.
We use these for one construction of free distributive lattices.⋅

Definition: lattice-ble
lattice-ble(l;eq;a;b) ==  eq a ∧ b

Lemma: lattice-ble_wf
[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)].  (lattice-ble(l;eq;a;b) ∈ 𝔹)

Lemma: assert-lattice-ble
[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)].  uiff(↑lattice-ble(l;eq;a;b);a ≤ b)

Definition: lattice-bless
lattice-bless(l;eq;a;b) ==  lattice-ble(l;eq;a;b) ∧b b(eq b))

Lemma: lattice-bless_wf
[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)].  (lattice-bless(l;eq;a;b) ∈ 𝔹)

Lemma: assert-lattice-bless
[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)].  uiff(↑lattice-bless(l;eq;a;b);a < b)

Definition: lattice-fset-meet
/\(s) ==  reduce(λx,y. x ∧ y;1;s)

Lemma: lattice-fset-meet_wf
[l:BoundedLattice]. ((∀x,y:Point(l).  Dec(x y ∈ Point(l)))  (∀[s:fset(Point(l))]. (/\(s) ∈ Point(l))))

Definition: lattice-fset-join
\/(s) ==  reduce(λx,y. x ∨ y;0;s)

Lemma: lattice-fset-join_wf
[l:BoundedLattice]. ((∀x,y:Point(l).  Dec(x y ∈ Point(l)))  (∀[s:fset(Point(l))]. (\/(s) ∈ Point(l))))

Lemma: lattice-fset-join-union
[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  (\/(s1 ⋃ s2) \/(s1) ∨ \/(s2) ∈ Point(l))

Lemma: lattice-fset-join-singleton
[l:BoundedLattice]. ∀[x:Point(l)].  (\/({x}) x ∈ Point(l))

Lemma: lattice-fset-join-is-lub
[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))].
  ((∀[s:fset(Point(l))]. ∀[x:Point(l)].  x ≤ \/(s) supposing x ∈ s)
  ∧ (∀[s:fset(Point(l))]. ∀[u:Point(l)].  ((∀x:Point(l). (x ∈  x ≤ u))  \/(s) ≤ u)))

Lemma: lattice-fset-join-le
[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s:fset(Point(l))]. ∀[x:Point(l)].
  (\/(s) ≤ ⇐⇒ ∀p:Point(l). (p ∈  p ≤ x))

Lemma: lattice-fset-join_functionality_wrt_subset
[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  \/(s1) ≤ \/(s2) supposing s1 ⊆ s2

Lemma: lattice-fset-join_functionality_wrt_subset2
[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  \/(s1) ≤ \/(s2) supposing s1 ⊆ {0} ⋃ s2

Lemma: lattice-fset-meet-union
[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  (/\(s1 ⋃ s2) /\(s1) ∧ /\(s2) ∈ Point(l))

Lemma: lattice-fset-meet-singleton
[l:BoundedLattice]. ∀[x:Point(l)].  (/\({x}) x ∈ Point(l))

Lemma: lattice-fset-meet-is-glb
[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))].
  ((∀[s:fset(Point(l))]. ∀[x:Point(l)].  /\(s) ≤ supposing x ∈ s)
  ∧ (∀[s:fset(Point(l))]. ∀[v:Point(l)].  ((∀x:Point(l). (x ∈  v ≤ x))  v ≤ /\(s))))

Lemma: lattice-fset-meet-is-1
[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s:fset(Point(l))].
  uiff(/\(s) 1 ∈ Point(l);∀x:Point(l). (x ∈  (x 1 ∈ Point(l))))

Lemma: lattice-fset-meet_functionality_wrt_subset
[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  /\(s1) ≤ /\(s2) supposing s2 ⊆ s1

Lemma: lattice-meet-fset-join-distrib
[l:BoundedDistributiveLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].
  (\/(s1) ∧ \/(s2) \/(f-union(eq;eq;s1;a.λb.a ∧ b"(s2))) ∈ Point(l))

Lemma: lattice-hom-join
[l1,l2:BoundedLattice]. ∀[f:Hom(l1;l2)]. ∀[a,b:Point(l1)].  ((f a ∨ b) a ∨ b ∈ Point(l2))

Lemma: lattice-hom-meet
[l1,l2:BoundedLattice]. ∀[f:Hom(l1;l2)]. ∀[a,b:Point(l1)].  ((f a ∧ b) a ∧ b ∈ Point(l2))

Lemma: lattice-hom-fset-join
[l1,l2:BoundedLattice]. ∀[eq1:EqDecider(Point(l1))]. ∀[eq2:EqDecider(Point(l2))]. ∀[f:Hom(l1;l2)].
[s:fset(Point(l1))].
  ((f \/(s)) \/(f"(s)) ∈ Point(l2))

Lemma: lattice-hom-fset-meet
[l1,l2:BoundedLattice]. ∀[eq1:EqDecider(Point(l1))]. ∀[eq2:EqDecider(Point(l2))]. ∀[f:Hom(l1;l2)].
[s:fset(Point(l1))].
  ((f /\(s)) /\(f"(s)) ∈ Point(l2))

Lemma: lattice-hom-le
[l1,l2:BoundedLattice]. ∀[f:Hom(l1;l2)]. ∀[x,y:Point(l1)].  x ≤ supposing x ≤ y

Comment: free distrib lattices using decidable equality doc
The following construction of free distributive lattices depends
on having decidable equality for the generators.


Definition: free-dist-lattice
free-dist-lattice(T; eq) ==
  {points={ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;
   meet=λac1,ac2. fset-ac-glb(eq;ac1;ac2);
   join=λac1,ac2. fset-ac-lub(eq;ac1;ac2);
   0={};
   1={{}}}

Lemma: free-dist-lattice_wf
[T:Type]. ∀[eq:EqDecider(T)].  (free-dist-lattice(T; eq) ∈ BoundedDistributiveLattice)

Lemma: free-dl-point
[T,eq:Top].  (Point(free-dist-lattice(T; eq)) {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )

Lemma: free-dl-1
T:Type. ∀eq:EqDecider(T). ∀x:Point(free-dist-lattice(T; eq)).  (x 1 ∈ Point(free-dist-lattice(T; eq)) ⇐⇒ {} ∈ x)

Lemma: free-dl-0-not-1
T:Type. ∀eq:EqDecider(T).  (0 1 ∈ Point(free-dist-lattice(T; eq))))

Lemma: decidable__equal_free-dl
[T:Type]. ∀eq:EqDecider(T). ∀x,y:Point(free-dist-lattice(T; eq)).  Dec(x y ∈ Point(free-dist-lattice(T; eq)))

Lemma: free-dl-meet
[T,eq,a,b:Top].  (a ∧ fset-ac-glb(eq;a;b))

Lemma: free-dl-join
[T,eq,a,b:Top].  (a ∨ fset-ac-lub(eq;a;b))

Lemma: free-dl-le
[T:Type]. ∀eq:EqDecider(T). ∀x,y:Point(free-dist-lattice(T; eq)).  (x ≤ ⇐⇒ fset-ac-le(eq;x;y))

Definition: free-dl-inc
free-dl-inc(x) ==  {{x}}

Lemma: free-dl-inc_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T].  (free-dl-inc(x) ∈ Point(free-dist-lattice(T; eq)))

Lemma: free-dl-1-join-irreducible
T:Type. ∀eq:EqDecider(T). ∀x,y:Point(free-dist-lattice(T; eq)).
  (x ∨ 1 ∈ Point(free-dist-lattice(T; eq))
  ⇐⇒ (x 1 ∈ Point(free-dist-lattice(T; eq))) ∨ (y 1 ∈ Point(free-dist-lattice(T; eq))))

Definition: lattice-extend
lattice-extend(L;eq;eqL;f;ac) ==  \/(λxs./\(f"(xs))"(ac))

Lemma: lattice-extend_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
[ac:Point(free-dist-lattice(T; eq))].
  (lattice-extend(L;eq;eqL;f;ac) ∈ Point(L))

Lemma: lattice-extend-1
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
  (lattice-extend(L;eq;eqL;f;1) 1 ∈ Point(L))

Lemma: lattice-extend-dl-inc
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)]. ∀[x:T].
  (lattice-extend(L;eq;eqL;f;free-dl-inc(x)) (f x) ∈ Point(L))

Lemma: lattice-extend-order-preserving
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
[x,y:Point(free-dist-lattice(T; eq))].
  lattice-extend(L;eq;eqL;f;x) ≤ lattice-extend(L;eq;eqL;f;y) supposing x ≤ y

Definition: lattice-extend'
lattice-extend'(L;eq;eqL;f;ac) ==  \/(λxs./\(f"(xs))"(ac))

Lemma: lattice-extend'_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
[ac:fset(fset(T))].
  (lattice-extend'(L;eq;eqL;f;ac) ∈ Point(L))

Lemma: lattice-extend-join
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
[a,b:Point(free-dist-lattice(T; eq))].
  lattice-extend(L;eq;eqL;f;a ∨ b) ≤ lattice-extend(L;eq;eqL;f;a) ∨ lattice-extend(L;eq;eqL;f;b)

Lemma: lattice-meet-join-images-distrib
L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀as,bs:fset(fset(Point(L))).
  (\/(λls./\(ls)"(as)) ∧ \/(λls./\(ls)"(bs))
  \/(λls./\(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);as;as.λbs.as ⋃ bs"(bs))))
  ∈ Point(L))

Lemma: lattice-extend-meet
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
[a,b:Point(free-dist-lattice(T; eq))].
  lattice-extend(L;eq;eqL;f;a) ∧ lattice-extend(L;eq;eqL;f;b) ≤ lattice-extend(L;eq;eqL;f;a ∧ b)

Lemma: lattice-extend-is-hom
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
  ac.lattice-extend(L;eq;eqL;f;ac) ∈ Hom(free-dist-lattice(T; eq);L))

Lemma: free-dist-lattice-property
T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f:T ⟶ Point(L).
  ∃g:Hom(free-dist-lattice(T; eq);L). (f (g x.free-dl-inc(x))) ∈ (T ⟶ Point(L)))

Lemma: lattice-fset-meet-free-dl-inc
[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)].  (/\(λx.free-dl-inc(x)"(s)) {s} ∈ Point(free-dist-lattice(T; eq)))

Lemma: free-dl-basis
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-dist-lattice(T; eq))].
  (x \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(free-dist-lattice(T; eq)))

Lemma: free-dist-lattice-hom-unique2
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
[g,h:Hom(free-dist-lattice(T; eq);L)].
  h ∈ Hom(free-dist-lattice(T; eq);L) supposing ∀x:T. ((g free-dl-inc(x)) (h free-dl-inc(x)) ∈ Point(L))

Lemma: free-dist-lattice-hom-unique
T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f:T ⟶ Point(L).
g,h:Hom(free-dist-lattice(T; eq);L).
  ((f (g x.free-dl-inc(x))) ∈ (T ⟶ Point(L)))
   (f (h x.free-dl-inc(x))) ∈ (T ⟶ Point(L)))
   (g h ∈ Hom(free-dist-lattice(T; eq);L)))

Lemma: decidable__equal-free-dist-lattice-point
[T:Type]. ∀eq:EqDecider(T). ∀a,b:Point(free-dist-lattice(T; eq)).  Dec(a b ∈ Point(free-dist-lattice(T; eq)))

Definition: opposite-lattice
opposite-lattice(L) ==  {points=Point(L);meet=λ2b.a ∨ b;join=λ2b.a ∧ b;0=1;1=0}

Lemma: opposite-lattice_wf
[L:BoundedDistributiveLattice]. (opposite-lattice(L) ∈ BoundedDistributiveLattice)

Lemma: opposite-lattice-point
[L:Top]. (Point(opposite-lattice(L)) Point(L))

Lemma: opposite-lattice-0
[L:Top]. (0 1)

Lemma: opposite-lattice-1
[L:Top]. (1 0)

Lemma: opposite-lattice-meet
[L,a,b:Top].  (a ∧ a ∨ b)

Lemma: opposite-lattice-join
[L,a,b:Top].  (a ∨ a ∧ b)

Definition: fin-powerset-lattice
fin-powerset-lattice(T;eq) ==  mk-distributive-lattice(fset(T); λa,b. a ⋂ b; λa,b. a ⋃ b)

Lemma: fin-powerset-lattice_wf
[T:Type]. ∀[eq:EqDecider(T)].  (fin-powerset-lattice(T;eq) ∈ DistributiveLattice)

Definition: finite-powerset-lattice
finite-powerset-lattice(T;eq;whole) ==  {points=fset(T);meet=λa,b. a ⋂ b;join=λa,b. a ⋃ b;0={};1=whole}

Lemma: finite-powerset-lattice_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[whole:fset(T)].
  finite-powerset-lattice(T;eq;whole) ∈ BoundedDistributiveLattice supposing ∀x:T. x ∈ whole

Definition: sub-powerset-lattice
sub-powerset-lattice(T;eq;whole;P) ==  {points={s:fset(T)| s} ;meet=λa,b. a ⋂ b;join=λa,b. a ⋃ b;0={};1=whole}

Lemma: sub-powerset-lattice_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[whole:fset(T)]. ∀[P:fset(T) ⟶ ℙ].
  sub-powerset-lattice(T;eq;whole;P) ∈ BoundedDistributiveLattice 
  supposing (∀x:T. x ∈ whole) ∧ (∀a,b:fset(T).  ((P a)  (P b)  ((P a ⋃ b) ∧ (P a ⋂ b)))) ∧ (P {}) ∧ (P whole)

Definition: up-set-lattice
up-set-lattice(T;eq;whole;x,y.le[x; y]) ==  sub-powerset-lattice(T;eq;whole;λs.∀x,y:T.  (x ∈  le[x; y]  y ∈ s))

Lemma: up-set-lattice_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[whole:fset(T)]. ∀[le:T ⟶ T ⟶ ℙ].
  up-set-lattice(T;eq;whole;x,y.le[x;y]) ∈ BoundedDistributiveLattice supposing (∀x:T. x ∈ whole) ∧ Trans(T;x,y.le[x;y])

Definition: constrained-antichain-lattice
constrained-antichain-lattice(T;eq;P) ==
  {points={ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;
   meet=λac1,ac2. glb(P;ac1;ac2);
   join=λac1,ac2. lub(P;ac1;ac2);
   0={};
   1={{}}}

Lemma: constrained-antichain-lattice_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹].
  constrained-antichain-lattice(T;eq;P) ∈ BoundedDistributiveLattice 
  supposing (∀x,y:fset(T).  (y ⊆  (↑(P x))  (↑(P y)))) ∧ (↑(P {}))

Lemma: cal-point
[T,eq,P:Top].
  (Point(constrained-antichain-lattice(T;eq;P)) {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} )

Definition: cal-filter
cal-filter(s;x.P[x]) ==  {x ∈ P[x]}

Lemma: cal-filter_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:Point(constrained-antichain-lattice(T;eq;P))]. ∀[Q:{x:fset(T)| 
                                                                                                          ↑P[x]}  ⟶ 𝔹].
  (cal-filter(s;x.Q[x]) ∈ Point(constrained-antichain-lattice(T;eq;P)))

Lemma: cal-filter-decomp
[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:Point(constrained-antichain-lattice(T;eq;P))]. ∀[Q:{x:fset(T)| 
                                                                                                          ↑P[x]}  ⟶ 𝔹].
  (s cal-filter(s;x.Q[x]) ∨ cal-filter(s;x.¬bQ[x]) ∈ Point(constrained-antichain-lattice(T;eq;P)))

Definition: free-dist-lattice-with-constraints
free-dist-lattice-with-constraints(T;eq;x.Cs[x]) ==
  constrained-antichain-lattice(T;eq;λs.fset-contains-none(eq;s;x.Cs[x]))

Lemma: free-dist-lattice-with-constraints_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))].
  (free-dist-lattice-with-constraints(T;eq;x.Cs[x]) ∈ BoundedDistributiveLattice)

Lemma: free-dlwc-point
[T,eq,Cs:Top].
  (Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) {ac:fset(fset(T))| 
                                                              (↑fset-antichain(eq;ac))
                                                              ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} )

Lemma: decidable__equal-free-dist-lattice-with-constraints-point
[T:Type]
  ∀eq:EqDecider(T). ∀Cs:T ⟶ fset(fset(T)). ∀a,b:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).
    Dec(a b ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))

Lemma: free-dlwc-point-subtype
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))].
  (Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) ⊆Point(free-dist-lattice(T; eq)))

Lemma: free-dlwc-meet
[T,eq,a,b,cs:Top].  (a ∧ glb(λs.fset-contains-none(eq;s;x.cs[x]);a;b))

Lemma: free-dlwc-join
[T,eq,a,b,cs:Top].  (a ∨ lub(λs.fset-contains-none(eq;s;x.cs[x]);a;b))

Lemma: free-dlwc-le
[T:Type]
  ∀eq:EqDecider(T). ∀cs:T ⟶ fset(fset(T)). ∀x,y:Point(free-dist-lattice-with-constraints(T;eq;x.cs[x])).
    (x ≤ ⇐⇒ fset-ac-le(eq;x;y))

Definition: free-dlwc-inc
free-dlwc-inc(eq;a.Cs[a];x) ==  if fset-null({c ∈ Cs[x] deq-f-subset(eq) {x}}) then {{x}} else {} fi 

Lemma: free-dlwc-inc_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[x:T].
  (free-dlwc-inc(eq;a.Cs[a];x) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))

Lemma: free-dlwc-1
[T:Type]
  ∀eq:EqDecider(T). ∀Cs:T ⟶ fset(fset(T)). ∀x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).
    (x 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) ⇐⇒ {} ∈ x)

Lemma: free-dlwc-1-join-irreducible
T:Type. ∀eq:EqDecider(T). ∀Cs:T ⟶ fset(fset(T)). ∀x,y:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).
  (x ∨ 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
  ⇐⇒ (x 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
      ∨ (y 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))))

Definition: lattice-extend-wc
lattice-extend-wc(L;eq;eqL;f;ac) ==  lattice-extend(L;eq;eqL;f;ac)

Lemma: lattice-extend-wc_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
[f:T ⟶ Point(L)]. ∀[ac:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
  (lattice-extend-wc(L;eq;eqL;f;ac) ∈ Point(L))

Lemma: lattice-extend-wc-1
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
[f:T ⟶ Point(L)].
  (lattice-extend-wc(L;eq;eqL;f;1) 1 ∈ Point(L))

Lemma: lattice-extend-dlwc-inc
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
[f:T ⟶ Point(L)].
  ∀[x:T]. (lattice-extend-wc(L;eq;eqL;f;free-dlwc-inc(eq;a.Cs[a];x)) (f x) ∈ Point(L)) 
  supposing ∀x:T. ∀c:fset(T).  (c ∈ Cs[x]  (/\(f"(c)) 0 ∈ Point(L)))

Lemma: lattice-fset-meet-free-dlwc-inc
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[s:fset(T)].
  /\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s)) {s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) 
  supposing ↑fset-contains-none(eq;s;x.Cs[x])

Lemma: free-dlwc-basis
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
  (x \/(λs./\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s))"(x)) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))

Lemma: free-dlwc-satisfies-constraints
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))].
  ((∀x:T. ∀c:fset(T).  (c ∈ Cs[x]  x ∈ c))
   (∀x:T. ∀c:fset(T).
        (c ∈ Cs[x]
         (/\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(c)) 0 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))))))

Lemma: lattice-extend-wc-order-preserving
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
[f:T ⟶ Point(L)]. ∀[x,y:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
  lattice-extend-wc(L;eq;eqL;f;x) ≤ lattice-extend-wc(L;eq;eqL;f;y) supposing x ≤ y

Lemma: lattice-extend-wc-join
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
[f:T ⟶ Point(L)]. ∀[a,b:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
  lattice-extend-wc(L;eq;eqL;f;a ∨ b) ≤ lattice-extend-wc(L;eq;eqL;f;a) ∨ lattice-extend-wc(L;eq;eqL;f;b)

Lemma: lattice-extend-wc-meet
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
[f:T ⟶ Point(L)].
  ∀[a,b:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
    lattice-extend-wc(L;eq;eqL;f;a) ∧ lattice-extend-wc(L;eq;eqL;f;b) ≤ lattice-extend-wc(L;eq;eqL;f;a ∧ b) 
  supposing ∀x:T. ∀c:fset(T).  (c ∈ Cs[x]  (/\(f"(c)) 0 ∈ Point(L)))

Lemma: lattice-extend-is-hom-constrained
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
[f:T ⟶ Point(L)].
  λac.lattice-extend-wc(L;eq;eqL;f;ac) ∈ Hom(free-dist-lattice-with-constraints(T;eq;x.Cs[x]);L) 
  supposing ∀x:T. ∀c:fset(T).  (c ∈ Cs[x]  (/\(f"(c)) 0 ∈ Point(L)))

Lemma: free-dist-lattice-with-constraints-property
[T:Type]
  ∀eq:EqDecider(T)
    ∀[Cs:T ⟶ fset(fset(T))]
      ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f:T ⟶ Point(L).
        ∃g:Hom(free-dist-lattice-with-constraints(T;eq;x.Cs[x]);L)
         (f (g x.free-dlwc-inc(eq;a.Cs[a];x))) ∈ (T ⟶ Point(L))) 
        supposing ∀x:T. ∀c:fset(T).  (c ∈ Cs[x]  (/\(f"(c)) 0 ∈ Point(L)))

Definition: face-lattice-constraints
face-lattice-constraints(x) ==  case of inl(a) => {{inl a,inr }} inr(a) => {{inl a,inr }}

Lemma: face-lattice-constraints_wf
[T:Type]. ∀[x:T T].  (face-lattice-constraints(x) ∈ fset(fset(T T)))

Definition: face-lattice
face-lattice(T;eq) ==  free-dist-lattice-with-constraints(T T;union-deq(T;T;eq;eq);x.face-lattice-constraints(x))

Lemma: face-lattice_wf
[T:Type]. ∀[eq:EqDecider(T)].  (face-lattice(T;eq) ∈ BoundedDistributiveLattice)

Definition: face-lattice0
(x=0) ==  {{inl x}}

Lemma: face-lattice0-is-inc
T:Type. ∀eq:EqDecider(T). ∀x:T.  ((x=0) free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inl x))

Lemma: face-lattice0_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T].  ((x=0) ∈ Point(face-lattice(T;eq)))

Definition: face-lattice1
(x=1) ==  {{inr }}

Lemma: face-lattice1-is-inc
T:Type. ∀eq:EqDecider(T). ∀x:T.  ((x=1) free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inr ))

Lemma: face-lattice1_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T].  ((x=1) ∈ Point(face-lattice(T;eq)))

Lemma: fl-point
[T:Type]. ∀[eq:EqDecider(T)].
  Point(face-lattice(T;eq)) ≡ {ac:fset(fset(T T))| 
                               (↑fset-antichain(union-deq(T;T;eq;eq);ac))
                               ∧ (∀a:fset(T T). (a ∈ ac  (∀z:T. (inl z ∈ a ∧ inr z  ∈ a)))))} 

Lemma: fl-point-sq
[T,eq:Top].
  (Point(face-lattice(T;eq)) {ac:fset(fset(T T))| 
                                (↑fset-antichain(union-deq(T;T;eq;eq);ac))
                                ∧ fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;
                                                                             eq);a;x.face-lattice-constraints(x)))} )

Definition: fl-deq
fl-deq(T;eq) ==  deq-fset(deq-fset(union-deq(T;T;eq;eq)))

Lemma: fl-deq_wf
[T:Type]. ∀[eq:EqDecider(T)].  (fl-deq(T;eq) ∈ EqDecider(Point(face-lattice(T;eq))))

Lemma: decidable__equal-fl-point
[T:Type]. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).  Dec(x y ∈ Point(face-lattice(T;eq)))

Definition: fl-vertex
fl-vertex(u) ==  {{u}}

Lemma: fl-vertex_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[u:T T].  (fl-vertex(u) ∈ Point(face-lattice(T;eq)))

Lemma: fl-meet-0-1
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T].  ((x=0) ∧ (x=1) 0 ∈ Point(face-lattice(T;eq)))

Lemma: face-lattice-property
T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f0,f1:T ⟶ Point(L).
  ∃g:Hom(face-lattice(T;eq);L) [(∀x:T. (((g (x=0)) (f0 x) ∈ Point(L)) ∧ ((g (x=1)) (f1 x) ∈ Point(L))))] 
  supposing ∀x:T. (f0 x ∧ f1 0 ∈ Point(L))

Lemma: face-lattice-basis
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(face-lattice(T;eq))].
  (x \/(λs./\(λu.{{u}}"(s))"(x)) ∈ Point(face-lattice(T;eq)))

Lemma: face-lattice-induction
T:Type. ∀eq:EqDecider(T).
  ∀[P:Point(face-lattice(T;eq)) ⟶ ℙ]
    ((∀x:Point(face-lattice(T;eq)). SqStable(P[x]))
     P[0]
     P[1]
     (∀x,y:Point(face-lattice(T;eq)).  (P[x]  P[y]  P[x ∨ y]))
     (∀x:Point(face-lattice(T;eq)). (P[x]  (∀i:T. (P[(i=0) ∧ x] ∧ P[(i=1) ∧ x]))))
     (∀x:Point(face-lattice(T;eq)). P[x]))

Lemma: face-lattice-le-1
T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).  (x ≤ ⇐⇒ fset-ac-le(union-deq(T;T;eq;eq);x;y))

Lemma: face-lattice-le
T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).
  (x ≤ ⇐⇒ ∀s:fset(T T). (s ∈  (↓∃t:fset(T T). (t ∈ y ∧ t ⊆ s))))

Lemma: face-lattice-subset-le
T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).  (x ⊆  x ≤ y)

Definition: fl-filter
fl-filter(s;x.Q[x]) ==  cal-filter(s;x.Q[x])

Lemma: fl-filter_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Q:{x:fset(T T)| 
                                    ↑fset-contains-none(union-deq(T;T;eq;eq);x;x.face-lattice-constraints(x))}  ⟶ 𝔹].
[s:Point(face-lattice(T;eq))].
  (fl-filter(s;x.Q[x]) ∈ Point(face-lattice(T;eq)))

Lemma: fl-filter-subset
[T:Type]. ∀[eq:EqDecider(T)]. ∀[Q:fset(T T) ⟶ 𝔹]. ∀[s:fset(fset(T T))].  fl-filter(s;x.Q[x]) ⊆ s

Lemma: fl-filter-filter
[P,Q,s:Top].  (fl-filter(fl-filter(s;x.P[x]);x.Q[x]) fl-filter(s;x.P[x] ∧b Q[x]))

Lemma: fl-filter-decomp
[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:Point(face-lattice(T;eq))].
[Q:{x:fset(T T)| ↑fset-contains-none(union-deq(T;T;eq;eq);x;x.face-lattice-constraints(x))}  ⟶ 𝔹].
  (s fl-filter(s;x.Q[x]) ∨ fl-filter(s;x.¬bQ[x]) ∈ Point(face-lattice(T;eq)))

Lemma: fset-ac-le-face-lattice0
[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T]. ∀[s:fset(fset(T T))].
  (fset-all(s;x.inl i ∈b x) ⇐⇒ fset-ac-le(union-deq(T;T;eq;eq);s;(i=0)))

Lemma: fset-ac-le-face-lattice1
[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T]. ∀[s:fset(fset(T T))].
  (fset-all(s;x.inr i  ∈b x) ⇐⇒ fset-ac-le(union-deq(T;T;eq;eq);s;(i=1)))

Lemma: implies-le-face-lattice-join
T:Type. ∀eq:EqDecider(T). ∀x,y,z:Point(face-lattice(T;eq)).
  ((∀s:fset(T T). (s ∈  ((↓∃t:fset(T T). (t ∈ x ∧ t ⊆ s)) ∨ (↓∃t:fset(T T). (t ∈ y ∧ t ⊆ s)))))  z ≤ x ∨ y)

Lemma: implies-le-face-lattice-join3
T:Type. ∀eq:EqDecider(T). ∀u,x,y,z:Point(face-lattice(T;eq)).
  ((∀s:fset(T T)
      (s ∈ z
       ((↓∃t:fset(T T). (t ∈ u ∧ t ⊆ s))
         ∨ (↓∃t:fset(T T). (t ∈ x ∧ t ⊆ s))
         ∨ (↓∃t:fset(T T). (t ∈ y ∧ t ⊆ s)))))
   z ≤ u ∨ x ∨ y)

Definition: fl-all
(∀i.phi) ==  fl-filter(phi;x.(¬binl i ∈b x) ∧b binr i  ∈b x))

Lemma: fl-all_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[phi:Point(face-lattice(T;eq))]. ∀[i:T].  ((∀i.phi) ∈ Point(face-lattice(T;eq)))

Lemma: fl-all-decomp
[T:Type]. ∀[eq:EqDecider(T)]. ∀[phi:Point(face-lattice(T;eq))]. ∀[i:T].
  (phi (∀i.phi) ∨ phi ∧ (i=0) ∨ phi ∧ (i=1) ∈ Point(face-lattice(T;eq)))

Definition: fl-lift
fl-lift(T;eq;L;eqL;f0;f1) ==  TERMOF{face-lattice-property:o, 1:l, 1:l} eq eqL f0 f1

Lemma: fl-lift_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f0,f1:T ⟶ Point(L)].
  fl-lift(T;eq;L;eqL;f0;f1) ∈ {g:Hom(face-lattice(T;eq);L)| 
                               ∀x:T. (((g (x=0)) (f0 x) ∈ Point(L)) ∧ ((g (x=1)) (f1 x) ∈ Point(L)))}  
  supposing ∀x:T. (f0 x ∧ f1 0 ∈ Point(L))

Lemma: face-lattice-hom-unique
T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f0,f1:T ⟶ Point(L).
  ∀[g,h:Hom(face-lattice(T;eq);L)].
    h ∈ Hom(face-lattice(T;eq);L) 
    supposing (∀x:T. (g (x=0) ∧ (x=1) 0 ∈ Point(L)))
    ∧ (∀x:T. ((g (x=0)) (h (x=0)) ∈ Point(L)))
    ∧ (∀x:T. ((g (x=1)) (h (x=1)) ∈ Point(L)))

Lemma: face-lattice-1-join-irreducible
T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).
  (x ∨ 1 ∈ Point(face-lattice(T;eq)) ⇐⇒ (x 1 ∈ Point(face-lattice(T;eq))) ∨ (y 1 ∈ Point(face-lattice(T;eq))))

Lemma: fl-lift-unique
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f0,f1:T ⟶ Point(L)].
  ∀g:Hom(face-lattice(T;eq);L)
    fl-lift(T;eq;L;eqL;f0;f1) g ∈ Hom(face-lattice(T;eq);L) 
    supposing ∀x:T. (((g (x=0)) (f0 x) ∈ Point(L)) ∧ ((g (x=1)) (f1 x) ∈ Point(L))) 
  supposing ∀x:T. (f0 x ∧ f1 0 ∈ Point(L))

Lemma: fl-lift-unique2
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f0,f1:T ⟶ Point(L)].
  ∀g:Hom(face-lattice(T;eq);L)
    ∀x:Point(face-lattice(T;eq)). ((fl-lift(T;eq;L;eqL;f0;f1) x) (g x) ∈ Point(L)) 
    supposing ∀x:T. (((g (x=0)) (f0 x) ∈ Point(L)) ∧ ((g (x=1)) (f1 x) ∈ Point(L))) 
  supposing ∀x:T. (f0 x ∧ f1 0 ∈ Point(L))

Definition: free-DeMorgan-lattice
free-DeMorgan-lattice(T;eq) ==  free-dist-lattice(T T; union-deq(T;T;eq;eq))

Lemma: free-DeMorgan-lattice_wf
[T:Type]. ∀[eq:EqDecider(T)].  (free-DeMorgan-lattice(T;eq) ∈ BoundedDistributiveLattice)

Definition: free-dml-deq
free-dml-deq(T;eq) ==  deq-fset(deq-fset(union-deq(T;T;eq;eq)))

Lemma: free-dml-deq_wf
[T:Type]. ∀[eq:EqDecider(T)].  (free-dml-deq(T;eq) ∈ EqDecider(Point(free-DeMorgan-lattice(T;eq))))

Lemma: free-dml-0-not-1
T:Type. ∀eq:EqDecider(T).  (0 1 ∈ Point(free-DeMorgan-lattice(T;eq))))

Definition: is-dml-1
is-dml-1(T;eq;x) ==  free-dml-deq(T;eq) 1

Lemma: is-dml-1_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-DeMorgan-lattice(T;eq))].  (is-dml-1(T;eq;x) ∈ 𝔹)

Lemma: assert-is-dml-1
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-DeMorgan-lattice(T;eq))].
  uiff(↑is-dml-1(T;eq;x);x 1 ∈ Point(free-DeMorgan-lattice(T;eq)))

Definition: dminc
<i> ==  free-dl-inc(inl i)

Lemma: dminc_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T].  (<i> ∈ Point(free-DeMorgan-lattice(T;eq)))

Definition: dmopp
<1-i> ==  free-dl-inc(inr )

Lemma: dmopp_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T].  (<1-i> ∈ Point(free-DeMorgan-lattice(T;eq)))

Definition: dm-neg
¬(x) ==
  lattice-extend(opposite-lattice(free-DeMorgan-lattice(T;eq));union-deq(T;T;eq;eq);
                 deq-fset(deq-fset(union-deq(T;T;eq;eq)));λz.case of inl(a) => {{inr }} inr(a) => {{inl a}};x)

Lemma: dm-neg_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-DeMorgan-lattice(T;eq))].  (x) ∈ Point(free-DeMorgan-lattice(T;eq)))

Lemma: dm-neg-is-hom
[T:Type]. ∀[eq:EqDecider(T)].
  x.¬(x) ∈ Hom(free-DeMorgan-lattice(T;eq);opposite-lattice(free-DeMorgan-lattice(T;eq))))

Lemma: dm-neg-properties
[T:Type]. ∀[eq:EqDecider(T)].
  ((∀[x,y:Point(free-DeMorgan-lattice(T;eq))].  (x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(free-DeMorgan-lattice(T;eq))))
  ∧ (∀[x,y:Point(free-DeMorgan-lattice(T;eq))].  (x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(free-DeMorgan-lattice(T;eq))))
  ∧ (0) 1 ∈ Point(free-DeMorgan-lattice(T;eq)))
  ∧ (1) 0 ∈ Point(free-DeMorgan-lattice(T;eq))))

Lemma: dm-neg-is-hom-opposite
[T:Type]. ∀[eq:EqDecider(T)].
  x.¬(x) ∈ Hom(opposite-lattice(free-DeMorgan-lattice(T;eq));free-DeMorgan-lattice(T;eq)))

Lemma: dm-neg-opp
[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T].  (<1-i>= <i> ∈ Point(free-DeMorgan-lattice(T;eq)))

Lemma: dm-neg-inc
[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T].  (<i>= <1-i> ∈ Point(free-DeMorgan-lattice(T;eq)))

Lemma: dm-neg-neg
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-DeMorgan-lattice(T;eq))].
  (x)) x ∈ Point(free-DeMorgan-lattice(T;eq)))

Definition: DeMorgan-algebra-structure
DeMorganAlgebraStructure ==
  "Point":Type
  "meet":self."Point" ⟶ self."Point" ⟶ self."Point"
  "join":self."Point" ⟶ self."Point" ⟶ self."Point"
  "1":self."Point"
  "0":self."Point"
  "neg":self."Point" ⟶ self."Point"

Lemma: DeMorgan-algebra-structure_wf
DeMorganAlgebraStructure ∈ 𝕌'

Lemma: DeMorgan-algebra-structure-subtype
DeMorganAlgebraStructure ⊆BoundedLatticeStructure

Definition: dma-neg
¬(x) ==  dma."neg" x

Lemma: dma-neg_wf
[dma:DeMorganAlgebraStructure]. ∀[x:Point(dma)].  (x) ∈ Point(dma))

Definition: DeMorgan-algebra-axioms
DeMorgan-algebra-axioms(dma) ==
  (∀x:Point(dma). (x)) x ∈ Point(dma))) ∧ (∀x,y:Point(dma).  (x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(dma)))

Lemma: DeMorgan-algebra-axioms_wf
[dma:DeMorganAlgebraStructure]. (DeMorgan-algebra-axioms(dma) ∈ ℙ)

Definition: DeMorgan-algebra
DeMorganAlgebra ==
  {dma:DeMorganAlgebraStructure| 
   lattice-axioms(dma)
   ∧ bounded-lattice-axioms(dma)
   ∧ (∀[a,b,c:Point(dma)].  (a ∧ b ∨ a ∧ b ∨ a ∧ c ∈ Point(dma)))
   ∧ DeMorgan-algebra-axioms(dma)} 

Lemma: DeMorgan-algebra_wf
DeMorganAlgebra ∈ 𝕌'

Lemma: DeMorgan-algebra-subtype
DeMorganAlgebra ⊆BoundedDistributiveLattice

Lemma: DeMorgan-algebra-laws
[dma:DeMorganAlgebra]
  ((∀x:Point(dma). (x)) x ∈ Point(dma)))
  ∧ (∀x,y:Point(dma).  (x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(dma)))
  ∧ (∀x,y:Point(dma).  (x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(dma)))
  ∧ (0) 1 ∈ Point(dma))
  ∧ (1) 0 ∈ Point(dma)))

Lemma: implies-DeMorgan-algebra-axioms
[dma:DeMorganAlgebraStructure]
  ((∀x:Point(dma). (x)) x ∈ Point(dma)))
   (∀x,y:Point(dma).  (x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(dma)))
   DeMorgan-algebra-axioms(dma))

Definition: mk-DeMorgan-algebra
mk-DeMorgan-algebra(L;n) ==  L["neg" := n]

Lemma: mk-DeMorgan-algebra_wf
[L:BoundedDistributiveLattice]. ∀[n:Point(L) ⟶ Point(L)].
  mk-DeMorgan-algebra(L;n) ∈ DeMorganAlgebra 
  supposing (∀x:Point(L). ((n (n x)) x ∈ Point(L)))
  ∧ ((∀x,y:Point(L).  ((n x ∧ y) x ∨ y ∈ Point(L))) ∨ (∀x,y:Point(L).  ((n x ∨ y) x ∧ y ∈ Point(L))))

Lemma: mk-DeMorgan-algebra-equal-bounded-lattice
[L:BoundedLatticeStructure]. ∀[n:Top].  (mk-DeMorgan-algebra(L;n) L ∈ BoundedLatticeStructure)

Definition: dma-hom
dma-hom(dma1;dma2) ==  {f:Hom(dma1;dma2)| ∀[a:Point(dma1)]. (f a) (f ¬(a)) ∈ Point(dma2))} 

Lemma: dma-hom_wf
[dma1:DeMorganAlgebra]. ∀dma2:DeMorganAlgebra. (dma-hom(dma1;dma2) ∈ Type)

Lemma: id-is-dma-hom
[dma:DeMorganAlgebra]. x.x ∈ dma-hom(dma;dma))

Lemma: compose-dma-hom
[dma1,dma2,dma3:DeMorganAlgebra]. ∀[f:dma-hom(dma1;dma2)]. ∀[g:dma-hom(dma2;dma3)].  (g f ∈ dma-hom(dma1;dma3))

Definition: free-DeMorgan-algebra
free-DeMorgan-algebra(T;eq) ==  mk-DeMorgan-algebra(free-DeMorgan-lattice(T;eq);λx.¬(x))

Lemma: free-DeMorgan-algebra_wf
[T:Type]. ∀[eq:EqDecider(T)].  (free-DeMorgan-algebra(T;eq) ∈ DeMorganAlgebra)

Lemma: free-dma-point
[T,eq:Top].  (Point(free-DeMorgan-algebra(T;eq)) Point(free-DeMorgan-lattice(T;eq)))

Lemma: free-dma-point-subtype
[T:Type]. ∀[eq:EqDecider(T)].  (Point(free-DeMorgan-lattice(T;eq)) ⊆Point(free-DeMorgan-algebra(T;eq)))

Lemma: free-dma-neg
[T,eq,x:Top].  (x) ~ ¬(x))

Lemma: free-dma-hom-is-lattice-hom
[T:Type]. ∀[eq:EqDecider(T)]. ∀[dm:BoundedDistributiveLattice].
  (Hom(free-DeMorgan-lattice(T;eq);dm) Hom(free-DeMorgan-algebra(T;eq);dm) ∈ Type)

Lemma: free-DeMorgan-algebra-property
T:Type. ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm).
  (∃g:dma-hom(free-DeMorgan-algebra(T;eq);dm) [(∀i:T. ((g <i>(f i) ∈ Point(dm)))])

Definition: free-dma-lift
free-dma-lift(T;eq;dm;eq2;f) ==  TERMOF{free-DeMorgan-algebra-property:o, 1:l, 1:l} eq dm eq2 f

Lemma: free-dma-lift_wf
T:Type. ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm).
  (free-dma-lift(T;eq;dm;eq2;f) ∈ {g:dma-hom(free-DeMorgan-algebra(T;eq);dm)| ∀i:T. ((g <i>(f i) ∈ Point(dm))} )

Lemma: free-dma-lift-inc
T:Type. ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm). ∀i:T.
  ((free-dma-lift(T;eq;dm;eq2;f) <i>(f i) ∈ Point(dm))

Lemma: free-dma-lift-0
T:Type. ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm).
x:Point(free-DeMorgan-algebra(T;eq)).
  (free-dma-lift(T;eq;dm;eq2;f) x) 0 ∈ Point(dm) supposing 0 ∈ Point(free-DeMorgan-algebra(T;eq))

Lemma: free-DeMorgan-algebra-hom-unique
[T:Type]. ∀[eq:EqDecider(T)]. ∀[dm:DeMorganAlgebra]. ∀[eq2:EqDecider(Point(dm))].
  ∀f:T ⟶ Point(dm)
    ∀[g,h:dma-hom(free-DeMorgan-algebra(T;eq);dm)].
      h ∈ dma-hom(free-DeMorgan-algebra(T;eq);dm) supposing ∀i:T. ((g <i>(h <i>) ∈ Point(dm))

Lemma: free-dma-lift-unique
[T:Type]. ∀[eq:EqDecider(T)]. ∀[dm:DeMorganAlgebra]. ∀[eq2:EqDecider(Point(dm))]. ∀[f:T ⟶ Point(dm)].
[g:dma-hom(free-DeMorgan-algebra(T;eq);dm)].
  free-dma-lift(T;eq;dm;eq2;f) g ∈ dma-hom(free-DeMorgan-algebra(T;eq);dm) 
  supposing ∀i:T. ((g <i>(f i) ∈ Point(dm))

Lemma: free-dma-lift-unique2
[T:Type]. ∀[eq:EqDecider(T)]. ∀[dm:DeMorganAlgebra]. ∀[eq2:EqDecider(Point(dm))]. ∀[f:T ⟶ Point(dm)].
[g:dma-hom(free-DeMorgan-algebra(T;eq);dm)].
  ∀x:Point(free-DeMorgan-algebra(T;eq)). ((free-dma-lift(T;eq;dm;eq2;f) x) (g x) ∈ Point(dm)) 
  supposing ∀i:T. ((g <i>(f i) ∈ Point(dm))

Lemma: free-dma-lift-id
T:Type. ∀eq:EqDecider(T).
  (free-dma-lift(T;eq;free-DeMorgan-algebra(T;eq);free-dml-deq(T;eq);λi.<i>)
  x.x)
  ∈ dma-hom(free-DeMorgan-algebra(T;eq);free-DeMorgan-algebra(T;eq)))

Definition: dma-lift-compose
dma-lift-compose(I;J;eqi;eqj;f;g) ==  free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f) g

Lemma: dma-lift-compose_wf
[I,J,K:Type]. ∀[eqi:EqDecider(I)]. ∀[eqj:EqDecider(J)]. ∀[f:J ⟶ Point(free-DeMorgan-algebra(I;eqi))].
[g:K ⟶ Point(free-DeMorgan-algebra(J;eqj))].
  (dma-lift-compose(I;J;eqi;eqj;f;g) ∈ K ⟶ Point(free-DeMorgan-algebra(I;eqi)))

Lemma: dma-lift-compose-assoc
[I,J,K,H:Type]. ∀[eqi:EqDecider(I)]. ∀[eqj:EqDecider(J)]. ∀[eqk:EqDecider(K)].
[f:J ⟶ Point(free-DeMorgan-algebra(I;eqi))]. ∀[g:K ⟶ Point(free-DeMorgan-algebra(J;eqj))].
[h:H ⟶ Point(free-DeMorgan-algebra(K;eqk))].
  (dma-lift-compose(I;K;eqi;eqk;dma-lift-compose(I;J;eqi;eqj;f;g);h)
  dma-lift-compose(I;J;eqi;eqj;f;dma-lift-compose(J;K;eqj;eqk;g;h))
  ∈ (H ⟶ Point(free-DeMorgan-algebra(I;eqi))))

Definition: real-interval-lattice
real-interval-lattice(I) ==  mk-distributive-lattice({r:ℝr ∈ I} ; λ2y.rmin(x;y); λ2y.rmax(x;y))

Lemma: real-interval-lattice_wf
[I:Interval]. (real-interval-lattice(I) ∈ DistributiveLattice)

Definition: general-bounded-lattice-structure
generalized bounded lattice structure includes
all the components of bounded lattice, and, in addition, 
relation on the points of the lattice.

When we define generalized bounded lattice, will be an
equivalence relation on the points, and the lattice axioms
will hold upto E-equivalence.⋅

GeneralBoundedLatticeStructure ==
  "Point":Type
  "meet":self."Point" ⟶ self."Point" ⟶ self."Point"
  "join":self."Point" ⟶ self."Point" ⟶ self."Point"
  "1":self."Point"
  "0":self."Point"
  "E":self."Point" ⟶ self."Point" ⟶ ℙ

Lemma: general-bounded-lattice-structure_wf
GeneralBoundedLatticeStructure ∈ 𝕌'

Lemma: general-bounded-lattice-structure-subtype
GeneralBoundedLatticeStructure ⊆BoundedLatticeStructure

Definition: lattice-equiv
a ≡ ==  l."E" b

Lemma: lattice-equiv_wf
[l:GeneralBoundedLatticeStructure]. ∀[a,b:Point(l)].  (a ≡ b ∈ ℙ)

Definition: general-lattice-axioms
is an equivalence relation on the lattice points.
The usual axioms for bounded lattice hold "upto E-equivalence".

For example the (constructive) real numbers in closed interval
form generalized bounded lattice where is ⌜y⌝ (req).⋅

general-lattice-axioms(l) ==
  EquivRel(Point(l);a,b.a ≡ b)
  ∧ (∀[a,b:Point(l)].  a ∧ b ≡ b ∧ a)
  ∧ (∀[a,b:Point(l)].  a ∨ b ≡ b ∨ a)
  ∧ (∀[a,b,c:Point(l)].  a ∧ b ∧ c ≡ a ∧ b ∧ c)
  ∧ (∀[a,b,c:Point(l)].  a ∨ b ∨ c ≡ a ∨ b ∨ c)
  ∧ (∀[a,b:Point(l)].  a ∨ a ∧ b ≡ a)
  ∧ (∀[a,b:Point(l)].  a ∧ a ∨ b ≡ a)
  ∧ (∀[a:Point(l)]. a ∨ 0 ≡ a)
  ∧ (∀[a:Point(l)]. a ∧ 1 ≡ a)

Lemma: general-lattice-axioms_wf
[l:GeneralBoundedLatticeStructure]. (general-lattice-axioms(l) ∈ ℙ)

Definition: general-bounded-lattice
GeneralBoundedLattice ==  {l:GeneralBoundedLatticeStructure| general-lattice-axioms(l)} 

Lemma: general-bounded-lattice_wf
GeneralBoundedLattice ∈ 𝕌'

Definition: mk-general-bounded-lattice
mk-general-bounded-lattice(T;m;j;z;o;E) ==  λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o]["E" := E]

Lemma: mk-general-bounded-lattice_wf
[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T]. ∀[E:T ⟶ T ⟶ ℙ].
  mk-general-bounded-lattice(T;m;j;z;o;E) ∈ GeneralBoundedLattice 
  supposing EquivRel(T;x,y.E y)
  ∧ (∀[a,b:T].  (E m[a;b] m[b;a]))
  ∧ (∀[a,b:T].  (E j[a;b] j[b;a]))
  ∧ (∀[a,b,c:T].  (E m[a;m[b;c]] m[m[a;b];c]))
  ∧ (∀[a,b,c:T].  (E j[a;j[b;c]] j[j[a;b];c]))
  ∧ (∀[a,b:T].  (E j[a;m[a;b]] a))
  ∧ (∀[a,b:T].  (E m[a;j[a;b]] a))
  ∧ (∀[a:T]. (E m[a;o] a))
  ∧ (∀[a:T]. (E j[a;z] a))

Definition: general-bounded-distributive-lattice
GeneralBoundedDistributiveLattice ==
  {l:GeneralBoundedLatticeStructure| general-lattice-axioms(l) ∧ (∀[a,b,c:Point(l)].  a ∧ b ∨ c ≡ a ∧ b ∨ a ∧ c)} 

Lemma: general-bounded-distributive-lattice_wf
GeneralBoundedDistributiveLattice ∈ 𝕌'

Definition: mk-general-bounded-dist-lattice
mk-general-bounded-dist-lattice(T;m;j;z;o;E) ==  mk-general-bounded-lattice(T;m;j;z;o;E)

Lemma: mk-general-bounded-dist-lattice_wf
[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T]. ∀[E:T ⟶ T ⟶ ℙ].
  mk-general-bounded-dist-lattice(T;m;j;z;o;E) ∈ GeneralBoundedDistributiveLattice 
  supposing EquivRel(T;x,y.E y)
  ∧ (∀[a,b:T].  (E m[a;b] m[b;a]))
  ∧ (∀[a,b:T].  (E j[a;b] j[b;a]))
  ∧ (∀[a,b,c:T].  (E m[a;m[b;c]] m[m[a;b];c]))
  ∧ (∀[a,b,c:T].  (E j[a;j[b;c]] j[j[a;b];c]))
  ∧ (∀[a,b:T].  (E j[a;m[a;b]] a))
  ∧ (∀[a,b:T].  (E m[a;j[a;b]] a))
  ∧ (∀[a:T]. (E m[a;o] a))
  ∧ (∀[a:T]. (E j[a;z] a))
  ∧ (∀[a,b,c:T].  (E m[a;j[b;c]] j[m[a;b];m[a;c]]))

Definition: real-closed-interval-lattice
For real numbers ⌜a ≤ b⌝the reals in the closed interval ⌜[a, b]⌝
form distributive lattice with meet ⌜rmin(x;y)⌝ and join ⌜rmax(x;y)⌝.
But they do not form bounded distributive lattice with and b
because we can't prove that ⌜rmin(a;x)⌝ is the same real as ⌜a⌝.
We can only prove that it is an "equivalent" real using the `req` relation
(that we display ⌜y⌝).

Thus the closed interval forms generalized-bounded-distributive-lattice.⋅

real-closed-interval-lattice(a;b) ==  mk-general-bounded-dist-lattice({r:ℝr ∈ [a, b]} 2y.rmin(x;y);λ2y.rmax(x;y)\000C;a;b;λ2y.x y)

Lemma: real-closed-interval-lattice_wf
[a,b:ℝ].  real-closed-interval-lattice(a;b) ∈ GeneralBoundedDistributiveLattice supposing a ≤ b

Definition: quotient-dl
l//x,y.eq[x; y] ==  {points=x,y:Point(l)//eq[x; y];meet=l."meet";join=l."join";0=l."0";1=l."1"}

Lemma: quotient-dl_wf
[l:BoundedDistributiveLattice]. ∀[eq:Point(l) ⟶ Point(l) ⟶ ℙ].
  (l//x,y.eq[x;y] ∈ BoundedDistributiveLattice) supposing 
     ((∀a,c,b,d:Point(l).  (eq[a;c]  eq[b;d]  eq[a ∨ b;c ∨ d])) and 
     (∀a,c,b,d:Point(l).  (eq[a;c]  eq[b;d]  eq[a ∧ b;c ∧ d])) and 
     EquivRel(Point(l);x,y.eq[x;y]))

Comment: free DeMorgan algebra using quotient doc
To construct the face lattice on an arbitrary type of generators,
we can start with the free distributive lattice ⌜free-dl(X X)⌝ on generators
X.  We call generator inl (x=0) and inr is (x=1).
Then we form quotient of that lattice so that (x=0) ∧ (x=1) 0 ∈ Point(free-dl(X X)).


Definition: flip-union
flip-union(x) ==  case of inl(a) => inr a  inr(a) => inl a

Lemma: flip-union_wf
[X:Type]. ∀[x:X X].  (flip-union(x) ∈ X)

Definition: flattice-order
flattice-order(X;as;bs) ==  (∀b∈bs.(∃x∈b. (∃y∈b. flip-union(x) ∈ (X X))) ∨ (∃a∈as. a ⊆ b))

Lemma: flattice-order_wf
[X:Type]. ∀[as,bs:(X X) List List].  (flattice-order(X;as;bs) ∈ ℙ)

Lemma: flattice-order_transitivity
[X:Type]. ∀as,bs,cs:(X X) List List.  (flattice-order(X;as;bs)  flattice-order(X;bs;cs)  flattice-order(X;as;cs))

Lemma: flattice-order-append
X:Type. ∀a1,b1,as,bs:(X X) List List.
  (flattice-order(X;a1;b1)  flattice-order(X;as;bs)  flattice-order(X;a1 as;b1 bs))

Lemma: flattice-order-meet
X:Type. ∀a1,b1,as,bs:(X X) List List.
  (flattice-order(X;a1;b1)  flattice-order(X;as;bs)  flattice-order(X;free-dl-meet(a1;as);free-dl-meet(b1;bs)))

Definition: flattice-equiv
flattice-equiv(X;x;y) ==
  ↓∃as,bs:(X X) List List
    ((x as ∈ Point(free-dl(X X)))
    ∧ (y bs ∈ Point(free-dl(X X)))
    ∧ flattice-order(X;as;bs)
    ∧ flattice-order(X;bs;as))

Lemma: flattice-equiv_wf
[X:Type]. ∀[x,y:Point(free-dl(X X))].  (flattice-equiv(X;x;y) ∈ ℙ)

Lemma: flattice-equiv-equiv
[X:Type]. EquivRel(Point(free-dl(X X));x,y.flattice-equiv(X;x;y))

Definition: f-lattice
f-lattice(X) ==  free-dl(X X)//x,y.flattice-equiv(X;x;y)

Lemma: f-lattice_wf
[X:Type]. (f-lattice(X) ∈ BoundedDistributiveLattice)



Home Index