{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | The Chu construction over a monoidal base category.
--
-- A Chu object is a polarity pair @A⁺@ and @A⁻@ together with a pairing
-- @A⁺ ⊗ A⁻ → ⊥@ into a dualising object.  A Chu morphism is an adjoint pair
-- satisfying the equation
--
-- > e_B (f⁺ a, d) = e_A (a, f⁻ d)
--
-- This is the only genuinely star-autonomous, non-compact structure in the
-- library: proper ⊗ vs ⅋, proper additives, a real negation, and an internal
-- hom that is not just @A⊥ ⊗ B@.  Promoting it to a base arrow makes the
-- linear-logic distinctions measurable for the first time.
module Circuit.Chu
  ( -- * Dualising semiring
    ChuSemiring (..),

    -- * Chu objects and morphisms
    ChuObj (..),
    PointedChuObj (..),
    ChuMorphism (..),
    Chu (..),
    ChuPosType,
    ChuNegType,
    negateChu,
    idChu,
    composeChu,

    -- * Adjoint law
    chuLaw,
    chuLawAt,

    -- * Delivery pairing
    deliversToSemiring,
    deliveryMatrix,

    -- * Tensor and par over Set
    ChuTensorNeg (..),
    ChuParPos (..),
    tensorChuObj,
    parChuObj,
    lolliChuObj,
    withChuObj,
    oplusChuObj,
    topChuObj,
    zeroChuObj,
    proj1Chu,
    proj2Chu,
    inj1Chu,
    inj2Chu,
    unitTopChu,
    unitZeroChu,
    pairChu,
    copairChu,
    withTopLChu,
    withTopLInvChu,
    withTopRChu,
    withTopRInvChu,
    zeroPlusLChu,
    zeroPlusLInvChu,
    zeroPlusRChu,
    zeroPlusRInvChu,
    evalChu,
    tensorChu,
    parChu,
    chuUnitObj,
    chuBottomObj,
    chuTensorNegs,
    chuParPoss,
    chuSeparated,
    chuExtensional,
    leftUnitorChu,
    leftUnitorChuInv,
    rightUnitorChu,
    rightUnitorChuInv,
    assocChu,
    assocChuInv,
    slideChu,

    -- * Embedding from 'Circuit.Poles'
    polesAsChu,
    lawfulDimap,

    -- * Object-indexed Chu category (SepChu / OChu)
    ChuObject (..),
    ChuSeparated,
    ChuExtensional,
    ChuPosNonEmpty,
    ChuNegNonEmpty,
    OChu (..),
    SepChu,

    -- * OChu constrained combinators (evidence at use sites)
    parOChu,
    unitlOChu,
    unitlOChu',
    unitrOChu,
    unitrOChu',
    swapOChu,
    parPOChu,
    unitlPOChu,
    unitlPOChu',
    unitrPOChu,
    unitrPOChu',
    evalOChu,
    curryOChu,
    uncurryOChu,
    discardEOChu,
    derelictOChu,
    introduceOChu,
    mergeEOChu,
    zeroEOChu,
    copyTOChu,
    discardTOChu,
    plusTOChu,
    zeroTOChu,
    ChuOUnit (..),
    ChuOTensor (..),
    ChuONeg (..),
    ChuOWith (..),
    ChuOPlus (..),
    ChuOPar (..),
    ChuOTop (..),
    ChuOZero (..),
    ChuTwo (..),
    ChuThree (..),
    ChuDouble01 (..),
    ChuDelivery (..),
    ChuAny (..),
    swapChu,
    dnUnitChu,
    dnCounitChu,
    ChuOLolli (..),
    curryChu,
    uncurryChu,
    chuFunctionals,
    bangChuObj,
    whyNotChuObj,
    copyBangChu,
    discardBangChu,
    mergeBangChu,
    zeroBangChu,
    derelictChu,
    zeroWhyNotChu,
    introduceChu,
    digChu,
    promoteChu,
    mergeWhyNotParChu,
    zeroWhyNotParChu,
    leftUnitorParChu,
    leftUnitorParChuInv,
    rightUnitorParChu,
    rightUnitorParChuInv,
    assocParChu,
    assocParChuInv,
    swapParChu,
    ChuOBang (..),
    ChuOWhyNot (..),
  )
where

import Circuit.Bimonoid (CopyT (..), DiscardT (..), MergeT (..), ZeroT (..))
import Circuit.Category (Category (..))
import Circuit.Channel (Channel (..))
import Circuit.Linear (BangCopy (..), BangWeaken (..), Exponential (..), Lolli (..), WhyNotIntro (..), WhyNotMonoid (..))
import Circuit.Par (Bot, Par (..))
import Circuit.Poles (In (..), Out (..), Poles (..), close, companion, conjoint)
import Circuit.Tensor (Action (..), Tensor (..), Unit)
import Data.Kind (Type)
import Data.Monoid (Any (..))
import Data.Proxy (Proxy (..))
import Data.Traversable (sequenceA)
import Data.Type.Bool (If)
import Data.Void (Void, absurd)
import Prelude hiding (curry, id, uncurry, (.))
import Prelude qualified as Pre

-- ---------------------------------------------------------------------------
-- Minimal semiring
-- ---------------------------------------------------------------------------

-- | A semiring, kept local to this module so the delivery instance does not
-- pull in an external numeric prelude.
class ChuSemiring r where
  sZero :: r
  sOne :: r
  sPlus :: r -> r -> r
  sTimes :: r -> r -> r

instance ChuSemiring Bool where
  sZero :: Bool
sZero = Bool
False
  sOne :: Bool
sOne = Bool
True
  sPlus :: Bool -> Bool -> Bool
sPlus = Bool -> Bool -> Bool
(||)
  sTimes :: Bool -> Bool -> Bool
sTimes = Bool -> Bool -> Bool
(&&)

instance ChuSemiring Double where
  sZero :: Double
sZero = Double
0
  sOne :: Double
sOne = Double
1
  sPlus :: Double -> Double -> Double
sPlus = Double -> Double -> Double
forall a. Num a => a -> a -> a
(+)
  sTimes :: Double -> Double -> Double
sTimes = Double -> Double -> Double
forall a. Num a => a -> a -> a
(*)

instance ChuSemiring Integer where
  sZero :: Integer
sZero = Integer
0
  sOne :: Integer
sOne = Integer
1
  sPlus :: Integer -> Integer -> Integer
sPlus = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)
  sTimes :: Integer -> Integer -> Integer
sTimes = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)

-- ---------------------------------------------------------------------------
-- Chu objects
-- ---------------------------------------------------------------------------

-- | An object of @Chu(C, ⊥)@.
--
-- * @a@ is the positive carrier.
-- * @b@ is the negative carrier.
-- * @chuPair@ is the pairing @a ⊗ b → r@ into the dualising object.
newtype ChuObj t r arr a b = ChuObj
  { -- | Pairing into the dualising object.
    forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair :: arr (t a b) r
  }

-- | A pointed Chu object: a 'ChuObj' together with a chosen point pair.
--
-- This is the separate wrapper used by 'polesAsChu' to retain the positive
-- and negative points that witness a self-dual channel.
data PointedChuObj t r arr a b = PointedChuObj
  { -- | Underlying Chu object.
    forall {k} {k} (t :: * -> * -> k) (r :: k) (arr :: k -> k -> *) a
       b.
PointedChuObj t r arr a b -> ChuObj t r arr a b
pointedObj :: ChuObj t r arr a b,
    -- | Positive point.
    forall {k} {k} (t :: * -> * -> k) (r :: k) (arr :: k -> k -> *) a
       b.
PointedChuObj t r arr a b -> a
pointedPos :: a,
    -- | Negative point.
    forall {k} {k} (t :: * -> * -> k) (r :: k) (arr :: k -> k -> *) a
       b.
PointedChuObj t r arr a b -> b
pointedNeg :: b
  }

-- | Negation swaps the carriers via the symmetric braiding.
--
-- Involution is definitional for a symmetric braiding:
-- @braid . braid = id@.
negateChu ::
  (Action t arr) =>
  ChuObj t r arr a b ->
  ChuObj t r arr b a
negateChu :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (r :: k)
       (a :: k) (b :: k).
Action t arr =>
ChuObj t r arr a b -> ChuObj t r arr b a
negateChu (ChuObj arr (t a b) r
e) = arr (t b a) r -> ChuObj t r arr b a
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (arr (t a b) r
e arr (t a b) r -> arr (t b a) (t a b) -> arr (t b a) r
forall (b :: k) (c :: k) (a :: k). arr b c -> arr a b -> arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr (t b a) (t a b)
forall (a :: k) (b :: k). arr (t a b) (t b a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
Action t arr =>
arr (t a b) (t b a)
braid)
{-# INLINE negateChu #-}

-- ---------------------------------------------------------------------------
-- Chu morphisms
-- ---------------------------------------------------------------------------

-- | A Chu morphism @A → B@ is a pair of base arrows:
--
-- * @chuForward :: arr a c@ runs forward from @A⁺@ to @B⁺@.
-- * @chuBackward :: arr d b@ runs backward from @B⁻@ to @A⁻@.
data ChuMorphism t r arr a b c d = ChuMorphism
  { -- | Forward component.
    forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
ChuMorphism t r arr a b c d -> arr a c
chuForward :: arr a c,
    -- | Backward component.
    forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
ChuMorphism t r arr a b c d -> arr d b
chuBackward :: arr d b
  }

-- | Identity Chu morphism.
idChu ::
  (Category arr) =>
  ChuMorphism t r arr a b a b
idChu :: forall {k} {k} {k} (arr :: k -> k -> *) (t :: k) (r :: k) (a :: k)
       (b :: k).
Category arr =>
ChuMorphism t r arr a b a b
idChu = arr a a -> arr b b -> ChuMorphism t r arr a b a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism arr a a
forall (a :: k). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id arr b b
forall (a :: k). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
{-# INLINE idChu #-}

-- | Sequential composition of Chu morphisms.
--
-- Forward components compose covariantly; backward components compose
-- contravariantly.
composeChu ::
  (Category arr) =>
  ChuMorphism t r arr c d e f ->
  ChuMorphism t r arr a b c d ->
  ChuMorphism t r arr a b e f
composeChu :: forall {k} {k} {k} (arr :: k -> k -> *) (t :: k) (r :: k) (c :: k)
       (d :: k) (e :: k) (f :: k) (a :: k) (b :: k).
Category arr =>
ChuMorphism t r arr c d e f
-> ChuMorphism t r arr a b c d -> ChuMorphism t r arr a b e f
composeChu (ChuMorphism arr c e
f2 arr f d
g2) (ChuMorphism arr a c
f1 arr d b
g1) =
  arr a e -> arr f b -> ChuMorphism t r arr a b e f
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (arr c e
f2 arr c e -> arr a c -> arr a e
forall (b :: k) (c :: k) (a :: k). arr b c -> arr a b -> arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr a c
f1) (arr d b
g1 arr d b -> arr f d -> arr f b
forall (b :: k) (c :: k) (a :: k). arr b c -> arr a b -> arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr f d
g2)

-- ---------------------------------------------------------------------------
-- Chu as a base arrow
-- ---------------------------------------------------------------------------

-- | Closed type family giving the positive carrier of a Chu object tag.
--
-- Every object of @Chu(C, ⊥)@ is ultimately a 'ChuObj'; this family exposes
-- the positive carrier so that identity and composition can be typed
-- uniformly without a separate type class.
type family ChuPosType a :: Type where
  ChuPosType (ChuObj t r arr p n) = p
  ChuPosType (ChuOUnit r) = ()
  ChuPosType (ChuOTensor r a b) = (ChuPosType a, ChuPosType b)
  ChuPosType (ChuONeg r a) = ChuNegType a
  ChuPosType ChuTwo = Bool
  ChuPosType ChuThree = Maybe Bool
  ChuPosType ChuDouble01 = Bool
  ChuPosType ChuDelivery = Bool
  ChuPosType ChuAny = Any
  ChuPosType (ChuOLolli r a b) = ChuParPos (ChuNegType a) (ChuPosType a) (ChuPosType b) (ChuNegType b)
  ChuPosType (ChuOWith r a b) = (ChuPosType a, ChuPosType b)
  ChuPosType (ChuOPlus r a b) = Either (ChuPosType a) (ChuPosType b)
  ChuPosType (ChuOPar r a b) = ChuParPos (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
  ChuPosType (ChuOTop r) = ()
  ChuPosType (ChuOZero r) = Void
  ChuPosType (ChuOBang r a) = ChuPosType a
  ChuPosType (ChuOWhyNot r a) = ChuNegType a -> r

-- | Closed type family giving the negative carrier of a Chu object tag.
--
-- See 'ChuPosType' for motivation; this is the dual side.
type family ChuNegType a :: Type where
  ChuNegType (ChuObj t r arr p n) = n
  ChuNegType (ChuOUnit r) = r
  ChuNegType (ChuOTensor r a b) = ChuTensorNeg (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
  ChuNegType (ChuONeg r a) = ChuPosType a
  ChuNegType ChuTwo = Bool
  ChuNegType ChuThree = Maybe Bool
  ChuNegType ChuDouble01 = Bool
  ChuNegType ChuDelivery = Bool
  ChuNegType ChuAny = Any
  ChuNegType (ChuOLolli r a b) = (ChuPosType a, ChuNegType b)
  ChuNegType (ChuOWith r a b) = Either (ChuNegType a) (ChuNegType b)
  ChuNegType (ChuOPlus r a b) = (ChuNegType a, ChuNegType b)
  ChuNegType (ChuOPar r a b) = (ChuNegType a, ChuNegType b)
  ChuNegType (ChuOTop r) = Void
  ChuNegType (ChuOZero r) = ()
  ChuNegType (ChuOBang r a) = ChuPosType a -> r
  ChuNegType (ChuOWhyNot r a) = ChuNegType a

-- | @Chu t r arr@ is the Chu construction as a base arrow.  Objects are
-- 'ChuObj's; morphisms are adjoint pairs wrapped by the 'Chu' constructor.
newtype Chu (t :: Type -> Type -> Type) (r :: Type) (arr :: Type -> Type -> Type) (a :: Type) (b :: Type) where
  Chu ::
    ChuMorphism t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b) ->
    Chu t r arr a b

instance (Category arr) => Category (Chu t r arr) where
  id :: forall a. Chu t r arr a a
  id :: forall a. Chu t r arr a a
id = ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType a) (ChuNegType a)
-> Chu t r arr a a
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType a) (ChuNegType a)
forall {k} {k} {k} (arr :: k -> k -> *) (t :: k) (r :: k) (a :: k)
       (b :: k).
Category arr =>
ChuMorphism t r arr a b a b
idChu :: ChuMorphism t r arr (ChuPosType a) (ChuNegType a) (ChuPosType a) (ChuNegType a))

  (.) ::
    forall a b c.
    Chu t r arr b c ->
    Chu t r arr a b ->
    Chu t r arr a c
  Chu ChuMorphism
  t r arr (ChuPosType b) (ChuNegType b) (ChuPosType c) (ChuNegType c)
g . :: forall a b c. Chu t r arr b c -> Chu t r arr a b -> Chu t r arr a c
. Chu ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
f = ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType c) (ChuNegType c)
-> Chu t r arr a c
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuMorphism
  t r arr (ChuPosType b) (ChuNegType b) (ChuPosType c) (ChuNegType c)
-> ChuMorphism
     t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> ChuMorphism
     t r arr (ChuPosType a) (ChuNegType a) (ChuPosType c) (ChuNegType c)
forall {k} {k} {k} (arr :: k -> k -> *) (t :: k) (r :: k) (c :: k)
       (d :: k) (e :: k) (f :: k) (a :: k) (b :: k).
Category arr =>
ChuMorphism t r arr c d e f
-> ChuMorphism t r arr a b c d -> ChuMorphism t r arr a b e f
composeChu ChuMorphism
  t r arr (ChuPosType b) (ChuNegType b) (ChuPosType c) (ChuNegType c)
g ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
f)

-- | The adjoint law for @arr = (->)@ and the cartesian tensor.
--
-- A pair @(f⁺, f⁻)@ is a Chu morphism exactly when
-- @e_B (f⁺ a, d) = e_A (a, f⁻ d)@ for all @a@ and @d@.
chuLaw ::
  (Eq r) =>
  ChuObj (,) r (->) a b ->
  ChuObj (,) r (->) c d ->
  ChuMorphism (,) r (->) a b c d ->
  a ->
  d ->
  Bool
chuLaw :: forall r a b c d.
Eq r =>
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuMorphism (,) r (->) a b c d
-> a
-> d
-> Bool
chuLaw ChuObj (,) r (->) a b
src ChuObj (,) r (->) c d
tgt (ChuMorphism a -> c
f d -> b
g) a
a d
d =
  ChuObj (,) r (->) c d -> (c, d) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair ChuObj (,) r (->) c d
