module Proarrow.Category.Bicategory.ThinCategoryAsBi where

import Prelude (type (~))

import Proarrow.Category.Bicategory (Bicategory (..))
import Proarrow.Category.Bicategory.LaxFunctor (LaxFunctor (..), Map0, Map1, (:->))
import Proarrow.Category.Enriched.Thin (Thin, ThinProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Hom, Profunctor (..), Promonad (..), dimapDefault, obj, type (+->))
import Proarrow.Profunctor.Representable (Representable (..), withObRep)

type THINK :: forall k -> CAT k
data THINK k i j = THIN

type ThinCategory :: CAT (THINK k i j)
data ThinCategory a b where
  Id :: forall {k} i j. (HasArrow (Hom k) i j, Ob i, Ob j) => ThinCategory (THIN :: THINK k (i :: k) (j :: k)) THIN

instance (Thin k) => Profunctor (ThinCategory :: CAT (THINK k i j)) where
  dimap :: forall (c :: THINK k i j) (a :: THINK k i j) (b :: THINK k i j)
       (d :: THINK k i j).
(c ~> a) -> (b ~> d) -> ThinCategory a b -> ThinCategory c d
dimap = (c ~> a) -> (b ~> d) -> ThinCategory a b -> ThinCategory c d
ThinCategory c a
-> ThinCategory b d -> ThinCategory a b -> ThinCategory c d
forall {k} (p :: 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 :: THINK k i j) (b :: THINK k i j) r.
((Ob a, Ob b) => r) -> ThinCategory a b -> r
\\ ThinCategory a b
Id = r
(Ob a, Ob b) => r
r
instance (Thin k) => Promonad (ThinCategory :: CAT (THINK k i j)) where
  id :: forall (a :: THINK k i j). Ob a => ThinCategory a a
id = ThinCategory a a
ThinCategory 'THIN 'THIN
forall {k} (i :: k) (j :: k).
(HasArrow (Hom k) i j, Ob i, Ob j) =>
ThinCategory 'THIN 'THIN
Id
  ThinCategory b c
Id . :: forall (b :: THINK k i j) (c :: THINK k i j) (a :: THINK k i j).
ThinCategory b c -> ThinCategory a b -> ThinCategory a c
. ThinCategory a b
Id = ThinCategory a c
ThinCategory 'THIN 'THIN
forall {k} (i :: k) (j :: k).
(HasArrow (Hom k) i j, Ob i, Ob j) =>
ThinCategory 'THIN 'THIN
Id
instance (Thin k) => CategoryOf (THINK k i j) where
  type (~>) = ThinCategory
  type Ob (a :: THINK k i j) = (a ~ THIN, Ob i, Ob j, HasArrow (Hom k) i j)

class (HasArrow (Hom k) a a) => HasIdArrow k a
instance (HasArrow (Hom k) a a) => HasIdArrow k a

class (Thin k, forall a. (Ob a) => HasIdArrow k a) => Thin' k
instance (Thin k, forall a. (Ob a) => HasIdArrow k a) => Thin' k

instance (Thin' k) => Bicategory (THINK k) where
  type Ob0 (THINK k) a = Ob a
  type I = THIN
  type O THIN THIN = THIN
  withOb2 :: forall {i :: k} {j :: k} {k :: k} (a :: THINK k j k)
       (b :: THINK k i j) r.
(Ob a, Ob b, Ob0 (THINK k) i, Ob0 (THINK k) j, Ob0 (THINK k) k) =>
(Ob (O a b) => r) -> r
withOb2 @(_ :: THINK k j l) @(_ :: THINK k i j) Ob (O a 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
forall (p :: k +-> k) (a :: k) (b :: k) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr @(Hom k) @i @l (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: k +-> k) (a :: k) (b :: k).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @(Hom k) @j @l Hom k j k -> (i ~> j) -> Hom k i k
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: k +-> k) (a :: k) (b :: k).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @(Hom k) @i @j) r
Ob (O a b) => r
(HasArrow (Hom k) i k, Ob i, Ob k) => r
r
  withOb0s :: forall {j :: k} {k :: k} (a :: THINK k j k) r.
