Nuprl Definition : refl-path
refl-path(A;a;I;alpha) == <fresh-cname(I), (a I alpha alpha iota'(I))>
Definitions occuring in Statement :
cubical-type-ap-morph: (u a f),
iota': iota'(I),
add-fresh-cname: I+,
fresh-cname: fresh-cname(I),
apply: f a,
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
fresh-cname: fresh-cname(I),
cubical-type-ap-morph: (u a f),
add-fresh-cname: I+,
iota': iota'(I),
apply: f a
FDL editor aliases :
refl-path
refl-path
Latex:
refl-path(A;a;I;alpha) == <fresh-cname(I), (a I alpha alpha iota'(I))>
Date html generated:
2016_06_16-PM-08_06_09
Last ObjectModification:
2015_09_23-AM-09_34_51
Theory : cubical!sets
Home
Index