---

Step * 2 2 of Lemma free-group-functor_wf

.....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))
BY
{ ((GenConcl ⌜(λx.free-letter(f x)) = h ∈ (X ⟶ |free-group(Y)|)⌝⋅ THEN Auto)
   THEN GenConcl ⌜(λx.free-letter(g x)) = h ∈ (Y ⟶ |free-group(z)|)⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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.free-letter(g  x))  o  fg-lift(free-group(Y);\mlambda{}x.free-letter(f  x))
    \mmember{}  MonHom(free-group(X),free-group(z))


By

---

Latex:
((GenConcl  \mkleeneopen{}(\mlambda{}x.free-letter(f  x))  =  h\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  GenConcl  \mkleeneopen{}(\mlambda{}x.free-letter(g  x))  =  h\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index