---

Step * 2 of Lemma free-group-adjunction


1. ∀d:Type
     ((fg-lift(free-group(d);λg.g) o fg-lift(free-group(free-word(d));λx.free-letter(free-letter(x))))
     = (λx.x)
     ∈ MonHom(free-group(d),free-group(d)))
2. c : Group{i}
⊢ (fg-lift(c;λg.g) o (λx.free-letter(x))) = (λx.x) ∈ (|c| ⟶ |c|)
BY
{ (FunExt THEN RepUR ``fg-lift fg-hom free-letter`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}d:Type
          ((fg-lift(free-group(d);\mlambda{}g.g)
            o  fg-lift(free-group(free-word(d));\mlambda{}x.free-letter(free-letter(x))))
          =  (\mlambda{}x.x))
2.  c  :  Group\{i\}
\mvdash{}  (fg-lift(c;\mlambda{}g.g)  o  (\mlambda{}x.free-letter(x)))  =  (\mlambda{}x.x)


By

---

Latex:
(FunExt  THEN  RepUR  ``fg-lift  fg-hom  free-letter``  0  THEN  Auto)

---

Home Index