{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Checking laws stated as code ("Proarrow.Tools.Laws") in a 'Testable' category: 'testLaws'
-- runs each law with random objects for its variables and random arrows for the ones it asks for,
-- and compares both sides.
--
-- The endpoints of a law's equation are built inside the law, so their 'TestOb' cannot be listed
-- up front. Instead the law is run in 'TESTED' @k@, whose objects are built from leaves by the
-- structures' object formers; there an object's 'Ob' is 'Tested', which rebuilds the 'TestOb' of
-- the object of @k@ it stands for from the 'Witnesses' passed at run time: one 'Witness' per
-- structure in the law's list, e.g. a 'WithTestOb2' for 'M.Monoidal'.
--
-- A structure this module does not cover can be added from outside it, in the same way as the ones
-- here:
--
-- * a former for each new kind of object (an open data family, or one of the free category's),
--   with a 'Tested' instance giving its 'Untest' and rebuilding its 'Ob' and 'TestOb';
-- * a 'Witness' instance for the structure, holding how 'TestOb' is closed under its formers;
-- * the structure's class instance for 'TESTED', whose arrows describe themselves ('prim' for a
--   named arrow, 'app', 'infixlDoc', 'infixrDoc' for operations on arrows).
module Proarrow.Testing.Laws.Run
  ( testLaws
  , testLawsWith
  , testProLaws

    -- * Witnesses
  , Witness (..)
  , Witnesses (..)
  , HasWitness (..)

    -- * Interpreting with testable objects
  , TESTED (..)
  , Tested (..)
  , untestOb2
  , untestOb3
  , untestTestOb2
  , TestedArr
  , pattern TestedArr

    -- * Interpreting profunctors
  , TestedP (..)
  , RepF
  , RepresentedBy
  , CorepF
  , CorepresentedBy

    -- * Describing arrows
  , Doc
  , prim
  , atom
  , app
  , apps
  , infixlDoc
  , infixrDoc
  ) where

import Data.Kind (Constraint, Type)
import Test.Falsify.Generator (Gen)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Falsify (Property, TestOptions, genWith, testProperty, testPropertyWith)
import Prelude hiding (fst, id, snd, (.))

import Proarrow.Adjunction qualified as Adj
import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Enriched.Finitary (Finitary (..))
import Proarrow.Category.Instance.Free qualified as Free
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Category.Monoidal.Closed qualified as Exponential
import Proarrow.Category.Monoidal.CompactClosed qualified as CC
import Proarrow.Category.Monoidal.CopyDiscard qualified as CopyDiscard
import Proarrow.Category.Monoidal.Distributive qualified as Distributive
import Proarrow.Category.Monoidal.StarAutonomous qualified as SA
import Proarrow.Category.Monoidal.Strength qualified as Strength
import Proarrow.Colimit.BinaryCoproduct qualified as BinaryCoproduct
import Proarrow.Colimit.Initial qualified as Initial
import Proarrow.Core (CAT, CategoryOf (..), Hom, Kind, Profunctor (..), Promonad (..), type (+->))
import Proarrow.Limit.BinaryProduct qualified as BinaryProduct
import Proarrow.Limit.Terminal qualified as Terminal
import Proarrow.Monoid qualified as Monoid
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), withObCorep)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (Representable (..), withObRep)
import Proarrow.Testing
  ( Some (..)
  , SomeProfunctorElt (..)
  , TestObIsOb
  , Testable (..)
  , TestableProfunctor (..)
  , TestableTypeP
  , WithTestOb2
  , WithTestObCoprod
  , WithTestObCorep
  , WithTestObDual
  , WithTestObExp
  , WithTestObProd
  , WithTestObRep
  , genNamed
  , genOb
  , genSuchThat
  , isGenNonEmpty
  , obFromTestOb
  , testEq
  )
import Proarrow.Tools.Laws qualified as Laws

-- | Check the laws of @'Laws.Laws' cs@ in @k@, one property per law: run each law in 'TESTED'
-- with random objects for its variables and random arrows for the ones it asks for. The
-- 'Witnesses' say how 'TestOb' is closed under the structures of @cs@ (see 'Tested').
testLaws :: forall cs k. (Laws.Laws cs, Testable k, Free.All cs (TESTED cs k)) => String -> Witnesses cs k -> TestTree
testLaws :: forall (cs :: [Type -> Constraint]) k.
(Laws cs, Testable k, All cs (TESTED cs k)) =>
String -> Witnesses cs k -> TestTree
testLaws = forall (cs :: [Type -> Constraint]) k.
(Laws cs, Testable k, All cs (TESTED cs k)) =>
Property (Some k) -> String -> Witnesses cs k -> TestTree
testLawsWith @cs (forall k. Testable k => Property (Some k)
genOb @k)

-- | 'testLaws' with the objects for the variables drawn from the given generator, e.g.
-- 'Proarrow.Testing.genObSmall' where the laws build large objects like exponentials.
testLawsWith
  :: forall cs k
   . (Laws.Laws cs, Testable k, Free.All cs (TESTED cs k))
  => Property (Some k) -> String -> Witnesses cs k -> TestTree
testLawsWith :: forall (cs :: [Type -> Constraint]) k.
(Laws cs, Testable k, All cs (TESTED cs k)) =>
Property (Some k) -> String -> Witnesses cs k -> TestTree
testLawsWith Property (Some k)
genObject String
name Witnesses cs k
witnesses =
  String -> [TestTree] -> TestTree
testGroup String
name [String -> Property' String () -> TestTree
testProperty (Law cs -> String
forall (cs :: [Type -> Constraint]). Law cs -> String
Laws.lawName Law cs
law) (Law cs -> Property' String ()
checkLaw Law cs
law) | Law cs
law <- forall (cs :: [Type -> Constraint]). Laws cs => [Law cs]
Laws.laws @cs]
  where
    checkLaw :: Laws.Law cs -> Property ()
    checkLaw :: Law cs -> Property' String ()
checkLaw (Laws.Law String
lawName LawBody cs
body) = do
      Some @a <- Property (Some k)
genObject
      Some @b <- genObject
      Some @c <- genObject
      Some @d <- genObject
      Some @e <- genObject
      eq <-
        body @(TLeaf a :: TESTED cs k) @(TLeaf b) @(TLeaf c) @(TLeaf d) @(TLeaf e) (genArr witnesses)
      testEquation witnesses lawName eq

-- | Check the laws of @'Laws.ProLaws' c@ for the profunctor @p@, one property per law: run each
-- law with @p@ interpreted as 'TestedP' @p@, its elements drawn by 'genProfunctorElt' (each picks
-- its two object variables), the other variables of a 'Laws.ProLaw' drawn along the chain
-- @e '~>' c '~>' a@ and @b '~>' d '~>' f@ where those hom-sets are non-empty, and random arrows
-- for the ones it asks for. The two 'Witnesses' are for the domain @j@ and the codomain
-- @k@ of @p@, the 'TestOptions' apply to each law's property, and the other variables are drawn from
-- the given generator of objects, e.g. 'genSomeSmall' where the laws tensor several objects
-- together.
testProLaws
  :: forall {j} {k} csj csk cl (p :: j +-> k)
   . (Laws.ProLaws cl, TestableProfunctor p, cl (TestedP p :: TESTED csj j +-> TESTED csk k))
  => TestOptions
  -> (forall i. (Testable i) => Gen (Some i))
  -> String
  -> Witnesses csj j
  -> Witnesses csk k
  -> TestTree
testProLaws :: forall {j} {k} (csj :: [Type -> Constraint])
       (csk :: [Type -> Constraint])
       (cl :: (TESTED csj j +-> TESTED csk k) -> Constraint)
       (p :: j +-> k).
(ProLaws cl, TestableProfunctor p, cl (TestedP p)) =>
TestOptions
-> (forall i. Testable i => Gen (Some i))
-> String
-> Witnesses csj j
-> Witnesses csk k
-> TestTree
testProLaws TestOptions
opts forall i. Testable i => Gen (Some i)
genObjects String
name Witnesses csj j
wsj Witnesses csk k
wsk =
  String -> [TestTree] -> TestTree
testGroup String
name [TestOptions -> String -> Property' String () -> TestTree
testPropertyWith TestOptions
opts (ProLaw cl -> String
forall {j} {k} (c :: (j +-> k) -> Constraint). ProLaw c -> String
Laws.proLawName ProLaw cl
law) (ProLaw cl -> Property' String ()
checkLaw ProLaw cl
law) | ProLaw cl
law <- forall {j} {k} (c :: (j +-> k) -> Constraint).
ProLaws c =>
[ProLaw c]
forall (c :: (TESTED csj j +-> TESTED csk k) -> Constraint).
ProLaws c =>
[ProLaw c]
Laws.proLaws @cl]
  where
    checkLaw :: Laws.ProLaw cl -> Property ()
    checkLaw :: ProLaw cl -> Property' String ()
checkLaw (Laws.ProLaw String
lawName ProLawBody cl
body) = do
      SomeP @a @b p0 <- forall {j} {k} (p :: j +-> k).
