module Proarrow.Category.Bicategory.Bidiscrete where

import Data.Type.Equality (type (~~))

import Proarrow.Category.Bicategory (Bicategory(..))
import Proarrow.Core (CAT, Profunctor (..), Promonad (..), CategoryOf(..), dimapDefault, Kind)

type DiscreteK :: CAT Kind
data DiscreteK j k where
  DK :: DiscreteK j j
type Bidiscrete :: CAT (DiscreteK j k)
data Bidiscrete a b where
  Bidiscrete :: Bidiscrete DK DK

instance Profunctor Bidiscrete where
  dimap :: forall (c :: DiscreteK j k) (a :: DiscreteK j k)
       (b :: DiscreteK j k) (d :: DiscreteK j k).
(c ~> a) -> (b ~> d) -> Bidiscrete a b -> Bidiscrete c d
dimap = (c ~> a) -> (b ~> d) -> Bidiscrete a b -> Bidiscrete c d
Bidiscrete c a
-> Bidiscrete b d -> Bidiscrete a b -> Bidiscrete c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: DiscreteK j k) (b :: DiscreteK j k) r.
((Ob a, Ob b) => r) -> Bidiscrete a b -> r
\\ Bidiscrete a b
Bidiscrete = r
(Ob a, Ob b) => r
r
instance Promonad Bidiscrete where
  id :: forall (a :: DiscreteK j k). Ob a => Bidiscrete a a
id = Bidiscrete 'DK 'DK
Bidiscrete a a
forall {k}. Bidiscrete 'DK 'DK
Bidiscrete
  Bidiscrete b c
Bidiscrete . :: forall (b :: DiscreteK j k) (c :: DiscreteK j k)
       (a :: DiscreteK j k).
Bidiscrete b c -> Bidiscrete a b -> Bidiscrete a c
. Bidiscrete a b
Bidiscrete = Bidiscrete 'DK 'DK
Bidiscrete a c
forall {k}. Bidiscrete 'DK 'DK
Bidiscrete
instance CategoryOf (DiscreteK j k) where
  type (~>) = Bidiscrete
  type Ob (a :: DiscreteK j k) = (j ~ k, a ~~ (DK :: DiscreteK j j))

-- | The bicategory with only identity 1-cells and identity 2-cells between those.
instance Bicategory DiscreteK where
  type I = DK
  type DK `O` DK = DK
  a ~> b
Bidiscrete a b
Bidiscrete o :: forall {k1} i j (a :: DiscreteK i j) (b :: DiscreteK i j)
       (c :: DiscreteK j k1) (d :: DiscreteK j k1).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` c ~> d
Bidiscrete c d
Bidiscrete = O a c ~> O b d
Bidiscrete 'DK 'DK
forall {k}. Bidiscrete 'DK 'DK
Bidiscrete
  (Ob0 DiscreteK i, Ob0 DiscreteK j, Ob ps, Ob qs) => r
r \\\ :: forall i j (ps :: DiscreteK i j) (qs :: DiscreteK i j) r.
((Ob0 DiscreteK i, Ob0 DiscreteK j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ ps ~> qs
Bidiscrete ps qs
Bidiscrete = r
(Ob0 DiscreteK i, Ob0 DiscreteK j, Ob ps, Ob qs) => r
r
  leftUnitor :: forall i j (a :: DiscreteK i j). Obj a -> O I a ~> a
leftUnitor Obj a
Bidiscrete a a
Bidiscrete = O I a ~> a
Bidiscrete 'DK 'DK
forall {k}. Bidiscrete 'DK 'DK
Bidiscrete
  leftUnitorInv :: forall i j (a :: DiscreteK i j). Obj a -> a ~> O I a
leftUnitorInv Obj a
Bidiscrete a a
Bidiscrete = a ~> O I a
Bidiscrete 'DK 'DK
forall {k}. Bidiscrete 'DK 'DK
Bidiscrete
  rightUnitor :: forall i j (a :: DiscreteK i j). Obj a -> O a I ~> a
rightUnitor Obj a
Bidiscrete a a
Bidiscrete = O a I ~> a
Bidiscrete 'DK 'DK
forall {k}. Bidiscrete 'DK 'DK
Bidiscrete
  rightUnitorInv :: forall i j (a :: DiscreteK i j). Obj a -> a ~> O a I
rightUnitorInv Obj a
Bidiscrete a a
Bidiscrete = a ~> O a I
Bidiscrete 'DK 'DK
forall {k}. Bidiscrete 'DK 'DK
Bidiscrete
  associator :: forall {j1} {k1} i j2 (a :: DiscreteK i j2) (b :: DiscreteK j2 j1)
       (c :: DiscreteK j1 k1).
Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c)
associator Obj a
Bidiscrete a a
Bidiscrete Obj b
Bidiscrete b b
Bidiscrete Obj c
Bidiscrete c c
Bidiscrete = O (O a b) c ~> O a (O b c)
Bidiscrete 'DK 'DK
forall {k}. Bidiscrete 'DK 'DK
Bidiscrete
  associatorInv :: forall {j1} {k1} i j2 (a :: DiscreteK i j2) (b :: DiscreteK j2 j1)
       (c :: DiscreteK j1 k1).
Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c
associatorInv Obj a
Bidiscrete a a
Bidiscrete Obj b
Bidiscrete b b
Bidiscrete Obj c
Bidiscrete c c
Bidiscrete = O a (O b c) ~> O (O a b) c
Bidiscrete 'DK 'DK
forall {k}. Bidiscrete 'DK 'DK
Bidiscrete