{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Profunctor.Cofree where

import Data.Kind (Constraint)

import Proarrow.Adjunction (Adjunction (..), counitFromRepCounit, unitFromRepUnit)
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Core (CategoryOf (..), OB, Profunctor (..), Promonad (..), type (+->))
import Proarrow.Profunctor.Forget (Forget)
import Proarrow.Profunctor.Representable (Representable (..), dimapRep, repObj)

type HasCofree :: forall {k}. (k -> Constraint) -> Constraint
class
  (CategoryOf k, Representable (Cofree ob), forall b. (Ob b) => ob (Cofree ob % b)) =>
  HasCofree (ob :: k -> Constraint)
  where
  type Cofree ob :: k +-> k
  lower' :: Cofree ob a b -> a ~> b
  section' :: (ob b) => a ~> b -> Cofree ob a b

lower :: forall ob a. (HasCofree ob, Ob a) => Cofree ob % a ~> a
lower :: forall {k} (ob :: k -> Constraint) (a :: k).
(HasCofree ob, Ob a) =>
(Cofree ob % a) ~> a
lower = forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
HasCofree ob =>
Cofree ob a b -> a ~> b
forall (ob :: k -> Constraint) (a :: k) (b :: k).
HasCofree ob =>
Cofree ob a b -> a ~> b
lower' @ob (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: k +-> k) (b :: k) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @(Cofree ob) (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
Obj (p % a)
repObj @(Cofree ob) @a))

section :: forall ob a. (HasCofree ob, ob a, Ob a) => a ~> Cofree ob % a
section :: forall {j} (ob :: j -> Constraint) (a :: j).
(HasCofree ob, ob a, Ob a) =>
a ~> (Cofree ob % a)
section = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: j +-> j) (a :: j) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index @(Cofree ob) (forall {k} (ob :: k -> Constraint) (b :: k) (a :: k).
(HasCofree ob, ob b) =>
(a ~> b) -> Cofree ob a b
forall (ob :: j -> Constraint) (b :: j) (a :: j).
(HasCofree ob, ob b) =>
(a ~> b) -> Cofree ob a b
section' @ob a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)

type CofreeSub :: forall (ob :: OB k) -> k +-> SUBCAT ob
data CofreeSub ob a b where
  CofreeSub :: (ob a) => Cofree ob a b -> CofreeSub ob (SUB a) b

instance (HasCofree ob) => Profunctor (CofreeSub ob) where
  dimap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> CofreeSub ob a b -> CofreeSub ob c d
dimap = (c ~> a) -> (b ~> d) -> CofreeSub ob a b -> CofreeSub ob c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: SUBCAT ob) (b :: k) r.
((Ob a, Ob b) => r) -> CofreeSub ob a b -> r
\\ CofreeSub Cofree ob a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> Cofree ob a b -> r
forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Cofree ob a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Cofree ob a b
p

instance (HasCofree ob) => Representable (CofreeSub ob) where
  type CofreeSub ob % a = SUB (Cofree ob % a)
  index :: forall (a :: SUBCAT ob) (b :: j).
CofreeSub ob a b -> a ~> (CofreeSub ob % b)
index (CofreeSub Cofree ob a b
p) = (a ~> (Cofree ob % b)) -> Sub (~>) (SUB a) (SUB (Cofree ob % b))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (Cofree ob a b -> a ~> (Cofree ob % b)
forall (a :: j) (b :: j). Cofree ob a b -> a ~> (Cofree ob % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index Cofree ob a b
p) ((Ob a, Ob b) => Sub (~>) (SUB a) (SUB (Cofree ob % b)))
-> Cofree ob a b -> Sub (~>) (SUB a) (SUB (Cofree ob % b))
forall (a :: j) (b :: j) r.
((Ob a, Ob b) => r) -> Cofree ob a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Cofree ob a b
p
  tabulate :: forall (b :: j) (a :: SUBCAT ob).
Ob b =>
(a ~> (CofreeSub ob % b)) -> CofreeSub ob a b
tabulate (Sub a1 ~> b1
f) = Cofree ob a1 b -> CofreeSub ob (SUB a1) b
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
ob a =>
Cofree ob a b -> CofreeSub ob (SUB a) b
CofreeSub ((a1 ~> (Cofree ob % b)) -> Cofree ob a1 b
forall (b :: j) (a :: j).
Ob b =>
(a ~> (Cofree ob % b)) -> Cofree ob a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a1 ~> b1
a1 ~> (Cofree ob % b)
f)
  repMap :: forall (a :: j) (b :: j).
(a ~> b) -> (CofreeSub ob % a) ~> (CofreeSub ob % b)
repMap a ~> b
f = ((Cofree ob % a) ~> (Cofree ob % b))
-> Sub (~>) (SUB (Cofree ob % a)) (SUB (Cofree ob % b))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> j) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(Cofree ob) a ~> b
f) ((Ob a, Ob b) =>
 Sub (~>) (SUB (Cofree ob % a)) (SUB (Cofree ob % b)))
-> (a ~> b) -> Sub (~>) (SUB (Cofree ob % a)) (SUB (Cofree ob % b))
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

instance (HasCofree ob) => Adjunction (Forget ob) (CofreeSub ob) where
  unit :: forall (a :: SUBCAT ob).
Ob a =>
(:.:) (CofreeSub ob) (Forget ob) a a
unit = (a ~> (CofreeSub ob % (Forget ob % a)))
-> (:.:) (CofreeSub ob) (Forget ob) a a
forall {i} {j} (l :: i +-> j) (r :: j +-> i) (a :: i).
(Representable l, Representable r, Ob a) =>
(a ~> (r % (l % a))) -> (:.:) r l a a
unitFromRepUnit ((UN SUB a ~> (Cofree ob % UN SUB a))
-> Sub (~>) (SUB (UN SUB a)) (SUB (Cofree ob % UN SUB a))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {j} (ob :: j -> Constraint) (a :: j).
(HasCofree ob, ob a, Ob a) =>
a ~> (Cofree ob % a)
forall (ob :: k -> Constraint) (a :: k).
(HasCofree ob, ob a, Ob a) =>
a ~> (Cofree ob % a)
section @ob))
  counit :: (Forget ob :.: CofreeSub ob) :~> (~>)
counit = (forall (c :: k). Ob c => (Forget ob % (CofreeSub ob % c)) ~> c)
-> (Forget ob :.: CofreeSub ob) :~> (~>)
forall {j} {k1} (l :: j +-> k1) (r :: k1 +-> j).
(Representable l, Representable r) =>
(forall (c :: k1). Ob c => (l % (r % c)) ~> c)
-> (l :.: r) :~> (~>)
counitFromRepCounit (forall {k} (ob :: k -> Constraint) (a :: k).
(HasCofree ob, Ob a) =>
(Cofree ob % a) ~> a
forall (ob :: k -> Constraint) (a :: k).
(HasCofree ob, Ob a) =>
(Cofree ob % a) ~> a
lower @ob)