Nuprl Definition : cat-inverse
fg=1 == (cat-comp(C) x y x f g) = (cat-id(C) x) ∈ (cat-arrow(C) x x)
Definitions occuring in Statement :
cat-comp: cat-comp(C),
cat-id: cat-id(C),
cat-arrow: cat-arrow(C),
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
equal: s = t ∈ T,
cat-arrow: cat-arrow(C),
cat-comp: cat-comp(C),
apply: f a,
cat-id: cat-id(C)
FDL editor aliases :
cat-inverse
Latex:
fg=1 == (cat-comp(C) x y x f g) = (cat-id(C) x)
Date html generated:
2020_05_20-AM-07_49_49
Last ObjectModification:
2017_01_08-PM-00_30_00
Theory : small!categories
Home
Index