Nuprl Definition : comp-op
comp-op(Gamma;A) ==
I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I}
⟶ rho:Gamma(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)
Definitions occuring in Statement :
cubical-path-1: cubical-path-1(Gamma;A;I;i;rho;phi;u),
cubical-path-0: cubical-path-0(Gamma;A;I;i;rho;phi;u),
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
subset-iota: iota,
cubical-subset: I,psi,
face-presheaf: 𝔽,
csm-comp: G o F,
context-map: <rho>,
formal-cube: formal-cube(I),
cube-set-restriction: f(s),
I_cube: A(I),
nc-s: s,
add-name: I+i,
fset-member: a ∈ s,
fset: fset(T),
int-deq: IntDeq,
nat: ℕ,
not: ¬A,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x]
Definitions occuring in definition :
fset: fset(T),
set: {x:A| B[x]} ,
nat: ℕ,
not: ¬A,
fset-member: a ∈ s,
int-deq: IntDeq,
I_cube: A(I),
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
csm-comp: G o F,
cubical-subset: I,psi,
cube-set-restriction: f(s),
face-presheaf: 𝔽,
nc-s: s,
formal-cube: formal-cube(I),
subset-iota: iota,
context-map: <rho>,
add-name: I+i,
function: x:A ⟶ B[x],
cubical-path-0: cubical-path-0(Gamma;A;I;i;rho;phi;u),
cubical-path-1: cubical-path-1(Gamma;A;I;i;rho;phi;u)
FDL editor aliases :
comp-op
Latex:
comp-op(Gamma;A) ==
I:fset(\mBbbN{})
{}\mrightarrow{} i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\}
{}\mrightarrow{} rho:Gamma(I+i)
{}\mrightarrow{} phi:\mBbbF{}(I)
{}\mrightarrow{} u:\{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\}
{}\mrightarrow{} cubical-path-0(Gamma;A;I;i;rho;phi;u)
{}\mrightarrow{} cubical-path-1(Gamma;A;I;i;rho;phi;u)
Date html generated:
2020_05_20-PM-03_48_28
Last ObjectModification:
2020_03_27-AM-10_36_30
Theory : cubical!type!theory
Home
Index