{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Squares where

import Data.Functor.Compose (Compose (..))
import Proarrow.Category.Bicategory (Bicategory (..), Ob')
import Proarrow.Category.Bicategory.Prof (FUN, PROFK (..), Prof (..))
import Proarrow.Category.Bicategory.Strictified
  ( Fold
  , IsPath (..)
  , Path (..)
  , SPath (..)
  , Strictified (..)
  , asObj
  , companionFold
  , fold
  , foldCompanion
  , mapCompanionSPath
  , singleton
  , type (+++)
  )
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), Sq (..))
import Proarrow.Category.Equipment qualified as E
import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Core (CategoryOf (..), Obj, Promonad ((.)), id, obj, (:~>), (\\))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (RepCostar (..), Representable)
import Proarrow.Profunctor.Star (Star (..))
import Prelude (Either (..), Traversable, either)

infixl 6 |||
infixl 5 ===

-- | The empty square for an object.
--
-- > K-----K
-- > |     |
-- > |     |
-- > |     |
-- > K-----K
object :: (HasCompanions hk vk, Ob0 vk k) => Sq '(Nil :: Path hk k k, Nil :: Path vk k k) '(Nil, Nil)
object :: forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(Nil, Nil) '(Nil, Nil)
object = Sq '(I, I) '(I, I)
Sq '(Nil, Nil) '(Nil, Nil)
forall {c} (hk :: CAT c) (vk :: CAT c) (k :: c).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(I, I) '(I, I)
E.object

-- | Make a square from a horizontal proarrow
--
-- > K-----K
-- > |     |
-- > p--@--q
-- > |     |
-- > J-----J
hArr
  :: forall {hk} {vk} {j} {k} (p :: hk j k) q
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k)
  => p ~> q
  -> Sq '(p ::: Nil, Nil :: Path vk k k) '(q ::: Nil, Nil :: Path vk j j)
hArr :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {j :: k}
       {k :: k} (p :: hk j k) (q :: hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(p ~> q) -> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil)
hArr = ((p ::: Nil) ~> (q ::: Nil)) -> Sq '(p ::: Nil, I) '(q ::: Nil, I)
Strictified (p ::: Nil) (q ::: Nil)
-> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil)
forall {c} {hk :: c -> c -> Type} {vk :: c -> c -> Type} {j :: c}
       {k :: c} (p :: hk j k) (q :: hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(p ~> q) -> Sq '(p, I) '(q, I)
E.hArr (Strictified (p ::: Nil) (q ::: Nil)
 -> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil))
-> ((p ~> q) -> Strictified (p ::: Nil) (q ::: Nil))
-> (p ~> q)
-> Sq '(p ::: Nil, Nil) '(q ::: Nil, Nil)
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
. (p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
(p ~> q) -> Strictified (p ::: Nil) (q ::: Nil)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton

-- | A horizontal identity square.
--
-- > J-----J
-- > |     |
-- > p-----p
-- > |     |
-- > K-----K
hId
  :: (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob (p :: hk k j)) => Sq '(p ::: Nil, Nil :: Path vk j j) '(p ::: Nil, Nil)
hId :: forall {k} (hk :: CAT k) (vk :: CAT k) (j :: k) (k :: k)
       (p :: hk k j).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob p) =>
Sq '(p ::: Nil, Nil) '(p ::: Nil, Nil)
hId = Sq '(p ::: Nil, I) '(p ::: Nil, I)
Sq '(p ::: Nil, Nil) '(p ::: Nil, Nil)
forall {c} (hk :: CAT c) (vk :: CAT c) (j :: c) (k :: c)
       (p :: hk k j).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob p) =>
Sq '(p, I) '(p, I)
E.hId

-- | A horizontal identity square for a companion.
--
-- Requires a type application: @compId \@f@
--
-- > K-----K
-- > |     |
-- > f>--->f
-- > |     |
-- > J-----J
compId
  :: forall {hk} {vk} {j} {k} f
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
  => Sq '(Companion hk f ::: Nil, Nil :: Path vk k k) '(Companion hk f ::: Nil, Nil :: Path vk j j)
compId :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Companion hk f ::: Nil, Nil) '(Companion hk f ::: Nil, Nil)
compId = forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Companion hk f, I) '(Companion hk f, I)
forall (f :: Path vk j k).
(HasCompanions (Path hk) (Path vk), Ob0 (Path vk) j,
 Ob0 (Path vk) k, Ob f) =>
Sq '(Companion (Path hk) f, I) '(Companion (Path hk) f, I)
E.compId @(f ::: Nil)

-- | A horizontal identity square for a conjoint.
--
-- Requires a type application: @conjId \@f@
--
-- > J-----J
-- > |     |
-- > f>--->f
-- > |     |
-- > K-----K
conjId
  :: forall {hk} {vk} {j} {k} f
   . (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
  => Sq '(Conjoint hk f ::: Nil, Nil :: Path vk j j) '(Conjoint hk f ::: Nil, Nil :: Path vk k k)
conjId :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f ::: Nil, Nil) '(Conjoint hk f ::: Nil, Nil)
conjId = forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f, I) '(Conjoint hk f, I)
forall (f :: Path vk j k).
(Equipment (Path hk) (Path vk), Ob0 (Path vk) j, Ob0 (Path vk) k,
 Ob f) =>
