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 ∧ b ==  l."meet" a b`

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

Definition: lattice-join
`a ∨ b ==  l."join" a 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 = b ∧ a ∈ Point(l)))`
`  ∧ (∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l)))`
`  ∧ (∀[a,b,c:Point(l)].  (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l)))`
`  ∧ (∀[a,b,c:Point(l)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l)))`
`  ∧ (∀[a,b:Point(l)].  (a ∨ a ∧ b = a ∈ Point(l)))`
`  ∧ (∀[a,b:Point(l)].  (a ∧ a ∨ b = 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 = b ∧ a ∈ Point(l)))`
`  ∧ (∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l)))`
`  ∧ (∀[a,b,c:Point(l)].  (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l)))`
`  ∧ (∀[a,b,c:Point(l)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l)))`
`  ∧ (∀[a,b:Point(l)].  (a ∨ a ∧ b = a ∈ Point(l)))`
`  ∧ (∀[a,b:Point(l)].  (a ∧ a ∨ b = a ∈ Point(l))))`

Definition: lattice-le
`a ≤ b ==  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 b = (f a ∧ b) ∈ Point(l2)) ∧ (f a ∨ f b = (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 o 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 ⊆r 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
`1 ==  l."1"`

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

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

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

Definition: bounded-lattice-axioms
`bounded-lattice-axioms(l) ==  (∀[a:Point(l)]. (a ∨ 0 = a ∈ Point(l))) ∧ (∀[a:Point(l)]. (a ∧ 1 = 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 ⊆r 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;λ2A B.e-isect(A;B);λ2A B.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;λ2A B.p-and(A;B);λ2A B.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)].`
`  f = 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 o 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 ∨ c = 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 ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l)))} `

Lemma: bdd-distributive-lattice_wf
`BoundedDistributiveLattice ∈ 𝕌'`

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

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

Lemma: bdd-distributive-lattice-subtype-distributive-lattice
`BoundedDistributiveLattice ⊆r 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 = u ∈ Point(l))`

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

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

Lemma: lattice-le_transitivity
`∀[l:Lattice]. ∀[a,b,c:Point(l)].  (a ≤ c) supposing (a ≤ b 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 ∧ b `⇐⇒` 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 ≤ c `⇐⇒` 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 ∧ c = a ∨ b ∧ a ∨ c ∈ Point(L))`

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

Lemma: distributive-lattice-dual-distrib2
`∀[L:DistributiveLattice]. ∀[a,b,c:Point(L)].  (b ∧ c ∨ a = 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 ∧ x = 0 ∈ Point(l))`

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

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

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

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

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

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

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

Lemma: lattice-meet-eq-1
`∀[l:BoundedLattice]. ∀[x,y:Point(l)].  uiff(x ∧ y = 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).  f a ∧ b ≤ f a ∧ f b) ∧ (∀a,b:Point(l1).  f a ∨ f b ≤ f a ∨ b) `
`  supposing ∀x,y:Point(l1).  (x ≤ y `` f x ≤ f 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 ≤ y `` f x ≤ f y))`
`  ∧ (∀a,b:Point(l1).  f a ∧ f b ≤ f a ∧ b)`
`  ∧ (∀a,b:Point(l1).  f a ∨ b ≤ f a ∨ f 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 ≤ y `` f x ≤ f y))`
`            ∧ (∀a,b:Point(l1).  f a ∧ f b ≤ f a ∧ b)`
`            ∧ (∀a,b:Point(l1).  f a ∨ b ≤ f a ∨ f b))`
`  ∧ ((f 0) = 0 ∈ Point(l2))`
`  ∧ ((f 1) = 1 ∈ Point(l2))`

Comment: free distributive lattices using quotient doc
`In order to construct a free distributive lattice on any type X 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) ∈ X 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=λ2x y.free-dl-meet(x;y);join=λ2x y.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)].`
`      f = 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 a and list item xs):`
`      a ∨ accumulate (with value b and list item x):`
`           b ∧ f 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 ∨ y = 1 ∈ Point(free-dl(X)) `⇐⇒` (x = 1 ∈ Point(free-dl(X))) ∨ (y = 1 ∈ Point(free-dl(X))))`

Definition: lattice-less
`a < b ==  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 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 a 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 ∈ s `` x ≤ u)) `` \/(s) ≤ u)))`

Lemma: lattice-fset-join-le
`∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s:fset(Point(l))]. ∀[x:Point(l)].`
`  (\/(s) ≤ x `⇐⇒` ∀p:Point(l). (p ∈ s `` 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) ≤ x supposing x ∈ s)`
`  ∧ (∀[s:fset(Point(l))]. ∀[v:Point(l)].  ((∀x:Point(l). (x ∈ s `` 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 ∈ s `` (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) = f a ∨ f b ∈ Point(l2))`

Lemma: lattice-hom-meet
`∀[l1,l2:BoundedLattice]. ∀[f:Hom(l1;l2)]. ∀[a,b:Point(l1)].  ((f a ∧ b) = f a ∧ f 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)].  f x ≤ f y 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 ∧ b ~ fset-ac-glb(eq;a;b))`

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

Lemma: free-dl-le
`∀[T:Type]. ∀eq:EqDecider(T). ∀x,y:Point(free-dist-lattice(T; eq)).  (x ≤ y `⇐⇒` 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 ∨ y = 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 o (λ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)].`
`  g = 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 o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L)))`
`  `` (f = (h o (λ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=λ2a b.a ∨ b;join=λ2a b.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 ∧ b ~ a ∨ b)`

Lemma: opposite-lattice-join
`∀[L,a,b:Top].  (a ∨ b ~ 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)| P 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 ∈ s `` 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 ⊆ x `` (↑(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 ∈ s | 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])) ⊆r Point(free-dist-lattice(T; eq)))`

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

Lemma: free-dlwc-join
`∀[T,eq,a,b,cs:Top].  (a ∨ b ~ 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 ≤ y `⇐⇒` 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) c {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 ∨ y = 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 o (λ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 x of inl(a) => {{inl a,inr a }} | inr(a) => {{inl a,inr a }}`

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 x }}`

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 x ))`

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 x = 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 ≤ y `⇐⇒` 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 ≤ y `⇐⇒` ∀s:fset(T + T). (s ∈ x `` (↓∃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 ⊆ y `` 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 ∈ z `` ((↓∃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} T eq L 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 x = 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)].`
`    g = h ∈ Hom(face-lattice(T;eq);L) `
`    supposing (∀x:T. (g (x=0) ∧ g (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 ∨ y = 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 x = 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 x = 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) x 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 i )`

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 z of inl(a) => {{inr a }} | 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 ⊆r 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 ∨ c = a ∧ b ∨ a ∧ c ∈ Point(dma)))`
`   ∧ DeMorgan-algebra-axioms(dma)} `

Lemma: DeMorgan-algebra_wf
`DeMorganAlgebra ∈ 𝕌'`

Lemma: DeMorgan-algebra-subtype
`DeMorganAlgebra ⊆r 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) = n x ∨ n y ∈ Point(L))) ∨ (∀x,y:Point(L).  ((n x ∨ y) = n x ∧ n 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 o 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)) ⊆r 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} T 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 x = 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)].`
`      g = 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) o 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: general-bounded-lattice-structure
`A generalized bounded lattice structure includes`
`all the components of a bounded lattice, and, in addition, `
`a relation E on the points of the lattice.`

`When we define a generalized bounded lattice, E 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 ⊆r BoundedLatticeStructure`

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

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

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

`For example the (constructive) real numbers in a closed interval`
`form a generalized bounded lattice where E is ⌜x = 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 x 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 x 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: 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 X of generators,`
`we can start with the free distributive lattice ⌜free-dl(X + X)⌝ on generators`
`X + X.  We call generator inl x (x=0) and inr x is (x=1).`
`Then we form a quotient of that lattice so that (x=0) ∧ (x=1) = 0 ∈ Point(free-dl(X + X)).`
`⋅`

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

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

Definition: flattice-order
`flattice-order(X;as;bs) ==  (∀b∈bs.(∃x∈b. (∃y∈b. y = 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)`

Definition: distributive-lattice-cat
`BddDistributiveLattice ==`
`  Cat(ob = BoundedDistributiveLattice;`
`      arrow(G,H) = Hom(G;H);`
`      id(G) = λx.x;`
`      comp(G,H,K,f,g) = g o f)`

Lemma: distributive-lattice-cat_wf
`BddDistributiveLattice ∈ SmallCategory'`

Definition: free-dl-functor
`FreeDistLattice ==  functor(ob(X) = free-dl(X);arrow(X,Y,f) = fdl-hom(free-dl(Y);λx.free-dl-generator(f x)))`

Lemma: free-dl-functor_wf
`FreeDistLattice ∈ Functor(TypeCat;BddDistributiveLattice)`

Definition: forget-lattice
`ForgetLattice ==  functor(ob(ltt) = Point(ltt);arrow(G,H,f) = f)`

Lemma: forget-lattice_wf
`ForgetLattice ∈ Functor(BddDistributiveLattice;TypeCat)`

`FreeDistLattice -| ForgetLattice`