TestableProfunctor p =>
String -> Property (SomeProfunctorElt p)
forall (p :: j +-> k).
TestableProfunctor p =>
String -> Property (SomeProfunctorElt p)
genProfunctorElt @p String
"p"
      Some @c <- objectSuchThat @k \(Some @c') -> forall a. TestableType a => Bool
isGenNonEmpty @(c' ~> a)
      Some @d <- objectSuchThat @j \(Some @d') -> forall a. TestableType a => Bool
isGenNonEmpty @(b ~> d')
      Some @e <- objectSuchThat @k \(Some @e') -> forall a. TestableType a => Bool
isGenNonEmpty @(e' ~> c)
      Some @f <- objectSuchThat @j \(Some @f') -> forall a. TestableType a => Bool
isGenNonEmpty @(d ~> f')
      eq <-
        body @(TestedP p) @(TLeaf a :: TESTED csk k) @(TLeaf b :: TESTED csj j) @(TLeaf c) @(TLeaf d) @(TLeaf e) @(TLeaf f)
          (prim "p" p0)
          (genArr wsk)
          (genArr wsj)
      testProEquation lawName eq
    checkLaw (Laws.ProLaw3 String
lawName ProLawBody3 cl
body) = do
      SomeP @a @b p0 <- forall {j} {k} (p :: j +-> k).
TestableProfunctor p =>
String -> Property (SomeProfunctorElt p)
forall (p :: j +-> k).
TestableProfunctor p =>
String -> Property (SomeProfunctorElt p)
genProfunctorElt @p String
"p"
      SomeP @c @d p1 <- genProfunctorElt @p "p'"
      SomeP @e @f p2 <- genProfunctorElt @p "p''"
      eq <-
        body @(TestedP p) @(TLeaf a :: TESTED csk k) @(TLeaf b :: TESTED csj j) @(TLeaf c) @(TLeaf d) @(TLeaf e) @(TLeaf f)
          (prim "p" p0)
          (prim "p'" p1)
          (prim "p''" p2)
          (genArr wsk)
          (genArr wsj)
      testProEquation lawName eq
    objectSuchThat :: forall i. (Testable i) => (Some i -> Bool) -> Property (Some i)
    objectSuchThat :: forall i. Testable i => (Some i -> Bool) -> Property (Some i)
objectSuchThat = (Some i -> Maybe String) -> Gen (Some i) -> Property (Some i)
forall a e.
HasCallStack =>
(a -> Maybe String) -> Gen a -> Property' e a
genWith (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> (Some i -> String) -> Some i -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Some i -> String
forall a. Show a => a -> String
show) (Gen (Some i) -> Property (Some i))
-> ((Some i -> Bool) -> Gen (Some i))
-> (Some i -> Bool)
-> Property (Some i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Gen (Some i) -> (Some i -> Bool) -> Gen (Some i)
forall key. Gen key -> (key -> Bool) -> Gen key
genSuchThat (forall i. Testable i => Gen (Some i)
genObjects @i)
    testProEquation :: String -> Laws.ProEquation (TestedP p :: TESTED csj j +-> TESTED csk k) -> Property ()
    testProEquation :: String -> ProEquation (TestedP p) -> Property' String ()
testProEquation String
lawName = \case
      TestedP p a b
l Laws.:=: TestedP p a b
r -> Witnesses csj j
-> Witnesses csk k
-> String
-> TestedP p a b
-> TestedP p a b
-> Property' String ()
forall {csj :: [Type -> Constraint]} {csk :: [Type -> Constraint]}
       {j} {k} (p :: j +-> k) (x :: TESTED csk k) (y :: TESTED csj j).
TestableProfunctor p =>
Witnesses csj j
-> Witnesses csk k
-> String
-> TestedP p x y
-> TestedP p x y
-> Property' String ()
testTested Witnesses csj j
wsj Witnesses csk k
wsk String
lawName TestedP p a b
l TestedP p a b
r
      Laws.InK Equation (TESTED csk k)
e -> Witnesses csk k
-> String -> Equation (TESTED csk k) -> Property' String ()
forall (cs :: [Type -> Constraint]) k.
Testable k =>
Witnesses cs k
-> String -> Equation (TESTED cs k) -> Property' String ()
testEquation Witnesses csk k
wsk String
lawName Equation (TESTED csk k)
e
      Laws.InJ Equation (TESTED csj j)
e -> Witnesses csj j
-> String -> Equation (TESTED csj j) -> Property' String ()
forall (cs :: [Type -> Constraint]) k.
Testable k =>
Witnesses cs k
-> String -> Equation (TESTED cs k) -> Property' String ()
testEquation Witnesses csj j
wsj String
lawName Equation (TESTED csj j)
e

-- | Compare the two sides of an equation between arrows of 'TESTED', printing them on failure.
testEquation :: forall cs k. (Testable k) => Witnesses cs k -> String -> Laws.Equation (TESTED cs k) -> Property ()
testEquation :: forall (cs :: [Type -> Constraint]) k.
Testable k =>
Witnesses cs k
-> String -> Equation (TESTED cs k) -> Property' String ()
testEquation Witnesses cs k
ws String
lawName Equation (TESTED cs k)
eq = Equation (TESTED cs k)
-> (forall (a :: TESTED cs k) (b :: TESTED cs k).
    (a ~> b) -> (a ~> b) -> Property' String ())
-> Property' String ()
forall {k} r.
Equation k
-> (forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r) -> r
Laws.withSides Equation (TESTED cs k)
eq (Witnesses cs k
-> Witnesses cs k
-> String
-> TestedP (Hom k) a b
-> TestedP (Hom k) a b
-> Property' String ()
forall {csj :: [Type -> Constraint]} {csk :: [Type -> Constraint]}
       {j} {k} (p :: j +-> k) (x :: TESTED csk k) (y :: TESTED csj j).
TestableProfunctor p =>
Witnesses csj j
-> Witnesses csk k
-> String
-> TestedP p x y
-> TestedP p x y
-> Property' String ()
testTested Witnesses cs k
ws Witnesses cs k
ws String
lawName)

-- | A named arbitrary element of @p@ between the objects of @k@ and @j@ that the endpoints stand
-- for. With @p@ the hom profunctor, a named arbitrary arrow.
genTested
  :: forall {csj} {csk} {j} {k} (p :: j +-> k) (x :: TESTED csk k) (y :: TESTED csj j)
   . (TestableTypeP p, Tested x, Tested y)
  => Witnesses csj j -> Witnesses csk k -> String -> Property (TestedP p x y)
genTested :: forall {csj :: [Type -> Constraint]} {csk :: [Type -> Constraint]}
       {j} {k} (p :: j +-> k) (x :: TESTED csk k) (y :: TESTED csj j).
(TestableTypeP p, Tested x, Tested y) =>
Witnesses csj j
-> Witnesses csk k -> String -> Property (TestedP p x y)
genTested Witnesses csj j
wsj Witnesses csk k
wsk String
s = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
forall (a :: TESTED csk k) r.
Tested a =>
Witnesses csk k -> (TestOb (Untest a) => r) -> r
untestTestOb @x Witnesses csk k
wsk ((TestOb (Untest x) => Property (TestedP p x y))
 -> Property (TestedP p x y))
-> (TestOb (Untest x) => Property (TestedP p x y))
-> Property (TestedP p x y)
forall a b. (a -> b) -> a -> b
$ forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
forall (a :: TESTED csj j) r.
Tested a =>
Witnesses csj j -> (TestOb (Untest a) => r) -> r
untestTestOb @y Witnesses csj j
wsj ((TestOb (Untest y) => Property (TestedP p x y))
 -> Property (TestedP p x y))
-> (TestOb (Untest y) => Property (TestedP p x y))
-> Property (TestedP p x y)
forall a b. (a -> b) -> a -> b
$ String -> p (Untest x) (Untest y) -> TestedP p x y
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
s (p (Untest x) (Untest y) -> TestedP p x y)
-> Property' String (p (Untest x) (Untest y))
-> Property (TestedP p x y)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TestableType a => String -> Property a
genNamed @(p (Untest x) (Untest y)) String
s

-- | A named arbitrary arrow, 'genTested' at the hom profunctor.
genArr
  :: forall cs k (x :: TESTED cs k) y. (Testable k, Tested x, Tested y) => Witnesses cs k -> String -> Property (x ~> y)
genArr :: forall (cs :: [Type -> Constraint]) k (x :: TESTED cs k)
       (y :: TESTED cs k).
(Testable k, Tested x, Tested y) =>
Witnesses cs k -> String -> Property (x ~> y)
genArr Witnesses cs k
ws = forall {csj :: [Type -> Constraint]} {csk :: [Type -> Constraint]}
       {j} {k} (p :: j +-> k) (x :: TESTED csk k) (y :: TESTED csj j).
(TestableTypeP p, Tested x, Tested y) =>
Witnesses csj j
-> Witnesses csk k -> String -> Property (TestedP p x y)
forall (p :: k +-> k) (x :: TESTED cs k) (y :: TESTED cs k).
(TestableTypeP p, Tested x, Tested y) =>
Witnesses cs k
-> Witnesses cs k -> String -> Property (TestedP p x y)
genTested @(Hom k) Witnesses cs k
ws Witnesses cs k
ws

-- | Compare two elements of @p@, printing their descriptions on failure.
testTested
  :: forall {csj} {csk} {j} {k} (p :: j +-> k) (x :: TESTED csk k) (y :: TESTED csj j)
   . (TestableProfunctor p)
  => Witnesses csj j -> Witnesses csk k -> String -> TestedP p x y -> TestedP p x y -> Property ()
testTested :: forall {csj :: [Type -> Constraint]} {csk :: [Type -> Constraint]}
       {j} {k} (p :: j +-> k) (x :: TESTED csk k) (y :: TESTED csj j).
TestableProfunctor p =>
Witnesses csj j
-> Witnesses csk k
-> String
-> TestedP p x y
-> TestedP p x y
-> Property' String ()
testTested Witnesses csj j
wsj Witnesses csk k
wsk String
lawName (TestedP Doc
dl p (Untest x) (Untest y)
l) (TestedP Doc
dr p (Untest x) (Untest y)
r) =
  forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
forall (a :: TESTED csk k) r.
Tested a =>
Witnesses csk k -> (TestOb (Untest a) => r) -> r
untestTestOb @x Witnesses csk k
wsk ((TestOb (Untest x) => Property' String ()) -> Property' String ())
-> (TestOb (Untest x) => Property' String ())
-> Property' String ()
forall a b. (a -> b) -> a -> b
$ forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
forall (a :: TESTED csj j) r.
Tested a =>
Witnesses csj j -> (TestOb (Untest a) => r) -> r
untestTestOb @y @(Property ()) Witnesses csj j
wsj ((TestOb (Untest y) => Property' String ()) -> Property' String ())
-> (TestOb (Untest y) => Property' String ())
-> Property' String ()
forall a b. (a -> b) -> a -> b
$ String
-> String
-> p (Untest x) (Untest y)
-> String
-> p (Untest x) (Untest y)
-> Property' String ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property' String ()
testEq String
lawName (Doc
dl Int
0 String
"") p (Untest x) (Untest y)
l (Doc
dr Int
0 String
"") p (Untest x) (Untest y)
r

-- | Objects of @k@ built from leaves by the structures' object formers. Checking a law
-- interprets it here rather than in @k@ itself: an object's 'Ob' is then 'Tested', which
-- recovers the 'TestOb' of the object of @k@ it stands for ('Untest') from the 'Witnesses' for
-- the structures @cs@, supplied at run time.
--
-- The only constructor is the leaf. Compound objects use the free category's formers, which are
-- open data families of any kind ('M.**!', 'BinaryProduct.*!', 'SA.DualF', ...), so a new
-- structure brings its own former and its own 'Tested' instance.
type TESTED :: [Kind -> Constraint] -> Kind -> Kind
type data TESTED cs k = TLeaf k

-- * Witnesses

-- | How 'TestOb' is closed under the object formers of the structure @c@, for the category @k@.
-- Structures without formers of their own have a witness that holds nothing.
type Witness :: (Kind -> Constraint) -> Kind -> Type
data family Witness c k

data instance Witness CategoryOf k = CategoryW
newtype instance Witness M.Monoidal k = MonoidalW (WithTestOb2 k)
data instance Witness M.SymMonoidal k = SymMonoidalW
newtype instance Witness BinaryProduct.HasBinaryProducts k = ProductsW (WithTestObProd k)
newtype instance Witness BinaryCoproduct.HasBinaryCoproducts k = CoproductsW (WithTestObCoprod k)
data instance Witness Terminal.HasTerminalObject k = TerminalW
data instance Witness Initial.HasInitialObject k = InitialW
data instance Witness Distributive.Distributive k = DistributiveW
newtype instance Witness Exponential.Closed k = ClosedW (WithTestObExp k)
newtype instance Witness SA.StarAutonomous k = StarAutonomousW (WithTestObDual k)
data instance Witness CC.CompactClosed k = CompactClosedW
data instance Witness Strength.TracedMonoidal k = TracedW
data instance Witness CopyDiscard.CopyDiscard k = CopyDiscardW
data instance Witness (Monoid.Supplies Monoid.Monoid) k = MonoidSupplyW
data instance Witness (Monoid.Supplies Monoid.Comonoid) k = ComonoidSupplyW
data instance Witness (Monoid.Supplies Monoid.CommutativeMonoid) k = CommutativeMonoidSupplyW
data instance Witness (Monoid.Supplies Monoid.CocommutativeComonoid) k = CocommutativeComonoidSupplyW

infixr 5 :&

-- | One 'Witness' for each structure in @cs@, in the same order.
type Witnesses :: [Kind -> Constraint] -> Kind -> Type
data Witnesses cs k where
  WNil :: Witnesses '[] k
  (:&) :: Witness c k -> Witnesses cs k -> Witnesses (c ': cs) k

-- | Look up the witness for the structure @c@.
type HasWitness :: (Kind -> Constraint) -> [Kind -> Constraint] -> Constraint
class HasWitness c cs where
  -- | The witness for @c@ in the list.
  witness :: Witnesses cs k -> Witness c k

instance {-# OVERLAPPABLE #-} (HasWitness c cs) => HasWitness c (d ': cs) where
  witness :: forall k. Witnesses (d : cs) k -> Witness c k
witness (Witness c k
_ :& Witnesses cs k
ws) = forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k.
HasWitness c cs =>
Witnesses cs k -> Witness c k
witness @c Witnesses cs k
ws
instance HasWitness c (c ': cs) where
  witness :: forall k. Witnesses (c : cs) k -> Witness c k
witness (Witness c k
w :& Witnesses cs k
_) = Witness c k
Witness c k
w

-- * The testable-objects category

-- | The objects of 'TESTED': those that stand for an object of @k@ ('Untest'), with how to
-- rebuild that object's 'Ob' and 'TestOb' from the ones of its parts. This is 'Ob' for 'TESTED'.
type Tested :: forall {cs} {k}. TESTED cs k -> Constraint
class Tested (a :: TESTED cs k) where
  -- | The object of @k@ that @a@ stands for. (The class variable is re-annotated so that @k@ is
  -- in scope in the result kind.)
  type Untest (a :: TESTED cs k) :: k

  -- | The 'Ob' of the object @a@ stands for, which the structures of @k@ provide.
  untestOb :: ((Ob (Untest a)) => r) -> r

  -- | The 'TestOb' of the object @a@ stands for, which the witnesses provide.
  untestTestOb :: Witnesses cs k -> ((TestOb (Untest a)) => r) -> r

instance (Testable k, TestOb (a :: k)) => Tested (TLeaf a :: TESTED cs k) where
  type Untest (TLeaf a) = a
  untestOb :: forall r. (Ob (Untest (TLeaf a)) => r) -> r
untestOb Ob (Untest (TLeaf a)) => r
r = forall (a :: k) r. (Testable k, TestOb a) => (Ob a => r) -> r
forall {k} (a :: k) r. (Testable k, TestOb a) => (Ob a => r) -> r
obFromTestOb @a r
Ob a => r
Ob (Untest (TLeaf a)) => r
r
  untestTestOb :: forall r. Witnesses cs k -> (TestOb (Untest (TLeaf a)) => r) -> r
untestTestOb Witnesses cs k
_ TestOb (Untest (TLeaf a)) => r
r = r
TestOb (Untest (TLeaf a)) => r
r
instance (Testable k, M.Monoidal k, TestOb (M.Unit :: k)) => Tested (M.UnitF :: TESTED cs k) where
  type Untest M.UnitF = M.Unit
  untestOb :: forall r. (Ob (Untest UnitF) => r) -> r
untestOb Ob (Untest UnitF) => r
r = r
Ob (Untest UnitF) => r
r
  untestTestOb :: forall r. Witnesses cs k -> (TestOb (Untest UnitF) => r) -> r
untestTestOb Witnesses cs k
_ TestOb (Untest UnitF) => r
r = r
TestOb (Untest UnitF) => r
r
instance (HasWitness M.Monoidal cs, M.Monoidal k, Tested (a :: TESTED cs k), Tested b) => Tested (a M.**! b) where
  type Untest (a M.**! b) = Untest a M.** Untest b
  untestOb :: forall r. (Ob (Untest (a **! b)) => r) -> r
untestOb Ob (Untest (a **! b)) => r
r = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @(Untest a) @(Untest b) r
Ob (Untest a ** Untest b) => r
Ob (Untest (a **! b)) => r
r)
  untestTestOb :: forall r. Witnesses cs k -> (TestOb (Untest (a **! b)) => r) -> r
untestTestOb Witnesses cs k
ws TestOb (Untest (a **! b)) => r
r = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
Witnesses cs k
-> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
Witnesses cs k
-> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
untestTestOb2 @a @b Witnesses cs k
ws (case forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k.
HasWitness c cs =>
Witnesses cs k -> Witness c k
witness @M.Monoidal Witnesses cs k
ws of MonoidalW WithTestOb2 k
f -> WithTestOb2 k
f @(Untest a) @(Untest b) r
TestOb (Untest a ** Untest b) => r
TestOb (Untest (a **! b)) => r
r)
instance
  (HasWitness BinaryProduct.HasBinaryProducts cs, BinaryProduct.HasBinaryProducts k, Tested (a :: TESTED cs k), Tested b)
  => Tested (a BinaryProduct.*! b)
  where
  type Untest (a BinaryProduct.*! b) = Untest a BinaryProduct.&& Untest b
  untestOb :: forall r. (Ob (Untest (a *! b)) => r) -> r
untestOb Ob (Untest (a *! b)) => r
r = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
BinaryProduct.withObProd @k @(Untest a) @(Untest b) r
Ob (Untest a && Untest b) => r
Ob (Untest (a *! b)) => r
r)
  untestTestOb :: forall r. Witnesses cs k -> (TestOb (Untest (a *! b)) => r) -> r
untestTestOb Witnesses cs k
ws TestOb (Untest (a *! b)) => r
r =
    forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
Witnesses cs k
-> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
Witnesses cs k
-> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
untestTestOb2 @a @b Witnesses cs k
ws (case forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k.
HasWitness c cs =>
Witnesses cs k -> Witness c k
witness @BinaryProduct.HasBinaryProducts Witnesses cs k
ws of ProductsW WithTestObProd k
f -> WithTestObProd k
f @(Untest a) @(Untest b) r
TestOb (Untest a && Untest b) => r
TestOb (Untest (a *! b)) => r
r)
instance (Testable k, Initial.HasInitialObject k, TestOb (Initial.InitialObject :: k)) => Tested (Initial.InitF :: TESTED cs k) where
  type Untest Initial.InitF = Initial.InitialObject
  untestOb :: forall r. (Ob (Untest InitF) => r) -> r
untestOb Ob (Untest InitF) => r
r = r
Ob (Untest InitF) => r
r
  untestTestOb :: forall r. Witnesses cs k -> (TestOb (Untest InitF) => r) -> r
untestTestOb Witnesses cs k
_ TestOb (Untest InitF) => r
r = r
TestOb (Untest InitF) => r
r
instance
  ( HasWitness BinaryCoproduct.HasBinaryCoproducts cs
  , BinaryCoproduct.HasBinaryCoproducts k
  , Tested (a :: TESTED cs k)
  , Tested b
  )
  => Tested (a BinaryCoproduct.+ b)
  where
  type Untest (a BinaryCoproduct.+ b) = Untest a BinaryCoproduct.|| Untest b
  untestOb :: forall r. (Ob (Untest (a + b)) => r) -> r
untestOb Ob (Untest (a + b)) => r
r = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
BinaryCoproduct.withObCoprod @k @(Untest a) @(Untest b) r
Ob (Untest a || Untest b) => r
Ob (Untest (a + b)) => r
r)
  untestTestOb :: forall r. Witnesses cs k -> (TestOb (Untest (a + b)) => r) -> r
untestTestOb Witnesses cs k
ws TestOb (Untest (a + b)) => r
r =
    forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
Witnesses cs k
-> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
Witnesses cs k
-> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
untestTestOb2 @a @b
      Witnesses cs k
ws
      (case forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k.
HasWitness c cs =>
Witnesses cs k -> Witness c k
witness @BinaryCoproduct.HasBinaryCoproducts Witnesses cs k
ws of CoproductsW WithTestObCoprod k
f -> WithTestObCoprod k
f @(Untest a) @(Untest b) r
TestOb (Untest a || Untest b) => r
TestOb (Untest (a + b)) => r
r)

instance
  (Testable k, Terminal.HasTerminalObject k, TestOb (Terminal.TerminalObject :: k))
  => Tested (Terminal.TermF :: TESTED cs k)
  where
  type Untest Terminal.TermF = Terminal.TerminalObject
  untestOb :: forall r. (Ob (Untest TermF) => r) -> r
untestOb Ob (Untest TermF) => r
r = r
Ob (Untest TermF) => r
r
  untestTestOb :: forall r. Witnesses cs k -> (TestOb (Untest TermF) => r) -> r
untestTestOb Witnesses cs k
_ TestOb (Untest TermF) => r
r = r
TestOb (Untest TermF) => r
r
instance
  (HasWitness Exponential.Closed cs, Exponential.Closed k, Tested (a :: TESTED cs k), Tested b)
  => Tested (a Exponential.--> b)
  where
  type Untest (a Exponential.--> b) = Untest a Exponential.~~> Untest b
  untestOb :: forall r. (Ob (Untest (a --> b)) => r) -> r
untestOb Ob (Untest (a --> b)) => r
r = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
Exponential.withObExp @k @(Untest a) @(Untest b) r
Ob (Untest a ~~> Untest b) => r
Ob (Untest (a --> b)) => r
r)
  untestTestOb :: forall r. Witnesses cs k -> (TestOb (Untest (a --> b)) => r) -> r
untestTestOb Witnesses cs k
ws TestOb (Untest (a --> b)) => r
r =
    forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
Witnesses cs k
-> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
Witnesses cs k
-> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
untestTestOb2 @a @b Witnesses cs k
ws (case forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k.
HasWitness c cs =>
Witnesses cs k -> Witness c k
witness @Exponential.Closed Witnesses cs k
ws of ClosedW WithTestObExp k
f -> WithTestObExp k
f @(Untest a) @(Untest b) r
TestOb (Untest a ~~> Untest b) => r
TestOb (Untest (a --> b)) => r
r)

instance (HasWitness SA.StarAutonomous cs, SA.StarAutonomous k, Tested (a :: TESTED cs k)) => Tested (SA.DualF a) where
  type Untest (SA.DualF a) = SA.Dual (Untest a)
  untestOb :: forall r. (Ob (Untest (DualF a)) => r) -> r
untestOb Ob (Untest (DualF a)) => r
r = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
SA.withObDual @k @(Untest a) r
Ob (Dual (Untest a)) => r
Ob (Untest (DualF a)) => r
r)
  untestTestOb :: forall r. Witnesses cs k -> (TestOb (Untest (DualF a)) => r) -> r
untestTestOb Witnesses cs k
ws TestOb (Untest (DualF a)) => r
r = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
forall (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
untestTestOb @a Witnesses cs k
ws (case forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k.
HasWitness c cs =>
Witnesses cs k -> Witness c k
witness @SA.StarAutonomous Witnesses cs k
ws of StarAutonomousW WithTestObDual k
f -> WithTestObDual k
f @(Untest a) r
TestOb (Dual (Untest a)) => r
TestOb (Untest (DualF a)) => r
r)

-- | 'untestOb' of two objects at once.
untestOb2 :: forall {cs} {k} (a :: TESTED cs k) b r. (Tested a, Tested b) => ((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 :: forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 (Ob (Untest a), Ob (Untest b)) => r
r = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @b r
Ob (Untest b) => r
(Ob (Untest a), Ob (Untest b)) => r
r)

-- | 'untestTestOb' of two objects at once.
untestTestOb2
  :: forall {cs} {k} (a :: TESTED cs k) (b :: TESTED cs k) r
   . (Tested a, Tested b) => Witnesses cs k -> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
untestTestOb2 :: forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
Witnesses cs k
-> ((TestOb (Untest a), TestOb (Untest b)) => r) -> r
untestTestOb2 Witnesses cs k
ws (TestOb (Untest a), TestOb (Untest b)) => r
r = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
forall (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
untestTestOb @a Witnesses cs k
ws (forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
forall (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
untestTestOb @b Witnesses cs k
ws r
(TestOb (Untest a), TestOb (Untest b)) => r
TestOb (Untest b) => r
r)

-- | 'untestOb' of three objects at once.
untestOb3
  :: forall {cs} {k} (a :: TESTED cs k) b c r
   . (Tested a, Tested b, Tested c) => ((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestOb3 :: forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} {cs :: [Type -> Constraint]} {k}
       (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestOb3 (Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r
r = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @b (forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @c r
Ob (Untest c) => r
(Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r
r))

-- | An arrow of @k@ between the objects the endpoints stand for, with a description of how it was
-- built: an element of the hom profunctor. These are the arrows of 'TESTED'.
type TestedArr :: forall cs k. CAT (TESTED cs k)
type TestedArr @cs @k = TestedP (Hom k)

-- | 'TestedP' at the hom profunctor.
pattern TestedArr
  :: forall cs k (a :: TESTED cs k) (b :: TESTED cs k)
   . () => (Tested a, Tested b) => Doc -> Untest a ~> Untest b -> TestedArr a b
pattern $mTestedArr :: forall {r} {cs :: [Type -> Constraint]} {k} {a :: TESTED cs k}
       {b :: TESTED cs k}.
TestedArr a b
-> ((Tested a, Tested b) => Doc -> (Untest a ~> Untest b) -> r)
-> ((# #) -> r)
-> r
$bTestedArr :: forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr d f = TestedP d f

{-# COMPLETE TestedArr #-}

-- | A description that can be shown at a precedence, like 'showsPrec'.
type Doc = Int -> ShowS

-- | A name, which never needs parentheses.
atom :: String -> Doc
atom :: String -> Doc
atom String
s Int
_ = String -> ShowS
showString String
s

-- | An element or arrow described by its name.
prim :: (Tested a, Tested b) => String -> p (Untest a) (Untest b) -> TestedP p a b
prim :: forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
s = Doc -> p (Untest a) (Untest b) -> TestedP p a b
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> Doc
atom String
s)

-- | A function applied to one argument.
app :: String -> Doc -> Doc
app :: String -> Doc -> Doc
app String
f Doc
x = String -> [Doc] -> Doc
apps String
f [Item [Doc]
Doc
x]

-- | A function applied to several arguments.
apps :: String -> [Doc] -> Doc
apps :: String -> [Doc] -> Doc
apps String
f [Doc]
xs Int
d = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (String -> ShowS
showString String
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Doc -> ShowS -> ShowS) -> ShowS -> [Doc] -> ShowS
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Doc
x ShowS
r -> Char -> ShowS
showChar Char
' ' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Doc
x Int
11 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ShowS
r) (\String
r -> String
r) [Doc]
xs)

-- | A left or right associative infix operator at the given precedence, like @infixl@ and
-- @infixr@. The operator string includes its surrounding spaces, e.g. @" . "@.
infixlDoc, infixrDoc :: Int -> String -> Doc -> Doc -> Doc
infixlDoc :: Int -> String -> Doc -> Doc -> Doc
infixlDoc Int
p String
op Doc
x Doc
y Int
d = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
p) (Doc
x Int
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. String -> ShowS
showString String
op ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Doc
y (Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
infixrDoc :: Int -> String -> Doc -> Doc -> Doc
infixrDoc Int
p String
op Doc
x Doc
y Int
d = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
p) (Doc
x (Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. String -> ShowS
showString String
op ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Doc
y Int
p)

instance (CategoryOf k) => CategoryOf (TESTED cs k) where
  type (~>) = TestedArr
  type Ob a = Tested a

instance
  ( HasWitness M.Monoidal csj
  , HasWitness M.Monoidal csk
  , Testable j
  , Testable k
  , M.MonoidalProfunctor p
  , TestOb (M.Unit :: j)
  , TestOb (M.Unit :: k)
  )
  => M.MonoidalProfunctor (TestedP p :: TESTED csj j +-> TESTED csk k)
  where
  one :: TestedP p Unit Unit
one = String -> p (Untest UnitF) (Untest UnitF) -> TestedP p UnitF UnitF
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"one" p Unit Unit
p (Untest UnitF) (Untest UnitF)
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
M.one
  TestedP Doc
df p (Untest x1) (Untest x2)
f ** :: forall (x1 :: TESTED csk k) (x2 :: TESTED csj j)
       (y1 :: TESTED csk k) (y2 :: TESTED csj j).
TestedP p x1 x2
-> TestedP p y1 y2 -> TestedP p (x1 ** y1) (x2 ** y2)
** TestedP Doc
dg p (Untest y1) (Untest y2)
g = Doc
-> p (Untest (x1 **! y1)) (Untest (x2 **! y2))
-> TestedP p (x1 **! y1) (x2 **! y2)
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (Int -> String -> Doc -> Doc -> Doc
infixlDoc Int
8 String
" ** " Doc
df Doc
dg) (p (Untest x1) (Untest x2)
f p (Untest x1) (Untest x2)
-> p (Untest y1) (Untest y2)
-> p (Untest x1 ** Untest y1) (Untest x2 ** Untest y2)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** p (Untest y1) (Untest y2)
g)
instance (HasWitness M.Monoidal cs, Testable k, M.Monoidal k, TestOb (M.Unit :: k)) => M.Monoidal (TESTED cs k) where
  type Unit = M.UnitF
  type a ** b = a M.**! b
  withOb2 :: forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: TESTED cs k). Ob a => (Unit ** a) ~> a
leftUnitor @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest (UnitF **! a) ~> Untest a)
-> TestedP (~>) (UnitF **! a) a
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"leftUnitor" (Unit ** Untest a) ~> Untest a
Untest (UnitF **! a) ~> Untest a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
M.leftUnitor)
  leftUnitorInv :: forall (a :: TESTED cs k). Ob a => a ~> (Unit ** a)
leftUnitorInv @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest a ~> Untest (UnitF **! a))
-> TestedP (~>) a (UnitF **! a)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"leftUnitorInv" Untest a ~> (Unit ** Untest a)
Untest a ~> Untest (UnitF **! a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
M.leftUnitorInv)
  rightUnitor :: forall (a :: TESTED cs k). Ob a => (a ** Unit) ~> a
rightUnitor @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest (a **! UnitF) ~> Untest a)
-> TestedP (~>) (a **! UnitF) a
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"rightUnitor" (Untest a ** Unit) ~> Untest a
Untest (a **! UnitF) ~> Untest a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
M.rightUnitor)
  rightUnitorInv :: forall (a :: TESTED cs k). Ob a => a ~> (a ** Unit)
rightUnitorInv @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest a ~> Untest (a **! UnitF))
-> TestedP (~>) a (a **! UnitF)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"rightUnitorInv" Untest a ~> (Untest a ** Unit)
Untest a ~> Untest (a **! UnitF)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
M.rightUnitorInv)
  associator :: forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} {cs :: [Type -> Constraint]} {k}
       (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestOb3 @a @b @c (String
-> (Untest ((a **! b) **! c) ~> Untest (a **! (b **! c)))
-> TestedP (~>) ((a **! b) **! c) (a **! (b **! c))
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"associator" (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
M.associator @k @(Untest a) @(Untest b) @(Untest c)))
  associatorInv :: forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} {cs :: [Type -> Constraint]} {k}
       (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestOb3 @a @b @c (String
-> (Untest (a **! (b **! c)) ~> Untest ((a **! b) **! c))
-> TestedP (~>) (a **! (b **! c)) ((a **! b) **! c)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"associatorInv" (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
M.associatorInv @k @(Untest a) @(Untest b) @(Untest c)))
instance (HasWitness M.Monoidal cs, Testable k, M.SymMonoidal k, TestOb (M.Unit :: k)) => M.SymMonoidal (TESTED cs k) where
  swap :: forall (a :: TESTED cs k) (b :: TESTED cs k).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @a @b = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (String
-> (Untest (a **! b) ~> Untest (b **! a))
-> TestedP (~>) (a **! b) (b **! a)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"swap" (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @k @(Untest a) @(Untest b)))

instance
  (HasWitness BinaryProduct.HasBinaryProducts cs, BinaryProduct.HasBinaryProducts k)
  => BinaryProduct.HasBinaryProducts (TESTED cs k)
  where
  type a && b = a BinaryProduct.*! b
  withObProd :: forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: TESTED cs k) (b :: TESTED cs k).
(Ob a, Ob b) =>
(a && b) ~> a
fst @a @b = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (String -> (Untest (a *! b) ~> Untest a) -> TestedP (~>) (a *! b) a
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"fst" (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
BinaryProduct.fst @k @(Untest a) @(Untest b)))
  snd :: forall (a :: TESTED cs k) (b :: TESTED cs k).
(Ob a, Ob b) =>
(a && b) ~> b
snd @a @b = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (String -> (Untest (a *! b) ~> Untest b) -> TestedP (~>) (a *! b) b
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"snd" (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
BinaryProduct.snd @k @(Untest a) @(Untest b)))
  TestedArr Doc
df Untest a ~> Untest x
f &&& :: forall (a :: TESTED cs k) (x :: TESTED cs k) (y :: TESTED cs k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& TestedArr Doc
dg Untest a ~> Untest y
g = Doc -> (Untest a ~> Untest (x *! y)) -> TestedArr a (x *! y)
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (Int -> String -> Doc -> Doc -> Doc
infixlDoc Int
5 String
" &&& " Doc
df Doc
dg) (Untest a ~> Untest x
f (Untest a ~> Untest x)
-> (Untest a ~> Untest y) -> Untest a ~> (Untest x && Untest y)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
BinaryProduct.&&& Untest a ~> Untest y
g)

instance (Testable k, Initial.HasInitialObject k, TestOb (Initial.InitialObject :: k)) => Initial.HasInitialObject (TESTED cs k) where
  type InitialObject = Initial.InitF
  initiate :: forall (a :: TESTED cs k). Ob a => InitialObject ~> a
initiate @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String -> (Untest InitF ~> Untest a) -> TestedP (~>) InitF a
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"initiate" InitialObject ~> Untest a
Untest InitF ~> Untest a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
Initial.initiate)

instance
  (HasWitness BinaryCoproduct.HasBinaryCoproducts cs, BinaryCoproduct.HasBinaryCoproducts k)
  => BinaryCoproduct.HasBinaryCoproducts (TESTED cs k)
  where
  type a || b = a BinaryCoproduct.+ b
  withObCoprod :: forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: TESTED cs k) (b :: TESTED cs k).
(Ob a, Ob b) =>
a ~> (a || b)
lft @a @b = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (String -> (Untest a ~> Untest (a + b)) -> TestedP (~>) a (a + b)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"lft" (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
BinaryCoproduct.lft @k @(Untest a) @(Untest b)))
  rgt :: forall (a :: TESTED cs k) (b :: TESTED cs k).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @a @b = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (String -> (Untest b ~> Untest (a + b)) -> TestedP (~>) b (a + b)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"rgt" (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
BinaryCoproduct.rgt @k @(Untest a) @(Untest b)))
  TestedArr Doc
df Untest x ~> Untest a
f ||| :: forall (x :: TESTED cs k) (a :: TESTED cs k) (y :: TESTED cs k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| TestedArr Doc
dg Untest y ~> Untest a
g = Doc -> (Untest (x + y) ~> Untest a) -> TestedArr (x + y) a
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (Int -> String -> Doc -> Doc -> Doc
infixlDoc Int
4 String
" ||| " Doc
df Doc
dg) (Untest x ~> Untest a
f (Untest x ~> Untest a)
-> (Untest y ~> Untest a) -> (Untest x || Untest y) ~> Untest a
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
BinaryCoproduct.||| Untest y ~> Untest a
g)

instance
  ( HasWitness M.Monoidal cs
  , HasWitness BinaryCoproduct.HasBinaryCoproducts cs
  , Testable k
  , Distributive.Distributive k
  , TestOb (M.Unit :: k)
  , TestOb (Initial.InitialObject :: k)
  )
  => Distributive.Distributive (TESTED cs k)
  where
  distL :: forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} {cs :: [Type -> Constraint]} {k}
       (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestOb3 @a @b @c (String
-> (Untest (a **! (b + c)) ~> Untest ((a **! b) + (a **! c)))
-> TestedP (~>) (a **! (b + c)) ((a **! b) + (a **! c))
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"distL" (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
Distributive.distL @k @(Untest a) @(Untest b) @(Untest c)))
  distR :: forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} {cs :: [Type -> Constraint]} {k}
       (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestOb3 @a @b @c (String
-> (Untest ((a + b) **! c) ~> Untest ((a **! c) + (b **! c)))
-> TestedP (~>) ((a + b) **! c) ((a **! c) + (b **! c))
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"distR" (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
Distributive.distR @k @(Untest a) @(Untest b) @(Untest c)))
  absorbL :: forall (a :: TESTED cs k).
Ob a =>
(a ** InitialObject) ~> InitialObject
absorbL @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest (a **! InitF) ~> Untest InitF)
-> TestedP (~>) (a **! InitF) InitF
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"absorbL" (forall k (a :: k).
(Distributive k, Ob a) =>
(a ** InitialObject) ~> InitialObject
Distributive.absorbL @k @(Untest a)))
  absorbR :: forall (a :: TESTED cs k).
Ob a =>
(InitialObject ** a) ~> InitialObject
absorbR @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest (InitF **! a) ~> Untest InitF)
-> TestedP (~>) (InitF **! a) InitF
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"absorbR" (forall k (a :: k).
(Distributive k, Ob a) =>
(InitialObject ** a) ~> InitialObject
Distributive.absorbR @k @(Untest a)))

instance
  (Testable k, Terminal.HasTerminalObject k, TestOb (Terminal.TerminalObject :: k))
  => Terminal.HasTerminalObject (TESTED cs k)
  where
  type TerminalObject = Terminal.TermF
  terminate :: forall (a :: TESTED cs k). Ob a => a ~> TerminalObject
terminate @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String -> (Untest a ~> Untest TermF) -> TestedP (~>) a TermF
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"terminate" Untest a ~> TerminalObject
Untest a ~> Untest TermF
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
Terminal.terminate)

instance
  (HasWitness M.Monoidal cs, HasWitness Exponential.Closed cs, Testable k, Exponential.Closed k, TestOb (M.Unit :: k))
  => Exponential.Closed (TESTED cs k)
  where
  type a ~~> b = a Exponential.--> b
  withObExp :: forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @a @b (TestedArr Doc
df Untest (a **! b) ~> Untest c
f) = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (Doc -> (Untest a ~> Untest (b --> c)) -> TestedP (~>) a (b --> c)
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"curry" Doc
df) (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
Exponential.curry @k @(Untest a) @(Untest b) (Untest a ** Untest b) ~> Untest c
Untest (a **! b) ~> Untest c
f))
  apply :: forall (a :: TESTED cs k) (b :: TESTED cs k).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @a @b = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (String
-> (Untest ((a --> b) **! a) ~> Untest b)
-> TestedP (~>) ((a --> b) **! a) b
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"apply" (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
Exponential.apply @k @(Untest a) @(Untest b)))

  -- '^^^' is infixl 9 and '.' infixr 9, so '^^^' is parenthesized under either side of '.'.
  TestedArr Doc
df Untest b ~> Untest y
f ^^^ :: forall (a :: TESTED cs k) (b :: TESTED cs k) (x :: TESTED cs k)
       (y :: TESTED cs k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ TestedArr Doc
dg Untest x ~> Untest a
g =
    Doc
-> (Untest (a --> b) ~> Untest (x --> y))
-> TestedArr (a --> b) (x --> y)
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (\Int
d -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
9) (Doc
df Int
9 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. String -> ShowS
showString String
" ^^^ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Doc
dg Int
10)) (Untest b ~> Untest y
f (Untest b ~> Untest y)
-> (Untest x ~> Untest a)
-> (Untest a ~~> Untest b) ~> (Untest x ~~> Untest y)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
Exponential.^^^ Untest x ~> Untest a
g)

instance
  ( HasWitness M.Monoidal cs
  , HasWitness Exponential.Closed cs
  , HasWitness SA.StarAutonomous cs
  , Testable k
  , SA.StarAutonomous k
  , TestOb (M.Unit :: k)
  )
  => SA.StarAutonomous (TESTED cs k)
  where
  type Dual a = SA.DualF a
  withObDual :: forall (a :: TESTED cs k) r. Ob a => (Ob (Dual a) => r) -> r
withObDual Ob (Dual a) => r
r = r
Ob (Dual a) => r
r
  dual :: forall (a :: TESTED cs k) (b :: TESTED cs k).
(a ~> b) -> Dual b ~> Dual a
dual (TestedArr Doc
df Untest a ~> Untest b
f) = Doc
-> (Untest (DualF b) ~> Untest (DualF a))
-> TestedArr (DualF b) (DualF a)
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"dual" Doc
df) ((Untest a ~> Untest b) -> Dual (Untest b) ~> Dual (Untest a)
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
SA.dual Untest a ~> Untest b
f)
  dualInv :: forall (a :: TESTED cs k) (b :: TESTED cs k).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv @a @b (TestedArr Doc
df Untest (DualF a) ~> Untest (DualF b)
f) = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (Doc -> (Untest b ~> Untest a) -> TestedP (~>) b a
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"dualInv" Doc
df) (forall k (a :: k) (b :: k).
(StarAutonomous k, Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
SA.dualInv @k @(Untest a) @(Untest b) Dual (Untest a) ~> Dual (Untest b)
Untest (DualF a) ~> Untest (DualF b)
f))
  linDist :: forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @a @b @c (TestedArr Doc
df Untest (a **! b) ~> Untest (DualF c)
f) =
    forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} {cs :: [Type -> Constraint]} {k}
       (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestOb3 @a @b @c (Doc
-> (Untest a ~> Untest (DualF (b **! c)))
-> TestedP (~>) a (DualF (b **! c))
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"linDist" Doc
df) (forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
SA.linDist @k @(Untest a) @(Untest b) @(Untest c) (Untest a ** Untest b) ~> Dual (Untest c)
Untest (a **! b) ~> Untest (DualF c)
f))
  linDistInv :: forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @a @b @c (TestedArr Doc
df Untest a ~> Untest (DualF (b **! c))
f) =
    forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} {cs :: [Type -> Constraint]} {k}
       (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestOb3 @a @b @c (Doc
-> (Untest (a **! b) ~> Untest (DualF c))
-> TestedP (~>) (a **! b) (DualF c)
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"linDistInv" Doc
df) (forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
SA.linDistInv @k @(Untest a) @(Untest b) @(Untest c) Untest a ~> Dual (Untest b ** Untest c)
Untest a ~> Untest (DualF (b **! c))
f))
  doubleNeg :: forall (a :: TESTED cs k). Ob a => Dual (Dual a) ~> a
doubleNeg @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest (DualF (DualF a)) ~> Untest a)
-> TestedP (~>) (DualF (DualF a)) a
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"doubleNeg" (forall k (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
SA.doubleNeg @k @(Untest a)))
  doubleNegInv :: forall (a :: TESTED cs k). Ob a => a ~> Dual (Dual a)
doubleNegInv @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest a ~> Untest (DualF (DualF a)))
-> TestedP (~>) a (DualF (DualF a))
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"doubleNegInv" (forall k (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
SA.doubleNegInv @k @(Untest a)))