Sq '(Conjoint (Path hk) f, I) '(Conjoint (Path hk) f, I)
E.conjId @(f ::: Nil)

-- | Make a square from a vertical arrow
--
-- > J--f--K
-- > |  v  |
-- > |  @  |
-- > |  v  |
-- > J--g--K
vArr
  :: forall {hk} {vk} {j} {k} (f :: vk j k) g
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k)
  => f ~> g
  -> Sq '(Nil :: Path hk j j, f ::: Nil) '(I :: Path hk k k, g ::: Nil)
vArr :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(f ~> g) -> Sq '(Nil, f ::: Nil) '(I, g ::: Nil)
vArr = ((f ::: Nil) ~> (g ::: Nil)) -> Sq '(I, f ::: Nil) '(I, g ::: Nil)
Strictified (f ::: Nil) (g ::: Nil)
-> Sq '(Nil, f ::: Nil) '(Nil, g ::: Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
(f ~> g) -> Sq '(I, f) '(I, g)
E.vArr (Strictified (f ::: Nil) (g ::: Nil)
 -> Sq '(Nil, f ::: Nil) '(Nil, g ::: Nil))
-> ((f ~> g) -> Strictified (f ::: Nil) (g ::: Nil))
-> (f ~> g)
-> Sq '(Nil, f ::: Nil) '(Nil, g ::: Nil)
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
. (f ~> g) -> (f ::: Nil) ~> (g ::: Nil)
(f ~> g) -> Strictified (f ::: Nil) (g ::: Nil)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j)
       (q :: kk i j).
Bicategory kk =>
(p ~> q) -> (p ::: Nil) ~> (q ::: Nil)
singleton

-- | A vertical identity square.
--
-- > J--f--K
-- > |  v  |
-- > |  |  |
-- > |  v  |
-- > J--f--K
vId
  :: forall {hk} {vk} {j} {k} (f :: vk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
  => Sq '(Nil :: Path hk j j, f ::: Nil) '(Nil :: Path hk k k, f ::: Nil)
vId :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId = Sq '(I, f ::: Nil) '(I, f ::: Nil)
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(I, f) '(I, f)
E.vId

vId'
  :: forall {hk} {vk} {j} {k} (f :: vk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k)
  => Obj f
  -> Sq '(Nil :: Path hk j j, f ::: Nil) '(Nil :: Path hk k k, f ::: Nil)
vId' :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k) =>
Obj f -> Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId' Obj f
f = Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
(Ob f, Ob f) => Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
vId ((Ob f, Ob f) => Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil))
-> Obj f -> Sq '(Nil, f ::: Nil) '(Nil, f ::: Nil)
forall (a :: vk j k) (b :: vk j k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj f
f

-- | Horizontal composition
--
-- > L--d--H     H--f--I     L-d+f-I
-- > |  v  |     |  v  |     |  v  |
-- > p--@--q ||| q--@--r  =  p--@--r
-- > |  v  |     |  v  |     |  v  |
-- > M--e--J     J--g--K     M-e+g-K
(|||)
  :: forall {hk} {vk} {h} {l} {m} (ps :: Path hk m l) qs rs (ds :: Path vk l h) es fs gs
   . (HasCompanions hk vk)
  => Sq '(ps, ds) '(qs, es)
  -> Sq '(qs, fs) '(rs, gs)
  -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
||| :: forall {k} {b :: k} {k :: k} {i :: k} {hk :: CAT k} {vk :: CAT k}
       {h :: k} {l :: k} {m :: k} (ps :: Path hk m l) (qs :: Path hk b h)
       (rs :: Path hk k i) (ds :: Path vk l h) (es :: Path vk m b)
       (fs :: Path vk h i) (gs :: Path vk b k).
HasCompanions hk vk =>
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
(|||) = Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, O fs ds) '(rs, O gs es)
Sq '(ps, ds) '(qs, es)
-> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
forall {s} {j :: s} {k :: s} {i :: s} {hk :: s -> s -> Type}
       {vk :: s -> s -> Type} {h :: s} {l :: s} {m :: s} (p :: hk m l)
       (q :: hk j h) (r :: hk k i) (d :: vk l h) (e :: vk m j)
       (f :: vk h i) (g :: vk j k).
HasCompanions hk vk =>
Sq '(p, d) '(q, e)
-> Sq '(q, f) '(r, g) -> Sq '(p, O f d) '(r, O g e)
(E.|||)

-- | Vertical composition
--
-- >  H--e--I
-- >  |  v  |
-- >  r--@--s
-- >  |  v  |
-- >  J--f--K
-- >    ===
-- >  J--f--K
-- >  |  v  |
-- >  p--@--q
-- >  |  v  |
-- >  L--g--M
-- >
-- >    v v
-- >
-- >  H--e--I
-- >  |  v  |
-- > p+r-@-q+s
-- >  |  v  |
-- >  J--g--K
(===)
  :: forall {hk} {vk} {h} {i} {j} {l} (ps :: Path hk l j) qs rs ss (es :: Path vk h i) fs gs
   . (HasCompanions hk vk)
  => Sq '(rs, es) '(ss, fs)
  -> Sq '(ps, fs) '(qs, gs)
  -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
=== :: forall {k} {k :: k} {b :: k} {hk :: CAT k} {vk :: CAT k} {h :: k}
       {i :: k} {j :: k} {l :: k} (ps :: Path hk l j) (qs :: Path hk k b)
       (rs :: Path hk j h) (ss :: Path hk b i) (es :: Path vk h i)
       (fs :: Path vk j b) (gs :: Path vk l k).
