{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Squares, specialized to profunctors.
--
-- This is the profunctor-specific counterpart of "Proarrow.Equipment.Squares" in
-- @proarrow-equipment@: instead of squares over an arbitrary proarrow equipment, the
-- legs here are 'Proarrow.Path.Path's of plain profunctors (horizontal) or
-- 'Representable' profunctors (vertical, playing the role of the tight morphisms of the
-- @Prof@ equipment). "Proarrow.Path" does the associator\/unitor bookkeeping once, by
-- induction over the path, so the combinators below never have to. A square's payload is
-- stated as @'Fold' (p '+++' f) :~> 'Fold' (g '+++' q)@ (the fold of each side's
-- concatenated path) rather than @'Fold' f ':.:' 'Fold' p :~> 'Fold' q ':.:' 'Fold' g@: it
-- means combinators whose legs are trivial (@'Nil'@ or a single element) need no unitors
-- at all, since e.g. @'Nil' '+++' ps@ and @ps '+++' 'Nil'@ both reduce to @ps@ for free.
module Proarrow.Squares where

import Data.Kind (Type)
import Prelude (($))

import Proarrow.Adjunction (Proadjunction)
import Proarrow.Adjunction qualified as Adj
import Proarrow.Category.Instance.Prof qualified as P
import Proarrow.Category.Monoidal (Monoidal (..), type (**))
import Proarrow.Category.Monoidal.Action (Act, ActionAt, MonoidalAction (..), actHom)
import Proarrow.Category.Monoidal.EndoProf (ENDO (..), Precomp)
import Proarrow.Category.Monoidal.Rev (REV (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), obj, rmap, (//), (:~>), (\\), type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Optic (ExOptic (..))
import Proarrow.Optic.Action (ActFl (..))
import Proarrow.Path
  ( Fold
  , IsPath
  , IsTight
  , Path (..)
  , SPath (..)
  , Tag (..)
  , appendPath
  , idN
  , singPath
  , weakenTight
  , whiskerL
  , whiskerR
  , withAssoc
  , withFoldOb
  , withFoldRep
  , withObAppend
  , type (+++)
  )
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (CorepStar (..), Rep (..), Representable (..))

infixl 6 |||
infixl 5 ===

-- | The kind of a square @p q f g@.
--
-- > h--f--i
-- > |  v  |
-- > p--@--q
-- > |  v  |
-- > j--g--k
type Sq :: Path j h -> Path k i -> Path h i -> Path j k -> Type
data Sq p q f g where
  Sq
    :: (IsPath p, IsPath q, IsTight f, IsTight g)
    => Fold (p +++ f) :~> Fold (g +++ q)
    -> Sq p q f g

-- | The empty square for an object.
--
-- > K-----K
-- > |     |
-- > |     |
-- > |     |
-- > K-----K
object :: (CategoryOf k) => Sq (Nil :: Path k k) Nil Nil Nil
object :: forall k. CategoryOf k => Sq Nil Nil Nil Nil
object = (Fold (Nil +++ Nil) :~> Fold (Nil +++ Nil)) -> Sq Nil Nil Nil Nil
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq Id a b -> Id a b
Fold (Nil +++ Nil) a b -> Fold (Nil +++ Nil) a b
Fold (Nil +++ Nil) :~> Fold (Nil +++ Nil)
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN

-- | Make a square from a horizontal proarrow.
--
-- > K-----K
-- > |     |
-- > p--@--q
-- > |     |
-- > J-----J
hArr :: (Profunctor p, Profunctor q) => p :~> q -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr :: forall {k} {i} (p :: k +-> i) (q :: k +-> i).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr = (forall (a :: i) (b :: k). p a b -> q a b)
-> Sq (p ::: Nil) (q ::: Nil) Nil Nil
(Fold ((p ::: Nil) +++ Nil) :~> Fold (Nil +++ (q ::: Nil)))
-> Sq (p ::: Nil) (q ::: Nil) Nil Nil
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq

-- | A horizontal identity square.
--
-- > J-----J
-- > |     |
-- > p-----p
-- > |     |
-- > K-----K
hId :: (Profunctor p) => Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId :: forall {k} {i} (p :: k +-> i).
Profunctor p =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId = (p :~> p) -> Sq (p ::: Nil) (p ::: Nil) Nil Nil
forall {k} {i} (p :: k +-> i) (q :: k +-> i).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr p a b -> p a b
p :~> p
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN

-- | Make a square from a vertical arrow.
--
-- > J--f--K
-- > |  v  |
-- > |  @  |
-- > |  v  |
-- > J--g--K
vArr :: (Representable f, Representable g) => f :~> g -> Sq Nil Nil (f ::: Nil) (g ::: Nil)
vArr :: forall {j} {k} (f :: j +-> k) (g :: j +-> k).
(Representable f, Representable g) =>
(f :~> g) -> Sq Nil Nil (f ::: Nil) (g ::: Nil)
vArr = (forall (a :: k) (b :: j). f a b -> g a b)
-> Sq Nil Nil (f ::: Nil) (g ::: Nil)
(Fold (Nil +++ (f ::: Nil)) :~> Fold ((g ::: Nil) +++ Nil))
-> Sq Nil Nil (f ::: Nil) (g ::: Nil)
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq

-- | A vertical identity square.
--
-- > J--f--K
-- > |  v  |
-- > |  |  |
-- > |  v  |
-- > J--f--K
vId :: (Representable f) => Sq Nil Nil (f ::: Nil) (f ::: Nil)
vId :: forall {j} {k} (f :: j +-> k).
Representable f =>
Sq Nil Nil (f ::: Nil) (f ::: Nil)
vId = (f :~> f) -> Sq Nil Nil (f ::: Nil) (f ::: Nil)
forall {j} {k} (f :: j +-> k) (g :: j +-> k).
(Representable f, Representable g) =>
(f :~> g) -> Sq Nil Nil (f ::: Nil) (g ::: Nil)
vArr f a b -> f a b
f :~> f
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN

-- | 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 ps qs rs ds es fs gs. Sq ps qs ds es -> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
Sq Fold (ps +++ ds) :~> Fold (es +++ qs)
l ||| :: forall {a} {a} {b} {b} {c} {c} (ps :: Path a a) (qs :: Path b b)
       (rs :: Path c c) (ds :: Path a b) (es :: Path a b) (fs :: Path b c)
       (gs :: Path b c).
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| Sq Fold (qs +++ fs) :~> Fold (gs +++ rs)
r =
  forall {j} {b} {k} (t :: Tag) (ps :: Path j b) (qs :: Path b k) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
forall (t :: Tag) (ps :: Path a b) (qs :: Path b c) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
withObAppend @Tight @ds @fs SPath 'Tight ds
tds ((IsOb 'Tight (ds +++ fs) => Sq ps rs (ds +++ fs) (es +++ gs))
 -> Sq ps rs (ds +++ fs) (es +++ gs))
-> (IsOb 'Tight (ds +++ fs) => Sq ps rs (ds +++ fs) (es +++ gs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall a b. (a -> b) -> a -> b
$
    forall {j} {b} {k} (t :: Tag) (ps :: Path j b) (qs :: Path b k) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
forall (t :: Tag) (ps :: Path a b) (qs :: Path b c) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
withObAppend @Tight @es @gs SPath 'Tight es
tes ((IsOb 'Tight (es +++ gs) => Sq ps rs (ds +++ fs) (es +++ gs))
 -> Sq ps rs (ds +++ fs) (es +++ gs))
-> (IsOb 'Tight (es +++ gs) => Sq ps rs (ds +++ fs) (es +++ gs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall a b. (a -> b) -> a -> b
$
      forall {a1} {a2} {b} {c} (ps :: Path a1 a2) (qs :: Path a2 b)
       (rs :: Path b c) (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
forall (ps :: Path a a) (qs :: Path a b) (rs :: Path b c)
       (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
withAssoc @ps @ds @fs @Prof ((Assoc ps ds fs => Sq ps rs (ds +++ fs) (es +++ gs))
 -> Sq ps rs (ds +++ fs) (es +++ gs))
-> (Assoc ps ds fs => Sq ps rs (ds +++ fs) (es +++ gs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall a b. (a -> b) -> a -> b
$
        forall {a1} {a2} {b} {c} (ps :: Path a1 a2) (qs :: Path a2 b)
       (rs :: Path b c) (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
forall (ps :: Path a b) (qs :: Path b b) (rs :: Path b c)
       (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
withAssoc @es @qs @fs @Tight ((Assoc es qs fs => Sq ps rs (ds +++ fs) (es +++ gs))
 -> Sq ps rs (ds +++ fs) (es +++ gs))
-> (Assoc es qs fs => Sq ps rs (ds +++ fs) (es +++ gs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall a b. (a -> b) -> a -> b
$
          forall {a1} {a2} {b} {c} (ps :: Path a1 a2) (qs :: Path a2 b)
       (rs :: Path b c) (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
forall (ps :: Path a b) (qs :: Path b c) (rs :: Path c c)
       (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
withAssoc @es @gs @rs @Tight ((Assoc es gs rs => Sq ps rs (ds +++ fs) (es +++ gs))
 -> Sq ps rs (ds +++ fs) (es +++ gs))
-> (Assoc es gs rs => Sq ps rs (ds +++ fs) (es +++ gs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall a b. (a -> b) -> a -> b
$
            (Fold (ps +++ (ds +++ fs)) :~> Fold ((es +++ gs) +++ rs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq ((Fold (ps +++ (ds +++ fs)) :~> Fold ((es +++ gs) +++ rs))
 -> Sq ps rs (ds +++ fs) (es +++ gs))
-> (Fold (ps +++ (ds +++ fs)) :~> Fold ((es +++ gs) +++ rs))
-> Sq ps rs (ds +++ fs) (es +++ gs)
forall a b. (a -> b) -> a -> b
$
              SPath 'Prof es
-> SPath 'Prof (qs +++ fs)
-> SPath 'Prof (gs +++ rs)
-> (Fold (qs +++ fs) :~> Fold (gs +++ rs))
-> Fold (es +++ (qs +++ fs)) :~> Fold (es +++ (gs +++ rs))
forall {j} {b} {k} (xs :: Path j b) (ys :: Path b k)
       (zs :: Path b k).
SPath 'Prof xs
-> SPath 'Prof ys
-> SPath 'Prof zs
-> (Fold ys :~> Fold zs)
-> Fold (xs +++ ys) :~> Fold (xs +++ zs)
whiskerL SPath 'Prof es
ses (SPath 'Prof qs -> SPath 'Prof fs -> SPath 'Prof (qs +++ fs)
forall {a} {b1} {b2} (t :: Tag) (ps :: Path a b1)
       (qs :: Path b1 b2).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath 'Prof qs
sqs SPath 'Prof fs
sfs) (SPath 'Prof gs -> SPath 'Prof rs -> SPath 'Prof (gs +++ rs)
forall {a} {b1} {b2} (t :: Tag) (ps :: Path a b1)
       (qs :: Path b1 b2).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath 'Prof gs
sgs SPath 'Prof rs
srs) Fold (qs +++ fs) a b -> Fold (gs +++ rs) a b
Fold (qs +++ fs) :~> Fold (gs +++ rs)
r
                (Fold (es +++ (qs +++ fs)) a b -> Fold (es +++ (gs +++ rs)) a b)
-> (Fold (ps +++ (ds +++ fs)) a b -> Fold (es +++ (qs +++ fs)) a b)
-> Fold (ps +++ (ds +++ fs)) a b
-> Fold (es +++ (gs +++ rs)) a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. SPath 'Prof (ps +++ ds)
-> SPath 'Prof (es +++ qs)
-> SPath 'Prof fs
-> (Fold (ps +++ ds) :~> Fold (es +++ qs))
-> Fold ((ps +++ ds) +++ fs) :~> Fold ((es +++ qs) +++ fs)
forall {j} {b} {k} (xs :: Path j b) (ys :: Path j b)
       (zs :: Path b k).
SPath 'Prof xs
-> SPath 'Prof ys
-> SPath 'Prof zs
-> (Fold xs :~> Fold ys)
-> Fold (xs +++ zs) :~> Fold (ys +++ zs)
whiskerR (SPath 'Prof ps -> SPath 'Prof ds -> SPath 'Prof (ps +++ ds)
forall {a} {b1} {b2} (t :: Tag) (ps :: Path a b1)
       (qs :: Path b1 b2).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath 'Prof ps
sps SPath 'Prof ds
sds) (SPath 'Prof es -> SPath 'Prof qs -> SPath 'Prof (es +++ qs)
forall {a} {b1} {b2} (t :: Tag) (ps :: Path a b1)
       (qs :: Path b1 b2).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath 'Prof es
ses SPath 'Prof qs
sqs) SPath 'Prof fs
sfs Fold (ps +++ ds) a b -> Fold (es +++ qs) a b
Fold (ps +++ ds) :~> Fold (es +++ qs)
l
  where
    tds :: SPath Tight ds
    tds :: SPath 'Tight ds
tds = SPath 'Tight ds
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    tes :: SPath Tight es
    tes :: SPath 'Tight es
tes = SPath 'Tight es
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    sps :: SPath Prof ps
    sps :: SPath 'Prof ps
sps = SPath 'Prof ps
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    sqs :: SPath Prof qs
    sqs :: SPath 'Prof qs
sqs = SPath 'Prof qs
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    srs :: SPath Prof rs
    srs :: SPath 'Prof rs
srs = SPath 'Prof rs
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    sds :: SPath Prof ds
    sds :: SPath 'Prof ds
sds = SPath 'Tight ds -> SPath 'Prof ds
forall {a} {b} (ps :: Path a b). SPath 'Tight ps -> SPath 'Prof ps
weakenTight SPath 'Tight ds
tds
    ses :: SPath Prof es
    ses :: SPath 'Prof es
ses = SPath 'Tight es -> SPath 'Prof es
forall {a} {b} (ps :: Path a b). SPath 'Tight ps -> SPath 'Prof ps
weakenTight SPath 'Tight es
tes
    sfs :: SPath Prof fs
    sfs :: SPath 'Prof fs
sfs = SPath 'Tight fs -> SPath 'Prof fs
forall {a} {b} (ps :: Path a b). SPath 'Tight ps -> SPath 'Prof ps
weakenTight SPath 'Tight fs
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    sgs :: SPath Prof gs
    sgs :: SPath 'Prof gs
sgs = SPath 'Tight gs -> SPath 'Prof gs
forall {a} {b} (ps :: Path a b). SPath 'Tight ps -> SPath 'Prof ps
weakenTight SPath 'Tight gs
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath

-- | 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 rs ss es fs ps qs gs. Sq rs ss es fs -> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
Sq Fold (rs +++ es) :~> Fold (fs +++ ss)
top === :: forall {b} {h} {b} {i} {j} {k} (rs :: Path b h) (ss :: Path b i)
       (es :: Path h i) (fs :: Path b b) (ps :: Path j b) (qs :: Path k b)
       (gs :: Path j k).
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== Sq Fold (ps +++ fs) :~> Fold (gs +++ qs)
bot =
  forall {j} {b} {k} (t :: Tag) (ps :: Path j b) (qs :: Path b k) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
forall (t :: Tag) (ps :: Path j b) (qs :: Path b h) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
withObAppend @Prof @ps @rs SPath 'Prof ps
sps ((IsOb 'Prof (ps +++ rs) => Sq (ps +++ rs) (qs +++ ss) es gs)
 -> Sq (ps +++ rs) (qs +++ ss) es gs)
-> (IsOb 'Prof (ps +++ rs) => Sq (ps +++ rs) (qs +++ ss) es gs)
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall a b. (a -> b) -> a -> b
$
    forall {j} {b} {k} (t :: Tag) (ps :: Path j b) (qs :: Path b k) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
forall (t :: Tag) (ps :: Path k b) (qs :: Path b i) r.
IsOb t qs =>
SPath t ps -> (IsOb t (ps +++ qs) => r) -> r
withObAppend @Prof @qs @ss SPath 'Prof qs
sqs ((IsOb 'Prof (qs +++ ss) => Sq (ps +++ rs) (qs +++ ss) es gs)
 -> Sq (ps +++ rs) (qs +++ ss) es gs)
-> (IsOb 'Prof (qs +++ ss) => Sq (ps +++ rs) (qs +++ ss) es gs)
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall a b. (a -> b) -> a -> b
$
      forall {a1} {a2} {b} {c} (ps :: Path a1 a2) (qs :: Path a2 b)
       (rs :: Path b c) (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
forall (ps :: Path j k) (qs :: Path k b) (rs :: Path b i)
       (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
withAssoc @gs @qs @ss @Tight ((Assoc gs qs ss => Sq (ps +++ rs) (qs +++ ss) es gs)
 -> Sq (ps +++ rs) (qs +++ ss) es gs)
-> (Assoc gs qs ss => Sq (ps +++ rs) (qs +++ ss) es gs)
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall a b. (a -> b) -> a -> b
$
        forall {a1} {a2} {b} {c} (ps :: Path a1 a2) (qs :: Path a2 b)
       (rs :: Path b c) (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
forall (ps :: Path j b) (qs :: Path b h) (rs :: Path h i)
       (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
withAssoc @ps @rs @es @Prof ((Assoc ps rs es => Sq (ps +++ rs) (qs +++ ss) es gs)
 -> Sq (ps +++ rs) (qs +++ ss) es gs)
-> (Assoc ps rs es => Sq (ps +++ rs) (qs +++ ss) es gs)
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall a b. (a -> b) -> a -> b
$
          forall {a1} {a2} {b} {c} (ps :: Path a1 a2) (qs :: Path a2 b)
       (rs :: Path b c) (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
forall (ps :: Path j b) (qs :: Path b b) (rs :: Path b i)
       (t :: Tag) r.
IsOb t ps =>
(Assoc ps qs rs => r) -> r
withAssoc @ps @fs @ss @Prof ((Assoc ps fs ss => Sq (ps +++ rs) (qs +++ ss) es gs)
 -> Sq (ps +++ rs) (qs +++ ss) es gs)
-> (Assoc ps fs ss => Sq (ps +++ rs) (qs +++ ss) es gs)
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall a b. (a -> b) -> a -> b
$
            (Fold ((ps +++ rs) +++ es) :~> Fold (gs +++ (qs +++ ss)))
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq ((Fold ((ps +++ rs) +++ es) :~> Fold (gs +++ (qs +++ ss)))
 -> Sq (ps +++ rs) (qs +++ ss) es gs)
-> (Fold ((ps +++ rs) +++ es) :~> Fold (gs +++ (qs +++ ss)))
-> Sq (ps +++ rs) (qs +++ ss) es gs
forall a b. (a -> b) -> a -> b
$
              SPath 'Prof (ps +++ fs)
-> SPath 'Prof (gs +++ qs)
-> SPath 'Prof ss
-> (Fold (ps +++ fs) :~> Fold (gs +++ qs))
-> Fold ((ps +++ fs) +++ ss) :~> Fold ((gs +++ qs) +++ ss)
forall {j} {b} {k} (xs :: Path j b) (ys :: Path j b)
       (zs :: Path b k).
SPath 'Prof xs
-> SPath 'Prof ys
-> SPath 'Prof zs
-> (Fold xs :~> Fold ys)
-> Fold (xs +++ zs) :~> Fold (ys +++ zs)
whiskerR (SPath 'Prof ps -> SPath 'Prof fs -> SPath 'Prof (ps +++ fs)
forall {a} {b1} {b2} (t :: Tag) (ps :: Path a b1)
       (qs :: Path b1 b2).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath 'Prof ps
sps SPath 'Prof fs
sfs) (SPath 'Prof gs -> SPath 'Prof qs -> SPath 'Prof (gs +++ qs)
forall {a} {b1} {b2} (t :: Tag) (ps :: Path a b1)
       (qs :: Path b1 b2).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath 'Prof gs
sgs SPath 'Prof qs
sqs) SPath 'Prof ss
sss Fold (ps +++ fs) a b -> Fold (gs +++ qs) a b
Fold (ps +++ fs) :~> Fold (gs +++ qs)
bot
                (Fold ((ps +++ fs) +++ ss) a b -> Fold (gs +++ (qs +++ ss)) a b)
-> (Fold (ps +++ (rs +++ es)) a b -> Fold ((ps +++ fs) +++ ss) a b)
-> Fold (ps +++ (rs +++ es)) a b
-> Fold (gs +++ (qs +++ ss)) a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. SPath 'Prof ps
-> SPath 'Prof (rs +++ es)
-> SPath 'Prof (fs +++ ss)
-> (Fold (rs +++ es) :~> Fold (fs +++ ss))
-> Fold (ps +++ (rs +++ es)) :~> Fold (ps +++ (fs +++ ss))
forall {j} {b} {k} (xs :: Path j b) (ys :: Path b k)
       (zs :: Path b k).
SPath 'Prof xs
-> SPath 'Prof ys
-> SPath 'Prof zs
-> (Fold ys :~> Fold zs)
-> Fold (xs +++ ys) :~> Fold (xs +++ zs)
whiskerL SPath 'Prof ps
sps (SPath 'Prof rs -> SPath 'Prof es -> SPath 'Prof (rs +++ es)
forall {a} {b1} {b2} (t :: Tag) (ps :: Path a b1)
       (qs :: Path b1 b2).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath 'Prof rs
srs SPath 'Prof es
ses) (SPath 'Prof fs -> SPath 'Prof ss -> SPath 'Prof (fs +++ ss)
forall {a} {b1} {b2} (t :: Tag) (ps :: Path a b1)
       (qs :: Path b1 b2).
SPath t ps -> SPath t qs -> SPath t (ps +++ qs)
appendPath SPath 'Prof fs
sfs SPath 'Prof ss
sss) Fold (rs +++ es) a b -> Fold (fs +++ ss) a b
Fold (rs +++ es) :~> Fold (fs +++ ss)
top
  where
    sps :: SPath Prof ps
    sps :: SPath 'Prof ps
sps = SPath 'Prof ps
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    sqs :: SPath Prof qs
    sqs :: SPath 'Prof qs
sqs = SPath 'Prof qs
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    srs :: SPath Prof rs
    srs :: SPath 'Prof rs
srs = SPath 'Prof rs
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    sss :: SPath Prof ss
    sss :: SPath 'Prof ss
sss = SPath 'Prof ss
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    ses :: SPath Prof es
    ses :: SPath 'Prof es
ses = SPath 'Tight es -> SPath 'Prof es
forall {a} {b} (ps :: Path a b). SPath 'Tight ps -> SPath 'Prof ps
weakenTight SPath 'Tight es
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    sfs :: SPath Prof fs
    sfs :: SPath 'Prof fs
sfs = SPath 'Tight fs -> SPath 'Prof fs
forall {a} {b} (ps :: Path a b). SPath 'Tight ps -> SPath 'Prof ps
weakenTight SPath 'Tight fs
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath
    sgs :: SPath Prof gs
    sgs :: SPath 'Prof gs
sgs = SPath 'Tight gs -> SPath 'Prof gs
forall {a} {b} (ps :: Path a b). SPath 'Tight ps -> SPath 'Prof ps
weakenTight SPath 'Tight gs
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath

-- | Bend a vertical arrow in the companion direction.
--
-- > J--f--K
-- > |  v  |
-- > |  \->f
-- > |     |
-- > J-----J
toRight :: (Representable f) => Sq Nil (f ::: Nil) (f ::: Nil) Nil
toRight :: forall {h} {k} (f :: h +-> k).
Representable f =>
Sq Nil (f ::: Nil) (f ::: Nil) Nil
toRight = (Fold (Nil +++ (f ::: Nil)) :~> Fold (Nil +++ (f ::: Nil)))
-> Sq Nil (f ::: Nil) (f ::: Nil) Nil
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq f a b -> f a b
Fold (Nil +++ (f ::: Nil)) a b -> Fold (Nil +++ (f ::: Nil)) a b
Fold (Nil +++ (f ::: Nil)) :~> Fold (Nil +++ (f ::: Nil))
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN

-- | Bend a vertical arrow in the conjoint direction.
--
-- > J--f--K
-- > |  v  |
-- > f<-/  |
-- > |     |
-- > K-----K
toLeft :: forall f f'. (Proadjunction f f', Representable f) => Sq (f' ::: Nil) Nil (f ::: Nil) Nil
toLeft :: forall {j} {i} (f :: j +-> i) (f' :: i +-> j).
(Proadjunction f f', Representable f) =>
Sq (f' ::: Nil) Nil (f ::: Nil) Nil
toLeft = (Fold ((f' ::: Nil) +++ (f ::: Nil)) :~> Fold (Nil +++ Nil))
-> Sq (f' ::: Nil) Nil (f ::: Nil) Nil
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq (forall {j} {k1} (p :: j +-> k1) (q :: k1 +-> j).
Proadjunction p q =>
(p :.: q) :~> Id
forall (p :: j +-> i) (q :: i +-> j).
Proadjunction p q =>
(p :.: q) :~> Id
counitNat @f @f')

-- | Bend a companion proarrow back to a vertical arrow.
--
-- > K-----K
-- > |     |
-- > f>-\  |
-- > |  v  |
-- > J--f--K
fromLeft :: (Representable f) => Sq (f ::: Nil) Nil Nil (f ::: Nil)
fromLeft :: forall {j} {k} (f :: j +-> k).
Representable f =>
Sq (f ::: Nil) Nil Nil (f ::: Nil)
fromLeft = (Fold ((f ::: Nil) +++ Nil) :~> Fold ((f ::: Nil) +++ Nil))
-> Sq (f ::: Nil) Nil Nil (f ::: Nil)
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq f a b -> f a b
Fold ((f ::: Nil) +++ Nil) a b -> Fold ((f ::: Nil) +++ Nil) a b
Fold ((f ::: Nil) +++ Nil) :~> Fold ((f ::: Nil) +++ Nil)
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN

-- | Bend a conjoint proarrow back to a vertical arrow.
--
-- > J-----J
-- > |     |
-- > |  /-<f
-- > |  v  |
-- > J--f--K
fromRight :: forall f f'. (Proadjunction f f', Representable f) => Sq Nil (f' ::: Nil) Nil (f ::: Nil)
fromRight :: forall {j} {k} (f :: j +-> k) (f' :: k +-> j).
(Proadjunction f f', Representable f) =>
Sq Nil (f' ::: Nil) Nil (f ::: Nil)
fromRight = (Fold (Nil +++ Nil) :~> Fold ((f ::: Nil) +++ (f' ::: Nil)))
-> Sq Nil (f' ::: Nil) Nil (f ::: Nil)
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq (forall {k1} {j} (p :: k1 +-> j) (q :: j +-> k1).
Proadjunction p q =>
Id :~> (q :.: p)
forall (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
Id :~> (q :.: p)
unitNat @f @f')

unitNat :: forall p q. (Proadjunction p q) => Id :~> q :.: p
unitNat :: forall {k1} {j} (p :: k1 +-> j) (q :: j +-> k1).
Proadjunction p q =>
Id :~> (q :.: p)
unitNat (Id a ~> b
f) = (a ~> b) -> (:.:) q p a a -> (:.:) q p a b
forall (b :: k1) (d :: k1) (a :: k1).
(b ~> d) -> (:.:) q p a b -> (:.:) q p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> b
f (forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: k1 +-> j) (q :: j +-> k1) (a :: k1).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
Adj.unit @p @q) ((Ob a, Ob b) => (:.:) q p a b) -> (a ~> b) -> (:.:) q p a b
forall (a :: k1) (b :: k1) 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
\\ a ~> b
f

counitNat :: forall p q. (Proadjunction p q) => p :.: q :~> Id
counitNat :: forall {j} {k1} (p :: j +-> k1) (q :: k1 +-> j).
Proadjunction p q =>
(p :.: q) :~> Id
counitNat (:.:) p q a b
pq = (a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((:.:) p q a b -> a ~> b
(p :.: q) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
Adj.counit (:.:) p q a b
pq)

-- > K--I--K
-- > |  v  |
-- > |  @  |
-- > |     |
-- > K-----K
vUnitor :: forall k. (CategoryOf k) => Sq Nil Nil ((Id :: CAT k) ::: Nil) Nil
vUnitor :: forall k. CategoryOf k => Sq Nil Nil (Id ::: Nil) Nil
vUnitor = forall {h} {i} (ps :: Path h i).
IsTight ps =>
Sq Nil Nil (Fold ps ::: Nil) ps
forall (ps :: Path k k).
IsTight ps =>
Sq Nil Nil (Fold ps ::: Nil) ps
vSplitAll @Nil

-- > K-----K
-- > |     |
-- > |  @  |
-- > |  v  |
-- > K--I--K
vUnitorInv :: forall k. (CategoryOf k) => Sq Nil Nil Nil ((Id :: CAT k) ::: Nil)
vUnitorInv :: forall k. CategoryOf k => Sq Nil Nil Nil (Id ::: Nil)
vUnitorInv = forall {j} {k} (ps :: Path j k).
IsTight ps =>
Sq Nil Nil ps (Fold ps ::: Nil)
forall (ps :: Path k k).
IsTight ps =>
Sq Nil Nil ps (Fold ps ::: Nil)
vCombineAll @Nil

-- > I-f-g-K
-- > | v v |
-- > | \@/ |
-- > |  v  |
-- > I-gof-K
vCombine :: forall p q. (Representable p, Representable q) => Sq Nil Nil (p ::: q ::: Nil) (q :.: p ::: Nil)
vCombine :: forall {j} {j} {k} (p :: j +-> j) (q :: j +-> k).
(Representable p, Representable q) =>
Sq Nil Nil (p ::: (q ::: Nil)) ((q :.: p) ::: Nil)
vCombine = forall {j} {k} (ps :: Path j k).
IsTight ps =>
Sq Nil Nil ps (Fold ps ::: Nil)
forall (ps :: Path j k).
IsTight ps =>
Sq Nil Nil ps (Fold ps ::: Nil)
vCombineAll @(p ::: q ::: Nil)

-- > I-gof-K
-- > |  v  |
-- > | /@\ |
-- > | v v |
-- > I-f-g-K
vSplit :: forall p q. (Representable p, Representable q) => Sq Nil Nil (q :.: p ::: Nil) (p ::: q ::: Nil)
vSplit :: forall {j} {j} {k} (p :: j +-> j) (q :: j +-> k).
(Representable p, Representable q) =>
Sq Nil Nil ((q :.: p) ::: Nil) (p ::: (q ::: Nil))
vSplit = forall {h} {i} (ps :: Path h i).
IsTight ps =>
Sq Nil Nil (Fold ps ::: Nil) ps
forall (ps :: Path j k).
IsTight ps =>
Sq Nil Nil (Fold ps ::: Nil) ps
vSplitAll @(p ::: q ::: Nil)

-- | Combine a whole bunch of vertical arrows into one composed arrow.
--
-- > J-p..-K
-- > | vvv |
-- > | \@/ |
-- > |  v  |
-- > J--f--K
vCombineAll :: forall ps. (IsTight ps) => Sq Nil Nil ps (Fold ps ::: Nil)
vCombineAll :: forall {j} {k} (ps :: Path j k).
IsTight ps =>
Sq Nil Nil ps (Fold ps ::: Nil)
vCombineAll = SPath 'Tight ps
-> (Representable (Fold ps) => Sq Nil Nil ps (Fold ps ::: Nil))
-> Sq Nil Nil ps (Fold ps ::: Nil)
forall {j} {k} (ps :: Path j k) r.
SPath 'Tight ps -> (Representable (Fold ps) => r) -> r
withFoldRep SPath 'Tight ps
tp ((Fold (Nil +++ ps) :~> Fold ((Fold ps ::: Nil) +++ Nil))
-> Sq Nil Nil ps (Fold ps ::: Nil)
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq Fold ps a b -> Fold ps a b
Fold (Nil +++ ps) a b -> Fold ((Fold ps ::: Nil) +++ Nil) a b
Fold (Nil +++ ps) :~> Fold ((Fold ps ::: Nil) +++ Nil)
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN)
  where
    tp :: SPath Tight ps
    tp :: SPath 'Tight ps
tp = SPath 'Tight ps
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath

-- | Split one composed arrow into a whole bunch of vertical arrows.
--
-- > J--f--K
-- > |  v  |
-- > | /@\ |
-- > | vvv |
-- > J-p..-K
vSplitAll :: forall ps. (IsTight ps) => Sq Nil Nil (Fold ps ::: Nil) ps
vSplitAll :: forall {h} {i} (ps :: Path h i).
IsTight ps =>
Sq Nil Nil (Fold ps ::: Nil) ps
vSplitAll = SPath 'Tight ps
-> (Representable (Fold ps) => Sq Nil Nil (Fold ps ::: Nil) ps)
-> Sq Nil Nil (Fold ps ::: Nil) ps
forall {j} {k} (ps :: Path j k) r.
SPath 'Tight ps -> (Representable (Fold ps) => r) -> r
withFoldRep SPath 'Tight ps
tp ((Fold (Nil +++ (Fold ps ::: Nil)) :~> Fold (ps +++ Nil))
-> Sq Nil Nil (Fold ps ::: Nil) ps
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq Fold ps a b -> Fold ps a b
Fold (Nil +++ (Fold ps ::: Nil)) a b -> Fold (ps +++ Nil) a b
Fold (Nil +++ (Fold ps ::: Nil)) :~> Fold (ps +++ Nil)
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN)
  where
    tp :: SPath Tight ps
    tp :: SPath 'Tight ps
tp = SPath 'Tight ps
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath

-- | Combine a whole bunch of horizontal proarrows into one composed proarrow.
--
-- > K-----K
-- > p--\  |
-- > :--@--F
-- > :--/  |
-- > J-----J
hCombineAll :: forall ps. (IsPath ps) => Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll :: forall {k} {i} (ps :: Path k i).
IsPath ps =>
Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll = SPath 'Prof ps
-> (Profunctor (Fold ps) => Sq ps (Fold ps ::: Nil) Nil Nil)
-> Sq ps (Fold ps ::: Nil) Nil Nil
forall {j} {k} (ps :: Path j k) r.
SPath 'Prof ps -> (Profunctor (Fold ps) => r) -> r
withFoldOb SPath 'Prof ps
sp ((Fold (ps +++ Nil) :~> Fold (Nil +++ (Fold ps ::: Nil)))
-> Sq ps (Fold ps ::: Nil) Nil Nil
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq Fold ps a b -> Fold ps a b
Fold (ps +++ Nil) a b -> Fold (Nil +++ (Fold ps ::: Nil)) a b
Fold (ps +++ Nil) :~> Fold (Nil +++ (Fold ps ::: Nil))
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN)
  where
    sp :: SPath Prof ps
    sp :: SPath 'Prof ps
sp = SPath 'Prof ps
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath

-- | Split one composed proarrow into a whole bunch of horizontal proarrows.
--
-- > K-----K
-- > |  /--p
-- > F--@--:
-- > |  \--:
-- > J-----J
hSplitAll :: forall ps. (IsPath ps) => Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll :: forall {k} {i} (ps :: Path k i).
IsPath ps =>
Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll = SPath 'Prof ps
-> (Profunctor (Fold ps) => Sq (Fold ps ::: Nil) ps Nil Nil)
-> Sq (Fold ps ::: Nil) ps Nil Nil
forall {j} {k} (ps :: Path j k) r.
SPath 'Prof ps -> (Profunctor (Fold ps) => r) -> r
withFoldOb SPath 'Prof ps
sp ((Fold ((Fold ps ::: Nil) +++ Nil) :~> Fold (Nil +++ ps))
-> Sq (Fold ps ::: Nil) ps Nil Nil
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq Fold ps a b -> Fold ps a b
Fold ((Fold ps ::: Nil) +++ Nil) a b -> Fold (Nil +++ ps) a b
Fold ((Fold ps ::: Nil) +++ Nil) :~> Fold (Nil +++ ps)
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
idN)
  where
    sp :: SPath Prof ps
    sp :: SPath 'Prof ps
sp = SPath 'Prof ps
forall j k (t :: Tag) (ps :: Path j k). IsOb t ps => SPath t ps
singPath

-- | The unit of an adjunction.
--
-- > J-------J
-- > |   /---q
-- > |   @   |
-- > |   \---p
-- > J-------J
unit :: forall p q. (Proadjunction p q) => Sq Nil (p ::: q ::: Nil) Nil Nil
unit :: forall {i} {j} (p :: i +-> j) (q :: j +-> i).
Proadjunction p q =>
Sq Nil (p ::: (q ::: Nil)) Nil Nil
unit = forall {k} {i} (ps :: Path k i).
IsPath ps =>
Sq ps (Fold ps ::: Nil) Nil Nil
forall (ps :: Path i i).
IsPath ps =>
Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll @Nil Sq Nil (Id ::: Nil) Nil Nil
-> Sq (Id ::: Nil) ((q :.: p) ::: Nil) Nil Nil
-> Sq Nil ((q :.: p) ::: Nil) (Nil +++ Nil) (Nil +++ Nil)
forall {a} {a} {b} {b} {c} {c} (ps :: Path a a) (qs :: Path b b)
       (rs :: Path c c) (ds :: Path a b) (es :: Path a b) (fs :: Path b c)
       (gs :: Path b c).
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| (Id :~> (q :.: p)) -> Sq (Id ::: Nil) ((q :.: p) ::: Nil) Nil Nil
forall {k} {i} (p :: k +-> i) (q :: k +-> i).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr (forall {k1} {j} (p :: k1 +-> j) (q :: j +-> k1).
Proadjunction p q =>
Id :~> (q :.: p)
forall (p :: i +-> j) (q :: j +-> i).
Proadjunction p q =>
Id :~> (q :.: p)
unitNat @p @q) Sq Nil ((q :.: p) ::: Nil) Nil Nil
-> Sq ((q :.: p) ::: Nil) (p ::: (q ::: Nil)) Nil Nil
-> Sq Nil (p ::: (q ::: Nil)) (Nil +++ Nil) (Nil +++ Nil)
forall {a} {a} {b} {b} {c} {c} (ps :: Path a a) (qs :: Path b b)
       (rs :: Path c c) (ds :: Path a b) (es :: Path a b) (fs :: Path b c)
       (gs :: Path b c).
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| forall {k} {i} (ps :: Path k i).
IsPath ps =>
Sq (Fold ps ::: Nil) ps Nil Nil
forall (ps :: Path i i).
IsPath ps =>
Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll @(p ::: q ::: Nil)

-- | The counit of an adjunction.
--
-- > K-------K
-- > p---\   |
-- > |   @   |
-- > q---/   |
-- > K-------K
counit :: forall p q. (Proadjunction p q) => Sq (q ::: p ::: Nil) Nil Nil Nil
counit :: forall {j} {i} (p :: j +-> i) (q :: i +-> j).
Proadjunction p q =>
Sq (q ::: (p ::: Nil)) Nil Nil Nil
counit = forall {k} {i} (ps :: Path k i).
IsPath ps =>
Sq ps (Fold ps ::: Nil) Nil Nil
forall (ps :: Path i i).
IsPath ps =>
Sq ps (Fold ps ::: Nil) Nil Nil
hCombineAll @(q ::: p ::: Nil) Sq (q ::: (p ::: Nil)) ((p :.: q) ::: Nil) Nil Nil
-> Sq ((p :.: q) ::: Nil) (Id ::: Nil) Nil Nil
-> Sq (q ::: (p ::: Nil)) (Id ::: Nil) (Nil +++ Nil) (Nil +++ Nil)
forall {a} {a} {b} {b} {c} {c} (ps :: Path a a) (qs :: Path b b)
       (rs :: Path c c) (ds :: Path a b) (es :: Path a b) (fs :: Path b c)
       (gs :: Path b c).
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| ((p :.: q) :~> Id) -> Sq ((p :.: q) ::: Nil) (Id ::: Nil) Nil Nil
forall {k} {i} (p :: k +-> i) (q :: k +-> i).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Sq (p ::: Nil) (q ::: Nil) Nil Nil
hArr (forall {j} {k1} (p :: j +-> k1) (q :: k1 +-> j).
Proadjunction p q =>
(p :.: q) :~> Id
forall (p :: j +-> i) (q :: i +-> j).
Proadjunction p q =>
(p :.: q) :~> Id
counitNat @p @q) Sq (q ::: (p ::: Nil)) (Id ::: Nil) Nil Nil
-> Sq (Id ::: Nil) Nil Nil Nil
-> Sq (q ::: (p ::: Nil)) Nil (Nil +++ Nil) (Nil +++ Nil)
forall {a} {a} {b} {b} {c} {c} (ps :: Path a a) (qs :: Path b b)
       (rs :: Path c c) (ds :: Path a b) (es :: Path a b) (fs :: Path b c)
       (gs :: Path b c).
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| forall {k} {i} (ps :: Path k i).
IsPath ps =>
Sq (Fold ps ::: Nil) ps Nil Nil
forall (ps :: Path i i).
IsPath ps =>
Sq (Fold ps ::: Nil) ps Nil Nil
hSplitAll @Nil

-- | Optics in the @Prof@ equipment.
--
-- > J-------J
-- > s>--@-->a
-- > |   @   |
-- > t<--@--<b
-- > K-------K
type EqpOptic a b s t = (IsOptic a b s t) => Sq (t ::: s ::: Nil) (b ::: a ::: Nil) Nil Nil

type IsOptic a b s t = (Representable s, Corepresentable t, Representable a, Corepresentable b)

mkOptic
  :: (IsOptic a b s t)
  => (forall x r. (Ob x) => (forall y. (Ob y) => (s % x ~> a % y) -> (b %% y ~> t %% x) -> r) -> r)
  -> EqpOptic a b s t
mkOptic :: forall {j1} {i} {k} {j1} (a :: j1 +-> i) (b :: k +-> j1)
       (s :: j1 +-> i) (t :: k +-> j1).
IsOptic a b s t =>
(forall (x :: j1) r.
 Ob x =>
 (forall (y :: j1).
  Ob y =>
  ((s % x) ~> (a % y)) -> ((b %% y) ~> (t %% x)) -> r)
 -> r)
-> EqpOptic a b s t
mkOptic forall (x :: j1) r.
Ob x =>
(forall (y :: j1).
 Ob y =>
 ((s % x) ~> (a % y)) -> ((b %% y) ~> (t %% x)) -> r)
-> r
k = (Fold ((t ::: (s ::: Nil)) +++ Nil)
 :~> Fold (Nil +++ (b ::: (a ::: Nil))))
-> Sq (t ::: (s ::: Nil)) (b ::: (a ::: Nil)) Nil Nil
forall {j} {b} {b} {k} (p :: Path j b) (q :: Path b k)
       (f :: Path b k) (g :: Path j b).
(IsPath p, IsPath q, IsTight f, IsTight g) =>
(Fold (p +++ f) :~> Fold (g +++ q)) -> Sq p q f g
Sq \((:.:) @x s a b
s t b b
t) -> s a b
s s a b -> ((Ob a, Ob b) => (:.:) a b a b) -> (:.:) a b a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall (x :: j1) r.
Ob x =>
(forall (y :: j1).
 Ob y =>
 ((s % x) ~> (a % y)) -> ((b %% y) ~> (t %% x)) -> r)
-> r
k @x \ @y (s % b) ~> (a % y)
get (b %% y) ~> (t %% b)
put -> forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j1 +-> i) (b :: j1) (a :: i).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @_ @y ((s % b) ~> (a % y)
get ((s % b) ~> (a % y)) -> (a ~> (s % b)) -> a ~> (a % y)
forall (b :: i) (c :: i) (a :: i). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s a b -> a ~> (s % b)
forall (a :: i) (b :: j1). s a b -> a ~> (s % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index s a b
s) a a y -> b y b -> (:.:) a b a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((b %% y) ~> b) -> b y b
forall (a :: j1) (b :: k). Ob a => ((b %% a) ~> b) -> b a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (t b b -> (t %% b) ~> b
forall (a :: j1) (b :: k). t a b -> (t %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex 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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (b %% y) ~> (t %% b)
put)

-- | Sequential composition of optics, with 2 holes.
seq
  :: forall a b s t a' b' u v
   . (Proadjunction u t, IsOptic a b s t, IsOptic a' b' u v)
  => EqpOptic a b s t -> EqpOptic a' b' u v -> Sq (v ::: s ::: Nil) (b' ::: a' ::: b ::: a ::: Nil) Nil Nil
seq :: forall {j} {i} {j} {j} {j} {k} (a :: j +-> i) (b :: j +-> j)
       (s :: j +-> i) (t :: j +-> j) (a' :: j +-> j) (b' :: k +-> j)
       (u :: j +-> j) (v :: k +-> j).
(Proadjunction u t, IsOptic a b s t, IsOptic a' b' u v) =>
EqpOptic a b s t
-> EqpOptic a' b' u v
-> Sq
     (v ::: (s ::: Nil)) (b' ::: (a' ::: (b ::: (a ::: Nil)))) Nil Nil
seq EqpOptic a b s t
st EqpOptic a' b' u v
uv = (forall {k} {i} (p :: k +-> i).
Profunctor p =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
forall (p :: j +-> i).
Profunctor p =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId @s Sq (s ::: Nil) (s ::: Nil) Nil Nil
-> Sq Nil (u ::: (t ::: Nil)) Nil Nil
-> Sq
     (Nil +++ (s ::: Nil)) ((u ::: (t ::: Nil)) +++ (s ::: Nil)) Nil Nil
forall {b} {h} {b} {i} {j} {k} (rs :: Path b h) (ss :: Path b i)
       (es :: Path h i) (fs :: Path b b) (ps :: Path j b) (qs :: Path k b)
       (gs :: Path j k).
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== forall {i} {j} (p :: i +-> j) (q :: j +-> i).
Proadjunction p q =>
Sq Nil (p ::: (q ::: Nil)) Nil Nil
forall (p :: j +-> j) (q :: j +-> j).
Proadjunction p q =>
Sq Nil (p ::: (q ::: Nil)) Nil Nil
unit @u @t Sq (s ::: Nil) (u ::: (t ::: (s ::: Nil))) Nil Nil
-> Sq (v ::: Nil) (v ::: Nil) Nil Nil
-> Sq
     ((v ::: Nil) +++ (s ::: Nil))
     ((v ::: Nil) +++ (u ::: (t ::: (s ::: Nil))))
     Nil
     Nil
forall {b} {h} {b} {i} {j} {k} (rs :: Path b h) (ss :: Path b i)
       (es :: Path h i) (fs :: Path b b) (ps :: Path j b) (qs :: Path k b)
       (gs :: Path j k).
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== forall {k} {i} (p :: k +-> i).
Profunctor p =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
forall (p :: k +-> j).
Profunctor p =>
Sq (p ::: Nil) (p ::: Nil) Nil Nil
hId @v) Sq (v ::: (s ::: Nil)) (v ::: (u ::: (t ::: (s ::: Nil)))) Nil Nil
-> Sq
     (v ::: (u ::: (t ::: (s ::: Nil))))
     (b' ::: (a' ::: (b ::: (a ::: Nil))))
     Nil
     Nil
-> Sq
     (v ::: (s ::: Nil))
     (b' ::: (a' ::: (b ::: (a ::: Nil))))
     (Nil +++ Nil)
     (Nil +++ Nil)
forall {a} {a} {b} {b} {c} {c} (ps :: Path a a) (qs :: Path b b)
       (rs :: Path c c) (ds :: Path a b) (es :: Path a b) (fs :: Path b c)
       (gs :: Path b c).
Sq ps qs ds es
-> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs)
||| (Sq (t ::: (s ::: Nil)) (b ::: (a ::: Nil)) Nil Nil
EqpOptic a b s t
st Sq (t ::: (s ::: Nil)) (b ::: (a ::: Nil)) Nil Nil
-> Sq (v ::: (u ::: Nil)) (b' ::: (a' ::: Nil)) Nil Nil
-> Sq
     ((v ::: (u ::: Nil)) +++ (t ::: (s ::: Nil)))
     ((b' ::: (a' ::: Nil)) +++ (b ::: (a ::: Nil)))
     Nil
     Nil
forall {b} {h} {b} {i} {j} {k} (rs :: Path b h) (ss :: Path b i)
       (es :: Path h i) (fs :: Path b b) (ps :: Path j b) (qs :: Path k b)
       (gs :: Path j k).
Sq rs ss es fs
-> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs
=== Sq (v ::: (u ::: Nil)) (b' ::: (a' ::: Nil)) Nil Nil
EqpOptic a' b' u v
uv)

data family Action :: (m, k) +-> k -> k -> m +-> k
instance (MonoidalAction act, Ob a) => FunctorForRep (Action act a :: m +-> k) where
  type Action act a @ x = Act act x a
  fmap :: forall (a :: m) (b :: m).
(a ~> b) -> (Action act a @ a) ~> (Action act a @ b)
fmap a ~> b
f = forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @act a ~> b
f (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

type ActionOptic act a b s t =
  EqpOptic (Rep (Action act a)) (Corep (Action act b)) (Rep (Action act s)) (Corep (Action act t))

fromOptic :: (MonoidalAction act, Ob a, Ob b, Ob s, Ob t) => ExOptic (ActFl act) a b s t -> ActionOptic act a b s t
fromOptic :: forall {j} {k} (act :: (j, k) +-> k) (a :: k) (b :: k) (s :: k)
       (t :: k).
(MonoidalAction act, Ob a, Ob b, Ob s, Ob t) =>
ExOptic (ActFl act) a b s t -> ActionOptic act a b s t
fromOptic @act @a @b @s @t (ExOptic (p s a
l :: p s a) (q b t
r :: q b t)) = (forall (x :: j) r.
 Ob x =>
 (forall (y :: j).
  Ob y =>
  ((Rep (Action act s) % x) ~> (Rep (Action act a) % y))
  -> ((Corep (Action act b) %% y) ~> (Corep (Action act t) %% x))
  -> r)
 -> r)
-> EqpOptic
     (Rep (Action act a))
     (Corep (Action act b))
     (Rep (Action act s))
     (Corep (Action act t))
forall {j1} {i} {k} {j1} (a :: j1 +-> i) (b :: k +-> j1)
       (s :: j1 +-> i) (t :: k +-> j1).
IsOptic a b s t =>
(forall (x :: j1) r.
 Ob x =>
 (forall (y :: j1).
  Ob y =>
  ((s % x) ~> (a % y)) -> ((b %% y) ~> (t %% x)) -> r)
 -> r)
-> EqpOptic a b s t
mkOptic \ @x forall (y :: j).
Ob y =>
((Rep (Action act s) % x) ~> (Rep (Action act a) % y))
-> ((Corep (Action act b) %% y) ~> (Corep (Action act t) %% x))
-> r
k ->
  forall {m} {k} (act :: (m, k) +-> k) (p :: k +-> k) (q :: k +-> k)
       (s :: k) (a :: k) (b :: k) (t :: k) r.
ActFl act p q =>
p s a
-> q b t
-> (forall (x :: m).
    Ob x =>
    (s ~> Act act x a) -> (Act act x b ~> t) -> r)
-> r
forall (act :: (j, k) +-> k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k) r.
ActFl act p q =>
p s a
-> q b t
-> (forall (x :: j).
    Ob x =>
    (s ~> Act act x a) -> (Act act x b ~> t) -> r)
-> r
withActP @act @p @q p s a
l q b t
r \ @z s ~> Act act x a
f Act act x b ~> t
g ->
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @z ((Ob (x ** x) => r) -> r) -> (Ob (x ** x) => r) -> r
forall a b. (a -> b) -> a -> b
$
      forall (y :: j).
Ob y =>
((Rep (Action act s) % x) ~> (Rep (Action act a) % y))
-> ((Corep (Action act b) %% y) ~> (Corep (Action act t) %% x))
-> r
k @(x ** z)
        (forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
forall (t :: (j, k) +-> k) (a :: j) (b :: j) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
multiplicatorInv @act @x @z @a (Act act x (Act act x a) ~> Act act (x ** x) a)
-> ((act % '(x, s)) ~> Act act x (Act act x a))
-> (act % '(x, s)) ~> Act act (x ** x) a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (j, k) +-> k) (a :: j) (b :: j) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @act (forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) s ~> Act act x a
f)
        (forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (j, k) +-> k) (a :: j) (b :: j) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @act (forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) Act act x b ~> t
g ((act % '(x, Act act x b)) ~> (act % '(x, t)))
-> ((act % '(x ** x, b)) ~> (act % '(x, Act act x b)))
-> (act % '(x ** x, b)) ~> (act % '(x, t))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
forall (t :: (j, k) +-> k) (a :: j) (b :: j) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
multiplicator @act @x @z @b)

toOptic
  :: forall h x (s :: x +-> h) (t :: h +-> x) (a :: x +-> h) (b :: h +-> x)
   . (CategoryOf h, CategoryOf x, Representable s, Corepresentable t, Representable a, Corepresentable b)
  => EqpOptic a b s t
  -> ExOptic (ActFl (Rep Precomp)) a (CorepStar b) s (CorepStar t)
toOptic :: forall h x (s :: x +-> h) (t :: h +-> x) (a :: x +-> h)
       (b :: h +-> x).
(CategoryOf h, CategoryOf x, Representable s, Corepresentable t,
 Representable a, Corepresentable b) =>
EqpOptic a b s t
-> ExOptic (ActFl (Rep Precomp)) a (CorepStar b) s (CorepStar t)
toOptic (Sq Fold ((t ::: (s ::: Nil)) +++ Nil)
:~> Fold (Nil +++ (b ::: (a ::: Nil)))
pl) =
  Rep (ActionAt (Rep Precomp) (R (E (b :.: CorepStar t)))) s a
-> Corep
     (ActionAt (Rep Precomp) (R (E (b :.: CorepStar t))))
     (CorepStar b)
     (CorepStar t)
-> ExOptic (ActFl (Rep Precomp)) a (CorepStar b) s (CorepStar t)
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> ExOptic w a b s t
ExOptic
    (forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall (b :: x +-> h) (f :: (x +-> h) +-> (x +-> h))
       (a :: x +-> h).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @a @(ActionAt (Rep Precomp) (R (E (b :.: CorepStar t)))) ((s :~> (a :.: (b :.: CorepStar t)))
-> Prof s (a :.: (b :.: CorepStar t))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
P.Prof s a b -> (:.:) a (b :.: CorepStar t) a b
s :~> (a :.: (b :.: CorepStar t))
get))
    (forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
forall (a :: x +-> h) (f :: (x +-> h) +-> (x +-> h))
       (b :: x +-> h).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep @(CorepStar b) @(ActionAt (Rep Precomp) (R (E (b :.: CorepStar t)))) (((CorepStar b :.: (b :.: CorepStar t)) :~> CorepStar t)
-> Prof (CorepStar b :.: (b :.: CorepStar t)) (CorepStar t)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
P.Prof (:.:) (CorepStar b) (b :.: CorepStar t) a b -> CorepStar t a b
(CorepStar b :.: (b :.: CorepStar t)) :~> CorepStar t
put))
  where
    get :: s :~> a :.: (b :.: CorepStar t)
    get :: s :~> (a :.: (b :.: CorepStar t))
get s a b
s = s a b
s s a b
-> ((Ob a, Ob b) => (:.:) a (b :.: CorepStar t) a b)
-> (:.:) a (b :.: CorepStar t) a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: x +-> h) (q :: h +-> x) (a :: x).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
Adj.unit @(CorepStar t) @t of t b b
t :.: CorepStar t b b
t' -> case Fold ((t ::: (s ::: Nil)) +++ Nil) a b
-> Fold (Nil +++ (b ::: (a ::: Nil))) a b
Fold ((t ::: (s ::: Nil)) +++ Nil)
:~> Fold (Nil +++ (b ::: (a ::: Nil)))
pl (s a b
s s a b -> t b b -> (:.:) s t a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: t b b
t) of a a b
a :.: b b b
b -> a a b
a a a b
-> (:.:) b (CorepStar t) b b -> (:.:) a (b :.: CorepStar t) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (b b b
b b b b -> CorepStar t b b -> (:.:) b (CorepStar t) b b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: CorepStar t b b
t')

    put :: CorepStar b :.: (b :.: CorepStar t) :~> CorepStar t
    put :: (CorepStar b :.: (b :.: CorepStar t)) :~> CorepStar t
put (CorepStar b a b
b' :.: (b b b
b :.: CorepStar t b b
t')) = (a ~> b) -> CorepStar t b b -> CorepStar t a b
forall (c :: h) (a :: h) (b :: x).
(c ~> a) -> CorepStar t a b -> CorepStar t c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
forall (p :: x +-> h) (q :: h +-> x).
Proadjunction p q =>
(p :.: q) :~> (~>)
Adj.counit @(CorepStar b) @b (CorepStar b a b
b' CorepStar b a b -> b b b -> (:.:) (CorepStar b) b a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: b b b
b)) CorepStar t b b
t'