Nuprl Definition : I-path-morph

I-path-morph(X;A;I;K;f;alpha;p) ==
  let z,w = p 
  in <fresh-cname(K), named-path-morph(X;A;I;K;z;fresh-cname(K);f;alpha;w)>


Definitions occuring in Statement :  named-path-morph: named-path-morph(X;A;I;K;z;x;f;alpha;w),  fresh-cname: fresh-cname(I),  spread: spread def,  pair: <a, b>
Definitions occuring in definition :  spread: spread def,  pair: <a, b>,  named-path-morph: named-path-morph(X;A;I;K;z;x;f;alpha;w),  fresh-cname: fresh-cname(I)
FDL editor aliases :  I-path-morph I-path-morph
Latex:
I-path-morph(X;A;I;K;f;alpha;p)  ==
    let  z,w  =  p 
    in  <fresh-cname(K),  named-path-morph(X;A;I;K;z;fresh-cname(K);f;alpha;w)>


Date html generated: 2016_06_16-PM-07_28_57
Last ObjectModification: 2015_09_23-AM-09_34_13

Theory : cubical!sets


Home Index