Nuprl Definition : nh-comp
g ⋅ f == dma-lift-compose(names(I);names(J);NamesDeq;NamesDeq;f;g)
Definitions occuring in Statement :
names-deq: NamesDeq,
names: names(I),
dma-lift-compose: dma-lift-compose(I;J;eqi;eqj;f;g)
Definitions occuring in definition :
dma-lift-compose: dma-lift-compose(I;J;eqi;eqj;f;g),
names: names(I),
names-deq: NamesDeq
FDL editor aliases :
nh-comp
Latex:
g \mcdot{} f == dma-lift-compose(names(I);names(J);NamesDeq;NamesDeq;f;g)
Date html generated:
2016_05_18-AM-11_59_29
Last ObjectModification:
2015_10_13-PM-01_26_55
Theory : cubical!type!theory
Home
Index