{-# OPTIONS_GHC -Wno-orphans #-}

-- | Initial objects: 'HasInitialObject' with the unique arrow 'initiate', instances for the base kinds,
-- and 'HasZeroObject' for categories where the initial and terminal objects coincide.
module Proarrow.Colimit.Initial where

import Data.Kind (Type)
import Data.Void (Void, absurd)
import Prelude (Show, type (~))
import Prelude qualified as P

import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Free
  ( Elem (..)
  , FREE (..)
  , Free (..)
  , HasStructure (..)
  , IsFreeOb (..)
  , Lower
  , withLowerOb
  )
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), obj, type (+->))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Instance.Initial (InitialProfunctor)
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Tools.Laws (Law (..), Laws (..), (===))

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

initiate' :: forall {k} a' a. (HasInitialObject k) => (a' :: k) ~> a -> InitialObject ~> a
initiate' :: forall {k} (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
initiate' a' ~> a
a = a' ~> a
a (a' ~> a) -> (InitialObject ~> a') -> InitialObject ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @k @a' ((Ob a', Ob a) => InitialObject ~> a)
-> (a' ~> a) -> InitialObject ~> a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a' ~> a
a

instance HasInitialObject Type where
  type InitialObject = Void
  initiate :: forall a. Ob a => InitialObject ~> a
initiate = InitialObject ~> a
Void -> a
forall a. Void -> a
absurd

instance HasInitialObject () where
  type InitialObject = '()
  initiate :: forall (a :: ()). Ob a => InitialObject ~> a
initiate = InitialObject ~> a
Unit '() '()
Unit

instance HasInitialObject BOOL where
  type InitialObject = FLS
  initiate :: forall (a :: BOOL). Ob a => InitialObject ~> a
initiate @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> InitialObject ~> a
Booleans 'FLS 'FLS
Fls
    Obj a
Booleans a a
Tru -> InitialObject ~> a
Booleans 'FLS 'TRU
F2T

instance (HasInitialObject j, HasInitialObject k) => HasInitialObject (j, k) where
  type InitialObject = '(InitialObject, InitialObject)
  initiate :: forall (a :: (j, k)). Ob a => InitialObject ~> a
initiate = InitialObject ~> (Fst @ a)
forall (a :: j). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate (InitialObject ~> (Fst @ a))
-> (InitialObject ~> (Snd @ a))
-> (:**:)
     (~>) (~>) '(InitialObject, InitialObject) '(Fst @ a, Snd @ a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: InitialObject ~> (Snd @ a)
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

instance (CategoryOf j, CategoryOf k) => HasInitialObject (j +-> k) where
  type InitialObject = InitialProfunctor
  initiate :: forall (a :: j +-> k). Ob a => InitialObject ~> a
initiate = (InitialProfunctor :~> a) -> Prof InitialProfunctor a
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case {}

instance (HasInitialObject j, CategoryOf k) => Corepresentable (TerminalProfunctor :: j +-> k) where
  type TerminalProfunctor %% x = InitialObject
  coindex :: forall (a :: k) (b :: j).
TerminalProfunctor a b -> (TerminalProfunctor %% a) ~> b
coindex TerminalProfunctor a b
TerminalProfunctor = (TerminalProfunctor %% a) ~> b
InitialObject ~> b
forall (a :: j). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
  cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((TerminalProfunctor %% a) ~> b) -> TerminalProfunctor a b
cotabulate (TerminalProfunctor %% a) ~> b
f = TerminalProfunctor a b
(Ob InitialObject, Ob b) => TerminalProfunctor a b
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor ((Ob InitialObject, Ob b) => TerminalProfunctor a b)
-> (InitialObject ~> b) -> TerminalProfunctor a b
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (TerminalProfunctor %% a) ~> b
InitialObject ~> b
f
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (TerminalProfunctor %% a) ~> (TerminalProfunctor %% b)
corepMap a ~> b
_ = (TerminalProfunctor %% a) ~> (TerminalProfunctor %% b)
InitialObject ~> InitialObject
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

class (HasInitialObject k, HasTerminalObject k, (InitialObject :: k) ~ TerminalObject) => HasZeroObject k where
  zero :: (Ob (a :: k), Ob b) => a ~> b
instance (HasInitialObject k, HasTerminalObject k, (InitialObject :: k) ~ TerminalObject) => HasZeroObject k where
  zero :: forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b
zero = TerminalObject ~> b
InitialObject ~> b
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate (TerminalObject ~> b) -> (a ~> TerminalObject) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

data family InitF :: k
instance (HasInitialObject `Elem` cs) => IsFreeOb (InitF :: FREE cs p) where
  type Lower f InitF = InitialObject
  lowerOb :: forall k' (f :: k +-> k') r.
(Representable f, All cs k') =>
(Ob (Lower f InitF) => r) -> r
lowerOb @k' @_ Ob (Lower f InitF) => r
r = forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k r.
(Elem c cs, All cs k) =>
(c k => r) -> r
fromAll @HasInitialObject @cs @k' r
Ob (Lower f InitF) => r
HasInitialObject k' => r
r
instance (HasInitialObject `Elem` cs) => HasStructure cs (p :: CAT k) HasInitialObject where
  data Struct HasInitialObject a b where
    Initial :: (Ob b) => Struct HasInitialObject InitF b
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(HasInitialObject k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct HasInitialObject a b -> Lower f a ~> Lower f b
foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Initial @b) = forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b InitialObject ~> Lower f b
Ob (Lower f b) => InitialObject ~> Lower f b
forall (a :: k'). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
instance Show (Struct HasInitialObject a b) where
  showsPrec :: Int -> Struct HasInitialObject a b -> ShowS
showsPrec Int
_ Struct HasInitialObject a b
R:StructkcspHasInitialObjectab k cs p a b
Initial = String -> ShowS
P.showString String
"initiate"
instance (HasInitialObject `Elem` cs) => HasInitialObject (FREE cs (p :: CAT k)) where
  type InitialObject = InitF
  initiate :: forall (a :: FREE cs p). Ob a => InitialObject ~> a
initiate = Struct HasInitialObject InitF a -> Free InitF InitF -> Free InitF a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
St Struct HasInitialObject InitF a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (b :: FREE cs p).
Ob b =>
Struct HasInitialObject InitF b
Initial Free InitF InitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil

instance (HasInitialObject k) => HasTerminalObject (OPPOSITE k) where
  type TerminalObject = OP InitialObject
  terminate :: forall (a :: OPPOSITE k). Ob a => a ~> TerminalObject
terminate = (InitialObject ~> UN OP a)
-> Op (~>) (OP (UN OP a)) (OP InitialObject)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op InitialObject ~> UN OP a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

instance (HasTerminalObject k) => HasInitialObject (OPPOSITE k) where
  type InitialObject = OP TerminalObject
  initiate :: forall (a :: OPPOSITE k). Ob a => InitialObject ~> a
initiate = (UN OP a ~> TerminalObject)
-> Op (~>) (OP TerminalObject) (OP (UN OP a))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op UN OP a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

-- | Every arrow out of the initial object is 'initiate'.
instance Laws '[HasInitialObject] where
  laws :: [Law '[HasInitialObject]]
laws =
    [ String -> LawBody '[HasInitialObject] -> Law '[HasInitialObject]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"uniqueness" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        g <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @InitialObject @a String
"g"
        g === initiate
    ]