---

Step * 2 of Lemma free-group-functor_wf


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))
BY
{ (BLemma `free-group-generators` THEN Auto) }

1
.....wf..... 
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))) ∈ MonHom(free-group(X),free-group(z))

2
.....wf..... 
1. X : Type
2. Y : Type
3. z : Type
4. f : X ⟶ Y
5. g : Y ⟶ z
⊢ 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
2. Y : Type
3. z : Type
4. f : X ⟶ Y
5. g : Y ⟶ z
6. x : X
⊢ (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)|

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `free-group-generators`  THEN  Auto)

---

Home Index