---

Step * of Lemma comb_for_compose_wf_for_mon_hom

λA,B,C,f,g,z. (g o f) ∈ A:IMonoid ⟶ B:IMonoid ⟶ C:IMonoid ⟶ f:MonHom(A,B) ⟶ g:MonHom(B,C) ⟶ (↓True) ⟶ MonHom(A,C)
BY
{ ProveOpCombTyping `compose_wf_for_mon_hom` }

---

Latex:

---

Latex:
\mlambda{}A,B,C,f,g,z.  (g  o  f)  \mmember{}  A:IMonoid
{}\mrightarrow{}  B:IMonoid
{}\mrightarrow{}  C:IMonoid
{}\mrightarrow{}  f:MonHom(A,B)
{}\mrightarrow{}  g:MonHom(B,C)
{}\mrightarrow{}  (\mdownarrow{}True)
{}\mrightarrow{}  MonHom(A,C)


By

---

Latex:
ProveOpCombTyping  `compose\_wf\_for\_mon\_hom`

---

Home Index