Nuprl Definition : cubical-type
{X ⊢ _} ==
{AF:A:I:(Cname List) ⟶ X(I) ⟶ Type × (I:(Cname List)
⟶ J:(Cname List)
⟶ f:name-morph(I;J)
⟶ a:X(I)
⟶ (A I a)
⟶ (A J f(a)))|
let A,F = AF
in (∀I:Cname List. ∀a:X(I). ∀u:A I a. ((F I I 1 a u) = u ∈ (A I a)))
∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A I a.
((F I K (f o g) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K (f o g)(a))))}
Wellformedness Lemmas :
cubical-type_wf
Definitions occuring in Statement :
cube-set-restriction: f(s),
I-cube: X(I),
name-comp: (f o g),
id-morph: 1,
name-morph: name-morph(I;J),
coordinate_name: Cname,
list: T List,
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,
id-morph: 1,
list: T List,
coordinate_name: Cname,
name-morph: name-morph(I;J),
I-cube: X(I),
all: ∀x:A. B[x],
equal: s = t ∈ T,
name-comp: (f o g),
cube-set-restriction: f(s),
apply: f a
FDL editor aliases :
cubical-type
cubical-type
Latex:
\{X \mvdash{} \_\} ==
\{AF:A:I:(Cname List) {}\mrightarrow{} X(I) {}\mrightarrow{} Type \mtimes{} (I:(Cname List)
{}\mrightarrow{} J:(Cname List)
{}\mrightarrow{} f:name-morph(I;J)
{}\mrightarrow{} a:X(I)
{}\mrightarrow{} (A I a)
{}\mrightarrow{} (A J f(a)))|
let A,F = AF
in (\mforall{}I:Cname List. \mforall{}a:X(I). \mforall{}u:A I a. ((F I I 1 a u) = u))
\mwedge{} (\mforall{}I,J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K). \mforall{}a:X(I). \mforall{}u:A I a.
((F I K (f o g) a u) = (F J K g f(a) (F I J f a u))))\}
Date html generated:
2016_06_16-PM-05_38_36
Last ObjectModification:
2015_09_23-AM-09_30_11
Theory : cubical!sets
Home
Index