Nuprl Lemma : context-map_wf
∀I:fset(ℕ). ∀Gamma:j⊢. ∀rho:Gamma(I). (<rho> ∈ formal-cube(I) j⟶ Gamma)
Proof
Definitions occuring in Statement :
context-map: <rho>,
cube_set_map: A ⟶ B,
formal-cube: formal-cube(I),
I_cube: A(I),
cubical_set: CubicalSet,
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
member: t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
cube-cat: CubeCat,
cubical_set: CubicalSet,
I_cube: A(I),
I_set: A(I),
cube_set_map: A ⟶ B,
formal-cube: formal-cube(I),
Yoneda: Yoneda(I),
context-map: <rho>,
ps-context-map: <rho>
Lemmas referenced :
ps-context-map_wf,
cube-cat_wf,
cat_ob_pair_lemma,
cat_arrow_triple_lemma,
cat_comp_tuple_lemma
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
dependent_functionElimination,
thin,
hypothesis,
sqequalRule,
Error :memTop
Latex:
\mforall{}I:fset(\mBbbN{}). \mforall{}Gamma:j\mvdash{}. \mforall{}rho:Gamma(I). (<rho> \mmember{} formal-cube(I) j{}\mrightarrow{} Gamma)
Date html generated:
2020_05_20-PM-01_41_01
Last ObjectModification:
2020_04_03-PM-03_33_32
Theory : cubical!type!theory
Home
Index