Nuprl Lemma : cubical_set-ext
{FM:F:fset(ℕ) ⟶ 𝕌{j'} × (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ J ⟶ I ⟶ (F I) ⟶ (F J))|
let F,M = FM
in (∀I:fset(ℕ). ∀s:FM(I). (1(s) = s ∈ FM(I)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀s:FM(I). (f ⋅ g(s) = g(f(s)) ∈ FM(K)))} ≡ CubicalSet{j}
Proof
Definitions occuring in Statement :
cube-set-restriction: f(s),
I_cube: A(I),
cubical_set: CubicalSet,
nh-comp: g ⋅ f,
nh-id: 1,
names-hom: I ⟶ J,
fset: fset(T),
nat: ℕ,
ext-eq: A ≡ B,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
cube-cat: CubeCat,
all: ∀x:A. B[x],
I_cube: A(I),
I_set: A(I),
cube-set-restriction: f(s),
psc-restriction: f(s),
cubical_set: CubicalSet
Lemmas referenced :
ps_context-ext,
cube-cat_wf,
cat_ob_pair_lemma,
cat_arrow_triple_lemma,
cat_id_tuple_lemma,
cat_comp_tuple_lemma
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
hypothesis,
sqequalRule,
dependent_functionElimination,
Error :memTop
Latex:
\{FM:F:fset(\mBbbN{}) {}\mrightarrow{} \mBbbU{}\{j'\} \mtimes{} (I:fset(\mBbbN{}) {}\mrightarrow{} J:fset(\mBbbN{}) {}\mrightarrow{} J {}\mrightarrow{} I {}\mrightarrow{} (F I) {}\mrightarrow{} (F J))|
let F,M = FM
in (\mforall{}I:fset(\mBbbN{}). \mforall{}s:FM(I). (1(s) = s))
\mwedge{} (\mforall{}I,J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}s:FM(I). (f \mcdot{} g(s) = g(f(s))))\} \mequiv{} CubicalSet\{j\}
Date html generated:
2020_05_20-PM-01_39_14
Last ObjectModification:
2020_04_03-PM-03_44_17
Theory : cubical!type!theory
Home
Index