{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Bicategory.Adj where

import Data.Kind (Constraint, Type)
import Prelude (type (~))

import Proarrow.Category.Bicategory
  ( Adjunction_ (..)
  , Bicategory (..)
  , Comonad (..)
  , Monad (..)
  )
import Proarrow.Category.Bicategory qualified as Bi
import Proarrow.Category.Bicategory.Strictified (Assoc, Path (..), type (+++))
import Proarrow.Category.Equipment (Cotight, CotightAdjoint, Equipment (..), IsOb, Tight, TightAdjoint, WithObO2 (..))
import Proarrow.Category.Instance.Simplex (Nat (..), Simplex (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, obj)
import Proarrow.Object (src, tgt)

type data AB = A | B

type ABK :: CAT AB
type data ABK a b where
  L :: ABK A B
  R :: ABK B A

type ADJK :: CAT AB
type data ADJK i j = AK (Path ABK i j)
type instance UN AK (AK ps) = ps

type Adj :: CAT (ADJK i j)
data Adj ps qs where
  AdjNil :: Adj (AK Nil) (AK Nil)
  AdjR :: Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
  AdjL :: Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
  AdjCup :: Adj (AK ps) qs -> Adj (AK (R ::: L ::: ps)) qs
  AdjCap :: Adj ps (AK qs) -> Adj ps (AK (L ::: R ::: qs))

type SAdj :: Path ABK i j -> Type
data SAdj p where
  SNil :: SAdj Nil
  SL :: (IsLRPath ps) => SAdj (L ::: ps)
  SR :: (IsLRPath ps) => SAdj (R ::: ps)

type IsLRPath :: forall {i} {j}. Path ABK i j -> Constraint
class (ps +++ Nil ~ ps, forall i h (qs :: Path ABK k h) (rs :: Path ABK h i). Assoc ps qs rs) => IsLRPath (ps :: Path ABK j k) where
  singPath :: SAdj ps
  withIsPath2 :: (IsLRPath qs) => ((IsLRPath (ps +++ qs)) => r) -> r
instance IsLRPath Nil where
  singPath :: SAdj Nil
singPath = SAdj Nil
forall (k :: AB). SAdj Nil
SNil
  withIsPath2 :: forall {k :: AB} (qs :: Path ABK k k) r.
IsLRPath qs =>
(IsLRPath (Nil +++ qs) => r) -> r
withIsPath2 IsLRPath (Nil +++ qs) => r
r = r
IsLRPath (Nil +++ qs) => r
r
instance (IsLRPath ps) => IsLRPath (L ::: ps) where
  singPath :: SAdj (L ::: ps)
singPath = SAdj (L ::: ps)
forall (k :: AB) (ps :: Path ABK B k).
IsLRPath ps =>
SAdj (L ::: ps)
SL
  withIsPath2 :: forall {k :: AB} (qs :: Path ABK k k) r.
IsLRPath qs =>
(IsLRPath ((L ::: ps) +++ qs) => r) -> r
withIsPath2 @qs IsLRPath ((L ::: ps) +++ qs) => r
r = forall (ps :: Path ABK B k) {k :: AB} (qs :: Path ABK k k) r.
(IsLRPath ps, IsLRPath qs) =>
(IsLRPath (ps +++ qs) => r) -> r
forall {j :: AB} {k :: AB} (ps :: Path ABK j k) {k :: AB}
       (qs :: Path ABK k k) r.
(IsLRPath ps, IsLRPath qs) =>
(IsLRPath (ps +++ qs) => r) -> r
withIsPath2 @ps @qs r
IsLRPath ((L ::: ps) +++ qs) => r
IsLRPath (ps +++ qs) => r
r
instance (IsLRPath ps) => IsLRPath (R ::: ps) where
  singPath :: SAdj (R ::: ps)
singPath = SAdj (R ::: ps)
forall (k :: AB) (ps :: Path ABK A k).
IsLRPath ps =>
SAdj (R ::: ps)
SR
  withIsPath2 :: forall {k :: AB} (qs :: Path ABK k k) r.
IsLRPath qs =>
(IsLRPath ((R ::: ps) +++ qs) => r) -> r
withIsPath2 @qs IsLRPath ((R ::: ps) +++ qs) => r
r = forall (ps :: Path ABK A k) {k :: AB} (qs :: Path ABK k k) r.
(IsLRPath ps, IsLRPath qs) =>
(IsLRPath (ps +++ qs) => r) -> r
forall {j :: AB} {k :: AB} (ps :: Path ABK j k) {k :: AB}
       (qs :: Path ABK k k) r.
(IsLRPath ps, IsLRPath qs) =>
(IsLRPath (ps +++ qs) => r) -> r
withIsPath2 @ps @qs r
IsLRPath (ps +++ qs) => r
IsLRPath ((R ::: ps) +++ qs) => r
r

instance Profunctor (Adj :: CAT (ADJK a b)) where
  dimap :: forall (c :: ADJK a b) (a :: ADJK a b) (b :: ADJK a b)
       (d :: ADJK a b).
(c ~> a) -> (b ~> d) -> Adj a b -> Adj c d
dimap = (c ~> a) -> (b ~> d) -> Adj a b -> Adj c d
Adj c a -> Adj b d -> Adj a b -> Adj 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 :: ADJK a b) (b :: ADJK a b) r.
((Ob a, Ob b) => r) -> Adj a b -> r
\\ Adj a b
AdjNil = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ AdjR Adj (AK ps) (AK qs)
f = r
(Ob a, Ob b) => r
(Ob (AK ps), Ob (AK qs)) => r
r ((Ob (AK ps), Ob (AK qs)) => r) -> Adj (AK ps) (AK qs) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ADJK A b) (b :: ADJK A b) r.
((Ob a, Ob b) => r) -> Adj a b -> r
\\ Adj (AK ps) (AK qs)
f
  (Ob a, Ob b) => r
r \\ AdjL Adj (AK ps) (AK qs)
f = r
(Ob a, Ob b) => r
(Ob (AK ps), Ob (AK qs)) => r
r ((Ob (AK ps), Ob (AK qs)) => r) -> Adj (AK ps) (AK qs) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ADJK B b) (b :: ADJK B b) r.
((Ob a, Ob b) => r) -> Adj a b -> r
\\ Adj (AK ps) (AK qs)
f
  (Ob a, Ob b) => r
r \\ AdjCup Adj (AK ps) qs
f = r
(Ob a, Ob b) => r
(Ob (AK ps), Ob qs) => r
r ((Ob (AK ps), Ob qs) => r) -> Adj (AK ps) qs -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ADJK B b) (b :: ADJK B b) r.
((Ob a, Ob b) => r) -> Adj a b -> r
\\ Adj (AK ps) qs
f
  (Ob a, Ob b) => r
