---

Step * 2 3 of Lemma free-group-functor_wf


1. X : Type@i'
2. Y : Type@i'
3. z : Type@i'
4. f : X ⟶ Y@i'
5. g : Y ⟶ z@i'
6. x : X@i
⊢ (fg-lift(free-group(z);λx@0.free-letter(g (f x@0))) free-letter(x))
= ((fg-lift(free-group(z);λx.free-letter(g x)) o fg-lift(free-group(Y);λx.free-letter(f x))) free-letter(x))
∈ |free-group(z)|
BY
{ (RepUR ``free-letter fg-lift fg-hom free-word-inv free-0 free-append`` 0 THEN Fold `free-letter` 0) }

1
1. X : Type@i'
2. Y : Type@i'
3. z : Type@i'
4. f : X ⟶ Y@i'
5. g : Y ⟶ z@i'
6. x : X@i
⊢ free-letter(g (f x)) = free-letter(g (f x)) ∈ free-word(z)

---

Latex:

---

Latex:

1.  X  :  Type@i'
2.  Y  :  Type@i'
3.  z  :  Type@i'
4.  f  :  X  {}\mrightarrow{}  Y@i'
5.  g  :  Y  {}\mrightarrow{}  z@i'
6.  x  :  X@i
\mvdash{}  (fg-lift(free-group(z);\mlambda{}x@0.free-letter(g  (f  x@0)))  free-letter(x))
=  ((fg-lift(free-group(z);\mlambda{}x.free-letter(g  x))  o  fg-lift(free-group(Y);\mlambda{}x.free-letter(f  x))) 
      free-letter(x))


By

---

Latex:
(RepUR  ``free-letter  fg-lift  fg-hom  free-word-inv  free-0  free-append``  0  THEN  Fold  `free-letter`  0)

---

Home Index