{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Loose bicategory of 'Circuit.Body.Body' values with varying carriers.
--
-- A KSW loose 1-cell is a body @arr (t ch a) (t ch b)@ with its carrier @ch@
-- hidden.  The 2-cells are carrier intertwiners: maps @α : ch -> ch'@ that make
-- the Mealy square commute.  'Body' is the fibre at fixed carrier; 'Circ' is
-- the coproduct of those fibres, and 'Sq' / 'Intertwiner' move between them.
--
-- == Carrier-tensoring composition
--
-- @cascade@ composes two bodies whose carriers are tensored:
--
-- @
--   f :: Body t ch  arr a b
--   g :: Body t ch' arr b c
--   cascade g f :: Circ t arr a c   -- carrier  t ch ch'
-- @
--
-- The composite is
--
-- @
--   assoc .> slide .> strength f .> slide .> strength g .> assoc'
-- @
--
-- using 'Circuit.Channel.assoc', 'assoc'', 'slide' and 'strength'.  No
-- braiding/'Action' is needed because 'slide' already swaps the second carrier
-- past the payload.
--
-- == Law witnesses
--
-- The bicategory laws hold only up to invertible 'Sq' witnesses: carriers
-- @ch ⊗ (ch' ⊗ ch'')@ and @(ch ⊗ ch') ⊗ ch''@ are different Haskell types, so
-- on-the-nose associativity is impossible.  The proof artifact is the
-- intertwiner itself; the falsification artifact is observational, via the
-- pointed specialisation 'Circuit.Body.cascadeSome' and 'Circuit.Body.runSomeBody'.
module Circuit.Circ
  ( -- * Loose 1-cell (carrier hidden)
    Circ (..),
    idCirc,

    -- * Indexed 2-cell (carrier map + commuting square)
    Sq (..),
    idSq,
    vcomp,

    -- * Existential closure of Sq
    Intertwiner (..),
    withIntertwiner,

    -- * The two paths whose equality is the square
    downThenAcross,
    acrossThenDown,

    -- * Carrier-tensoring composition
    cascade,

    -- * Structural proof witnesses (unitors and associator)
    unitorLeft,
    unitorRight,
    unitorLeftSq,
    unitorRightSq,
    associator,
    associatorSq,

    -- * Feedback (closed loop over a carrier component)
    feedback,

    -- * Elgot dagger (feedback over 'Either' as iteration)
    elgotBody,
    elgotDagger,
    elgotFeedbackBody,

    -- * Bisimulation (behavioural quotient of bodies)
    bisimilarStates,
    isBisimulation,
    maxBisimulation,

    -- * Horizontal 2-cell algebra
    rightWhisker,
    leftWhisker,
    hcompose,
    whiskerSq,
  )
where

import Circuit.Body (Body (..), SomeBody (..), cascadeBody)
import Circuit.Category (Category (..), (.>))
import Circuit.Channel (Channel (..), Strength (..))
import Circuit.Tensor (Tensor (..), Unit, Unital (..))
import Data.Void (Void, absurd)
import Prelude hiding (id, (.))

-- $setup
-- >>> :set -XTypeApplications
-- >>> import Circuit.Circ
-- >>> import Circuit.Body (Body (..))

-- | Loose 1-cell: a body with its carrier type hidden.
data Circ t arr a b where
  Circ :: Body t ch arr a b -> Circ t arr a b

-- | Identity loose 1-cell at the tensor unit carrier.
--
-- The carrier is pinned to 'Unit' so that the unit law can be witnessed with
-- the unitor; without the annotation GHC would instantiate the hidden carrier
-- to 'Any'.
idCirc :: forall t arr a. (Strength t arr) => Circ t arr a a
idCirc :: forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> *) (a :: k2).
Strength t arr =>
Circ t arr a a
idCirc = Body t (Unit t) arr a a -> Circ t arr a a
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
Body t ch arr a b -> Circ t arr a b
Circ (arr (t (Unit t) a) (t (Unit t) a) -> Body t (Unit t) arr a a
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body arr (t (Unit t) a) (t (Unit t) a)
forall (a :: k2). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id :: Body t (Unit t) arr a a)

-- | Square (indexed 2-cell).  The carrier maps compose; the middle body must
-- match (a caller side condition).
data Sq t arr ch ch' a b = Sq
  { -- | Map between carriers.
    forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap :: arr ch ch',
    -- | Source body, over the source carrier.
    forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch arr a b
sqSrc :: Body t ch arr a b,
    -- | Target body, over the target carrier.
    forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch' arr a b
sqTgt :: Body t ch' arr a b
  }

-- | Identity square on a body.
idSq :: (Category arr) => Body t ch arr a b -> Sq t arr ch ch a b
idSq :: forall {k2} {k1} (arr :: k2 -> k2 -> *) (t :: k2 -> k1 -> k2)
       (ch :: k2) (a :: k1) (b :: k1).
Category arr =>
Body t ch arr a b -> Sq t arr ch ch a b
idSq Body t ch arr a b
b = arr ch ch
-> Body t ch arr a b -> Body t ch arr a b -> Sq t arr ch ch a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
arr ch ch'
-> Body t ch arr a b -> Body t ch' arr a b -> Sq t arr ch ch' a b
Sq arr ch ch
forall (a :: k2). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id Body t ch arr a b
b Body t ch arr a b
b

-- | Vertical composition of squares.
--
-- The middle body must match; this is a caller side condition.
vcomp ::
  (Category arr) =>
  Sq t arr ch' ch'' a b ->
  Sq t arr ch ch' a b ->
  Sq t arr ch ch'' a b