r \\ AdjCap Adj ps (AK qs)
f = r
(Ob a, Ob b) => r
(Ob ps, Ob (AK qs)) => r
r ((Ob ps, Ob (AK qs)) => r) -> Adj ps (AK qs) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ADJK A b) (b :: ADJK A b) r.
((Ob a, Ob b) => r) -> Adj a b -> r
\\ Adj ps (AK qs)
f
instance Promonad (Adj :: CAT (ADJK a b)) where
  id :: forall (a :: ADJK a b). Ob a => Adj a a
id @ps = SAdj (UN AK a) -> Adj (AK (UN AK a)) (AK (UN AK a))
forall {i :: AB} {j :: AB} (ps' :: Path ABK i j).
SAdj ps' -> Adj (AK ps') (AK ps')
go (forall (ps :: Path ABK a b). IsLRPath ps => SAdj ps
forall {j :: AB} {k :: AB} (ps :: Path ABK j k).
IsLRPath ps =>
SAdj ps
singPath @(UN AK ps))
    where
      go :: forall ps'. SAdj ps' -> Adj (AK ps') (AK ps')
      go :: forall {i :: AB} {j :: AB} (ps' :: Path ABK i j).
SAdj ps' -> Adj (AK ps') (AK ps')
go SAdj ps'
SNil = Adj (AK Nil) (AK Nil)
Adj (AK ps') (AK ps')
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil
      go SAdj ps'
SL = Adj (AK ps) (AK ps) -> Adj (AK (L ::: ps)) (AK (L ::: ps))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL Adj (AK ps) (AK ps)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ADJK B j). Ob a => Adj a a
id
      go SAdj ps'
SR = Adj (AK ps) (AK ps) -> Adj (AK (R ::: ps)) (AK (R ::: ps))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR Adj (AK ps) (AK ps)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ADJK A j). Ob a => Adj a a
id
  Adj b c
AdjNil . :: forall (b :: ADJK a b) (c :: ADJK a b) (a :: ADJK a b).
Adj b c -> Adj a b -> Adj a c
. Adj a b
f = Adj a b
Adj a c
f
  Adj b c
f . Adj a b
AdjNil = Adj b c
Adj a c
f
  AdjR Adj (AK ps) (AK qs)
f . AdjR Adj (AK ps) (AK qs)
g = Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR (Adj (AK ps) (AK qs)
f Adj (AK ps) (AK qs) -> Adj (AK ps) (AK ps) -> Adj (AK ps) (AK qs)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ADJK A b) (c :: ADJK A b) (a :: ADJK A b).
Adj b c -> Adj a b -> Adj a c
. Adj (AK ps) (AK ps)
Adj (AK ps) (AK qs)
g)
  AdjL Adj (AK ps) (AK qs)
f . AdjL Adj (AK ps) (AK qs)
g = Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL (Adj (AK ps) (AK qs)
f Adj (AK ps) (AK qs) -> Adj (AK ps) (AK ps) -> Adj (AK ps) (AK qs)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ADJK B b) (c :: ADJK B b) (a :: ADJK B b).
Adj b c -> Adj a b -> Adj a c
. Adj (AK ps) (AK ps)
Adj (AK ps) (AK qs)
g)
  Adj b c
f . AdjCup Adj (AK ps) qs
g = Adj (AK ps) c -> Adj (AK (R ::: (L ::: ps))) c
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup (Adj b c
Adj qs c
f Adj qs c -> Adj (AK ps) qs -> Adj (AK ps) c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ADJK B b) (c :: ADJK B b) (a :: ADJK B b).
Adj b c -> Adj a b -> Adj a c
. Adj (AK ps) qs
g)
  AdjCap Adj ps (AK qs)
f . Adj a b
g = Adj a (AK qs) -> Adj a (AK (L ::: (R ::: qs)))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap (Adj ps (AK qs)
f Adj ps (AK qs) -> Adj a ps -> Adj a (AK qs)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ADJK A b) (c :: ADJK A b) (a :: ADJK A b).
Adj b c -> Adj a b -> Adj a c
. Adj a b
Adj a ps
g)
  AdjL (AdjR Adj (AK ps) (AK qs)
f) . AdjCap Adj ps (AK qs)
g = Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap (Adj (AK ps) (AK qs)
f Adj (AK ps) (AK qs) -> Adj ps (AK ps) -> Adj ps (AK qs)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ADJK A b) (c :: ADJK A b) (a :: ADJK A b).
Adj b c -> Adj a b -> Adj a c
. Adj ps (AK ps)
Adj ps (AK qs)
g)
  AdjCup Adj (AK ps) qs
f . AdjR (AdjL Adj (AK ps) (AK qs)
g) = Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup (Adj (AK ps) qs
f Adj (AK ps) qs -> Adj (AK ps) (AK ps) -> Adj (AK ps) qs
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ADJK B b) (c :: ADJK B b) (a :: ADJK B b).
Adj b c -> Adj a b -> Adj a c
. Adj (AK ps) (AK ps)
Adj (AK ps) (AK qs)
g)
  AdjL (AdjCup Adj (AK ps) qs
f) . AdjCap Adj ps (AK qs)
g = Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL Adj (AK ps) qs
Adj (AK ps) (AK qs)
f Adj (AK (L ::: ps)) c -> Adj a (AK (L ::: ps)) -> Adj 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 (b :: ADJK a b) (c :: ADJK a b) (a :: ADJK a b).
Adj b c -> Adj a b -> Adj a c
. Adj a (AK (L ::: ps))
Adj ps (AK qs)
g -- zigzag
  AdjCup Adj (AK ps) qs
f . AdjR (AdjCap Adj ps (AK qs)
g) = Adj (AK (R ::: qs)) c
Adj (AK ps) qs
f Adj (AK (R ::: qs)) c -> Adj a (AK (R ::: qs)) -> Adj 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 (b :: ADJK a b) (c :: ADJK a b) (a :: ADJK a b).
Adj b c -> Adj a b -> Adj a c
. Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR Adj ps (AK qs)
Adj (AK ps) (AK qs)
g -- zagzig

instance CategoryOf (ADJK a b) where
  type (~>) = Adj
  type Ob ps = (Is AK ps, IsLRPath (UN AK ps))

-- | The walking adjunction
instance Bicategory ADJK where
  type I = AK Nil
  type ps `O` qs = AK (UN AK qs +++ UN AK ps)
  withOb2 :: forall {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k)
       (b :: ADJK i j) r.
(Ob a, Ob b, Ob0 ADJK i, Ob0 ADJK j, Ob0 ADJK k) =>
(Ob (O a b) => r) -> r
withOb2 @ps @qs Ob (O a b) => r
k = forall (ps :: Path ABK i j) {k :: AB} (qs :: Path ABK j k) r.
(IsLRPath ps, IsLRPath qs) =>
(IsLRPath (ps +++ qs) => r) -> r
forall {j :: AB} {k :: AB} (ps :: Path ABK j k) {k :: AB}
       (qs :: Path ABK k k) r.
