Nuprl Lemma : cubical-universe_wf

āˆ€[X:jāŠ¢]. X āŠ¢cš•Œ


Proof




Definitions occuring in Statement :  cubical-universe: cš•Œ cubical-type: {X āŠ¢ _} cubical_set: CubicalSet uall: āˆ€[x:A]. B[x] member: t āˆˆ T
Definitions unfolded in proof :  uall: āˆ€[x:A]. B[x] member: t āˆˆ T cubical-universe: cš•Œ
Lemmas referenced :  closed-type-to-type_wf closed-cubical-universe_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule thin instantiate extract_by_obid sqequalHypSubstitution isectElimination hypothesis hypothesisEquality axiomEquality equalityTransitivity equalitySymmetry universeIsType

Latex:
\mforall{}[X:j\mvdash{}].  X  \mvdash{}'  c\mBbbU{}



Date html generated: 2020_05_20-PM-07_06_30
Last ObjectModification: 2020_04_25-PM-00_20_54

Theory : cubical!type!theory


Home Index