tgt (a -> c
f a
a, d
d) r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== ChuObj (,) r (->) a b -> (a, b) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair ChuObj (,) r (->) a b
src (a
a, d -> b
g d
d)
{-# INLINE chuLaw #-}

-- | Pointwise adjoint law for @arr = (->)@.
--
-- When the dualising object @r@ does not have an 'Eq' instance (e.g. it is
-- itself a function), supply a probe @k :: r -> s@ with 'Eq' @s@.
chuLawAt ::
  (Eq s) =>
  ChuObj (,) r (->) a b ->
  ChuObj (,) r (->) c d ->
  ChuMorphism (,) r (->) a b c d ->
  a ->
  d ->
  (r -> s) ->
  Bool
chuLawAt :: forall s r a b c d.
Eq s =>
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuMorphism (,) r (->) a b c d
-> a
-> d
-> (r -> s)
-> Bool
chuLawAt ChuObj (,) r (->) a b
src ChuObj (,) r (->) c d
tgt (ChuMorphism a -> c
f d -> b
g) a
a d
d r -> s
k =
  r -> s
k (ChuObj (,) r (->) c d -> (c, d) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair ChuObj (,) r (->) c d
tgt (a -> c
f a
a, d
d)) s -> s -> Bool
forall a. Eq a => a -> a -> Bool
== r -> s
k (ChuObj (,) r (->) a b -> (a, b) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair ChuObj (,) r (->) a b
src (a
a, d -> b
g d
d))
{-# INLINE chuLawAt #-}

-- ---------------------------------------------------------------------------
-- Delivery pairing
-- ---------------------------------------------------------------------------

-- | Named-recipient delivery predicate over an arbitrary semiring.
--
-- A post whose recipient list contains @who@ delivers with 'sOne';
-- an empty list delivers to no one with 'sZero'.
deliversToSemiring ::
  (ChuSemiring r, Eq a) =>
  -- | Recipients on the post.
  [a] ->
  -- | Recipient name.
  a ->
  r
deliversToSemiring :: forall r a. (ChuSemiring r, Eq a) => [a] -> a -> r
deliversToSemiring [a]
recipients a
who
  | [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
recipients = r
forall r. ChuSemiring r => r
sZero
  | a
who a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
recipients = r
forall r. ChuSemiring r => r
sOne
  | Bool
otherwise = r
forall r. ChuSemiring r => r
sZero

-- | Delivery matrix for a fixed list of posts and a roster of agents.
--
-- Rows are posts (in the order given), columns are agents (in the order
-- given), and entry @(p, a)@ is the delivery weight of post @p@ to agent @a@.
deliveryMatrix ::
  (ChuSemiring r, Eq col) =>
  -- | Agents (column labels).
  [col] ->
  -- | Recipient lists for each post (row labels are implicit).
  [[col]] ->
  [[r]]
deliveryMatrix :: forall r col. (ChuSemiring r, Eq col) => [col] -> [[col]] -> [[r]]
deliveryMatrix [col]
agents [[col]]
recipients =
  [(col -> r) -> [col] -> [r]
forall a b. (a -> b) -> [a] -> [b]
map ([col] -> col -> r
forall r a. (ChuSemiring r, Eq a) => [a] -> a -> r
deliversToSemiring [col]
recips) [col]
agents | [col]
recips <- [[col]]
recipients]

-- ===========================================================================
-- Tensor and par structure over Set (arr = (->), t = (,))
-- ===========================================================================
--
-- The Chu construction Chu(Set, K) is *-autonomous on the full subcategory of
-- separated extensional objects.  The operations below are defined for
-- arbitrary Chu objects, but the unit laws hold only when the objects are
-- separated and extensional.  See Barr, "The separated extensional Chu
-- category" (TAC 1998).

-- | Negative part of the Chu tensor @A ⊗ B@.
--
-- A value @(f, g)@ lives here when @e_A(a, g(b)) = e_B(b, f(a))@ for all
-- @a ∈ A⁺@, @b ∈ B⁺@.
data ChuTensorNeg a b c d = ChuTensorNeg
  { -- | @A⁺ -> B⁻@
    forall a b c d. ChuTensorNeg a b c d -> a -> d
ctnForward :: a -> d,
    -- | @B⁺ -> A⁻@
    forall a b c d. ChuTensorNeg a b c d -> c -> b
ctnBackward :: c -> b
  }

-- | Positive part of the Chu par @A ⅋ B@.
--
-- A value @(f, g)@ lives here when @e_A(g(d), a) = e_B(f(a), d)@ for all
-- @a ∈ A⁻@, @d ∈ B⁻@.
data ChuParPos a b c d = ChuParPos
  { -- | @A⁻ -> C⁺@
    forall a b c d. ChuParPos a b c d -> b -> c
cppForward :: b -> c,
    -- | @D⁻ -> A⁺@
    forall a b c d. ChuParPos a b c d -> d -> a
cppBackward :: d -> a
  }

-- | Tensor product of Chu objects over @Set@.
tensorChuObj ::
  (Eq r) =>
  ChuObj (,) r (->) a b ->
  ChuObj (,) r (->) c d ->
  ChuObj (,) r (->) (a, c) (ChuTensorNeg a b c d)
tensorChuObj :: forall r a b c d.
Eq r =>
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuObj (,) r (->) (a, c) (ChuTensorNeg a b c d)
tensorChuObj (ChuObj (a, b) -> r
r) (ChuObj (c, d) -> r
s) =
  (((a, c), ChuTensorNeg a b c d) -> r)
-> ChuObj (,) r (->) (a, c) (ChuTensorNeg a b c d)
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj ((((a, c), ChuTensorNeg a b c d) -> r)
 -> ChuObj (,) r (->) (a, c) (ChuTensorNeg a b c d))
-> (((a, c), ChuTensorNeg a b c d) -> r)
-> ChuObj (,) r (->) (a, c) (ChuTensorNeg a b c d)
forall a b. (a -> b) -> a -> b
$
    \((a
x, c
y), ChuTensorNeg a -> d
f c -> b
g) ->
      let lhs :: r
lhs = (a, b) -> r
r (a
x, c -> b
g c
y)
          rhs :: r
rhs = (c, d) -> r
s (c
y, a -> d
f a
x)
       in if r
lhs r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
rhs then r
lhs else [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"tensorChuObj: ChuTensorNeg violates bilinear law"

-- | Par product of Chu objects over @Set@.
parChuObj ::
  (Eq r) =>
  ChuObj (,) r (->) a b ->
  ChuObj (,) r (->) c d ->
  ChuObj (,) r (->) (ChuParPos a b c d) (b, d)
parChuObj :: forall r a b c d.
Eq r =>
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuObj (,) r (->) (ChuParPos a b c d) (b, d)
parChuObj (ChuObj (a, b) -> r
r) (ChuObj (c, d) -> r
s) =
  ((ChuParPos a b c d, (b, d)) -> r)
-> ChuObj (,) r (->) (ChuParPos a b c d) (b, d)
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (((ChuParPos a b c d, (b, d)) -> r)
 -> ChuObj (,) r (->) (ChuParPos a b c d) (b, d))
-> ((ChuParPos a b c d, (b, d)) -> r)
-> ChuObj (,) r (->) (ChuParPos a b c d) (b, d)
forall a b. (a -> b) -> a -> b
$
    \(ChuParPos b -> c
f d -> a
g, (b
x, d
y)) ->
      let lhs :: r
lhs = (a, b) -> r
r (d -> a
g d
y, b
x)
          rhs :: r
rhs = (c, d) -> r
s (b -> c
f b
x, d
y)
       in if r
lhs r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
rhs then r
lhs else [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"parChuObj: ChuParPos violates bilinear law"

-- | Linear implication @A ⊸ B = A⊥ ⅋ B@ over @Set@.
--
-- The positive carrier is the set of Chu morphisms @A → B@, packaged as
-- 'ChuParPos' after negating @A@.
lolliChuObj ::
  (Eq r) =>
  ChuObj (,) r (->) a b ->
  ChuObj (,) r (->) c d ->
  ChuObj (,) r (->) (ChuParPos b a c d) (a, d)
lolliChuObj :: forall r a b c d.
Eq r =>
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuObj (,) r (->) (ChuParPos b a c d) (a, d)
lolliChuObj ChuObj (,) r (->) a b
a ChuObj (,) r (->) c d
b = ChuObj (,) r (->) b a
-> ChuObj (,) r (->) c d
-> ChuObj (,) r (->) (ChuParPos b a c d) (a, d)
forall r a b c d.
Eq r =>
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuObj (,) r (->) (ChuParPos a b c d) (b, d)
parChuObj (ChuObj (,) r (->) a b -> ChuObj (,) r (->) b a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (r :: k)
       (a :: k) (b :: k).
Action t arr =>
ChuObj t r arr a b -> ChuObj t r arr b a
negateChu ChuObj (,) r (->) a b
a) ChuObj (,) r (->) c d
b

-- | Additive conjunction @A & B@ over @Set@.
--
-- Positive carrier is @A⁺ × B⁺@; negative carrier is the disjoint union
-- @A⁻ + B⁻@.
withChuObj ::
  ChuObj (,) r (->) a b ->
  ChuObj (,) r (->) c d ->
  ChuObj (,) r (->) (a, c) (Either b d)
withChuObj :: forall r a b c d.
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d -> ChuObj (,) r (->) (a, c) (Either b d)
withChuObj (ChuObj (a, b) -> r
eA) (ChuObj (c, d) -> r
eB) =
  (((a, c), Either b d) -> r)
-> ChuObj (,) r (->) (a, c) (Either b d)
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj ((((a, c), Either b d) -> r)
 -> ChuObj (,) r (->) (a, c) (Either b d))
-> (((a, c), Either b d) -> r)
-> ChuObj (,) r (->) (a, c) (Either b d)
forall a b. (a -> b) -> a -> b
$
    \((a
x, c
y), Either b d
q) -> case Either b d
q of
      Left b
b -> (a, b) -> r
eA (a
x, b
b)
      Right d
d -> (c, d) -> r
eB (c
y, d
d)

-- | Additive disjunction @A ⊕ B@ over @Set@.
--
-- Positive carrier is the disjoint union @A⁺ + B⁺@; negative carrier is
-- @A⁻ × B⁻@.
oplusChuObj ::
  ChuObj (,) r (->) a b ->
  ChuObj (,) r (->) c d ->
  ChuObj (,) r (->) (Either a c) (b, d)
oplusChuObj :: forall r a b c d.
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d -> ChuObj (,) r (->) (Either a c) (b, d)
oplusChuObj (ChuObj (a, b) -> r
eA) (ChuObj (c, d) -> r
eB) =
  ((Either a c, (b, d)) -> r)
-> ChuObj (,) r (->) (Either a c) (b, d)
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (((Either a c, (b, d)) -> r)
 -> ChuObj (,) r (->) (Either a c) (b, d))
-> ((Either a c, (b, d)) -> r)
-> ChuObj (,) r (->) (Either a c) (b, d)
forall a b. (a -> b) -> a -> b
$
    \(Either a c
q, (b
x, d
y)) -> case Either a c
q of
      Left a
a -> (a, b) -> r
eA (a
a, b
x)
      Right c
c -> (c, d) -> r
eB (c
c, d
y)

-- | Additive unit @⊤@ over @Set@.
--
-- Positive carrier is the terminal object @1@; negative carrier is the
-- initial object @0@.
topChuObj :: ChuObj (,) r (->) () Void
topChuObj :: forall r. ChuObj (,) r (->) () Void
topChuObj = (((), Void) -> r) -> ChuObj (,) r (->) () Void
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (\((), Void
v) -> Void -> r
forall a. Void -> a
absurd Void
v)

-- | Additive unit @0@ over @Set@.
--
-- Positive carrier is the initial object @0@; negative carrier is the
-- terminal object @1@.
zeroChuObj :: ChuObj (,) r (->) Void ()
zeroChuObj :: forall r. ChuObj (,) r (->) Void ()
zeroChuObj = ((Void, ()) -> r) -> ChuObj (,) r (->) Void ()
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (\(Void
v, ()) -> Void -> r
forall a. Void -> a
absurd Void
v)

-- | First projection @A & B → A@.
proj1Chu ::
  ChuMorphism (,) r (->) (a, c) (Either b d) a b
proj1Chu :: forall {k} (r :: k) a c b d.
ChuMorphism (,) r (->) (a, c) (Either b d) a b
proj1Chu = ((a, c) -> a)
-> (b -> Either b d)
-> ChuMorphism (,) r (->) (a, c) (Either b d) a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (a, c) -> a
forall a b. (a, b) -> a
fst b -> Either b d
forall a b. a -> Either a b
Left
{-# INLINE proj1Chu #-}

-- | Second projection @A & B → B@.
proj2Chu ::
  ChuMorphism (,) r (->) (a, c) (Either b d) c d
proj2Chu :: forall {k} (r :: k) a c b d.
ChuMorphism (,) r (->) (a, c) (Either b d) c d
proj2Chu = ((a, c) -> c)
-> (d -> Either b d)
-> ChuMorphism (,) r (->) (a, c) (Either b d) c d
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (a, c) -> c
forall a b. (a, b) -> b
snd d -> Either b d
forall a b. b -> Either a b
Right
{-# INLINE proj2Chu #-}

-- | Left injection @A → A ⊕ B@.
inj1Chu ::
  ChuMorphism (,) r (->) a b (Either a c) (b, d)
inj1Chu :: forall {k} (r :: k) a b c d.
ChuMorphism (,) r (->) a b (Either a c) (b, d)
inj1Chu = (a -> Either a c)
-> ((b, d) -> b) -> ChuMorphism (,) r (->) a b (Either a c) (b, d)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism a -> Either a c
forall a b. a -> Either a b
Left (b, d) -> b
forall a b. (a, b) -> a
fst
{-# INLINE inj1Chu #-}

-- | Right injection @A → A ⊕ B@.
inj2Chu ::
  ChuMorphism (,) r (->) c d (Either a c) (b, d)
inj2Chu :: forall {k} (r :: k) c d a b.
ChuMorphism (,) r (->) c d (Either a c) (b, d)
inj2Chu = (c -> Either a c)
-> ((b, d) -> d) -> ChuMorphism (,) r (->) c d (Either a c) (b, d)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism c -> Either a c
forall a b. b -> Either a b
Right (b, d) -> d
forall a b. (a, b) -> b
snd
{-# INLINE inj2Chu #-}

-- | Unique morphism @A → ⊤@.
unitTopChu ::
  ChuMorphism (,) r (->) a b () Void
unitTopChu :: forall {k} (r :: k) a b. ChuMorphism (,) r (->) a b () Void
unitTopChu = (a -> ()) -> (Void -> b) -> ChuMorphism (,) r (->) a b () Void
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (() -> a -> ()
forall a b. a -> b -> a
const ()) Void -> b
forall a. Void -> a
absurd
{-# INLINE unitTopChu #-}

-- | Unique morphism @0 → A@.
unitZeroChu ::
  ChuMorphism (,) r (->) Void () a b
unitZeroChu :: forall {k} (r :: k) a b. ChuMorphism (,) r (->) Void () a b
unitZeroChu = (Void -> a) -> (b -> ()) -> ChuMorphism (,) r (->) Void () a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism Void -> a
forall a. Void -> a
absurd (() -> b -> ()
forall a b. a -> b -> a
const ())
{-# INLINE unitZeroChu #-}

-- | Pairing of morphisms into the additive conjunction.
--
-- Universal property of @A & B@: given @f : C → A@ and @g : C → B@, produce
-- @⟨f,g⟩ : C → A & B@.
pairChu ::
  ChuMorphism (,) r (->) c d a b ->
  ChuMorphism (,) r (->) c d e f ->
  ChuMorphism (,) r (->) c d (a, e) (Either b f)
pairChu :: forall {k} (r :: k) c d a b e f.
ChuMorphism (,) r (->) c d a b
-> ChuMorphism (,) r (->) c d e f
-> ChuMorphism (,) r (->) c d (a, e) (Either b f)
pairChu (ChuMorphism c -> a
fPos b -> d
fNeg) (ChuMorphism c -> e
gPos f -> d
gNeg) =
  (c -> (a, e))
-> (Either b f -> d)
-> ChuMorphism (,) r (->) c d (a, e) (Either b f)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\c
c -> (c -> a
fPos c
c, c -> e
gPos c
c)) ((b -> d) -> (f -> d) -> Either b f -> d
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> d
fNeg f -> d
gNeg)
{-# INLINE pairChu #-}

-- | Copairing of morphisms out of the additive disjunction.
--
-- Universal property of @A ⊕ B@: given @f : A → C@ and @g : B → C@, produce
-- @[f,g] : A ⊕ B → C@.
copairChu ::
  ChuMorphism (,) r (->) a b c d ->
  ChuMorphism (,) r (->) e f c d ->
  ChuMorphism (,) r (->) (Either a e) (b, f) c d
copairChu :: forall {k} (r :: k) a b c d e f.
ChuMorphism (,) r (->) a b c d
-> ChuMorphism (,) r (->) e f c d
-> ChuMorphism (,) r (->) (Either a e) (b, f) c d
copairChu (ChuMorphism a -> c
fPos d -> b
fNeg) (ChuMorphism e -> c
gPos d -> f
gNeg) =
  (Either a e -> c)
-> (d -> (b, f)) -> ChuMorphism (,) r (->) (Either a e) (b, f) c d
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism ((a -> c) -> (e -> c) -> Either a e -> c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> c
fPos e -> c
gPos) (\d
d -> (d -> b
fNeg d
d, d -> f
gNeg d
d))
{-# INLINE copairChu #-}

-- | Right unit isomorphism @A → A & ⊤@.
withTopRChu ::
  ChuMorphism (,) r (->) a b (a, ()) (Either b Void)
withTopRChu :: forall {k} (r :: k) a b.
ChuMorphism (,) r (->) a b (a, ()) (Either b Void)
withTopRChu = (a -> (a, ()))
-> (Either b Void -> b)
-> ChuMorphism (,) r (->) a b (a, ()) (Either b Void)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\a
a -> (a
a, ())) ((b -> b) -> (Void -> b) -> Either b Void -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id Void -> b
forall a. Void -> a
absurd)
{-# INLINE withTopRChu #-}

-- | Inverse of 'withTopRChu'.
withTopRInvChu ::
  ChuMorphism (,) r (->) (a, ()) (Either b Void) a b
withTopRInvChu :: forall {k} (r :: k) a b.
ChuMorphism (,) r (->) (a, ()) (Either b Void) a b
withTopRInvChu = ((a, ()) -> a)
-> (b -> Either b Void)
-> ChuMorphism (,) r (->) (a, ()) (Either b Void) a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (a, ()) -> a
forall a b. (a, b) -> a
fst b -> Either b Void
forall a b. a -> Either a b
Left
{-# INLINE withTopRInvChu #-}

-- | Left unit isomorphism @A → ⊤ & A@.
withTopLChu ::
  ChuMorphism (,) r (->) a b ((), a) (Either Void b)
withTopLChu :: forall {k} (r :: k) a b.
ChuMorphism (,) r (->) a b ((), a) (Either Void b)
withTopLChu = (a -> ((), a))
-> (Either Void b -> b)
-> ChuMorphism (,) r (->) a b ((), a) (Either Void b)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\a
a -> ((), a
a)) ((Void -> b) -> (b -> b) -> Either Void b -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Void -> b
forall a. Void -> a
absurd b -> b
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id)
{-# INLINE withTopLChu #-}

-- | Inverse of 'withTopLChu'.
withTopLInvChu ::
  ChuMorphism (,) r (->) ((), a) (Either Void b) a b
withTopLInvChu :: forall {k} (r :: k) a b.
ChuMorphism (,) r (->) ((), a) (Either Void b) a b
withTopLInvChu = (((), a) -> a)
-> (b -> Either Void b)
-> ChuMorphism (,) r (->) ((), a) (Either Void b) a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism ((), a) -> a
forall a b. (a, b) -> b
snd b -> Either Void b
forall a b. b -> Either a b
Right
{-# INLINE withTopLInvChu #-}

-- | Left unit isomorphism @A → 0 ⊕ A@.
zeroPlusLChu ::
  ChuMorphism (,) r (->) a b (Either Void a) ((), b)
zeroPlusLChu :: forall {k} (r :: k) a b.
ChuMorphism (,) r (->) a b (Either Void a) ((), b)
zeroPlusLChu = (a -> Either Void a)
-> (((), b) -> b)
-> ChuMorphism (,) r (->) a b (Either Void a) ((), b)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism a -> Either Void a
forall a b. b -> Either a b
Right ((), b) -> b
forall a b. (a, b) -> b
snd
{-# INLINE zeroPlusLChu #-}

-- | Inverse of 'zeroPlusLChu'.
zeroPlusLInvChu ::
  ChuMorphism (,) r (->) (Either Void a) ((), b) a b
zeroPlusLInvChu :: forall {k} (r :: k) a b.
ChuMorphism (,) r (->) (Either Void a) ((), b) a b
zeroPlusLInvChu = (Either Void a -> a)
-> (b -> ((), b))
-> ChuMorphism (,) r (->) (Either Void a) ((), b) a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism ((Void -> a) -> (a -> a) -> Either Void a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Void -> a
forall a. Void -> a
absurd a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id) (\b
n -> ((), b
n))
{-# INLINE zeroPlusLInvChu #-}

-- | Right unit isomorphism @A → A ⊕ 0@.
zeroPlusRChu ::
  ChuMorphism (,) r (->) a b (Either a Void) (b, ())
zeroPlusRChu :: forall {k} (r :: k) a b.
ChuMorphism (,) r (->) a b (Either a Void) (b, ())
zeroPlusRChu = (a -> Either a Void)
-> ((b, ()) -> b)
-> ChuMorphism (,) r (->) a b (Either a Void) (b, ())
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism a -> Either a Void
forall a b. a -> Either a b
Left (b, ()) -> b
forall a b. (a, b) -> a
fst
{-# INLINE zeroPlusRChu #-}

-- | Inverse of 'zeroPlusRChu'.
zeroPlusRInvChu ::
  ChuMorphism (,) r (->) (Either a Void) (b, ()) a b
zeroPlusRInvChu :: forall {k} (r :: k) a b.
ChuMorphism (,) r (->) (Either a Void) (b, ()) a b
zeroPlusRInvChu = (Either a Void -> a)
-> (b -> (b, ()))
-> ChuMorphism (,) r (->) (Either a Void) (b, ()) a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism ((a -> a) -> (Void -> a) -> Either a Void -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id Void -> a
forall a. Void -> a
absurd) (\b
n -> (b
n, ()))
{-# INLINE zeroPlusRInvChu #-}

-- | Evaluation counit @A ⊗ (A ⊸ B) → B@ over @Set@.
--
-- Forward applies the Chu morphism stored in the implication object.
-- Backward pairs the argument with its own positive point, recovering the
-- adjoint condition.
evalChu ::
  ChuObj (,) r (->) a b ->
  ChuObj (,) r (->) c d ->
  ChuMorphism (,) r (->) (a, ChuParPos b a c d) (ChuTensorNeg a b (ChuParPos b a c d) (a, d)) c d
evalChu :: forall r a b c d.
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuMorphism
     (,)
     r
     (->)
     (a, ChuParPos b a c d)
     (ChuTensorNeg a b (ChuParPos b a c d) (a, d))
     c
     d
evalChu ChuObj (,) r (->) a b
_ ChuObj (,) r (->) c d
_ =
  ((a, ChuParPos b a c d) -> c)
-> (d -> ChuTensorNeg a b (ChuParPos b a c d) (a, d))
-> ChuMorphism
     (,)
     r
     (->)
     (a, ChuParPos b a c d)
     (ChuTensorNeg a b (ChuParPos b a c d) (a, d))
     c
     d
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\(a
x, ChuParPos b a c d
m) -> ChuParPos b a c d -> a -> c
forall a b c d. ChuParPos a b c d -> b -> c
cppForward ChuParPos b a c d
m a
x)
    (\d
d -> (a -> (a, d))
-> (ChuParPos b a c d -> b)
-> ChuTensorNeg a b (ChuParPos b a c d) (a, d)
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (\a
x -> (a
x, d
d)) (\ChuParPos b a c d
m -> ChuParPos b a c d -> d -> b
forall a b c d. ChuParPos a b c d -> d -> a
cppBackward ChuParPos b a c d
m d
d))

-- | Tensor of two Chu morphisms.
tensorChu ::
  ChuMorphism (,) r (->) a b c d ->
  ChuMorphism (,) r (->) e f g h ->
  ChuMorphism (,) r (->) (a, e) (ChuTensorNeg a b e f) (c, g) (ChuTensorNeg c d g h)
tensorChu :: forall {k} (r :: k) a b c d e f g h.
ChuMorphism (,) r (->) a b c d
-> ChuMorphism (,) r (->) e f g h
-> ChuMorphism
     (,)
     r
     (->)
     (a, e)
     (ChuTensorNeg a b e f)
     (c, g)
     (ChuTensorNeg c d g h)
tensorChu (ChuMorphism a -> c
fPos d -> b
fNeg) (ChuMorphism e -> g
gPos h -> f
gNeg) =
  ((a, e) -> (c, g))
-> (ChuTensorNeg c d g h -> ChuTensorNeg a b e f)
-> ChuMorphism
     (,)
     r
     (->)
     (a, e)
     (ChuTensorNeg a b e f)
     (c, g)
     (ChuTensorNeg c d g h)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\(a
x, e
y) -> (a -> c
fPos a
x, e -> g
gPos e
y))
    (\(ChuTensorNeg c -> h
h g -> d
k) -> (a -> f) -> (e -> b) -> ChuTensorNeg a b e f
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (h -> f
gNeg (h -> f) -> (c -> h) -> c -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. c -> h
h (c -> f) -> (a -> c) -> a -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> c
fPos) (d -> b
fNeg (d -> b) -> (g -> d) -> g -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. g -> d
k (g -> b) -> (e -> g) -> e -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. e -> g
gPos))

-- | Par of two Chu morphisms.
parChu ::
  ChuMorphism (,) r (->) a b c d ->
  ChuMorphism (,) r (->) e f g h ->
  ChuMorphism (,) r (->) (ChuParPos a b e f) (b, f) (ChuParPos c d g h) (d, h)
parChu :: forall {k} (r :: k) a b c d e f g h.
ChuMorphism (,) r (->) a b c d
-> ChuMorphism (,) r (->) e f g h
-> ChuMorphism
     (,) r (->) (ChuParPos a b e f) (b, f) (ChuParPos c d g h) (d, h)
parChu (ChuMorphism a -> c
fPos d -> b
fNeg) (ChuMorphism e -> g
gPos h -> f
gNeg) =
  (ChuParPos a b e f -> ChuParPos c d g h)
-> ((d, h) -> (b, f))
-> ChuMorphism
     (,) r (->) (ChuParPos a b e f) (b, f) (ChuParPos c d g h) (d, h)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\(ChuParPos b -> e
h f -> a
k) -> (d -> g) -> (h -> c) -> ChuParPos c d g h
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos (e -> g
gPos (e -> g) -> (b -> e) -> b -> g
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. b -> e
h (b -> g) -> (d -> b) -> d -> g
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. d -> b
fNeg) (a -> c
fPos (a -> c) -> (f -> a) -> f -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. f -> a
k (f -> c) -> (h -> f) -> h -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. h -> f
gNeg))
    (\(d
x, h
y) -> (d -> b
fNeg d
x, h -> f
gNeg h
y))

-- | Unit object @I = (1, K)@ with pairing @snd@.
chuUnitObj :: ChuObj (,) r (->) () r
chuUnitObj :: forall r. ChuObj (,) r (->) () r
chuUnitObj = (((), r) -> r) -> ChuObj (,) r (->) () r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj ((), r) -> r
forall a b. (a, b) -> b
snd

-- | Bottom object @⊥ = (K, 1)@, dual of the unit.
chuBottomObj :: ChuObj (,) r (->) r ()
chuBottomObj :: forall r. ChuObj (,) r (->) r ()
chuBottomObj = ((r, ()) -> r) -> ChuObj (,) r (->) r ()
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (\(r
k, ()) -> r
k)

-- | Left unitor @λ_A : I ⊗ A → A@ over @Set@.
--
-- Forward drops the unit; backward maps a negative point @b@ to the unique
-- Chu tensor negative with @f() = b@ and @g a = e(a, b)@.
leftUnitorChu ::
  ChuObj (,) r (->) a b ->
  ChuMorphism (,) r (->) ((), a) (ChuTensorNeg () r a b) a b
leftUnitorChu :: forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) ((), a) (ChuTensorNeg () r a b) a b
leftUnitorChu (ChuObj (a, b) -> r
e) =
  (((), a) -> a)
-> (b -> ChuTensorNeg () r a b)
-> ChuMorphism (,) r (->) ((), a) (ChuTensorNeg () r a b) a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism ((), a) -> a
forall a b. (a, b) -> b
snd (\b
b -> (() -> b) -> (a -> r) -> ChuTensorNeg () r a b
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (b -> () -> b
forall a b. a -> b -> a
const b
b) (\a
a -> (a, b) -> r
e (a
a, b
b)))

-- | Inverse of the left unitor.
leftUnitorChuInv ::
  ChuObj (,) r (->) a b ->
  ChuMorphism (,) r (->) a b ((), a) (ChuTensorNeg () r a b)
leftUnitorChuInv :: forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) a b ((), a) (ChuTensorNeg () r a b)
leftUnitorChuInv ChuObj (,) r (->) a b
_ = (a -> ((), a))
-> (ChuTensorNeg () r a b -> b)
-> ChuMorphism (,) r (->) a b ((), a) (ChuTensorNeg () r a b)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism ((),) (\(ChuTensorNeg () -> b
f a -> r
_) -> () -> b
f ())

-- | Right unitor @ρ_A : A ⊗ I → A@ over @Set@.
rightUnitorChu ::
  ChuObj (,) r (->) a b ->
  ChuMorphism (,) r (->) (a, ()) (ChuTensorNeg a b () r) a b
rightUnitorChu :: forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) (a, ()) (ChuTensorNeg a b () r) a b
rightUnitorChu (ChuObj (a, b) -> r
e) =
  ((a, ()) -> a)
-> (b -> ChuTensorNeg a b () r)
-> ChuMorphism (,) r (->) (a, ()) (ChuTensorNeg a b () r) a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (a, ()) -> a
forall a b. (a, b) -> a
fst (\b
b -> (a -> r) -> (() -> b) -> ChuTensorNeg a b () r
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (\a
a -> (a, b) -> r
e (a
a, b
b)) (b -> () -> b
forall a b. a -> b -> a
const b
b))

-- | Inverse of the right unitor.
rightUnitorChuInv ::
  ChuObj (,) r (->) a b ->
  ChuMorphism (,) r (->) a b (a, ()) (ChuTensorNeg a b () r)
rightUnitorChuInv :: forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) a b (a, ()) (ChuTensorNeg a b () r)
rightUnitorChuInv ChuObj (,) r (->) a b
_ = (a -> (a, ()))
-> (ChuTensorNeg a b () r -> b)
-> ChuMorphism (,) r (->) a b (a, ()) (ChuTensorNeg a b () r)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\a
a -> (a
a, ())) (\(ChuTensorNeg a -> r
_ () -> b
g) -> () -> b
g ())

-- | Associator @(A ⊗ B) ⊗ C → A ⊗ (B ⊗ C)@ over @Set@.
--
-- Positives reassociate as pairs.  Negatives reassociate the adjoint
-- pairs: a negative of @A ⊗ (B ⊗ C)@ is sent to a negative of
-- @(A ⊗ B) ⊗ C@ by unpacking the inner 'ChuTensorNeg'.
assocChu ::
  ChuMorphism
    (,)
    r
    (->)
    ((a, c), e)
    (ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f)
    (a, (c, e))
    (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
assocChu :: forall {k} (r :: k) a c e b d f.
ChuMorphism
  (,)
  r
  (->)
  ((a, c), e)
  (ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f)
  (a, (c, e))
  (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
assocChu =
  (((a, c), e) -> (a, (c, e)))
-> (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f)
    -> ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f)
-> ChuMorphism
     (,)
     r
     (->)
     ((a, c), e)
     (ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f)
     (a, (c, e))
     (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\((a
x, c
y), e
z) -> (a
x, (c
y, e
z)))
    ( \(ChuTensorNeg a -> ChuTensorNeg c d e f
h (c, e) -> b
k) ->
        ((a, c) -> f)
-> (e -> ChuTensorNeg a b c d)
-> ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg
          (\(a
x, c
y) -> ChuTensorNeg c d e f -> c -> f
forall a b c d. ChuTensorNeg a b c d -> a -> d
ctnForward (a -> ChuTensorNeg c d e f
h a
x) c
y)
          (\e
z -> (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (\a
x -> ChuTensorNeg c d e f -> e -> d
forall a b c d. ChuTensorNeg a b c d -> c -> b
ctnBackward (a -> ChuTensorNeg c d e f
h a
x) e
z) (\c
y -> (c, e) -> b
k (c
y, e
z)))
    )
{-# INLINE assocChu #-}

-- | Inverse associator @A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C@ over @Set@.
assocChuInv ::
  ChuMorphism
    (,)
    r
    (->)
    (a, (c, e))
    (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
    ((a, c), e)
    (ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f)
assocChuInv :: forall {k} (r :: k) a c e b d f.
ChuMorphism
  (,)
  r
  (->)
  (a, (c, e))
  (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
  ((a, c), e)
  (ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f)
assocChuInv =
  ((a, (c, e)) -> ((a, c), e))
-> (ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f
    -> ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
-> ChuMorphism
     (,)
     r
     (->)
     (a, (c, e))
     (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
     ((a, c), e)
     (ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\(a
x, (c
y, e
z)) -> ((a
x, c
y), e
z))
    ( \(ChuTensorNeg (a, c) -> f
f e -> ChuTensorNeg a b c d
g) ->
        (a -> ChuTensorNeg c d e f)
-> ((c, e) -> b) -> ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f)
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg
          (\a
x -> (c -> f) -> (e -> d) -> ChuTensorNeg c d e f
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (\c
y -> (a, c) -> f
f (a
x, c
y)) (\e
z -> ChuTensorNeg a b c d -> a -> d
forall a b c d. ChuTensorNeg a b c d -> a -> d
ctnForward (e -> ChuTensorNeg a b c d
g e
z) a
x))
          (\(c
y, e
z) -> ChuTensorNeg a b c d -> c -> b
forall a b c d. ChuTensorNeg a b c d -> c -> b
ctnBackward (e -> ChuTensorNeg a b c d
g e
z) c
y)
    )
{-# INLINE assocChuInv #-}

-- | Slide @A ⊗ (B ⊗ C) → B ⊗ (A ⊗ C)@ over @Set@.
--
-- This is the Channel 'slide', derived as @assoc . tensor braid id . assoc'@
-- and written directly so the instance does not have to manufacture
-- intermediate object constraints.
slideChu ::
  ChuMorphism
    (,)
    r
    (->)
    (a, (c, e))
    (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
    (c, (a, e))
    (ChuTensorNeg c d (a, e) (ChuTensorNeg a b e f))
slideChu :: forall {k} (r :: k) a c e b d f.
ChuMorphism
  (,)
  r
  (->)
  (a, (c, e))
  (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
  (c, (a, e))
  (ChuTensorNeg c d (a, e) (ChuTensorNeg a b e f))
slideChu =
  ((a, (c, e)) -> (c, (a, e)))
-> (ChuTensorNeg c d (a, e) (ChuTensorNeg a b e f)
    -> ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
-> ChuMorphism
     (,)
     r
     (->)
     (a, (c, e))
     (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
     (c, (a, e))
     (ChuTensorNeg c d (a, e) (ChuTensorNeg a b e f))
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\(a
x, (c
y, e
z)) -> (c
y, (a
x, e
z)))
    ( \(ChuTensorNeg c -> ChuTensorNeg a b e f
h' (a, e) -> d
k') ->
        (a -> ChuTensorNeg c d e f)
-> ((c, e) -> b) -> ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f)
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg
          (\a
x -> (c -> f) -> (e -> d) -> ChuTensorNeg c d e f
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (\c
y -> ChuTensorNeg a b e f -> a -> f
forall a b c d. ChuTensorNeg a b c d -> a -> d
ctnForward (c -> ChuTensorNeg a b e f
h' c
y) a
x) (\e
z -> (a, e) -> d
k' (a
x, e
z)))
          (\(c
y, e
z) -> ChuTensorNeg a b e f -> e -> b
forall a b c d. ChuTensorNeg a b c d -> c -> b
ctnBackward (c -> ChuTensorNeg a b e f
h' c
y) e
z)
    )
{-# INLINE slideChu #-}

-- | Enumerate all 'ChuTensorNeg' values for finite carriers.
chuTensorNegs ::
  forall r a b.
  (Eq r, Eq (ChuPosType a), Eq (ChuPosType b), ChuObject r a, ChuObject r b) =>
  Proxy a ->
  Proxy b ->
  [ChuTensorNeg (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)]
chuTensorNegs :: forall r a b.
(Eq r, Eq (ChuPosType a), Eq (ChuPosType b), ChuObject r a,
 ChuObject r b) =>
Proxy a
-> Proxy b
-> [ChuTensorNeg
      (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)]
chuTensorNegs Proxy a
_ Proxy b
_ =
  let as :: [ChuPosType a]
as = forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @a
      bs :: [ChuNegType a]
bs = forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @a
      cs :: [ChuPosType b]
cs = forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @b
      ds :: [ChuNegType b]
ds = forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @b
      r :: (ChuPosType a, ChuNegType a) -> r
r = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> (ChuPosType a, ChuNegType a) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)
      s :: (ChuPosType b, ChuNegType b) -> r
s = ChuObj (,) r (->) (ChuPosType b) (ChuNegType b)
-> (ChuPosType b, ChuNegType b) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @b)
   in [ (ChuPosType a -> ChuNegType b)
-> (ChuPosType b -> ChuNegType a)
-> ChuTensorNeg
     (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg ChuPosType a -> ChuNegType b
f ChuPosType b -> ChuNegType a
g
      | ChuPosType a -> ChuNegType b
f <- [ChuPosType a] -> [ChuNegType b] -> [ChuPosType a -> ChuNegType b]
forall a b. Eq a => [a] -> [b] -> [a -> b]
functions [ChuPosType a]
as [ChuNegType b]
ds,
        ChuPosType b -> ChuNegType a
g <- [ChuPosType b] -> [ChuNegType a] -> [ChuPosType b -> ChuNegType a]
forall a b. Eq a => [a] -> [b] -> [a -> b]
functions [ChuPosType b]
cs [ChuNegType a]
bs,
        ((ChuPosType a, ChuPosType b) -> Bool)
-> [(ChuPosType a, ChuPosType b)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(ChuPosType a
a, ChuPosType b
c) -> (ChuPosType a, ChuNegType a) -> r
r (ChuPosType a
a, ChuPosType b -> ChuNegType a
g ChuPosType b
c) r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== (ChuPosType b, ChuNegType b) -> r
s (ChuPosType b
c, ChuPosType a -> ChuNegType b
f ChuPosType a
a)) ([ChuPosType a] -> [ChuPosType b] -> [(ChuPosType a, ChuPosType b)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian [ChuPosType a]
as [ChuPosType b]
cs)
      ]

-- | Enumerate all 'ChuParPos' values for finite carriers.
chuParPoss ::
  forall r a b.
  (Eq r, Eq (ChuNegType a), Eq (ChuNegType b), ChuObject r a, ChuObject r b) =>
  Proxy a ->
  Proxy b ->
  [ChuParPos (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)]
chuParPoss :: forall r a b.
(Eq r, Eq (ChuNegType a), Eq (ChuNegType b), ChuObject r a,
 ChuObject r b) =>
Proxy a
-> Proxy b
-> [ChuParPos
      (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)]
chuParPoss Proxy a
_ Proxy b
_ =
  let as :: [ChuPosType a]
as = forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @a
      bs :: [ChuNegType a]
bs = forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @a
      cs :: [ChuPosType b]
cs = forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @b
      ds :: [ChuNegType b]
ds = forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @b
      r :: (ChuPosType a, ChuNegType a) -> r
r = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> (ChuPosType a, ChuNegType a) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)
      s :: (ChuPosType b, ChuNegType b) -> r
s = ChuObj (,) r (->) (ChuPosType b) (ChuNegType b)
-> (ChuPosType b, ChuNegType b) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @b)
   in [ (ChuNegType a -> ChuPosType b)
-> (ChuNegType b -> ChuPosType a)
-> ChuParPos
     (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos ChuNegType a -> ChuPosType b
f ChuNegType b -> ChuPosType a
g
      | ChuNegType a -> ChuPosType b
f <- [ChuNegType a] -> [ChuPosType b] -> [ChuNegType a -> ChuPosType b]
forall a b. Eq a => [a] -> [b] -> [a -> b]
functions [ChuNegType a]
bs [ChuPosType b]
cs,
        ChuNegType b -> ChuPosType a
g <- [ChuNegType b] -> [ChuPosType a] -> [ChuNegType b -> ChuPosType a]
forall a b. Eq a => [a] -> [b] -> [a -> b]
functions [ChuNegType b]
ds [ChuPosType a]
as,
        ((ChuNegType a, ChuNegType b) -> Bool)
-> [(ChuNegType a, ChuNegType b)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(ChuNegType a
b, ChuNegType b
d) -> (ChuPosType a, ChuNegType a) -> r
r (ChuNegType b -> ChuPosType a
g ChuNegType b
d, ChuNegType a
b) r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== (ChuPosType b, ChuNegType b) -> r
s (ChuNegType a -> ChuPosType b
f ChuNegType a
b, ChuNegType b
d)) ([ChuNegType a] -> [ChuNegType b] -> [(ChuNegType a, ChuNegType b)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian [ChuNegType a]
bs [ChuNegType b]
ds)
      ]

-- | All functions from a finite domain to a finite codomain.
--
-- The domain list is assumed to be an exhaustive enumeration of the type;
-- supplying an incomplete list makes the returned functions silently wrong
-- rather than loudly partial. The empty-domain case returns a bottom so that
-- the list type remains useful, but callers should avoid reaching it.
functions :: (Eq a) => [a] -> [b] -> [a -> b]
functions :: forall a b. Eq a => [a] -> [b] -> [a -> b]
functions [] [b]
_ = [b -> a -> b
forall a b. a -> b -> a
const ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"functions: empty domain")]
functions [a]
domain [b]
codomain = ([b] -> a -> b) -> [[b]] -> [a -> b]
forall a b. (a -> b) -> [a] -> [b]
map ([a] -> [b] -> a -> b
forall a b. Eq a => [a] -> [b] -> a -> b
listToFunction [a]
domain) ([[b]] -> [[b]]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA (Int -> [b] -> [[b]]
forall a. Int -> a -> [a]
replicate ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
domain) [b]
codomain))

listToFunction :: (Eq a) => [a] -> [b] -> a -> b
listToFunction :: forall a b. Eq a => [a] -> [b] -> a -> b
listToFunction [a]
domain [b]
values a
x = Maybe b -> b
forall {a}. Maybe a -> a
fromJust (a -> [(a, b)] -> Maybe b
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
x ([a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
domain [b]
values))
  where
    fromJust :: Maybe a -> a
fromJust (Just a
y) = a
y
    fromJust Maybe a
Nothing = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"listToFunction: input not in domain"

-- | Cartesian product of two lists.
cartesian :: [a] -> [b] -> [(a, b)]
cartesian :: forall a b. [a] -> [b] -> [(a, b)]
cartesian [a]
xs [b]
ys = [(a
x, b
y) | a
x <- [a]
xs, b
y <- [b]
ys]

-- | A Chu object is /separated/ when the pairing distinguishes every pair of
-- positive points.  Equivalently, the transposed pairing @A⁺ -> (A⁻ ⊸ ⊥)@ is
-- injective.
chuSeparated ::
  forall r a.
  (Eq r, Eq (ChuPosType a), ChuObject r a) =>
  Proxy a ->
  Bool
chuSeparated :: forall r a.
(Eq r, Eq (ChuPosType a), ChuObject r a) =>
Proxy a -> Bool
chuSeparated Proxy a
_ =
  let e :: (ChuPosType a, ChuNegType a) -> r
e = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> (ChuPosType a, ChuNegType a) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)
      as :: [ChuPosType a]
as = forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @a
      bs :: [ChuNegType a]
bs = forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @a
   in ((ChuPosType a, ChuPosType a) -> Bool)
-> [(ChuPosType a, ChuPosType a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
        (\(ChuPosType a
a1, ChuPosType a
a2) -> ChuPosType a
a1 ChuPosType a -> ChuPosType a -> Bool
forall a. Eq a => a -> a -> Bool
== ChuPosType a
a2 Bool -> Bool -> Bool
|| (ChuNegType a -> Bool) -> [ChuNegType a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ChuNegType a
b -> (ChuPosType a, ChuNegType a) -> r
e (ChuPosType a
a1, ChuNegType a
b) r -> r -> Bool
forall a. Eq a => a -> a -> Bool
/= (ChuPosType a, ChuNegType a) -> r
e (ChuPosType a
a2, ChuNegType a
b)) [ChuNegType a]
bs)
        ([ChuPosType a] -> [ChuPosType a] -> [(ChuPosType a, ChuPosType a)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian [ChuPosType a]
as [ChuPosType a]
as)

-- | A Chu object is /extensional/ when the pairing distinguishes every pair of
-- negative points.  Equivalently, the pairing @A⁻ -> (A⁺ ⊸ ⊥)@ is injective.
chuExtensional ::
  forall r a.
  (Eq r, Eq (ChuNegType a), ChuObject r a) =>
  Proxy a ->
  Bool
chuExtensional :: forall r a.
(Eq r, Eq (ChuNegType a), ChuObject r a) =>
Proxy a -> Bool
chuExtensional Proxy a
_ =
  let e :: (ChuPosType a, ChuNegType a) -> r
e = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> (ChuPosType a, ChuNegType a) -> r
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
ChuObj t r arr a b -> arr (t a b) r
chuPair (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)
      as :: [ChuPosType a]
as = forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @a
      bs :: [ChuNegType a]
bs = forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @a
   in ((ChuNegType a, ChuNegType a) -> Bool)
-> [(ChuNegType a, ChuNegType a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
        (\(ChuNegType a
b1, ChuNegType a
b2) -> ChuNegType a
b1 ChuNegType a -> ChuNegType a -> Bool
forall a. Eq a => a -> a -> Bool
== ChuNegType a
b2 Bool -> Bool -> Bool
|| (ChuPosType a -> Bool) -> [ChuPosType a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ChuPosType a
a -> (ChuPosType a, ChuNegType a) -> r
e (ChuPosType a
a, ChuNegType a
b1) r -> r -> Bool
forall a. Eq a => a -> a -> Bool
/= (ChuPosType a, ChuNegType a) -> r
e (ChuPosType a
a, ChuNegType a
b2)) [ChuPosType a]
as)
        ([ChuNegType a] -> [ChuNegType a] -> [(ChuNegType a, ChuNegType a)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian [ChuNegType a]
bs [ChuNegType a]
bs)

-- ===========================================================================
-- Object-indexed Chu category (OChu / SepChu)
-- ===========================================================================
--
-- The existing 'Chu' category treats any 'ChuObj'-shaped type as an object.
-- That is too unstructured for a 'Tensor' instance: the unit object is not
-- the bare @()@, and structural morphisms such as the unitors need the
-- object's pairing.  'OChu' restricts objects to types that carry a canonical
-- 'ChuObj' value via the 'ChuObject' class, and its 'Ob' further requires
-- separation and extensionality.  That is Barr's separated-extensional
-- subcategory: the room where @A ≅ A⊥⊥@ and the associator pentagon lives.
-- 'SepChu' is a synonym for this reading.

-- | A type-level Chu object: a tag with a canonical 'ChuObj' value and
-- finite carrier enumerations.
--
-- 'chuPosAll' and 'chuNegAll' are used by separation / extensionality oracles
-- and by enumeration of tensor / par negatives.  They default to a runtime
-- error; only objects that actually participate in finite oracles need to
-- supply them.
class ChuObject (r :: Type) a where
  chuObject :: ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
  chuPosAll :: [ChuPosType a]
  chuPosAll = [Char] -> [ChuPosType a]
forall a. HasCallStack => [Char] -> a
error [Char]
"chuPosAll: not defined for this object"
  chuNegAll :: [ChuNegType a]
  chuNegAll = [Char] -> [ChuNegType a]
forall a. HasCallStack => [Char] -> a
error [Char]
"chuNegAll: not defined for this object"

-- | Marker: the pairing distinguishes positive points.
--
-- Runtime evidence is available through 'chuSeparated'.  Instances close the
-- constructors we admit ('ChuTwo', 'ChuOUnit', tensor, negation).
class (ChuObject r a) => ChuSeparated r a

-- | Marker: the pairing distinguishes negative points.
--
-- Runtime evidence is available through 'chuExtensional'.  Negation swaps
-- this with 'ChuSeparated'.
class (ChuObject r a) => ChuExtensional r a

-- | Type-level non-emptiness of an object's positive carrier.
--
-- Used to guard additive marker instances: @A & B@ can only be extensional
-- when both @A@ and @B@ have at least one positive point, because the
-- negative carrier is the disjoint union and distinct injections must be
-- separated by a positive pair.
type family ChuPosNonEmpty (a :: Type) :: Bool where
  ChuPosNonEmpty (ChuOUnit r) = 'True
  ChuPosNonEmpty (ChuOTop r) = 'True
  ChuPosNonEmpty (ChuOZero r) = 'False
  ChuPosNonEmpty (ChuOTensor r a b) = If (ChuPosNonEmpty a) (ChuPosNonEmpty b) 'False
  ChuPosNonEmpty (ChuOWith r a b) = If (ChuPosNonEmpty a) (ChuPosNonEmpty b) 'False
  ChuPosNonEmpty (ChuOPlus r a b) = If (ChuPosNonEmpty a) 'True (ChuPosNonEmpty b)
  ChuPosNonEmpty (ChuOPar r a b) = 'True
  ChuPosNonEmpty (ChuONeg r a) = ChuNegNonEmpty a
  ChuPosNonEmpty (ChuOLolli r a b) = 'True
  ChuPosNonEmpty (ChuOBang r a) = ChuPosNonEmpty a
  ChuPosNonEmpty (ChuOWhyNot r a) = 'True
  ChuPosNonEmpty ChuTwo = 'True
  ChuPosNonEmpty ChuThree = 'True
  ChuPosNonEmpty ChuDouble01 = 'True
  ChuPosNonEmpty ChuDelivery = 'True

-- | Type-level non-emptiness of an object's negative carrier.
--
-- Used to guard additive marker instances: @A ⊕ B@ can only be separated
-- when both @A@ and @B@ have at least one negative point, because the
-- positive carrier is the disjoint union and distinct injections must be
-- separated by a negative pair.
type family ChuNegNonEmpty (a :: Type) :: Bool where
  ChuNegNonEmpty (ChuOUnit r) = 'True
  ChuNegNonEmpty (ChuOTop r) = 'False
  ChuNegNonEmpty (ChuOZero r) = 'True
  ChuNegNonEmpty (ChuOTensor r a b) = 'True
  ChuNegNonEmpty (ChuOWith r a b) = If (ChuNegNonEmpty a) 'True (ChuNegNonEmpty b)
  ChuNegNonEmpty (ChuOPlus r a b) = If (ChuNegNonEmpty a) (ChuNegNonEmpty b) 'False
  ChuNegNonEmpty (ChuOPar r a b) = If (ChuNegNonEmpty a) (ChuNegNonEmpty b) 'False
  ChuNegNonEmpty (ChuONeg r a) = ChuPosNonEmpty a
  ChuNegNonEmpty (ChuOLolli r a b) = If (ChuPosNonEmpty a) (ChuNegNonEmpty b) 'False
  ChuNegNonEmpty (ChuOBang r a) = 'True
  ChuNegNonEmpty (ChuOWhyNot r a) = ChuNegNonEmpty a
  ChuNegNonEmpty ChuTwo = 'True
  ChuNegNonEmpty ChuThree = 'True
  ChuNegNonEmpty ChuDouble01 = 'True
  ChuNegNonEmpty ChuDelivery = 'True

-- | Unit object type for 'OChu'.
data ChuOUnit (r :: Type) = ChuOUnit

instance ChuObject r (ChuOUnit r) where
  chuObject :: ChuObj
  (,) r (->) (ChuPosType (ChuOUnit r)) (ChuNegType (ChuOUnit r))
chuObject = ChuObj (,) r (->) () r
ChuObj
  (,) r (->) (ChuPosType (ChuOUnit r)) (ChuNegType (ChuOUnit r))
forall r. ChuObj (,) r (->) () r
chuUnitObj
  chuPosAll :: [ChuPosType (ChuOUnit r)]
chuPosAll = [()]
  chuNegAll :: [ChuNegType (ChuOUnit r)]
chuNegAll = [Char] -> [r]
forall a. HasCallStack => [Char] -> a
error [Char]
"chuNegAll: ChuOUnit negative carrier is the dualising object and is not enumerated"

instance ChuSeparated r (ChuOUnit r)

instance ChuExtensional r (ChuOUnit r)

-- | Tensor object type for 'OChu'.
data ChuOTensor (r :: Type) a b = ChuOTensor

type instance Unit (ChuOTensor r) = ChuOUnit r

instance
  (Eq r, ChuObject r a, ChuObject r b) =>
  ChuObject r (ChuOTensor r a b)
  where
  chuObject :: ChuObj
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a b))
  (ChuNegType (ChuOTensor r a b))
chuObject = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuObj (,) r (->) (ChuPosType b) (ChuNegType b)
-> ChuObj
     (,)
     r
     (->)
     (ChuPosType a, ChuPosType b)
     (ChuTensorNeg
        (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
forall r a b c d.
Eq r =>
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuObj (,) r (->) (a, c) (ChuTensorNeg a b c d)
tensorChuObj (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a) (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @b)
  chuPosAll :: [ChuPosType (ChuOTensor r a b)]
chuPosAll = [ChuPosType a] -> [ChuPosType b] -> [(ChuPosType a, ChuPosType b)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian (forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @a) (forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @b)
  chuNegAll :: [ChuNegType (ChuOTensor r a b)]
chuNegAll = [Char]
-> [ChuTensorNeg
      (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)]
forall a. HasCallStack => [Char] -> a
error [Char]
"chuNegAll: tensor negative carrier is not enumerated"

instance (Eq r, ChuSeparated r a, ChuSeparated r b) => ChuSeparated r (ChuOTensor r a b)

instance (Eq r, ChuExtensional r a, ChuExtensional r b) => ChuExtensional r (ChuOTensor r a b)

-- | Object-level negation @A⊥@.
--
-- Carriers swap; the pairing is 'negateChu' of the underlying object.
-- Separation and extensionality swap: if @A@ is separated then @A⊥@ is
-- extensional, and conversely.
data ChuONeg (r :: Type) a = ChuONeg

instance (ChuObject r a) => ChuObject r (ChuONeg r a) where
  chuObject :: ChuObj
  (,) r (->) (ChuPosType (ChuONeg r a)) (ChuNegType (ChuONeg r a))
chuObject = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuObj (,) r (->) (ChuNegType a) (ChuPosType a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (r :: k)
       (a :: k) (b :: k).
Action t arr =>
ChuObj t r arr a b -> ChuObj t r arr b a
negateChu (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)
  chuPosAll :: [ChuPosType (ChuONeg r a)]
chuPosAll = forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @a
  chuNegAll :: [ChuNegType (ChuONeg r a)]
chuNegAll = forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @a

instance (ChuExtensional r a) => ChuSeparated r (ChuONeg r a)

instance (ChuSeparated r a) => ChuExtensional r (ChuONeg r a)

-- | The self-dual two-point Chu object used in the oracles.
data ChuTwo = ChuTwo

instance ChuObject Bool ChuTwo where
  chuObject :: ChuObj (,) Bool (->) (ChuPosType ChuTwo) (ChuNegType ChuTwo)
chuObject = ((Bool, Bool) -> Bool) -> ChuObj (,) Bool (->) Bool Bool
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj ((Bool -> LolliT (,) (->) Bool Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> LolliT (,) (->) b c) -> (a, b) -> c
forall (t :: * -> * -> *) (arr :: * -> * -> *) a b c.
Lolli t arr =>
arr a (LolliT t arr b c) -> arr (t a b) c
uncurry Bool -> LolliT (,) (->) Bool Bool
Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==))
  chuPosAll :: [ChuPosType ChuTwo]
chuPosAll = [Bool
ChuPosType ChuTwo
False, Bool
ChuPosType ChuTwo
True]
  chuNegAll :: [ChuNegType ChuTwo]
chuNegAll = [Bool
ChuNegType ChuTwo
False, Bool
ChuNegType ChuTwo
True]

instance ChuSeparated Bool ChuTwo

instance ChuExtensional Bool ChuTwo

-- | A non-self-dual three-point Chu object over 'Bool'.
--
-- Both carriers are @Maybe Bool@, but the pairing is the non-symmetric
-- partial-order relation (@Nothing <= Just False <= Just True@), not equality.
-- This breaks the self-duality coincidence of 'ChuTwo' while keeping the
-- object separated and extensional.
data ChuThree = ChuThree

instance ChuObject Bool ChuThree where
  chuObject :: ChuObj (,) Bool (->) (ChuPosType ChuThree) (ChuNegType ChuThree)
chuObject = ((Maybe Bool, Maybe Bool) -> Bool)
-> ChuObj (,) Bool (->) (Maybe Bool) (Maybe Bool)
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj ((Maybe Bool -> LolliT (,) (->) (Maybe Bool) Bool)
-> (Maybe Bool, Maybe Bool) -> Bool
forall a b c. (a -> LolliT (,) (->) b c) -> (a, b) -> c
forall (t :: * -> * -> *) (arr :: * -> * -> *) a b c.
Lolli t arr =>
arr a (LolliT t arr b c) -> arr (t a b) c
uncurry Maybe Bool -> LolliT (,) (->) (Maybe Bool) Bool
Maybe Bool -> Maybe Bool -> Bool
forall a. Ord a => a -> a -> Bool
(<=))
  chuPosAll :: [ChuPosType ChuThree]
chuPosAll = [Maybe Bool
ChuPosType ChuThree
forall a. Maybe a
Nothing, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True]
  chuNegAll :: [ChuNegType ChuThree]
chuNegAll = [Maybe Bool
ChuNegType ChuThree
forall a. Maybe a
Nothing, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True]

instance ChuSeparated Bool ChuThree

instance ChuExtensional Bool ChuThree

-- | A finite Double-semiring Chu object.
--
-- Carriers are the two-element type @Bool@, representing the subset
-- @{0, 1}@ of 'Double'.  The full real line is replaced by this tiny
-- subset so the finite oracles remain runnable.  The pairing lands in
-- 'Double' via the existing 'ChuSemiring' instance.
data ChuDouble01 = ChuDouble01

instance ChuObject Double ChuDouble01 where
  chuObject :: ChuObj
  (,) Double (->) (ChuPosType ChuDouble01) (ChuNegType ChuDouble01)
chuObject = ((Bool, Bool) -> Double) -> ChuObj (,) Double (->) Bool Bool
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (Bool, Bool) -> Double
chuDouble01Pair
    where
      chuDouble01Pair :: (Bool, Bool) -> Double
      chuDouble01Pair :: (Bool, Bool) -> Double
chuDouble01Pair (Bool
False, Bool
False) = Double
0
      chuDouble01Pair (Bool
False, Bool
True) = Double
0.5
      chuDouble01Pair (Bool
True, Bool
False) = Double
0
      chuDouble01Pair (Bool
True, Bool
True) = Double
1
  chuPosAll :: [ChuPosType ChuDouble01]
chuPosAll = [Bool
ChuPosType ChuDouble01
False, Bool
ChuPosType ChuDouble01
True]
  chuNegAll :: [ChuNegType ChuDouble01]
chuNegAll = [Bool
ChuNegType ChuDouble01
False, Bool
ChuNegType ChuDouble01
True]

instance ChuSeparated Double ChuDouble01

instance ChuExtensional Double ChuDouble01

-- | A concrete delivery-matrix Chu object: two posts and two agents.
--
-- The pairing is the boolean delivery matrix computed by 'deliveryMatrix'
-- and 'deliversToSemiring'.  Posts and agents are indexed by 'Bool' so the
-- carriers stay finite and the oracles remain runnable.
data ChuDelivery = ChuDelivery

instance ChuObject Bool ChuDelivery where
  chuObject :: ChuObj
  (,) Bool (->) (ChuPosType ChuDelivery) (ChuNegType ChuDelivery)
chuObject = ((Bool, Bool) -> Bool) -> ChuObj (,) Bool (->) Bool Bool
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (Bool, Bool) -> Bool
chuDeliveryPair
    where
      agents :: [Bool]
      agents :: [Bool]
agents = [Bool
False, Bool
True]
      recipients :: [[Bool]]
      recipients :: [[Bool]]
recipients = [[Bool
False], [Bool
False, Bool
True]]
      chuDeliveryPair :: (Bool, Bool) -> Bool
      chuDeliveryPair :: (Bool, Bool) -> Bool
chuDeliveryPair (Bool
p, Bool
a) = [Bool] -> [[Bool]] -> [[Bool]]
forall r col. (ChuSemiring r, Eq col) => [col] -> [[col]] -> [[r]]
deliveryMatrix [Bool]
agents [[Bool]]
recipients [[Bool]] -> Int -> [Bool]
forall a. HasCallStack => [a] -> Int -> a
!! Bool -> Int
forall a. Enum a => a -> Int
fromEnum Bool
p [Bool] -> Int -> Bool
forall a. HasCallStack => [a] -> Int -> a
!! Bool -> Int
forall a. Enum a => a -> Int
fromEnum Bool
a
  chuPosAll :: [ChuPosType ChuDelivery]
chuPosAll = [Bool
ChuPosType ChuDelivery
False, Bool
ChuPosType ChuDelivery
True]
  chuNegAll :: [ChuNegType ChuDelivery]
chuNegAll = [Bool
ChuNegType ChuDelivery
False, Bool
ChuNegType ChuDelivery
True]

instance ChuSeparated Bool ChuDelivery

instance ChuExtensional Bool ChuDelivery

-- | A tiny self-dual Chu object over @Any@ (disjunction monoid) with equality
-- pairing. Used to test the bimonoid on @!A@ from a 'Monoid' on @A⁺@.
data ChuAny = ChuAny

instance ChuObject Bool ChuAny where
  chuObject :: ChuObj (,) Bool (->) (ChuPosType ChuAny) (ChuNegType ChuAny)
chuObject = ((Any, Any) -> Bool) -> ChuObj (,) Bool (->) Any Any
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (\(Any Bool
x, Any Bool
y) -> Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
y)
  chuPosAll :: [ChuPosType ChuAny]
chuPosAll = [Bool -> Any
Any Bool
False, Bool -> Any
Any Bool
True]
  chuNegAll :: [ChuNegType ChuAny]
chuNegAll = [Bool -> Any
Any Bool
False, Bool -> Any
Any Bool
True]

instance ChuSeparated Bool ChuAny

instance ChuExtensional Bool ChuAny

-- | The object-indexed Chu construction as a base arrow.
newtype OChu (r :: Type) (a :: Type) (b :: Type) = OChu {forall r a b. OChu r a b -> Chu (,) r (->) a b
unOChu :: Chu (,) r (->) a b}

-- | Documentation alias for 'OChu'.
--
-- This is a plain type synonym, not a separate category: the
-- separated-extensional conditions are enforced only by the 'Ob' constraint
-- of 'OChu'.  If you need Barr's subcategory to be tracked in the type
-- system, wrap 'OChu' in a newtype with its own 'Category' instance.
type SepChu = OChu

instance Category (OChu r) where
  id :: forall a. OChu r a a
  id :: forall a. OChu r a a
id = Chu (,) r (->) a a -> OChu r a a
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu Chu (,) r (->) a a
forall a. Chu (,) r (->) a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  (.) :: forall a b c. OChu r b c -> OChu r a b -> OChu r a c
  OChu Chu (,) r (->) b c
g . :: forall a b c. OChu r b c -> OChu r a b -> OChu r a c
. OChu Chu (,) r (->) a b
f = Chu (,) r (->) a c -> OChu r a c
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (Chu (,) r (->) b c
g Chu (,) r (->) b c -> Chu (,) r (->) a b -> Chu (,) r (->) a c
forall b c a.
Chu (,) r (->) b c -> Chu (,) r (->) a b -> Chu (,) r (->) a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Chu (,) r (->) a b
f)

-- | Symmetric braiding for the Chu tensor over @Set@.
swapChu ::
  forall r a b.
  ( ChuPosType (ChuOTensor r a b) ~ (ChuPosType a, ChuPosType b),
    ChuNegType (ChuOTensor r a b)
      ~ ChuTensorNeg (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b),
    ChuPosType (ChuOTensor r b a) ~ (ChuPosType b, ChuPosType a),
    ChuNegType (ChuOTensor r b a)
      ~ ChuTensorNeg (ChuPosType b) (ChuNegType b) (ChuPosType a) (ChuNegType a)
  ) =>
  ChuMorphism
    (,)
    r
    (->)
    (ChuPosType (ChuOTensor r a b))
    (ChuNegType (ChuOTensor r a b))
    (ChuPosType (ChuOTensor r b a))
    (ChuNegType (ChuOTensor r b a))
swapChu :: forall r a b.
(ChuPosType (ChuOTensor r a b) ~ (ChuPosType a, ChuPosType b),
 ChuNegType (ChuOTensor r a b)
 ~ ChuTensorNeg
     (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b),
 ChuPosType (ChuOTensor r b a) ~ (ChuPosType b, ChuPosType a),
 ChuNegType (ChuOTensor r b a)
 ~ ChuTensorNeg
     (ChuPosType b) (ChuNegType b) (ChuPosType a) (ChuNegType a)) =>
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a b))
  (ChuNegType (ChuOTensor r a b))
  (ChuPosType (ChuOTensor r b a))
  (ChuNegType (ChuOTensor r b a))
swapChu = ((ChuPosType a, ChuPosType b) -> (ChuPosType b, ChuPosType a))
-> (ChuTensorNeg
      (ChuPosType b) (ChuNegType b) (ChuPosType a) (ChuNegType a)
    -> ChuTensorNeg
         (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a, ChuPosType b)
     (ChuTensorNeg
        (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
     (ChuPosType b, ChuPosType a)
     (ChuTensorNeg
        (ChuPosType b) (ChuNegType b) (ChuPosType a) (ChuNegType a))
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\(ChuPosType a
x, ChuPosType b
y) -> (ChuPosType b
y, ChuPosType a
x)) (\(ChuTensorNeg ChuPosType b -> ChuNegType a
h ChuPosType a -> ChuNegType b
k) -> (ChuPosType a -> ChuNegType b)
-> (ChuPosType b -> ChuNegType a)
-> ChuTensorNeg
     (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg ChuPosType a -> ChuNegType b
k ChuPosType b -> ChuNegType a
h)

-- | Parallel composition for 'OChu'.
parOChu ::
  forall r (a :: Type) (b :: Type) (c :: Type) (d :: Type).
  OChu r a b ->
  OChu r c d ->
  OChu r (ChuOTensor r a c) (ChuOTensor r b d)
parOChu :: forall r a b c d.
OChu r a b
-> OChu r c d -> OChu r (ChuOTensor r a c) (ChuOTensor r b d)
parOChu (OChu (Chu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType b)
  (ChuNegType b)
f)) (OChu (Chu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType c)
  (ChuNegType c)
  (ChuPosType d)
  (ChuNegType d)
g)) = Chu (,) r (->) (ChuOTensor r a c) (ChuOTensor r b d)
-> OChu r (ChuOTensor r a c) (ChuOTensor r b d)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a c))
  (ChuNegType (ChuOTensor r a c))
  (ChuPosType (ChuOTensor r b d))
  (ChuNegType (ChuOTensor r b d))
-> Chu (,) r (->) (ChuOTensor r a c) (ChuOTensor r b d)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType b)
  (ChuNegType b)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType c)
     (ChuNegType c)
     (ChuPosType d)
     (ChuNegType d)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a, ChuPosType c)
     (ChuTensorNeg
        (ChuPosType a) (ChuNegType a) (ChuPosType c) (ChuNegType c))
     (ChuPosType b, ChuPosType d)
     (ChuTensorNeg
        (ChuPosType b) (ChuNegType b) (ChuPosType d) (ChuNegType d))
forall {k} (r :: k) a b c d e f g h.
ChuMorphism (,) r (->) a b c d
-> ChuMorphism (,) r (->) e f g h
-> ChuMorphism
     (,)
     r
     (->)
     (a, e)
     (ChuTensorNeg a b e f)
     (c, g)
     (ChuTensorNeg c d g h)
tensorChu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType b)
  (ChuNegType b)
f ChuMorphism
  (,)
  r
  (->)
  (ChuPosType c)
  (ChuNegType c)
  (ChuPosType d)
  (ChuNegType d)
g))
{-# INLINE parOChu #-}

-- | Left unitor @I ⊗ A → A@ for 'OChu'.
unitlOChu ::
  forall r (a :: Type).
  (ChuObject r a) =>
  OChu r (ChuOTensor r (ChuOUnit r) a) a
unitlOChu :: forall r a. ChuObject r a => OChu r (ChuOTensor r (ChuOUnit r) a) a
unitlOChu = Chu (,) r (->) (ChuOTensor r (ChuOUnit r) a) a
-> OChu r (ChuOTensor r (ChuOUnit r) a) a
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r (ChuOUnit r) a))
  (ChuNegType (ChuOTensor r (ChuOUnit r) a))
  (ChuPosType a)
  (ChuNegType a)
-> Chu (,) r (->) (ChuOTensor r (ChuOUnit r) a) a
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuMorphism
     (,)
     r
     (->)
     ((), ChuPosType a)
     (ChuTensorNeg () r (ChuPosType a) (ChuNegType a))
     (ChuPosType a)
     (ChuNegType a)
forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) ((), a) (ChuTensorNeg () r a b) a b
leftUnitorChu (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)))
{-# INLINE unitlOChu #-}

-- | Inverse left unitor @A → I ⊗ A@ for 'OChu'.
unitlOChu' ::
  forall r (a :: Type).
  (ChuObject r a) =>
  OChu r a (ChuOTensor r (ChuOUnit r) a)
unitlOChu' :: forall r a. ChuObject r a => OChu r a (ChuOTensor r (ChuOUnit r) a)
unitlOChu' = Chu (,) r (->) a (ChuOTensor r (ChuOUnit r) a)
-> OChu r a (ChuOTensor r (ChuOUnit r) a)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuOTensor r (ChuOUnit r) a))
  (ChuNegType (ChuOTensor r (ChuOUnit r) a))
-> Chu (,) r (->) a (ChuOTensor r (ChuOUnit r) a)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a)
     (ChuNegType a)
     ((), ChuPosType a)
     (ChuTensorNeg () r (ChuPosType a) (ChuNegType a))
forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) a b ((), a) (ChuTensorNeg () r a b)
leftUnitorChuInv (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)))
{-# INLINE unitlOChu' #-}

-- | Right unitor @A ⊗ I → A@ for 'OChu'.
unitrOChu ::
  forall r (a :: Type).
  (ChuObject r a) =>
  OChu r (ChuOTensor r a (ChuOUnit r)) a
unitrOChu :: forall r a. ChuObject r a => OChu r (ChuOTensor r a (ChuOUnit r)) a
unitrOChu = Chu (,) r (->) (ChuOTensor r a (ChuOUnit r)) a
-> OChu r (ChuOTensor r a (ChuOUnit r)) a
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a (ChuOUnit r)))
  (ChuNegType (ChuOTensor r a (ChuOUnit r)))
  (ChuPosType a)
  (ChuNegType a)
-> Chu (,) r (->) (ChuOTensor r a (ChuOUnit r)) a
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a, ())
     (ChuTensorNeg (ChuPosType a) (ChuNegType a) () r)
     (ChuPosType a)
     (ChuNegType a)
forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) (a, ()) (ChuTensorNeg a b () r) a b
rightUnitorChu (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)))
{-# INLINE unitrOChu #-}

-- | Inverse right unitor @A → A ⊗ I@ for 'OChu'.
unitrOChu' ::
  forall r (a :: Type).
  (ChuObject r a) =>
  OChu r a (ChuOTensor r a (ChuOUnit r))
unitrOChu' :: forall r a. ChuObject r a => OChu r a (ChuOTensor r a (ChuOUnit r))
unitrOChu' = Chu (,) r (->) a (ChuOTensor r a (ChuOUnit r))
-> OChu r a (ChuOTensor r a (ChuOUnit r))
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuOTensor r a (ChuOUnit r)))
  (ChuNegType (ChuOTensor r a (ChuOUnit r)))
-> Chu (,) r (->) a (ChuOTensor r a (ChuOUnit r))
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a)
     (ChuNegType a)
     (ChuPosType a, ())
     (ChuTensorNeg (ChuPosType a) (ChuNegType a) () r)
forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) a b (a, ()) (ChuTensorNeg a b () r)
rightUnitorChuInv (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)))
{-# INLINE unitrOChu' #-}

-- | Symmetric braiding @A ⊗ B → B ⊗ A@ for 'OChu'.
swapOChu ::
  forall r (a :: Type) (b :: Type).
  OChu r (ChuOTensor r a b) (ChuOTensor r b a)
swapOChu :: forall r a b. OChu r (ChuOTensor r a b) (ChuOTensor r b a)
swapOChu = Chu (,) r (->) (ChuOTensor r a b) (ChuOTensor r b a)
-> OChu r (ChuOTensor r a b) (ChuOTensor r b a)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a b))
  (ChuNegType (ChuOTensor r a b))
  (ChuPosType (ChuOTensor r b a))
  (ChuNegType (ChuOTensor r b a))
-> Chu (,) r (->) (ChuOTensor r a b) (ChuOTensor r b a)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (forall r a b.
(ChuPosType (ChuOTensor r a b) ~ (ChuPosType a, ChuPosType b),
 ChuNegType (ChuOTensor r a b)
 ~ ChuTensorNeg
     (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b),
 ChuPosType (ChuOTensor r b a) ~ (ChuPosType b, ChuPosType a),
 ChuNegType (ChuOTensor r b a)
 ~ ChuTensorNeg
     (ChuPosType b) (ChuNegType b) (ChuPosType a) (ChuNegType a)) =>
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a b))
  (ChuNegType (ChuOTensor r a b))
  (ChuPosType (ChuOTensor r b a))
  (ChuNegType (ChuOTensor r b a))
