{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Squares.Relative where

import Proarrow.Category.Bicategory.Relative qualified as Rel
import Proarrow.Category.Bicategory.Strictified (Path (..), SPath (..), Strictified (..))
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), Sq (..))
import Proarrow.Core (CategoryOf (..), obj)
import Proarrow.Category.Bicategory (Bicategory(..))

-- | The unit square for a @j@-relative monad @t@.
--
-- > A-----A
-- > |  /-<j
-- > |  @  |
-- > |  \->t
-- > A-----A
unit :: forall {hk} {vk} {a} {e} {j :: vk a e} {t :: vk a e}
     . (Equipment hk vk, Rel.Monad (Conjoint hk j) (Companion hk t), Ob0 vk a, Ob0 vk e, Ob t, Ob j)
     => Sq '(Nil, Nil :: Path vk a a) '(Companion hk t ::: Conjoint hk j ::: Nil, Nil)
unit :: forall {k} {hk :: CAT k} {vk :: CAT k} {a :: k} {e :: k}
       {j :: vk a e} {t :: vk a e}.
(Equipment hk vk, Monad (Conjoint hk j) (Companion hk t), Ob0 vk a,
 Ob0 vk e, Ob t, Ob j) =>
Sq '(Nil, Nil) '(Companion hk t ::: (Conjoint hk j ::: Nil), Nil)
unit = let jc :: Conjoint hk j ~> Conjoint hk j
jc = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j); tc :: Companion hk t ~> Companion hk t
tc = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @t)
  in (O (Companion (Path hk) Nil) Nil
 ~> O (Companion hk t ::: (Conjoint hk j ::: Nil))
      (Companion (Path hk) Nil))
-> Sq
     '(Nil, Nil) '(Companion hk t ::: (Conjoint hk j ::: Nil), Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c}
       {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq (SPath Nil
-> SPath (Companion hk t ::: (Conjoint hk j ::: Nil))
-> (Fold Nil ~> Fold (Companion hk t ::: (Conjoint hk j ::: Nil)))
-> Strictified Nil (Companion hk t ::: (Conjoint hk j ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil ((Companion hk t ~> Companion hk t)
-> SPath (Conjoint hk j ::: Nil)
-> SPath (Companion hk t ::: (Conjoint hk j ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk t ~> Companion hk t
tc ((Conjoint hk j ~> Conjoint hk j)
-> SPath Nil -> SPath (Conjoint hk j ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Conjoint hk j ~> Conjoint hk j
jc SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil)) (forall (j :: hk e a) (t :: hk a e). Monad j t => I ~> O j t
forall {s} {kk :: CAT s} {a :: s} {e :: s} (j :: kk e a)
       (t :: kk a e).
Monad j t =>
I ~> O j t
Rel.unit @(Conjoint hk j) @(Companion hk t)))

-- | The multiplication square for a @j@-relative monad @t@.
--
-- > E-----E
-- > t>-\  |
-- > j<-@->t
-- > t>-/  |
-- > A-----A
mult :: forall {hk} {vk} {a} {e} {j :: vk a e} {t :: vk a e}
     . (Equipment hk vk, Rel.Monad (Conjoint hk j) (Companion hk t), Ob0 vk a, Ob0 vk e, Ob t, Ob j)
     => Sq '(Companion hk t ::: Conjoint hk j ::: Companion hk t ::: Nil, Nil :: Path vk e e) '(Companion hk t ::: Nil, Nil)
mult :: forall {k} {hk :: CAT k} {vk :: CAT k} {a :: k} {e :: k}
       {j :: vk a e} {t :: vk a e}.
(Equipment hk vk, Monad (Conjoint hk j) (Companion hk t), Ob0 vk a,
 Ob0 vk e, Ob t, Ob j) =>
Sq
  '(Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)),
    Nil)
  '(Companion hk t ::: Nil, Nil)
mult = let jc :: Conjoint hk j ~> Conjoint hk j
jc = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
Equipment hk vk =>
(f ~> g) -> Conjoint hk g ~> Conjoint hk f
mapConjoint @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @j); tc :: Companion hk t ~> Companion hk t
tc = forall {c} (hk :: CAT c) (vk :: CAT c) {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
forall (hk :: CAT k) (vk :: CAT k) {j :: k} {k :: k} (f :: vk j k)
       (g :: vk j k).
HasCompanions hk vk =>
(f ~> g) -> Companion hk f ~> Companion hk g
mapCompanion @hk (forall (a :: vk a e). (CategoryOf (vk a e), Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @t)
  in (O (Companion (Path hk) Nil)
   (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
 ~> O (Companion hk t ::: Nil) (Companion (Path hk) Nil))
-> Sq
     '(Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)),
       Nil)
     '(Companion hk t ::: Nil, Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c}
       {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq (SPath
  (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
-> SPath (Companion hk t ::: Nil)
-> (Fold
      (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
    ~> Fold (Companion hk t ::: Nil))
-> Strictified
     (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
     (Companion hk t ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob0 kk j, Ob0 kk k1) =>
SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
Str ((Companion hk t ~> Companion hk t)
-> SPath (Conjoint hk j ::: (Companion hk t ::: Nil))
-> SPath
     (Companion hk t ::: (Conjoint hk j ::: (Companion hk t ::: Nil)))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk t ~> Companion hk t
tc ((Conjoint hk j ~> Conjoint hk j)
-> SPath (Companion hk t ::: Nil)
-> SPath (Conjoint hk j ::: (Companion hk t ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Conjoint hk j ~> Conjoint hk j
jc ((Companion hk t ~> Companion hk t)
-> SPath Nil -> SPath (Companion hk t ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk t ~> Companion hk t
tc SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil))) ((Companion hk t ~> Companion hk t)
-> SPath Nil -> SPath (Companion hk t ::: Nil)
forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k}
       (p :: kk j j1) (ps1 :: Path kk j1 k1).
Ob0 kk j =>
Obj p -> SPath ps1 -> SPath (p ::: ps1)
SCons Companion hk t ~> Companion hk t
tc SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) (forall (j :: hk e a) (t :: hk a e). Monad j t => O (O t j) t ~> t
forall {s} {kk :: CAT s} {a :: s} {e :: s} (j :: kk e a)
       (t :: kk a e).
Monad j t =>
O (O t j) t ~> t
Rel.mult @(Conjoint hk j) @(Companion hk t)))