---

Step * 3 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)))
⊢ counit-unit-equations(<Type, λI,J. (I ⟶ J), λI,x. x, λI,J,K,f,g. (g o f)>;<BoundedDistributiveLattice
                                   , λG,H. Hom(G;H)
                                   , λG,x. x
                                   , λG,H,K,f,g. (g
                                                 o f)>;functor(ob(X) = free-dl(X);
                  arrow(X,Y,f) =
                   fdl-hom(free-dl(Y);λx.free-dl-generator(f 
                                                           x)));functor(ob(ltt) = Point(ltt);
                                                                        arrow(G,H,f) =
                                                                         f);λG.fdl-hom(G;λg.g);λX,x. ...)
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. 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))

2
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))

---

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)))
\mvdash{}  counit-unit-equations(<Type,  \mlambda{}I,J.  (I  {}\mrightarrow{}  J),  \mlambda{}I,x.  x,  \mlambda{}I,J,K,f,g.  (g  o  f)><BoundedDistributiveLat\000Ctice
                                                                      ,  \mlambda{}G,H.  Hom(G;H)
                                                                      ,  \mlambda{}G,x.  x
                                                                      ,  \mlambda{}G,H,K,f,g.  (g
                                                                                                  o  f)>functor(ob(X)  =  free-dl(X);
                                    arrow(X,Y,f)  =
                                      fdl-hom(free-dl(Y);\mlambda{}x.free-dl-generator(f 
                                                                                                                      x)));functor(ob(ltt)  =  Point(ltt);
                                                                                                                                                arrow(G,H,f)  =
                                                                                                                                                  f);\mlambda{}G.fdl-hom(G;\mlambda{}g.g);...)


By

---

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

---

Home Index