---

Step * 3 1 of Lemma free-group-adjunction


1. b1 : Group{i}
2. b2 : Group{i}
3. g : MonHom(b1,b2)
⊢ fg-lift(free-group(|b2|);λx.free-letter(g x)) ∈ MonHom(free-group(|b1|),free-group(|b2|))
BY
{ (InstLemma `fg-lift_wf` [⌜|b1|⌝;⌜free-group(|b2|)⌝;⌜λx.free-letter(g x)⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  b1  :  Group\{i\}
2.  b2  :  Group\{i\}
3.  g  :  MonHom(b1,b2)
\mvdash{}  fg-lift(free-group(|b2|);\mlambda{}x.free-letter(g  x))  \mmember{}  MonHom(free-group(|b1|),free-group(|b2|))


By

---

Latex:
(InstLemma  `fg-lift\_wf`  [\mkleeneopen{}|b1|\mkleeneclose{};\mkleeneopen{}free-group(|b2|)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.free-letter(g  x)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index