Ob a =>
((Ob0 (THINK k) j, Ob0 (THINK k) k) => r) -> r
withOb0s (Ob0 (THINK k) j, Ob0 (THINK k) k) => r
r = r
(Ob0 (THINK k) j, Ob0 (THINK k) k) => r
r
  (Ob0 (THINK k) i, Ob0 (THINK k) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: k) (j :: k) (ps :: THINK k i j) (qs :: THINK k i j) r.
((Ob0 (THINK k) i, Ob0 (THINK k) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ ps ~> qs
ThinCategory ps qs
Id = r
(Ob0 (THINK k) i, Ob0 (THINK k) j, Ob ps, Ob qs) => r
r
  o :: forall {i :: k} {j :: k} {k :: k} (a :: THINK k j k)
       (b :: THINK k j k) (c :: THINK k i j) (d :: THINK k i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
o @a @_ @c a ~> b
ThinCategory a b
Id c ~> d
ThinCategory c d
Id = forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
forall (kk :: k +-> k) {i :: k} {j :: k} {k :: k} (a :: kk j k)
       (b :: kk i j) r.
(Bicategory kk, Ob a, Ob b, Ob0 kk i, Ob0 kk j, Ob0 kk k) =>
(Ob (O a b) => r) -> r
withOb2 @(THINK k) @a @c ThinCategory 'THIN 'THIN
Ob (O a c) => ThinCategory 'THIN 'THIN
forall {k} (i :: k) (j :: k).
(HasArrow (Hom k) i j, Ob i, Ob j) =>
ThinCategory 'THIN 'THIN
Id
  leftUnitor :: forall {i :: k} {j :: k} (a :: THINK k i j).
(Ob0 (THINK k) i, Ob0 (THINK k) j, Ob a) =>
O I a ~> a
leftUnitor = O I a ~> a
ThinCategory 'THIN 'THIN
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: THINK k i j). Ob a => ThinCategory a a
id
  leftUnitorInv :: forall {i :: k} {j :: k} (a :: THINK k i j).
(Ob0 (THINK k) i, Ob0 (THINK k) j, Ob a) =>
a ~> O I a
leftUnitorInv = a ~> O I a
ThinCategory 'THIN 'THIN
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: THINK k i j). Ob a => ThinCategory a a
id
  rightUnitor :: forall {i :: k} {j :: k} (a :: THINK k i j).
(Ob0 (THINK k) i, Ob0 (THINK k) j, Ob a) =>
O a I ~> a
rightUnitor = O a I ~> a
ThinCategory 'THIN 'THIN
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: THINK k i j). Ob a => ThinCategory a a
id
  rightUnitorInv :: forall {i :: k} {j :: k} (a :: THINK k i j).
(Ob0 (THINK k) i, Ob0 (THINK k) j, Ob a) =>
a ~> O a I
rightUnitorInv = a ~> O a I
ThinCategory 'THIN 'THIN
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: THINK k i j). Ob a => ThinCategory a a
id
  associator :: forall {h :: k} {i :: k} {j :: k} {k :: k} (a :: THINK k j k)
       (b :: THINK k i j) (c :: THINK k h i).
(Ob0 (THINK k) h, Ob0 (THINK k) i, Ob0 (THINK k) j,
 Ob0 (THINK k) k, Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator @p @q @r = forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: THINK k j k).
(CategoryOf (THINK k j k), Ob a) =>
Obj a
obj @p ('THIN ~> 'THIN)
-> ('THIN ~> 'THIN) -> O 'THIN 'THIN ~> O 'THIN 'THIN
forall {i :: k} {j :: k} {k :: k} (a :: THINK k j k)
       (b :: THINK k j k) (c :: THINK k i j) (d :: THINK k i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: THINK k i j).
