Nuprl Lemma : context-subset-type-subtype

āˆ€[G:jāŠ¢]. āˆ€[phi:{G āŠ¢ _:š”½}].  ({G āŠ¢_} āŠ†{G, phi āŠ¢_})


Proof




Definitions occuring in Statement :  context-subset: Gamma, phi face-type: š”½ cubical-term: {X āŠ¢ _:A} cubical-type: {X āŠ¢ _} cubical_set: CubicalSet subtype_rel: A āŠ†B uall: āˆ€[x:A]. B[x]
Definitions unfolded in proof :  uall: āˆ€[x:A]. B[x] subtype_rel: A āŠ†B member: t āˆˆ T cubical-type: {X āŠ¢ _} and: P āˆ§ Q all: āˆ€x:A. B[x] uimplies: supposing a squash: ā†“T prop: ā„™ true: True guard: {T} iff: ā‡ā‡’ Q rev_implies: ā‡ Q implies: ā‡’ Q so_lambda: Ī»2x.t[x] so_apply: x[s] cube-set-restriction: f(s) pi2: snd(t) context-subset: Gamma, phi
Lemmas referenced :  fset_wf nat_wf I_cube_wf context-subset_wf nh-id_wf subtype_rel-equal cube-set-restriction_wf equal_wf squash_wf true_wf istype-universe cube-set-restriction-id subtype_rel_self iff_weakening_equal names-hom_wf nh-comp_wf cube-set-restriction-comp cubical-type_wf cubical-term_wf face-type_wf cubical_set_wf subtype_rel_dep_function subset-I_cube context-subset-is-subset context-subset-restriction
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaEquality_alt rename sqequalHypSubstitution setElimination thin cut productElimination dependent_set_memberEquality_alt sqequalRule productIsType functionIsType universeIsType introduction extract_by_obid isectElimination hypothesis hypothesisEquality applyEquality equalityIstype because_Cache instantiate independent_isectElimination imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed independent_functionElimination dependent_functionElimination dependent_pairEquality_alt functionExtensionality lambdaFormation_alt cumulativity functionEquality inhabitedIsType Error :memTop,  independent_pairFormation promote_hyp

Latex:
\mforall{}[G:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].    (\{G  \mvdash{}j  \_\}  \msubseteq{}r  \{G,  phi  \mvdash{}j  \_\})



Date html generated: 2020_05_20-PM-02_57_53
Last ObjectModification: 2020_04_04-PM-05_13_00

Theory : cubical!type!theory


Home Index