Nuprl Lemma : equiv_path-1

[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}].  G ⊢ (equiv_path(G;A;B;f))[1(𝕀)]=B:c𝕌


Proof




Definitions occuring in Statement :  equiv_path: equiv_path(G;A;B;f) universe-decode: decode(t) cubical-universe: c𝕌 cubical-equiv: Equiv(T;A) same-cubical-term: X ⊢ u=v:A interval-1: 1(𝕀) csm-id-adjoin: [u] csm-ap-term: (t)s cubical-term: {X ⊢ _:A} cubical_set: CubicalSet uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] same-cubical-term: X ⊢ u=v:A equiv_path: equiv_path(G;A;B;f) member: t ∈ T subtype_rel: A ⊆B all: x:A. B[x] implies:  Q let: let prop: squash: T true: True csm-comp-structure: (cA)tau interval-1: 1(𝕀) csm-id-adjoin: [u] interval-type: 𝕀 csm-comp: F csm-id: 1(X) csm-adjoin: (s;u) compose: g csm-ap: (s)x guard: {T} uimplies: supposing a and: P ∧ Q iff: ⇐⇒ Q rev_implies:  Q universe-comp-fun: CompFun(A)
Lemmas referenced :  equiv-path2_wf universe-decode_wf universe-comp-fun_wf cubical_set_cumulativity-i-j comp-fun-to-comp-op_wf cube-context-adjoin_wf interval-type_wf equiv-path1_wf composition-structure-cumulativity csm-universe-encode csm-id-adjoin_wf interval-1_wf same-cubical-term_wf cubical-universe_wf cubical-type-cumulativity2 istype-cubical-term cubical-equiv_wf istype-cubical-universe-term cubical_set_wf universe-encode-decode squash_wf true_wf cubical-type_wf universe-encode_wf composition-op_wf equiv-path1-1 subtype_rel_self composition-structure_wf csm-comp-structure_wf csm-id-adjoin_wf-interval-1 equiv-path2-1 csm-comp-fun-to-comp-op equal_wf istype-universe csm-ap-type_wf universe-comp-op_wf subtype_rel-equal iff_weakening_equal comp-op-to-comp-fun-inverse
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality hypothesis instantiate applyEquality sqequalRule equalityTransitivity equalitySymmetry inhabitedIsType lambdaFormation_alt rename dependent_functionElimination hyp_replacement applyLambdaEquality equalityIstype independent_functionElimination universeIsType lambdaEquality_alt imageElimination natural_numberEquality imageMemberEquality baseClosed universeEquality independent_isectElimination dependent_set_memberEquality_alt independent_pairFormation productIsType setElimination productElimination

Latex:
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}].
    G  \mvdash{}  (equiv\_path(G;A;B;f))[1(\mBbbI{})]=B:c\mBbbU{}



Date html generated: 2020_05_20-PM-07_30_15
Last ObjectModification: 2020_04_28-PM-07_05_30

Theory : cubical!type!theory


Home Index