Nuprl Lemma : sets_wf
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. (sets(C; X) ∈ small-category{[i | j']:l})
Proof
Error : references
Latex:
\mforall{}[C:SmallCategory]. \mforall{}[X:ps\_context\{j:l\}(C)]. (sets(C; X) \mmember{} small-category\{[i | j']:l\})
Date html generated:
2020_05_21-AM-10_29_37
Last ObjectModification:
2020_04_01-AM-10_44_31
Theory : presheaf!models!of!type!theory
Home
Index