Nuprl Lemma : discrete-cubical-term_wf

[T:Type]. ∀[t:T]. ∀[X:CubicalSet].  (discr(t) ∈ {X ⊢ _:discr(T)})


Proof




Definitions occuring in Statement :  discrete-cubical-term: discr(t) discrete-cubical-type: discr(T) cubical-term: {X ⊢ _:AF} cubical-set: CubicalSet uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T discrete-cubical-term: discr(t) discrete-cubical-type: discr(T) cubical-term: {X ⊢ _:AF} pi1: fst(t) all: x:A. B[x] so_lambda: λ2x.t[x] subtype_rel: A ⊆B implies:  Q top: Top prop: so_apply: x[s]
Lemmas referenced :  I-cube_wf list_wf coordinate_name_wf name-morph_wf all_wf equal_wf cube-set-restriction_wf top_wf pi1_wf_top cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality sqequalRule lambdaEquality hypothesisEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaFormation because_Cache cumulativity applyEquality functionExtensionality independent_pairEquality isect_memberEquality universeEquality productEquality functionEquality isectEquality instantiate productElimination voidElimination voidEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination axiomEquality

Latex:
\mforall{}[T:Type].  \mforall{}[t:T].  \mforall{}[X:CubicalSet].    (discr(t)  \mmember{}  \{X  \mvdash{}  \_:discr(T)\})



Date html generated: 2017_10_05-AM-10_17_19
Last ObjectModification: 2017_07_28-AM-11_20_15

Theory : cubical!sets


Home Index