vcomp :: forall {k2} {k1} (arr :: k2 -> k2 -> *) (t :: k2 -> k1 -> k2)
       (ch' :: k2) (ch'' :: k2) (a :: k1) (b :: k1) (ch :: k2).
Category arr =>
Sq t arr ch' ch'' a b
-> Sq t arr ch ch' a b -> Sq t arr ch ch'' a b
vcomp Sq t arr ch' ch'' a b
g Sq t arr ch ch' a b
f = arr ch ch''
-> Body t ch arr a b -> Body t ch'' arr a b -> Sq t arr ch ch'' a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
arr ch ch'
-> Body t ch arr a b -> Body t ch' arr a b -> Sq t arr ch ch' a b
Sq (Sq t arr ch ch' a b -> arr ch ch'
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap Sq t arr ch ch' a b
f arr ch ch' -> arr ch' ch'' -> arr ch ch''
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> Sq t arr ch' ch'' a b -> arr ch' ch''
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap Sq t arr ch' ch'' a b
g) (Sq t arr ch ch' a b -> Body t ch arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch arr a b
sqSrc Sq t arr ch ch' a b
f) (Sq t arr ch' ch'' a b -> Body t ch'' arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch' arr a b
sqTgt Sq t arr ch' ch'' a b
g)

-- | Existential closure of 'Sq', for stating "there exists a 2-cell".
data Intertwiner t arr a b where
  Intertwiner :: Sq t arr ch ch' a b -> Intertwiner t arr a b

-- | Eliminator for the existential carrier types of an 'Intertwiner'.
withIntertwiner ::
  Intertwiner t arr a b ->
  (forall ch ch'. Sq t arr ch ch' a b -> r) ->
  r
withIntertwiner :: forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (a :: k1) (b :: k1) r.
Intertwiner t arr a b
-> (forall (ch :: k2) (ch' :: k2). Sq t arr ch ch' a b -> r) -> r
withIntertwiner (Intertwiner Sq t arr ch ch' a b
sq) forall (ch :: k2) (ch' :: k2). Sq t arr ch ch' a b -> r
k = Sq t arr ch ch' a b -> r
forall (ch :: k2) (ch' :: k2). Sq t arr ch ch' a b -> r
k Sq t arr ch ch' a b
sq

-- | Go down (carrier map) then across (target body).
--
-- A nondegenerate intertwiner witness: counter state quotiented by parity.
-- The payload is 'Char' so the carrier slot and payload slot are type-distinct;
-- slot confusion is a type error.  These examples exercise both parities and
-- both reset branches.  A paired perturbation doctest on 'acrossThenDown'
-- shows the equality can fail, so these agreement cases are not vacuous.
--
-- >>> let counter = (Body $ \(n, r) -> let n' = if r then 0 else n + 1 in (n', if odd n' then 'x' else 'y')) :: Body (,) Int (->) Bool Char
-- >>> let parity = (Body $ \(b, r) -> let b' = not r && not b in (b', if b' then 'x' else 'y')) :: Body (,) Bool (->) Bool Char
-- >>> let sq = Sq odd counter parity :: Sq (,) (->) Int Bool Bool Char
-- >>> downThenAcross sq (4, False)
-- (True,'x')
-- >>> downThenAcross sq (4, True)
-- (False,'y')
-- >>> downThenAcross sq (5, False)
-- (False,'y')
downThenAcross ::
  (Tensor t arr) =>
  Sq t arr ch ch' a b ->
  arr (t ch a) (t ch' b)
downThenAcross :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *) (ch :: k1)
       (ch' :: k1) (a :: k1) (b :: k1).
Tensor t arr =>
Sq t arr ch ch' a b -> arr (t ch a) (t ch' b)
downThenAcross Sq t arr ch ch' a b
sq = arr ch ch' -> arr a a -> arr (t ch a) (t ch' a)
forall (a :: k1) (b :: k1) (c :: k1) (d :: k1).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor (Sq t arr ch ch' a b -> arr ch ch'
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap Sq t arr ch ch' a b
sq) arr a a
forall (a :: k1). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id arr (t ch a) (t ch' a)
-> arr (t ch' a) (t ch' b) -> arr (t ch a) (t ch' b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> Body t ch' arr a b -> arr (t ch' a) (t ch' b)
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3) (ch :: k1)
       (arr :: k3 -> k3 -> *) (a :: k2) (b :: k2).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism (Sq t arr ch ch' a b -> Body t ch' arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch' arr a b
sqTgt Sq t arr ch ch' a b
sq)

-- | Go across (source body) then down (carrier map).
--
-- Agreement cases for the same witness:
--
-- >>> let counter = (Body $ \(n, r) -> let n' = if r then 0 else n + 1 in (n', if odd n' then 'x' else 'y')) :: Body (,) Int (->) Bool Char
-- >>> let parity = (Body $ \(b, r) -> let b' = not r && not b in (b', if b' then 'x' else 'y')) :: Body (,) Bool (->) Bool Char
-- >>> let sq = Sq odd counter parity :: Sq (,) (->) Int Bool Bool Char
-- >>> acrossThenDown sq (4, False)
-- (True,'x')
-- >>> acrossThenDown sq (4, True)
-- (False,'y')
-- >>> acrossThenDown sq (5, False)
-- (False,'y')
--
-- Perturbation: observe even-ness instead of odd-ness.  The two paths now
-- disagree, which proves the agreement cases above are not vacuous.
--
-- >>> let badCounter = (Body $ \(n, r) -> let n' = if r then 0 else n + 1 in (n', if even n' then 'x' else 'y')) :: Body (,) Int (->) Bool Char
-- >>> let bad = Sq odd badCounter parity :: Sq (,) (->) Int Bool Bool Char
-- >>> downThenAcross bad (4, False)
-- (True,'x')
-- >>> acrossThenDown bad (4, False)
-- (True,'y')
acrossThenDown ::
  (Tensor t arr) =>
  Sq t arr ch ch' a b ->
  arr (t ch a) (t ch' b)
acrossThenDown :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *) (ch :: k1)
       (ch' :: k1) (a :: k1) (b :: k1).
Tensor t arr =>
Sq t arr ch ch' a b -> arr (t ch a) (t ch' b)
acrossThenDown Sq t arr ch ch' a b
sq = Body t ch arr a b -> arr (t ch a) (t ch b)
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3) (ch :: k1)
       (arr :: k3 -> k3 -> *) (a :: k2) (b :: k2).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism (Sq t arr ch ch' a b -> Body t ch arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch arr a b
sqSrc Sq t arr ch ch' a b
sq) arr (t ch a) (t ch b)
-> arr (t ch b) (t ch' b) -> arr (t ch a) (t ch' b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr ch ch' -> arr b b -> arr (t ch b) (t ch' b)
forall (a :: k1) (b :: k1) (c :: k1) (d :: k1).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor (Sq t arr ch ch' a b -> arr ch ch'
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap Sq t arr ch ch' a b
sq) arr b b
forall (a :: k1). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id

-- | Carrier-tensoring composition of loose 1-cells.
--
-- The composite has carrier @t ch ch'@ when the first body has carrier @ch@
-- and the second has carrier @ch'@.
cascade ::
  (Strength t arr) =>
  Circ t arr b c ->
  Circ t arr a b ->
  Circ t arr a c
cascade :: forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> *) (b :: k2)
       (c :: k2) (a :: k2).
Strength t arr =>
Circ t arr b c -> Circ t arr a b -> Circ t arr a c
cascade (Circ Body t ch arr b c
g) (Circ Body t ch arr a b
f) =
  Body t (t ch ch) arr a c -> Circ t arr a c
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
Body t ch arr a b -> Circ t arr a b
Circ (Body t (t ch ch) arr a c -> Circ t arr a c)
-> Body t (t ch ch) arr a c -> Circ t arr a c
forall a b. (a -> b) -> a -> b
$
    arr (t (t ch ch) a) (t (t ch ch) c) -> Body t (t ch ch) arr a c
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body
      ( arr (t (t ch ch) a) (t ch (t ch a))
forall (a :: k2) (b :: k2) (c :: k2).
arr (t (t a b) c) (t a (t b c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc
          arr (t (t ch ch) a) (t ch (t ch a))
-> arr (t ch (t ch a)) (t ch (t ch a))
-> arr (t (t ch ch) a) (t ch (t ch a))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch (t ch a)) (t ch (t ch a))
forall (a :: k2) (b :: k2) (c :: k2).
arr (t a (t b c)) (t b (t a c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t b (t a c))
slide
          arr (t (t ch ch) a) (t ch (t ch a))
-> arr (t ch (t ch a)) (t ch (t ch b))
-> arr (t (t ch ch) a) (t ch (t ch b))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch a) (t ch b) -> arr (t ch (t ch a)) (t ch (t ch b))
forall (b :: k2) (c :: k2) (a :: k2).
arr b c -> arr (t a b) (t a c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (b :: k)
       (c :: k) (a :: k).
Strength t arr =>
arr b c -> arr (t a b) (t a c)
strength (Body t ch arr a b -> arr (t ch a) (t ch b)
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3) (ch :: k1)
       (arr :: k3 -> k3 -> *) (a :: k2) (b :: k2).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism Body t ch arr a b
f)
          arr (t (t ch ch) a) (t ch (t ch b))
-> arr (t ch (t ch b)) (t ch (t ch b))
-> arr (t (t ch ch) a) (t ch (t ch b))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch (t ch b)) (t ch (t ch b))
forall (a :: k2) (b :: k2) (c :: k2).
arr (t a (t b c)) (t b (t a c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t b (t a c))
slide
          arr (t (t ch ch) a) (t ch (t ch b))
-> arr (t ch (t ch b)) (t ch (t ch c))
-> arr (t (t ch ch) a) (t ch (t ch c))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch b) (t ch c) -> arr (t ch (t ch b)) (t ch (t ch c))
forall (b :: k2) (c :: k2) (a :: k2).
arr b c -> arr (t a b) (t a c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (b :: k)
       (c :: k) (a :: k).
Strength t arr =>
arr b c -> arr (t a b) (t a c)
strength (Body t ch arr b c -> arr (t ch b) (t ch c)
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3) (ch :: k1)
       (arr :: k3 -> k3 -> *) (a :: k2) (b :: k2).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism Body t ch arr b c
g)
          arr (t (t ch ch) a) (t ch (t ch c))
-> arr (t ch (t ch c)) (t (t ch ch) c)
-> arr (t (t ch ch) a) (t (t ch ch) c)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch (t ch c)) (t (t ch ch) c)
forall (a :: k2) (b :: k2) (c :: k2).
arr (t a (t b c)) (t (t a b) c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc'
      )

-- | Indexed left unitor square.
unitorLeftSq ::
  (Unital t arr, Strength t arr) =>
  Body t ch arr a b ->
  Sq t arr (t (Unit t) ch) ch a b
unitorLeftSq :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch :: k)
       (a :: k) (b :: k).
(Unital t arr, Strength t arr) =>
Body t ch arr a b -> Sq t arr (t (Unit t) ch) ch a b
unitorLeftSq Body t ch arr a b
b = arr (t (Unit t) ch) ch
-> Body t (t (Unit t) ch) arr a b
-> Body t ch arr a b
-> Sq t arr (t (Unit t) ch) ch a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
arr ch ch'
-> Body t ch arr a b -> Body t ch' arr a b -> Sq t arr ch ch' a b
Sq arr (t (Unit t) ch) ch
forall (a :: k). arr (t (Unit t) a) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t (Unit t) a) a
unitl (Body t ch arr a b
-> Body t (Unit t) arr a a -> Body t (t (Unit t) ch) arr a b
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody Body t ch arr a b
b (arr (t (Unit t) a) (t (Unit t) a) -> Body t (Unit t) arr a a
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body arr (t (Unit t) a) (t (Unit t) a)
forall (a :: k). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id)) Body t ch arr a b
b

-- | Left unitor witness: composing a body with the identity at the unit carrier
-- is isomorphic to the original body.
unitorLeft ::
  (Unital t arr, Strength t arr) =>
  Body t ch arr a b ->
  Intertwiner t arr a b
unitorLeft :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *) (ch :: k1)
       (a :: k1) (b :: k1).
(Unital t arr, Strength t arr) =>
Body t ch arr a b -> Intertwiner t arr a b
unitorLeft Body t ch arr a b
b = Sq t arr (t (Unit t) ch) ch a b -> Intertwiner t arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Intertwiner t arr a b
Intertwiner (Body t ch arr a b -> Sq t arr (t (Unit t) ch) ch a b
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch :: k)
       (a :: k) (b :: k).
(Unital t arr, Strength t arr) =>
Body t ch arr a b -> Sq t arr (t (Unit t) ch) ch a b
unitorLeftSq Body t ch arr a b
b)

-- | Indexed right unitor square.
unitorRightSq ::
  (Unital t arr, Strength t arr) =>
  Body t ch arr a b ->
  Sq t arr (t ch (Unit t)) ch a b
unitorRightSq :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch :: k)
       (a :: k) (b :: k).
(Unital t arr, Strength t arr) =>
Body t ch arr a b -> Sq t arr (t ch (Unit t)) ch a b
unitorRightSq Body t ch arr a b
b = arr (t ch (Unit t)) ch
-> Body t (t ch (Unit t)) arr a b
-> Body t ch arr a b
-> Sq t arr (t ch (Unit t)) ch a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
arr ch ch'
-> Body t ch arr a b -> Body t ch' arr a b -> Sq t arr ch ch' a b
Sq arr (t ch (Unit t)) ch
forall (a :: k). arr (t a (Unit t)) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t a (Unit t)) a
unitr (Body t (Unit t) arr b b
-> Body t ch arr a b -> Body t (t ch (Unit t)) arr a b
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody (arr (t (Unit t) b) (t (Unit t) b) -> Body t (Unit t) arr b b
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body arr (t (Unit t) b) (t (Unit t) b)
forall (a :: k). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id) Body t ch arr a b
b) Body t ch arr a b
b

-- | Right unitor witness.
unitorRight ::
  (Unital t arr, Strength t arr) =>
  Body t ch arr a b ->
  Intertwiner t arr a b
unitorRight :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *) (ch :: k1)
       (a :: k1) (b :: k1).
