module Proarrow.Category.Bicategory.Bidiscrete where

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

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

type DiscreteK :: forall {c}. OB c -> CAT c
type data DiscreteK (ob :: OB c) j k where
  DK :: DiscreteK ob j j
type Bidiscrete :: CAT (DiscreteK ob j k)
data Bidiscrete a b where
  Bidiscrete :: (ob j) => Bidiscrete (DK :: DiscreteK ob j j) DK

instance Profunctor Bidiscrete where
  dimap :: forall (c :: DiscreteK ob j k) (a :: DiscreteK ob j k)
       (b :: DiscreteK ob j k) (d :: DiscreteK ob 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 ob j k) (b :: DiscreteK ob 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 ob j k). Ob a => Bidiscrete a a
id = Bidiscrete DK DK
Bidiscrete a a
forall {c} (ob :: c -> Constraint) (j :: c).
ob j =>
Bidiscrete DK DK
Bidiscrete
  Bidiscrete b c
Bidiscrete . :: forall (b :: DiscreteK ob j k) (c :: DiscreteK ob j k)
       (a :: DiscreteK ob j k).
Bidiscrete b c -> Bidiscrete a b -> Bidiscrete a c
. Bidiscrete a b
Bidiscrete = Bidiscrete DK DK
Bidiscrete a c
forall {c} (ob :: c -> Constraint) (j :: c).
ob j =>
Bidiscrete DK DK
Bidiscrete
instance CategoryOf (DiscreteK ob j k) where
  type (~>) = Bidiscrete
  type Ob (a :: DiscreteK ob j k) = (j ~ k, a ~~ (DK :: DiscreteK ob j j), ob j)

-- | The bicategory with only identity 1-cells and identity 2-cells between those.
instance CategoryOf c => Bicategory (DiscreteK (ob :: OB c)) where
  type Ob0 (DiscreteK ob) k = ob k
  type I = DK
  type DK `O` DK = DK
  a ~> b
Bidiscrete a b
Bidiscrete o :: forall {i :: c} (j :: c) (k :: c) (a :: DiscreteK ob j k)
       (b :: DiscreteK ob j k) (c :: DiscreteK ob i j)
       (d :: DiscreteK ob i j).
(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 {c} (ob :: c -> Constraint) (j :: c).
ob j =>
Bidiscrete DK DK
Bidiscrete
  (Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: c) (j :: c) (ps :: DiscreteK ob i j)
       (qs :: DiscreteK ob i j) r.
((Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ ps ~> qs
Bidiscrete ps qs
Bidiscrete = r
(Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob ps, Ob qs) => r
r
  leftUnitor :: forall {i :: c} {j :: c} (a :: DiscreteK ob i j).
(Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob a) =>
O I a ~> a
leftUnitor = O I a ~> a
Bidiscrete DK DK
forall {c} (ob :: c -> Constraint) (j :: c).
ob j =>
Bidiscrete DK DK
Bidiscrete
  leftUnitorInv :: forall {i :: c} {j :: c} (a :: DiscreteK ob i j).
(Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob a) =>
a ~> O I a
leftUnitorInv = a ~> O I a
Bidiscrete DK DK
forall {c} (ob :: c -> Constraint) (j :: c).
ob j =>
Bidiscrete DK DK
Bidiscrete
  rightUnitor :: forall {i :: c} {j :: c} (a :: DiscreteK ob i j).
(Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob a) =>
O a I ~> a
rightUnitor = O a I ~> a
Bidiscrete DK DK
forall {c} (ob :: c -> Constraint) (j :: c).
ob j =>
Bidiscrete DK DK
Bidiscrete
  rightUnitorInv :: forall {i :: c} {j :: c} (a :: DiscreteK ob i j).
(Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j, Ob a) =>
a ~> O a I
rightUnitorInv = a ~> O a I
Bidiscrete DK DK
forall {c} (ob :: c -> Constraint) (j :: c).
ob j =>
Bidiscrete DK DK
Bidiscrete
  associator :: forall {h :: c} {i :: c} {j :: c} {k :: c} (a :: DiscreteK ob j k)
       (b :: DiscreteK ob i j) (c :: DiscreteK ob h i).
(Ob0 (DiscreteK ob) h, Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j,
 Ob0 (DiscreteK ob) k, Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator = O (O a b) c ~> O a (O b c)
Bidiscrete DK DK
forall {c} (ob :: c -> Constraint) (j :: c).
ob j =>
Bidiscrete DK DK
Bidiscrete
  associatorInv :: forall {h :: c} {i :: c} {j :: c} {k :: c} (a :: DiscreteK ob j k)
       (b :: DiscreteK ob i j) (c :: DiscreteK ob h i).
(Ob0 (DiscreteK ob) h, Ob0 (DiscreteK ob) i, Ob0 (DiscreteK ob) j,
 Ob0 (DiscreteK ob) k, Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv = O a (O b c) ~> O (O a b) c
Bidiscrete DK DK
forall {c} (ob :: c -> Constraint) (j :: c).
ob j =>
Bidiscrete DK DK
Bidiscrete