instance
  ( HasWitness M.Monoidal cs
  , HasWitness Exponential.Closed cs
  , HasWitness SA.StarAutonomous cs
  , Testable k
  , CC.CompactClosed k
  , TestOb (M.Unit :: k)
  )
  => CC.CompactClosed (TESTED cs k)
  where
  distribDual :: forall (a :: TESTED cs k) (b :: TESTED cs k).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @a @b = forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) r.
(Tested a, Tested b) =>
((Ob (Untest a), Ob (Untest b)) => r) -> r
untestOb2 @a @b (String
-> (Untest (DualF (a **! b)) ~> Untest (DualF a **! DualF b))
-> TestedP (~>) (DualF (a **! b)) (DualF a **! DualF b)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"distribDual" (forall k (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
CC.distribDual @k @(Untest a) @(Untest b)))
  dualUnit :: Dual Unit ~> Unit
dualUnit = String
-> (Untest (DualF UnitF) ~> Untest UnitF)
-> TestedP (~>) (DualF UnitF) UnitF
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"dualUnit" Dual Unit ~> Unit
Untest (DualF UnitF) ~> Untest UnitF
forall k. CompactClosed k => Dual Unit ~> Unit
CC.dualUnit
  dualityUnit :: forall (a :: TESTED cs k). Ob a => Unit ~> (a ** Dual a)
dualityUnit @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest UnitF ~> Untest (a **! DualF a))
-> TestedP (~>) UnitF (a **! DualF a)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"dualityUnit" (forall k (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
CC.dualityUnit @k @(Untest a)))
  dualityCounit :: forall (a :: TESTED cs k). Ob a => (Dual a ** a) ~> Unit
