{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Squares.Relative where

import Proarrow.Category.Bicategory (flipLeftAdjoint, flipRightAdjointInv)
import Proarrow.Category.Bicategory.Relative qualified as Rel
import Proarrow.Category.Bicategory.Strictified (Path (..), Strictified (..))
import Proarrow.Category.Equipment (Equipment (..), IsTight, TightPair)
import Proarrow.Squares (Sq, Sq' (..))

-- | The unit square for a @j@-relative monad @t@.
--
-- > A-----A
-- > |  /--j
-- > |  @  |
-- > |  \->t
-- > A-----A
unit
  :: forall {kk} {a} {e} {j :: kk e a} {t :: kk a e}
   . (Equipment kk, Rel.Monad j t, IsTight t)
  => Sq Nil (t ::: j ::: Nil) Nil Nil
unit :: forall {k} {kk :: k -> k -> Type} {a :: k} {e :: k} {j :: kk e a}
       {t :: kk a e}.
(Equipment kk, Monad j t, IsTight t) =>
Sq Nil (t ::: (j ::: Nil)) Nil Nil
unit = (O Nil Nil ~> O (t ::: (j ::: Nil)) Nil)
-> Sq' '(Nil, SUB Nil) '(t ::: (j ::: Nil), SUB Nil)
forall {c} {kk1 :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c}
       (p :: Path kk1 j h) (q :: Path kk1 k i) (f :: Path kk1 h i)
       (g :: Path kk1 j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq ((Fold Nil ~> Fold (t ::: (j ::: Nil)))
-> Strictified Nil (t ::: (j ::: Nil))
forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St (forall (j :: kk e a) (t :: kk 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 @j @t))

-- | The multiplication square for a @j@-relative monad @t@.
--
-- > A-------A
-- > j--\ /-<t
-- > |   @   |
-- > t>-/ \->t
-- > A-------A
mult
  :: forall {kk} {a} {e} {j :: kk e a} {t :: kk a e} t'
   . (Equipment kk, Rel.Monad j t, TightPair t t')
  => Sq (t ::: j ::: Nil) (t ::: t' ::: Nil) Nil Nil
mult :: forall {k} {kk :: k -> k -> Type} {a :: k} {e :: k} {j :: kk e a}
       {t :: kk a e} (t' :: kk e a).
(Equipment kk, Monad j t, TightPair t t') =>
Sq (t ::: (j ::: Nil)) (t ::: (t' ::: Nil)) Nil Nil
mult = (O Nil (t ::: (j ::: Nil)) ~> O (t ::: (t' ::: Nil)) Nil)
-> Sq' '(t ::: (j ::: Nil), SUB Nil) '(t ::: (t' ::: Nil), SUB Nil)
forall {c} {kk1 :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c}
       (p :: Path kk1 j h) (q :: Path kk1 k i) (f :: Path kk1 h i)
       (g :: Path kk1 j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq (forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
forall (l :: Path kk a e) (r :: Path kk e a) (a :: Path kk a a)
       (b :: Path kk a e).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
flipLeftAdjoint @(t ::: Nil) (forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk a e) (qs :: Path kk a e).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St @(t ::: j ::: t ::: Nil) @(t ::: Nil) (forall (j :: kk e a) (t :: kk 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 @j @t)))

-- | @j@-relative adjunction
--
-- > A-----A
-- > |  /--j
-- > l<-@  |
-- > |  \->r
-- > C-----C
leftAdjunct
  :: forall {kk} {a} {c} {e} {j :: kk e a} {l :: kk a c} {l' :: kk c a} {r :: kk c e}
   . (Equipment kk, Rel.Adjunction j l r, IsTight r, TightPair l l')
  => Sq (l' ::: Nil) (r ::: j ::: Nil) Nil Nil
leftAdjunct :: forall {k} {kk :: k -> k -> Type} {a :: k} {c :: k} {e :: k}
       {j :: kk e a} {l :: kk a c} {l' :: kk c a} {r :: kk c e}.
(Equipment kk, Adjunction j l r, IsTight r, TightPair l l') =>
Sq (l' ::: Nil) (r ::: (j ::: Nil)) Nil Nil
leftAdjunct = (O Nil (l' ::: Nil) ~> O (r ::: (j ::: Nil)) Nil)
-> Sq' '(l' ::: Nil, SUB Nil) '(r ::: (j ::: Nil), SUB Nil)
forall {c} {kk1 :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c}
       (p :: Path kk1 j h) (q :: Path kk1 k i) (f :: Path kk1 h i)
       (g :: Path kk1 j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq (forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk c i) (b :: kk d i).
(Adjunction l r, Ob b) =>
(a ~> O b l) -> O a r ~> b
forall (l :: Path kk a c) (r :: Path kk c a) (a :: Path kk a a)
       (b :: Path kk c a).
(Adjunction l r, Ob b) =>
(a ~> O b l) -> O a r ~> b
flipRightAdjointInv @(l ::: Nil) (forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk a a) (qs :: Path kk a a).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St @Nil @(l ::: r ::: j ::: Nil) (forall (j :: kk e a) (l :: kk a c) (r :: kk c e).
Adjunction j l r =>
I ~> O (O j r) l
forall {s} {kk :: CAT s} {a :: s} {c :: s} {e :: s} (j :: kk e a)
       (l :: kk a c) (r :: kk c e).
Adjunction j l r =>
I ~> O (O j r) l
Rel.eta @j @l @r)))

-- | @j@-relative adjunction, other direction
--
-- > A-----A
-- > j--\  |
-- > |  @<-l
-- > r->/  |
-- > C-----C
rightAdjunct
  :: forall {kk} {a} {c} {e} {j :: kk e a} {l :: kk a c} {l' :: kk c a} {r :: kk c e}
   . (Equipment kk, Rel.Adjunction j l r, IsTight r, TightPair l l')
  => Sq (r ::: j ::: Nil) (l' ::: Nil) Nil Nil
rightAdjunct :: forall {k} {kk :: k -> k -> Type} {a :: k} {c :: k} {e :: k}
       {j :: kk e a} {l :: kk a c} {l' :: kk c a} {r :: kk c e}.
(Equipment kk, Adjunction j l r, IsTight r, TightPair l l') =>
Sq (r ::: (j ::: Nil)) (l' ::: Nil) Nil Nil
rightAdjunct = (O Nil (r ::: (j ::: Nil)) ~> O (l' ::: Nil) Nil)
-> Sq' '(r ::: (j ::: Nil), SUB Nil) '(l' ::: Nil, SUB Nil)
forall {c} {kk1 :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c}
       (p :: Path kk1 j h) (q :: Path kk1 k i) (f :: Path kk1 h i)
       (g :: Path kk1 j k).
(Ob p, Ob q, IsTight f, IsTight g) =>
(O f p ~> O q g) -> Sq' '(p, SUB f) '(q, SUB g)
Sq (forall {s} {kk :: s -> s -> Type} {c :: s} {d :: s} {i :: s}
       (l :: kk c d) (r :: kk d c) (a :: kk i c) (b :: kk i d).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
forall (l :: Path kk a c) (r :: Path kk c a) (a :: Path kk c a)
       (b :: Path kk c c).
(Adjunction l r, Ob a) =>
(O l a ~> b) -> a ~> O r b
flipLeftAdjoint @(l ::: Nil) (forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1)
       (qs :: Path kk j k1).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
forall (ps :: Path kk c c) (qs :: Path kk c c).
(Ob ps, Ob qs) =>
(Fold ps ~> Fold qs) -> Strictified ps qs
St @(r ::: j ::: l ::: Nil) @Nil (forall (j :: kk e a) (l :: kk a c) (r :: kk c e).
Adjunction j l r =>
O (O l j) r ~> I
forall {s} {kk :: CAT s} {a :: s} {c :: s} {e :: s} (j :: kk e a)
       (l :: kk a c) (r :: kk c e).
Adjunction j l r =>
O (O l j) r ~> I
Rel.epsilon @j @l @r)))