Nuprl Lemma : face-zero-and-one

āˆ€[X:jāŠ¢]. āˆ€[z:{X āŠ¢ _:š•€}].  (((z=0) āˆ§ (z=1)) 0(š”½) āˆˆ {X āŠ¢ _:š”½})


Proof




Definitions occuring in Statement :  face-zero: (i=0) face-one: (i=1) face-and: (a āˆ§ b) face-0: 0(š”½) face-type: š”½ interval-type: š•€ cubical-term: {X āŠ¢ _:A} cubical_set: CubicalSet uall: āˆ€[x:A]. B[x] equal: t āˆˆ T
Definitions unfolded in proof :  uall: āˆ€[x:A]. B[x] member: t āˆˆ T squash: ā†“T true: True subtype_rel: A āŠ†B uimplies: supposing a guard: {T} iff: ā‡ā‡’ Q and: P āˆ§ Q rev_implies: ā‡ Q implies: ā‡’ Q
Lemmas referenced :  equal_wf cubical-term_wf face-type_wf face-and-com face-zero_wf face-one_wf face-0_wf iff_weakening_equal face-one-and-zero interval-type_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut applyEquality thin instantiate lambdaEquality_alt sqequalHypSubstitution imageElimination extract_by_obid isectElimination because_Cache hypothesis hypothesisEquality natural_numberEquality sqequalRule imageMemberEquality baseClosed equalityTransitivity equalitySymmetry independent_isectElimination productElimination independent_functionElimination universeIsType isect_memberEquality_alt axiomEquality isectIsTypeImplies inhabitedIsType

Latex:
\mforall{}[X:j\mvdash{}].  \mforall{}[z:\{X  \mvdash{}  \_:\mBbbI{}\}].    (((z=0)  \mwedge{}  (z=1))  =  0(\mBbbF{}))



Date html generated: 2020_05_20-PM-02_43_24
Last ObjectModification: 2020_04_04-PM-04_57_39

Theory : cubical!type!theory


Home Index