Nuprl Lemma : cubical-id-equiv-subset
∀[G,phi,A:Top]. (IdEquiv(G, phi;A) ~ IdEquiv(G;A))
Proof
Definitions occuring in Statement :
cubical-id-equiv: IdEquiv(X;T),
context-subset: Gamma, phi,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
cubical-id-equiv: IdEquiv(X;T),
cubical-id-fun: cubical-id-fun(X),
cubical-lam: cubical-lam(X;b),
cubical-id-is-equiv: cubical-id-is-equiv(X;T),
id-fiber-center: id-fiber-center(X;T),
contr-witness: contr-witness(X;c;p),
id-fiber-contraction: id-fiber-contraction(X;T),
cubical-refl: refl(a),
term-to-path: <>(a),
singleton-contraction: singleton-contraction(X;pth),
member: t ∈ T,
top: Top,
path-contraction: path-contraction(X;pth),
path-type: (Path_A a b),
pathtype: Path(A),
cube-context-adjoin: X.A,
cubical-fun: (A ⟶ B),
context-subset: Gamma, phi,
all: ∀x:A. B[x],
cubical-fun-family: cubical-fun-family(X; A; B; I; a),
pi1: fst(t),
pi2: snd(t),
cubical-lambda: (λb),
implies: P ⇒ Q,
prop: ℙ
Lemmas referenced :
top_wf,
cubical-lambda-subset,
cubical-lambda-subset2,
I_cube_pair_redex_lemma,
cube_set_restriction_pair_lemma,
equal_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
because_Cache,
cut,
introduction,
extract_by_obid,
hypothesis,
hypothesisEquality,
isect_memberEquality,
voidElimination,
voidEquality,
sqequalRule,
sqequalHypSubstitution,
isectElimination,
thin,
dependent_functionElimination,
lambdaFormation,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination
Latex:
\mforall{}[G,phi,A:Top]. (IdEquiv(G, phi;A) \msim{} IdEquiv(G;A))
Date html generated:
2017_10_05-AM-02_08_45
Last ObjectModification:
2017_07_28-AM-10_18_21
Theory : cubical!type!theory
Home
Index