---

Step * of Lemma csm-id-comp

No Annotations
∀[A,B:j⊢]. ∀[sigma:A j⟶ B].  ((sigma o 1(A) = sigma ∈ A j⟶ B) ∧ (1(B) o sigma = sigma ∈ A j⟶ B))
BY
{ PresheafMLTTInstance Obid: pscm-id-comp⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:j\mvdash{}].  \mforall{}[sigma:A  j{}\mrightarrow{}  B].    ((sigma  o  1(A)  =  sigma)  \mwedge{}  (1(B)  o  sigma  =  sigma))


By

---

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

---

Home Index