Nuprl Lemma : cubical-isect-family-comp
∀X,Delta:⊢. ∀s:Delta ⟶ X. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Delta(I). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}.
∀w:cubical-isect-family(X;A;B;I;(s)a).
(λK,g. (w K f ⋅ g) ∈ cubical-isect-family(X;A;B;J;(s)f(a)))
Proof
Definitions occuring in Statement :
cubical-isect-family: cubical-isect-family(X;A;B;I;a),
cube-context-adjoin: X.A,
cubical-type: {X ⊢ _},
csm-ap: (s)x,
cube_set_map: A ⟶ B,
cube-set-restriction: f(s),
I_cube: A(I),
cubical_set: CubicalSet,
nh-comp: g ⋅ f,
names-hom: I ⟶ J,
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
member: t ∈ T,
apply: f a,
lambda: λx.A[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
cubical-isect-family: cubical-isect-family(X;A;B;I;a),
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
true: True,
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
guard: {T},
uimplies: b supposing a,
prop: ℙ,
squash: ↓T,
cand: A c∧ B,
top: Top
Lemmas referenced :
cubical-isect-family_wf,
csm-ap_wf,
cubical-type_wf,
cube-context-adjoin_wf,
I_cube_wf,
names-hom_wf,
fset_wf,
nat_wf,
cube_set_map_wf,
cubical_set_wf,
cc-adjoin-cube_wf,
cube-set-restriction-comp,
iff_weakening_equal,
subtype_rel_self,
cube-set-restriction_wf,
nh-comp_wf,
csm-ap-restriction,
istype-universe,
true_wf,
squash_wf,
equal_wf,
cubical-type-at_wf,
istype-cubical-type-at,
subtype_rel-equal,
cubical-type-ap-morph_wf,
nh-comp-assoc,
istype-void,
cc-adjoin-cube-restriction
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalHypSubstitution,
setElimination,
thin,
rename,
dependent_set_memberEquality_alt,
sqequalRule,
hypothesis,
universeIsType,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
inhabitedIsType,
lambdaEquality_alt,
hyp_replacement,
equalitySymmetry,
equalityTransitivity,
applyEquality,
natural_numberEquality,
independent_functionElimination,
productElimination,
independent_isectElimination,
baseClosed,
imageMemberEquality,
dependent_functionElimination,
universeEquality,
instantiate,
because_Cache,
imageElimination,
isectEquality,
isect_memberEquality_alt,
equalityIsType1,
applyLambdaEquality,
productIsType,
independent_pairFormation,
voidElimination,
functionIsType,
equalityIstype
Latex:
\mforall{}X,Delta:\mvdash{}. \mforall{}s:Delta {}\mrightarrow{} X. \mforall{}I,J:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}a:Delta(I). \mforall{}A:\{X \mvdash{} \_\}. \mforall{}B:\{X.A \mvdash{} \_\}.
\mforall{}w:cubical-isect-family(X;A;B;I;(s)a).
(\mlambda{}K,g. (w K f \mcdot{} g) \mmember{} cubical-isect-family(X;A;B;J;(s)f(a)))
Date html generated:
2019_11_05-PM-00_22_48
Last ObjectModification:
2018_12_12-PM-06_35_03
Theory : cubical!type!theory
Home
Index