Nuprl Definition : cubical-type
{X ⊢ _} ==
{AF:A:I:fset(ℕ) ⟶ X(I) ⟶ Type × (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:X(I) ⟶ (A I a) ⟶ (A J f(a)))|
let A,F = AF
in (∀I:fset(ℕ). ∀a:X(I). ∀u:A I a. ((F I I 1 a u) = u ∈ (A I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:X(I). ∀u:A I a.
((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))}
Definitions occuring in Statement :
cube-set-restriction: f(s),
I_cube: A(I),
nh-comp: g ⋅ f,
nh-id: 1,
names-hom: I ⟶ J,
fset: fset(T),
nat: ℕ,
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 occuring in definition :
set: {x:A| B[x]} ,
product: x:A × B[x],
universe: Type,
function: x:A ⟶ B[x],
spread: spread def,
and: P ∧ Q,
nh-id: 1,
fset: fset(T),
nat: ℕ,
names-hom: I ⟶ J,
I_cube: A(I),
all: ∀x:A. B[x],
equal: s = t ∈ T,
nh-comp: g ⋅ f,
cube-set-restriction: f(s),
apply: f a
FDL editor aliases :
cubical-type
cubical-type
Latex:
\{X \mvdash{} \_\} ==
\{AF:A:I:fset(\mBbbN{}) {}\mrightarrow{} X(I) {}\mrightarrow{} Type \mtimes{} (I:fset(\mBbbN{})
{}\mrightarrow{} J:fset(\mBbbN{})
{}\mrightarrow{} f:J {}\mrightarrow{} I
{}\mrightarrow{} a:X(I)
{}\mrightarrow{} (A I a)
{}\mrightarrow{} (A J f(a)))|
let A,F = AF
in (\mforall{}I:fset(\mBbbN{}). \mforall{}a:X(I). \mforall{}u:A I a. ((F I I 1 a u) = u))
\mwedge{} (\mforall{}I,J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}a:X(I). \mforall{}u:A I a.
((F I K f \mcdot{} g a u) = (F J K g f(a) (F I J f a u))))\}
Date html generated:
2016_05_18-PM-01_37_55
Last ObjectModification:
2015_10_28-PM-04_18_36
Theory : cubical!type!theory
Home
Index