Nuprl Definition : closed-cubical-type
{ * ⊢ _} ==
{AF:A:I:fset(ℕ) ⟶ Type × (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ (A I) ⟶ (A J))|
let A,F = AF
in (∀I:fset(ℕ). ∀u:A I. ((F I I 1 u) = u ∈ (A I)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A I. ((F I K f ⋅ g u) = (F J K g (F I J f u)) ∈ (A K)))}
Definitions occuring in Statement :
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,
all: ∀x:A. B[x],
equal: s = t ∈ T,
nh-comp: g ⋅ f,
apply: f a
FDL editor aliases :
closed-cubical-type
Latex:
\{ * \mvdash{} \_\} ==
\{AF:A:I:fset(\mBbbN{}) {}\mrightarrow{} Type \mtimes{} (I:fset(\mBbbN{}) {}\mrightarrow{} J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I {}\mrightarrow{} (A I) {}\mrightarrow{} (A J))|
let A,F = AF
in (\mforall{}I:fset(\mBbbN{}). \mforall{}u:A I. ((F I I 1 u) = u))
\mwedge{} (\mforall{}I,J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}u:A I. ((F I K f \mcdot{} g u) = (F J K g (F I J f u))))\}
Date html generated:
2020_05_20-PM-01_50_22
Last ObjectModification:
2020_03_20-AM-10_25_48
Theory : cubical!type!theory
Home
Index