---

Step * of Lemma csm-comp_wf

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

---

Latex:

---

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


By

---

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

---

Home Index