(Unital t arr, Strength t arr) =>
Body t ch arr a b -> Intertwiner t arr a b
unitorRight Body t ch arr a b
b = Sq t arr (t ch (Unit t)) ch a b -> Intertwiner t arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Intertwiner t arr a b
Intertwiner (Body t ch arr a b -> Sq t arr (t ch (Unit t)) ch a b
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch :: k)
       (a :: k) (b :: k).
(Unital t arr, Strength t arr) =>
Body t ch arr a b -> Sq t arr (t ch (Unit t)) ch a b
unitorRightSq Body t ch arr a b
b)

-- | Indexed associator square.
associatorSq ::
  (Strength t arr) =>
  Body t ch3 arr c d ->
  Body t ch2 arr b c ->
  Body t ch1 arr a b ->
  Sq t arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3)) a d
associatorSq :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *)
       (ch3 :: k1) (c :: k1) (d :: k1) (ch2 :: k1) (b :: k1) (ch1 :: k1)
       (a :: k1).
Strength t arr =>
Body t ch3 arr c d
-> Body t ch2 arr b c
-> Body t ch1 arr a b
-> Sq t arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3)) a d
associatorSq Body t ch3 arr c d
h Body t ch2 arr b c
g Body t ch1 arr a b
f =
  arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3))
