---

Step * 1 of Lemma pscm-id-sq


1. C : SmallCategory
2. X : ps_context{j:l}(C)
⊢ 1(X) ~ identity-trans(op-cat(C);type-cat{j':l};X)
BY
{ (RepUR ``pscm-id identity-trans mk-nat-trans cat-id type-cat`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
\mvdash{}  1(X)  \msim{}  identity-trans(op-cat(C);type-cat\{j':l\};X)


By

---

Latex:
(RepUR  ``pscm-id  identity-trans  mk-nat-trans  cat-id  type-cat``  0  THEN  Auto)

---

Home Index