---

Step * of Lemma free-group-functor_wf

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

1
1. X : Type@i'
2. Y : Type@i'
3. f : X ⟶ Y@i'
⊢ fg-lift(free-group(Y);λx.free-letter(f x)) ∈ MonHom(free-group(X),free-group(Y))

2
1. X : Type@i'
2. Y : Type@i'
3. z : Type@i'
4. f : X ⟶ Y@i'
5. g : Y ⟶ z@i'
⊢ 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@i'
⊢ fg-lift(free-group(X);λx@0.free-letter(x@0)) = (λx.x) ∈ MonHom(free-group(X),free-group(X))

---

Latex:

---

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


By

---

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

---

Home Index