Nuprl Definition : dM-lift
dM-lift(I;J;f) == free-dma-lift(names(J);NamesDeq;dM(I);free-dml-deq(names(I);NamesDeq);f)
Definitions occuring in Statement :
dM: dM(I),
names-deq: NamesDeq,
names: names(I),
free-dma-lift: free-dma-lift(T;eq;dm;eq2;f),
free-dml-deq: free-dml-deq(T;eq)
Definitions occuring in definition :
free-dma-lift: free-dma-lift(T;eq;dm;eq2;f),
dM: dM(I),
free-dml-deq: free-dml-deq(T;eq),
names: names(I),
names-deq: NamesDeq
FDL editor aliases :
dM-lift
Latex:
dM-lift(I;J;f) == free-dma-lift(names(J);NamesDeq;dM(I);free-dml-deq(names(I);NamesDeq);f)
Date html generated:
2016_05_18-AM-11_57_47
Last ObjectModification:
2015_10_13-PM-02_53_29
Theory : cubical!type!theory
Home
Index