HasCompanions hk vk =>
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
(===) = Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(O rs ps, es) '(O ss qs, gs)
Sq '(rs, es) '(ss, fs)
-> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
forall {s1} {k :: s1} {j1 :: s1} {hk :: s1 -> s1 -> Type}
       {vk :: s1 -> s1 -> Type} {h :: s1} {i :: s1} {j2 :: s1} {l :: s1}
       (p :: hk l j2) (q :: hk k j1) (r :: hk j2 h) (s2 :: hk j1 i)
       (e :: vk h i) (f :: vk j2 j1) (g :: vk l k).
HasCompanions hk vk =>
Sq '(r, e) '(s2, f)
-> Sq '(p, f) '(q, g) -> Sq '(O r p, e) '(O s2 q, g)
(E.===)

-- | Bend a vertical arrow in the companion direction.
--
-- > J--f--K
-- > |  v  |
-- > |  \->f
-- > |     |
-- > J-----J
toRight
  :: forall {hk} {vk} {j} {k} f
   . (HasCompanions hk vk, Ob' (f :: vk j k))
  => Sq '(Nil, f ::: Nil) '(Companion hk f ::: Nil, Nil)
toRight :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(Nil, f ::: Nil) '(Companion hk f ::: Nil, Nil)
toRight = Sq '(I, f ::: Nil) '(Companion (Path hk) (f ::: Nil), I)
Sq '(Nil, f ::: Nil) '(Companion hk f ::: Nil, Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(I, f) '(Companion hk f, I)
E.toRight

-- | Bend a vertical arrow in the conjoint direction.
--
-- > J--f--K
-- > |  v  |
-- > f<-/  |
-- > |     |
-- > K-----K
toLeft
  :: forall {hk} {vk} {j} {k} (f :: vk j k)
   . (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob (f :: vk j k))
  => Sq '(Conjoint hk f ::: Nil, f ::: Nil) '(Nil, Nil)
toLeft :: forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f ::: Nil, f ::: Nil) '(Nil, Nil)
toLeft = Sq '(Conjoint (Path hk) (f ::: Nil), f ::: Nil) '(I, I)
Sq '(Conjoint hk f ::: Nil, f ::: Nil) '(Nil, Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Conjoint hk f, f) '(I, I)
E.toLeft

-- | Bend a companion proarrow back to a vertical arrow.
--
-- > K-----K
-- > |     |
-- > f>-\  |
-- > |  v  |
-- > J--f--K
fromLeft
  :: forall {hk} {vk} {j} {k} f
   . (HasCompanions hk vk, Ob' (f :: vk j k))
  => Sq '(Companion hk f ::: Nil, Nil) '(Nil, f ::: Nil)
fromLeft :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(Companion hk f ::: Nil, Nil) '(Nil, f ::: Nil)
fromLeft = Sq '(Companion (Path hk) (f ::: Nil), I) '(I, f ::: Nil)
Sq '(Companion hk f ::: Nil, Nil) '(Nil, f ::: Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(HasCompanions hk vk, Ob' f) =>
Sq '(Companion hk f, I) '(I, f)
E.fromLeft

-- | Bend a conjoint proarrow back to a vertical arrow.
--
-- > J-----J
-- > |     |
-- > |  /-<f
-- > |  v  |
-- > J--f--K
fromRight
  :: forall {hk} {vk} {j} {k} (f :: vk j k)
   . (Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f)
  => Sq '(Nil, Nil) '(Conjoint hk f ::: Nil, f ::: Nil)
fromRight :: forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(Nil, Nil) '(Conjoint hk f ::: Nil, f ::: Nil)
fromRight = Sq '(I, I) '(Conjoint (Path hk) (f ::: Nil), f ::: Nil)
Sq '(Nil, Nil) '(Conjoint hk f ::: Nil, f ::: Nil)
forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (f :: vk j k).
(Equipment hk vk, Ob0 vk j, Ob0 vk k, Ob f) =>
Sq '(I, I) '(Conjoint hk f, f)
E.fromRight

-- > K--I--K
-- > |  v  |
-- > |  @  |
-- > |     |
-- > K-----K
vUnitor
  :: forall hk vk k
   . (HasCompanions hk vk, Ob0 vk k)
  => Sq '(Nil :: Path hk k k, I ::: Nil) '(Nil :: Path hk k k, Nil :: Path vk k k)
vUnitor :: forall {k} (hk :: CAT k) (vk :: CAT k) (k :: k).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(Nil, I ::: Nil) '(Nil, Nil)
vUnitor = Sq '(Nil, I ::: Nil) '(Nil, Nil)
Sq '(Nil, Fold Nil ::: Nil) '(Nil, Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
vSplitAll

-- > K-----K
-- > |     |
-- > |  @  |
-- > |  v  |
-- > K--I--K
vUnitorInv
  :: forall hk vk k
   . (HasCompanions hk vk, Ob0 vk k)
  => Sq '(Nil :: Path hk k k, Nil :: Path vk k k) '(Nil :: Path hk k k, I ::: Nil)
vUnitorInv :: forall {k} (hk :: CAT k) (vk :: CAT k) (k :: k).
(HasCompanions hk vk, Ob0 vk k) =>
Sq '(Nil, Nil) '(Nil, I ::: Nil)
vUnitorInv = Sq '(Nil, Nil) '(Nil, I ::: Nil)
Sq '(Nil, Nil) '(Nil, Fold Nil ::: Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, ps) '(Nil, Fold ps ::: Nil)
vCombineAll

-- > I-f-g-K
-- > | v v |
-- > | \@/ |
-- > |  v  |
-- > I-gof-K
vCombine
  :: forall {hk} {vk} {i} {j} {k} (f :: vk i j) (g :: vk j k)
   . (HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob f, Ob g)
  => Sq '(Nil :: Path hk i i, f ::: g ::: Nil) '(Nil, g `O` f ::: Nil)
vCombine :: forall {k} {hk :: CAT k} {vk :: CAT k} {i :: k} {j :: k} {k :: k}
       (f :: vk i j) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob f, Ob g) =>
Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
vCombine = Sq '(Nil, f ::: (g ::: Nil)) '(Nil, O g f ::: Nil)
Sq
  '(Nil, f ::: (g ::: Nil)) '(Nil, Fold (f ::: (g ::: Nil)) ::: Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, ps) '(Nil, Fold ps ::: Nil)
vCombineAll

-- > I-gof-K
-- > |  v  |
-- > | /@\ |
-- > | v v |
-- > I-f-g-K
vSplit
  :: forall {hk} {vk} {i} {j} {k} (f :: vk i j) (g :: vk j k)
   . (HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob f, Ob g)
  => Sq '(Nil :: Path hk i i, g `O` f ::: Nil) '(Nil, f ::: g ::: Nil)
vSplit :: forall {k} {hk :: CAT k} {vk :: CAT k} {i :: k} {j :: k} {k :: k}
       (f :: vk i j) (g :: vk j k).
(HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob f, Ob g) =>
Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
vSplit = Sq '(Nil, O g f ::: Nil) '(Nil, f ::: (g ::: Nil))
Sq
  '(Nil, Fold (f ::: (g ::: Nil)) ::: Nil) '(Nil, f ::: (g ::: Nil))
forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
vSplitAll

-- | Combine a whole bunch of vertical arrows into one composed arrow.
--
-- > J-p..-K
-- > | vvv |
-- > | \@/ |
-- > |  v  |
-- > J--f--K
vCombineAll
  :: forall {hk} {vk} {j} {k} (ps :: Path vk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps)
  => Sq '(Nil :: Path hk j j, ps) '(Nil :: Path hk k k, Fold ps ::: Nil)
vCombineAll :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, ps) '(Nil, Fold ps ::: Nil)
vCombineAll =
  let ps :: SPath ps
ps = forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path vk j k). IsPath ps => SPath ps
singPath @ps; fps :: Fold ps ~> Fold ps
fps = SPath ps -> Fold ps ~> Fold ps
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath ps
ps
  in (O (Companion (Path hk) ps) Nil
 ~> O Nil (Companion (Path hk) (Fold ps ::: Nil)))
-> Sq '(Nil, ps) '(Nil, Fold ps ::: 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 (Path hk) ps)
-> SPath (Companion hk (Fold ps) ::: Nil)
-> (Fold (Companion (Path hk) ps)
    ~> Fold (Companion hk (Fold ps) ::: Nil))
-> Strictified
     (Companion (Path hk) ps) (Companion hk (Fold ps) ::: 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 ps -> SPath (Companion (Path hk) ps)
forall {k1} (hk :: CAT k1) {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath SPath ps
ps) (Obj (Companion hk (Fold ps))
-> SPath Nil -> SPath (Companion hk (Fold ps) ::: 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 ((Fold ps ~> Fold ps) -> Obj (Companion hk (Fold ps))
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
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
mapCompanion Fold ps ~> Fold ps
fps) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) (SPath ps -> Fold (Companion (Path hk) ps) ~> Companion hk (Fold ps)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> Fold (Companion (Path hk) fs) ~> Companion hk (Fold fs)
foldCompanion SPath ps
ps)) ((Ob (Fold ps), Ob (Fold ps)) =>
 Sq '(Nil, ps) '(Nil, Fold ps ::: Nil))
-> (Fold ps ~> Fold ps) -> Sq '(Nil, ps) '(Nil, Fold ps ::: Nil)
forall (a :: vk j k) (b :: vk j k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold ps ~> Fold ps
fps

-- | Split one composed arrow into a whole bunch of vertical arrows.
--
-- > J--f--K
-- > |  v  |
-- > | /@\ |
-- > | vvv |
-- > J-p..-K
vSplitAll
  :: forall {hk} {vk} {j} {k} (ps :: Path vk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps)
  => Sq '(Nil :: Path hk j j, Fold ps ::: Nil) '(Nil :: Path hk k k, ps)
vSplitAll :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path vk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
vSplitAll =
  let ps :: SPath ps
ps = forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path vk j k). IsPath ps => SPath ps
singPath @ps; fps :: Fold ps ~> Fold ps
fps = SPath ps -> Fold ps ~> Fold ps
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath ps
ps; cps :: SPath (Companion (Path hk) ps)
cps = forall {k1} (hk :: CAT k1) {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
forall (hk :: CAT k) {vk :: CAT k} {j :: k} {k2 :: k}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> SPath (Companion (Path hk) fs)
mapCompanionSPath @hk SPath ps
ps
  in (O (Companion (Path hk) (Fold ps ::: Nil)) Nil
 ~> O Nil (Companion (Path hk) ps))
-> Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
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 (Fold ps) ::: Nil)
-> SPath (Companion (Path hk) ps)
-> (Fold (Companion hk (Fold ps) ::: Nil)
    ~> Fold (Companion (Path hk) ps))
-> Strictified
     (Companion hk (Fold ps) ::: Nil) (Companion (Path hk) ps)
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 (Obj (Companion hk (Fold ps))
-> SPath Nil -> SPath (Companion hk (Fold ps) ::: 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 ((Fold ps ~> Fold ps) -> Obj (Companion hk (Fold ps))
forall {j :: k} {k :: k} (f :: vk j k) (g :: vk j k).
(f ~> g) -> Companion hk f ~> Companion hk g
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
mapCompanion Fold ps ~> Fold ps
fps) SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) SPath (Companion (Path hk) ps)
cps (SPath ps -> Companion hk (Fold ps) ~> Fold (Companion (Path hk) ps)
forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1}
       (fs :: Path vk j k2).
HasCompanions hk vk =>
SPath fs -> Companion hk (Fold fs) ~> Fold (Companion (Path hk) fs)
companionFold SPath ps
ps)) ((Ob (Fold ps), Ob (Fold ps)) =>
 Sq '(Nil, Fold ps ::: Nil) '(Nil, ps))
-> (Fold ps ~> Fold ps) -> Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
forall (a :: vk j k) (b :: vk j k) r.
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold ps ~> Fold ps
fps ((Ob (Companion (Path hk) ps), Ob (Companion (Path hk) ps)) =>
 Sq '(Nil, Fold ps ::: Nil) '(Nil, ps))
-> Strictified (Companion (Path hk) ps) (Companion (Path hk) ps)
-> Sq '(Nil, Fold ps ::: Nil) '(Nil, ps)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: Path hk j k) (b :: Path hk j k) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ SPath (Companion (Path hk) ps) -> Obj (Companion (Path hk) ps)
forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j).
Bicategory kk =>
SPath ps -> Obj ps
asObj SPath (Companion (Path hk) ps)
cps