dualityCounit @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest (DualF a **! a) ~> Untest UnitF)
-> TestedP (~>) (DualF a **! a) UnitF
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"dualityCounit" (forall k (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
CC.dualityCounit @k @(Untest a)))

-- | Every object is a monoid when the category supplies them, with the monoid of the object it
-- stands for.
instance
  (HasWitness M.Monoidal cs, Testable k, M.Monoidal k, Monoid.Supplies Monoid.Monoid k, TestOb (M.Unit :: k), Tested a)
  => Monoid.Monoid (a :: TESTED cs k)
  where
  mempty :: Unit ~> a
mempty = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String -> (Untest UnitF ~> Untest a) -> TestedP (~>) UnitF a
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"mempty" (forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
Monoid.mempty @(Untest a)))
  mappend :: (a ** a) ~> a
mappend = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest (a **! a) ~> Untest a) -> TestedP (~>) (a **! a) a
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"mappend" (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend @(Untest a)))

-- | Every object is a comonoid when the category supplies them.
instance
  (HasWitness M.Monoidal cs, Testable k, M.Monoidal k, Monoid.Supplies Monoid.Comonoid k, TestOb (M.Unit :: k), Tested a)
  => Monoid.Comonoid (a :: TESTED cs k)
  where
  counit :: a ~> Unit