-> Body t (t (t ch1 ch2) ch3) arr a d
-> Body t (t ch1 (t ch2 ch3)) arr a d
-> Sq t arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3)) a d
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
arr ch ch'
-> Body t ch arr a b -> Body t ch' arr a b -> Sq t arr ch ch' a b
Sq
    arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3))
forall (a :: k1) (b :: k1) (c :: k1).
arr (t (t a b) c) (t a (t b c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc
    (Body t ch3 arr c d
-> Body t (t ch1 ch2) arr a c -> Body t (t (t ch1 ch2) ch3) arr a d
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody Body t ch3 arr c d
h (Body t ch2 arr b c
-> Body t ch1 arr a b -> Body t (t ch1 ch2) arr a c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody Body t ch2 arr b c
g Body t ch1 arr a b
f))
    (Body t (t ch2 ch3) arr b d
-> Body t ch1 arr a b -> Body t (t ch1 (t ch2 ch3)) arr a d
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody (Body t ch3 arr c d
-> Body t ch2 arr b c -> Body t (t ch2 ch3) arr b d
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody Body t ch3 arr c d
h Body t ch2 arr b c
g) Body t ch1 arr a b
f)

-- | Associator witness: carrier bracketing of three composed bodies is
-- isomorphic up to the associator of the tensor.
associator ::
  (Strength t arr) =>
  Body t ch3 arr c d ->
  Body t ch2 arr b c ->
  Body t ch1 arr a b ->
  Intertwiner t arr a d
associator :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *)
       (ch3 :: k1) (c :: k1) (d :: k1) (ch2 :: k1) (b :: k1) (ch1 :: k1)
       (a :: k1).
Strength t arr =>
Body t ch3 arr c d
-> Body t ch2 arr b c
-> Body t ch1 arr a b
-> Intertwiner t arr a d
associator Body t ch3 arr c d
h Body t ch2 arr b c
g Body t ch1 arr a b
f = Sq t arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3)) a d
-> Intertwiner t arr a d
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Intertwiner t arr a b
Intertwiner (Body t ch3 arr c d
-> Body t ch2 arr b c
-> Body t ch1 arr a b
-> Sq t arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3)) a d
forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *)
       (ch3 :: k1) (c :: k1) (d :: k1) (ch2 :: k1) (b :: k1) (ch1 :: k1)
       (a :: k1).
Strength t arr =>
Body t ch3 arr c d
-> Body t ch2 arr b c
-> Body t ch1 arr a b
-> Sq t arr (t (t ch1 ch2) ch3) (t ch1 (t ch2 ch3)) a d
associatorSq Body t ch3 arr c d
h Body t ch2 arr b c
g Body t ch1 arr a b
f)

