Nuprl Lemma : contractible-iff-inhabited-prop
∀X:j⊢. ∀A:{X ⊢ _}. ∀cA:X +⊢ Compositon(A). ({X ⊢ _:Contractible(A)} ⇐⇒ {X ⊢ _:isProp(A)} ∧ {X ⊢ _:A})
Proof
Definitions occuring in Statement :
composition-structure: Gamma ⊢ Compositon(A),
is-prop: isProp(A),
contractible-type: Contractible(A),
cubical-term: {X ⊢ _:A},
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
rev_implies: P ⇐ Q,
composition-structure: Gamma ⊢ Compositon(A),
composition-function: composition-function{j:l,i:l}(Gamma;A),
uniform-comp-function: uniform-comp-function{j:l, i:l}(Gamma; A; comp)
Lemmas referenced :
is-prop-contractible,
cubical-term_wf,
contractible-type_wf,
cubical-type-cumulativity2,
cubical_set_cumulativity-i-j,
is-prop_wf,
composition-structure_wf,
cubical-type_wf,
cubical_set_wf,
contractible-to-prop_wf,
subtype_rel_self,
contr-center_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_pairFormation,
rename,
universeIsType,
instantiate,
isectElimination,
applyEquality,
sqequalRule,
productElimination,
independent_functionElimination,
productIsType,
because_Cache
Latex:
\mforall{}X:j\mvdash{}. \mforall{}A:\{X \mvdash{} \_\}. \mforall{}cA:X +\mvdash{} Compositon(A).
(\{X \mvdash{} \_:Contractible(A)\} \mLeftarrow{}{}\mRightarrow{} \{X \mvdash{} \_:isProp(A)\} \mwedge{} \{X \mvdash{} \_:A\})
Date html generated:
2020_05_20-PM-04_58_38
Last ObjectModification:
2020_04_13-PM-02_17_08
Theory : cubical!type!theory
Home
Index