counit = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String -> (Untest a ~> Untest UnitF) -> TestedP (~>) a UnitF
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"counit" (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
Monoid.counit @(Untest a)))
  comult :: a ~> (a ** a)
comult = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest a ~> Untest (a **! a)) -> TestedP (~>) a (a **! a)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"comult" (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
Monoid.comult @(Untest a)))

-- | The monoids of a category that supplies commutative ones are commutative.
instance
  ( HasWitness M.Monoidal cs
  , Testable k
  , M.SymMonoidal k
  , Monoid.Supplies Monoid.CommutativeMonoid k
  , TestOb (M.Unit :: k)
  , Tested a
  )
  => Monoid.CommutativeMonoid (a :: TESTED cs k)

-- | The comonoids of a category that supplies cocommutative ones are cocommutative.
instance
  ( HasWitness M.Monoidal cs
  , Testable k
  , M.SymMonoidal k
  , Monoid.Supplies Monoid.CocommutativeComonoid k
  , TestOb (M.Unit :: k)
  , Tested a
  )
  => Monoid.CocommutativeComonoid (a :: TESTED cs k)

-- | 'Strength.act' of the tensor of @p@.
instance
  (HasWitness M.Monoidal cs, Testable k, M.Monoidal k, Strength.Strong M.Tensor p, TestOb (M.Unit :: k))
  => Strength.Strong M.Tensor (TestedP p :: CAT (TESTED cs k))
  where
  act :: forall (a :: TESTED cs k) (x :: TESTED cs k) (y :: TESTED cs k).
