---

Step * 3 1 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))
BY
{ ((BLemma `free-dl-generators` THEN Auto)
   THEN Try ((BLemma `id-is-bounded-lattice-hom` THEN Auto))
   THEN Repeat (Try ((BLemma `compose-bounded-lattice-hom` 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. d : Type
4. x : d
⊢ ((fdl-hom(free-dl(d);λg.g) o fdl-hom(free-dl(Point(free-dl(d)));λx.free-dl-generator(free-dl-generator(x)))) 
   free-dl-generator(x))
= ((λx.x) free-dl-generator(x))
∈ Point(free-dl(d))

---

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.  d  :  Type
\mvdash{}  (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)


By

---

Latex:
((BLemma  `free-dl-generators`  THEN  Auto)
  THEN  Try  ((BLemma  `id-is-bounded-lattice-hom`  THEN  Auto))
  THEN  Repeat  (Try  ((BLemma  `compose-bounded-lattice-hom`  THEN  Auto))))

---

Home Index