Nuprl Lemma : presheaf-unit_wf

[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].  (1 ∈ X ⊢ )


Proof




Definitions occuring in Statement :  presheaf-unit: 1 presheaf-type: {X ⊢ _} ps_context: __⊢ uall: [x:A]. B[x] member: t ∈ T small-category: SmallCategory
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T presheaf-unit: 1 subtype_rel: A ⊆B
Lemmas referenced :  discrete-presheaf-type_wf unit_wf2 ps_context_wf small-category-cumulativity-2 small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry universeIsType instantiate applyEquality isect_memberEquality_alt isectIsTypeImplies inhabitedIsType

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].    (1  \mmember{}  X  \mvdash{}  )



Date html generated: 2020_05_20-PM-01_34_40
Last ObjectModification: 2020_04_02-PM-06_33_46

Theory : presheaf!models!of!type!theory


Home Index