---

Step * 1 1 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. Y : Type@i'
5. z : Type@i'
6. f : X ⟶ Y@i'
7. g : Y ⟶ z@i'
8. x : X@i
⊢ (fdl-hom(free-dl(z);λx@0.free-dl-generator(g (f x@0))) free-dl-generator(x))
= (fdl-hom(free-dl(z);λx.free-dl-generator(g x)) (fdl-hom(free-dl(Y);λx.free-dl-generator(f x)) free-dl-generator(x)))
∈ Point(free-dl(z))
BY
{ ((InstLemma `fdl-hom-agrees` [⌜X⌝;⌜free-dl(Y)⌝;⌜λx.free-dl-generator(f x)⌝;⌜x⌝]⋅ THENA Auto) THEN Reduce -1) }

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. X : Type@i'
4. Y : Type@i'
5. z : Type@i'
6. f : X ⟶ Y@i'
7. g : Y ⟶ z@i'
8. x : X@i
9. (fdl-hom(free-dl(Y);λx.free-dl-generator(f x)) free-dl-generator(x)) = free-dl-generator(f x) ∈ Point(free-dl(Y))
⊢ (fdl-hom(free-dl(z);λx@0.free-dl-generator(g (f x@0))) free-dl-generator(x))
= (fdl-hom(free-dl(z);λx.free-dl-generator(g x)) (fdl-hom(free-dl(Y);λx.free-dl-generator(f x)) free-dl-generator(x)))
∈ Point(free-dl(z))

---

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.  Y  :  Type@i'
5.  z  :  Type@i'
6.  f  :  X  {}\mrightarrow{}  Y@i'
7.  g  :  Y  {}\mrightarrow{}  z@i'
8.  x  :  X@i
\mvdash{}  (fdl-hom(free-dl(z);\mlambda{}x@0.free-dl-generator(g  (f  x@0)))  free-dl-generator(x))
=  (fdl-hom(free-dl(z);\mlambda{}x.free-dl-generator(g  x)) 
      (fdl-hom(free-dl(Y);\mlambda{}x.free-dl-generator(f  x))  free-dl-generator(x)))


By

---

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

---

Home Index