Nuprl Lemma : unit-cube-cubical-type
∀[I:fset(ℕ)]
({formal-cube(I) ⊢ _} ~ {AF:A:L:fset(ℕ) ⟶ L ⟶ I ⟶ Type × (L:fset(ℕ)
⟶ J:fset(ℕ)
⟶ f:J ⟶ L
⟶ a:L ⟶ I
⟶ (A L a)
⟶ (A J a ⋅ f))|
let A,F = AF
in (∀K:fset(ℕ). ∀a:K ⟶ I. ∀u:A K a. ((F K K 1 a u) = u ∈ (A K a)))
∧ (∀L,J,K:fset(ℕ). ∀f:J ⟶ L. ∀g:K ⟶ J. ∀a:L ⟶ I. ∀u:A L a.
((F L K f ⋅ g a u) = (F J K g a ⋅ f (F L J f a u)) ∈ (A K a ⋅ f ⋅ g)))} )
Proof
Definitions occuring in Statement :
cubical-type: {X ⊢ _},
formal-cube: formal-cube(I),
nh-comp: g ⋅ f,
nh-id: 1,
names-hom: I ⟶ J,
fset: fset(T),
nat: ℕ,
uall: ∀[x:A]. B[x],
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,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
cube-cat: CubeCat,
all: ∀x:A. B[x],
top: Top,
formal-cube: formal-cube(I),
Yoneda: Yoneda(I)
Lemmas referenced :
unit-set-presheaf-type,
cube-cat_wf,
cat_ob_pair_lemma,
cat_arrow_triple_lemma,
cat_comp_tuple_lemma,
cubical-type-sq-presheaf-type,
cat_id_tuple_lemma
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
hypothesis,
sqequalRule,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}[I:fset(\mBbbN{})]
(\{formal-cube(I) \mvdash{} \_\} \msim{} \{AF:A:L:fset(\mBbbN{}) {}\mrightarrow{} L {}\mrightarrow{} I {}\mrightarrow{} Type \mtimes{} (L:fset(\mBbbN{})
{}\mrightarrow{} J:fset(\mBbbN{})
{}\mrightarrow{} f:J {}\mrightarrow{} L
{}\mrightarrow{} a:L {}\mrightarrow{} I
{}\mrightarrow{} (A L a)
{}\mrightarrow{} (A J a \mcdot{} f))|
let A,F = AF
in (\mforall{}K:fset(\mBbbN{}). \mforall{}a:K {}\mrightarrow{} I. \mforall{}u:A K a. ((F K K 1 a u) = u))
\mwedge{} (\mforall{}L,J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} L. \mforall{}g:K {}\mrightarrow{} J. \mforall{}a:L {}\mrightarrow{} I. \mforall{}u:A L a.
((F L K f \mcdot{} g a u) = (F J K g a \mcdot{} f (F L J f a u))))\} )
Date html generated:
2018_05_23-AM-09_15_40
Last ObjectModification:
2018_05_20-PM-06_14_36
Theory : cubical!type!theory
Home
Index