-- | The identity profunctor 'Id', wrapping the hom arrows of a category. It is the unit of profunctor
-- composition ("Proarrow.Profunctor.Instance.Composition") and the identity 'Promonad'.
module Proarrow.Profunctor.Instance.Identity where

import Proarrow.Category.Enriched.Dagger (Dagger, DaggerProfunctor (..))
import Proarrow.Category.Enriched.Thin (DecidableProfunctor (..), Thin, ThinProfunctor (..), mapDecision)
import Proarrow.Core (CAT, CategoryOf (..), Hom, Profunctor (..), Promonad (..))
import Proarrow.Functor (FunctorForRep (..))

-- | The identity profunctor: the hom arrows of the category wrapped as a data type. It is the unit
-- of profunctor composition and the identity 'Promonad'.
type Id :: CAT k
newtype Id a b = Id {forall k (a :: k) (b :: k). Id a b -> a ~> b
unId :: a ~> b}

instance (CategoryOf k) => Profunctor (Id :: CAT k) where
  lmap :: forall (c :: k) (a :: k) (b :: k). (c ~> a) -> Id a b -> Id c b
lmap c ~> a
l (Id a ~> b
f) = (c ~> b) -> Id c b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (a ~> b
f (a ~> b) -> (c ~> a) -> c ~> 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
. c ~> a
l)
  rmap :: forall (b :: k) (d :: k) (a :: k). (b ~> d) -> Id a b -> Id a d
rmap b ~> d
r (Id a ~> b
f) = (a ~> d) -> Id a d
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (b ~> d
r (b ~> d) -> (a ~> b) -> a ~> d
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 ~> b
f)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Id a b -> r
\\ Id a ~> b
f = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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 ~> b
f

instance (CategoryOf k) => Promonad (Id :: CAT k) where
  id :: forall (a :: k). Ob a => Id a a
id = (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  Id b ~> c
f . :: forall (b :: k) (c :: k) (a :: k). Id b c -> Id a b -> Id a c
. Id a ~> b
g = (a ~> c) -> Id a c
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (b ~> c
f (b ~> c) -> (a ~> b) -> a ~> c
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 ~> b
g)

instance (CategoryOf k) => FunctorForRep (Id :: CAT k) where
  type Id @ a = a
  fmap :: forall (a :: k) (b :: k). (a ~> b) -> (Id @ a) ~> (Id @ b)
fmap a ~> b
f = a ~> b
(Id @ a) ~> (Id @ b)
f

instance (Dagger k) => DaggerProfunctor (Id :: CAT k) where
  dagger :: forall (a :: k) (b :: k). Id a b -> Id b a
dagger (Id a ~> b
p) = (b ~> a) -> Id b a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((a ~> b) -> b ~> a
forall (a :: k) (b :: k). (a ~> b) -> b ~> a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger a ~> b
p)

instance (Thin k) => ThinProfunctor (Id :: CAT k) where
  type HasArrow (Id :: CAT k) a b = HasArrow (Hom k) a b
  arr :: forall (a :: k) (b :: k). (Ob a, Ob b, HasArrow Id a b) => Id a b
arr = (a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> b
forall (a :: k) (b :: k).
(Ob a, Ob b, HasArrow (Hom k) a b) =>
a ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
  withArr :: forall (a :: k) (b :: k) r.
Id a b -> ((HasArrow Id a b, Ob a, Ob b) => r) -> r
withArr (Id a ~> b
f) (HasArrow Id a b, Ob a, Ob b) => r
r = (a ~> b) -> ((HasArrow (Hom k) a b, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> ((HasArrow (Hom k) a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr a ~> b
f r
(HasArrow (Hom k) a b, Ob a, Ob b) => r
(HasArrow Id a b, Ob a, Ob b) => r
r

instance (DecidableProfunctor (Hom k)) => DecidableProfunctor (Id :: CAT k) where
  type Holds (Id :: CAT k) a b = Holds (Hom k) a b
  decide :: forall (a :: k) (b :: k).
(Ob a, Ob b) =>
Decision Id a b (Holds Id a b)
decide @a @b = ((a ~> b) -> Id a b)
-> Decision (Hom k) a b (Holds (Hom k) a b)
-> Decision Id a b (Holds (Hom k) a b)
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision (a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: k +-> k) (a :: k) (b :: k).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @(Hom k) @a @b)
  toHolds :: forall (a :: k) (b :: k) r.
Id a b -> ((Holds Id a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds (Id a ~> b
f) (Holds Id a b ~ 'TRU, Ob a, Ob b) => r
r = (a ~> b) -> ((Holds (Hom k) a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> ((Holds (Hom k) a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds a ~> b
f r
(Holds (Hom k) a b ~ 'TRU, Ob a, Ob b) => r
(Holds Id a b ~ 'TRU, Ob a, Ob b) => r
r