(IsLRPath ps, IsLRPath qs) =>
(IsLRPath (ps +++ qs) => r) -> r
withIsPath2 @(UN AK qs) @(UN AK ps) r
Ob (O a b) => r
IsLRPath (UN AK b +++ UN AK a) => r
k
  withOb0s :: forall {j :: AB} {k :: AB} (a :: ADJK j k) r.
Ob a =>
((Ob0 ADJK j, Ob0 ADJK k) => r) -> r
withOb0s (Ob0 ADJK j, Ob0 ADJK k) => r
r = r
(Ob0 ADJK j, Ob0 ADJK k) => r
r
  (Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: AB) (j :: AB) (ps :: ADJK i j) (qs :: ADJK i j) r.
((Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ ps ~> qs
Adj ps qs
AdjNil = r
(Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
r
  (Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
r \\\ AdjR Adj (AK ps) (AK qs)
f = r
(Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
(Ob0 ADJK A, Ob0 ADJK j, Ob (AK ps), Ob (AK qs)) => r
r ((Ob0 ADJK A, Ob0 ADJK j, Ob (AK ps), Ob (AK qs)) => r)
-> (AK ps ~> AK qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall (i :: AB) (j :: AB) (ps :: ADJK i j) (qs :: ADJK i j) r.
((Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ AK ps ~> AK qs
Adj (AK ps) (AK qs)
f
  (Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
r \\\ AdjL Adj (AK ps) (AK qs)
f = r
(Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
(Ob0 ADJK B, Ob0 ADJK j, Ob (AK ps), Ob (AK qs)) => r
r ((Ob0 ADJK B, Ob0 ADJK j, Ob (AK ps), Ob (AK qs)) => r)
-> (AK ps ~> AK qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall (i :: AB) (j :: AB) (ps :: ADJK i j) (qs :: ADJK i j) r.
((Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ AK ps ~> AK qs
Adj (AK ps) (AK qs)
f
  (Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
r \\\ AdjCup Adj (AK ps) qs
f = r
(Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
(Ob0 ADJK i, Ob0 ADJK j, Ob (AK ps), Ob qs) => r
r ((Ob0 ADJK i, Ob0 ADJK j, Ob (AK ps), Ob qs) => r)
-> (AK ps ~> qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall (i :: AB) (j :: AB) (ps :: ADJK i j) (qs :: ADJK i j) r.
((Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ AK ps ~> qs
Adj (AK ps) qs
f
  (Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
r \\\ AdjCap Adj ps (AK qs)
f = r
(Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r
(Ob0 ADJK A, Ob0 ADJK j, Ob ps, Ob (AK qs)) => r
r ((Ob0 ADJK A, Ob0 ADJK j, Ob ps, Ob (AK qs)) => r)
-> (ps ~> AK qs) -> r
forall {s} (kk :: CAT s) (i :: s) (j :: s) (ps :: kk i j)
       (qs :: kk i j) r.
Bicategory kk =>
((Ob0 kk i, Ob0 kk j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
forall (i :: AB) (j :: AB) (ps :: ADJK i j) (qs :: ADJK i j) r.
((Ob0 ADJK i, Ob0 ADJK j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r
\\\ ps ~> AK qs
Adj ps (AK qs)
f
  o :: forall {a} {b} (ps :: ADJK a b) qs rs ss. (ps ~> qs) -> (rs ~> ss) -> (ps `O` rs) ~> (qs `O` ss)
  ps ~> qs
Adj ps qs
AdjNil o :: forall {i :: AB} (j :: AB) (k :: AB) (a :: ADJK j k)
       (b :: ADJK j k) (c :: ADJK i j) (d :: ADJK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` rs ~> ss
f = rs ~> ss
Adj (AK (UN AK rs +++ Nil)) (AK (UN AK ss +++ Nil))
(Ob rs, Ob ss) =>
Adj (AK (UN AK rs +++ Nil)) (AK (UN AK ss +++ Nil))
f ((Ob rs, Ob ss) =>
 Adj (AK (UN AK rs +++ Nil)) (AK (UN AK ss +++ Nil)))
-> Adj rs ss -> Adj (AK (UN AK rs +++ Nil)) (AK (UN AK ss +++ Nil))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ADJK i a) (b :: ADJK i a) r.
((Ob a, Ob b) => r) -> Adj a b -> r
\\ rs ~> ss
Adj rs ss
f
  ps ~> qs
f `o` rs ~> ss
Adj rs ss
AdjNil = ps ~> qs
Adj (AK (UN AK ps)) (AK (UN AK qs))
(Ob ps, Ob qs) => Adj (AK (UN AK ps)) (AK (UN AK qs))
f ((Ob ps, Ob qs) => Adj (AK (UN AK ps)) (AK (UN AK qs)))
-> Adj ps qs -> Adj (AK (UN AK ps)) (AK (UN AK qs))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ADJK a b) (b :: ADJK a b) r.
((Ob a, Ob b) => r) -> Adj a b -> r
\\ ps ~> qs
Adj ps qs
f
  ps ~> qs
f `o` AdjR Adj (AK ps) (AK qs)
g = Adj (AK (ps +++ UN AK ps)) (AK (qs +++ UN AK qs))
-> Adj
     (AK (R ::: (ps +++ UN AK ps))) (AK (R ::: (qs +++ UN AK qs)))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR (ps ~> qs
f (ps ~> qs) -> (AK ps ~> AK qs) -> O ps (AK ps) ~> O qs (AK qs)
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
forall {i :: AB} (j :: AB) (k :: AB) (a :: ADJK j k)
       (b :: ADJK j k) (c :: ADJK i j) (d :: ADJK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` AK ps ~> AK qs
Adj (AK ps) (AK qs)
g)
  ps ~> qs
f `o` AdjL Adj (AK ps) (AK qs)
g = Adj (AK (ps +++ UN AK ps)) (AK (qs +++ UN AK qs))
-> Adj
     (AK (L ::: (ps +++ UN AK ps))) (AK (L ::: (qs +++ UN AK qs)))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL (ps ~> qs
f (ps ~> qs) -> (AK ps ~> AK qs) -> O ps (AK ps) ~> O qs (AK qs)
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
forall {i :: AB} (j :: AB) (k :: AB) (a :: ADJK j k)
       (b :: ADJK j k) (c :: ADJK i j) (d :: ADJK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` AK ps ~> AK qs
Adj (AK ps) (AK qs)
g)
  ps ~> qs
f `o` AdjCup Adj (AK ps) qs
g = Adj (AK (ps +++ UN AK ps)) (AK (UN AK ss +++ UN AK qs))
-> Adj
     (AK (R ::: (L ::: (ps +++ UN AK ps)))) (AK (UN AK ss +++ UN AK qs))
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup (ps ~> qs
f (ps ~> qs) -> (AK ps ~> ss) -> O ps (AK ps) ~> O qs ss
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
forall {i :: AB} (j :: AB) (k :: AB) (a :: ADJK j k)
       (b :: ADJK j k) (c :: ADJK i j) (d :: ADJK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` AK ps ~> ss
Adj (AK ps) qs
g)
  ps ~> qs
f `o` AdjCap Adj ps (AK qs)
g = Adj (AK (UN AK rs +++ UN AK ps)) (AK (qs +++ UN AK qs))
-> Adj
     (AK (UN AK rs +++ UN AK ps)) (AK (L ::: (R ::: (qs +++ UN AK qs))))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap (ps ~> qs
f (ps ~> qs) -> (rs ~> AK qs) -> O ps rs ~> O qs (AK qs)
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
forall {i :: AB} (j :: AB) (k :: AB) (a :: ADJK j k)
       (b :: ADJK j k) (c :: ADJK i j) (d :: ADJK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` rs ~> AK qs
Adj ps (AK qs)
g)
  leftUnitor :: forall {i :: AB} {j :: AB} (a :: ADJK i j).
(Ob0 ADJK i, Ob0 ADJK j, Ob a) =>
O I a ~> a
leftUnitor = O I a ~> a
Adj (AK (UN AK a)) (AK (UN AK a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ADJK i j). Ob a => Adj a a
id
  leftUnitorInv :: forall {i :: AB} {j :: AB} (a :: ADJK i j).
(Ob0 ADJK i, Ob0 ADJK j, Ob a) =>
a ~> O I a
leftUnitorInv = a ~> O I a
Adj (AK (UN AK a)) (AK (UN AK a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ADJK i j). Ob a => Adj a a
id
  rightUnitor :: forall {i :: AB} {j :: AB} (a :: ADJK i j).
(Ob0 ADJK i, Ob0 ADJK j, Ob a) =>
O a I ~> a
rightUnitor = O a I ~> a
Adj (AK (UN AK a)) (AK (UN AK a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ADJK i j). Ob a => Adj a a
id
  rightUnitorInv :: forall {i :: AB} {j :: AB} (a :: ADJK i j).
(Ob0 ADJK i, Ob0 ADJK j, Ob a) =>
a ~> O a I
rightUnitorInv = a ~> O a I
Adj (AK (UN AK a)) (AK (UN AK a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ADJK i j). Ob a => Adj a a
id
  associator :: forall {h :: AB} {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k)
       (b :: ADJK i j) (c :: ADJK h i).
(Ob0 ADJK h, Ob0 ADJK i, Ob0 ADJK j, Ob0 ADJK 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 :: ADJK j k). (CategoryOf (ADJK j k), Ob a) => Obj a
obj @p (AK (UN AK a) ~> AK (UN AK a))
-> (AK (UN AK b) ~> AK (UN AK b))
-> O (AK (UN AK a)) (AK (UN AK b))
   ~> O (AK (UN AK a)) (AK (UN AK b))
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
forall {i :: AB} (j :: AB) (k :: AB) (a :: ADJK j k)
       (b :: ADJK j k) (c :: ADJK i j) (d :: ADJK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ADJK i j). (CategoryOf (ADJK i j), Ob a) => Obj a
obj @q (AK (UN AK (AK (UN AK b)) +++ UN AK (AK (UN AK a)))
 ~> AK (UN AK (AK (UN AK b)) +++ UN AK (AK (UN AK a))))
-> (AK (UN AK c) ~> AK (UN AK c))
-> O (AK (UN AK (AK (UN AK b)) +++ UN AK (AK (UN AK a))))
     (AK (UN AK c))
   ~> O (AK (UN AK (AK (UN AK b)) +++ UN AK (AK (UN AK a))))
        (AK (UN AK c))
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
forall {i :: AB} (j :: AB) (k :: AB) (a :: ADJK j k)
       (b :: ADJK j k) (c :: ADJK i j) (d :: ADJK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ADJK h i). (CategoryOf (ADJK h i), Ob a) => Obj a
obj @r
  associatorInv :: forall {h :: AB} {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k)
       (b :: ADJK i j) (c :: ADJK h i).
(Ob0 ADJK h, Ob0 ADJK i, Ob0 ADJK j, Ob0 ADJK 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 :: ADJK j k). (CategoryOf (ADJK j k), Ob a) => Obj a
obj @p (AK (UN AK a) ~> AK (UN AK a))
-> (AK (UN AK b) ~> AK (UN AK b))
-> O (AK (UN AK a)) (AK (UN AK b))
   ~> O (AK (UN AK a)) (AK (UN AK b))
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
forall {i :: AB} (j :: AB) (k :: AB) (a :: ADJK j k)
       (b :: ADJK j k) (c :: ADJK i j) (d :: ADJK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ADJK i j). (CategoryOf (ADJK i j), Ob a) => Obj a
obj @q (AK (UN AK (AK (UN AK b)) +++ UN AK (AK (UN AK a)))
 ~> AK (UN AK (AK (UN AK b)) +++ UN AK (AK (UN AK a))))
-> (AK (UN AK c) ~> AK (UN AK c))
-> O (AK (UN AK (AK (UN AK b)) +++ UN AK (AK (UN AK a))))
     (AK (UN AK c))
   ~> O (AK (UN AK (AK (UN AK b)) +++ UN AK (AK (UN AK a))))
        (AK (UN AK c))
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
forall {i :: AB} (j :: AB) (k :: AB) (a :: ADJK j k)
       (b :: ADJK j k) (c :: ADJK i j) (d :: ADJK i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ADJK h i). (CategoryOf (ADJK h i), Ob a) => Obj a
obj @r

type family RepLR (n :: Nat) :: Path ABK A A where
  RepLR Z = Nil
  RepLR (S n) = L ::: R ::: RepLR n

-- | Adj(A, A) is the walking monoid
fromSimplex :: Simplex a b -> Adj (AK (RepLR a)) (AK (RepLR b))
fromSimplex :: forall (a :: Nat) (b :: Nat).
Simplex a b -> Adj (AK (RepLR a)) (AK (RepLR b))
fromSimplex Simplex a b
ZZ = Adj (AK Nil) (AK Nil)
Adj (AK (RepLR a)) (AK (RepLR b))
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil
fromSimplex (Y Simplex a y
n) = Adj (AK (RepLR a)) (AK (RepLR y))
-> Adj (AK (RepLR a)) (AK (L ::: (R ::: RepLR y)))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap (Simplex a y -> Adj (AK (RepLR a)) (AK (RepLR y))
forall (a :: Nat) (b :: Nat).
Simplex a b -> Adj (AK (RepLR a)) (AK (RepLR b))
fromSimplex Simplex a y
n)
fromSimplex (X (Y Simplex x y
n)) = Adj (AK (R ::: RepLR x)) (AK (R ::: RepLR y))
-> Adj (AK (L ::: (R ::: RepLR x))) (AK (L ::: (R ::: RepLR y)))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL (Adj (AK (RepLR x)) (AK (RepLR y))
-> Adj (AK (R ::: RepLR x)) (AK (R ::: RepLR y))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR (Simplex x y -> Adj (AK (RepLR x)) (AK (RepLR y))
forall (a :: Nat) (b :: Nat).
Simplex a b -> Adj (AK (RepLR a)) (AK (RepLR b))
fromSimplex Simplex x y
n))
fromSimplex (X (X Simplex x (S y)
n)) = Simplex (S x) (S y) -> Adj (AK (RepLR (S x))) (AK (RepLR (S y)))
forall (a :: Nat) (b :: Nat).
Simplex a b -> Adj (AK (RepLR a)) (AK (RepLR b))
fromSimplex (Simplex x (S y) -> Simplex (S x) (S y)
forall (x :: Nat) (y :: Nat).
Simplex x (S y) -> Simplex (S x) (S y)
X Simplex x (S y)
n) Adj (AK (L ::: (R ::: RepLR x))) (AK (L ::: (R ::: RepLR y)))
-> Adj
     (AK (L ::: (R ::: (L ::: (R ::: RepLR x)))))
     (AK (L ::: (R ::: RepLR x)))
-> Adj
     (AK (L ::: (R ::: (L ::: (R ::: RepLR x)))))
     (AK (L ::: (R ::: RepLR y)))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ADJK A A) (c :: ADJK A A) (a :: ADJK A A).
Adj b c -> Adj a b -> Adj a c
. Adj (AK (R ::: (L ::: (R ::: RepLR x)))) (AK (R ::: RepLR x))
-> Adj
     (AK (L ::: (R ::: (L ::: (R ::: RepLR x)))))
     (AK (L ::: (R ::: RepLR x)))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL (Adj (AK (R ::: RepLR x)) (AK (R ::: RepLR x))
-> Adj (AK (R ::: (L ::: (R ::: RepLR x)))) (AK (R ::: RepLR x))
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup (Adj (AK (RepLR x)) (AK (RepLR x))
-> Adj (AK (R ::: RepLR x)) (AK (R ::: RepLR x))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR (Adj (AK (RepLR x)) (AK (L ::: (R ::: RepLR y)))
-> Obj (AK (RepLR x))
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src (Simplex x (S y) -> Adj (AK (RepLR x)) (AK (RepLR (S y)))
forall (a :: Nat) (b :: Nat).
Simplex a b -> Adj (AK (RepLR a)) (AK (RepLR b))
fromSimplex Simplex x (S y)
n))))

type family CountLR (ps :: Path ABK A A) :: Nat where
  CountLR Nil = Z
  CountLR (L ::: ps) = S (CountLR' ps)

type family CountLR' (ps :: Path ABK B A) :: Nat where
  CountLR' (R ::: n) = CountLR n

toSimplex :: Adj (AK a) (AK b) -> Simplex (CountLR a) (CountLR b)
toSimplex :: forall (a :: Path ABK A A) (b :: Path ABK A A).
Adj (AK a) (AK b) -> Simplex (CountLR a) (CountLR b)
toSimplex Adj (AK a) (AK b)
AdjNil = Simplex Z Z
Simplex (CountLR a) (CountLR b)
ZZ
toSimplex (AdjCap Adj ps (AK qs)
f) = Simplex (CountLR a) (CountLR qs)
-> Simplex (CountLR a) (S (CountLR qs))
forall (a :: Nat) (y :: Nat). Simplex a y -> Simplex a (S y)
Y (Adj (AK a) (AK qs) -> Simplex (CountLR a) (CountLR qs)
forall (a :: Path ABK A A) (b :: Path ABK A A).
Adj (AK a) (AK b) -> Simplex (CountLR a) (CountLR b)
toSimplex Adj ps (AK qs)
Adj (AK a) (AK qs)
f)
toSimplex (AdjL Adj (AK ps) (AK qs)
f) = Adj (AK ps) (AK qs)
-> (Simplex (S (CountLR' ps)) (S (CountLR' qs))
    -> Simplex (S (CountLR' ps)) (S (CountLR' qs)))
-> Simplex (S (CountLR' ps)) (S (CountLR' qs))
forall (f :: Path ABK B A) (g :: Path ABK B A) r.
Adj (AK f) (AK g)
-> (Simplex (S (CountLR' f)) (S (CountLR' g)) -> r) -> r
go Adj (AK ps) (AK qs)
f Simplex (S (CountLR' ps)) (S (CountLR' qs))
-> Simplex (S (CountLR' ps)) (S (CountLR' qs))
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  where
    go :: Adj (AK f) (AK g) -> (Simplex (S (CountLR' f)) (S (CountLR' g)) -> r) -> r
    go :: forall (f :: Path ABK B A) (g :: Path ABK B A) r.
Adj (AK f) (AK g)
-> (Simplex (S (CountLR' f)) (S (CountLR' g)) -> r) -> r
go (AdjR Adj (AK ps) (AK qs)
g) Simplex (S (CountLR' f)) (S (CountLR' g)) -> r
xny = Simplex (S (CountLR' f)) (S (CountLR' g)) -> r
xny (Simplex (CountLR ps) (S (CountLR qs))
-> Simplex (S (CountLR ps)) (S (CountLR qs))
forall (x :: Nat) (y :: Nat).
Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex (CountLR ps) (CountLR qs)
-> Simplex (CountLR ps) (S (CountLR qs))
forall (a :: Nat) (y :: Nat). Simplex a y -> Simplex a (S y)
Y (Adj (AK ps) (AK qs) -> Simplex (CountLR ps) (CountLR qs)
forall (a :: Path ABK A A) (b :: Path ABK A A).
Adj (AK a) (AK b) -> Simplex (CountLR a) (CountLR b)
toSimplex Adj (AK ps) (AK qs)
g)))
    go (AdjCup Adj (AK ps) qs
g) Simplex (S (CountLR' f)) (S (CountLR' g)) -> r
xny = Adj (AK ps) (AK g)
-> (Simplex (S (CountLR' ps)) (S (CountLR' g)) -> r) -> r
forall (f :: Path ABK B A) (g :: Path ABK B A) r.
Adj (AK f) (AK g)
-> (Simplex (S (CountLR' f)) (S (CountLR' g)) -> r) -> r
go Adj (AK ps) qs
Adj (AK ps) (AK g)
g (Simplex (S (S (CountLR' ps))) (S (CountLR' g)) -> r
Simplex (S (CountLR' f)) (S (CountLR' g)) -> r
xny (Simplex (S (S (CountLR' ps))) (S (CountLR' g)) -> r)
-> (Simplex (S (CountLR' ps)) (S (CountLR' g))
    -> Simplex (S (S (CountLR' ps))) (S (CountLR' g)))
-> Simplex (S (CountLR' ps)) (S (CountLR' g))
-> r
forall b c a. (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
. Simplex (S (CountLR' ps)) (S (CountLR' g))
-> Simplex (S (S (CountLR' ps))) (S (CountLR' g))
forall (x :: Nat) (y :: Nat).
Simplex x (S y) -> Simplex (S x) (S y)
X)

type family RepRL (n :: Nat) :: Path ABK B B where
  RepRL Z = Nil
  RepRL (S n) = R ::: L ::: RepRL n

-- | Adj(B, B) is the walking comonoid
fromSimplexOp :: Simplex b a -> Adj (AK (RepRL a)) (AK (RepRL b))
fromSimplexOp :: forall (b :: Nat) (a :: Nat).
Simplex b a -> Adj (AK (RepRL a)) (AK (RepRL b))
fromSimplexOp Simplex b a
ZZ = Adj (AK Nil) (AK Nil)
Adj (AK (RepRL a)) (AK (RepRL b))
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil
fromSimplexOp (Y Simplex b y
n) = Adj (AK (RepRL y)) (AK (RepRL b))
-> Adj (AK (R ::: (L ::: RepRL y))) (AK (RepRL b))
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup (Simplex b y -> Adj (AK (RepRL y)) (AK (RepRL b))
forall (b :: Nat) (a :: Nat).
Simplex b a -> Adj (AK (RepRL a)) (AK (RepRL b))
fromSimplexOp Simplex b y
n)
fromSimplexOp (X (Y Simplex x y
n)) = Adj (AK (L ::: RepRL y)) (AK (L ::: RepRL x))
-> Adj (AK (R ::: (L ::: RepRL y))) (AK (R ::: (L ::: RepRL x)))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR (Adj (AK (RepRL y)) (AK (RepRL x))
-> Adj (AK (L ::: RepRL y)) (AK (L ::: RepRL x))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL (Simplex x y -> Adj (AK (RepRL y)) (AK (RepRL x))
forall (b :: Nat) (a :: Nat).
Simplex b a -> Adj (AK (RepRL a)) (AK (RepRL b))
fromSimplexOp Simplex x y
n))
fromSimplexOp (X (X Simplex x (S y)
n)) = Adj (AK (L ::: RepRL x)) (AK (L ::: (R ::: (L ::: RepRL x))))
-> Adj
     (AK (R ::: (L ::: RepRL x)))
     (AK (R ::: (L ::: (R ::: (L ::: RepRL x)))))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR (Adj (AK (L ::: RepRL x)) (AK (L ::: RepRL x))
-> Adj (AK (L ::: RepRL x)) (AK (L ::: (R ::: (L ::: RepRL x))))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap (Adj (AK (RepRL x)) (AK (RepRL x))
-> Adj (AK (L ::: RepRL x)) (AK (L ::: RepRL x))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL (Adj (AK (R ::: (L ::: RepRL y))) (AK (RepRL x))
-> Obj (AK (RepRL x))
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt (Simplex x (S y) -> Adj (AK (RepRL (S y))) (AK (RepRL x))
forall (b :: Nat) (a :: Nat).
Simplex b a -> Adj (AK (RepRL a)) (AK (RepRL b))
fromSimplexOp Simplex x (S y)
n)))) Adj
  (AK (R ::: (L ::: RepRL x)))
  (AK (R ::: (L ::: (R ::: (L ::: RepRL x)))))
-> Adj (AK (R ::: (L ::: RepRL y))) (AK (R ::: (L ::: RepRL x)))
-> Adj
     (AK (R ::: (L ::: RepRL y)))
     (AK (R ::: (L ::: (R ::: (L ::: RepRL x)))))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ADJK B B) (c :: ADJK B B) (a :: ADJK B B).
Adj b c -> Adj a b -> Adj a c
. Simplex (S x) (S y) -> Adj (AK (RepRL (S y))) (AK (RepRL (S x)))
forall (b :: Nat) (a :: Nat).
Simplex b a -> Adj (AK (RepRL a)) (AK (RepRL b))
fromSimplexOp (Simplex x (S y) -> Simplex (S x) (S y)
forall (x :: Nat) (y :: Nat).
Simplex x (S y) -> Simplex (S x) (S y)
X Simplex x (S y)
n)

type family CountRL (ps :: Path ABK B B) :: Nat where
  CountRL Nil = Z
  CountRL (R ::: ps) = S (CountRL' ps)

type family CountRL' (ps :: Path ABK A B) :: Nat where
  CountRL' (L ::: n) = CountRL n

toSimplexOp :: Adj (AK a) (AK b) -> Simplex (CountRL b) (CountRL a)
toSimplexOp :: forall (a :: Path ABK B B) (b :: Path ABK B B).
Adj (AK a) (AK b) -> Simplex (CountRL b) (CountRL a)
toSimplexOp Adj (AK a) (AK b)
AdjNil = Simplex Z Z
Simplex (CountRL b) (CountRL a)
ZZ
toSimplexOp (AdjCup Adj (AK ps) qs
f) = Simplex (CountRL b) (CountRL ps)
-> Simplex (CountRL b) (S (CountRL ps))
forall (a :: Nat) (y :: Nat). Simplex a y -> Simplex a (S y)
Y (Adj (AK ps) (AK b) -> Simplex (CountRL b) (CountRL ps)
forall (a :: Path ABK B B) (b :: Path ABK B B).
Adj (AK a) (AK b) -> Simplex (CountRL b) (CountRL a)
toSimplexOp Adj (AK ps) qs
Adj (AK ps) (AK b)
f)
toSimplexOp (AdjR Adj (AK ps) (AK qs)
f) = Adj (AK ps) (AK qs)
-> (Simplex (S (CountRL' qs)) (S (CountRL' ps))
    -> Simplex (S (CountRL' qs)) (S (CountRL' ps)))
-> Simplex (S (CountRL' qs)) (S (CountRL' ps))
forall (f :: Path ABK A B) (g :: Path ABK A B) r.
Adj (AK f) (AK g)
-> (Simplex (S (CountRL' g)) (S (CountRL' f)) -> r) -> r
go Adj (AK ps) (AK qs)
f Simplex (S (CountRL' qs)) (S (CountRL' ps))
-> Simplex (S (CountRL' qs)) (S (CountRL' ps))
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  where
    go :: Adj (AK f) (AK g) -> (Simplex (S (CountRL' g)) (S (CountRL' f)) -> r) -> r
    go :: forall (f :: Path ABK A B) (g :: Path ABK A B) r.
Adj (AK f) (AK g)
-> (Simplex (S (CountRL' g)) (S (CountRL' f)) -> r) -> r
go (AdjL Adj (AK ps) (AK qs)
g) Simplex (S (CountRL' g)) (S (CountRL' f)) -> r
xny = Simplex (S (CountRL' g)) (S (CountRL' f)) -> r
xny (Simplex (CountRL qs) (S (CountRL ps))
-> Simplex (S (CountRL qs)) (S (CountRL ps))
forall (x :: Nat) (y :: Nat).
Simplex x (S y) -> Simplex (S x) (S y)
X (Simplex (CountRL qs) (CountRL ps)
-> Simplex (CountRL qs) (S (CountRL ps))
forall (a :: Nat) (y :: Nat). Simplex a y -> Simplex a (S y)
Y (Adj (AK ps) (AK qs) -> Simplex (CountRL qs) (CountRL ps)
forall (a :: Path ABK B B) (b :: Path ABK B B).
Adj (AK a) (AK b) -> Simplex (CountRL b) (CountRL a)
toSimplexOp Adj (AK ps) (AK qs)
g)))
    go (AdjCap Adj ps (AK qs)
g) Simplex (S (CountRL' g)) (S (CountRL' f)) -> r
xny = Adj (AK f) (AK qs)
-> (Simplex (S (CountRL' qs)) (S (CountRL' f)) -> r) -> r
forall (f :: Path ABK A B) (g :: Path ABK A B) r.
Adj (AK f) (AK g)
-> (Simplex (S (CountRL' g)) (S (CountRL' f)) -> r) -> r
go Adj ps (AK qs)
Adj (AK f) (AK qs)
g (Simplex (S (S (CountRL' qs))) (S (CountRL' f)) -> r
Simplex (S (CountRL' g)) (S (CountRL' f)) -> r
xny (Simplex (S (S (CountRL' qs))) (S (CountRL' f)) -> r)
-> (Simplex (S (CountRL' qs)) (S (CountRL' f))
    -> Simplex (S (S (CountRL' qs))) (S (CountRL' f)))
-> Simplex (S (CountRL' qs)) (S (CountRL' f))
-> r
forall b c a. (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
. Simplex (S (CountRL' qs)) (S (CountRL' f))
-> Simplex (S (S (CountRL' qs))) (S (CountRL' f))
forall (x :: Nat) (y :: Nat).
Simplex x (S y) -> Simplex (S x) (S y)
X)

instance Adjunction_ (AK Nil) (AK Nil) where
  adj :: Adj (AK Nil) (AK Nil)
adj = (I ~> O (AK Nil) (AK Nil))
-> (O (AK Nil) (AK Nil) ~> I) -> Adj (AK Nil) (AK Nil)
forall {k} (kk :: k -> k -> Type) (c :: k) (d :: k) (l :: kk c d)
       (r :: kk d c).
(Bicategory kk, Ob l, Ob r) =>
(I ~> O r l) -> (O l r ~> I) -> Adj l r
Bi.Adj I ~> O (AK Nil) (AK Nil)
Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil O (AK Nil) (AK Nil) ~> I
Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil

instance Adjunction_ (AK (L ::: Nil)) (AK (R ::: Nil)) where
  adj :: Adj (AK (L ::: Nil)) (AK (R ::: Nil))
adj = Bi.Adj{adjUnit :: I ~> O (AK (R ::: Nil)) (AK (L ::: Nil))
adjUnit = Adj (AK Nil) (AK Nil) -> Adj (AK Nil) (AK (L ::: (R ::: Nil)))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil, adjCounit :: O (AK (L ::: Nil)) (AK (R ::: Nil)) ~> I
adjCounit = Adj (AK Nil) (AK Nil) -> Adj (AK (R ::: (L ::: Nil))) (AK Nil)
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil}

instance Adjunction_ (AK (L ::: R ::: L ::: Nil)) (AK (R ::: L ::: R ::: Nil)) where
  adj :: Adj
  (AK (L ::: (R ::: (L ::: Nil)))) (AK (R ::: (L ::: (R ::: Nil))))
adj = Bi.Adj{adjUnit :: I
~> O (AK (R ::: (L ::: (R ::: Nil))))
     (AK (L ::: (R ::: (L ::: Nil))))
adjUnit = Adj (AK Nil) (AK (L ::: (R ::: (L ::: (R ::: Nil)))))
-> Adj
     (AK Nil) (AK (L ::: (R ::: (L ::: (R ::: (L ::: (R ::: Nil)))))))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap (Adj (AK Nil) (AK (L ::: (R ::: Nil)))
-> Adj (AK Nil) (AK (L ::: (R ::: (L ::: (R ::: Nil)))))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap (Adj (AK Nil) (AK Nil) -> Adj (AK Nil) (AK (L ::: (R ::: Nil)))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil)), adjCounit :: O (AK (L ::: (R ::: (L ::: Nil)))) (AK (R ::: (L ::: (R ::: Nil))))
~> I
adjCounit = Adj (AK (R ::: (L ::: (R ::: (L ::: Nil))))) (AK Nil)
-> Adj
     (AK (R ::: (L ::: (R ::: (L ::: (R ::: (L ::: Nil))))))) (AK Nil)
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup (Adj (AK (R ::: (L ::: Nil))) (AK Nil)
-> Adj (AK (R ::: (L ::: (R ::: (L ::: Nil))))) (AK Nil)
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup (Adj (AK Nil) (AK Nil) -> Adj (AK (R ::: (L ::: Nil))) (AK Nil)
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil))}

instance Monad (AK (L ::: R ::: Nil)) where
  eta :: I ~> AK (L ::: (R ::: Nil))
eta = Adj (AK Nil) (AK Nil) -> Adj (AK Nil) (AK (L ::: (R ::: Nil)))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil
  mu :: O (AK (L ::: (R ::: Nil))) (AK (L ::: (R ::: Nil)))
~> AK (L ::: (R ::: Nil))
mu = Adj (AK (R ::: (L ::: (R ::: Nil)))) (AK (R ::: Nil))
-> Adj
     (AK (L ::: (R ::: (L ::: (R ::: Nil))))) (AK (L ::: (R ::: Nil)))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL (Adj (AK (R ::: Nil)) (AK (R ::: Nil))
-> Adj (AK (R ::: (L ::: (R ::: Nil)))) (AK (R ::: Nil))
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup (Adj (AK Nil) (AK Nil) -> Adj (AK (R ::: Nil)) (AK (R ::: Nil))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil))

instance Comonad (AK (R ::: L ::: Nil)) where
  epsilon :: AK (R ::: (L ::: Nil)) ~> I
epsilon = Adj (AK Nil) (AK Nil) -> Adj (AK (R ::: (L ::: Nil))) (AK Nil)
forall {j :: AB} (ps :: Path ABK B j) (qs :: ADJK B j).
Adj (AK ps) qs -> Adj (AK (R ::: (L ::: ps))) qs
AdjCup Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil
  delta :: AK (R ::: (L ::: Nil))
~> O (AK (R ::: (L ::: Nil))) (AK (R ::: (L ::: Nil)))
delta = Adj (AK (L ::: Nil)) (AK (L ::: (R ::: (L ::: Nil))))
-> Adj
     (AK (R ::: (L ::: Nil))) (AK (R ::: (L ::: (R ::: (L ::: Nil)))))
forall {j :: AB} (ps :: Path ABK A j) (qs :: Path ABK A j).
Adj (AK ps) (AK qs) -> Adj (AK (R ::: ps)) (AK (R ::: qs))
AdjR (Adj (AK (L ::: Nil)) (AK (L ::: Nil))
-> Adj (AK (L ::: Nil)) (AK (L ::: (R ::: (L ::: Nil))))
forall {j :: AB} (ps :: ADJK A j) (qs :: Path ABK A j).
Adj ps (AK qs) -> Adj ps (AK (L ::: (R ::: qs)))
AdjCap (Adj (AK Nil) (AK Nil) -> Adj (AK (L ::: Nil)) (AK (L ::: Nil))
forall {j :: AB} (ps :: Path ABK B j) (qs :: Path ABK B j).
Adj (AK ps) (AK qs) -> Adj (AK (L ::: ps)) (AK (L ::: qs))
AdjL Adj (AK Nil) (AK Nil)
forall {j :: AB}. Adj (AK Nil) (AK Nil)
AdjNil))

type SNilOrL :: Path ABK i j -> Type
data SNilOrL p where
  SNilL :: SNilOrL Nil
  SLL :: SNilOrL (L ::: Nil)
type SNilOrR :: Path ABK i j -> Type
data SNilOrR p where
  SNilR :: SNilOrR Nil
  SRR :: SNilOrR (R ::: Nil)

type IsTight :: forall {i} {j}. Path ABK i j -> Constraint
class (IsLRPath ps, IsCotight (CotightAdj ps), Adjunction_ (AK ps) (AK (CotightAdj ps))) => IsTight (ps :: Path ABK i j) where
  type CotightAdj (ps :: Path ABK i j) :: Path ABK j i
  isNilOrL :: SNilOrL ps
instance IsTight Nil where
  type CotightAdj Nil = Nil
  isNilOrL :: SNilOrL Nil
isNilOrL = SNilOrL Nil
forall (j :: AB). SNilOrL Nil
SNilL
instance IsTight (L ::: Nil) where
  type CotightAdj (L ::: Nil) = R ::: Nil
  isNilOrL :: SNilOrL (L ::: Nil)
isNilOrL = SNilOrL (L ::: Nil)
SLL
type IsCotight :: forall {i} {j}. Path ABK i j -> Constraint
class (IsLRPath ps, IsTight (TightAdj ps), Adjunction_ (AK (TightAdj ps)) (AK ps)) => IsCotight (ps :: Path ABK i j) where
  type TightAdj (ps :: Path ABK i j) :: Path ABK j i
  isNilOrR :: SNilOrR ps
instance IsCotight Nil where
  type TightAdj Nil = Nil
  isNilOrR :: SNilOrR Nil
isNilOrR = SNilOrR Nil
forall (j :: AB). SNilOrR Nil
SNilR
instance IsCotight (R ::: Nil) where
  type TightAdj (R ::: Nil) = L ::: Nil
  isNilOrR :: SNilOrR (R ::: Nil)
isNilOrR = SNilOrR (R ::: Nil)
SRR

type instance IsOb Tight (AK ps) = IsTight ps
type instance IsOb Cotight (AK ps) = IsCotight ps
type instance TightAdjoint (AK ps) = AK (TightAdj ps)
type instance CotightAdjoint (AK ps) = AK (CotightAdj ps)
instance WithObO2 Tight ADJK where
  withObO2 :: forall {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k)
       (b :: ADJK i j) r.
(Ob a, Ob b, IsOb Tight a, IsOb Tight b) =>
((IsOb Tight (O a b), Ob (O a b)) => r) -> r
withObO2 @(AK ps) @(AK qs) (IsOb Tight (O a b), Ob (O a b)) => r
r = case (forall (ps :: Path ABK j k). IsTight ps => SNilOrL ps
forall {i :: AB} {j :: AB} (ps :: Path ABK i j).
IsTight ps =>
SNilOrL ps
isNilOrL @ps, forall (ps :: Path ABK i j). IsTight ps => SNilOrL ps
forall {i :: AB} {j :: AB} (ps :: Path ABK i j).
IsTight ps =>
SNilOrL ps
isNilOrL @qs) of
    (SNilOrL (UN AK a)
SNilL, SNilOrL (UN AK b)
_) -> r
(IsOb Tight (O a b), Ob (O a b)) => r
r
    (SNilOrL (UN AK a)
SLL, SNilOrL (UN AK b)
SNilL) -> r
(IsOb Tight (O a b), Ob (O a b)) => r
r
instance WithObO2 Cotight ADJK where
  withObO2 :: forall {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k)
       (b :: ADJK i j) r.
(Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) =>
((IsOb Cotight (O a b), Ob (O a b)) => r) -> r
withObO2 @(AK ps) @(AK qs) (IsOb Cotight (O a b), Ob (O a b)) => r
r = case (forall (ps :: Path ABK j k). IsCotight ps => SNilOrR ps
forall {i :: AB} {j :: AB} (ps :: Path ABK i j).
IsCotight ps =>
SNilOrR ps
isNilOrR @ps, forall (ps :: Path ABK i j). IsCotight ps => SNilOrR ps
forall {i :: AB} {j :: AB} (ps :: Path ABK i j).
IsCotight ps =>
SNilOrR ps
isNilOrR @qs) of
    (SNilOrR (UN AK a)
SNilR, SNilOrR (UN AK b)
_) -> r
(IsOb Cotight (O a b), Ob (O a b)) => r
r
    (SNilOrR (UN AK a)
SRR, SNilOrR (UN AK b)
SNilR) -> r
(IsOb Cotight (O a b), Ob (O a b)) => r
r
instance Equipment ADJK where
  withTightAdjoint :: forall {j :: AB} {k1 :: AB} (f :: ADJK j k1) r.
IsCotight f =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint (Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r = r
(Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r
  withCotightAdjoint :: forall {j :: AB} {k1 :: AB} (f :: ADJK j k1) r.
IsTight f =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint (Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r = r
(Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r