swapChu @r @a @b))
{-# INLINE swapOChu #-}

-- | Monoidal structure on the object-level Chu tensor.
--
-- 'assoc' / 'assoc'' / 'slide' are the Set-level maps 'assocChu',
-- 'assocChuInv', and 'slideChu'.  The pentagon is checked on 'ChuTwo'
-- by finite enumeration in @circuits-axioma@.
instance (Eq r) => Channel (ChuOTensor r) (OChu r) where
  assoc :: forall a b c.
OChu
  r
  (ChuOTensor r (ChuOTensor r a b) c)
  (ChuOTensor r a (ChuOTensor r b c))
assoc = Chu
  (,)
  r
  (->)
  (ChuOTensor r (ChuOTensor r a b) c)
  (ChuOTensor r a (ChuOTensor r b c))
-> OChu
     r
     (ChuOTensor r (ChuOTensor r a b) c)
     (ChuOTensor r a (ChuOTensor r b c))
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r (ChuOTensor r a b) c))
  (ChuNegType (ChuOTensor r (ChuOTensor r a b) c))
  (ChuPosType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuNegType (ChuOTensor r a (ChuOTensor r b c)))
-> Chu
     (,)
     r
     (->)
     (ChuOTensor r (ChuOTensor r a b) c)
     (ChuOTensor r a (ChuOTensor r b c))
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu ChuMorphism
  (,)
  r
  (->)
  ((ChuPosType a, ChuPosType b), ChuPosType c)
  (ChuTensorNeg
     (ChuPosType a, ChuPosType b)
     (ChuTensorNeg
        (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
     (ChuPosType c)
     (ChuNegType c))
  (ChuPosType a, (ChuPosType b, ChuPosType c))
  (ChuTensorNeg
     (ChuPosType a)
     (ChuNegType a)
     (ChuPosType b, ChuPosType c)
     (ChuTensorNeg
        (ChuPosType b) (ChuNegType b) (ChuPosType c) (ChuNegType c)))
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r (ChuOTensor r a b) c))
  (ChuNegType (ChuOTensor r (ChuOTensor r a b) c))
  (ChuPosType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuNegType (ChuOTensor r a (ChuOTensor r b c)))
