Nuprl Lemma : cubical-bool_wf
Bool ∈ {() ⊢ _:c𝕌}
Proof
Definitions occuring in Statement :
cubical-bool: Bool,
cubical-universe: c𝕌,
cubical-term: {X ⊢ _:A},
trivial-cube-set: (),
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
cubical-bool: Bool
Lemmas referenced :
discrete-comp_wf,
bool_wf,
discrete-cubical-type_wf,
trivial-cube-set_wf,
universe-encode_wf
Rules used in proof :
hypothesis,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution
Latex:
Bool \mmember{} \{() \mvdash{} \_:c\mBbbU{}\}
Date html generated:
2017_02_21-AM-11_04_07
Last ObjectModification:
2017_02_13-PM-04_49_39
Theory : cubical!type!theory
Home
Index