---

Step * 3 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. ∀d:Type
     ((fdl-hom(free-dl(d);λg.g) o fdl-hom(free-dl(Point(free-dl(d)));λx.free-dl-generator(free-dl-generator(x))))
     = (λx.x)
     ∈ Hom(free-dl(d);free-dl(d)))
4. c : BoundedDistributiveLattice
⊢ (fdl-hom(c;λg.g) o (λx.free-dl-generator(x))) = (λx.x) ∈ (Point(c) ⟶ Point(c))
BY
{ (FunExt THEN RepUR ``fdl-hom free-dl-generator`` 0 THEN Auto) }

---

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.  \mforall{}d:Type
          ((fdl-hom(free-dl(d);\mlambda{}g.g)
            o  fdl-hom(free-dl(Point(free-dl(d)));\mlambda{}x.free-dl-generator(free-dl-generator(x))))
          =  (\mlambda{}x.x))
4.  c  :  BoundedDistributiveLattice
\mvdash{}  (fdl-hom(c;\mlambda{}g.g)  o  (\mlambda{}x.free-dl-generator(x)))  =  (\mlambda{}x.x)


By

---

Latex:
(FunExt  THEN  RepUR  ``fdl-hom  free-dl-generator``  0  THEN  Auto)

---

Home Index