forall {k} (r :: k) a c e b d f.
ChuMorphism
  (,)
  r
  (->)
  ((a, c), e)
  (ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f)
  (a, (c, e))
  (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
assocChu)
  assoc' :: forall a b c.
OChu
  r
  (ChuOTensor r a (ChuOTensor r b c))
  (ChuOTensor r (ChuOTensor r a b) c)
assoc' = Chu
  (,)
  r
  (->)
  (ChuOTensor r a (ChuOTensor r b c))
  (ChuOTensor r (ChuOTensor r a b) c)
-> OChu
     r
     (ChuOTensor r a (ChuOTensor r b c))
     (ChuOTensor r (ChuOTensor r a b) c)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuNegType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuPosType (ChuOTensor r (ChuOTensor r a b) c))
  (ChuNegType (ChuOTensor r (ChuOTensor r a b) c))
-> Chu
     (,)
     r
     (->)
     (ChuOTensor r a (ChuOTensor r b c))
     (ChuOTensor r (ChuOTensor r a b) c)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a, (ChuPosType b, ChuPosType c))
  (ChuTensorNeg
     (ChuPosType a)
     (ChuNegType a)
     (ChuPosType b, ChuPosType c)
     (ChuTensorNeg
        (ChuPosType b) (ChuNegType b) (ChuPosType c) (ChuNegType c)))
  ((ChuPosType a, ChuPosType b), ChuPosType c)
  (ChuTensorNeg
     (ChuPosType a, ChuPosType b)
     (ChuTensorNeg
        (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
     (ChuPosType c)
     (ChuNegType c))
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuNegType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuPosType (ChuOTensor r (ChuOTensor r a b) c))
  (ChuNegType (ChuOTensor r (ChuOTensor r a b) c))
forall {k} (r :: k) a c e b d f.
ChuMorphism
  (,)
  r
  (->)
  (a, (c, e))
  (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
  ((a, c), e)
  (ChuTensorNeg (a, c) (ChuTensorNeg a b c d) e f)
assocChuInv)
  slide :: forall a b c.
OChu
  r
  (ChuOTensor r a (ChuOTensor r b c))
  (ChuOTensor r b (ChuOTensor r a c))
slide = Chu
  (,)
  r
  (->)
  (ChuOTensor r a (ChuOTensor r b c))
  (ChuOTensor r b (ChuOTensor r a c))
-> OChu
     r
     (ChuOTensor r a (ChuOTensor r b c))
     (ChuOTensor r b (ChuOTensor r a c))
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuNegType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuPosType (ChuOTensor r b (ChuOTensor r a c)))
  (ChuNegType (ChuOTensor r b (ChuOTensor r a c)))
-> Chu
     (,)
     r
     (->)
     (ChuOTensor r a (ChuOTensor r b c))
     (ChuOTensor r b (ChuOTensor r a c))
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a, (ChuPosType b, ChuPosType c))
  (ChuTensorNeg
     (ChuPosType a)
     (ChuNegType a)
     (ChuPosType b, ChuPosType c)
     (ChuTensorNeg
        (ChuPosType b) (ChuNegType b) (ChuPosType c) (ChuNegType c)))
  (ChuPosType b, (ChuPosType a, ChuPosType c))
  (ChuTensorNeg
     (ChuPosType b)
     (ChuNegType b)
     (ChuPosType a, ChuPosType c)
     (ChuTensorNeg
        (ChuPosType a) (ChuNegType a) (ChuPosType c) (ChuNegType c)))
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuNegType (ChuOTensor r a (ChuOTensor r b c)))
  (ChuPosType (ChuOTensor r b (ChuOTensor r a c)))
  (ChuNegType (ChuOTensor r b (ChuOTensor r a c)))
forall {k} (r :: k) a c e b d f.
ChuMorphism
  (,)
  r
  (->)
  (a, (c, e))
  (ChuTensorNeg a b (c, e) (ChuTensorNeg c d e f))
  (c, (a, e))
  (ChuTensorNeg c d (a, e) (ChuTensorNeg a b e f))
slideChu)

-- | Double-negation unit @A → A⊥⊥@.
--
-- On carriers this is the identity: two braids restore @A⁺@ and @A⁻@, and
-- the pairing is @e . braid . braid = e@.  It is an isomorphism precisely
-- on separated-extensional objects.
dnUnitChu :: forall r a. OChu r a (ChuONeg r (ChuONeg r a))
dnUnitChu :: forall r a. OChu r a (ChuONeg r (ChuONeg r a))
dnUnitChu =
  Chu (,) r (->) a (ChuONeg r (ChuONeg r a))
-> OChu r a (ChuONeg r (ChuONeg r a))
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuONeg r (ChuONeg r a)))
  (ChuNegType (ChuONeg r (ChuONeg r a)))
-> Chu (,) r (->) a (ChuONeg r (ChuONeg r a))
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType a)
  (ChuNegType a)
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuONeg r (ChuONeg r a)))
  (ChuNegType (ChuONeg r (ChuONeg r a)))
forall {k} {k} {k} (arr :: k -> k -> *) (t :: k) (r :: k) (a :: k)
       (b :: k).
Category arr =>
ChuMorphism t r arr a b a b
idChu ::
            ChuMorphism
              (,)
              r
              (->)
              (ChuPosType a)
              (ChuNegType a)
              (ChuPosType (ChuONeg r (ChuONeg r a)))
              (ChuNegType (ChuONeg r (ChuONeg r a)))
        )
    )

-- | Double-negation counit @A⊥⊥ → A@.
dnCounitChu :: forall r a. OChu r (ChuONeg r (ChuONeg r a)) a
dnCounitChu :: forall r a. OChu r (ChuONeg r (ChuONeg r a)) a
dnCounitChu =
  Chu (,) r (->) (ChuONeg r (ChuONeg r a)) a
-> OChu r (ChuONeg r (ChuONeg r a)) a
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuONeg r (ChuONeg r a)))
  (ChuNegType (ChuONeg r (ChuONeg r a)))
  (ChuPosType a)
  (ChuNegType a)
-> Chu (,) r (->) (ChuONeg r (ChuONeg r a)) a
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType a)
  (ChuNegType a)
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuONeg r (ChuONeg r a)))
  (ChuNegType (ChuONeg r (ChuONeg r a)))
  (ChuPosType a)
  (ChuNegType a)
forall {k} {k} {k} (arr :: k -> k -> *) (t :: k) (r :: k) (a :: k)
       (b :: k).
Category arr =>
ChuMorphism t r arr a b a b
idChu ::
            ChuMorphism
              (,)
              r
              (->)
              (ChuPosType (ChuONeg r (ChuONeg r a)))
              (ChuNegType (ChuONeg r (ChuONeg r a)))
              (ChuPosType a)
              (ChuNegType a)
        )
    )

-- | Object-level linear implication @A ⊸ B = A⊥ ⅋ B@.
data ChuOLolli (r :: Type) a b = ChuOLolli

instance
  (Eq r, ChuObject r a, ChuObject r b) =>
  ChuObject r (ChuOLolli r a b)
  where
  chuObject :: ChuObj
  (,)
  r
  (->)
  (ChuPosType (ChuOLolli r a b))
  (ChuNegType (ChuOLolli r a b))
chuObject = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuObj (,) r (->) (ChuPosType b) (ChuNegType b)
-> ChuObj
     (,)
     r
     (->)
     (ChuParPos
        (ChuNegType a) (ChuPosType a) (ChuPosType b) (ChuNegType b))
     (ChuPosType a, ChuNegType b)
forall r a b c d.
Eq r =>
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuObj (,) r (->) (ChuParPos b a c d) (a, d)
lolliChuObj (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a) (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @b)
  chuPosAll :: [ChuPosType (ChuOLolli r a b)]
chuPosAll = [Char]
-> [ChuParPos
      (ChuNegType a) (ChuPosType a) (ChuPosType b) (ChuNegType b)]
forall a. HasCallStack => [Char] -> a
error [Char]
"chuPosAll: linear implication positive carrier is not enumerated"
  chuNegAll :: [ChuNegType (ChuOLolli r a b)]
