Nuprl Definition : cat-co-retraction
co-retraction(f) == ∃g:cat-arrow(C) y x. 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 :
exists: ∃x:A. B[x],
apply: f a,
cat-arrow: cat-arrow(C),
cat-inverse: fg=1
FDL editor aliases :
cat-co-retraction
Latex:
co-retraction(f) == \mexists{}g:cat-arrow(C) y x. fg=1
Date html generated:
2020_05_20-AM-07_49_52
Last ObjectModification:
2017_01_08-PM-00_36_32
Theory : small!categories
Home
Index