---

Step * of Lemma free-dist-lattice-adjunction

FreeDistLattice -| ForgetLattice
BY
{ (((Assert ∀Y:Type. (Point(free-dl(Y)) ~ free-dl-type(Y)) BY
           (Intro THEN RW (SubC (TagC (mk_tag_term 100))) 0 THEN Auto))
    THEN (Assert ∀Y:Type. ∀y:Y.  (free-dl-generator(y) ∈ Point(free-dl(Y))) BY
                (ParallelOp 1 THEN RWO  "-1" 0 THEN Auto))
    )
   THEN (UseWitness ⌜mk-adjunction(G.fdl-hom(G;λg.g);X.λx.free-dl-generator(x))⌝⋅ THEN MemCD)
   THEN Try (QuickAuto)
   THEN (RepUR ``distributive-lattice-cat type-cat free-dl-functor`` 0 THEN RepUR ``forget-lattice mk-cat`` 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

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. G : cat-ob(BddDistributiveLattice)
⊢ G ∈ LatticeStructure

3
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. ...)

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

5
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. a1 : Type
4. a2 : Type
5. g : a1 ⟶ a2
⊢ (fdl-hom(free-dl(a2);λx.free-dl-generator(g x)) o (λx.free-dl-generator(x)))
= ((λx.free-dl-generator(x)) o g)
∈ (a1 ⟶ Point(free-dl(a2)))

---

Latex:

---

Latex:
FreeDistLattice  -|  ForgetLattice


By

---

Latex:
(((Assert  \mforall{}Y:Type.  (Point(free-dl(Y))  \msim{}  free-dl-type(Y))  BY
                  (Intro  THEN  RW  (SubC  (TagC  (mk\_tag\_term  100)))  0  THEN  Auto))
    THEN  (Assert  \mforall{}Y:Type.  \mforall{}y:Y.    (free-dl-generator(y)  \mmember{}  Point(free-dl(Y)))  BY
                            (ParallelOp  1  THEN  RWO    "-1"  0  THEN  Auto))
    )
  THEN  (UseWitness  \mkleeneopen{}mk-adjunction(G.fdl-hom(G;\mlambda{}g.g);X.\mlambda{}x.free-dl-generator(x))\mkleeneclose{}\mcdot{}  THEN  MemCD)
  THEN  Try  (QuickAuto)
  THEN  (RepUR  ``distributive-lattice-cat  type-cat  free-dl-functor``  0
              THEN  RepUR  ``forget-lattice  mk-cat``  0
              )
  THEN  Auto)

---

Home Index