chuNegAll = [ChuPosType a] -> [ChuNegType b] -> [(ChuPosType a, ChuNegType b)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian (forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @a) (forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @b)

instance (Eq r, ChuSeparated r a, ChuSeparated r b) => ChuSeparated r (ChuOLolli r a b)

instance (Eq r, ChuExtensional r a, ChuExtensional r b) => ChuExtensional r (ChuOLolli r a b)

-- | Object-level additive conjunction @A & B@.
--
-- 'ChuSeparated' is available whenever both summands are separated.
-- 'ChuExtensional' is guarded by 'ChuPosNonEmpty': when one summand has an
-- empty positive carrier (e.g. @A & 0@), distinct negative injections cannot
-- be separated, so the instance is not asserted.
data ChuOWith (r :: Type) a b = ChuOWith

instance
  (ChuObject r a, ChuObject r b) =>
  ChuObject r (ChuOWith r a b)
  where
  chuObject :: ChuObj
  (,)
  r
  (->)
  (ChuPosType (ChuOWith r a b))
  (ChuNegType (ChuOWith r a b))
chuObject = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuObj (,) r (->) (ChuPosType b) (ChuNegType b)
-> ChuObj
     (,)
     r
     (->)
     (ChuPosType a, ChuPosType b)
     (Either (ChuNegType a) (ChuNegType b))
forall r a b c d.
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d -> ChuObj (,) r (->) (a, c) (Either b d)
withChuObj (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a) (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @b)
  chuPosAll :: [ChuPosType (ChuOWith r a b)]
chuPosAll = [ChuPosType a] -> [ChuPosType b] -> [(ChuPosType a, ChuPosType b)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian (forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @a) (forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @b)
  chuNegAll :: [ChuNegType (ChuOWith r a b)]
chuNegAll = (ChuNegType a -> Either (ChuNegType a) (ChuNegType b))
-> [ChuNegType a] -> [Either (ChuNegType a) (ChuNegType b)]
forall a b. (a -> b) -> [a] -> [b]
map ChuNegType a -> Either (ChuNegType a) (ChuNegType b)
forall a b. a -> Either a b
Left (forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @a) [Either (ChuNegType a) (ChuNegType b)]
-> [Either (ChuNegType a) (ChuNegType b)]
-> [Either (ChuNegType a) (ChuNegType b)]
forall a. [a] -> [a] -> [a]
++ (ChuNegType b -> Either (ChuNegType a) (ChuNegType b))
-> [ChuNegType b] -> [Either (ChuNegType a) (ChuNegType b)]
forall a b. (a -> b) -> [a] -> [b]
map ChuNegType b -> Either (ChuNegType a) (ChuNegType b)
forall a b. b -> Either a b
Right (forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @b)

instance (ChuSeparated r a, ChuSeparated r b) => ChuSeparated r (ChuOWith r a b)

instance
  ( ChuExtensional r a,
    ChuExtensional r b,
    ChuPosNonEmpty a ~ 'True,
    ChuPosNonEmpty b ~ 'True
  ) =>
  ChuExtensional r (ChuOWith r a b)

-- | Object-level additive disjunction @A ⊕ B@.
--
-- 'ChuExtensional' is available whenever both summands are extensional.
-- 'ChuSeparated' is guarded by 'ChuNegNonEmpty': when one summand has an
-- empty negative carrier (e.g. @⊤ ⊕ B@), distinct positive injections cannot
-- be separated, so the instance is not asserted.
data ChuOPlus (r :: Type) a b = ChuOPlus

instance
  (ChuObject r a, ChuObject r b) =>
  ChuObject r (ChuOPlus r a b)
  where
  chuObject :: ChuObj
  (,)
  r
  (->)
  (ChuPosType (ChuOPlus r a b))
  (ChuNegType (ChuOPlus r a b))
chuObject = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuObj (,) r (->) (ChuPosType b) (ChuNegType b)
-> ChuObj
     (,)
     r
     (->)
     (Either (ChuPosType a) (ChuPosType b))
     (ChuNegType a, ChuNegType b)
forall r a b c d.
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d -> ChuObj (,) r (->) (Either a c) (b, d)
oplusChuObj (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a) (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @b)
  chuPosAll :: [ChuPosType (ChuOPlus r a b)]
chuPosAll = (ChuPosType a -> Either (ChuPosType a) (ChuPosType b))
-> [ChuPosType a] -> [Either (ChuPosType a) (ChuPosType b)]
forall a b. (a -> b) -> [a] -> [b]
map ChuPosType a -> Either (ChuPosType a) (ChuPosType b)
forall a b. a -> Either a b
Left (forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @a) [Either (ChuPosType a) (ChuPosType b)]
-> [Either (ChuPosType a) (ChuPosType b)]
-> [Either (ChuPosType a) (ChuPosType b)]
forall a. [a] -> [a] -> [a]
++ (ChuPosType b -> Either (ChuPosType a) (ChuPosType b))
-> [ChuPosType b] -> [Either (ChuPosType a) (ChuPosType b)]
forall a b. (a -> b) -> [a] -> [b]
map ChuPosType b -> Either (ChuPosType a) (ChuPosType b)
forall a b. b -> Either a b
Right (forall r a. ChuObject r a => [ChuPosType a]
chuPosAll @r @b)
  chuNegAll :: [ChuNegType (ChuOPlus r a b)]
chuNegAll = [ChuNegType a] -> [ChuNegType b] -> [(ChuNegType a, ChuNegType b)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian (forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @a) (forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @b)

instance
  ( ChuSeparated r a,
    ChuSeparated r b,
    ChuNegNonEmpty a ~ 'True,
    ChuNegNonEmpty b ~ 'True
  ) =>
  ChuSeparated r (ChuOPlus r a b)

instance (ChuExtensional r a, ChuExtensional r b) => ChuExtensional r (ChuOPlus r a b)

-- | Object-level multiplicative disjunction @A ⅋ B@.
--
-- Positive carrier is the set of 'ChuParPos' witnesses; negative carrier is
-- the product @A⁻ × B⁻@.  This is the real par, distinct from the additive
-- disjunction 'ChuOPlus'.
data ChuOPar (r :: Type) a b = ChuOPar

instance
  (Eq r, ChuObject r a, ChuObject r b) =>
  ChuObject r (ChuOPar r a b)
  where
  chuObject :: ChuObj
  (,)
  r
  (->)
  (ChuPosType (ChuOPar r a b))
  (ChuNegType (ChuOPar r a b))
chuObject = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuObj (,) r (->) (ChuPosType b) (ChuNegType b)
-> ChuObj
     (,)
     r
     (->)
     (ChuParPos
        (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
     (ChuNegType a, ChuNegType b)
forall r a b c d.
Eq r =>
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuObj (,) r (->) (ChuParPos a b c d) (b, d)
parChuObj (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a) (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @b)
  chuPosAll :: [ChuPosType (ChuOPar r a b)]
chuPosAll = [Char]
-> [ChuParPos
      (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)]
forall a. HasCallStack => [Char] -> a
error [Char]
"chuPosAll: par positive carrier is not enumerated"
  chuNegAll :: [ChuNegType (ChuOPar r a b)]
chuNegAll = [ChuNegType a] -> [ChuNegType b] -> [(ChuNegType a, ChuNegType b)]
forall a b. [a] -> [b] -> [(a, b)]
cartesian (forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @a) (forall r a. ChuObject r a => [ChuNegType a]
chuNegAll @r @b)

instance (Eq r, ChuSeparated r a, ChuSeparated r b) => ChuSeparated r (ChuOPar r a b)

instance (Eq r, ChuExtensional r a, ChuExtensional r b) => ChuExtensional r (ChuOPar r a b)

-- | Object-level additive unit @⊤@.
data ChuOTop (r :: Type) = ChuOTop

instance ChuObject r (ChuOTop r) where
  chuObject :: ChuObj (,) r (->) (ChuPosType (ChuOTop r)) (ChuNegType (ChuOTop r))
chuObject = ChuObj (,) r (->) () Void
ChuObj (,) r (->) (ChuPosType (ChuOTop r)) (ChuNegType (ChuOTop r))
forall r. ChuObj (,) r (->) () Void
topChuObj
  chuPosAll :: [ChuPosType (ChuOTop r)]
chuPosAll = [()]
  chuNegAll :: [ChuNegType (ChuOTop r)]
chuNegAll = []

instance ChuSeparated r (ChuOTop r)

instance ChuExtensional r (ChuOTop r)

-- | Object-level additive zero @0@.
data ChuOZero (r :: Type) = ChuOZero

instance ChuObject r (ChuOZero r) where
  chuObject :: ChuObj
  (,) r (->) (ChuPosType (ChuOZero r)) (ChuNegType (ChuOZero r))
chuObject = ChuObj (,) r (->) Void ()
ChuObj
  (,) r (->) (ChuPosType (ChuOZero r)) (ChuNegType (ChuOZero r))
forall r. ChuObj (,) r (->) Void ()
zeroChuObj
  chuPosAll :: [ChuPosType (ChuOZero r)]
chuPosAll = []
  chuNegAll :: [ChuNegType (ChuOZero r)]
chuNegAll = [()]

instance ChuSeparated r (ChuOZero r)

instance ChuExtensional r (ChuOZero r)

-- | The par unit is the dual of the tensor unit: @⊥ = I⊥@.
type instance Bot (ChuOPar r) = ChuONeg r (ChuOUnit r)

-- | Par structure on the object-indexed Chu category.
--
-- The par product of objects is 'ChuOPar'; the structural morphisms are the
-- Set-level par maps already defined for 'Chu' morphisms.

-- | Parallel composition for the par product on 'OChu'.
parPOChu ::
  forall r (a :: Type) (b :: Type) (c :: Type) (d :: Type).
  OChu r a b ->
  OChu r c d ->
  OChu r (ChuOPar r a c) (ChuOPar r b d)
parPOChu :: forall r a b c d.
OChu r a b -> OChu r c d -> OChu r (ChuOPar r a c) (ChuOPar r b d)
parPOChu (OChu (Chu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType b)
  (ChuNegType b)
f)) (OChu (Chu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType c)
  (ChuNegType c)
  (ChuPosType d)
  (ChuNegType d)
g)) = Chu (,) r (->) (ChuOPar r a c) (ChuOPar r b d)
-> OChu r (ChuOPar r a c) (ChuOPar r b d)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOPar r a c))
  (ChuNegType (ChuOPar r a c))
  (ChuPosType (ChuOPar r b d))
  (ChuNegType (ChuOPar r b d))
-> Chu (,) r (->) (ChuOPar r a c) (ChuOPar r b d)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType b)
  (ChuNegType b)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType c)
     (ChuNegType c)
     (ChuPosType d)
     (ChuNegType d)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuParPos
        (ChuPosType a) (ChuNegType a) (ChuPosType c) (ChuNegType c))
     (ChuNegType a, ChuNegType c)
     (ChuParPos
        (ChuPosType b) (ChuNegType b) (ChuPosType d) (ChuNegType d))
     (ChuNegType b, ChuNegType d)
forall {k} (r :: k) a b c d e f g h.
ChuMorphism (,) r (->) a b c d
-> ChuMorphism (,) r (->) e f g h
-> ChuMorphism
     (,) r (->) (ChuParPos a b e f) (b, f) (ChuParPos c d g h) (d, h)
parChu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType b)
  (ChuNegType b)
f ChuMorphism
  (,)
  r
  (->)
  (ChuPosType c)
  (ChuNegType c)
  (ChuPosType d)
  (ChuNegType d)
g))
{-# INLINE parPOChu #-}

-- | Left unitor @⊥ ⅋ A → A@ for 'OChu'.
unitlPOChu ::
  forall r (a :: Type).
  OChu r (ChuOPar r (Bot (ChuOPar r)) a) a
unitlPOChu :: forall r a. OChu r (ChuOPar r (Bot (ChuOPar r)) a) a
unitlPOChu = Chu (,) r (->) (ChuOPar r (ChuONeg r (ChuOUnit r)) a) a
-> OChu r (ChuOPar r (ChuONeg r (ChuOUnit r)) a) a
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOPar r (ChuONeg r (ChuOUnit r)) a))
  (ChuNegType (ChuOPar r (ChuONeg r (ChuOUnit r)) a))
  (ChuPosType a)
  (ChuNegType a)
-> Chu (,) r (->) (ChuOPar r (ChuONeg r (ChuOUnit r)) a) a
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu ChuMorphism
  (,)
  r
  (->)
  (ChuParPos r () (ChuPosType a) (ChuNegType a))
  ((), ChuNegType a)
  (ChuPosType a)
  (ChuNegType a)
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOPar r (ChuONeg r (ChuOUnit r)) a))
  (ChuNegType (ChuOPar r (ChuONeg r (ChuOUnit r)) a))
  (ChuPosType a)
  (ChuNegType a)
forall r p n.
ChuMorphism (,) r (->) (ChuParPos r () p n) ((), n) p n
leftUnitorParChu)
{-# INLINE unitlPOChu #-}

-- | Inverse left unitor @A → ⊥ ⅋ A@ for 'OChu'.
unitlPOChu' ::
  forall r (a :: Type).
  (ChuObject r a) =>
  OChu r a (ChuOPar r (Bot (ChuOPar r)) a)
unitlPOChu' :: forall r a.
ChuObject r a =>
OChu r a (ChuOPar r (Bot (ChuOPar r)) a)
unitlPOChu' = Chu (,) r (->) a (ChuOPar r (ChuONeg r (ChuOUnit r)) a)
-> OChu r a (ChuOPar r (ChuONeg r (ChuOUnit r)) a)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuOPar r (ChuONeg r (ChuOUnit r)) a))
  (ChuNegType (ChuOPar r (ChuONeg r (ChuOUnit r)) a))
-> Chu (,) r (->) a (ChuOPar r (ChuONeg r (ChuOUnit r)) a)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a)
     (ChuNegType a)
     (ChuParPos r () (ChuPosType a) (ChuNegType a))
     ((), ChuNegType a)
forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) a b (ChuParPos r () a b) ((), b)
leftUnitorParChuInv (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)))
{-# INLINE unitlPOChu' #-}

-- | Right unitor @A ⅋ ⊥ → A@ for 'OChu'.
unitrPOChu ::
  forall r (a :: Type).
  OChu r (ChuOPar r a (Bot (ChuOPar r))) a
unitrPOChu :: forall r a. OChu r (ChuOPar r a (Bot (ChuOPar r))) a
unitrPOChu = Chu (,) r (->) (ChuOPar r a (ChuONeg r (ChuOUnit r))) a
-> OChu r (ChuOPar r a (ChuONeg r (ChuOUnit r))) a
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOPar r a (ChuONeg r (ChuOUnit r))))
  (ChuNegType (ChuOPar r a (ChuONeg r (ChuOUnit r))))
  (ChuPosType a)
  (ChuNegType a)
-> Chu (,) r (->) (ChuOPar r a (ChuONeg r (ChuOUnit r))) a
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu ChuMorphism
  (,)
  r
  (->)
  (ChuParPos (ChuPosType a) (ChuNegType a) r ())
  (ChuNegType a, ())
  (ChuPosType a)
  (ChuNegType a)
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOPar r a (ChuONeg r (ChuOUnit r))))
  (ChuNegType (ChuOPar r a (ChuONeg r (ChuOUnit r))))
  (ChuPosType a)
  (ChuNegType a)
forall r p n.
ChuMorphism (,) r (->) (ChuParPos p n r ()) (n, ()) p n
rightUnitorParChu)
{-# INLINE unitrPOChu #-}

-- | Inverse right unitor @A → A ⅋ ⊥@ for 'OChu'.
unitrPOChu' ::
  forall r (a :: Type).
  (ChuObject r a) =>
  OChu r a (ChuOPar r a (Bot (ChuOPar r)))
unitrPOChu' :: forall r a.
ChuObject r a =>
OChu r a (ChuOPar r a (Bot (ChuOPar r)))
unitrPOChu' = Chu (,) r (->) a (ChuOPar r a (ChuONeg r (ChuOUnit r)))
-> OChu r a (ChuOPar r a (ChuONeg r (ChuOUnit r)))
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuOPar r a (ChuONeg r (ChuOUnit r))))
  (ChuNegType (ChuOPar r a (ChuONeg r (ChuOUnit r))))
-> Chu (,) r (->) a (ChuOPar r a (ChuONeg r (ChuOUnit r)))
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a)
     (ChuNegType a)
     (ChuParPos (ChuPosType a) (ChuNegType a) r ())
     (ChuNegType a, ())
forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) a b (ChuParPos a b r ()) (b, ())
rightUnitorParChuInv (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)))
{-# INLINE unitrPOChu' #-}

-- | Curry @(A ⊗ B → C) → (A → B ⊸ C)@ over @Set@.
curryChu ::
  ChuMorphism
    (,)
    r
    (->)
    (a, c)
    (ChuTensorNeg a b c d)
    e
    f ->
  ChuMorphism
    (,)
    r
    (->)
    a
    b
    (ChuParPos d c e f)
    (c, f)
curryChu :: forall {k} (r :: k) a c b d e f.
ChuMorphism (,) r (->) (a, c) (ChuTensorNeg a b c d) e f
-> ChuMorphism (,) r (->) a b (ChuParPos d c e f) (c, f)
curryChu (ChuMorphism (a, c) -> e
fPos f -> ChuTensorNeg a b c d
fNeg) =
  (a -> ChuParPos d c e f)
-> ((c, f) -> b)
-> ChuMorphism (,) r (->) a b (ChuParPos d c e f) (c, f)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\a
x -> (c -> e) -> (f -> d) -> ChuParPos d c e f
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos (\c
y -> (a, c) -> e
fPos (a
x, c
y)) (\f
z -> ChuTensorNeg a b c d -> a -> d
forall a b c d. ChuTensorNeg a b c d -> a -> d
ctnForward (f -> ChuTensorNeg a b c d
fNeg f
z) a
x))
    (\(c
y, f
z) -> ChuTensorNeg a b c d -> c -> b
forall a b c d. ChuTensorNeg a b c d -> c -> b
ctnBackward (f -> ChuTensorNeg a b c d
fNeg f
z) c
y)
{-# INLINE curryChu #-}

-- | Uncurry @(A → B ⊸ C) → (A ⊗ B → C)@ over @Set@.
uncurryChu ::
  ChuMorphism
    (,)
    r
    (->)
    a
    b
    (ChuParPos d c e f)
    (c, f) ->
  ChuMorphism
    (,)
    r
    (->)
    (a, c)
    (ChuTensorNeg a b c d)
    e
    f
uncurryChu :: forall {k} (r :: k) a b d c e f.
ChuMorphism (,) r (->) a b (ChuParPos d c e f) (c, f)
-> ChuMorphism (,) r (->) (a, c) (ChuTensorNeg a b c d) e f
uncurryChu (ChuMorphism a -> ChuParPos d c e f
gPos (c, f) -> b
gNeg) =
  ((a, c) -> e)
-> (f -> ChuTensorNeg a b c d)
-> ChuMorphism (,) r (->) (a, c) (ChuTensorNeg a b c d) e f
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\(a
x, c
y) -> ChuParPos d c e f -> c -> e
forall a b c d. ChuParPos a b c d -> b -> c
cppForward (a -> ChuParPos d c e f
gPos a
x) c
y)
    (\f
z -> (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (\a
x -> ChuParPos d c e f -> f -> d
forall a b c d. ChuParPos a b c d -> d -> a
cppBackward (a -> ChuParPos d c e f
gPos a
x) f
z) (\c
y -> (c, f) -> b
gNeg (c
y, f
z)))
{-# INLINE uncurryChu #-}

-- | Evaluation counit @A ⊗ (A ⊸ B) → B@ for 'OChu'.
evalOChu ::
  forall r (a :: Type) (b :: Type).
  (ChuObject r a, ChuObject r b) =>
  OChu r (ChuOTensor r a (ChuOLolli r a b)) b
evalOChu :: forall r a b.
(ChuObject r a, ChuObject r b) =>
OChu r (ChuOTensor r a (ChuOLolli r a b)) b
evalOChu = Chu (,) r (->) (ChuOTensor r a (ChuOLolli r a b)) b
-> OChu r (ChuOTensor r a (ChuOLolli r a b)) b
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a (ChuOLolli r a b)))
  (ChuNegType (ChuOTensor r a (ChuOLolli r a b)))
  (ChuPosType b)
  (ChuNegType b)
-> Chu (,) r (->) (ChuOTensor r a (ChuOLolli r a b)) b
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuObj (,) r (->) (ChuPosType b) (ChuNegType b)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a,
      ChuParPos
        (ChuNegType a) (ChuPosType a) (ChuPosType b) (ChuNegType b))
     (ChuTensorNeg
        (ChuPosType a)
        (ChuNegType a)
        (ChuParPos
           (ChuNegType a) (ChuPosType a) (ChuPosType b) (ChuNegType b))
        (ChuPosType a, ChuNegType b))
     (ChuPosType b)
     (ChuNegType b)
forall r a b c d.
ChuObj (,) r (->) a b
-> ChuObj (,) r (->) c d
-> ChuMorphism
     (,)
     r
     (->)
     (a, ChuParPos b a c d)
     (ChuTensorNeg a b (ChuParPos b a c d) (a, d))
     c
     d
evalChu (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a) (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @b)))
{-# INLINE evalOChu #-}

-- | Curry @(A ⊗ B → C) → (A → B ⊸ C)@ for 'OChu'.
curryOChu ::
  forall r (a :: Type) (b :: Type) (c :: Type).
  OChu r (ChuOTensor r a b) c ->
  OChu r a (ChuOLolli r b c)
curryOChu :: forall r a b c.
OChu r (ChuOTensor r a b) c -> OChu r a (ChuOLolli r b c)
curryOChu (OChu (Chu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a b))
  (ChuNegType (ChuOTensor r a b))
  (ChuPosType c)
  (ChuNegType c)
f)) = Chu (,) r (->) a (ChuOLolli r b c) -> OChu r a (ChuOLolli r b c)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuOLolli r b c))
  (ChuNegType (ChuOLolli r b c))
-> Chu (,) r (->) a (ChuOLolli r b c)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a, ChuPosType b)
  (ChuTensorNeg
     (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
  (ChuPosType c)
  (ChuNegType c)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a)
     (ChuNegType a)
     (ChuParPos
        (ChuNegType b) (ChuPosType b) (ChuPosType c) (ChuNegType c))
     (ChuPosType b, ChuNegType c)
forall {k} (r :: k) a c b d e f.
ChuMorphism (,) r (->) (a, c) (ChuTensorNeg a b c d) e f
-> ChuMorphism (,) r (->) a b (ChuParPos d c e f) (c, f)
curryChu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a, ChuPosType b)
  (ChuTensorNeg
     (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
  (ChuPosType c)
  (ChuNegType c)
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a b))
  (ChuNegType (ChuOTensor r a b))
  (ChuPosType c)
  (ChuNegType c)
