Nuprl Lemma : csm-cubical-id-equiv
∀[G,K:j⊢]. ∀[tau:K j⟶ G]. ∀[A:{G ⊢ _}]. ((IdEquiv(G;A))tau = IdEquiv(K;(A)tau) ∈ {K ⊢ _:Equiv((A)tau;(A)tau)})
Proof
Definitions occuring in Statement :
cubical-id-equiv: IdEquiv(X;T),
cubical-equiv: Equiv(T;A),
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
cubical-type: {X ⊢ _},
cube_set_map: A ⟶ B,
cubical_set: CubicalSet,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
cubical-term-at: u(a),
cubical-id-equiv: IdEquiv(X;T),
equiv-witness: equiv-witness(f;cntr),
cubical-id-fun: cubical-id-fun(X),
cc-snd: q,
cubical-lam: cubical-lam(X;b),
cubical-lambda: (λb),
cc-adjoin-cube: (v;u),
csm-ap-term: (t)s,
pi2: snd(t),
cubical-equiv: Equiv(T;A),
squash: ↓T,
prop: ℙ,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
true: True,
uimplies: b supposing a,
cubical-type: {X ⊢ _},
csm-ap-type: (AF)s,
csm-id-adjoin: [u],
cc-fst: p,
csm-ap: (s)x,
csm-id: 1(X),
csm-adjoin: (s;u),
pi1: fst(t)
Lemmas referenced :
csm-cubical-pair,
cubical-term-at_wf,
squash_wf,
true_wf,
I_cube_wf,
fset_wf,
nat_wf,
cubical-term_wf,
cubical-type-cumulativity2,
cubical_set_cumulativity-i-j,
cubical-type_wf,
cubical-sigma_wf,
cubical-fun_wf,
csm-ap-type_wf,
is-cubical-equiv_wf,
cube-context-adjoin_wf,
cc-fst_wf,
cc-snd_wf-cubical-fun,
cubical-pair_wf,
csm-id-adjoin_wf,
cubical-id-fun_wf,
cubical-term-equal,
cubical-equiv_wf,
cubical-id-equiv_wf,
cube_set_map_wf,
cubical_set_wf,
csm-is-cubical-equiv,
csm-cubical-id-is-equiv
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
equalitySymmetry,
functionExtensionality,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
Error :memTop,
hypothesis,
applyEquality,
lambdaEquality_alt,
imageElimination,
hypothesisEquality,
equalityTransitivity,
universeIsType,
instantiate,
because_Cache,
dependent_functionElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed,
independent_isectElimination,
isect_memberEquality_alt,
axiomEquality,
isectIsTypeImplies,
inhabitedIsType,
setElimination,
rename,
productElimination,
hyp_replacement
Latex:
\mforall{}[G,K:j\mvdash{}]. \mforall{}[tau:K j{}\mrightarrow{} G]. \mforall{}[A:\{G \mvdash{} \_\}]. ((IdEquiv(G;A))tau = IdEquiv(K;(A)tau))
Date html generated:
2020_05_20-PM-03_34_22
Last ObjectModification:
2020_04_07-PM-05_56_55
Theory : cubical!type!theory
Home
Index