-- | Right whisker: tensor a square with an identity-on-boundaries 1-cell on
-- the right.
rightWhisker ::
  (Tensor t arr, Strength t arr) =>
  Sq t arr ch ch' a b ->
  Body t d arr b c ->
  Sq t arr (t ch d) (t ch' d) a c
rightWhisker :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *) (ch :: k1)
       (ch' :: k1) (a :: k1) (b :: k1) (d :: k1) (c :: k1).
(Tensor t arr, Strength t arr) =>
Sq t arr ch ch' a b
-> Body t d arr b c -> Sq t arr (t ch d) (t ch' d) a c
rightWhisker Sq t arr ch ch' a b
sq Body t d arr b c
r =
  arr (t ch d) (t ch' d)
-> Body t (t ch d) arr a c
-> Body t (t ch' d) arr a c
-> Sq t arr (t ch d) (t ch' d) a c
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
arr ch ch'
-> Body t ch arr a b -> Body t ch' arr a b -> Sq t arr ch ch' a b
Sq
    (arr ch ch' -> arr d d -> arr (t ch d) (t ch' d)
forall (a :: k1) (b :: k1) (c :: k1) (d :: k1).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor (Sq t arr ch ch' a b -> arr ch ch'
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap Sq t arr ch ch' a b
sq) arr d d
forall (a :: k1). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id)
    (Body t d arr b c -> Body t ch arr a b -> Body t (t ch d) arr a c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody Body t d arr b c
r (Sq t arr ch ch' a b -> Body t ch arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch arr a b
sqSrc Sq t arr ch ch' a b
sq))
    (Body t d arr b c -> Body t ch' arr a b -> Body t (t ch' d) arr a c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody Body t d arr b c
r (Sq t arr ch ch' a b -> Body t ch' arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch' arr a b
sqTgt Sq t arr ch ch' a b
sq))

-- | Left whisker: tensor an identity-on-boundaries 1-cell on the left of a
-- square.
leftWhisker ::
  (Tensor t arr, Strength t arr) =>
  Body t d arr a' a ->
  Sq t arr ch ch' a b ->
  Sq t arr (t d ch) (t d ch') a' b
leftWhisker :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *) (d :: k1)
       (a' :: k1) (a :: k1) (ch :: k1) (ch' :: k1) (b :: k1).
(Tensor t arr, Strength t arr) =>
Body t d arr a' a
-> Sq t arr ch ch' a b -> Sq t arr (t d ch) (t d ch') a' b
leftWhisker Body t d arr a' a
l Sq t arr ch ch' a b
sq =
  arr (t d ch) (t d ch')
-> Body t (t d ch) arr a' b
-> Body t (t d ch') arr a' b
-> Sq t arr (t d ch) (t d ch') a' b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
arr ch ch'
-> Body t ch arr a b -> Body t ch' arr a b -> Sq t arr ch ch' a b
Sq
    (arr d d -> arr ch ch' -> arr (t d ch) (t d ch')
forall (a :: k1) (b :: k1) (c :: k1) (d :: k1).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor arr d d
forall (a :: k1). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (Sq t arr ch ch' a b -> arr ch ch'
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap Sq t arr ch ch' a b
sq))
    (Body t ch arr a b -> Body t d arr a' a -> Body t (t d ch) arr a' b
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody (Sq t arr ch ch' a b -> Body t ch arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch arr a b
sqSrc Sq t arr ch ch' a b
sq) Body t d arr a' a
l)
    (Body t ch' arr a b
-> Body t d arr a' a -> Body t (t d ch') arr a' b
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody (Sq t arr ch ch' a b -> Body t ch' arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch' arr a b
sqTgt Sq t arr ch ch' a b
sq) Body t d arr a' a
l)

-- | Horizontal composition of two squares.
hcompose ::
  (Tensor t arr, Strength t arr) =>
  Sq t arr ch2 ch2' b c ->
  Sq t arr ch1 ch1' a b ->
  Sq t arr (t ch1 ch2) (t ch1' ch2') a c
hcompose :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *)
       (ch2 :: k1) (ch2' :: k1) (b :: k1) (c :: k1) (ch1 :: k1)
       (ch1' :: k1) (a :: k1).
(Tensor t arr, Strength t arr) =>
Sq t arr ch2 ch2' b c
-> Sq t arr ch1 ch1' a b -> Sq t arr (t ch1 ch2) (t ch1' ch2') a c
hcompose Sq t arr ch2 ch2' b c
sq2 Sq t arr ch1 ch1' a b
sq1 =
  arr (t ch1 ch2) (t ch1' ch2')
-> Body t (t ch1 ch2) arr a c
-> Body t (t ch1' ch2') arr a c
-> Sq t arr (t ch1 ch2) (t ch1' ch2') a c
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
arr ch ch'
-> Body t ch arr a b -> Body t ch' arr a b -> Sq t arr ch ch' a b
Sq
    (arr ch1 ch1' -> arr ch2 ch2' -> arr (t ch1 ch2) (t ch1' ch2')
forall (a :: k1) (b :: k1) (c :: k1) (d :: k1).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor (Sq t arr ch1 ch1' a b -> arr ch1 ch1'
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap Sq t arr ch1 ch1' a b
sq1) (Sq t arr ch2 ch2' b c -> arr ch2 ch2'
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap Sq t arr ch2 ch2' b c
sq2))
    (Body t ch2 arr b c
-> Body t ch1 arr a b -> Body t (t ch1 ch2) arr a c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody (Sq t arr ch2 ch2' b c -> Body t ch2 arr b c
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch arr a b
sqSrc Sq t arr ch2 ch2' b c
sq2) (Sq t arr ch1 ch1' a b -> Body t ch1 arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch arr a b
sqSrc Sq t arr ch1 ch1' a b
sq1))
    (Body t ch2' arr b c
-> Body t ch1' arr a b -> Body t (t ch1' ch2') arr a c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch' :: k)
       (b :: k) (c :: k) (ch :: k) (a :: k).
Strength t arr =>
Body t ch' arr b c
-> Body t ch arr a b -> Body t (t ch ch') arr a c
cascadeBody (Sq t arr ch2 ch2' b c -> Body t ch2' arr b c
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch' arr a b
sqTgt Sq t arr ch2 ch2' b c
sq2) (Sq t arr ch1 ch1' a b -> Body t ch1' arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch' arr a b
sqTgt Sq t arr ch1 ch1' a b
sq1))

-- | Boundary whisker: apply tight maps to the input and output boundaries of a
-- square.  This is the `Sq` side of the interchange law; the `Poles` side is
-- `iomap` on the Moore-split representation.
whiskerSq ::
  (Tensor t arr) =>
  arr a' a ->
  arr b b' ->
  Sq t arr ch ch' a b ->
  Sq t arr ch ch' a' b'
whiskerSq :: forall {k1} (t :: k1 -> k1 -> k1) (arr :: k1 -> k1 -> *) (a' :: k1)
       (a :: k1) (b :: k1) (b' :: k1) (ch :: k1) (ch' :: k1).
Tensor t arr =>
arr a' a
-> arr b b' -> Sq t arr ch ch' a b -> Sq t arr ch ch' a' b'
whiskerSq arr a' a
f arr b b'
g Sq t arr ch ch' a b
sq =
  arr ch ch'
-> Body t ch arr a' b'
-> Body t ch' arr a' b'
-> Sq t arr ch ch' a' b'
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
arr ch ch'
-> Body t ch arr a b -> Body t ch' arr a b -> Sq t arr ch ch' a b
Sq
    (Sq t arr ch ch' a b -> arr ch ch'
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> arr ch ch'
carrierMap Sq t arr ch ch' a b
sq)
    (arr (t ch a') (t ch b') -> Body t ch arr a' b'
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (arr (t ch a') (t ch b') -> Body t ch arr a' b')
-> arr (t ch a') (t ch b') -> Body t ch arr a' b'
forall a b. (a -> b) -> a -> b
$ arr ch ch -> arr a' a -> arr (t ch a') (t ch a)
forall (a :: k1) (b :: k1) (c :: k1) (d :: k1).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor arr ch ch
forall (a :: k1). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id arr a' a
f arr (t ch a') (t ch a)
-> arr (t ch a) (t ch b) -> arr (t ch a') (t ch b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> Body t ch arr a b -> arr (t ch a) (t ch b)
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3) (ch :: k1)
       (arr :: k3 -> k3 -> *) (a :: k2) (b :: k2).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism (Sq t arr ch ch' a b -> Body t ch arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch arr a b
sqSrc Sq t arr ch ch' a b
sq) arr (t ch a') (t ch b)
-> arr (t ch b) (t ch b') -> arr (t ch a') (t ch b')
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr ch ch -> arr b b' -> arr (t ch b) (t ch b')
forall (a :: k1) (b :: k1) (c :: k1) (d :: k1).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor arr ch ch
forall (a :: k1). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id arr b b'
g)
    (arr (t ch' a') (t ch' b') -> Body t ch' arr a' b'
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (arr (t ch' a') (t ch' b') -> Body t ch' arr a' b')
-> arr (t ch' a') (t ch' b') -> Body t ch' arr a' b'
forall a b. (a -> b) -> a -> b
$ arr ch' ch' -> arr a' a -> arr (t ch' a') (t ch' a)
forall (a :: k1) (b :: k1) (c :: k1) (d :: k1).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor arr ch' ch'
forall (a :: k1). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id arr a' a
f arr (t ch' a') (t ch' a)
-> arr (t ch' a) (t ch' b) -> arr (t ch' a') (t ch' b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> Body t ch' arr a b -> arr (t ch' a) (t ch' b)
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3) (ch :: k1)
       (arr :: k3 -> k3 -> *) (a :: k2) (b :: k2).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism (Sq t arr ch ch' a b -> Body t ch' arr a b
forall {k2} {k1} (t :: k2 -> k1 -> k2) (arr :: k2 -> k2 -> *)
       (ch :: k2) (ch' :: k2) (a :: k1) (b :: k1).
Sq t arr ch ch' a b -> Body t ch' arr a b
sqTgt Sq t arr ch ch' a b
sq) arr (t ch' a') (t ch' b)
-> arr (t ch' b) (t ch' b') -> arr (t ch' a') (t ch' b')
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr ch' ch' -> arr b b' -> arr (t ch' b) (t ch' b')
forall (a :: k1) (b :: k1) (c :: k1) (d :: k1).
arr a b -> arr c d -> arr (t a c) (t b d)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k) (d :: k).
Tensor t arr =>
arr a b -> arr c d -> arr (t a c) (t b d)
tensor arr ch' ch'
forall (a :: k1). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id arr b b'
g)

-- | Close a feedback loop over a component @s@ of the input/output object.
--
-- The 1-cell must be of the form @Circ t arr (t s a) (t s b)@: the feedback
-- value @s@ appears as the first component of the tensor in both domain and
-- codomain.  The result moves @s@ into the hidden carrier, turning it into
-- state.  This is the guarded / state-bootstrapping feedback of KSW, not the
-- immediate fixed-point trace: yanking fails here, which is the expected
-- behaviour for a feedback category.
--
-- Implemented by reassociating so that @s@ becomes part of the carrier:
--
-- @
--   feedback (Circ (Body f)) = Circ (Body (assoc .> f .> assoc'))
-- @
feedback ::
  (Channel t arr) =>
  Circ t arr (t s a) (t s b) ->
  Circ t arr a b
feedback :: forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> *) (s :: k2)
       (a :: k2) (b :: k2).
Channel t arr =>
Circ t arr (t s a) (t s b) -> Circ t arr a b
feedback (Circ (Body arr (t ch (t s a)) (t ch (t s b))
f)) = Body t (t ch s) arr a b -> Circ t arr a b
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
Body t ch arr a b -> Circ t arr a b
Circ (Body t (t ch s) arr a b -> Circ t arr a b)
-> Body t (t ch s) arr a b -> Circ t arr a b
forall a b. (a -> b) -> a -> b
$ arr (t (t ch s) a) (t (t ch s) b) -> Body t (t ch s) arr a b
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body (arr (t (t ch s) a) (t (t ch s) b) -> Body t (t ch s) arr a b)
-> arr (t (t ch s) a) (t (t ch s) b) -> Body t (t ch s) arr a b
forall a b. (a -> b) -> a -> b
$ arr (t (t ch s) a) (t ch (t s a))
forall (a :: k2) (b :: k2) (c :: k2).
arr (t (t a b) c) (t a (t b c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc arr (t (t ch s) a) (t ch (t s a))
-> arr (t ch (t s a)) (t ch (t s b))
-> arr (t (t ch s) a) (t ch (t s b))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch (t s a)) (t ch (t s b))
f arr (t (t ch s) a) (t ch (t s b))
-> arr (t ch (t s b)) (t (t ch s) b)
-> arr (t (t ch s) a) (t (t ch s) b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch (t s b)) (t (t ch s) b)
forall (a :: k2) (b :: k2) (c :: k2).
arr (t a (t b c)) (t (t a b) c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc'

-- * Elgot dagger

-- | Build the Elgot coalgebra @[Left, f]@ from a loop body @f :: a -> Either a b@.
--
-- The resulting body has the 'Void' unit carrier and payload
-- @Either a a -> Either a b@, so it can be passed to 'feedback'.  The dagger
-- of @f@ is then a morphism @a -> b@ in 'Circ'.
elgotBody :: (a -> Either a b) -> Body Either Void (->) (Either a a) (Either a b)
elgotBody :: forall a b.
(a -> Either a b)
-> Body Either Void (->) (Either a a) (Either a b)
elgotBody a -> Either a b
f =
  (Either Void (Either a a) -> Either Void (Either a b))
-> Body Either Void (->) (Either a a) (Either a b)
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body ((Either Void (Either a a) -> Either Void (Either a b))
 -> Body Either Void (->) (Either a a) (Either a b))
-> (Either Void (Either a a) -> Either Void (Either a b))
-> Body Either Void (->) (Either a a) (Either a b)
forall a b. (a -> b) -> a -> b
$ \case
    Right (Left a
s) -> Either a b -> Either Void (Either a b)
forall {a} {b} {a}. Either a b -> Either a (Either a b)
wrap (a -> Either a b
f a
s)
    Right (Right a
a) -> Either a b -> Either Void (Either a b)
forall {a} {b} {a}. Either a b -> Either a (Either a b)
wrap (a -> Either a b
f a
a)
    Left Void
v -> Void -> Either Void (Either a b)
forall a. Void -> a
absurd Void
v
  where
    wrap :: Either a b -> Either a (Either a b)
wrap (Left a
s) = Either a b -> Either a (Either a b)
forall a b. b -> Either a b
Right (a -> Either a b
forall a b. a -> Either a b
Left a
s)
    wrap (Right b
b) = Either a b -> Either a (Either a b)
forall a b. b -> Either a b
Right (b -> Either a b
forall a b. b -> Either a b
Right b
b)

-- | The feedback body of the Elgot dagger of @f :: a -> Either a b@.
--
-- Exposed so that callers can run it directly with a seed of type
-- @Either Void a@, which is the hidden carrier produced by 'feedback'.
elgotFeedbackBody :: (a -> Either a b) -> Body Either (Either Void a) (->) a b
elgotFeedbackBody :: forall a b.
(a -> Either a b) -> Body Either (Either Void a) (->) a b
elgotFeedbackBody a -> Either a b
f = (Either (Either Void a) a -> Either (Either Void a) b)
-> Body Either (Either Void a) (->) a b
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
arr (t ch a) (t ch b) -> Body t ch arr a b
Body ((Either (Either Void a) a -> Either (Either Void a) b)
 -> Body Either (Either Void a) (->) a b)
-> (Either (Either Void a) a -> Either (Either Void a) b)
-> Body Either (Either Void a) (->) a b
forall a b. (a -> b) -> a -> b
$ Either (Either Void a) a -> Either Void (Either a a)
forall a b c. Either (Either a b) c -> Either a (Either b c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc (Either (Either Void a) a -> Either Void (Either a a))
-> (Either Void (Either a a) -> Either Void (Either a b))
-> Either (Either Void a) a
-> Either Void (Either a b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> Body Either Void (->) (Either a a) (Either a b)
-> Either Void (Either a a) -> Either Void (Either a b)
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3) (ch :: k1)
       (arr :: k3 -> k3 -> *) (a :: k2) (b :: k2).
Body t ch arr a b -> arr (t ch a) (t ch b)
morphism ((a -> Either a b)
-> Body Either Void (->) (Either a a) (Either a b)
forall a b.
(a -> Either a b)
-> Body Either Void (->) (Either a a) (Either a b)
elgotBody a -> Either a b
f) (Either (Either Void a) a -> Either Void (Either a b))
-> (Either Void (Either a b) -> Either (Either Void a) b)
-> Either (Either Void a) a -> Either (Either Void a) b
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> Either Void (Either a b) -> Either (Either Void a) b
forall a b c. Either a (Either b c) -> Either (Either a b) c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc'

-- | Elgot dagger of @f :: a -> Either a b@ via 'feedback'.
elgotDagger :: (a -> Either a b) -> Circ Either (->) a b
elgotDagger :: forall a b. (a -> Either a b) -> Circ Either (->) a b
elgotDagger a -> Either a b
f = Body Either (Either Void a) (->) a b -> Circ Either (->) a b
forall {k} {k1} {k2} (t :: k -> k1 -> k2) (ch :: k)
       (arr :: k2 -> k2 -> *) (a :: k1) (b :: k1).
Body t ch arr a b -> Circ t arr a b
Circ ((a -> Either a b) -> Body Either (Either Void a) (->) a b
forall a b.
(a -> Either a b) -> Body Either (Either Void a) (->) a b
elgotFeedbackBody a -> Either a b
f)

-- * Bisimulation

-- | Step a @(,) / (->)@ body: given a state and an input, return the next
-- state and output.
stepBody :: Body (,) s (->) a b -> s -> a -> (s, b)
stepBody :: forall s a b. Body (,) s (->) a b -> s -> a -> (s, b)
stepBody (Body (s, a) -> (s, b)
f) s
s a
a = (s, a) -> (s, b)
f (s
s, a
a)

-- | Check whether a relation is a bisimulation between two finite-state bodies.
--
-- The relation must be over the provided state spaces; the check is exact over
-- the bounded input alphabet.  A relation @R@ is a bisimulation when for every
-- @(s1, s2) ∈ R@ and every input @a@, the outputs coincide and the successor
-- states are again @R@-related.
isBisimulation ::
  (Eq s1, Eq s2, Eq b) =>
  [a] ->
  Body (,) s1 (->) a b ->
  Body (,) s2 (->) a b ->
  [(s1, s2)] ->
  Bool
isBisimulation :: forall s1 s2 b a.
(Eq s1, Eq s2, Eq b) =>
[a]
-> Body (,) s1 (->) a b
-> Body (,) s2 (->) a b
-> [(s1, s2)]
-> Bool
isBisimulation [a]
inputs Body (,) s1 (->) a b
body1 Body (,) s2 (->) a b
body2 [(s1, s2)]
rel =
  ((s1, s2) -> Bool) -> [(s1, s2)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
    ( \(s1
s1, s2
s2) ->
        (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
          ( \a
a ->
              let (s1
s1', b
b1) = Body (,) s1 (->) a b -> s1 -> a -> (s1, b)
forall s a b. Body (,) s (->) a b -> s -> a -> (s, b)
stepBody Body (,) s1 (->) a b
body1 s1
s1 a
a
                  (s2
s2', b
b2) = Body (,) s2 (->) a b -> s2 -> a -> (s2, b)
forall s a b. Body (,) s (->) a b -> s -> a -> (s, b)
stepBody Body (,) s2 (->) a b
body2 s2
s2 a
a
               in b
b1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b2 Bool -> Bool -> Bool
&& (s1
s1', s2
s2') (s1, s2) -> [(s1, s2)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(s1, s2)]
rel
          )
          [a]
inputs
    )
    [(s1, s2)]
rel

-- | Compute the maximal bisimulation between two finite-state bodies over a
-- bounded input alphabet.  The state spaces are supplied explicitly because a
-- 'Body' is a function and does not enumerate its own states.
maxBisimulation ::
  (Eq s1, Eq s2, Eq b) =>
  [a] ->
  [s1] ->
  [s2] ->
  Body (,) s1 (->) a b ->
  Body (,) s2 (->) a b ->
  [(s1, s2)]
maxBisimulation :: forall s1 s2 b a.
(Eq s1, Eq s2, Eq b) =>
[a]
-> [s1]
-> [s2]
-> Body (,) s1 (->) a b
-> Body (,) s2 (->) a b
-> [(s1, s2)]
maxBisimulation [a]
inputs [s1]
states1 [s2]
states2 Body (,) s1 (->) a b
body1 Body (,) s2 (->) a b
body2 = [(s1, s2)] -> [(s1, s2)]
go [(s1, s2)]
initRel
  where
    initRel :: [(s1, s2)]
initRel = [(s1
s1, s2
s2) | s1
s1 <- [s1]
states1, s2
s2 <- [s2]
states2]
    go :: [(s1, s2)] -> [(s1, s2)]
go [(s1, s2)]
rel =
      let rel' :: [(s1, s2)]
rel' =
            ((s1, s2) -> Bool) -> [(s1, s2)] -> [(s1, s2)]
forall a. (a -> Bool) -> [a] -> [a]
filter
              ( \(s1
s1, s2
s2) ->
                  (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
                    ( \a
a ->
                        let (s1
s1', b
b1) = Body (,) s1 (->) a b -> s1 -> a -> (s1, b)
forall s a b. Body (,) s (->) a b -> s -> a -> (s, b)
stepBody Body (,) s1 (->) a b
body1 s1
s1 a
a
                            (s2
s2', b
b2) = Body (,) s2 (->) a b -> s2 -> a -> (s2, b)
forall s a b. Body (,) s (->) a b -> s -> a -> (s, b)
stepBody Body (,) s2 (->) a b
body2 s2
s2 a
a
                         in b
b1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b2 Bool -> Bool -> Bool
&& (s1
s1', s2
s2') (s1, s2) -> [(s1, s2)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(s1, s2)]
rel
                    )
                    [a]
inputs
              )
              [(s1, s2)]
rel
       in if [(s1, s2)]
rel' [(s1, s2)] -> [(s1, s2)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(s1, s2)]
rel then [(s1, s2)]
rel else [(s1, s2)] -> [(s1, s2)]
go [(s1, s2)]
rel'

-- | Check whether two specific states are bisimilar.
bisimilarStates ::
  (Eq s1, Eq s2, Eq b) =>
  [a] ->
  [s1] ->
  [s2] ->
  Body (,) s1 (->) a b ->
  Body (,) s2 (->) a b ->
  s1 ->
  s2 ->
  Bool
bisimilarStates :: forall s1 s2 b a.
(Eq s1, Eq s2, Eq b) =>
[a]
-> [s1]
-> [s2]
-> Body (,) s1 (->) a b
-> Body (,) s2 (->) a b
-> s1
-> s2
-> Bool
bisimilarStates [a]
inputs [s1]
states1 [s2]
states2 Body (,) s1 (->) a b
body1 Body (,) s2 (->) a b
body2 s1
s1 s2
s2 =
  (s1
s1, s2
s2) (s1, s2) -> [(s1, s2)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
-> [s1]
-> [s2]
-> Body (,) s1 (->) a b
-> Body (,) s2 (->) a b
-> [(s1, s2)]
forall s1 s2 b a.
(Eq s1, Eq s2, Eq b) =>
[a]
-> [s1]
-> [s2]
-> Body (,) s1 (->) a b
-> Body (,) s2 (->) a b
-> [(s1, s2)]
maxBisimulation [a]
inputs [s1]
states1 [s2]
states2 Body (,) s1 (->) a b
body1 Body (,) s2 (->) a b
body2

-- | 'Category' instance for 'Circ'.
--
-- The laws hold only up to invertible 'Sq': on-the-nose associativity and
-- unitality are impossible as Haskell values because the carriers of the two
-- sides differ.  Observational witnesses live in "Axioma.Circ".
instance (Strength t arr) => Category (Circ t arr) where
  id :: forall a. Circ t arr a a
  id :: forall (a :: k). Circ t arr a a
id = Circ t arr a a
forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> *) (a :: k2).
Strength t arr =>
Circ t arr a a
idCirc
  {-# INLINE id #-}

  (.) :: forall a b c. Circ t arr b c -> Circ t arr a b -> Circ t arr a c
  . :: forall (a :: k) (b :: k) (c :: k).
Circ t arr b c -> Circ t arr a b -> Circ t arr a c
(.) = Circ t arr b c -> Circ t arr a b -> Circ t arr a c
forall {k2} (t :: k2 -> k2 -> k2) (arr :: k2 -> k2 -> *) (b :: k2)
       (c :: k2) (a :: k2).
Strength t arr =>
Circ t arr b c -> Circ t arr a b -> Circ t arr a c
cascade
  {-# INLINE (.) #-}