---

Step * 2 of Lemma free-dl-functor_wf


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. X : Type@i'
4. x : X@i
⊢ (fdl-hom(free-dl(X);λx@0.free-dl-generator(x@0)) free-dl-generator(x))
= ((λx.x) free-dl-generator(x))
∈ Point(free-dl(X))
BY
{ ((Subst' (λx.x) free-dl-generator(x) ~ (λx@0.free-dl-generator(x@0)) x 0 THENA (Reduce 0 THEN Auto))
   THEN BLemma `fdl-hom-agrees`
   THEN Auto) }

---

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.  X  :  Type@i'
4.  x  :  X@i
\mvdash{}  (fdl-hom(free-dl(X);\mlambda{}x@0.free-dl-generator(x@0))  free-dl-generator(x))
=  ((\mlambda{}x.x)  free-dl-generator(x))


By

---

Latex:
((Subst'  (\mlambda{}x.x)  free-dl-generator(x)  \msim{}  (\mlambda{}x@0.free-dl-generator(x@0))  x  0  THENA  (Reduce  0  THEN  Auto))
  THEN  BLemma  `fdl-hom-agrees`
  THEN  Auto)

---

Home Index