Nuprl Definition : path-eq

path-eq(X;A;I;alpha;p;q) ==
  let z,w = p 
  in let z',w' = q 
     in (w iota(z)(alpha) rename-one-name(z;z')) = w' ∈ A(iota(z')(alpha))


Definitions occuring in Statement :  cubical-type-ap-morph: (u a f),  cubical-type-at: A(a),  cube-set-restriction: f(s),  rename-one-name: rename-one-name(z1;z2),  iota: iota(x),  cons: [a / b],  spread: spread def,  equal: s = t ∈ T
Definitions occuring in definition :  spread: spread def,  equal: s = t ∈ T,  cubical-type-at: A(a),  cubical-type-ap-morph: (u a f),  rename-one-name: rename-one-name(z1;z2),  cube-set-restriction: f(s),  cons: [a / b],  iota: iota(x)
FDL editor aliases :  path-eq path-eq
Latex:
path-eq(X;A;I;alpha;p;q)  ==
    let  z,w  =  p 
    in  let  z',w'  =  q 
          in  (w  iota(z)(alpha)  rename-one-name(z;z'))  =  w'


Date html generated: 2016_06_16-PM-07_29_09
Last ObjectModification: 2015_09_23-AM-09_34_17

Theory : cubical!sets


Home Index