---

Step * 4 1 1 1 1 1 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. b1 : BoundedDistributiveLattice@i'
4. b2 : BoundedDistributiveLattice@i'
5. g : Hom(b1;b2)@i
6. x : Point(b1)@i
7. (fdl-hom(free-dl(Point(b2));λx.free-dl-generator(g x)) free-dl-generator(x))
= free-dl-generator(g x)
∈ Point(free-dl(Point(b2)))
8. (fdl-hom(b2;λg.g) (fdl-hom(free-dl(Point(b2));λx.free-dl-generator(g x)) free-dl-generator(x)))
= (fdl-hom(b2;λg.g) free-dl-generator(g x))
∈ Point(b2)
9. free-dl-generator(x) ∈ Point(free-dl(Point(b1)))
⊢ (g (fdl-hom(b1;λg.g) free-dl-generator(x))) = (fdl-hom(b2;λg.g) free-dl-generator(g x)) ∈ Point(b2)
BY
{ skip{((InstLemma `fdl-hom-agrees` [⌜Point(free-dl(Point(b1)))⌝;⌜free-dl(Point(b1))⌝;⌜λg.g⌝;⌜free-dl-generator(x)⌝]⋅
         THENA Auto
         )
        THEN (InstLemma `fdl-hom-agrees` [%⌜Point(free-dl(Point(b1)))⌝;⌜free-dl(Point(b1))⌝;⌜λg.g⌝;
              ⌜free-dl-generator(x)⌝%]⋅
              THENA 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@i'
4. b2 : BoundedDistributiveLattice@i'
5. g : Hom(b1;b2)@i
6. x : Point(b1)@i
7. (fdl-hom(free-dl(Point(b2));λx.free-dl-generator(g x)) free-dl-generator(x))
= free-dl-generator(g x)
∈ Point(free-dl(Point(b2)))
8. (fdl-hom(b2;λg.g) (fdl-hom(free-dl(Point(b2));λx.free-dl-generator(g x)) free-dl-generator(x)))
= (fdl-hom(b2;λg.g) free-dl-generator(g x))
∈ Point(b2)
9. free-dl-generator(x) ∈ Point(free-dl(Point(b1)))
⊢ (g (fdl-hom(b1;λg.g) free-dl-generator(x))) = (fdl-hom(b2;λg.g) free-dl-generator(g 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@i'
4.  b2  :  BoundedDistributiveLattice@i'
5.  g  :  Hom(b1;b2)@i
6.  x  :  Point(b1)@i
7.  (fdl-hom(free-dl(Point(b2));\mlambda{}x.free-dl-generator(g  x))  free-dl-generator(x))
=  free-dl-generator(g  x)
8.  (fdl-hom(b2;\mlambda{}g.g)  (fdl-hom(free-dl(Point(b2));\mlambda{}x.free-dl-generator(g  x))  free-dl-generator(x)))
=  (fdl-hom(b2;\mlambda{}g.g)  free-dl-generator(g  x))
9.  free-dl-generator(x)  \mmember{}  Point(free-dl(Point(b1)))
\mvdash{}  (g  (fdl-hom(b1;\mlambda{}g.g)  free-dl-generator(x)))  =  (fdl-hom(b2;\mlambda{}g.g)  free-dl-generator(g  x))


By

---

Latex:
skip\{((InstLemma  `fdl-hom-agrees`  [\mkleeneopen{}Point(free-dl(Point(b1)))\mkleeneclose{};\mkleeneopen{}free-dl(Point(b1))\mkleeneclose{};\mkleeneopen{}\mlambda{}g.g\mkleeneclose{};
              \mkleeneopen{}free-dl-generator(x)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
            THEN  (InstLemma  `fdl-hom-agrees`  [\%\mkleeneopen{}Point(free-dl(Point(b1)))\mkleeneclose{};\mkleeneopen{}free-dl(Point(b1))\mkleeneclose{};\mkleeneopen{}\mlambda{}g.g\mkleeneclose{};
                        \mkleeneopen{}free-dl-generator(x)\mkleeneclose{}\%]\mcdot{}
                        THENA  Auto
                        )
            )\}

---

Home Index