Nuprl Lemma : cubical-identity_wf

[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}].  X ⊢ (Id_A b)


Proof




Definitions occuring in Statement :  cubical-identity: (Id_A b) cubical-term: {X ⊢ _:AF} 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 ⊢ _} cubical-identity: (Id_A b) all: x:A. B[x] and: P ∧ Q cand: c∧ B squash: T prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  cubical-path_wf I-cube_wf list_wf coordinate_name_wf I-path-morph_wf2 name-morph_wf cube-set-restriction_wf equal_wf squash_wf true_wf I-path-morph-id iff_weakening_equal I-path-morph-comp all_wf id-morph_wf subtype_rel-equal cube-set-restriction-id name-comp_wf cube-set-restriction-comp cubical-term_wf cubical-type_wf 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 sqequalRule dependent_functionElimination because_Cache functionEquality applyEquality functionExtensionality lambdaFormation imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination independent_pairFormation productEquality instantiate axiomEquality isect_memberEquality

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].    X  \mvdash{}  (Id\_A  a  b)



Date html generated: 2017_10_05-PM-03_56_05
Last ObjectModification: 2017_07_28-AM-11_28_35

Theory : cubical!sets


Home Index