---

Step * 3 1 1 1 1 1 1 of Lemma free-dist-lattice-adjunction

.....subterm..... T:t
3:n
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@i'
4. x : d@i
5. (fdl-hom(free-dl(Point(free-dl(d)));λx.free-dl-generator(free-dl-generator(x))) free-dl-generator(x))
= free-dl-generator(free-dl-generator(x))
∈ Point(free-dl(Point(free-dl(d))))
6. (fdl-hom(free-dl(d);λg.g) 
    (fdl-hom(free-dl(Point(free-dl(d)));λx.free-dl-generator(free-dl-generator(x))) free-dl-generator(x)))
= (fdl-hom(free-dl(d);λg.g) free-dl-generator(free-dl-generator(x)))
∈ Point(free-dl(d))
⊢ free-dl-generator(x) = (fdl-hom(free-dl(d);λg.g) free-dl-generator(free-dl-generator(x))) ∈ Point(free-dl(d))
BY
{ ((InstLemma `fdl-hom-agrees` [⌜Point(free-dl(d))⌝;⌜free-dl(d)⌝;⌜λg.g⌝;⌜free-dl-generator(x)⌝]⋅ THENA Auto)
   THEN Reduce -1
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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@i'
4.  x  :  d@i
5.  (fdl-hom(free-dl(Point(free-dl(d)));\mlambda{}x.free-dl-generator(free-dl-generator(x))) 
        free-dl-generator(x))
=  free-dl-generator(free-dl-generator(x))
6.  (fdl-hom(free-dl(d);\mlambda{}g.g) 
        (fdl-hom(free-dl(Point(free-dl(d)));\mlambda{}x.free-dl-generator(free-dl-generator(x))) 
          free-dl-generator(x)))
=  (fdl-hom(free-dl(d);\mlambda{}g.g)  free-dl-generator(free-dl-generator(x)))
\mvdash{}  free-dl-generator(x)  =  (fdl-hom(free-dl(d);\mlambda{}g.g)  free-dl-generator(free-dl-generator(x)))


By

---

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

---

Home Index