CODEWITHSUNDEEP
haskellcategory-theoryarrow-abstractioncategory-abstractions
Zhiltsoff Igor
Zhiltsoff Igor

Reputation: 1822

Does Pointed for categories embody well-pointed categories?

In this post leftaroundabout speaks of well-pointed categories. In the post, the WellPointed class is a subclass of Category, unlike Control.Arrow.Constrained.WellPointed (the reasons for this we discussed in the comments under the post):

class Category c => WellPointed c where
  type Terminal c :: *
  point :: a -> Terminal c `c` a
  unpoint :: Terminal c `c` a -> a

As far as I understand, this code could be generalised a bit with Data.Pointed.Pointed and Data.Copointed.Copointed (there is a HaskellWiki on why using Pointed is not the best idea, yet we are speaking pure theory, not library design).

But why do we need Copointed interface for well-pointed categories? In Wikipedia it says that the well-pointed category simply has enough points to tell different morphisms apart. If we have point (or globalElement in Control.Arrow.Constrained.WellPointed's terms), we would have the whole domain of any morphisms lifted into the category, including the points where different morphisms are unequal for every pair. leftaroundabout notes that Monad m => Kleisli m does not allow copoint, but it seems to me it is well-pointed (Monad m => Kleisli m is an instance of Control.Arrow.Constrained.WellPointed).

So, my questions are:

Upvotes: 1

Views: 105

Answers (0)

Related Questions