Ob a =>
TestedP p x y -> TestedP p (Act Tensor a x) (Act Tensor a y)
act @a (TestedP Doc
dx p (Untest x) (Untest y)
x) = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (Doc
-> p (Untest (a **! x)) (Untest (a **! y))
-> TestedP p (a **! x) (a **! y)
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> Doc -> Doc
app String
"act" Doc
dx) (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
Strength.act @M.Tensor @p @(Untest a) p (Untest x) (Untest y)
x))

-- | 'Strength.coact' over the tensor of @p@, e.g. the trace of the category the objects stand for.
instance
  (HasWitness M.Monoidal cs, Testable k, M.Monoidal k, Strength.Costrong M.Tensor p, TestOb (M.Unit :: k))
  => Strength.Costrong M.Tensor (TestedP p :: CAT (TESTED cs k))
  where
  coact :: forall (a :: TESTED cs k) (x :: TESTED cs k) (y :: TESTED cs k).
(Ob a, Ob x, Ob y) =>
TestedP p (Act Tensor a x) (Act Tensor a y) -> TestedP p x y
coact @a @x @y (TestedP Doc
df p (Untest (Act Tensor a x)) (Untest (Act Tensor a y))
f) =
    forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} {cs :: [Type -> Constraint]} {k}
       (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
forall (a :: TESTED cs k) (b :: TESTED cs k) (c :: TESTED cs k) r.
(Tested a, Tested b, Tested c) =>
((Ob (Untest a), Ob (Untest b), Ob (Untest c)) => r) -> r
untestOb3 @a @x @y (Doc -> p (Untest x) (Untest y) -> TestedP p x y
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> Doc -> Doc
app String
"coact" Doc
df) (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
Strength.coact @M.Tensor @p @(Untest a) @(Untest x) @(Untest y) p (Act Tensor (Untest a) (Untest x))
  (Act Tensor (Untest a) (Untest y))
p (Untest (Act Tensor a x)) (Untest (Act Tensor a y))
f))

