Nuprl Definition : named-path-morph
named-path-morph(X;A;I;K;z;x;f;alpha;w) == (w iota(z)(alpha) f[z:=x])
Definitions occuring in Statement :
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s),
iota: iota(x),
extend-name-morph: f[z1:=z2],
cons: [a / b]
Definitions occuring in definition :
cubical-type-ap-morph: (u a f),
extend-name-morph: f[z1:=z2],
cube-set-restriction: f(s),
cons: [a / b],
iota: iota(x)
FDL editor aliases :
named-path-morph
named-path-morph
Latex:
named-path-morph(X;A;I;K;z;x;f;alpha;w) == (w iota(z)(alpha) f[z:=x])
Date html generated:
2016_06_16-PM-07_28_08
Last ObjectModification:
2015_09_23-AM-09_34_06
Theory : cubical!sets
Home
Index