---

Step * 1 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))
BY
{ ((BLemma `free-group-generators` THEN Auto) THEN Try ((BLemma `id-is-monoid_hom` THEN Auto))) }

1
1. d : Type
⊢ fg-lift(free-group(free-word(d));λx.free-letter(free-letter(x))) ∈ MonHom(free-group(d),free-group(free-word(d)))

---

Latex:

---

Latex:

1.  d  :  Type
\mvdash{}  (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)


By

---

Latex:
((BLemma  `free-group-generators`  THEN  Auto)  THEN  Try  ((BLemma  `id-is-monoid\_hom`  THEN  Auto)))

---

Home Index