Profunctor-based category theory

KindCat.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE BlockArguments #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT disable #-}

module KindCat where

import Prelude (Either(..), Bool(..), String, Int, ($), either, fmap, const)
import qualified Prelude as P
import Data.Kind (Type, Constraint)
import Data.Void
import GHC.Exts (Any)


infixr 0 ~>, .~>, :~>
infixl 1 \\
infixr 0 //
infixr 3 :**:, :++:, &&, ||, ~~>
infixr 9 .

type PRO k1 k2 = k1 -> k2 -> Type
type CAT k = PRO k k
type BI k = (k, k) -> k
type OB k = k -> Constraint

type Category :: CAT k -> Constraint
class (Profunctor cat, (~>) ~ cat) => Category (cat :: CAT k) where
  type Ob (a :: k) :: Constraint
  type Ob a = ()
  id :: Ob a => cat a a
  (.) :: cat b c -> cat a b -> cat a c

type family (~>) :: CAT k
type CategoryOf k = Category ((~>) :: CAT k)

type Obj a = a ~> a
obj :: forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj = id @k @_ @a
src :: forall {k} a b p. Profunctor p => p (a :: k) b -> Obj a
src p = obj @a \\ p
tgt :: forall {k} a b p. Profunctor p => p (a :: k) b -> Obj b
tgt p = obj @b \\ p

type Profunctor :: forall {k1} {k2}. PRO k1 k2 -> Constraint
class (CategoryOf k1, CategoryOf k2) => Profunctor (p :: PRO k1 k2) where
  dimap :: c ~> a -> b ~> d -> p a b -> p c d
  (\\) :: ((Ob a, Ob b) => r) -> p a b -> r
  default (\\) :: (Ob a, Ob b) => ((Ob a, Ob b) => r) -> p a b -> r
  r \\ _ = r

