---

Step * 2 of Lemma free-dist-lattice-adjunction


1. ∀Y:Type. (Point(free-dl(Y)) ~ free-dl-type(Y))
2. ∀Y:Type. ∀y:Y.  (free-dl-generator(y) ∈ Point(free-dl(Y)))
3. G : cat-ob(BddDistributiveLattice)
⊢ G ∈ LatticeStructure
BY
{ (RepUR ``counit-unit-equations`` 0 THEN Auto) }

1
1. ∀Y:Type. (Point(free-dl(Y)) ~ free-dl-type(Y))
2. ∀Y:Type. ∀y:Y.  (free-dl-generator(y) ∈ Point(free-dl(Y)))
3. G : cat-ob(BddDistributiveLattice)
⊢ G ∈ LatticeStructure

---

Latex:

---

Latex:

1.  \mforall{}Y:Type.  (Point(free-dl(Y))  \msim{}  free-dl-type(Y))
2.  \mforall{}Y:Type.  \mforall{}y:Y.    (free-dl-generator(y)  \mmember{}  Point(free-dl(Y)))
3.  G  :  cat-ob(BddDistributiveLattice)
\mvdash{}  G  \mmember{}  LatticeStructure


By

---

Latex:
(RepUR  ``counit-unit-equations``  0  THEN  Auto)

---

Home Index