(CategoryOf (THINK k i j), Ob a) =>
Obj a
obj @q (O 'THIN 'THIN ~> O 'THIN 'THIN)
-> ('THIN ~> 'THIN)
-> O (O 'THIN 'THIN) 'THIN ~> O (O 'THIN 'THIN) 'THIN
forall {i :: k} {j :: k} {k :: k} (a :: THINK k j k)
       (b :: THINK k j k) (c :: THINK k i j) (d :: THINK k i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: THINK k h i).
(CategoryOf (THINK k h i), Ob a) =>
Obj a
obj @r
  associatorInv :: forall {h :: k} {i :: k} {j :: k} {k :: k} (a :: THINK k j k)
       (b :: THINK k i j) (c :: THINK k h i).
(Ob0 (THINK k) h, Ob0 (THINK k) i, Ob0 (THINK k) j,
 Ob0 (THINK k) k, Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv @p @q @r = forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: THINK k j k).
(CategoryOf (THINK k j k), Ob a) =>
Obj a
obj @p ('THIN ~> 'THIN)
-> ('THIN ~> 'THIN) -> O 'THIN 'THIN ~> O 'THIN 'THIN
forall {i :: k} {j :: k} {k :: k} (a :: THINK k j k)
       (b :: THINK k j k) (c :: THINK k i j) (d :: THINK k i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: THINK k i j).
(CategoryOf (THINK k i j), Ob a) =>
Obj a
obj @q (O 'THIN 'THIN ~> O 'THIN 'THIN)
-> ('THIN ~> 'THIN)
-> O (O 'THIN 'THIN) 'THIN ~> O (O 'THIN 'THIN) 'THIN
forall {i :: k} {j :: k} {k :: k} (a :: THINK k j k)
       (b :: THINK k j k) (c :: THINK k i j) (d :: THINK k i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
forall {s} (kk :: CAT s) {i :: s} {j :: s} {k :: s} (a :: kk j k)
       (b :: kk j k) (c :: kk i j) (d :: kk i j).
Bicategory kk =>
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: THINK k h i).
(CategoryOf (THINK k h i), Ob a) =>
Obj a
obj @r

-- | A functor between thin categories, i.e. a monotone function.
data family ThinFunctor (p :: j +-> k) :: THINK j :-> THINK k

type instance Map0 (ThinFunctor p) a = p % a
type instance Map1 (ThinFunctor p) THIN = THIN
instance (Representable p, Thin' j, Thin' k) => LaxFunctor (ThinFunctor (p :: j +-> k)) where
  map2 :: forall {i :: j} {j :: j} (a :: THINK j i j) (b :: THINK j i j).
(Ob0 (THINK j) i, Ob0 (THINK j) j, Ob a, Ob b) =>
(a ~> b) -> Map1 (ThinFunctor p) a ~> Map1 (ThinFunctor p) b
map2 @a a ~> b
ThinCategory 'THIN 'THIN
Id = forall {sk} {sl} {kk :: CAT sk} {ll :: CAT sl} (f :: kk :-> ll)
       {i :: sk} {j :: sk} (a :: kk i j) r.
(LaxFunctor f, Ob0 kk i, Ob0 kk j, Ob a) =>
((Ob (Map1 f a), Ob0 ll (Map0 f i), Ob0 ll (Map0 f j)) => r) -> r
forall (f :: THINK j :-> THINK k) {i :: j} {j :: j}
       (a :: THINK j i j) r.
(LaxFunctor f, Ob0 (THINK j) i, Ob0 (THINK j) j, Ob a) =>
((Ob (Map1 f a), Ob0 (THINK k) (Map0 f i),
  Ob0 (THINK k) (Map0 f j)) =>
 r)
-> r
withMap1Ob @(ThinFunctor p) @a ThinCategory 'THIN 'THIN
(Ob (Map1 (ThinFunctor p) a),
 Ob0 (THINK k) (Map0 (ThinFunctor p) i),
 Ob0 (THINK k) (Map0 (ThinFunctor p) j)) =>
