Nuprl Lemma : pscm-id-sq

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

Proof

Error : references

Latex:
\mforall{}[C:SmallCategory]. \mforall{}[X:ps\_context\{j:l\}(C)]. (1(X) \msim{} identity-trans(op-cat(C);type-cat\{j':l\};X)) Date html generated: 2020_05_21-AM-10_29_41 Last ObjectModification: 2020_04_01-AM-09_42_10 Theory : presheaf!models!of!type!theory Home Index