---

Step * of Lemma free-group-adjunction

FreeGp -| ForgetGroup
BY
{ ((UseWitness ⌜mk-adjunction(G.fg-lift(G;λg.g);X.λx.free-letter(x))⌝⋅ THEN MemCD)
   THEN Try (QuickAuto)
   THEN RepUR ``group-cat type-cat free-group-functor forget-group mk-cat`` 0
   THEN RepUR ``counit-unit-equations`` 0
   THEN Auto) }

1
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
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|)

3
1. b1 : Group{i}
2. b2 : Group{i}
3. g : MonHom(b1,b2)
⊢ (g o fg-lift(b1;λg.g))
= (fg-lift(b2;λg.g) o fg-lift(free-group(|b2|);λx.free-letter(g x)))
∈ MonHom(free-group(|b1|),b2)

---

Latex:

---

Latex:
FreeGp  -|  ForgetGroup


By

---

Latex:
((UseWitness  \mkleeneopen{}mk-adjunction(G.fg-lift(G;\mlambda{}g.g);X.\mlambda{}x.free-letter(x))\mkleeneclose{}\mcdot{}  THEN  MemCD)
  THEN  Try  (QuickAuto)
  THEN  RepUR  ``group-cat  type-cat  free-group-functor  forget-group  mk-cat``  0
  THEN  RepUR  ``counit-unit-equations``  0
  THEN  Auto)

---

Home Index