Nuprl Lemma : csm-subtype-iso-instance1

āˆ€[X,H:jāŠ¢]. āˆ€[phi:{H āŠ¢ _:š”½}].  (X jāŸ¶ H.š•€(phi)p āŠ†jāŸ¶ H, phi.š•€)


Proof




Definitions occuring in Statement :  context-subset: Gamma, phi face-type: š”½ interval-type: š•€ cc-fst: p cube-context-adjoin: X.A csm-ap-term: (t)s cubical-term: {X āŠ¢ _:A} cube_set_map: A āŸ¶ B cubical_set: CubicalSet subtype_rel: A āŠ†B uall: āˆ€[x:A]. B[x]
Definitions unfolded in proof :  uall: āˆ€[x:A]. B[x] member: t āˆˆ T uimplies: supposing a
Lemmas referenced :  cube-context-adjoin_wf interval-type_wf context-subset_wf csm-subset-codomain csm-ap-term_wf face-type_wf csm-face-type cc-fst_wf context-adjoin-subset1 cubical-term_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut thin instantiate introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule Error :memTop,  equalityTransitivity equalitySymmetry independent_isectElimination universeIsType inhabitedIsType

Latex:
\mforall{}[X,H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].    (X  j{}\mrightarrow{}  H.\mBbbI{},  (phi)p  \msubseteq{}r  X  j{}\mrightarrow{}  H,  phi.\mBbbI{})



Date html generated: 2020_05_20-PM-03_05_52
Last ObjectModification: 2020_04_06-PM-07_34_51

Theory : cubical!type!theory


Home Index