ThinCategory 'THIN 'THIN
forall {k} (i :: k) (j :: k).
(HasArrow (Hom k) i j, Ob i, Ob j) =>
ThinCategory 'THIN 'THIN
Id
  laxId :: forall (i :: Sort (THINK j)).
Ob0 (THINK j) i =>
I ~> Map1 (ThinFunctor p) I
laxId @i = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @i ThinCategory 'THIN 'THIN
Ob (p % i) => ThinCategory 'THIN 'THIN
forall {k} (i :: k) (j :: k).
(HasArrow (Hom k) i j, Ob i, Ob j) =>
ThinCategory 'THIN 'THIN
Id
  laxComp :: forall {i :: j} {j :: j} {k :: j} (a :: THINK j j k)
       (b :: THINK j i j).
(Ob0 (THINK j) i, Ob0 (THINK j) j, Ob0 (THINK j) k, Ob a, Ob b) =>
O (Map1 (ThinFunctor p) a) (Map1 (ThinFunctor p) b)
~> Map1 (ThinFunctor p) (O a b)
laxComp @(THIN :: THINK j b c) @(THIN :: THINK j a b) =
    ((p % i) ~> (p % k))
-> ((HasArrow (~>) (p % i) (p % k), Ob (p % i), Ob (p % k)) =>
    ThinCategory 'THIN 'THIN)
-> ThinCategory 'THIN 'THIN
forall (a :: k) (b :: k) r.
(a ~> b) -> ((HasArrow (~>) 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 (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: j +-> j) (a :: j) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @_ @b @c) ((p % j) ~> (p % k)) -> ((p % i) ~> (p % j)) -> (p % i) ~> (p % k)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: j +-> j) (a :: j) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @_ @a @b)) ThinCategory 'THIN 'THIN
(HasArrow (~>) (p % i) (p % k), Ob (p % i), Ob (p % k)) =>
ThinCategory 'THIN 'THIN
forall {k} (i :: k) (j :: k).
(HasArrow (Hom k) i j, Ob i, Ob j) =>
ThinCategory 'THIN 'THIN
Id
  withMap0Ob0 :: forall (i :: Sort (THINK j)) r.
Ob0 (THINK j) i =>
(Ob0 (THINK k) (Map0 (ThinFunctor p) i) => r) -> r
withMap0Ob0 @i Ob0 (THINK k) (Map0 (ThinFunctor p) i) => r
r = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @i r
Ob (p % i) => r
Ob0 (THINK k) (Map0 (ThinFunctor p) i) => r
r
  withMap1Ob :: forall {i :: j} {j :: j} (a :: THINK j i j) r.
(Ob0 (THINK j) i, Ob0 (THINK j) j, Ob a) =>
((Ob (Map1 (ThinFunctor p) a),
  Ob0 (THINK k) (Map0 (ThinFunctor p) i),
  Ob0 (THINK k) (Map0 (ThinFunctor p) j)) =>
 r)
-> r
withMap1Ob @(THIN :: THINK j a b) (Ob (Map1 (ThinFunctor p) a),
 Ob0 (THINK k) (Map0 (ThinFunctor p) i),
 Ob0 (THINK k) (Map0 (ThinFunctor p) j)) =>
r
r = ((p % i) ~> (p % j))
-> ((HasArrow (~>) (p % i) (p % j), Ob (p % i), Ob (p % j)) => r)
-> r
forall (a :: k) (b :: k) r.
(a ~> b) -> ((HasArrow (~>) 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 (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: j +-> j) (a :: j) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @_ @a @b)) r
(Ob (Map1 (ThinFunctor p) a),
 Ob0 (THINK k) (Map0 (ThinFunctor p) i),
 Ob0 (THINK k) (Map0 (ThinFunctor p) j)) =>
r
(HasArrow (~>) (p % i) (p % j), Ob (p % i), Ob (p % j)) => r
r