---

Step * 2 1 of Lemma free-group-functor_wf

.....wf..... 
1. X : Type
2. Y : Type
3. z : Type
4. f : X ⟶ Y
5. g : Y ⟶ z
⊢ fg-lift(free-group(z);λx@0.free-letter(g (f x@0))) ∈ MonHom(free-group(X),free-group(z))
BY
{ (GenConcl ⌜(λx.free-letter(g (f x))) = h ∈ (X ⟶ |free-group(z)|)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  X  :  Type
2.  Y  :  Type
3.  z  :  Type
4.  f  :  X  {}\mrightarrow{}  Y
5.  g  :  Y  {}\mrightarrow{}  z
\mvdash{}  fg-lift(free-group(z);\mlambda{}x@0.free-letter(g  (f  x@0)))  \mmember{}  MonHom(free-group(X),free-group(z))


By

---

Latex:
(GenConcl  \mkleeneopen{}(\mlambda{}x.free-letter(g  (f  x)))  =  h\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index