Nuprl Definition : cat-isomorphism
cat-isomorphism(C;x;y;f) == ∃g:cat-arrow(C) y x. (fg=1 ∧ gf=1)
Definitions occuring in Statement :
cat-inverse: fg=1,
cat-arrow: cat-arrow(C),
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a
Definitions occuring in definition :
cat-inverse: fg=1,
and: P ∧ Q,
cat-arrow: cat-arrow(C),
apply: f a,
exists: ∃x:A. B[x]
FDL editor aliases :
cat-isomorphism
Latex:
cat-isomorphism(C;x;y;f) == \mexists{}g:cat-arrow(C) y x. (fg=1 \mwedge{} gf=1)
Date html generated:
2017_01_09-AM-09_11_11
Last ObjectModification:
2017_01_08-PM-01_04_06
Theory : small!categories
Home
Index