---

Step * of Lemma csm-id-sq

No Annotations
∀[X:j⊢]. (1(X) ~ identity-trans(op-cat(CubeCat);type-cat{j':l};X))
BY
{ PresheafMLTTInstance Obid: pscm-id-sq⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  (1(X)  \msim{}  identity-trans(op-cat(CubeCat);type-cat\{j':l\};X))


By

---

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

---

Home Index