Nuprl Lemma : constant-cubical-type_wf

[X,Gamma:CubicalSet].  Gamma ⊢ (X)


Proof




Definitions occuring in Statement :  constant-cubical-type: (X) 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-type: {X ⊢ _} constant-cubical-type: (X) subtype_rel: A ⊆B and: P ∧ Q cand: c∧ B all: x:A. B[x] squash: T prop: true: True uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  I-cube_wf list_wf coordinate_name_wf cube-set-restriction_wf name-morph_wf equal_wf squash_wf true_wf cube-set-restriction-id iff_weakening_equal name-comp_wf cube-set-restriction-comp all_wf id-morph_wf subtype_rel-equal cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality dependent_pairEquality lambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis because_Cache sqequalRule applyEquality functionEquality functionExtensionality lambdaFormation imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination independent_pairFormation dependent_functionElimination productEquality instantiate axiomEquality isect_memberEquality

Latex:
\mforall{}[X,Gamma:CubicalSet].    Gamma  \mvdash{}  (X)



Date html generated: 2017_10_05-AM-10_17_24
Last ObjectModification: 2017_07_28-AM-11_20_17

Theory : cubical!sets


Home Index