(//) :: Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r
p // r = r \\ p

lmap :: Profunctor p => c ~> a -> p a b -> p c b
lmap l p = dimap l id p \\ p

rmap :: Profunctor p => b ~> d -> p a b -> p a d
rmap r p = dimap id r p \\ p

dimapDefault :: CategoryOf k => (c :: k) ~> a -> (b :: k) ~> d -> a ~> b -> c ~> d
dimapDefault f g h = g . h . f

class Ob a => Ob' a
instance Ob a => Ob' a
type VacuusOb k = forall a. Ob' (a :: k)


type instance (~>) = (->)
instance Category (->) where
  id = \a -> a
  f . g = \x -> f (g x)
instance Profunctor (->) where
  dimap = dimapDefault


type Unit :: CAT ()
data Unit a b where
  Unit :: Unit '() '()
type instance (~>) = Unit
instance Category Unit where
  type Ob a = a ~ '()
  id = Unit
  Unit . Unit = Unit
instance Profunctor Unit where
  dimap = dimapDefault
  r \\ Unit = r


type Zero :: CAT Void
data Zero a b
class IsVoid (a :: Void) where voidId :: Zero a a
type instance (~>) = Zero
instance Category Zero where
  type Ob a = IsVoid a
  id = voidId
  (.) = \case
instance Profunctor Zero where
  dimap = dimapDefault
  _ \\ x = case x of


type Fst :: (a, b) -> a
type family Fst a where Fst '(a, b) = a
type Snd :: (a, b) -> b
type family Snd a where Snd '(a, b) = b

type (:**:) :: CAT k1 -> CAT k2 -> CAT (k1, k2)
data (c :**: d) a b where
  (:**:) :: c a1 b1 -> d a2 b2 -> (c :**: d) '(a1, a2) '(b1, b2)
type instance (~>) = (~>) :**: (~>)
instance (Category c, Category d) => Category (c :**: d) where
  type Ob a = (a ~ '(Fst a, Snd a), Ob (Fst a), Ob (Snd a))
  id = id :**: id
  (f1 :**: f2) . (g1 :**: g2) = (f1 . g1) :**: (f2 . g2)
instance (Category c, Category d) => Profunctor (c :**: d) where
  dimap = dimapDefault
  r \\ (f :**: g) = r \\ f \\ g


type (:++:) :: CAT k1 -> CAT k2 -> CAT (P.Either k1 k2)
data (c :++: d) a b where
  L :: c a b -> (c :++: d) ('Left a) ('Left b)
  R :: d a b -> (c :++: d) ('Right a) ('Right b)
class IsEither (a :: Either k1 k2) where
  eitherId :: ((~>) :++: (~>)) a a
instance (Ob a, Category ((~>) :: CAT k)) => IsEither ('Left (a :: k)) where eitherId = L id
instance (Ob a, Category ((~>) :: CAT k)) => IsEither ('Right (a :: k)) where eitherId = R id
type instance (~>) = (~>) :++: (~>)
instance (Category c, Category d) => Category (c :++: d) where
  type Ob a = IsEither a
  id = eitherId
  L f . L g = L (f . g)
  R f . R g = R (f . g)
instance (Category c, Category d) => Profunctor (c :++: d) where
  dimap = dimapDefault
  r \\ L f = r \\ f
  r \\ R f = r \\ f


type f .~> g = forall a. Ob a => f a ~> g a

type Nat :: CAT (k1 -> k2)
data Nat f g where
  Nat :: (Functor f, Functor g)
      => { getNat :: f .~> g }
      -> Nat f g
type instance (~>) = Nat :: CAT (k1 -> Type)
instance Category (Nat :: CAT (k1 -> Type)) where
  type Ob f = Functor f
  id = n where
    n :: forall f. Functor f => Nat f f
    n = Nat (map @f id)
  Nat f . Nat g = Nat (f . g)
instance Profunctor (Nat :: CAT (k1 -> Type)) where
  dimap f g h = g . h . f
  r \\ Nat{} = r
type instance (~>) = Nat :: CAT (k1 -> k2 -> k3 -> Type)
instance Category (Nat :: CAT (k1 -> k2 -> k3 -> Type)) where
  type Ob f = Functor f
  id = n where
    n :: forall f. Functor f => Nat f f
    n = Nat (map @f id)
  Nat f . Nat g = Nat (f . g)
instance Profunctor (Nat :: CAT (k1 -> k2 -> k3 -> Type)) where
  dimap f g h = g . h . f
  r \\ Nat{} = r
type instance (~>) = Nat :: CAT (k1 -> k2 -> k3 -> k4 -> Type)
instance Category (Nat :: CAT (k1 -> k2 -> k3 -> k4 -> Type)) where
  type Ob f = Functor f
  id = n where
    n :: forall f. Functor f => Nat f f
    n = Nat (map @f id)
  Nat f . Nat g = Nat (f . g)
instance Profunctor (Nat :: CAT (k1 -> k2 -> k3 -> k4 -> Type)) where
  dimap f g h = g . h . f
  r \\ Nat{} = r

type p :~> q = forall a b. p a b ~> q a b

type Prof :: CAT (PRO k1 k2)
data Prof p q where
  Prof :: (Profunctor p, Profunctor q)
      => { getProf :: p :~> q }
      -> Prof p q
type instance (~>) = Prof
instance Category Prof where
  type Ob p = Profunctor p
  id = Prof id
  Prof f . Prof g = Prof (f . g)
instance Profunctor Prof where
  dimap f g h = g . h . f
  r \\ Prof{} = r

type Functor :: forall {k1} {k2}. (k1 -> k2) -> Constraint
class (CategoryOf k1, CategoryOf k2) => Functor (f :: k1 -> k2) where
  map :: a ~> b -> f a ~> f b

withFCod' :: forall f a r. (Functor f, Ob a) => (Ob (f a) => Obj (f a) -> r) -> r
withFCod' r = let o = map @f (obj @a) in r o \\ o

withFCod :: forall f a r. (Functor f, Ob a) => (Ob (f a) => r) -> r
withFCod r = withFCod' @f @a (const r)


newtype OP k = OP k
type family UNOP (a :: OP k) :: k where UNOP ('OP k) = k
type Op :: PRO k1 k2 -> PRO (OP k2) (OP k1)
data Op c a b where
  Op :: { getOp :: c b a } -> Op c ('OP a) ('OP b)
instance Profunctor p => Functor (Op p a) where
  map (Op f) (Op p) = Op (lmap f p)
instance Profunctor p => Profunctor (Op p) where
  dimap (Op l) (Op r) = Op . dimap r l . getOp
  r \\ Op f = r \\ f
type instance (~>) = Op (~>)
instance Category c => Category (Op c) where
  type Ob a = (a ~ 'OP (UNOP a), Ob (UNOP a))
  id = Op id
  Op f . Op g = Op (g . f)



type Costar :: (k1 -> k2) -> PRO k1 k2
data Costar f a b where
  Costar :: Ob a => { getCostar :: f a ~> b } -> Costar f a b
instance Functor f => Profunctor (Costar f) where
  dimap l r (Costar f) = Costar (r . f . map l) \\ l
  r \\ Costar f = r \\ f

type Star :: (k1 -> k2) -> PRO k2 k1
data Star f a b where
  Star :: Ob b => { getStar :: a ~> f b } -> Star f a b
instance Functor f => Profunctor (Star f) where
  dimap l r (Star f) = Star (map @f r . f . l) \\ r
  r \\ Star f = r \\ f

type Distar :: (k1 -> k2) -> PRO k1 k1
data Distar f a b where
  Distar :: (Ob a, Ob b) => { getDistar :: f a ~> f b } -> Distar f a b
instance Functor f => Profunctor (Distar f) where
  dimap l r (Distar f) = Distar (map r . f . map l) \\ l \\ r
  r \\ Distar{} = r


type Id :: CAT k
newtype Id a b = Id { getId :: a ~> b }
instance CategoryOf k => Profunctor (Id :: CAT k) where
  dimap l r (Id f) = Id (r . f . l)
  r \\ Id f = r \\ f

type (:.:) :: (k2 -> k3 -> Type) -> (k1 -> k2 -> Type) -> k1 -> k3 -> Type
data (p :.: q) a c where
  (:.:) :: p b c -> q a b -> (p :.: q) a c
instance (Profunctor p, Profunctor q) => Profunctor (p :.: q) where
  dimap l r (p :.: q) = rmap r p :.: lmap l q
  r \\ p :.: q = r \\ p \\ q
instance Profunctor p => Functor ((:.:) p) where
  map (Prof n) = Prof \(p :.: q) -> p :.: n q
instance Functor (:.:) where
  map (Prof n) = Nat $ Prof \(p :.: q) -> n p :.: q


type Rift :: OP (PRO k2 k3) -> PRO k1 k3 -> PRO k1 k2
data Rift j p a b where
  Rift :: (Ob a, Ob b) => { getRift :: forall x. Ob x => j b x -> p a x } -> Rift ('OP j) p a b
runRift :: Profunctor j => j b x -> Rift ('OP j) p a b -> p a x
runRift j (Rift k) = k j \\ j
instance (Profunctor p, Profunctor j) => Profunctor (Rift ('OP j) p) where
  dimap l r (Rift k) = r // l // Rift $ lmap l . k . lmap r
  r \\ Rift{} = r
instance Profunctor j => Functor (Rift ('OP j)) where
  map (Prof n) = Prof \(Rift k) -> Rift $ n . k
instance Functor Rift where
  map (Op (Prof n)) = Nat $ Prof \(Rift k) -> Rift $ k . n

type Ran :: OP (PRO k3 k1) -> PRO k3 k2 -> PRO k1 k2
data Ran j p a b where
  Ran :: (Ob a, Ob b) => { getRan :: forall x. Ob x => j x a -> p x b } -> Ran ('OP j) p a b
runRan :: Profunctor j => j x a -> Ran ('OP j) p a b -> p x b
runRan j (Ran k) = k j \\ j
instance (Profunctor p, Profunctor j) => Profunctor (Ran ('OP j) p) where
  dimap l r (Ran k) = l // r // Ran $ rmap r . k . rmap l
  r \\ Ran{} = r
instance Profunctor j => Functor (Ran ('OP j)) where
  map (Prof n) = Prof \(Ran k) -> Ran $ n . k
instance Functor Ran where
  map (Op (Prof n)) = Nat $ Prof \(Ran k) -> Ran $ k . n

type p <| j = Rift ('OP j) p
type j |> p = Ran ('OP j) p


type Adjunction :: forall {k1} {k2}. (k2 -> k1 -> Type) -> (k1 -> k2 -> Type) -> Constraint
class (Profunctor p, Profunctor q) => Adjunction (p :: k2 -> k1 -> Type) q where
  unit :: Ob a => (p :.: q) a a -- (~>) :~> p :.: q
  counit :: q :.: p :~> (~>)

leftAdjunct
  :: forall l r a b. (Adjunction (Star l) (Star r), Functor r)
  => Ob a => (l a ~> b) -> (a ~> r b)
leftAdjunct f = case unit @(Star l) @(Star r) @a of Star l :.: Star r -> map (f . l) . r

rightAdjunct
  :: forall l r a b. (Adjunction (Star l) (Star r), Functor l)
  => Ob b => (a ~> r b) -> (l a ~> b)
rightAdjunct f = counit (Star f :.: Star (map id)) \\ f

unitFromStarUnit
  :: forall l r a. (Functor l, Ob a) => (a ~> r (l a)) -> (Star l :.: Star r) a a
unitFromStarUnit f = withFCod' @l @a \la -> Star la :.: Star f

counitFromStarCounit
  :: Functor l => (forall c. Ob c => l (r c) ~> c) -> (Star r :.: Star l) a b -> (a ~> b)
counitFromStarCounit f (Star r :.: Star l) = f . map r . l


instance Functor f => Adjunction (Star f) (Costar f) where
  unit = Star (map id) :.: Costar (map id)
  counit (Costar f :.: Star g) = f . g

instance (Functor f, Functor g, Adjunction (Star f) (Star g)) => Adjunction (Costar f) (Costar g) where
  unit :: forall a. (Ob a) => (Costar f :.: Costar g) a a
  unit = withFCod' @g @a \ga -> Costar (counit (Star ga :.: Star (map id))) :.: Costar id
  counit :: forall a b. (Costar g :.: Costar f) a b -> a ~> b
  counit (Costar g :.: Costar f) = case unit @(Star f) @(Star g) @a of Star f' :.: Star g' -> g . map (f . f') . g'

instance CategoryOf k => Adjunction (Id :: CAT k) Id where
  unit = Id id :.: Id id
  counit (Id f :.: Id g) = f . g

instance (Adjunction l1 r1, Adjunction l2 r2) => Adjunction (l2 :.: l1) (r1 :.: r2) where
  unit :: forall a. Ob a => ((l2 :.: l1) :.: (r1 :.: r2)) a a
  unit = case unit @l2 @r2 @a of
    l2 :.: r2 -> l2 // case unit @l1 @r1 of
      l1 :.: r1 -> (l2 :.: l1) :.: (r1 :.: r2)
  counit ((r1 :.: r2) :.: (l2 :.: l1)) = counit (r1 :.: l1) . counit (r2 :.: l2)

instance Functor ((,) a) where
  map = fmap
instance Functor ((->) a) where
  map = fmap
instance Adjunction (Star ((,) a)) (Star ((->) a)) where
  unit = unitFromStarUnit \a b -> (b, a)
  counit = counitFromStarCounit \(a, f) -> f a


newtype Precompose j p a b = Precompose { getPrecompose :: (p :.: j) a b }
  deriving newtype Profunctor
instance Profunctor j => Functor (Precompose j) where
  map f = f // Prof \(Precompose pj) -> Precompose $ getProf (getNat (map f)) pj

instance Profunctor j => Adjunction (Star (Precompose j)) (Star (Ran ('OP j))) where
  unit = unitFromStarUnit $ Prof \p -> p // Ran \j -> Precompose (p :.: j)
  counit = counitFromStarCounit $ Prof \(Precompose (r :.: j)) -> runRan j r

instance Profunctor j => Adjunction (Star ((:.:) j)) (Star (Rift ('OP j))) where
  unit = unitFromStarUnit $ Prof \a -> Rift (:.: a) \\ a
  counit = counitFromStarCounit $ Prof \(j :.: r) -> runRift j r



class Profunctor p => Promonad p where
  unit' :: Ob a => p a a
  mult :: p :.: p :~> p

newtype TAG (p :: CAT k) = TAG { unTAG :: k }
-- can't use unTAG at the type level
type family UNTAG (a :: TAG (p :: CAT k)) :: k where UNTAG ('TAG k) = k
type Tag :: CAT (TAG p)
data Tag (a :: TAG p) b where
  Tag :: p a b -> Tag ('TAG a :: TAG p) ('TAG b)
type instance (~>) = Tag
instance Promonad p => Profunctor (Tag :: CAT (TAG p)) where
  dimap = dimapDefault
  r \\ Tag p = r \\ p
instance Promonad p => Category (Tag :: CAT (TAG p)) where
  type Ob a = (a ~ 'TAG (UNTAG a), Ob (UNTAG a))
  id = Tag (unit' @p)
  Tag f . Tag g = Tag (mult @p (f :.: g))



newtype SUB (ob :: OB k) = SUB { unSUB :: k }
type family UNSUB (a :: SUB (ob :: OB k)) :: k where UNSUB ('SUB k) = k
type Sub :: CAT (SUB ob)
data Sub a b where
  Sub :: (ob a, ob b) => a ~> b -> Sub ('SUB a :: SUB ob) ('SUB b)
type instance (~>) = Sub
instance Profunctor ((~>) :: CAT k) => Profunctor (Sub :: CAT (SUB (ob :: OB k))) where
  dimap = dimapDefault
  r \\ Sub p = r \\ p
instance Category ((~>) :: CAT k) => Category (Sub :: CAT (SUB (ob :: OB k))) where
  type Ob (a :: SUB ob) = (a ~ 'SUB (UNSUB a), Ob (UNSUB a), ob (UNSUB a))
  id = Sub id
  Sub f . Sub g = Sub (f . g)


type List :: PRO Type (SUB P.Monoid)
data List a b where
  List :: P.Monoid b => ([a] -> b) -> List a ('SUB b)
instance Profunctor List where
  dimap l (Sub r) (List f) = List (r . f . P.map l)
  r \\ List{} = r

type Forget :: forall (ob :: OB k) -> PRO (SUB ob) k
data Forget ob a b where
  Forget :: ob a => a ~> b -> Forget ob ('SUB a) b
instance Category ((~>) :: CAT k) => Profunctor (Forget (ob :: OB k)) where
  dimap (Sub l) r (Forget f) = Forget (r . f . l)
  r \\ Forget f = r \\ f

instance Adjunction List (Forget P.Monoid) where
  unit = List P.mconcat :.: Forget id
  counit (Forget f :.: List g) = f . g . P.pure


newtype State s a b = State { getState :: (s, a) -> (s, b) }
instance Profunctor (State s) where
  dimap l r (State f) = State $ fmap r . f . fmap l
instance Promonad (State s) where
  unit' = State id
  mult (State f :.: State g) = State (f . g)

newtype Reader r a b = Reader { getReader :: (r, a) -> b }
instance Profunctor (Reader r) where
  dimap l r (Reader f) = Reader $ r . f . fmap l
instance Promonad (Reader r) where
  unit' = Reader snd
  mult (Reader f :.: Reader g) = Reader \(r, a) -> f (r, g (r, a))

newtype Writer m a b = Writer { getWriter :: a -> (m, b) }
instance Profunctor (Writer m) where
  dimap l r (Writer f) = Writer $ fmap r . f . l
instance P.Monoid m => Promonad (Writer m) where
  unit' = Writer $ (,) P.mempty
  mult (Writer f :.: Writer g) = Writer \a -> case g a of (m1, b) -> case f b of (m2, c) -> (m1 P.<> m2, c)

instance Adjunction p q => Promonad (p :.: q) where
  unit' = unit
  mult ((p :.: q) :.: (p' :.: q')) = p :.: rmap (counit (q :.: p')) q'


type (.:.) :: (k2 -> Type) -> (k1 -> k2) -> k1 -> Type
newtype (f .:. g) a = Comp { getComp :: f (g a) }
instance (Functor f, Functor g) => Functor (f .:. g) where
  map f = Comp . map (map f) . getComp
instance (Functor l, Functor r, Adjunction (Star l) (Star r)) => Promonad (Star (r .:. l)) where
  unit' :: forall a. Ob a => Star (r .:. l) a a
  unit' = case unit @(Star l) @(Star r) @a of Star l :.: Star r -> Star (Comp . map l . r)
  mult :: forall a b. (Ob a, Ob b) => (Star (r .:. l) :.: Star (r .:. l)) a b -> Star (r .:. l) a b
  mult (Star f :.: Star g) = withFCod @l @b $ withFCod' @r @(l b) \rlb -> withFCod' @l @(r (l b)) \lrlb ->
    Star $ Comp . map (counit @(Star l) @(Star r) (Star rlb :.: Star lrlb)) . getComp . map (getComp . f) . g
instance (Functor l, Functor r, Adjunction (Star l) (Star r)) => Promonad (Costar (l .:. r)) where
  unit' :: forall a. Ob a => Costar (l .:. r) a a
  unit' = withFCod' @r @a \ra -> Costar $ counit (Star ra :.: Star id) . getComp
  mult :: forall a b. (Ob a, Ob b) => (Costar (l .:. r) :.: Costar (l .:. r)) a b -> Costar (l .:. r) a b
  mult (Costar f :.: Costar g) = withFCod @r @a $ case unit @(Star l) @(Star r) @(r a) of Star l :.: Star r -> Costar (f . map (g . Comp) . Comp . map (map l . r) . getComp)



type Collage :: PRO k1 k2 -> PRO (Either k1 k2) (Either k1 k2)
data Collage p a b where
  InL :: (a ~> b) -> Collage p ('Left a) ('Left b)
  InR :: (a ~> b) -> Collage p ('Right a) ('Right b)
  L2R :: p a b -> Collage p ('Left a) ('Right b)
instance Profunctor p => Profunctor (Collage p) where
  dimap (L l) (L r) (InL f) = InL $ dimap l r f
  dimap (R l) (R r) (InR f) = InR $ dimap l r f
  dimap (L l) (R r) (L2R p) = L2R $ dimap l r p
  dimap (R _) (L _) f = case f of
  r \\ InL f = r \\ f
  r \\ InR f = r \\ f
  r \\ L2R p = r \\ p
instance Profunctor p => Promonad (Collage p) where
  unit' :: forall a. Ob a => Collage p a a
  unit' = case eitherId @_ @_ @a of L f -> InL f; R f -> InR f
  mult (InL f :.: InL g) = InL (f . g)
  mult (L2R p :.: InL g) = L2R (lmap g p)
  mult (InR f :.: L2R p) = L2R (rmap f p)
  mult (InR f :.: InR g) = InR (f . g)
instance Functor Collage where
  map (Prof n) = Prof \case
    InL l -> InL l
    InR r -> InR r
    L2R p -> L2R (n p)


infixr 4 :|
type FreeCat :: (k -> k -> Type) -> CAT k
data FreeCat g a b where
  FreeId :: FreeCat g a a
  (:|) :: g a b -> FreeCat g b c -> FreeCat g a c
instance (Category (FreeCat g), VacuusOb k) => Profunctor (FreeCat (g :: k -> k -> Type)) where
  dimap = dimapDefault
class Rewrite g where
  rewriteAfterCons :: FreeCat g :~> FreeCat g
instance (Rewrite g, Category (FreeCat g), VacuusOb k) => Promonad (FreeCat (g :: k -> k -> Type)) where
  unit' = id
  mult (FreeId :.: a) = a
  mult (a :.: FreeId) = a
  mult (a :.: (g :| b)) = rewriteAfterCons (g :| mult (a :.: b))


type Yoneda :: (k1 -> k2 -> Type) -> PRO k1 k2
data Yoneda p a b where
  Yoneda :: (Ob a, Ob b) => { getYoneda :: forall c d. (c ~> a) -> (b ~> d) -> p c d } -> Yoneda p a b
instance (CategoryOf k1, CategoryOf k2) => Profunctor (Yoneda (p :: PRO k1 k2)) where
  dimap l r (Yoneda k) = l // r // Yoneda \ca bd -> k (l . ca) (bd . r)
  r \\ Yoneda{} = r
freePro :: (CategoryOf k1, CategoryOf k2, Ob a, Ob b) => Yoneda (p :: k1 -> k2 -> Type) a b -> p a b
freePro (Yoneda k) = k id id




type Representable :: forall {k1} {k2}. PRO k1 k2 -> Constraint
class Profunctor p => Representable (p :: PRO k1 k2) where
  type p % (a :: k2) :: k1
  index :: p a b -> a ~> p % b
  tabulate :: Ob b => (a ~> p % b) -> p a b
  repMap :: (a ~> b) -> p % a ~> p % b

withRepCod :: forall p a r. (Representable p, Ob a) => (Ob (p % a) => r) -> r
withRepCod r = r \\ repMap @p (obj @a)

instance Functor f => Representable (Star f) where
  type Star f % a = f a
  index = getStar
  tabulate = Star
  repMap = map

instance CategoryOf k => Representable (Id :: CAT k) where
  type Id % a = a
  index = getId
  tabulate = Id
  repMap = id

instance (Representable p, Representable q) => Representable (p :.: q) where
  type (p :.: q) % a = q % (p % a)
  index (p :.: q) = repMap @q (index p) . index q
  tabulate :: forall a b. Ob b => (a ~> ((p :.: q) % b)) -> (:.:) p q a b
  tabulate f = withRepCod @p @b $ tabulate id :.: tabulate f
  repMap f = repMap @q (repMap @p f)


type Corepresentable :: forall {k1} {k2}. PRO k1 k2 -> Constraint
class Profunctor p => Corepresentable (p :: PRO k1 k2) where
  type p %% (a :: k1) :: k2
  coindex :: p a b -> p %% a ~> b
  cotabulate :: Ob a => (p %% a ~> b) -> p a b
  corepMap :: (a ~> b) -> p %% a ~> p %% b

withCorepCod :: forall p a r. (Corepresentable p, Ob a) => (Ob (p %% a) => r) -> r
withCorepCod r = r \\ corepMap @p (obj @a)

instance Functor f => Corepresentable (Costar f) where
  type Costar f %% a = f a
  coindex = getCostar
  cotabulate = Costar
  corepMap = map

instance CategoryOf k => Corepresentable (Id :: CAT k) where
  type Id %% a = a
  coindex = getId
  cotabulate = Id
  corepMap = id

instance (Corepresentable p, Corepresentable q) => Corepresentable (p :.: q) where
  type (p :.: q) %% a = p %% (q %% a)
  coindex (p :.: q) = corepMap @q (coindex p) . coindex q
  cotabulate :: forall a b. Ob a => (((p :.: q) %% a) ~> b) -> (:.:) p q a b
  cotabulate f = withCorepCod @q @a $ cotabulate f :.: cotabulate id
  corepMap f = corepMap @p (corepMap @q f)



-- profunctor-weighted limits
type HasLimits :: PRO a i -> Type -> Constraint
class HasLimits (j :: PRO a i) k where
  -- Limit has to be Representable too
  type Limit (j :: PRO a i) (d :: PRO k i) :: PRO k a
  limit :: Representable (d :: PRO k i) => Limit j d :~> d <| j
  limitInv :: Representable (d :: PRO k i) => d <| j :~> Limit j d

type HasColimits :: PRO i a -> Type -> Constraint
class HasColimits (j :: PRO i a) k where
  -- Colimit has to be Corepresentable too
  type Colimit (j :: PRO i a) (d :: PRO i k) :: PRO a k
  colimit :: Corepresentable (d :: PRO i k) => Colimit j d :~> j |> d
  colimitInv :: Corepresentable (d :: PRO i k) => j |> d :~> Colimit j d


class (CategoryOf k, Ob (TerminalObject :: k)) => HasTerminalObject k where
  type TerminalObject :: k
  terminate' :: Obj (a :: k) -> a ~> TerminalObject

terminate :: forall {k} a. (HasTerminalObject k, Ob (a :: k)) => a ~> TerminalObject
terminate = terminate' (obj @a)

type El a = TerminalObject ~> a

instance HasTerminalObject Type where
  type TerminalObject = ()
  terminate' _ _ = ()

instance HasTerminalObject () where
  type TerminalObject = '()
  terminate' Unit = Unit

instance HasInitialObject k => HasTerminalObject (OP k) where
  type TerminalObject = 'OP InitialObject
  terminate' (Op a) = Op (initiate' a)


class (CategoryOf k, Ob (InitialObject :: k)) => HasInitialObject k where
  type InitialObject :: k
  initiate' :: Obj (a :: k) -> InitialObject ~> a

initiate :: forall {k} a. (HasInitialObject k, Ob (a :: k)) => InitialObject ~> a
initiate = initiate' (obj @a)

instance HasInitialObject Type where
  type InitialObject = Void
  initiate' _ = absurd

instance HasInitialObject () where
  type InitialObject = '()
  initiate' Unit = Unit

instance HasTerminalObject k => HasInitialObject (OP k) where
  type InitialObject = 'OP TerminalObject
  initiate' (Op a) = Op (terminate' a)



class CategoryOf k => HasBinaryProducts k where
  type (a :: k) && (b :: k) :: k
  fst' :: Obj (a :: k) -> Obj b -> a && b ~> a
  snd' :: Obj (a :: k) -> Obj b -> a && b ~> b
  (&&&) :: (a :: k) ~> x -> a ~> y -> a ~> x && y
  (***) :: forall a b x y. (a :: k) ~> x -> b ~> y -> a && b ~> x && y
  l *** r = (l . fst @a @b) &&& (r . snd @a @b) \\ l \\ r

fst :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> a
fst = fst' (obj @a) (obj @b)
snd :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, Ob a, Ob b) => (a && b) ~> b
snd = snd' (obj @a) (obj @b)

type HasProducts k = (HasTerminalObject k, HasBinaryProducts k)

instance HasBinaryProducts Type where
  type a && b = (a, b)
  fst' _ _ = P.fst
  snd' _ _ = P.snd
  f &&& g = \a -> (f a, g a)

instance HasBinaryProducts () where
  type '() && '() = '()
  fst' Unit Unit = Unit
  snd' Unit Unit = Unit
  Unit &&& Unit = Unit

instance HasBinaryCoproducts k => HasBinaryProducts (OP k) where
  type 'OP a && 'OP b = 'OP (a || b)
  fst' (Op a) (Op b) = Op (left' a b)
  snd' (Op a) (Op b) = Op (right' a b)
  Op a &&& Op b = Op (a ||| b)

type ProductFunctor :: PRO k (k, k)
data ProductFunctor a b where
  ProductFunctor :: (Ob c, Ob d) => a ~> (c && d) -> ProductFunctor a '(c, d)
instance HasBinaryProducts k => Profunctor (ProductFunctor :: PRO k (k, k)) where
  dimap l (r1 :**: r2) (ProductFunctor f) = r1 // r2 // ProductFunctor ((r1 *** r2) . f . l)
  r \\ ProductFunctor f = r \\ f
instance HasBinaryProducts k => Representable (ProductFunctor :: PRO k (k, k)) where
  type ProductFunctor % '(a, b) = a && b
  index (ProductFunctor f) = f
  tabulate f = ProductFunctor f
  repMap (f :**: g) = f *** g



class CategoryOf k => HasBinaryCoproducts k where
  type (a :: k) || (b :: k) :: k
  left' :: Obj (a :: k) -> Obj b -> a ~> (a || b)
  right' :: Obj (a :: k) -> Obj b -> b ~> (a || b)
  (|||) :: (x :: k) ~> a -> y ~> a -> (x || y) ~> a
  (+++) :: forall a b x y. (a :: k) ~> x -> b ~> y -> a || b ~> x || y
  l +++ r = (left @x @y . l) ||| (right @x @y . r) \\ l \\ r

left :: forall {k} (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => a ~> (a || b)
left = left' (obj @a) (obj @b)
right :: forall {k} (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => b ~> (a || b)
right = right' (obj @a) (obj @b)

type HasCoproducts k = (HasInitialObject k, HasBinaryCoproducts k)

instance HasBinaryCoproducts Type where
  type a || b = Either a b
  left' _ _ = Left
  right' _ _ = Right
  (|||) = either

instance HasBinaryCoproducts () where
  type '() || '() = '()
  left' Unit Unit = Unit
  right' Unit Unit = Unit
  Unit ||| Unit = Unit

instance HasBinaryProducts k => HasBinaryCoproducts (OP k) where
  type 'OP a || 'OP b = 'OP (a && b)
  left' (Op a) (Op b) = Op (fst' a b)
  right' (Op a) (Op b) = Op (snd' a b)
  Op a ||| Op b = Op (a &&& b)

type CoproductFunctor :: PRO k (k, k)
data CoproductFunctor a b where
  CoproductFunctor :: (Ob c, Ob d) => a ~> (c || d) -> CoproductFunctor a '(c, d)
instance HasBinaryCoproducts k => Profunctor (CoproductFunctor :: PRO k (k, k)) where
  dimap l (r1 :**: r2) (CoproductFunctor f) = CoproductFunctor ((r1 +++ r2) . f . l) \\ r1 \\ r2
  r \\ CoproductFunctor f = r \\ f
instance HasBinaryCoproducts k => Representable (CoproductFunctor :: PRO k (k, k)) where
  type CoproductFunctor % '(a, b) = a || b
  index (CoproductFunctor f) = f
  tabulate f = CoproductFunctor f
  repMap (f :**: g) = f +++ g


type Unweighted :: PRO i j
data Unweighted a b where
  Unweighted :: Obj a -> Obj b -> Unweighted a b
instance (CategoryOf i, CategoryOf j) => Profunctor (Unweighted :: PRO i j) where
  dimap l r Unweighted{} = Unweighted id id \\ l \\ r
  r \\ Unweighted a b = r \\ a \\ b

type TerminalLimit :: PRO k Void -> PRO k ()
data TerminalLimit d a b where
  TerminalLimit :: forall d a. a ~> TerminalObject -> TerminalLimit d a '()
instance HasTerminalObject k => HasLimits (Unweighted :: PRO () Void) k where
  type Limit Unweighted d = TerminalLimit d
  limit (TerminalLimit @d f) = f // Rift \(Unweighted _ o) -> tabulate $ case o of . f
  limitInv Rift{} = TerminalLimit terminate

type ProductLimit :: PRO k (Either () ()) -> PRO k ()
data ProductLimit d a b where
  ProductLimit :: forall d a. a ~> ((d % Left '()) && (d % Right '())) -> ProductLimit d a '()
instance CategoryOf k => Profunctor (ProductLimit d :: PRO k ()) where
  dimap l Unit (ProductLimit f) = ProductLimit (f . l) \\ l
  r \\ (ProductLimit f) = r \\ f
instance (HasBinaryProducts k, Representable d) => Representable (ProductLimit d :: PRO k ()) where
  type ProductLimit d % '() = (d % Left '()) && (d % Right '())
  index (ProductLimit f) = f
  tabulate f = ProductLimit f
  repMap Unit = repMap @d (L Unit) *** repMap @d (R Unit)
instance HasBinaryProducts k => HasLimits (Unweighted :: PRO () (Either () ())) k where
  type Limit Unweighted d = ProductLimit d
  limit (ProductLimit @d f) = f // Rift \(Unweighted _ o) -> tabulate $ choose @_ @d o . f
  limitInv (Rift k) =
    let l = k (Unweighted Unit (L Unit))
        r = k (Unweighted Unit (R Unit))
    in ProductLimit $ index l &&& index r

choose
  :: forall k (d :: PRO k (Either () ())) b
  .  (HasBinaryProducts k, Representable d)
  => Obj b -> ((d % Left '()) && (d % Right '())) ~> (d % b)
choose b = withRepCod @d @(Left '()) $ withRepCod @d @(Right '()) $ case b of
  (L Unit) -> fst @(d % Left '()) @(d % Right '())
  (R Unit) -> snd @(d % Left '()) @(d % Right '())



type InitialLimit :: PRO Void k -> PRO () k
data InitialLimit d a b where
  InitialLimit :: forall d a. Ob a => InitialObject ~> a -> InitialLimit d '() a
instance HasInitialObject k => HasColimits (Unweighted :: PRO Void ()) k where
  type Colimit Unweighted d = InitialLimit d
  colimit (InitialLimit @d f) = Ran \(Unweighted o _) -> cotabulate $ f . case o of
  colimitInv Ran{} = InitialLimit initiate

type CoproductColimit :: PRO (Either () ()) k -> PRO () k
data CoproductColimit d a b where
  CoproductColimit :: forall d b. Ob b => ((d %% Left '()) || (d %% Right '())) ~> b -> CoproductColimit d '() b
instance HasBinaryCoproducts k => HasColimits (Unweighted :: PRO (Either () ()) ()) k where
  type Colimit Unweighted d = CoproductColimit d
  colimit (CoproductColimit @d f) = Ran \(Unweighted o _) -> cotabulate $ f . cochoose @_ @d o
  colimitInv (Ran k) =
    let l = k (Unweighted (L Unit) Unit)
        r = k (Unweighted (R Unit) Unit)
    in CoproductColimit $ coindex l ||| coindex r

cochoose
  :: forall k (d :: PRO (Either () ()) k) b
  .  (HasBinaryCoproducts k, Corepresentable d)
  => Obj b -> (d %% b) ~> ((d %% Left '()) || (d %% Right '()))
cochoose b = withCorepCod @d @(Left '()) $ withCorepCod @d @(Right '()) $ case b of
  (L Unit) -> left @(d %% Left '()) @(d %% Right '())
  (R Unit) -> right @(d %% Left '()) @(d %% Right '())


class (CategoryOf k, Ob ((a :: k) ~~> b)) => ExpOb k a b where expId :: Obj (a ~~> b)
instance (CategoryOf k, Ob ((a :: k) ~~> b)) => ExpOb k a b where expId = obj @(a ~~> b)

class (HasProducts k, forall (a ::k) (b :: k). (Ob a, Ob b) => ExpOb k a b) => CartesianClosed k where
  type (a :: k) ~~> (b :: k) :: k
  curry' :: Obj (a :: k) -> Obj b -> a && b ~> c -> a ~> b ~~> c
  uncurry' :: Obj (b :: k) -> Obj c -> a ~> b ~~> c -> a && b ~> c
  (^^^) :: forall (a :: k) b x y. b ~> y -> x ~> a -> a ~~> b ~> x ~~> y
  by ^^^ xa = xa // by //
    let xb = comp @x @a @b . (expId @k @a @b *** mkExponential xa) . rightUnitorInv @ProductFunctor @(a ~~> b)
    in comp @x @b @y . (mkExponential by *** xb) . leftUnitorInv @ProductFunctor @(a ~~> b)

curry :: forall {k} (a :: k) b c. (CartesianClosed k, Ob a, Ob b) => a && b ~> c -> a ~> b ~~> c
curry = curry' (obj @a) (obj @b)

uncurry :: forall {k} (a :: k) b c. (CartesianClosed k, Ob b, Ob c) => a ~> b ~~> c -> a && b ~> c
uncurry = uncurry' (obj @b) (obj @c)

comp :: forall {k} (a :: k) b c. (CartesianClosed k, Ob a, Ob b, Ob c) => (b ~~> c) && (a ~~> b) ~> a ~~> c
comp = curry @_ @a @c (eval @b @c . (expId @k @b @c *** eval @a @b) . associator @ProductFunctor @(b ~~> c) @(a ~~> b) @a)
  \\ (expId @k @b @c *** expId @k @a @b)

mkExponential :: forall {k} a b. CartesianClosed k => (a :: k) ~> b -> El (a ~~> b)
mkExponential ab = curry @_ @a (ab . leftUnitor @ProductFunctor @a) \\ ab

eval :: forall {k} a b. (CartesianClosed k, Ob a, Ob b) => ((a :: k) ~~> b) && a ~> b
eval = uncurry @_ @a @b (expId @k @a @b)


instance CartesianClosed Type where
  type a ~~> b = a -> b
  curry' _ _ = P.curry
  uncurry' _ _ = P.uncurry

instance CartesianClosed () where
  type '() ~~> '() = '()
  curry' Unit Unit Unit = Unit
  uncurry' Unit Unit Unit = Unit

type ExponentialFunctor :: PRO k (OP k, k)
data ExponentialFunctor a b where
  ExponentialFunctor :: (Ob c, Ob d) => a ~> (c ~~> d) -> ExponentialFunctor a '( 'OP c, d )
instance CartesianClosed k => Profunctor (ExponentialFunctor :: PRO k (OP k, k)) where
  dimap l (Op r1 :**: r2) (ExponentialFunctor f) = ExponentialFunctor ((r2 ^^^ r1) . f . l) \\ r1 \\ r2
  r \\ ExponentialFunctor f = r \\ f
instance CartesianClosed k => Representable (ExponentialFunctor :: PRO k (OP k, k)) where
  type ExponentialFunctor % '( 'OP a, b ) = a ~~> b
  index (ExponentialFunctor f) = f
  tabulate f = ExponentialFunctor f
  repMap (Op f :**: g) = g ^^^ f



type Tensor :: forall {k}. PRO k (k, k) -> Constraint
class (Representable t, Ob @k (U t)) => Tensor (t :: PRO k (k, k)) where
  type U t :: k
  leftUnitor :: Ob a => t % '(U t, a) ~> a
  leftUnitorInv :: Ob a => a ~> t % '(U t, a)
  rightUnitor :: Ob a => t % '(a, U t) ~> a
  rightUnitorInv :: Ob a => a ~> t % '(a, U t)
  associator' :: Obj a -> Obj b -> Obj c -> t % '(t % '(a, b), c) ~> t % '(a, t % '(b, c))
  associatorInv' :: Obj a -> Obj b -> Obj c -> t % '(a, t % '(b, c)) ~> t % '(t % '(a, b), c)

associator
  :: forall {k} t a b c. (Ob (a :: k), Ob b, Ob c, Tensor (t :: PRO k (k, k)))
  => t % '(t % '(a, b), c) ~> t % '(a, t % '(b, c))
associator = associator' @t (obj @a) (obj @b) (obj @c)

associatorInv
  :: forall {k} t a b c. (Ob (a :: k), Ob b, Ob c, Tensor (t :: PRO k (k, k)))
  => t % '(a, t % '(b, c)) ~> t % '(t % '(a, b), c)
associatorInv = associatorInv' @t (obj @a) (obj @b) (obj @c)

instance HasProducts k => Tensor (ProductFunctor :: PRO k (k, k)) where
  type U (ProductFunctor :: PRO k (k, k)) = TerminalObject :: k
  leftUnitor :: forall a. Ob (a :: k) => (ProductFunctor % '(TerminalObject, a)) ~> a
  leftUnitor = snd @(TerminalObject :: k) @(a :: k)
  leftUnitorInv :: forall a. Ob (a :: k) => a ~> (ProductFunctor % '(TerminalObject, a))
  leftUnitorInv = terminate @a &&& obj @a
  rightUnitor :: forall a. Ob (a :: k) => (ProductFunctor % '(a, TerminalObject)) ~> a
  rightUnitor = fst @(a :: k) @(TerminalObject :: k)
  rightUnitorInv :: forall a. Ob (a :: k) => a ~> (ProductFunctor % '(a, TerminalObject))
  rightUnitorInv = obj @a &&& terminate @a
  associator' a b c = (fst' a b . fst' (a *** b) c) &&& (snd' a b *** c) \\ (a *** b)
  associatorInv' a b c = (a *** fst' b c) &&& (snd' b c . snd' a (b *** c)) \\ (a *** b)

instance HasCoproducts k => Tensor (CoproductFunctor :: PRO k (k, k)) where
  type U (CoproductFunctor :: PRO k (k, k)) = InitialObject :: k
  leftUnitor :: forall a. Ob (a :: k) => (CoproductFunctor % '(InitialObject, a)) ~> a
  leftUnitor = initiate @a ||| obj @a
  leftUnitorInv :: forall a. Ob (a :: k) => a ~> (CoproductFunctor % '(InitialObject, a))
  leftUnitorInv = right @(InitialObject :: k) @(a :: k)
  rightUnitor :: forall a. Ob (a :: k) => (CoproductFunctor % '(a, InitialObject)) ~> a
  rightUnitor = obj @a ||| initiate @a
  rightUnitorInv :: forall a. Ob (a :: k) => a ~> (CoproductFunctor % '(a, InitialObject))
  rightUnitorInv = left @(a :: k) @(InitialObject :: k)
  associator' a b c = (a +++ left' b c) ||| (right' a (b +++ c) . right' b c) \\ (a +++ b)
  associatorInv' a b c = (left' (a +++ b) c . left' a b) ||| (right' a b +++ c) \\ (a +++ b)


class Tensor t => Semigroup t m where
  mmult :: t % '(m, m) ~> m

class Semigroup t m => Monoid t m where
  munit :: U t ~> m


type Day :: PRO j (j, j) -> PRO k (k, k) -> BI (PRO j k)
data Day s t pq a b where
  Day :: p a b -> q c d -> e ~> s % '(a, c) -> t % '(b, d) ~> f -> Day s t '(p, q) e f
instance (Profunctor p, Profunctor q) => Profunctor (Day s t '(p, q)) where
  dimap l r (Day p q f g) = Day p q (f . l) (r . g)
  r \\ Day _ _ f g = r \\ f \\ g
instance Functor (Day s t) where
  map (Prof l :**: Prof r) = Prof $ \(Day p q f g) -> Day (l p) (r q) f g

type DayUnit :: PRO j (j, j) -> PRO k (k, k) -> PRO j k
data DayUnit s t a b where
  DayUnit :: a ~> U s -> U t ~> b -> DayUnit s t a b
instance (CategoryOf j, CategoryOf k) => Profunctor (DayUnit (s :: PRO j (j, j)) (t :: PRO k (k, k))) where
  dimap l r (DayUnit f g) = DayUnit (f . l) (r . g)
  r \\ DayUnit f g = r \\ f \\ g
instance (Tensor s, Tensor t) => Tensor (Star (Day s t)) where
  type U (Star (Day s t)) = DayUnit s t
  leftUnitor = Prof $ \(Day (DayUnit l r) q f g) ->
    dimap
      (leftUnitor @s . repMap @s (l :**: src q) . f)
      (g . repMap @t (r :**: tgt q) . leftUnitorInv @t)
      q
    \\ q
  leftUnitorInv = Prof $ \q -> Day (DayUnit id id) q (leftUnitorInv @s) (leftUnitor @t) \\ q
  rightUnitor = Prof $ \(Day p (DayUnit l r) f g) ->
    dimap
      (rightUnitor @s . repMap @s (src p :**: l) . f)
      (g . repMap @t (tgt p :**: r) . rightUnitorInv @t)
      p
    \\ p
  rightUnitorInv = Prof $ \p -> Day p (DayUnit id id) (rightUnitorInv @s) (rightUnitor @t) \\ p
  associator' Prof{} Prof{} Prof{} = Prof $ \(Day (Day p q f g) r h i) ->
    Day p (Day q r (repMap @s $ src q :**: src r) (repMap @t $ tgt q :**: tgt r))
      (associator' @s (src p) (src q) (src r) . repMap @s (f :**: src r) . h)
      (i . repMap @t (g :**: tgt r) . associatorInv' @t (tgt p) (tgt q) (tgt r))
  associatorInv' Prof{} Prof{} Prof{} = Prof $ \(Day p (Day q r f g) h i) ->
    Day (Day p q (repMap @s $ src p :**: src q) (repMap @t $ tgt p :**: tgt q)) r
      (associatorInv' @s (src p) (src q) (src r) . repMap @s (src p :**: f) . h)
      (i . repMap @t (tgt p :**: g) . associator' @t (tgt p) (tgt q) (tgt r))


type Applicative :: forall {k1} {k2}. (k1 -> k2) -> Constraint
class (HasProducts k1, HasProducts k2, Functor f) => Applicative (f :: k1 -> k2) where
  pure :: El a -> El (f a)
  liftA2 :: (a && b ~> c) -> f a && f b ~> f c
type Alternative :: forall {k1} {k2}. (k1 -> k2) -> Constraint
class (HasCoproducts k1, HasProducts k2, Functor f) => Alternative (f :: k1 -> k2) where
  empty :: El (f a)
  alt :: (a || b ~> c) -> f a && f b ~> f c
instance Applicative f => Semigroup (Star (Day ProductFunctor ProductFunctor)) (Star f) where
  mmult = Prof $ \(Day (Star @x @b bfx) (Star @y cfy) abc xyz) ->
    xyz // Star $ liftA2 @f @x @y xyz . (bfx *** cfy) . abc
instance Applicative f => Monoid (Star (Day ProductFunctor ProductFunctor)) (Star f) where
  munit = Prof $ \(DayUnit a x) -> x // Star $ pure x . a
instance Alternative f => Semigroup (Star (Day ProductFunctor CoproductFunctor)) (Star f) where
  mmult = Prof $ \(Day (Star @x @b bfx) (Star @y cfy) abc xyz) ->
    xyz // Star $ alt @f @x @y xyz . (bfx *** cfy) . abc
instance Alternative f => Monoid (Star (Day ProductFunctor CoproductFunctor)) (Star f) where
  munit = Prof $ \(DayUnit a x) -> x // Star $ empty . a




type Booleans :: CAT Bool
data Booleans a b where
  Fls :: Booleans False False
  F2T :: Booleans False True
  Tru :: Booleans True True
type instance (~>) = Booleans
class IsBool (b :: Bool) where boolId :: b ~> b
instance IsBool False where boolId = Fls
instance IsBool True where boolId = Tru
instance Category Booleans where
  type Ob b = IsBool b
  id = boolId
  Fls . Fls = Fls
  F2T . Fls = F2T
  Tru . F2T = F2T
  Tru . Tru = Tru
instance Profunctor Booleans where
  dimap = dimapDefault
  r \\ Fls = r
  r \\ F2T = r
  r \\ Tru = r

instance HasTerminalObject Bool where
  type TerminalObject = True
  terminate' Fls = F2T
  terminate' Tru = Tru
instance HasBinaryProducts Bool where
  type True && True = True
  type False && True = False
  type True && False = False
  type False && False = False
  fst' Fls Fls = Fls
  fst' Fls Tru = Fls
  fst' Tru Fls = F2T
  fst' Tru Tru = Tru
  snd' Fls Fls = Fls
  snd' Fls Tru = F2T
  snd' Tru Fls = Fls
  snd' Tru Tru = Tru
  Fls &&& Fls = Fls
  Fls &&& F2T = Fls
  F2T &&& Fls = Fls
  F2T &&& F2T = F2T
  Tru &&& Tru = Tru

instance HasInitialObject Bool where
  type InitialObject = False
  initiate' Fls = Fls
  initiate' Tru = F2T
instance HasBinaryCoproducts Bool where
  type False || False = False
  type False || True = True
  type True || False = True
  type True || True = True
  left' Fls Fls = Fls
  left' Fls Tru = F2T
  left' Tru Fls = Tru
  left' Tru Tru = Tru
  right' Fls Fls = Fls
  right' Fls Tru = Tru
  right' Tru Fls = F2T
  right' Tru Tru = Tru
  Fls ||| Fls = Fls
  F2T ||| F2T = F2T
  F2T ||| Tru = Tru
  Tru ||| F2T = Tru
  Tru ||| Tru = Tru

instance CartesianClosed Bool where
  type False ~~> False = True
  type False ~~> True = True
  type True ~~> False = False
  type True ~~> True = True
  curry' Fls Fls Fls = F2T
  curry' Fls Fls F2T = F2T
  curry' Fls Tru Fls = Fls
  curry' Fls Tru F2T = F2T
  curry' Tru Fls Fls = Tru
  curry' Tru Fls F2T = Tru
  curry' Tru Tru Tru = Tru
  uncurry' Fls Fls F2T = Fls
  uncurry' Fls Fls Tru = Fls
  uncurry' Fls Tru F2T = F2T
  uncurry' Fls Tru Tru = F2T
  uncurry' Tru Fls Fls = Fls
  uncurry' Tru Tru F2T = F2T
  uncurry' Tru Tru Tru = Tru



newtype KIND = KIND Type
type family UNKIND (a :: KIND) :: Type where UNKIND ('KIND k) = k
type Cat :: CAT KIND
data Cat a b where
  Cat :: Profunctor (p :: PRO k1 k2) => Cat ('KIND k1) ('KIND k2)
type instance (~>) = Cat
instance Category Cat where
  type Ob c = (c ~ 'KIND (UNKIND c), Category ((~>) :: CAT (UNKIND c)))
  id = Cat @_ @_ @Id
  Cat @_ @_ @p . Cat @_ @_ @q = Cat @_ @_ @(p :.: q)
instance Profunctor Cat where
  dimap = dimapDefault
  r \\ Cat = r


type Terminate :: PRO k ()
data Terminate a b where
  Terminate :: Ob a => Terminate a '()
instance CategoryOf k => Profunctor (Terminate :: PRO k ()) where
  dimap l Unit Terminate = Terminate \\ l
  r \\ Terminate = r
instance HasTerminalObject KIND where
  type TerminalObject = 'KIND ()
  terminate' (Cat @a) = Cat @_ @_ @Terminate


type FstCat :: PRO (k1, k2) k1
data FstCat a b where
  FstCat :: Ob b => a ~> c -> FstCat '(a, b) c
instance (CategoryOf k1, CategoryOf k2) => Profunctor (FstCat :: PRO (k1, k2) k1) where
  dimap (l1 :**: l2) r (FstCat f) = FstCat (r . f . l1) \\ l2
  r \\ FstCat f = r \\ f

type SndCat :: PRO (k1, k2) k2
data SndCat a b where
  SndCat :: Ob a => b ~> c -> SndCat '(a, b) c
instance (CategoryOf k1, CategoryOf k2) => Profunctor (SndCat :: PRO (k1, k2) k2) where
  dimap (l1 :**: l2) r (SndCat f) = SndCat (r . f . l2) \\ l1
  r \\ SndCat f = r \\ f

type (:&&&:) :: PRO k1 k2 -> PRO k1 k3 -> PRO k1 (k2, k3)
data (p :&&&: q) a b where
  (:&&&:) :: p a b -> q a c -> (p :&&&: q) a '(b, c)
instance (Profunctor p, Profunctor q) => Profunctor (p :&&&: q) where
  dimap l (r1 :**: r2) (p :&&&: q) = dimap l r1 p :&&&: dimap l r2 q
  r \\ (p :&&&: q) = r \\ p \\ q

instance HasBinaryProducts KIND where
  type 'KIND l && 'KIND r = 'KIND (l, r)
  fst' Cat Cat = Cat @_ @_ @FstCat
  snd' Cat Cat = Cat @_ @_ @SndCat
  Cat @_ @_ @p &&& Cat @_ @_ @q = Cat @_ @_ @(p :&&&: q)



newtype CONSTRAINT = CNSTRNT Constraint
type family UNCNSTRNT (a :: CONSTRAINT) :: Constraint where UNCNSTRNT (CNSTRNT a) = a
data (:-) a b where
  Entails :: { getEntails :: forall r. a => (b => r) -> r } -> CNSTRNT a :- CNSTRNT b
type instance (~>) = (:-)
instance Category (:-) where
  type Ob a = (a ~ CNSTRNT (UNCNSTRNT a))
  id = Entails \r -> r
  Entails f . Entails g = Entails \r -> g (f r)
instance Profunctor (:-) where
  dimap = dimapDefault
  r \\ Entails{} = r

instance HasTerminalObject CONSTRAINT where
  type TerminalObject = CNSTRNT ()
  terminate' Entails{} = Entails \r -> r

-- copied from constraints package
class Any => Bottom where
  no :: a
instance HasInitialObject CONSTRAINT where
  type InitialObject = CNSTRNT Bottom
  initiate' Entails{} = Entails \_ -> no

instance HasBinaryProducts CONSTRAINT where
  type CNSTRNT l && CNSTRNT r = CNSTRNT (l, r)
  fst' Entails{} Entails{} = Entails \r -> r
  snd' Entails{} Entails{} = Entails \r -> r
  Entails f &&& Entails g = Entails \r -> f (g r)




data Ent = Emp | Dept
data EntEdge a b where
  Mgr :: EntEdge Emp Emp
  Wrk :: EntEdge Emp Dept
  Sec :: EntEdge Dept Emp
instance Rewrite EntEdge where
  rewriteAfterCons = \case
    Mgr :| Mgr :| h -> Mgr :| h
    Mgr :| Wrk :| h -> Wrk :| h
    Sec :| Wrk :| h -> h
    h -> h
type instance (~>) = FreeCat EntEdge
instance Category (FreeCat EntEdge) where
  id = FreeId
  f . g = mult (f :.: g)

type Schema :: PRO Ent Type
data Schema e t where
  Last :: Schema Emp String
  Name :: Schema Dept String
  Sal :: Schema Emp Int
type Instance :: TAG (Collage (Yoneda Schema)) -> Type
data Instance a where
  E1 :: Instance ('TAG (Left Emp))
  E2 :: Instance ('TAG (Left Emp))
  D1 :: Instance ('TAG (Left Dept))
  IVal :: v -> Instance ('TAG (Right v))
instance Functor Instance where
  map (Tag (InL FreeId)) e = e
  map (Tag (InL (f :| a))) i = map (Tag (InL a)) (h f i)
    where
      h :: EntEdge a b -> Instance ('TAG (Left a)) -> Instance ('TAG (Left b))
      h Wrk E1 = D1
      h Wrk E2 = D1
      h Mgr E1 = E2
      h Mgr E2 = E2
      h Sec D1 = E1
  map (Tag (L2R p)) i = IVal (h (freePro p) i)
    where
      h :: Schema e t -> Instance ('TAG (Left e)) -> t
      h Last E1 = "Gauss"
      h Last E2 = "Noether"
      h Name D1 = "HR"
      h Sal E1 = 200
      h Sal E2 = 250
  map (Tag (InR f)) (IVal x) = IVal (f x)