-- | Combine a whole bunch of horizontal proarrows into one composed proarrow.
--
-- > K-----K
-- > p--\  |
-- > :--@--f
-- > :--/  |
-- > J-----J
hCombineAll
  :: forall {hk} {vk} {j} {k} (ps :: Path hk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps)
  => Sq '(ps, Nil :: Path vk k k) '(Fold ps ::: Nil, Nil)
hCombineAll :: forall {k} {hk :: CAT k} {vk :: CAT k} {j :: k} {k :: k}
       (ps :: Path hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(ps, Nil) '(Fold ps ::: Nil, Nil)
hCombineAll = let ps :: SPath ps
ps = forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path hk j k). IsPath ps => SPath ps
singPath @ps; fps :: Fold ps ~> Fold ps
fps = SPath ps -> Fold ps ~> Fold ps
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath ps
ps in (O (Companion (Path hk) Nil) ps
 ~> O (Fold ps ::: Nil) (Companion (Path hk) Nil))
-> Sq '(ps, Nil) '(Fold ps ::: 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 ps
-> SPath (Fold ps ::: Nil)
-> (Fold ps ~> Fold (Fold ps ::: Nil))
-> Strictified ps (Fold ps ::: 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 ps
ps ((Fold ps ~> Fold ps) -> SPath Nil -> SPath (Fold ps ::: 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 Fold ps ~> Fold ps
fps SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) Fold ps ~> Fold ps
Fold ps ~> Fold (Fold ps ::: Nil)
fps) ((Ob0 hk j, Ob0 hk k, Ob (Fold ps), Ob (Fold ps)) =>
 Sq '(ps, Nil) '(Fold ps ::: Nil, Nil))
-> (Fold ps ~> Fold ps) -> Sq '(ps, Nil) '(Fold ps ::: Nil, Nil)
forall (i :: k) (j :: k) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk j, Ob ps, Ob qs) => r) -> (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
\\\ Fold ps ~> Fold ps
fps

-- | Split one composed proarrow into a whole bunch of horizontal proarrows.
--
-- > K-----K
-- > |  /--p
-- > f--@--:
-- > |  \--:
-- > J-----J
hSplitAll
  :: forall {hk} {vk} {j} {k} (ps :: Path hk j k)
   . (HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps)
  => Sq '(Fold ps ::: Nil, Nil :: Path vk k k) '(ps, Nil)
hSplitAll :: forall {c} {hk :: CAT c} {vk :: CAT c} {j :: c} {k :: c}
       (ps :: Path hk j k).
(HasCompanions hk vk, Ob0 vk j, Ob0 vk k, Ob ps) =>
Sq '(Fold ps ::: Nil, Nil) '(ps, Nil)
hSplitAll = let ps :: SPath ps
ps = forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1).
IsPath ps =>
SPath ps
forall (ps :: Path hk j k). IsPath ps => SPath ps
singPath @ps; fps :: Fold ps ~> Fold ps
fps = SPath ps -> Fold ps ~> Fold ps
forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j).
Bicategory kk =>
SPath as -> Fold as ~> Fold as
fold SPath ps
ps in (O (Companion (Path hk) Nil) (Fold ps ::: Nil)
 ~> O ps (Companion (Path hk) Nil))
