---

Step * 1 of Lemma free-group-functor_wf


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

---

Latex:

---

Latex:

1.  X  :  Type
2.  Y  :  Type
3.  f  :  X  {}\mrightarrow{}  Y
\mvdash{}  fg-lift(free-group(Y);\mlambda{}x.free-letter(f  x))  \mmember{}  MonHom(free-group(X),free-group(Y))


By

---

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

---

Home Index