f))
{-# INLINE curryOChu #-}

-- | Uncurry @(A → B ⊸ C) → (A ⊗ B → C)@ for 'OChu'.
uncurryOChu ::
  forall r (a :: Type) (b :: Type) (c :: Type).
  OChu r a (ChuOLolli r b c) ->
  OChu r (ChuOTensor r a b) c
uncurryOChu :: forall r a b c.
OChu r a (ChuOLolli r b c) -> OChu r (ChuOTensor r a b) c
uncurryOChu (OChu (Chu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuOLolli r b c))
  (ChuNegType (ChuOLolli r b c))
g)) =
  Chu (,) r (->) (ChuOTensor r a b) c -> OChu r (ChuOTensor r a b) c
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r a b))
  (ChuNegType (ChuOTensor r a b))
  (ChuPosType c)
  (ChuNegType c)
-> Chu (,) r (->) (ChuOTensor r a b) c
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuParPos
     (ChuNegType b) (ChuPosType b) (ChuPosType c) (ChuNegType c))
  (ChuPosType b, ChuNegType c)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a, ChuPosType b)
     (ChuTensorNeg
        (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
     (ChuPosType c)
     (ChuNegType c)
forall {k} (r :: k) a b d c e f.
ChuMorphism (,) r (->) a b (ChuParPos d c e f) (c, f)
-> ChuMorphism (,) r (->) (a, c) (ChuTensorNeg a b c d) e f
uncurryChu ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuParPos
     (ChuNegType b) (ChuPosType b) (ChuPosType c) (ChuNegType c))
  (ChuPosType b, ChuNegType c)
ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuOLolli r b c))
  (ChuNegType (ChuOLolli r b c))
g ::
            ChuMorphism
              (,)
              r
              (->)
              (ChuPosType a, ChuPosType b)
              (ChuTensorNeg (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b))
              (ChuPosType c)
              (ChuNegType c)
        )
    )
{-# INLINE uncurryOChu #-}

-- ===========================================================================
-- Exponentials: !A = (A⁺, A⁺ → r, eval), ?A = (!A⊥)⊥
-- ===========================================================================

-- | All functions from a finite domain to a finite codomain.
chuFunctionals :: (Eq a) => [a] -> [r] -> [a -> r]
chuFunctionals :: forall a b. Eq a => [a] -> [b] -> [a -> b]
chuFunctionals = [a] -> [r] -> [a -> r]
forall a b. Eq a => [a] -> [b] -> [a -> b]
functions

-- | Cofree cocommutative comonoid on a Set-based Chu object.
--
-- Positives are those of @A@; negatives are every functional @A⁺ → r@;
-- the pairing is evaluation.  Original negatives embed by Yoneda
-- @d ↦ \\a -> e(a, d)@, and constants @k ↦ const k@ supply discard.
bangChuObj :: ChuObj (,) r (->) a b -> ChuObj (,) r (->) a (a -> r)
bangChuObj :: forall r a b. ChuObj (,) r (->) a b -> ChuObj (,) r (->) a (a -> r)
bangChuObj ChuObj (,) r (->) a b
_ = ((a, a -> r) -> r) -> ChuObj (,) r (->) a (a -> r)
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj (\(a
x, a -> r
f) -> a -> r
f a
x)

-- | Free commutative monoid @?A = (!A⊥)⊥@.
--
-- Positives are the functionals @A⁻ → r@; negatives are those of @A@.
whyNotChuObj :: ChuObj (,) r (->) a b -> ChuObj (,) r (->) (b -> r) b
whyNotChuObj :: forall r a b. ChuObj (,) r (->) a b -> ChuObj (,) r (->) (b -> r) b
whyNotChuObj ChuObj (,) r (->) a b
a = ChuObj (,) r (->) b (b -> r) -> ChuObj (,) r (->) (b -> r) b
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (r :: k)
       (a :: k) (b :: k).
Action t arr =>
ChuObj t r arr a b -> ChuObj t r arr b a
negateChu (ChuObj (,) r (->) b a -> ChuObj (,) r (->) b (b -> r)
forall r a b. ChuObj (,) r (->) a b -> ChuObj (,) r (->) a (a -> r)
bangChuObj (ChuObj (,) r (->) a b -> ChuObj (,) r (->) b a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (r :: k)
       (a :: k) (b :: k).
Action t arr =>
ChuObj t r arr a b -> ChuObj t r arr b a
negateChu ChuObj (,) r (->) a b
a))

-- | Copy @!A → !A ⊗ !A@: diagonal on points, contraction on functionals.
copyBangChu ::
  ChuMorphism
    (,)
    r
    (->)
    a
    (a -> r)
    (a, a)
    (ChuTensorNeg a (a -> r) a (a -> r))
copyBangChu :: forall r a.
ChuMorphism
  (,) r (->) a (a -> r) (a, a) (ChuTensorNeg a (a -> r) a (a -> r))
copyBangChu =
  (a -> (a, a))
-> (ChuTensorNeg a (a -> r) a (a -> r) -> (a -> r))
-> ChuMorphism
     (,) r (->) a (a -> r) (a, a) (ChuTensorNeg a (a -> r) a (a -> r))
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\a
x -> (a
x, a
x))
    (\ChuTensorNeg a (a -> r) a (a -> r)
n a
x -> ChuTensorNeg a (a -> r) a (a -> r) -> a -> a -> r
forall a b c d. ChuTensorNeg a b c d -> c -> b
ctnBackward ChuTensorNeg a (a -> r) a (a -> r)
n a
x a
x)
{-# INLINE copyBangChu #-}

-- | Discard @!A → I@: the constant functionals.
discardBangChu ::
  ChuMorphism (,) r (->) a (a -> r) () r
discardBangChu :: forall r a. ChuMorphism (,) r (->) a (a -> r) () r
discardBangChu =
  (a -> ())
-> (r -> (a -> r)) -> ChuMorphism (,) r (->) a (a -> r) () r
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\a
_ -> ()) r -> (a -> r)
forall a b. a -> b -> a
const
{-# INLINE discardBangChu #-}

-- | Merge @!A ⊗ !A → !A@: the monoid operation on points, bilinearly
-- extended to functionals.
mergeBangChu ::
  (Monoid a) =>
  ChuMorphism
    (,)
    r
    (->)
    (a, a)
    (ChuTensorNeg a (a -> r) a (a -> r))
    a
    (a -> r)
mergeBangChu :: forall a r.
Monoid a =>
ChuMorphism
  (,) r (->) (a, a) (ChuTensorNeg a (a -> r) a (a -> r)) a (a -> r)
mergeBangChu =
  ((a, a) -> a)
-> ((a -> r) -> ChuTensorNeg a (a -> r) a (a -> r))
-> ChuMorphism
     (,) r (->) (a, a) (ChuTensorNeg a (a -> r) a (a -> r)) a (a -> r)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    ((a -> LolliT (,) (->) a a) -> (a, a) -> a
forall a b c. (a -> LolliT (,) (->) b c) -> (a, b) -> c
forall (t :: * -> * -> *) (arr :: * -> * -> *) a b c.
Lolli t arr =>
arr a (LolliT t arr b c) -> arr (t a b) c
uncurry a -> LolliT (,) (->) a a
a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>))
    (\a -> r
k -> (a -> a -> r)
-> (a -> a -> r) -> ChuTensorNeg a (a -> r) a (a -> r)
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (\a
x a
y -> a -> r
k (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y)) (\a
y a
x -> a -> r
k (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y)))
{-# INLINE mergeBangChu #-}

-- | Zero @I → !A@: the monoid unit as a point of @A⁺@.
zeroBangChu ::
  (Monoid a) =>
  ChuMorphism (,) r (->) () r a (a -> r)
zeroBangChu :: forall a r. Monoid a => ChuMorphism (,) r (->) () r a (a -> r)
zeroBangChu =
  (() -> a)
-> ((a -> r) -> r) -> ChuMorphism (,) r (->) () r a (a -> r)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\()
_ -> a
forall a. Monoid a => a
mempty) (\a -> r
k -> a -> r
k a
forall a. Monoid a => a
mempty)
{-# INLINE zeroBangChu #-}

-- | Dereliction @!A → A@: identity on points, Yoneda on negatives.
derelictChu ::
  ChuObj (,) r (->) a b ->
  ChuMorphism (,) r (->) a (a -> r) a b
derelictChu :: forall r a b.
ChuObj (,) r (->) a b -> ChuMorphism (,) r (->) a (a -> r) a b
derelictChu (ChuObj (a, b) -> r
e) =
  (a -> a)
-> (b -> (a -> r)) -> ChuMorphism (,) r (->) a (a -> r) a b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id (\b
d a
a -> (a, b) -> r
e (a
a, b
d))
{-# INLINE derelictChu #-}

-- | Introduction @A → ?A@: Yoneda on positives, identity on negatives.
introduceChu ::
  ChuObj (,) r (->) a b ->
  ChuMorphism (,) r (->) a b (b -> r) b
introduceChu :: forall r a b.
ChuObj (,) r (->) a b -> ChuMorphism (,) r (->) a b (b -> r) b
introduceChu (ChuObj (a, b) -> r
e) =
  (a -> (b -> r))
-> (b -> b) -> ChuMorphism (,) r (->) a b (b -> r) b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\a
x b
d -> (a, b) -> r
e (a
x, b
d)) b -> b
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
{-# INLINE introduceChu #-}

-- | Digging @!A → !!A@.
--
-- Over the Set-based ! of this module, @!!A@ is the same object as @!A@
-- (positive carrier @A⁺@, negative carrier @A⁺ → r@), so digging is the
-- identity. This is an observable fact about the model, not a stub.
digChu ::
  ChuMorphism (,) r (->) a (a -> r) a (a -> r)
digChu :: forall r a. ChuMorphism (,) r (->) a (a -> r) a (a -> r)
digChu = ChuMorphism (,) r (->) a (a -> r) a (a -> r)
forall {k} {k} {k} (arr :: k -> k -> *) (t :: k) (r :: k) (a :: k)
       (b :: k).
Category arr =>
ChuMorphism t r arr a b a b
idChu
{-# INLINE digChu #-}

-- | Promotion @!A ⊗ !B → !(A & B)@.
--
-- Forward is the identity on the shared positive carrier @(A⁺, B⁺)@.
-- Backward turns a bilinear element of @!A ⊗ !B@ into a functional on
-- @(A⁺, B⁺)@ using either leg of the bilinear condition.
promoteChu ::
  ChuMorphism
    (,)
    r
    (->)
    (a, c)
    (ChuTensorNeg a (a -> r) c (c -> r))
    (a, c)
    ((a, c) -> r)
promoteChu :: forall r a c.
ChuMorphism
  (,)
  r
  (->)
  (a, c)
  (ChuTensorNeg a (a -> r) c (c -> r))
  (a, c)
  ((a, c) -> r)
promoteChu =
  ((a, c) -> (a, c))
-> (((a, c) -> r) -> ChuTensorNeg a (a -> r) c (c -> r))
-> ChuMorphism
     (,)
     r
     (->)
     (a, c)
     (ChuTensorNeg a (a -> r) c (c -> r))
     (a, c)
     ((a, c) -> r)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (a, c) -> (a, c)
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
    (\(a, c) -> r
n -> (a -> c -> r)
-> (c -> a -> r) -> ChuTensorNeg a (a -> r) c (c -> r)
forall a b c d. (a -> d) -> (c -> b) -> ChuTensorNeg a b c d
ChuTensorNeg (\a
x c
y -> (a, c) -> r
n (a
x, c
y)) (\c
y a
x -> (a, c) -> r
n (a
x, c
y)))
{-# INLINE promoteChu #-}

-- | Zero @I → ?A@.  The unit functional is constantly 'sZero'.
--
-- This is not the ⅋-monoid unit (that is 'zeroWhyNotParChu' : @⊥ → ?A@).
zeroWhyNotChu ::
  (ChuSemiring r) =>
  ChuMorphism (,) r (->) () r (b -> r) b
zeroWhyNotChu :: forall r b. ChuSemiring r => ChuMorphism (,) r (->) () r (b -> r) b
zeroWhyNotChu =
  (() -> (b -> r))
-> (b -> r) -> ChuMorphism (,) r (->) () r (b -> r) b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\()
_ -> r -> b -> r
forall a b. a -> b -> a
const r
forall r. ChuSemiring r => r
sZero) (\b
_ -> r
forall r. ChuSemiring r => r
sZero)
{-# INLINE zeroWhyNotChu #-}

-- | Merge @?A ⅋ ?A → ?A@: the dual of 'copyBangChu'.
--
-- A par-positive is a pair of functionals @A⁻ → (A⁻ → r)@ satisfying
-- @g y x = f x y@.  Merge contracts the diagonal @\\x -> g x x@.
mergeWhyNotParChu ::
  ChuMorphism
    (,)
    r
    (->)
    (ChuParPos (b -> r) b (b -> r) b)
    (b, b)
    (b -> r)
    b
mergeWhyNotParChu :: forall r b.
ChuMorphism
  (,) r (->) (ChuParPos (b -> r) b (b -> r) b) (b, b) (b -> r) b
mergeWhyNotParChu =
  (ChuParPos (b -> r) b (b -> r) b -> (b -> r))
-> (b -> (b, b))
-> ChuMorphism
     (,) r (->) (ChuParPos (b -> r) b (b -> r) b) (b, b) (b -> r) b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\(ChuParPos b -> b -> r
_ b -> b -> r
g) b
x -> b -> b -> r
g b
x b
x)
    (\b
d -> (b
d, b
d))
{-# INLINE mergeWhyNotParChu #-}

-- | ⅋-monoid unit @⊥ → ?A@: constants, dual of 'discardBangChu'.
zeroWhyNotParChu ::
  ChuMorphism (,) r (->) r () (b -> r) b
zeroWhyNotParChu :: forall r b. ChuMorphism (,) r (->) r () (b -> r) b
zeroWhyNotParChu =
  (r -> (b -> r))
-> (b -> ()) -> ChuMorphism (,) r (->) r () (b -> r) b
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism r -> (b -> r)
forall a b. a -> b -> a
const (\b
_ -> ())
{-# INLINE zeroWhyNotParChu #-}

-- | Left unitor @⊥ ⅋ A → A@ over @Set@.
leftUnitorParChu ::
  ChuMorphism (,) r (->) (ChuParPos r () p n) ((), n) p n
leftUnitorParChu :: forall r p n.
ChuMorphism (,) r (->) (ChuParPos r () p n) ((), n) p n
leftUnitorParChu =
  (ChuParPos r () p n -> p)
-> (n -> ((), n))
-> ChuMorphism (,) r (->) (ChuParPos r () p n) ((), n) p n
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\ChuParPos r () p n
q -> ChuParPos r () p n -> () -> p
forall a b c d. ChuParPos a b c d -> b -> c
cppForward ChuParPos r () p n
q ()) (\n
d -> ((), n
d))
{-# INLINE leftUnitorParChu #-}

-- | Right unitor @A ⅋ ⊥ → A@ over @Set@.
rightUnitorParChu ::
  ChuMorphism (,) r (->) (ChuParPos p n r ()) (n, ()) p n
rightUnitorParChu :: forall r p n.
ChuMorphism (,) r (->) (ChuParPos p n r ()) (n, ()) p n
rightUnitorParChu =
  (ChuParPos p n r () -> p)
-> (n -> (n, ()))
-> ChuMorphism (,) r (->) (ChuParPos p n r ()) (n, ()) p n
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism (\ChuParPos p n r ()
q -> ChuParPos p n r () -> () -> p
forall a b c d. ChuParPos a b c d -> d -> a
cppBackward ChuParPos p n r ()
q ()) (\n
d -> (n
d, ()))
{-# INLINE rightUnitorParChu #-}

-- | Inverse of the left par unitor: @A → ⊥ ⅋ A@ over @Set@.
leftUnitorParChuInv ::
  ChuObj (,) r (->) a b ->
  ChuMorphism (,) r (->) a b (ChuParPos r () a b) ((), b)
leftUnitorParChuInv :: forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) a b (ChuParPos r () a b) ((), b)
leftUnitorParChuInv (ChuObj (a, b) -> r
e) =
  (a -> ChuParPos r () a b)
-> (((), b) -> b)
-> ChuMorphism (,) r (->) a b (ChuParPos r () a b) ((), b)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\a
x -> (() -> a) -> (b -> r) -> ChuParPos r () a b
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos (\()
_ -> a
x) (\b
d -> (a, b) -> r
e (a
x, b
d)))
    ((), b) -> b
forall a b. (a, b) -> b
snd
{-# INLINE leftUnitorParChuInv #-}

-- | Inverse of the right par unitor: @A → A ⅋ ⊥@ over @Set@.
rightUnitorParChuInv ::
  ChuObj (,) r (->) a b ->
  ChuMorphism (,) r (->) a b (ChuParPos a b r ()) (b, ())
rightUnitorParChuInv :: forall r a b.
ChuObj (,) r (->) a b
-> ChuMorphism (,) r (->) a b (ChuParPos a b r ()) (b, ())
rightUnitorParChuInv (ChuObj (a, b) -> r
e) =
  (a -> ChuParPos a b r ())
-> ((b, ()) -> b)
-> ChuMorphism (,) r (->) a b (ChuParPos a b r ()) (b, ())
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\a
x -> (b -> r) -> (() -> a) -> ChuParPos a b r ()
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos (\b
d -> (a, b) -> r
e (a
x, b
d)) (\()
_ -> a
x))
    (b, ()) -> b
forall a b. (a, b) -> a
fst
{-# INLINE rightUnitorParChuInv #-}

-- | Associator @(A ⅋ B) ⅋ C → A ⅋ (B ⅋ C)@ over @Set@.
assocParChu ::
  ChuMorphism
    (,)
    r
    (->)
    (ChuParPos (ChuParPos a b c d) (b, d) e f)
    ((b, d), f)
    (ChuParPos a b (ChuParPos c d e f) (d, f))
    (b, (d, f))
assocParChu :: forall {k} (r :: k) a b c d e f.
ChuMorphism
  (,)
  r
  (->)
  (ChuParPos (ChuParPos a b c d) (b, d) e f)
  ((b, d), f)
  (ChuParPos a b (ChuParPos c d e f) (d, f))
  (b, (d, f))
assocParChu =
  (ChuParPos (ChuParPos a b c d) (b, d) e f
 -> ChuParPos a b (ChuParPos c d e f) (d, f))
-> ((b, (d, f)) -> ((b, d), f))
-> ChuMorphism
     (,)
     r
     (->)
     (ChuParPos (ChuParPos a b c d) (b, d) e f)
     ((b, d), f)
     (ChuParPos a b (ChuParPos c d e f) (d, f))
     (b, (d, f))
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    ( \ChuParPos (ChuParPos a b c d) (b, d) e f
p ->
        (b -> ChuParPos c d e f)
-> ((d, f) -> a) -> ChuParPos a b (ChuParPos c d e f) (d, f)
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos
          ( \b
x ->
              (d -> e) -> (f -> c) -> ChuParPos c d e f
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos
                (\d
y -> ChuParPos (ChuParPos a b c d) (b, d) e f -> (b, d) -> e
forall a b c d. ChuParPos a b c d -> b -> c
cppForward ChuParPos (ChuParPos a b c d) (b, d) e f
p (b
x, d
y))
                (\f
z -> ChuParPos a b c d -> b -> c
forall a b c d. ChuParPos a b c d -> b -> c
cppForward (ChuParPos (ChuParPos a b c d) (b, d) e f -> f -> ChuParPos a b c d
forall a b c d. ChuParPos a b c d -> d -> a
cppBackward ChuParPos (ChuParPos a b c d) (b, d) e f
p f
z) b
x)
          )
          (\(d
y, f
z) -> ChuParPos a b c d -> d -> a
forall a b c d. ChuParPos a b c d -> d -> a
cppBackward (ChuParPos (ChuParPos a b c d) (b, d) e f -> f -> ChuParPos a b c d
forall a b c d. ChuParPos a b c d -> d -> a
cppBackward ChuParPos (ChuParPos a b c d) (b, d) e f
p f
z) d
y)
    )
    (\(b
x, (d
y, f
z)) -> ((b
x, d
y), f
z))
{-# INLINE assocParChu #-}

-- | Inverse associator @A ⅋ (B ⅋ C) → (A ⅋ B) ⅋ C@ over @Set@.
assocParChuInv ::
  ChuMorphism
    (,)
    r
    (->)
    (ChuParPos a b (ChuParPos c d e f) (d, f))
    (b, (d, f))
    (ChuParPos (ChuParPos a b c d) (b, d) e f)
    ((b, d), f)
assocParChuInv :: forall {k} (r :: k) a b c d e f.
ChuMorphism
  (,)
  r
  (->)
  (ChuParPos a b (ChuParPos c d e f) (d, f))
  (b, (d, f))
  (ChuParPos (ChuParPos a b c d) (b, d) e f)
  ((b, d), f)
assocParChuInv =
  (ChuParPos a b (ChuParPos c d e f) (d, f)
 -> ChuParPos (ChuParPos a b c d) (b, d) e f)
-> (((b, d), f) -> (b, (d, f)))
-> ChuMorphism
     (,)
     r
     (->)
     (ChuParPos a b (ChuParPos c d e f) (d, f))
     (b, (d, f))
     (ChuParPos (ChuParPos a b c d) (b, d) e f)
     ((b, d), f)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    ( \ChuParPos a b (ChuParPos c d e f) (d, f)
q ->
        ((b, d) -> e)
-> (f -> ChuParPos a b c d)
-> ChuParPos (ChuParPos a b c d) (b, d) e f
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos
          (\(b
x, d
y) -> ChuParPos c d e f -> d -> e
forall a b c d. ChuParPos a b c d -> b -> c
cppForward (ChuParPos a b (ChuParPos c d e f) (d, f) -> b -> ChuParPos c d e f
forall a b c d. ChuParPos a b c d -> b -> c
cppForward ChuParPos a b (ChuParPos c d e f) (d, f)
q b
x) d
y)
          ( \f
z ->
              (b -> c) -> (d -> a) -> ChuParPos a b c d
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos
                (\b
x -> ChuParPos c d e f -> f -> c
forall a b c d. ChuParPos a b c d -> d -> a
cppBackward (ChuParPos a b (ChuParPos c d e f) (d, f) -> b -> ChuParPos c d e f
forall a b c d. ChuParPos a b c d -> b -> c
cppForward ChuParPos a b (ChuParPos c d e f) (d, f)
q b
x) f
z)
                (\d
y -> ChuParPos a b (ChuParPos c d e f) (d, f) -> (d, f) -> a
forall a b c d. ChuParPos a b c d -> d -> a
cppBackward ChuParPos a b (ChuParPos c d e f) (d, f)
q (d
y, f
z))
          )
    )
    (\((b
x, d
y), f
z) -> (b
x, (d
y, f
z)))
{-# INLINE assocParChuInv #-}

-- | Symmetric braiding @A ⅋ B → B ⅋ A@ over @Set@.
swapParChu ::
  ChuMorphism
    (,)
    r
    (->)
    (ChuParPos a b c d)
    (b, d)
    (ChuParPos c d a b)
    (d, b)
swapParChu :: forall {k} (r :: k) a b c d.
ChuMorphism
  (,) r (->) (ChuParPos a b c d) (b, d) (ChuParPos c d a b) (d, b)
swapParChu =
  (ChuParPos a b c d -> ChuParPos c d a b)
-> ((d, b) -> (b, d))
-> ChuMorphism
     (,) r (->) (ChuParPos a b c d) (b, d) (ChuParPos c d a b) (d, b)
forall {k} {k} {k} {k} (t :: k) (r :: k) (arr :: k -> k -> *)
       (a :: k) (b :: k) (c :: k) (d :: k).
arr a c -> arr d b -> ChuMorphism t r arr a b c d
ChuMorphism
    (\(ChuParPos b -> c
f d -> a
g) -> (d -> a) -> (b -> c) -> ChuParPos c d a b
forall a b c d. (b -> c) -> (d -> a) -> ChuParPos a b c d
ChuParPos d -> a
g b -> c
f)
    (\(d
x, b
y) -> (b
y, d
x))
{-# INLINE swapParChu #-}

-- | Object-level @!A@.
data ChuOBang (r :: Type) a = ChuOBang

instance (ChuObject r a) => ChuObject r (ChuOBang r a) where
  chuObject :: ChuObj
  (,) r (->) (ChuPosType (ChuOBang r a)) (ChuNegType (ChuOBang r a))
chuObject = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuObj (,) r (->) (ChuPosType a) (ChuPosType a -> r)
forall r a b. ChuObj (,) r (->) a b -> ChuObj (,) r (->) a (a -> r)
bangChuObj (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)

instance (ChuSeparated r a) => ChuSeparated r (ChuOBang r a)

instance (ChuObject r a) => ChuExtensional r (ChuOBang r a)

-- | Object-level @?A = (!A⊥)⊥@.
data ChuOWhyNot (r :: Type) a = ChuOWhyNot

instance (ChuObject r a) => ChuObject r (ChuOWhyNot r a) where
  chuObject :: ChuObj
  (,)
  r
  (->)
  (ChuPosType (ChuOWhyNot r a))
  (ChuNegType (ChuOWhyNot r a))
chuObject = ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuObj (,) r (->) (ChuNegType a -> r) (ChuNegType a)
forall r a b. ChuObj (,) r (->) a b -> ChuObj (,) r (->) (b -> r) b
whyNotChuObj (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)

instance (ChuObject r a) => ChuSeparated r (ChuOWhyNot r a)

instance (ChuExtensional r a) => ChuExtensional r (ChuOWhyNot r a)

-- | Discard @!A → I@ for 'OChu'.
discardEOChu ::
  forall r (a :: Type).
  OChu r (ChuOBang r a) (ChuOUnit r)
discardEOChu :: forall r a. OChu r (ChuOBang r a) (ChuOUnit r)
discardEOChu =
  Chu (,) r (->) (ChuOBang r a) (ChuOUnit r)
-> OChu r (ChuOBang r a) (ChuOUnit r)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOBang r a))
  (ChuNegType (ChuOBang r a))
  (ChuPosType (ChuOUnit r))
  (ChuNegType (ChuOUnit r))
-> Chu (,) r (->) (ChuOBang r a) (ChuOUnit r)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism (,) r (->) (ChuPosType a) (ChuPosType a -> r) () r
forall r a. ChuMorphism (,) r (->) a (a -> r) () r
discardBangChu ::
            ChuMorphism
              (,)
              r
              (->)
              (ChuPosType a)
              (ChuPosType a -> r)
              ()
              r
        )
    )
{-# INLINE discardEOChu #-}

-- | Dereliction @!A → A@ for 'OChu'.
derelictOChu ::
  forall r a.
  (ChuObject r a) =>
  OChu r (ChuOBang r a) a
derelictOChu :: forall r a. ChuObject r a => OChu r (ChuOBang r a) a
derelictOChu = Chu (,) r (->) (ChuOBang r a) a -> OChu r (ChuOBang r a) a
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOBang r a))
  (ChuNegType (ChuOBang r a))
  (ChuPosType a)
  (ChuNegType a)
-> Chu (,) r (->) (ChuOBang r a) a
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a)
     (ChuPosType a -> r)
     (ChuPosType a)
     (ChuNegType a)
forall r a b.
ChuObj (,) r (->) a b -> ChuMorphism (,) r (->) a (a -> r) a b
derelictChu (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)))
{-# INLINE derelictOChu #-}

-- | Introduction @A → ?A@ for 'OChu'.
introduceOChu ::
  forall r a.
  (ChuObject r a) =>
  OChu r a (ChuOWhyNot r a)
introduceOChu :: forall r a. ChuObject r a => OChu r a (ChuOWhyNot r a)
introduceOChu = Chu (,) r (->) a (ChuOWhyNot r a) -> OChu r a (ChuOWhyNot r a)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu (ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuNegType a)
  (ChuPosType (ChuOWhyNot r a))
  (ChuNegType (ChuOWhyNot r a))
-> Chu (,) r (->) a (ChuOWhyNot r a)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu (ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
-> ChuMorphism
     (,)
     r
     (->)
     (ChuPosType a)
     (ChuNegType a)
     (ChuNegType a -> r)
     (ChuNegType a)
forall r a b.
ChuObj (,) r (->) a b -> ChuMorphism (,) r (->) a b (b -> r) b
introduceChu (forall r a.
ChuObject r a =>
ChuObj (,) r (->) (ChuPosType a) (ChuNegType a)
chuObject @r @a)))
{-# INLINE introduceOChu #-}

-- | Merge @?A ⅋ ?A → ?A@ for 'OChu'.
mergeEOChu ::
  forall r (a :: Type).
  OChu r (ChuOPar r (ChuOWhyNot r a) (ChuOWhyNot r a)) (ChuOWhyNot r a)
mergeEOChu :: forall r a.
OChu
  r (ChuOPar r (ChuOWhyNot r a) (ChuOWhyNot r a)) (ChuOWhyNot r a)
mergeEOChu =
  Chu
  (,)
  r
  (->)
  (ChuOPar r (ChuOWhyNot r a) (ChuOWhyNot r a))
  (ChuOWhyNot r a)
-> OChu
     r (ChuOPar r (ChuOWhyNot r a) (ChuOWhyNot r a)) (ChuOWhyNot r a)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOPar r (ChuOWhyNot r a) (ChuOWhyNot r a)))
  (ChuNegType (ChuOPar r (ChuOWhyNot r a) (ChuOWhyNot r a)))
  (ChuPosType (ChuOWhyNot r a))
  (ChuNegType (ChuOWhyNot r a))