-- | Copying and discarding in the category the objects stand for.
instance
  (HasWitness M.Monoidal cs, Testable k, CopyDiscard.CopyDiscard k, TestOb (M.Unit :: k))
  => CopyDiscard.CopyDiscard (TESTED cs k)
  where
  copy :: forall (a :: TESTED cs k). Ob a => a ~> (a ** a)
copy @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> (Untest a ~> Untest (a **! a)) -> TestedP (~>) a (a **! a)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"copy" (forall k (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
CopyDiscard.copy @k @(Untest a)))
  discard :: forall (a :: TESTED cs k). Ob a => a ~> Unit
discard @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String -> (Untest a ~> Untest UnitF) -> TestedP (~>) a UnitF
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"discard" (forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
CopyDiscard.discard @k @(Untest a)))

instance (CategoryOf k) => Laws.Labelled (TESTED cs k) where
  label :: forall (a :: TESTED cs k) (b :: TESTED cs k).
String -> (a ~> b) -> a ~> b
label String
s (TestedArr Doc
_ Untest a ~> Untest b
f) = String -> (Untest a ~> Untest b) -> TestedArr a b
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
s Untest a ~> Untest b
f

-- * The testable-objects profunctor

-- | An element of @p@ between the objects the endpoints stand for, with a description of how it
-- was built, for printing a failing law.
type TestedP :: forall {csj} {csk} {j} {k}. (j +-> k) -> TESTED csj j +-> TESTED csk k
data TestedP p a b where
  TestedP :: (Tested a, Tested b) => Doc -> p (Untest a) (Untest b) -> TestedP p a b

instance (Profunctor p) => Profunctor (TestedP p :: TESTED csj j +-> TESTED csk k) where
  dimap :: forall (c :: TESTED csk k) (a :: TESTED csk k) (b :: TESTED csj j)
       (d :: TESTED csj j).
(c ~> a) -> (b ~> d) -> TestedP p a b -> TestedP p c d
dimap (TestedArr Doc
df Untest c ~> Untest a
f) (TestedArr Doc
dg Untest b ~> Untest d
g) (TestedP Doc
dx p (Untest a) (Untest b)
x) = Doc -> p (Untest c) (Untest d) -> TestedP p c d
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> [Doc] -> Doc
apps String
"dimap" [Item [Doc]
Doc
df, Item [Doc]
Doc
dg, Item [Doc]
Doc
dx]) ((Untest c ~> Untest a)
-> (Untest b ~> Untest d)
-> p (Untest a) (Untest b)
-> p (Untest c) (Untest d)
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap Untest c ~> Untest a
f Untest b ~> Untest d
g p (Untest a) (Untest b)
x)
  lmap :: forall (c :: TESTED csk k) (a :: TESTED csk k) (b :: TESTED csj j).
(c ~> a) -> TestedP p a b -> TestedP p c b
lmap (TestedArr Doc
df Untest c ~> Untest a
f) (TestedP Doc
dx p (Untest a) (Untest b)
x) = Doc -> p (Untest c) (Untest b) -> TestedP p c b
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> [Doc] -> Doc
apps String
"lmap" [Item [Doc]
Doc
df, Item [Doc]
Doc
dx]) ((Untest c ~> Untest a)
-> p (Untest a) (Untest b) -> p (Untest c) (Untest b)
forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap Untest c ~> Untest a
f p (Untest a) (Untest b)
x)
  rmap :: forall (b :: TESTED csj j) (d :: TESTED csj j) (a :: TESTED csk k).
(b ~> d) -> TestedP p a b -> TestedP p a d
rmap (TestedArr Doc
dg Untest b ~> Untest d
g) (TestedP Doc
dx p (Untest a) (Untest b)
x) = Doc -> p (Untest a) (Untest d) -> TestedP p a d
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> [Doc] -> Doc
apps String
"rmap" [Item [Doc]
Doc
dg, Item [Doc]
Doc
dx]) ((Untest b ~> Untest d)
-> p (Untest a) (Untest b) -> p (Untest a) (Untest d)
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap Untest b ~> Untest d
g p (Untest a) (Untest b)
x)
  (Ob a, Ob b) => r
r \\ :: forall (a :: TESTED csk k) (b :: TESTED csj j) r.
((Ob a, Ob b) => r) -> TestedP p a b -> r
\\ TestedP{} = r
(Ob a, Ob b) => r
r

instance (Promonad p) => Promonad (TestedP p :: CAT (TESTED cs k)) where
  id :: forall (a :: TESTED cs k). Ob a => TestedP p a a
id @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED cs k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String -> p (Untest a) (Untest a) -> TestedP p a a
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"id" p (Untest a) (Untest a)
forall (a :: k). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
  TestedP Doc
dy p (Untest b) (Untest c)
y . :: forall (b :: TESTED cs k) (c :: TESTED cs k) (a :: TESTED cs k).
TestedP p b c -> TestedP p a b -> TestedP p a c
. TestedP Doc
dx p (Untest a) (Untest b)
x = Doc -> p (Untest a) (Untest c) -> TestedP p a c
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (Int -> String -> Doc -> Doc -> Doc
infixrDoc Int
9 String
" . " Doc
dy Doc
dx) (p (Untest b) (Untest c)
y p (Untest b) (Untest c)
-> p (Untest a) (Untest b) -> p (Untest a) (Untest c)
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p (Untest a) (Untest b)
x)

-- | The object @p '%' b@, for the interpretation of a 'Representable' @p@.
type RepF :: forall {csj} {j} {k} {o}. (j +-> k) -> TESTED csj j -> o
data family RepF p b

-- | The structure of being closed under the representing functor of @p@, whose objects in 'TESTED'
-- are formed by 'RepF'. Its witness needs the witnesses of the domain @j@ of @p@, @csj@.
type RepresentedBy :: forall {j} {k}. [Kind -> Constraint] -> (j +-> k) -> Kind -> Constraint
class RepresentedBy csj p k'

instance RepresentedBy csj p k'

data instance Witness (RepresentedBy csj (p :: j +-> k)) k' = RepresentedW (Witnesses csj j) (WithTestObRep j p)

instance
  (HasWitness (RepresentedBy csj p) csk, Representable p, Tested (b :: TESTED csj j))
  => Tested (RepF (p :: j +-> k) b :: TESTED csk k)
  where
  type Untest (RepF p b) = p % Untest b
  untestOb :: forall r. (Ob (Untest (RepF p b)) => r) -> r
untestOb Ob (Untest (RepF p b)) => r
r = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csj j) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @b (forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @(Untest b) r
Ob (p % Untest b) => r
Ob (Untest (RepF p b)) => r
r)
  untestTestOb :: forall r. Witnesses csk k -> (TestOb (Untest (RepF p b)) => r) -> r
untestTestOb Witnesses csk k
ws TestOb (Untest (RepF p b)) => r
r = case forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k.
HasWitness c cs =>
Witnesses cs k -> Witness c k
witness @(RepresentedBy csj p) Witnesses csk k
ws of
    RepresentedW Witnesses csj j
wsj WithTestObRep j p
f -> forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
forall (a :: TESTED csj j) r.
Tested a =>
Witnesses csj j -> (TestOb (Untest a) => r) -> r
untestTestOb @b Witnesses csj j
wsj (WithTestObRep j p
f @(Untest b) r
TestOb (p % Untest b) => r
TestOb (Untest (RepF p b)) => r
r)

instance
  (HasWitness (RepresentedBy csj p) csk, Representable p)
  => Representable (TestedP p :: TESTED csj j +-> TESTED csk k)
  where
  type TestedP p % b = RepF p b
  index :: forall (a :: TESTED csk k) (b :: TESTED csj j).
TestedP p a b -> a ~> (TestedP p % b)
index (TestedP Doc
dx p (Untest a) (Untest b)
x) = Doc -> (Untest a ~> Untest (RepF p b)) -> TestedArr a (RepF p b)
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"index" Doc
dx) (p (Untest a) (Untest b) -> Untest a ~> (p % Untest b)
forall (a :: k) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p (Untest a) (Untest b)
x)
  tabulate :: forall (b :: TESTED csj j) (a :: TESTED csk k).
Ob b =>
(a ~> (TestedP p % b)) -> TestedP p a b
tabulate @b (TestedArr Doc
df Untest a ~> Untest (RepF p b)
f) = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csj j) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @b (Doc -> p (Untest a) (Untest b) -> TestedP p a b
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> Doc -> Doc
app String
"tabulate" Doc
df) (forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate @p @(Untest b) Untest a ~> (p % Untest b)
Untest a ~> Untest (RepF p b)
f))
  repMap :: forall (a :: TESTED csj j) (b :: TESTED csj j).
(a ~> b) -> (TestedP p % a) ~> (TestedP p % b)
repMap (TestedArr Doc
df Untest a ~> Untest b
f) = Doc
-> (Untest (RepF p a) ~> Untest (RepF p b))
-> TestedArr (RepF p a) (RepF p b)
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"repMap" Doc
df) (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p Untest a ~> Untest b
f)
  repUniv :: forall (a :: TESTED csj j). Ob a => TestedP p (TestedP p % a) a
repUniv @b = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csj j) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @b (String
-> p (Untest (RepF p a)) (Untest a) -> TestedP p (RepF p a) a
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"repUniv" (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv @p @(Untest b)))

-- | The object @p '%%' a@, for the interpretation of a 'Corepresentable' @p@.
type CorepF :: forall {csk} {j} {k} {o}. (j +-> k) -> TESTED csk k -> o
data family CorepF p a

