---

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: real-interval-lattice
real-interval-lattice(I) ==  mk-distributive-lattice({r:ℝ| r ∈ I} ; λ2x y.rmin(x;y); λ2x y.rmax(x;y))

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

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: real-closed-interval-lattice
For real numbers ⌜a ≤ b⌝, the reals in the closed interval ⌜[a, b]⌝
form a distributive lattice with meet ⌜rmin(x;y)⌝ and join ⌜rmax(x;y)⌝.
But they do not form a bounded distributive lattice with 0 = a and 1 = 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 ⌜x = y⌝).

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

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



Home Index