---

Step * 4 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. b1 : BoundedDistributiveLattice
4. b2 : BoundedDistributiveLattice
5. g : Hom(b1;b2)
⊢ (g o fdl-hom(b1;λg.g))
= (fdl-hom(b2;λg.g) o fdl-hom(free-dl(Point(b2));λx.free-dl-generator(g x)))
∈ Hom(free-dl(Point(b1));b2)
BY
{ ((BLemma `free-dl-generators` 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. b1 : BoundedDistributiveLattice
4. b2 : BoundedDistributiveLattice
5. g : Hom(b1;b2)
6. x : Point(b1)
⊢ ((g o fdl-hom(b1;λg.g)) free-dl-generator(x))
= ((fdl-hom(b2;λg.g) o fdl-hom(free-dl(Point(b2));λx.free-dl-generator(g x))) free-dl-generator(x))
∈ Point(b2)

---

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.  b1  :  BoundedDistributiveLattice
4.  b2  :  BoundedDistributiveLattice
5.  g  :  Hom(b1;b2)
\mvdash{}  (g  o  fdl-hom(b1;\mlambda{}g.g))
=  (fdl-hom(b2;\mlambda{}g.g)  o  fdl-hom(free-dl(Point(b2));\mlambda{}x.free-dl-generator(g  x)))


By

---

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

---

Home Index