module Proarrow.Profunctor.Forget where

import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Core (CategoryOf (..), OB, Profunctor (..), Promonad (..), type (+->))
import Proarrow.Profunctor.Representable (Representable (..))

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

instance (CategoryOf k) => Profunctor (Forget (ob :: OB k)) where
  dimap :: forall (c :: k) (a :: k) (b :: SUBCAT ob) (d :: SUBCAT ob).
(c ~> a) -> (b ~> d) -> Forget ob a b -> Forget ob c d
dimap c ~> a
l (Sub a1 ~> b1
r) (Forget a ~> b
f) = (c ~> b1) -> Forget ob c (SUB b1)
forall {k} (ob :: k -> Constraint) (b :: k) (a :: k).
ob b =>
(a ~> b) -> Forget ob a (SUB b)
Forget (a1 ~> b1
r (a1 ~> b1) -> (c ~> a1) -> c ~> b1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a1
a ~> b
f (a ~> a1) -> (c ~> a) -> c ~> a1
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: SUBCAT ob) r.
((Ob a, Ob b) => r) -> Forget ob a b -> r
\\ Forget a ~> b
f = r
(Ob a, Ob b) => 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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

instance (CategoryOf k) => Representable (Forget (ob :: OB k)) where
  type Forget ob % (SUB a) = a
  index :: forall (a :: k) (b :: SUBCAT ob).
Forget ob a b -> a ~> (Forget ob % b)
index (Forget a ~> b
f) = a ~> b
a ~> (Forget ob % b)
f
  tabulate :: forall (b :: SUBCAT ob) (a :: k).
Ob b =>
(a ~> (Forget ob % b)) -> Forget ob a b
tabulate = (a ~> UN SUB b) -> Forget ob a (SUB (UN SUB b))
(a ~> (Forget ob % b)) -> Forget ob a b
forall {k} (ob :: k -> Constraint) (b :: k) (a :: k).
ob b =>
(a ~> b) -> Forget ob a (SUB b)
Forget
  repMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(a ~> b) -> (Forget ob % a) ~> (Forget ob % b)
repMap (Sub a1 ~> b1
f) = a1 ~> b1
(Forget ob % a) ~> (Forget ob % b)
f