---

Step * of Lemma free-group-functor_wf

FreeGp ∈ Functor(TypeCat;Group)
BY
{ (ProveWfLemma THEN All (RepUR  ``type-cat group-cat mk-cat``) THEN Auto) }

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

2
1. X : Type
2. Y : Type
3. z : Type
4. f : X ⟶ Y
5. g : Y ⟶ z
⊢ fg-lift(free-group(z);λx@0.free-letter(g (f x@0)))
= (fg-lift(free-group(z);λx.free-letter(g x)) o fg-lift(free-group(Y);λx.free-letter(f x)))
∈ MonHom(free-group(X),free-group(z))

3
1. X : Type
⊢ fg-lift(free-group(X);λx@0.free-letter(x@0)) = (λx.x) ∈ MonHom(free-group(X),free-group(X))

---

Latex:

---

Latex:
FreeGp  \mmember{}  Functor(TypeCat;Group)


By

---

Latex:
(ProveWfLemma  THEN  All  (RepUR    ``type-cat  group-cat  mk-cat``)  THEN  Auto)

---

Home Index