---

Step * of Lemma pscm-id-sq

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].  (1(X) ~ identity-trans(op-cat(C);type-cat{j':l};X))
BY
{ Auto }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
⊢ 1(X) ~ identity-trans(op-cat(C);type-cat{j':l};X)

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index