Nuprl Lemma : is-cubical-equiv-at
∀[X:j⊢]. ∀[T:{X ⊢ _}]. ∀[A,w,I,rho:Top].
(IsEquiv(T;A;w)(rho) ~ {eqv:J:fset(ℕ)
⟶ f:J ⟶ I
⟶ u:A(f(rho))
⟶ (u1:u1:T((p)(f(rho);u)) × (Path_((A)p)p (q)p app(((w)p)p; q))(((f(rho);u);u1))
× cubical-pi-family(X.A.Fiber((w)p;q);(Fiber((w)p;q))p;(Path_((Fiber((w)p;q))p)p (q)p
q);J;((f(rho);u);u1)))|
∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f(rho)).
((eqv J f u (f(rho);u) g)
= (eqv K f ⋅ g (u f(rho) g))
∈ (u1:u1:T((p)g((f(rho);u))) × (Path_((A)p)p (q)p app(((w)p)p; q))((g((f(rho);u));u1))
× cubical-pi-family(X.A.Fiber((w)p;q);(Fiber((w)p;q))p;(Path_((Fiber((w)p;q))p)p (q)p
q);K;(g((f(rho);u));u1))))} )
Proof
Definitions occuring in Statement :
is-cubical-equiv: IsEquiv(T;A;w),
cubical-fiber: Fiber(w;a),
contractible-type: Contractible(A),
path-type: (Path_A a b),
cubical-app: app(w; u),
cubical-pi-family: cubical-pi-family(X;A;B;I;a),
cc-snd: q,
cc-fst: p,
cc-adjoin-cube: (v;u),
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
cubical-type: {X ⊢ _},
csm-ap: (s)x,
cube-set-restriction: f(s),
cubical_set: CubicalSet,
nh-comp: g ⋅ f,
names-hom: I ⟶ J,
fset: fset(T),
nat: ℕ,
uall: ∀[x:A]. B[x],
top: Top,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
is-cubical-equiv: IsEquiv(T;A;w),
all: ∀x:A. B[x],
cubical-pi: ΠA B,
cubical-pi-family: cubical-pi-family(X;A;B;I;a)
Lemmas referenced :
cc_fst_adjoin_cube_lemma,
cubical_type_at_pair_lemma,
istype-top,
cubical-type_wf,
cubical_set_wf,
contractible-type-at,
cubical-fiber-at,
csm-ap-type-at
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
Error :memTop,
hypothesis,
axiomSqEquality,
inhabitedIsType,
hypothesisEquality,
isect_memberEquality_alt,
isectElimination,
isectIsTypeImplies,
universeIsType,
instantiate,
because_Cache
Latex:
\mforall{}[X:j\mvdash{}]. \mforall{}[T:\{X \mvdash{} \_\}]. \mforall{}[A,w,I,rho:Top].
(IsEquiv(T;A;w)(rho) \msim{} \{eqv:J:fset(\mBbbN{})
{}\mrightarrow{} f:J {}\mrightarrow{} I
{}\mrightarrow{} u:A(f(rho))
{}\mrightarrow{} (u1:u1:T((p)(f(rho);u))
\mtimes{} (Path\_((A)p)p (q)p app(((w)p)p; q))(((f(rho);u);u1))
\mtimes{} cubical-pi-family(X.A.Fiber((w)p;q);(Fiber((w)p;q))
p;(Path\_((Fiber((w)p;q))p)p (q)p
q);J;((f(rho);u);u1)))|
\mforall{}J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}u:A(f(rho)).
((eqv J f u (f(rho);u) g) = (eqv K f \mcdot{} g (u f(rho) g)))\} )
Date html generated:
2020_05_20-PM-03_25_43
Last ObjectModification:
2020_04_06-PM-06_44_14
Theory : cubical!type!theory
Home
Index