Nuprl Lemma : face-forall-q=0-or-q=1
∀[Gamma:j⊢]. ((Gamma ⊢ ∀ ((q=0) ∨ (q=1))) = 0(𝔽) ∈ {Gamma ⊢ _:𝔽})
Proof
Definitions occuring in Statement : 
face-forall: (∀ phi)
, 
face-zero: (i=0)
, 
face-one: (i=1)
, 
face-or: (a ∨ b)
, 
face-0: 0(𝔽)
, 
face-type: 𝔽
, 
cc-snd: q
, 
cubical-term: {X ⊢ _:A}
, 
cubical_set: CubicalSet
, 
uall: ∀[x:A]. B[x]
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
subtype_rel: A ⊆r B
, 
cc-snd: q
, 
interval-type: 𝕀
, 
cc-fst: p
, 
csm-ap-type: (AF)s
, 
constant-cubical-type: (X)
, 
true: True
, 
squash: ↓T
, 
prop: ℙ
, 
uimplies: b supposing a
, 
guard: {T}
, 
iff: P 
⇐⇒ Q
, 
and: P ∧ Q
, 
rev_implies: P 
⇐ Q
, 
implies: P 
⇒ Q
Lemmas referenced : 
cubical_set_wf, 
face-zero_wf, 
cube-context-adjoin_wf, 
cubical_set_cumulativity-i-j, 
interval-type_wf, 
cc-snd_wf, 
face-one_wf, 
face-0_wf, 
face-or-0, 
equal_wf, 
squash_wf, 
true_wf, 
istype-universe, 
face-forall-or, 
face-or_wf, 
cubical-term_wf, 
face-type_wf, 
face-forall-q=0, 
face-forall-q=1, 
subtype_rel_self, 
iff_weakening_equal
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
hypothesis, 
universeIsType, 
instantiate, 
introduction, 
extract_by_obid, 
because_Cache, 
hypothesisEquality, 
thin, 
sqequalHypSubstitution, 
isectElimination, 
applyEquality, 
sqequalRule, 
equalityTransitivity, 
equalitySymmetry, 
natural_numberEquality, 
lambdaEquality_alt, 
imageElimination, 
universeEquality, 
inhabitedIsType, 
imageMemberEquality, 
baseClosed, 
independent_isectElimination, 
productElimination, 
independent_functionElimination
Latex:
\mforall{}[Gamma:j\mvdash{}].  ((Gamma  \mvdash{}  \mforall{}  ((q=0)  \mvee{}  (q=1)))  =  0(\mBbbF{}))
Date html generated:
2020_05_20-PM-02_50_59
Last ObjectModification:
2020_04_06-AM-10_23_41
Theory : cubical!type!theory
Home
Index