-> Chu
     (,)
     r
     (->)
     (ChuOPar r (ChuOWhyNot r a) (ChuOWhyNot r a))
     (ChuOWhyNot r a)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism
  (,)
  r
  (->)
  (ChuParPos
     (ChuNegType a -> r)
     (ChuNegType a)
     (ChuNegType a -> r)
     (ChuNegType a))
  (ChuNegType a, ChuNegType a)
  (ChuNegType a -> r)
  (ChuNegType a)
forall r b.
ChuMorphism
  (,) r (->) (ChuParPos (b -> r) b (b -> r) b) (b, b) (b -> r) b
mergeWhyNotParChu ::
            ChuMorphism
              (,)
              r
              (->)
              (ChuParPos (ChuNegType a -> r) (ChuNegType a) (ChuNegType a -> r) (ChuNegType a))
              (ChuNegType a, ChuNegType a)
              (ChuNegType a -> r)
              (ChuNegType a)
        )
    )
{-# INLINE mergeEOChu #-}

-- | Unit @⊥ → ?A@ for 'OChu'.
zeroEOChu ::
  forall r (a :: Type).
  OChu r (ChuONeg r (ChuOUnit r)) (ChuOWhyNot r a)
zeroEOChu :: forall r a. OChu r (ChuONeg r (ChuOUnit r)) (ChuOWhyNot r a)
zeroEOChu =
  Chu (,) r (->) (ChuONeg r (ChuOUnit r)) (ChuOWhyNot r a)
-> OChu r (ChuONeg r (ChuOUnit r)) (ChuOWhyNot r a)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuONeg r (ChuOUnit r)))
  (ChuNegType (ChuONeg r (ChuOUnit r)))
  (ChuPosType (ChuOWhyNot r a))
  (ChuNegType (ChuOWhyNot r a))
-> Chu (,) r (->) (ChuONeg r (ChuOUnit r)) (ChuOWhyNot r a)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism (,) r (->) r () (ChuNegType a -> r) (ChuNegType a)
forall r b. ChuMorphism (,) r (->) r () (b -> r) b
zeroWhyNotParChu ::
            ChuMorphism
              (,)
              r
              (->)
              r
              ()
              (ChuNegType a -> r)
              (ChuNegType a)
        )
    )
{-# INLINE zeroEOChu #-}

-- | Copy @!A → !A ⊗ !A@ for 'OChu'.
copyTOChu ::
  forall r (a :: Type).
  OChu r (ChuOBang r a) (ChuOTensor r (ChuOBang r a) (ChuOBang r a))
copyTOChu :: forall r a.
OChu r (ChuOBang r a) (ChuOTensor r (ChuOBang r a) (ChuOBang r a))
copyTOChu =
  Chu
  (,)
  r
  (->)
  (ChuOBang r a)
  (ChuOTensor r (ChuOBang r a) (ChuOBang r a))
-> OChu
     r (ChuOBang r a) (ChuOTensor r (ChuOBang r a) (ChuOBang r a))
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOBang r a))
  (ChuNegType (ChuOBang r a))
  (ChuPosType (ChuOTensor r (ChuOBang r a) (ChuOBang r a)))
  (ChuNegType (ChuOTensor r (ChuOBang r a) (ChuOBang r a)))
-> Chu
     (,)
     r
     (->)
     (ChuOBang r a)
     (ChuOTensor r (ChuOBang r a) (ChuOBang r a))
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a)
  (ChuPosType a -> r)
  (ChuPosType a, ChuPosType a)
  (ChuTensorNeg
     (ChuPosType a)
     (ChuPosType a -> r)
     (ChuPosType a)
     (ChuPosType a -> r))
forall r a.
ChuMorphism
  (,) r (->) a (a -> r) (a, a) (ChuTensorNeg a (a -> r) a (a -> r))
copyBangChu ::
            ChuMorphism
              (,)
              r
              (->)
              (ChuPosType a)
              (ChuPosType a -> r)
              (ChuPosType a, ChuPosType a)
              (ChuTensorNeg (ChuPosType a) (ChuPosType a -> r) (ChuPosType a) (ChuPosType a -> r))
        )
    )
{-# INLINE copyTOChu #-}

-- | Discard @!A → I@ for 'OChu'.
discardTOChu ::
  forall r (a :: Type).
  OChu r (ChuOBang r a) (ChuOUnit r)
discardTOChu :: forall r a. OChu r (ChuOBang r a) (ChuOUnit r)
discardTOChu =
  Chu (,) r (->) (ChuOBang r a) (ChuOUnit r)
-> OChu r (ChuOBang r a) (ChuOUnit r)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOBang r a))
  (ChuNegType (ChuOBang r a))
  (ChuPosType (ChuOUnit r))
  (ChuNegType (ChuOUnit r))
-> Chu (,) r (->) (ChuOBang r a) (ChuOUnit r)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism (,) r (->) (ChuPosType a) (ChuPosType a -> r) () r
forall r a. ChuMorphism (,) r (->) a (a -> r) () r
discardBangChu ::
            ChuMorphism
              (,)
              r
              (->)
              (ChuPosType a)
              (ChuPosType a -> r)
              ()
              r
        )
    )
{-# INLINE discardTOChu #-}

-- | Merge @!A ⊗ !A → !A@ for 'OChu'.
plusTOChu ::
  forall r (a :: Type).
  (Monoid (ChuPosType a)) =>
  OChu r (ChuOTensor r (ChuOBang r a) (ChuOBang r a)) (ChuOBang r a)
plusTOChu :: forall r a.
Monoid (ChuPosType a) =>
OChu r (ChuOTensor r (ChuOBang r a) (ChuOBang r a)) (ChuOBang r a)
plusTOChu =
  Chu
  (,)
  r
  (->)
  (ChuOTensor r (ChuOBang r a) (ChuOBang r a))
  (ChuOBang r a)
-> OChu
     r (ChuOTensor r (ChuOBang r a) (ChuOBang r a)) (ChuOBang r a)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOTensor r (ChuOBang r a) (ChuOBang r a)))
  (ChuNegType (ChuOTensor r (ChuOBang r a) (ChuOBang r a)))
  (ChuPosType (ChuOBang r a))
  (ChuNegType (ChuOBang r a))
-> Chu
     (,)
     r
     (->)
     (ChuOTensor r (ChuOBang r a) (ChuOBang r a))
     (ChuOBang r a)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType a, ChuPosType a)
  (ChuTensorNeg
     (ChuPosType a)
     (ChuPosType a -> r)
     (ChuPosType a)
     (ChuPosType a -> r))
  (ChuPosType a)
  (ChuPosType a -> r)
forall a r.
Monoid a =>
ChuMorphism
  (,) r (->) (a, a) (ChuTensorNeg a (a -> r) a (a -> r)) a (a -> r)
mergeBangChu ::
            ChuMorphism
              (,)
              r
              (->)
              (ChuPosType a, ChuPosType a)
              (ChuTensorNeg (ChuPosType a) (ChuPosType a -> r) (ChuPosType a) (ChuPosType a -> r))
              (ChuPosType a)
              (ChuPosType a -> r)
        )
    )
{-# INLINE plusTOChu #-}

-- | Zero @I → !A@ for 'OChu'.
zeroTOChu ::
  forall r (a :: Type).
  (Monoid (ChuPosType a)) =>
  OChu r (ChuOUnit r) (ChuOBang r a)
zeroTOChu :: forall r a.
Monoid (ChuPosType a) =>
OChu r (ChuOUnit r) (ChuOBang r a)
zeroTOChu =
  Chu (,) r (->) (ChuOUnit r) (ChuOBang r a)
-> OChu r (ChuOUnit r) (ChuOBang r a)
forall r a b. Chu (,) r (->) a b -> OChu r a b
OChu
    ( ChuMorphism
  (,)
  r
  (->)
  (ChuPosType (ChuOUnit r))
  (ChuNegType (ChuOUnit r))
  (ChuPosType (ChuOBang r a))
  (ChuNegType (ChuOBang r a))
-> Chu (,) r (->) (ChuOUnit r) (ChuOBang r a)
forall (t :: * -> * -> *) r (arr :: * -> * -> *) a b.
ChuMorphism
  t r arr (ChuPosType a) (ChuNegType a) (ChuPosType b) (ChuNegType b)
-> Chu t r arr a b
Chu
        ( ChuMorphism (,) r (->) () r (ChuPosType a) (ChuPosType a -> r)
forall a r. Monoid a => ChuMorphism (,) r (->) () r a (a -> r)
zeroBangChu ::
            ChuMorphism
              (,)
              r
              (->)
              ()
              r
              (ChuPosType a)
              (ChuPosType a -> r)
        )
    )
{-# INLINE zeroTOChu #-}

-- ---------------------------------------------------------------------------
-- Embedding from 'Circuit.Poles'
-- ---------------------------------------------------------------------------

-- | Embed a symmetric pole into a pointed Chu object.
--
-- A self-dual channel @Poles arr a a@ has write pole @In arr a@ and read pole
-- @Out arr a@.  'Circuit.Poles.close' is already the pairing
-- @In ⊗ Out → arr a a@, so the embedding is direct.  The point pair
-- @(conjoint e, companion e)@ is retained as the chosen point of the pointed
-- object.
polesAsChu ::
  Poles arr a a ->
  PointedChuObj (,) (arr a a) (->) (In arr a) (Out arr a)
polesAsChu :: forall {k1} (arr :: k1 -> k1 -> *) (a :: k1).
Poles arr a a
-> PointedChuObj (,) (arr a a) (->) (In arr a) (Out arr a)
polesAsChu Poles arr a a
e = ChuObj (,) (arr a a) (->) (In arr a) (Out arr a)
-> In arr a
-> Out arr a
-> PointedChuObj (,) (arr a a) (->) (In arr a) (Out arr a)
forall {k} {k} (t :: * -> * -> k) (r :: k) (arr :: k -> k -> *) a
       b.
ChuObj t r arr a b -> a -> b -> PointedChuObj t r arr a b
PointedChuObj (((In arr a, Out arr a) -> arr a a)
-> ChuObj (,) (arr a a) (->) (In arr a) (Out arr a)
forall {k} {k} {k} {k} (t :: k -> k -> k) (r :: k)
       (arr :: k -> k -> *) (a :: k) (b :: k).
arr (t a b) r -> ChuObj t r arr a b
ChuObj ((In arr a -> Out arr a -> arr a a)
-> (In arr a, Out arr a) -> arr a a
forall a b c. (a -> b -> c) -> (a, b) -> c
Pre.uncurry In arr a -> Out arr a -> arr a a
forall {k} (arr :: k -> k -> *) (a :: k).
In arr a -> Out arr a -> arr a a
close)) (Poles arr a a -> In arr a
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k1) (b :: k2).
Poles arr a b -> In arr a
conjoint Poles arr a a
e) (Poles arr a a -> Out arr a
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k1) (b :: k2).
Poles arr a b -> Out arr b
companion Poles arr a a
e)
{-# INLINE polesAsChu #-}

-- | Apply a Chu endomorphism to a symmetric pole.
--
-- This is the lawful counterpart to the free 'Circuit.Poles.dimap': the
-- forward and backward maps are an adjoint pair by construction of
-- 'ChuMorphism'.  The Chu law is discharged by the type, not just tested.
lawfulDimap ::
  ChuMorphism (,) (arr a a) (->) (In arr a) (Out arr a) (In arr a) (Out arr a) ->
  Poles arr a a ->
  Poles arr a a
lawfulDimap :: forall {k1} (arr :: k1 -> k1 -> *) (a :: k1).
ChuMorphism
  (,) (arr a a) (->) (In arr a) (Out arr a) (In arr a) (Out arr a)
-> Poles arr a a -> Poles arr a a
lawfulDimap (ChuMorphism In arr a -> In arr a
f Out arr a -> Out arr a
g) Poles arr a a
e = In arr a -> Out arr a -> Poles arr a a
forall {k} {k1} (arr :: k -> k1 -> *) (a :: k) (b :: k1).
In arr a -> Out arr b -> Poles arr a b
Poles (In arr a -> In arr a
f (Poles arr a a -> In arr a
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k1) (b :: k2).
Poles arr a b -> In arr a
conjoint Poles arr a a
e)) (Out arr a -> Out arr a
g (Poles arr a a -> Out arr a
forall {k1} {k2} (arr :: k1 -> k2 -> *) (a :: k1) (b :: k2).
Poles arr a b -> Out arr b
companion Poles arr a a
e))
{-# INLINE lawfulDimap #-}