Nuprl Definition : cubical-term
{X ⊢ _:AF} ==
{u:I:(Cname List) ⟶ a:X(I) ⟶ ((fst(AF)) I a)|
∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I). let A,F = AF in (F I J f a (u I a)) = (u J f(a)) ∈ (A J f(a))}
Wellformedness Lemmas :
cubical-term_wf
Definitions occuring in Statement :
cube-set-restriction: f(s),
I-cube: X(I),
name-morph: name-morph(I;J),
coordinate_name: Cname,
list: T List,
pi1: fst(t),
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
spread: spread def,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
pi1: fst(t),
list: T List,
coordinate_name: Cname,
name-morph: name-morph(I;J),
all: ∀x:A. B[x],
I-cube: X(I),
spread: spread def,
equal: s = t ∈ T,
apply: f a,
cube-set-restriction: f(s)
FDL editor aliases :
cubical-term
cubical-term
Latex:
\{X \mvdash{} \_:AF\} ==
\{u:I:(Cname List) {}\mrightarrow{} a:X(I) {}\mrightarrow{} ((fst(AF)) I a)|
\mforall{}I,J:Cname List. \mforall{}f:name-morph(I;J). \mforall{}a:X(I). let A,F = AF in (F I J f a (u I a)) = (u J f(a))\}
Date html generated:
2016_06_16-PM-05_39_55
Last ObjectModification:
2015_09_23-AM-09_30_19
Theory : cubical!sets
Home
Index