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))
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