-- | The structure of being closed under the corepresenting functor of @p@, whose objects in
-- 'TESTED' are formed by 'CorepF'. Its witness needs the witnesses of the codomain @k@ of @p@,
-- @csk@.
type CorepresentedBy :: forall {j} {k}. [Kind -> Constraint] -> (j +-> k) -> Kind -> Constraint
class CorepresentedBy csk p j'

instance CorepresentedBy csk p j'

data instance Witness (CorepresentedBy csk (p :: j +-> k)) j' = CorepresentedW (Witnesses csk k) (WithTestObCorep k p)

instance
  (HasWitness (CorepresentedBy csk p) csj, Corepresentable p, Tested (a :: TESTED csk k))
  => Tested (CorepF (p :: j +-> k) a :: TESTED csj j)
  where
  type Untest (CorepF p a) = p %% Untest a
  untestOb :: forall r. (Ob (Untest (CorepF p a)) => r) -> r
untestOb Ob (Untest (CorepF p a)) => r
r = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csk k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
forall (p :: j +-> k) (a :: k) r.
(Corepresentable p, Ob a) =>
(Ob (p %% a) => r) -> r
withObCorep @p @(Untest a) r
Ob (p %% Untest a) => r
Ob (Untest (CorepF p a)) => r
r)
  untestTestOb :: forall r.
Witnesses csj j -> (TestOb (Untest (CorepF p a)) => r) -> r
untestTestOb Witnesses csj j
ws TestOb (Untest (CorepF p a)) => r
r = case forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k.
HasWitness c cs =>
Witnesses cs k -> Witness c k
witness @(CorepresentedBy csk p) Witnesses csj j
ws of
    CorepresentedW Witnesses csk k
wsk WithTestObCorep k p
f -> forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
Witnesses cs k -> (TestOb (Untest a) => r) -> r
forall (a :: TESTED csk k) r.
Tested a =>
Witnesses csk k -> (TestOb (Untest a) => r) -> r
untestTestOb @a Witnesses csk k
wsk (WithTestObCorep k p
f @(Untest a) r
TestOb (p %% Untest a) => r
TestOb (Untest (CorepF p a)) => r
r)

instance
  (HasWitness (CorepresentedBy csk p) csj, Corepresentable p)
  => Corepresentable (TestedP p :: TESTED csj j +-> TESTED csk k)
  where
  type TestedP p %% a = CorepF p a
  coindex :: forall (a :: TESTED csk k) (b :: TESTED csj j).
TestedP p a b -> (TestedP p %% a) ~> b
coindex (TestedP Doc
dx p (Untest a) (Untest b)
x) = Doc
-> (Untest (CorepF p a) ~> Untest b) -> TestedArr (CorepF p a) b
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"coindex" Doc
dx) (p (Untest a) (Untest b) -> (p %% Untest a) ~> Untest b
forall (a :: k) (b :: j). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex p (Untest a) (Untest b)
x)
  cotabulate :: forall (a :: TESTED csk k) (b :: TESTED csj j).
Ob a =>
((TestedP p %% a) ~> b) -> TestedP p a b
cotabulate @a (TestedArr Doc
df Untest (CorepF p a) ~> Untest b
f) = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csk k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (Doc -> p (Untest a) (Untest b) -> TestedP p a b
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> Doc -> Doc
app String
"cotabulate" Doc
df) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate @p @(Untest a) (p %% Untest a) ~> Untest b
Untest (CorepF p a) ~> Untest b
f))
  corepMap :: forall (a :: TESTED csk k) (b :: TESTED csk k).
(a ~> b) -> (TestedP p %% a) ~> (TestedP p %% b)
corepMap (TestedArr Doc
df Untest a ~> Untest b
f) = Doc
-> (Untest (CorepF p a) ~> Untest (CorepF p b))
-> TestedArr (CorepF p a) (CorepF p b)
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"corepMap" Doc
df) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p Untest a ~> Untest b
f)
  corepUniv :: forall (a :: TESTED csk k). Ob a => TestedP p a (TestedP p %% a)
corepUniv @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csk k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (String
-> p (Untest a) (Untest (CorepF p a)) -> TestedP p a (CorepF p a)
forall {csk :: [Type -> Constraint]} {k}
       {csj :: [Type -> Constraint]} {j} (a :: TESTED csk k)
       (b :: TESTED csj j) (p :: k -> j -> Type).
(Tested a, Tested b) =>
String -> p (Untest a) (Untest b) -> TestedP p a b
prim String
"corepUniv" (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv @p @(Untest a)))

instance (DaggerProfunctor p) => DaggerProfunctor (TestedP p :: CAT (TESTED cs k)) where
  dagger :: forall (a :: TESTED cs k) (b :: TESTED cs k).
TestedP p a b -> TestedP p b a
dagger (TestedP Doc
d p (Untest a) (Untest b)
x) = Doc -> p (Untest b) (Untest a) -> TestedP p b a
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> Doc -> Doc
app String
"dagger" Doc
d) (p (Untest a) (Untest b) -> p (Untest b) (Untest a)
forall (a :: k) (b :: k). p a b -> p b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger p (Untest a) (Untest b)
x)

instance (Finitary p) => Finitary (TestedP p :: TESTED csj j +-> TESTED csk k) where
  size :: forall (a :: TESTED csk k) (b :: TESTED csj j).
(Ob a, Ob b) =>
Natural
size @a @b = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csk k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csj j) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @b (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
size @p @(Untest a) @(Untest b)))
  toIndex :: forall (a :: TESTED csk k) (b :: TESTED csj j).
(Ob a, Ob b) =>
TestedP p a b -> Natural
toIndex @a @b (TestedP Doc
_ p (Untest a) (Untest b)
x) = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csk k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csj j) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @b (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex @p @(Untest a) @(Untest b) p (Untest a) (Untest b)
x))
  fromIndex :: forall (a :: TESTED csk k) (b :: TESTED csj j).
(Ob a, Ob b) =>
Natural -> TestedP p a b
fromIndex @a @b Natural
i = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csk k) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a (forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csj j) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @b (Doc -> p (Untest a) (Untest b) -> TestedP p a b
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> Doc -> Doc
app String
"fromIndex" (\Int
_ -> Natural -> ShowS
forall a. Show a => a -> ShowS
shows Natural
i)) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex @p @(Untest a) @(Untest b) Natural
i)))

-- | The adjunction of the profunctors the objects stand for. The middle object of the 'Adj.unit'
-- is only known to be an object, so it becomes a leaf, which needs 'TestOb' to follow from 'Ob'.
instance
  (Adj.Proadjunction p q, Testable j, Testable k, TestObIsOb j, TestObIsOb k)
  => Adj.Proadjunction (TestedP p :: TESTED csj j +-> TESTED csk k) (TestedP q :: TESTED csk k +-> TESTED csj j)
  where
  unit :: forall (a :: TESTED csj j).
Ob a =>
(:.:) (TestedP q) (TestedP p) a a
unit @a = forall {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k) r.
Tested a =>
(Ob (Untest a) => r) -> r
forall (a :: TESTED csj j) r. Tested a => (Ob (Untest a) => r) -> r
untestOb @a case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
Adj.unit @p @q @(Untest a) of
    (:.:) @m q (Untest a) b
l p b (Untest a)
r -> (forall (m :: k) (x :: TESTED csj j).
TestedP q x (TLeaf m) -> TestedP q x (TLeaf m)
leaf @m (Doc -> q (Untest a) (Untest (TLeaf b)) -> TestedP q a (TLeaf b)
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> Doc
atom String
"unitQ") q (Untest a) b
q (Untest a) (Untest (TLeaf b))
l) TestedP q a (TLeaf b)
-> TestedP p (TLeaf b) a -> (:.:) (TestedP q) (TestedP p) a a
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Doc -> p (Untest (TLeaf b)) (Untest a) -> TestedP p (TLeaf b) a
forall {cs :: [Type -> Constraint]} {k}
       {cs :: [Type -> Constraint]} {k} (a :: TESTED cs k)
       (b :: TESTED cs k) (p :: k +-> k).
(Tested a, Tested b) =>
Doc -> p (Untest a) (Untest b) -> TestedP p a b
TestedP (String -> Doc
atom String
"unitP") p b (Untest a)
p (Untest (TLeaf b)) (Untest a)
r) ((Ob (Untest a), Ob b) => (:.:) (TestedP q) (TestedP p) a a)
-> q (Untest a) b -> (:.:) (TestedP q) (TestedP p) a a
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> q a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ q (Untest a) b
l
    where
      leaf :: forall m (x :: TESTED csj j). TestedP q x (TLeaf m :: TESTED csk k) -> TestedP q x (TLeaf m :: TESTED csk k)
      leaf :: forall (m :: k) (x :: TESTED csj j).
TestedP q x (TLeaf m) -> TestedP q x (TLeaf m)
leaf TestedP q x (TLeaf m)
x = TestedP q x (TLeaf m)
x
  counit :: (TestedP p :.: TestedP q) :~> (~>)
counit (TestedP Doc
dp p (Untest a) (Untest b)
x :.: TestedP Doc
dq q (Untest b) (Untest b)
y) = Doc -> (Untest a ~> Untest b) -> TestedArr a b
forall (cs :: [Type -> Constraint]) k (a :: TESTED cs k)
       (b :: TESTED cs k).
(Tested a, Tested b) =>
Doc -> (Untest a ~> Untest b) -> TestedArr a b
TestedArr (String -> Doc -> Doc
app String
"counit" (Int -> String -> Doc -> Doc -> Doc
infixlDoc Int
9 String
" :.: " Doc
dp Doc
dq)) ((:.:) p q (Untest a) (Untest b) -> Untest a ~> Untest b
(p :.: q) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
Adj.counit (p (Untest a) (Untest b)
x p (Untest a) (Untest b)
-> q (Untest b) (Untest b) -> (:.:) p q (Untest a) (Untest b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q (Untest b) (Untest b)
y))