instance Category Object

[Icelandjack]

You can implement a Category Object if you add Coyonedas to the Object to get rid of the Functor constraint, maybe you find it useful

newtype Object :: (Type -> Type) -> (Type -> Type) -> Type where
  Object :: (forall xx. Coyoneda f xx -> Coyoneda g (xx, Object f g)) -> Object f g

instance Category Object where
  id :: Object f f
  id = Object (\a -> fmap (, id) a)

  (.) :: Object b c -> Object a b -> Object a c
  Object obj' . Object obj = Object (fmap (\((x, ab), bc) -> (x, bc . ab)) . obj' . obj)

[fumieval]

I have thought about it several years ago but I thought it's not worth changing the representation at the time. Maybe it's time to revisit...

[Icelandjack]

One possibility is:

Define the ‘default’ Object (with Coyoneda) and an isomorphic Obj type (without Coyoneda)

newtype Object f g = Object_ (forall xx. Coyoneda f xx -> Coyoneda g (xx, Object f g))
newtype Obj    f g = Obj     (forall xx. f xx -> g (xx, Obj f g))

toObj :: Functor g => Object f g -> Obj f g
toObj (Object_ object_) = Obj (lowerCoyoneda . object_ . liftCoyoneda)

fromObj :: Functor f => Obj f g -> Object f g
fromObj (Obj obj) = Object_ (liftCoyoneda . obj . lowerCoyoneda)

Then define a -XPatternSynonym

pattern Object :: (Functor f, Functor g) => (forall xx. f xx -> g (xx, Object f g)) -> Object f g
pattern Object obj <- (toObj -> Obj obj)
  where Object obj = fromObj (Obj obj)

---

Now, we can exploit more categorical structure. "Lateral composition" from your paper is witnessed by an instance of `

class CoproductCat Object where
  type Coprod Object = Sum

  inl :: Object f (Sum f g)
  inl = Object_ (fmap (, inl) . hoistCoyoneda InL)

  inr :: Object g (Sum f g)
  inr = Object_ (fmap (, inr) . hoistCoyoneda InR)

  (|||) :: Object f1 g -> Object f2 g -> Object (Sum f1 f2) g
  Object_ obj1 ||| Object_ obj2 = Object_ $ \case
    Coyoneda f (InL xs) -> fmap (fmap (||| Object_ obj2)) (obj1 (Coyoneda f xs))
    Coyoneda f (InR xs) -> fmap (fmap (Object_ obj1 |||)) (obj2 (Coyoneda f xs))

and (I haven't checked the laws) but Object may have initial and terminal objects

instance HasInitial Object where
  type Initial Object = Zero

  initial :: Object Zero f
  initial = Object_ (\(Coyoneda _ zero) -> absurd1 zero)

instance HasTerminal Object where
  type Terminal Object = Proxy

  term :: Object f Proxy
  term = Object_ (\_ -> liftCoyoneda Proxy)

for

data Zero :: k -> Type

type Cat ob = ob -> ob -> Type

class Category cat => HasTerminal (cat :: Cat ob) where
  type Terminal cat :: ob
  terminal :: cat a (Terminal cat)

class Category cat => HasInitial (cat :: Cat ob) where
  type Initial cat :: ob
  initial :: cat (Initial cat) a

[Icelandjack]

Sadly using pattern Object induces Functor constraints everywhere.