Nuprl Definition : cat-retraction
retraction(g) == ∃f:cat-arrow(C) x y. fg=1
Definitions occuring in Statement :
cat-inverse: fg=1,
cat-arrow: cat-arrow(C),
exists: ∃x:A. B[x],
apply: f a
Definitions occuring in definition :
cat-inverse: fg=1,
cat-arrow: cat-arrow(C),
apply: f a,
exists: ∃x:A. B[x]
FDL editor aliases :
cat-retraction
Latex:
retraction(g) == \mexists{}f:cat-arrow(C) x y. fg=1
Date html generated:
2017_01_09-AM-09_11_05
Last ObjectModification:
2017_01_08-PM-00_34_08
Theory : small!categories
Home
Index