---

Step * of Lemma csm-comp-assoc

No Annotations
∀[A,B,C,D:j⊢]. ∀[F:A j⟶ B]. ∀[G:B j⟶ C]. ∀[H:C j⟶ D].  (H o G o F = H o G o F ∈ A j⟶ D)
BY
{ PresheafMLTTInstance Obid: pscm-comp-assoc⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B,C,D:j\mvdash{}].  \mforall{}[F:A  j{}\mrightarrow{}  B].  \mforall{}[G:B  j{}\mrightarrow{}  C].  \mforall{}[H:C  j{}\mrightarrow{}  D].    (H  o  G  o  F  =  H  o  G  o  F)


By

---

Latex:
PresheafMLTTInstance  Obid:  pscm-comp-assoc\mcdot{}

---

Home Index