-> Sq '(Fold ps ::: Nil, Nil) '(ps, 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 (Fold ps ::: Nil)
-> SPath ps
-> (Fold (Fold ps ::: Nil) ~> Fold ps)
-> Strictified (Fold ps ::: Nil) ps
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 ((Fold ps ~> Fold ps) -> SPath Nil -> SPath (Fold ps ::: 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 Fold ps ~> Fold ps
fps SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil) SPath ps
ps Fold ps ~> Fold ps
Fold (Fold ps ::: Nil) ~> Fold ps
fps) ((Ob0 hk j, Ob0 hk k, Ob (Fold ps), Ob (Fold ps)) =>
 Sq '(Fold ps ::: Nil, Nil) '(ps, Nil))
-> (Fold ps ~> Fold ps) -> Sq '(Fold ps ::: Nil, Nil) '(ps, Nil)
forall (i :: c) (j :: c) (ps :: hk i j) (qs :: hk i j) r.
((Ob0 hk i, Ob0 hk j, Ob ps, Ob qs) => r) -> (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
\\\ Fold ps ~> Fold ps
fps

-- | Optics in proarrow equipments.
--
-- > J-------J
-- > s>--@-->a
-- > |   @   |
-- > t<--@--<b
-- > K-------K
type Optic hk (a :: vk z j) (b :: vk z k) (s :: vk x j) (t :: vk x k) =
  Sq '(Conjoint hk t ::: Companion hk s ::: Nil, Nil :: Path vk j j) '(Conjoint hk b ::: Companion hk a ::: Nil, Nil)

-- > J-------J
-- > s>-\ /->a
-- > |   @   |
-- > |   v   |
-- > X---m---Z

-- > X---m---Z
-- > |   v   |
-- > |   @   |
-- > t<-/ \-<b
-- > K-------K


-- > J-------J     J-------J
-- > a>--@   |     s>--@   |
-- > |   @---p ==> |   @---p
-- > b<--@   |     t<--@   |
-- > K-------K     K-------K

-- > J-------J     J-------J
-- > a>----->a     s>--@-->a
-- > |       | ==> |   @   |
-- > b<-----<b     t<--@--<b
-- > K-------K     K-------K

-- > J-------J     J-------J
-- > |   @-->a     |   @-->a
-- > |   @   |     |   @-->m
-- > p---@   | ==> p---@   |
-- > |   @   |     |   @--<m
-- > |   @--<b     |   @--<b
-- > K-------K     K-------K


type ProfOptic a b s t = Optic PROFK (FUN a) (FUN b) (FUN s) (FUN t)
mkProfOptic
  :: (Representable s, Representable t, Representable a, Representable b)
  => s :.: RepCostar t :~> a :.: RepCostar b -> ProfOptic a b s t
mkProfOptic :: forall {x} {j} {k} {z} (s :: x +-> j) (t :: x +-> k) (a :: z +-> j)
       (b :: z +-> k).
(Representable s, Representable t, Representable a,
 Representable b) =>
((s :.: RepCostar t) :~> (a :.: RepCostar b)) -> ProfOptic a b s t
mkProfOptic (s :.: RepCostar t) :~> (a :.: RepCostar b)
n = (O (Companion (Path PROFK) Nil)
   (PK (RepCostar t) ::: (PK s ::: Nil))
 ~> O (PK (RepCostar b) ::: (PK a ::: Nil))
      (Companion (Path PROFK) Nil))
-> Sq
     '(PK (RepCostar t) ::: (PK s ::: Nil), Nil)
     '(PK (RepCostar b) ::: (PK a ::: 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 (PK (RepCostar t) ::: (PK s ::: Nil))
-> SPath (PK (RepCostar b) ::: (PK a ::: Nil))
-> (Fold (PK (RepCostar t) ::: (PK s ::: Nil))
    ~> Fold (PK (RepCostar b) ::: (PK a ::: Nil)))
-> Strictified
     (PK (RepCostar t) ::: (PK s ::: Nil))
     (PK (RepCostar b) ::: (PK a ::: 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 (Obj (PK (RepCostar t))
-> SPath (PK s ::: Nil)
-> SPath (PK (RepCostar t) ::: (PK s ::: 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 Obj (PK (RepCostar t))
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj (Obj (PK s) -> SPath Nil -> SPath (PK s ::: 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 Obj (PK s)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil)) (Obj (PK (RepCostar b))
-> SPath (PK a ::: Nil)
-> SPath (PK (RepCostar b) ::: (PK a ::: 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 Obj (PK (RepCostar b))
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj (Obj (PK a) -> SPath Nil -> SPath (PK a ::: 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 Obj (PK a)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj SPath Nil
forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath Nil
SNil)) (((s :.: RepCostar t) :~> (a :.: RepCostar b))
-> Prof (PK (s :.: RepCostar t)) (PK (a :.: RepCostar b))
forall {j} {k} (p1 :: j +-> k) (q1 :: j +-> k).
(Ob p1, Ob q1) =>
(p1 :~> q1) -> Prof (PK p1) (PK q1)
Prof (:.:) s (RepCostar t) a b -> (:.:) a (RepCostar b) a b
(s :.: RepCostar t) :~> (a :.: RepCostar b)
n))

type HaskOptic a b s t = ProfOptic (Star a) (Star b) (Star s) (Star t)
mkHaskOptic
  :: (Functor a, Functor b, Functor s, Functor t)
  => (forall x r. (Ob x) => (forall y. (Ob y) => (s x ~> a y) -> (b y ~> t x) -> r) -> r) -> HaskOptic a b s t
mkHaskOptic :: forall {z} {j} {k} {x} (a :: z -> j) (b :: z -> k) (s :: x -> j)
       (t :: x -> k).
(Functor a, Functor b, Functor s, Functor t) =>
(forall (x :: x) r.
 Ob x =>
 (forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r)
-> HaskOptic a b s t
mkHaskOptic forall (x :: x) r.
Ob x =>
(forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r
k = ((Star s :.: RepCostar (Star t))
 :~> (Star a :.: RepCostar (Star b)))
-> Sq
     '(Conjoint PROFK (SUB (PK (Star t)))
       ::: (Companion PROFK (SUB (PK (Star s))) ::: Nil),
       Nil)
     '(Conjoint PROFK (SUB (PK (Star b)))
       ::: (Companion PROFK (SUB (PK (Star a))) ::: Nil),
       Nil)
forall {x} {j} {k} {z} (s :: x +-> j) (t :: x +-> k) (a :: z +-> j)
       (b :: z +-> k).
(Representable s, Representable t, Representable a,
 Representable b) =>
((s :.: RepCostar t) :~> (a :.: RepCostar b)) -> ProfOptic a b s t
mkProfOptic \(Star @y a ~> s b
s :.: RepCostar (Star t % b) ~> b
t) -> forall (x :: x) r.
Ob x =>
(forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r
k @y \s b ~> a y
get b y ~> t b
put -> (a ~> a y) -> Star a a y
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (s b ~> a y
get (s b ~> a y) -> (a ~> s b) -> a ~> a y
forall (b :: j) (c :: j) (a :: j). (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
. a ~> s b
s) Star a a y
-> RepCostar (Star b) y b
-> (:.:) (Star a) (RepCostar (Star b)) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((Star b % y) ~> b) -> RepCostar (Star b) y b
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (t b ~> b
(Star t % b) ~> b
t (t b ~> b) -> (b y ~> t b) -> b y ~> b
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
. b y ~> t b
put)

type Lens s t a b = HaskOptic ((,) a) ((,) b) ((,) s) ((,) t)
mkLens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
mkLens :: forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
mkLens s -> a
f s -> b -> t
g = (forall x r.
 Ob x =>
 (forall y. Ob y => ((s, x) ~> (a, y)) -> ((b, y) ~> (t, x)) -> r)
 -> r)
-> Sq
     '(Conjoint PROFK (SUB (PK (Star ((,) t))))
       ::: (Companion PROFK (SUB (PK (Star ((,) s)))) ::: Nil),
       Nil)
     '(Conjoint PROFK (SUB (PK (Star ((,) b))))
       ::: (Companion PROFK (SUB (PK (Star ((,) a)))) ::: Nil),
       Nil)
forall {z} {j} {k} {x} (a :: z -> j) (b :: z -> k) (s :: x -> j)
       (t :: x -> k).
(Functor a, Functor b, Functor s, Functor t) =>
(forall (x :: x) r.
 Ob x =>
 (forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r)
-> HaskOptic a b s t
mkHaskOptic (\forall y. Ob y => ((s, x) ~> (a, y)) -> ((b, y) ~> (t, x)) -> r
k -> ((s, x) ~> (a, (b -> t, x))) -> ((b, (b -> t, x)) ~> (t, x)) -> r
forall y. Ob y => ((s, x) ~> (a, y)) -> ((b, y) ~> (t, x)) -> r
k (\(s
s, x
x) -> (s -> a
f s
s, (s -> b -> t
g s
s, x
x))) (\(b
b, (b -> t
bt, x
x)) -> (b -> t
bt b
b, x
x)))

type Prism s t a b = HaskOptic (Either a) (Either b) (Either s) (Either t)
mkPrism :: (s -> Either a t) -> (b -> t) -> Prism s t a b
mkPrism :: forall s a t b. (s -> Either a t) -> (b -> t) -> Prism s t a b
mkPrism s -> Either a t
f b -> t
g = (forall x r.
 Ob x =>
 (forall y.
  Ob y =>
  (Either s x ~> Either a y) -> (Either b y ~> Either t x) -> r)
 -> r)
-> Sq
     '(Conjoint PROFK (SUB (PK (Star (Either t))))
       ::: (Companion PROFK (SUB (PK (Star (Either s)))) ::: Nil),
       Nil)
     '(Conjoint PROFK (SUB (PK (Star (Either b))))
       ::: (Companion PROFK (SUB (PK (Star (Either a)))) ::: Nil),
       Nil)
forall {z} {j} {k} {x} (a :: z -> j) (b :: z -> k) (s :: x -> j)
       (t :: x -> k).
(Functor a, Functor b, Functor s, Functor t) =>
(forall (x :: x) r.
 Ob x =>
 (forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r)
-> HaskOptic a b s t
mkHaskOptic (\forall y.
Ob y =>
(Either s x ~> Either a y) -> (Either b y ~> Either t x) -> r
k -> (Either s x ~> Either a (Either t x))
-> (Either b (Either t x) ~> Either t x) -> r
forall y.
Ob y =>
(Either s x ~> Either a y) -> (Either b y ~> Either t x) -> r
k ((s -> Either a (Either t x))
-> (x -> Either a (Either t x))
-> Either s x
-> Either a (Either t x)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((a -> Either a (Either t x))
-> (t -> Either a (Either t x))
-> Either a t
-> Either a (Either t x)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Either a (Either t x)
forall a b. a -> Either a b
Left (Either t x -> Either a (Either t x)
forall a b. b -> Either a b
Right (Either t x -> Either a (Either t x))
-> (t -> Either t x) -> t -> Either a (Either t x)
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
. t -> Either t x
forall a b. a -> Either a b
Left) (Either a t -> Either a (Either t x))
-> (s -> Either a t) -> s -> Either a (Either t x)
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
. s -> Either a t
f) (Either t x -> Either a (Either t x)
forall a b. b -> Either a b
Right (Either t x -> Either a (Either t x))
-> (x -> Either t x) -> x -> Either a (Either t x)
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
. x -> Either t x
forall a b. b -> Either a b
Right)) ((b -> Either t x)
-> (Either t x -> Either t x)
-> Either b (Either t x)
-> Either t x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (t -> Either t x
forall a b. a -> Either a b
Left (t -> Either t x) -> (b -> t) -> b -> Either t x
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
. b -> t
g) Either t x -> Either t x
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id))

data FlipApp a f = FlipApp {forall {k} (a :: k) (f :: k -> Type). FlipApp a f -> f a
unFlipApp :: f a}
instance (Ob a) => Functor (FlipApp a) where
  map :: forall (a :: k -> Type) (b :: k -> Type).
(a ~> b) -> FlipApp a a ~> FlipApp a b
map (Nat a .~> b
f) (FlipApp a a
x) = b a -> FlipApp a b
forall {k} (a :: k) (f :: k -> Type). f a -> FlipApp a f
FlipApp (a a ~> b a
a a -> b a
a .~> b
f a a
x)
type Traversal s t a b = HaskOptic (FlipApp a) (FlipApp b) (FlipApp s) (FlipApp t)
mkTraversal :: (Traversable f, Functor f) => Traversal (f a) (f b) a b
mkTraversal :: forall (f :: Type -> Type) a b.
(Traversable f, Functor f) =>
Traversal (f a) (f b) a b
mkTraversal = (forall (x :: Type -> Type) r.
 Ob x =>
 (forall (y :: Type -> Type).
  Ob y =>
  (FlipApp (f a) x ~> FlipApp a y)
  -> (FlipApp b y ~> FlipApp (f b) x) -> r)
 -> r)
-> Sq
     '(Conjoint PROFK (SUB (PK (Star (FlipApp (f b)))))
       ::: (Companion PROFK (SUB (PK (Star (FlipApp (f a))))) ::: Nil),
       Nil)
     '(Conjoint PROFK (SUB (PK (Star (FlipApp b))))
       ::: (Companion PROFK (SUB (PK (Star (FlipApp a)))) ::: Nil),
       Nil)
forall {z} {j} {k} {x} (a :: z -> j) (b :: z -> k) (s :: x -> j)
       (t :: x -> k).
(Functor a, Functor b, Functor s, Functor t) =>
(forall (x :: x) r.
 Ob x =>
 (forall (y :: z). Ob y => (s x ~> a y) -> (b y ~> t x) -> r) -> r)
-> HaskOptic a b s t
mkHaskOptic (\forall (y :: Type -> Type).
Ob y =>
(FlipApp (f a) x ~> FlipApp a y)
-> (FlipApp b y ~> FlipApp (f b) x) -> r
k -> (FlipApp (f a) x ~> FlipApp a (Compose x f))
-> (FlipApp b (Compose x f) ~> FlipApp (f b) x) -> r
forall (y :: Type -> Type).
Ob y =>
(FlipApp (f a) x ~> FlipApp a y)
-> (FlipApp b y ~> FlipApp (f b) x) -> r
k (Compose x f a -> FlipApp a (Compose x f)
forall {k} (a :: k) (f :: k -> Type). f a -> FlipApp a f
FlipApp (Compose x f a -> FlipApp a (Compose x f))
-> (FlipApp (f a) x -> Compose x f a)
-> FlipApp (f a) x
-> FlipApp a (Compose x f)
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
. x (f a) -> Compose x f a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (x (f a) -> Compose x f a)
-> (FlipApp (f a) x -> x (f a)) -> FlipApp (f a) x -> Compose x f a
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
. FlipApp (f a) x -> x (f a)
forall {k} (a :: k) (f :: k -> Type). FlipApp a f -> f a
unFlipApp) (x (f b) -> FlipApp (f b) x
forall {k} (a :: k) (f :: k -> Type). f a -> FlipApp a f
FlipApp (x (f b) -> FlipApp (f b) x)
-> (FlipApp b (Compose x f) -> x (f b))
-> FlipApp b (Compose x f)
-> FlipApp (f b) x
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
. Compose x f b -> x (f b)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose x f b -> x (f b))
-> (FlipApp b (Compose x f) -> Compose x f b)
-> FlipApp b (Compose x f)
-> x (f b)
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
. FlipApp b (Compose x f) -> Compose x f b
forall {k} (a :: k) (f :: k -> Type). FlipApp a f -> f a
unFlipApp))