Nuprl Lemma : equiv-contr_wf
∀[G:j⊢]. ∀[A,T:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(T;A)}]. ∀[a:{G ⊢ _:A}].
  (equiv-contr(f;a) ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))})
Proof
Definitions occuring in Statement : 
equiv-contr: equiv-contr(f;a)
, 
equiv-fun: equiv-fun(f)
, 
cubical-equiv: Equiv(T;A)
, 
cubical-fiber: Fiber(w;a)
, 
contractible-type: Contractible(A)
, 
cubical-term: {X ⊢ _:A}
, 
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-equiv: Equiv(T;A)
, 
subtype_rel: A ⊆r B
, 
squash: ↓T
, 
all: ∀x:A. B[x]
, 
true: True
, 
equiv-fun: equiv-fun(f)
, 
is-cubical-equiv: IsEquiv(T;A;w)
, 
prop: ℙ
, 
uimplies: b supposing a
, 
guard: {T}
, 
iff: P 
⇐⇒ Q
, 
and: P ∧ Q
, 
implies: P 
⇒ Q
, 
cubical-type: {X ⊢ _}
, 
csm-id: 1(X)
, 
csm-ap-type: (AF)s
, 
cc-fst: p
, 
csm-id-adjoin: [u]
, 
csm-ap: (s)x
, 
csm-adjoin: (s;u)
, 
pi1: fst(t)
, 
equiv-contr: equiv-contr(f;a)
, 
cc-snd: q
, 
csm-comp: G o F
, 
compose: f o g
, 
pi2: snd(t)
, 
rev_implies: P 
⇐ Q
Lemmas referenced : 
cubical-snd_wf, 
cubical_set_cumulativity-i-j, 
cubical-fun_wf, 
is-cubical-equiv_wf, 
cube-context-adjoin_wf, 
cubical-type-cumulativity2, 
csm-ap-type_wf, 
cc-fst_wf, 
cc-snd_wf, 
cubical-term_wf, 
csm-cubical-fun, 
cubical-equiv_wf, 
cubical-type_wf, 
cubical_set_wf, 
csm-ap-term_wf, 
contractible-type_wf, 
cubical-fiber_wf, 
csm-id-adjoin_wf, 
equiv-fun_wf, 
member_wf, 
squash_wf, 
true_wf, 
istype-universe, 
csm-cubical-pi, 
iff_weakening_equal, 
csm-contractible-type, 
csm-adjoin_wf, 
equal_wf, 
csm-ap-type-fst-id-adjoin, 
subtype_rel_self, 
csm-cubical-fiber, 
csm_ap_term_fst_adjoin_lemma, 
cc_snd_csm_id_adjoin_lemma, 
cc-snd-csm-adjoin-sq, 
csm-id_wf, 
subset-cubical-term2, 
sub_cubical_set_self, 
cubical-sigma_wf, 
csm-ap-id-type, 
csm-ap-id-term, 
equal_functionality_wrt_subtype_rel2, 
cubical-app_wf, 
csm-comp_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
introduction, 
cut, 
sqequalHypSubstitution, 
thin, 
instantiate, 
extract_by_obid, 
isectElimination, 
hypothesisEquality, 
applyEquality, 
hypothesis, 
sqequalRule, 
because_Cache, 
lambdaEquality_alt, 
imageElimination, 
dependent_functionElimination, 
natural_numberEquality, 
imageMemberEquality, 
baseClosed, 
equalityTransitivity, 
equalitySymmetry, 
hyp_replacement, 
universeIsType, 
axiomEquality, 
isect_memberEquality_alt, 
isectIsTypeImplies, 
inhabitedIsType, 
universeEquality, 
independent_isectElimination, 
productElimination, 
independent_functionElimination, 
setElimination, 
rename, 
lambdaFormation_alt, 
equalityIstype, 
Error :memTop, 
cumulativity
Latex:
\mforall{}[G:j\mvdash{}].  \mforall{}[A,T:\{G  \mvdash{}  \_\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(T;A)\}].  \mforall{}[a:\{G  \mvdash{}  \_:A\}].
    (equiv-contr(f;a)  \mmember{}  \{G  \mvdash{}  \_:Contractible(Fiber(equiv-fun(f);a))\})
Date html generated:
2020_05_20-PM-03_27_10
Last ObjectModification:
2020_04_08-PM-04_45_44
Theory : cubical!type!theory
Home
Index