Add an identity to get a category

[treeowl]

This might already exist somewhere, but I couldn't find it. I'm not at all committed to these names.

data Categorize s a b where
  Id :: Categorize s a a
  Embed :: s a b -> Categorize s a b

instance Semigroupoid s => Semigroupoid (Categorize s) where
  Id `o` y = y
  x `o` Id = x
  Embed x `o` Embed y = Embed (x `o` y)

instance Semigroupoid s => Category (Categorize s) where
  id = Id
  (.) = o

[treeowl]

Since Option is in semigroups, I think semigroupoids is likely the right place for this thing, whatever it and its constructors should be called.

[ekmett]

I have no objection to adding such a construction in principle. Not sure about the name.

[treeowl]

Do you have better names?

[treeowl]

Bump! I want this for a fork of type-aligned I'm working on. Any chance you can pick a name and stick it in? Also, it supports the following eliminator, which should therefore be included.

categorize :: (a ~ b => r) -> (s a b -> r) -> Categorize s a b -> r
categorize r _ Id = r
categorize _ f (Embed x) = f x

[kozross]

@RyanGlScott I'd be happy to add this in, but the name issue never got resolved. Would Categorical suit? If so, I'd be happy to implement.

[RyanGlScott]

Honestly, I don't have a better name myself. Admittedly, my knowledge of category theory is pretty limited, so I'm perhaps not the best person to task with thinking of a good name for this. Ultimately, I think we have to just pick something.