{-# LANGUAGE AllowAmbiguousTypes #-}

{- HLINT ignore "Redundant id" -}

-- | Reusable law-checking properties, parameterized over any 'Testable' kind: 'propCategory',
-- 'propMonoidal', 'propBinaryProducts', 'propClosed', 'propProfunctor', 'propMonoid', and friends.
-- Wiring a new category into a test suite is a 'Testable' instance plus calls to these -- see
-- proarrow's own test suite for many examples.
--
-- Many of these take an explicit witness that 'TestOb' is closed under the structure being tested
-- (e.g. that @'TestOb' (a '**' b)@ follows from @'TestOb' a@ and @'TestOb' b@), since in general a
-- category may restrict which objects are testable. The @_@-suffixed variant (e.g. 'propMonoidal_')
-- supplies that witness for free, and so carries a 'TestObIsOb' constraint: it applies exactly when
-- every object is a 'TestOb' -- typically a category that leaves 'TestOb' at its @'Ob'@ default.
module Proarrow.Testing.Laws where

import Control.Monad (unless)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Falsify (Property, genWith, testFailed, testProperty)
import Prelude hiding (elem, fst, id, snd, (.), (>>))

import Proarrow.Adjunction (Adjunction)
import Proarrow.Category.Instance.Opposite (OPPOSITE (..))
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Category.Monoidal.Cartesian qualified as Cartesian
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.Hypergraph qualified as Hypergraph
import Proarrow.Category.Monoidal.StarAutonomous qualified as SA
import Proarrow.Colimit.BinaryCoproduct qualified as BinaryCoproduct
import Proarrow.Colimit.Coequalizer qualified as Coequalizer
import Proarrow.Colimit.Initial qualified as Initial
import Proarrow.Colimit.Pushout qualified as Pushout
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), lmap, obj, rmap, (:~>), type (+->))
import Proarrow.Functor qualified as Functor
import Proarrow.Limit.BinaryProduct qualified as BinaryProduct
import Proarrow.Limit.Equalizer qualified as Equalizer
import Proarrow.Limit.Pullback qualified as Pullback
import Proarrow.Limit.Terminal qualified as Terminal
import Proarrow.Monoid qualified as Monoid
import Proarrow.Object (pattern Objs)
import Proarrow.Optic (ExOptic, Flip, Optic)
import Proarrow.Optic.Getter (GetterFl, review, view)
import Proarrow.Profunctor.Corepresentable
  ( Corepresentable
  , coindex
  , corepMap
  , cotabulate
  , withObCorep
  , type (%%)
  )
import Proarrow.Profunctor.Representable (Rep, Representable, index, repMap, tabulate, withObRep, type (%))
import Proarrow.Testing
  ( Some (..)
  , SomeProfunctorElt (..)
  , TestOb'
  , TestObIsOb
  , Testable (..)
  , TestableProfunctor (..)
  , TestableTypeP
  , TestingEqShow (..)
  , genNamed
  , genOb
  , genObSuchThat
  , genSuchThat
  , isGenNonEmpty
  , obFromTestOb
  )

testEq :: (TestingEqShow a) => String -> String -> a -> String -> a -> Property ()
testEq :: forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq String
nm String
sl a
l String
sr a
r = do
  isEq <- a -> a -> Property Bool
forall a. TestingEqShow a => a -> a -> Property Bool
eqP a
l a
r
  unless isEq $
    testFailed $
      "Failed "
        ++ nm
        ++ ":\n"
        ++ sl
        ++ " = "
        ++ showP l
        ++ "\n"
        ++ sr
        ++ " = "
        ++ showP r

propCategory :: forall k. (Testable k) => TestTree
propCategory :: forall k. Testable k => TestTree
propCategory = String -> Property () -> TestTree
testProperty String
"Category" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  f <- genNamed @(a ~> b) "f"
  testEq "left identity" "id . f" (id . f) "f" f
  testEq "right identity" "f . id" (f . id) "f" f
  Some @c <- genOb
  Some @d <- genOb
  g <- genNamed @(b ~> c) "g"
  h <- genNamed @(c ~> d) "h"
  testEq "associativity" "(h . g) . f" ((h . g) . f) "h . (g . f)" (h . (g . f))

propTerminalObject
  :: forall k
   . (Testable k, Terminal.HasTerminalObject k, TestOb (Terminal.TerminalObject :: k))
  => TestTree
propTerminalObject :: forall k.
(Testable k, HasTerminalObject k, TestOb TerminalObject) =>
TestTree
propTerminalObject = String -> Property () -> TestTree
testProperty String
"Terminal object" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  f <- genNamed @(a ~> b) "f"
  testEq "uniqueness" "terminate . f" (Terminal.terminate . f) "terminate" Terminal.terminate

propInitialObject
  :: forall k
   . (Testable k, Initial.HasInitialObject k, TestOb (Initial.InitialObject :: k))
  => TestTree
propInitialObject :: forall k.
(Testable k, HasInitialObject k, TestOb InitialObject) =>
TestTree
propInitialObject = String -> Property () -> TestTree
testProperty String
"Initial object" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  f <- genNamed @(a ~> b) "f"
  testEq "uniqueness" "f . initiate" (f . Initial.initiate) "initiate" Initial.initiate

propBinaryProducts
  :: forall k
   . (Testable k, BinaryProduct.HasBinaryProducts k)
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a BinaryProduct.&& b)) => r) -> r)
  -> TestTree
propBinaryProducts :: forall k.
(Testable k, HasBinaryProducts k) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a && b) => r) -> r)
-> TestTree
propBinaryProducts forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a && b) => r) -> r
withTestObProd = String -> Property () -> TestTree
testProperty String
"Binary products" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  Some @c <- genOb
  Some @z <- genOb
  withTestObProd @b @c $ do
    f <- genNamed @(a ~> b) "f"
    g <- genNamed @(a ~> c) "g"
    testEq "fst" "fst . (f &&& g)" (BinaryProduct.fst @k @b @c . (f BinaryProduct.&&& g)) "f" f
    testEq "snd" "snd . (f &&& g)" (BinaryProduct.snd @k @b @c . (f BinaryProduct.&&& g)) "g" g
    h <- genNamed @(z ~> a) "h"
    testEq
      "uniqueness"
      "(f . h) &&& (g . h)"
      ((f . h) BinaryProduct.&&& (g . h))
      "(f &&& g) . h"
      ((f BinaryProduct.&&& g) . h)

propBinaryProducts_
  :: forall k
   . (Testable k, BinaryProduct.HasBinaryProducts k, TestObIsOb k)
  => TestTree
propBinaryProducts_ :: forall k.
(Testable k, HasBinaryProducts k, TestObIsOb k) =>
TestTree
propBinaryProducts_ = forall k.
(Testable k, HasBinaryProducts k) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a && b) => r) -> r)
-> TestTree
propBinaryProducts @k (\ @a @b TestOb (a && b) => r
r -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
BinaryProduct.withObProd @k @a @b r
Ob (a && b) => r
TestOb (a && b) => r
r)

propBinaryCoproducts
  :: forall k
   . (Testable k, BinaryCoproduct.HasBinaryCoproducts k)
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a BinaryCoproduct.|| b)) => r) -> r)
  -> TestTree
propBinaryCoproducts :: forall k.
(Testable k, HasBinaryCoproducts k) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a || b) => r) -> r)
-> TestTree
propBinaryCoproducts forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a || b) => r) -> r
withTestObCoprod = String -> Property () -> TestTree
testProperty String
"Binary coproducts" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  Some @c <- genOb
  Some @z <- genOb
  withTestObCoprod @a @b $ do
    f <- genNamed @(a ~> c) "f"
    g <- genNamed @(b ~> c) "g"
    testEq "lft" "(f ||| g) . lft" ((f BinaryCoproduct.||| g) . BinaryCoproduct.lft @k @a @b) "f" f
    testEq "rgt" "(f ||| g) . rgt" ((f BinaryCoproduct.||| g) . BinaryCoproduct.rgt @k @a @b) "g" g
    h <- genNamed @(c ~> z) "h"
    testEq
      "uniqueness"
      "(h . f) ||| (h . g)"
      ((h . f) BinaryCoproduct.||| (h . g))
      "h . (f ||| g)"
      (h . (f BinaryCoproduct.||| g))

propBinaryCoproducts_
  :: forall k
   . (Testable k, BinaryCoproduct.HasBinaryCoproducts k, TestObIsOb k)
  => TestTree
propBinaryCoproducts_ :: forall k.
(Testable k, HasBinaryCoproducts k, TestObIsOb k) =>
TestTree
propBinaryCoproducts_ = forall k.
(Testable k, HasBinaryCoproducts k) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a || b) => r) -> r)
-> TestTree
propBinaryCoproducts @k (\ @a @b TestOb (a || b) => r
r -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
BinaryCoproduct.withObCoprod @k @a @b r
Ob (a || b) => r
TestOb (a || b) => r
r)

-- | Checks the equalizer laws: the equalizer arrow @e@ equalizes @f@ and @g@; any @h@ that factors
-- through @e@ (built here as @e . p@ for an arbitrary @p@, so the precondition holds by construction)
-- is correctly recovered by 'Equalizer.factorEqualizer'; and @e@ is mono (composing with it on the
-- left reflects equality).
--
-- Unlike 'propBinaryProducts', the equalizer object isn't computed from @a@, @b@ by a type family --
-- it's an arbitrary object revealed at runtime, whose 'Ob' evidence 'Objs' recovers generically from
-- the equalizer arrow. So @withTestOb@ only ever needs to bridge that single recovered 'Ob' to 'TestOb'.
propEqualizers
  :: forall k
   . (Testable k, Equalizer.HasEqualizers k)
  => (forall (e :: k) r. (Ob e) => ((TestOb e) => r) -> r)
  -> TestTree
propEqualizers :: forall k.
(Testable k, HasEqualizers k) =>
(forall (e :: k) r. Ob e => (TestOb e => r) -> r) -> TestTree
propEqualizers forall (e :: k) r. Ob e => (TestOb e => r) -> r
withTestOb = String -> Property () -> TestTree
testProperty String
"Equalizers" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  f <- genNamed @(a ~> b) "f"
  g <- genNamed @(a ~> b) "g"
  Equalizer.equalize f g \ @e ee :: e ~> a
ee@e ~> a
Objs -> forall (e :: k) r. Ob e => (TestOb e => r) -> r
withTestOb @e ((TestOb e => Property ()) -> Property ())
-> (TestOb e => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$ do
    String -> String -> (e ~> a) -> String -> (e ~> a) -> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq String
"equalizing" String
"f . e" (a ~> a
f (a ~> a) -> (e ~> a) -> e ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. e ~> a
ee) String
"g . e" (a ~> a
g (a ~> a) -> (e ~> a) -> e ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. e ~> a
ee)
    Some @z <- Property (Some k)
forall k. Testable k => Property (Some k)
genOb
    p <- genNamed @(z ~> e) "p"
    let h = e ~> a
ee (e ~> a) -> (a ~> e) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> e
p
        factored = (e ~> a) -> (a ~> a) -> a ~> e
forall (e :: k) (x :: k) (e' :: k).
(e ~> x) -> (e' ~> x) -> e' ~> e
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
Equalizer.factorEqualizer e ~> a
ee a ~> a
h
    testEq "factorization" "e . factored" (ee . factored) "h" h
    k1 <- genNamed @(z ~> e) "k1"
    k2 <- genNamed @(z ~> e) "k2"
    eqComposed <- eqP (ee . k1) (ee . k2)
    eqDirect <- eqP k1 k2
    unless (eqComposed == eqDirect) $
      testFailed $
        "Failed mono: (e . k1 == e . k2) = "
          ++ show eqComposed
          ++ " but (k1 == k2) = "
          ++ show eqDirect

propEqualizers_
  :: forall k
   . (Testable k, Equalizer.HasEqualizers k, TestObIsOb k)
  => TestTree
propEqualizers_ :: forall k. (Testable k, HasEqualizers k, TestObIsOb k) => TestTree
propEqualizers_ = forall k.
(Testable k, HasEqualizers k) =>
(forall (e :: k) r. Ob e => (TestOb e => r) -> r) -> TestTree
propEqualizers @k (\TestOb e => r
r -> r
TestOb e => r
r)

-- | Checks the coequalizer laws, dual to 'propEqualizers': the coequalizer arrow @c@ coequalizes @f@
-- and @g@; any @h@ that factors through @c@ (built here as @p . c@ for an arbitrary @p@, so the
-- precondition holds by construction) is correctly recovered by 'Coequalizer.factorCoequalizer'; and
-- @c@ is epi (post-composing with it on the right reflects equality).
propCoequalizers
  :: forall k
   . (Testable k, Coequalizer.HasCoequalizers k)
  => (forall (c :: k) r. (Ob c) => ((TestOb c) => r) -> r)
  -> TestTree
propCoequalizers :: forall k.
(Testable k, HasCoequalizers k) =>
(forall (c :: k) r. Ob c => (TestOb c => r) -> r) -> TestTree
propCoequalizers forall (c :: k) r. Ob c => (TestOb c => r) -> r
withTestOb = String -> Property () -> TestTree
testProperty String
"Coequalizers" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  f <- genNamed @(a ~> b) "f"
  g <- genNamed @(a ~> b) "g"
  Coequalizer.coequalize f g \ @c cq :: a ~> c
cq@a ~> c
Objs -> forall (c :: k) r. Ob c => (TestOb c => r) -> r
withTestOb @c ((TestOb c => Property ()) -> Property ())
-> (TestOb c => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$ do
    String -> String -> (a ~> c) -> String -> (a ~> c) -> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq String
"coequalizing" String
"c . f" (a ~> c
cq (a ~> c) -> (a ~> a) -> a ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
f) String
"c . g" (a ~> c
cq (a ~> c) -> (a ~> a) -> a ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
g)
    Some @z <- Property (Some k)
forall k. Testable k => Property (Some k)
genOb
    p <- genNamed @(c ~> z) "p"
    let h = c ~> a
p (c ~> a) -> (a ~> c) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> c
cq
        factored = (a ~> c) -> (a ~> a) -> c ~> a
forall (c :: k) (x :: k) (c' :: k).
(x ~> c) -> (x ~> c') -> c ~> c'
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
Coequalizer.factorCoequalizer a ~> c
cq a ~> a
h
    testEq "factorization" "factored . c" (factored . cq) "h" h
    k1 <- genNamed @(c ~> z) "k1"
    k2 <- genNamed @(c ~> z) "k2"
    eqComposed <- eqP (k1 . cq) (k2 . cq)
    eqDirect <- eqP k1 k2
    unless (eqComposed == eqDirect) $
      testFailed $
        "Failed epi: (k1 . c == k2 . c) = "
          ++ show eqComposed
          ++ " but (k1 == k2) = "
          ++ show eqDirect

propCoequalizers_
  :: forall k
   . (Testable k, Coequalizer.HasCoequalizers k, TestObIsOb k)
  => TestTree
propCoequalizers_ :: forall k. (Testable k, HasCoequalizers k, TestObIsOb k) => TestTree
propCoequalizers_ = forall k.
(Testable k, HasCoequalizers k) =>
(forall (c :: k) r. Ob c => (TestOb c => r) -> r) -> TestTree
propCoequalizers @k (\TestOb c => r
r -> r
TestOb c => r
r)

-- | Checks the pullback laws: the pullback cone commutes; it's jointly monic (composing with both
-- legs at once reflects equality); and any compatible cone (built here as @(p1 . j, p2 . j)@ for an
-- arbitrary @j@, so compatibility holds by construction) is correctly recovered by
-- 'Pullback.factorPullback'.
propPullbacks
  :: forall k
   . (Testable k, Pullback.HasPullbacks k)
  => (forall (p :: k) r. (Ob p) => ((TestOb p) => r) -> r)
  -> TestTree
propPullbacks :: forall k.
(Testable k, HasPullbacks k) =>
(forall (p :: k) r. Ob p => (TestOb p => r) -> r) -> TestTree
propPullbacks forall (p :: k) r. Ob p => (TestOb p => r) -> r
withTestOb = String -> Property () -> TestTree
testProperty String
"Pullbacks" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @o <- forall k. Testable k => Property (Some k)
genOb @k
  Some @a <- genOb
  Some @b <- genOb
  f <- genNamed @(a ~> o) "f"
  g <- genNamed @(b ~> o) "g"
  Pullback.pullback f g \ @p p1 :: p ~> a
p1@p ~> a
Objs p ~> a
p2 -> forall (p :: k) r. Ob p => (TestOb p => r) -> r
withTestOb @p ((TestOb p => Property ()) -> Property ())
-> (TestOb p => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$ do
    String -> String -> (p ~> a) -> String -> (p ~> a) -> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq String
"commutes" String
"f . p1" (a ~> a
f (a ~> a) -> (p ~> a) -> p ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p ~> a
p1) String
"g . p2" (a ~> a
g (a ~> a) -> (p ~> a) -> p ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p ~> a
p2)
    Some @z <- Property (Some k)
forall k. Testable k => Property (Some k)
genOb
    k1' <- genNamed @(z ~> p) "k1"
    k2' <- genNamed @(z ~> p) "k2"
    eq1 <- eqP (p1 . k1') (p1 . k2')
    eq2 <- eqP (p2 . k1') (p2 . k2')
    let eqBoth = Bool
eq1 Bool -> Bool -> Bool
&& Bool
eq2
    eqDirect <- eqP k1' k2'
    unless (eqBoth == eqDirect) $
      testFailed $
        "Failed jointly monic: (p1 . k1 == p1 . k2 && p2 . k1 == p2 . k2) = "
          ++ show eqBoth
          ++ " but (k1 == k2) = "
          ++ show eqDirect
    j <- genNamed @(z ~> p) "j"
    let k1 = p ~> a
p1 (p ~> a) -> (a ~> p) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> p
j
        k2 = p ~> a
p2 (p ~> a) -> (a ~> p) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> p
j
        factored = (p ~> a) -> (p ~> a) -> (a ~> a) -> (a ~> a) -> a ~> p
forall (a :: k) (b :: k) (p :: k) (q :: k).
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
forall k (a :: k) (b :: k) (p :: k) (q :: k).
HasPullbacks k =>
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
Pullback.factorPullback p ~> a
p1 p ~> a
p2 a ~> a
k1 a ~> a
k2
    testEq "factorization (1)" "p1 . factored" (p1 . factored) "k1" k1
    testEq "factorization (2)" "p2 . factored" (p2 . factored) "k2" k2

propPullbacks_
  :: forall k
   . (Testable k, Pullback.HasPullbacks k, TestObIsOb k)
  => TestTree
propPullbacks_ :: forall k. (Testable k, HasPullbacks k, TestObIsOb k) => TestTree
propPullbacks_ = forall k.
(Testable k, HasPullbacks k) =>
(forall (p :: k) r. Ob p => (TestOb p => r) -> r) -> TestTree
propPullbacks @k (\TestOb p => r
r -> r
TestOb p => r
r)

-- | Checks the pushout laws, dual to 'propPullbacks': the pushout cocone commutes; it's jointly epic
-- (post-composing with both legs at once reflects equality); and any compatible cocone (built here as
-- @(j . p1, j . p2)@ for an arbitrary @j@, so compatibility holds by construction) is correctly
-- recovered by 'Pushout.factorPushout'.
propPushouts
  :: forall k
   . (Testable k, Pushout.HasPushouts k)
  => (forall (p :: k) r. (Ob p) => ((TestOb p) => r) -> r)
  -> TestTree
propPushouts :: forall k.
(Testable k, HasPushouts k) =>
(forall (p :: k) r. Ob p => (TestOb p => r) -> r) -> TestTree
propPushouts forall (p :: k) r. Ob p => (TestOb p => r) -> r
withTestOb = String -> Property () -> TestTree
testProperty String
"Pushouts" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @o <- forall k. Testable k => Property (Some k)
genOb @k
  Some @a <- genOb
  Some @b <- genOb
  f <- genNamed @(o ~> a) "f"
  g <- genNamed @(o ~> b) "g"
  Pushout.pushout f g \ @p p1 :: a ~> p
p1@a ~> p
Objs a ~> p
p2 -> forall (p :: k) r. Ob p => (TestOb p => r) -> r
withTestOb @p ((TestOb p => Property ()) -> Property ())
-> (TestOb p => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$ do
    String -> String -> (a ~> p) -> String -> (a ~> p) -> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq String
"commutes" String
"p1 . f" (a ~> p
p1 (a ~> p) -> (a ~> a) -> a ~> p
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
f) String
"p2 . g" (a ~> p
p2 (a ~> p) -> (a ~> a) -> a ~> p
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
g)
    Some @z <- Property (Some k)
forall k. Testable k => Property (Some k)
genOb
    k1' <- genNamed @(p ~> z) "k1"
    k2' <- genNamed @(p ~> z) "k2"
    eq1 <- eqP (k1' . p1) (k2' . p1)
    eq2 <- eqP (k1' . p2) (k2' . p2)
    let eqBoth = Bool
eq1 Bool -> Bool -> Bool
&& Bool
eq2
    eqDirect <- eqP k1' k2'
    unless (eqBoth == eqDirect) $
      testFailed $
        "Failed jointly epic: (k1 . p1 == k2 . p1 && k1 . p2 == k2 . p2) = "
          ++ show eqBoth
          ++ " but (k1 == k2) = "
          ++ show eqDirect
    j <- genNamed @(p ~> z) "j"
    let k1 = p ~> a
j (p ~> a) -> (a ~> p) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> p
p1
        k2 = p ~> a
j (p ~> a) -> (a ~> p) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> p
p2
        factored = (a ~> p) -> (a ~> p) -> (a ~> a) -> (a ~> a) -> p ~> a
forall (a :: k) (b :: k) (p :: k) (q :: k).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
forall k (a :: k) (b :: k) (p :: k) (q :: k).
HasPushouts k =>
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
Pushout.factorPushout a ~> p
p1 a ~> p
p2 a ~> a
k1 a ~> a
k2
    testEq "factorization (1)" "factored . p1" (factored . p1) "k1" k1
    testEq "factorization (2)" "factored . p2" (factored . p2) "k2" k2

propPushouts_
  :: forall k
   . (Testable k, Pushout.HasPushouts k, TestObIsOb k)
  => TestTree
propPushouts_ :: forall k. (Testable k, HasPushouts k, TestObIsOb k) => TestTree
propPushouts_ = forall k.
(Testable k, HasPushouts k) =>
(forall (p :: k) r. Ob p => (TestOb p => r) -> r) -> TestTree
propPushouts @k (\TestOb p => r
r -> r
TestOb p => r
r)

propMonoidal
  :: forall k
   . (Testable k, M.Monoidal k, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
propMonoidal :: forall k.
(Testable k, Monoidal k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
propMonoidal forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 = String -> Property () -> TestTree
testProperty String
"Monoidal" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  Some @c <- genOb
  Some @d <- genOb
  f <- genNamed @(a ~> b) "f"
  g <- genNamed @(b ~> c) "g"
  h <- genNamed @(c ~> d) "h"
  withTestOb2 @a @b $
    withTestOb2 @b @c $
      withTestOb2 @c @d $
        withTestOb2 @(a M.** b) @(c M.** d) $
          withTestOb2 @M.Unit @a $
            withTestOb2 @M.Unit @b $
              withTestOb2 @a @(M.Unit M.** b) $
                withTestOb2 @a @M.Unit $
                  withTestOb2 @b @M.Unit $
                    withTestOb2 @(a M.** M.Unit) @b $
                      withTestOb2 @(a M.** b) @c $
                        withTestOb2 @a @(b M.** c) $
                          withTestOb2 @(a M.** (b M.** c)) @d $
                            withTestOb2 @(b M.** c) @d $
                              withTestOb2 @a @((b M.** c) M.** d) $
                                withTestOb2 @b @(c M.** d) $
                                  withTestOb2 @a @(b M.** (c M.** d)) $
                                    withTestOb2 @((a M.** b) M.** c) @d $
                                      do
                                        propIso (M.associator @k @a @b @c) (M.associatorInv @k @a @b @c)
                                        propIso (M.leftUnitor @k @a) (M.leftUnitorInv @k @a)
                                        propIso (M.rightUnitor @k @a) (M.rightUnitorInv @k @a)
                                        testEq
                                          "associator naturality"
                                          "associator . ((f ** g) ** h)"
                                          (M.associator @k @b @c @d . ((f M.** g) M.** h))
                                          "(f ** (g ** h)) . associator"
                                          ((f M.** (g M.** h)) . M.associator @k @a @b @c)
                                        testEq
                                          "associatorInv naturality"
                                          "associatorInv . (f ** (g ** h))"
                                          (M.associatorInv @k @b @c @d . (f M.** (g M.** h)))
                                          "((f ** g) ** h) . associatorInv"
                                          (((f M.** g) M.** h) . M.associatorInv @k @a @b @c)
                                        testEq
                                          "leftUnitor naturality"
                                          "leftUnitor . (one ** f)"
                                          (M.leftUnitor @k @b . (obj @M.Unit M.** f))
                                          "f . leftUnitor"
                                          (f . M.leftUnitor @k @a)
                                        testEq
                                          "leftUnitorInv naturality"
                                          "leftUnitorInv . f"
                                          (M.leftUnitorInv @k @b . f)
                                          "(one ** f) . leftUnitorInv"
                                          ((obj @M.Unit M.** f) . M.leftUnitorInv @k @a)
                                        testEq
                                          "rightUnitor naturality"
                                          "rightUnitor . (f ** one)"
                                          (M.rightUnitor @k @b . (f M.** obj @M.Unit))
                                          "f . rightUnitor"
                                          (f . M.rightUnitor @k @a)
                                        testEq
                                          "rightUnitorInv naturality"
                                          "rightUnitorInv . f"
                                          (M.rightUnitorInv @k @b . f)
                                          "(f ** one) . rightUnitorInv"
                                          ((f M.** obj @M.Unit) . M.rightUnitorInv @k @a)
                                        testEq
                                          "triangle identity"
                                          "(id ** leftUnitor) . associator"
                                          ((obj @a M.** M.leftUnitor @k @b) . M.associator @k @a @M.Unit @b)
                                          "rightUnitor ** id"
                                          (M.rightUnitor @k @a M.** obj @b)
                                        testEq
                                          "pentagon identity"
                                          "(id ** associator) . associator . (associator ** id)"
                                          ( (obj @a M.** M.associator @k @b @c @d)
                                              . M.associator @k @a @(b M.** c) @d
                                              . (M.associator @k @a @b @c M.** obj @d)
                                          )
                                          "associator . associator"
                                          (M.associator @k @a @b @(c M.** d) . M.associator @k @(a M.** b) @c @d)

propMonoidal_
  :: forall k
   . (Testable k, M.Monoidal k, TestObIsOb k)
  => TestTree
propMonoidal_ :: forall k. (Testable k, Monoidal k, TestObIsOb k) => TestTree
propMonoidal_ = forall k.
(Testable k, Monoidal k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
propMonoidal @k (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)

propSymMonoidal
  :: forall k
   . (Testable k, M.SymMonoidal k, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
propSymMonoidal :: forall k.
(Testable k, SymMonoidal k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
propSymMonoidal forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 = String -> Property () -> TestTree
testProperty String
"Symmetric monoidal" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  Some @c <- genOb
  withTestOb2 @a @b $
    withTestOb2 @b @c $
      withTestOb2 @c @a $
        withTestOb2 @(a M.** b) @c $
          withTestOb2 @b @(c M.** a) $
            do
              testEq "swap swap" "swap . swap" (M.swap @k @b @a . M.swap @k @a @b) "id" id
              testEq
                "hexagon identity"
                "associator . swap . associator"
                (M.associator @k @b @c @a . M.swap @k @a @(b M.** c) . M.associator @k @a @b @c)
                "(swap ** id) . associator . (id ** swap)"
                ((obj @b M.** M.swap @k @a @c) . M.associator @k @b @a @c . (M.swap @k @a @b M.** obj @c))

propSymMonoidal_
  :: forall k
   . (Testable k, M.SymMonoidal k, TestObIsOb k)
  => TestTree
propSymMonoidal_ :: forall k. (Testable k, SymMonoidal k, TestObIsOb k) => TestTree
propSymMonoidal_ = forall k.
(Testable k, SymMonoidal k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
propSymMonoidal @k (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)

propCopyDiscard
  :: forall k
   . (Testable k, CopyDiscard.CopyDiscard k, TestOb (M.Unit @k))
  => (forall (a :: k) r. (TestOb a) => ((Ob a, Monoid.CocommutativeComonoid a) => r) -> r)
  -> (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
propCopyDiscard :: forall k.
(Testable k, CopyDiscard k, TestOb Unit) =>
(forall (a :: k) r.
 TestOb a =>
 ((Ob a, CocommutativeComonoid a) => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a ** b) => r) -> r)
-> TestTree
propCopyDiscard forall (a :: k) r.
TestOb a =>
((Ob a, CocommutativeComonoid a) => r) -> r
withCoco forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 = String -> Property () -> TestTree
testProperty String
"CopyDiscard" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  withCoco @a (propCocommutativeComonoid @a (\ @x @y TestOb (a ** b) => r
r -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @x @y r
TestOb (a ** b) => r
r))

-- | The cocommutative comonoid on each object is supplied by 'CopyDiscard.CopyDiscard' itself (its
-- @'Monoid.Supplies' 'Monoid.CocommutativeComonoid' k@ superclass), so only @'Ob' a@ has to be
-- recovered from @'TestOb' a@ -- through 'obFromTestOb', because with that quantified superclass in
-- scope GHC no longer finds the @TestOb a => Ob' a => Ob a@ route on its own.
propCopyDiscard_
  :: forall k
   . (Testable k, CopyDiscard.CopyDiscard k, TestObIsOb k)
  => TestTree
propCopyDiscard_ :: forall k. (Testable k, CopyDiscard k, TestObIsOb k) => TestTree
propCopyDiscard_ =
  forall k.
(Testable k, CopyDiscard k, TestOb Unit) =>
(forall (a :: k) r.
 TestOb a =>
 ((Ob a, CocommutativeComonoid a) => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a ** b) => r) -> r)
-> TestTree
propCopyDiscard @k (\ @a (Ob a, CocommutativeComonoid 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 a, CocommutativeComonoid a) => r
r) (\ @a @b TestOb (a ** b) => 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 (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 @b (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)))

-- | The coherence law tying 'Cartesian.Cartesian' to its 'CopyDiscard.CopyDiscard' superclass
-- (Fox's theorem): the comonoid supplied on every object is the natural one, @copy = id &&& id@
-- and @discard = terminate@.
propCartesian
  :: forall k
   . (Testable k, Cartesian.Cartesian k, TestOb (M.Unit @k))
  => (forall (a :: k) r. (TestOb a) => ((Ob a) => r) -> r)
  -> (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
propCartesian :: forall k.
(Testable k, Cartesian k, TestOb Unit) =>
(forall (a :: k) r. TestOb a => (Ob a => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a ** b) => r) -> r)
-> TestTree
propCartesian forall (a :: k) r. TestOb a => (Ob a => r) -> r
withOb forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 = String -> Property () -> TestTree
testProperty String
"Cartesian" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  withOb @a (withTestOb2 @a @a (propCartesianAt @a))

-- Hoisted so that @a ** a ~ a && a@ is an ordinary given ('Cartesian.TensorIsProduct'), which the
-- quantified superclass of 'Cartesian.Cartesian' can't supply as a rewrite on its own.
propCartesianAt
  :: forall {k} (a :: k)
   . ( Testable k
     , Cartesian.Cartesian k
     , Cartesian.TensorIsProduct a a
     , TestOb (M.Unit @k)
     , TestOb a
     , Ob a
     , TestOb (a M.** a)
     )
  => Property ()
propCartesianAt :: forall {k} (a :: k).
(Testable k, Cartesian k, TensorIsProduct a a, TestOb Unit,
 TestOb a, Ob a, TestOb (a ** a)) =>
Property ()
propCartesianAt = do
  String
-> String
-> (a ~> (a && a))
-> String
-> (a ~> (a && a))
-> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq String
"copy" String
"copy" (forall k (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
CopyDiscard.copy @k @a) String
"id &&& id" (forall (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
BinaryProduct.diag @a)
  String
-> String
-> (a ~> TerminalObject)
-> String
-> (a ~> TerminalObject)
-> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq String
"discard" String
"discard" (forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
CopyDiscard.discard @k @a) String
"terminate" (forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
Terminal.terminate @k @a)

propCartesian_
  :: forall k
   . (Testable k, Cartesian.Cartesian k, TestObIsOb k, TestOb (M.Unit @k))
  => TestTree
propCartesian_ :: forall k.
(Testable k, Cartesian k, TestObIsOb k, TestOb Unit) =>
TestTree
propCartesian_ =
  forall k.
(Testable k, Cartesian k, TestOb Unit) =>
(forall (a :: k) r. TestOb a => (Ob a => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a ** b) => r) -> r)
-> TestTree
propCartesian @k (\ @a Ob 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
r) (\ @a @b TestOb (a ** b) => 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 (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 @b (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)))

propDistributive
  :: forall k
   . (Testable k, Distributive.Distributive k, TestOb (Initial.InitialObject :: k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a BinaryCoproduct.|| b)) => r) -> r)
  -> TestTree
propDistributive :: forall k.
(Testable k, Distributive k, TestOb InitialObject) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a || b) => r) -> r)
-> TestTree
propDistributive forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a || b) => r) -> r
withTestObCoprod = String -> Property () -> TestTree
testProperty String
"Distributive" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  Some @c <- genOb
  withTestObCoprod @b @c $
    withTestObCoprod @a @b $
      withTestOb2 @a @b $
        withTestOb2 @a @c $
          withTestOb2 @b @c $
            withTestOb2 @a @(b BinaryCoproduct.|| c) $
              withTestOb2 @(a BinaryCoproduct.|| b) @c $
                withTestObCoprod @(a M.** b) @(a M.** c) $
                  withTestObCoprod @(a M.** c) @(b M.** c) $
                    withTestOb2 @a @(Initial.InitialObject :: k) $
                      withTestOb2 @(Initial.InitialObject :: k) @a $
                        do
                          propIso (Distributive.distL @k @a @b @c) (Distributive.distLInv @a @b @c)
                          propIso (Distributive.distR @k @a @b @c) (Distributive.distRInv @a @b @c)
                          propIso (Distributive.absorbL @k @a) Initial.initiate
                          propIso (Distributive.absorbR @k @a) Initial.initiate

propDistributive_
  :: forall k
   . (Testable k, Distributive.Distributive k, TestObIsOb k)
  => TestTree
propDistributive_ :: forall k. (Testable k, Distributive k, TestObIsOb k) => TestTree
propDistributive_ =
  forall k.
(Testable k, Distributive k, TestOb InitialObject) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a || b) => r) -> r)
-> TestTree
propDistributive @k
    (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)
    (\ @a @b TestOb (a || b) => r
r -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
BinaryCoproduct.withObCoprod @k @a @b r
Ob (a || b) => r
TestOb (a || b) => r
r)

propClosed
  :: forall k
   . (Testable k, Exponential.Closed k, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a Exponential.~~> b)) => r) -> r)
  -> TestTree
propClosed :: forall k.
(Testable k, Closed k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a ~~> b) => r) -> r)
-> TestTree
propClosed forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ~~> b) => r) -> r
withTestObExp =
  String -> [TestTree] -> TestTree
testGroup
    String
"Closed"
    [ String -> Property () -> TestTree
testProperty String
"Exponential is functorial" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
        forall {j} {k} (p :: j +-> k).
(Profunctor p, Testable j, Testable k) =>
Property (SomeProfunctorElt p)
-> (forall (a :: k) (b :: j) r.
    (TestOb a, TestOb b) =>
    (TestingEqShow (p a b) => r) -> r)
-> Property ()
forall (p :: (OPPOSITE k, k) +-> k).
(Profunctor p, Testable (OPPOSITE k, k), Testable k) =>
Property (SomeProfunctorElt p)
-> (forall (a :: k) (b :: (OPPOSITE k, k)) r.
    (TestOb a, TestOb b) =>
    (TestingEqShow (p a b) => r) -> r)
-> Property ()
propProfunctorWith @(Rep (Exponential.ExpRep @k))
          ( do
              (Some @a, Some @b1, Some @b2) <-
                ((Some k, Some k, Some k) -> Maybe String)
-> Gen (Some k, Some k, Some k)
-> Property' String (Some k, Some k, Some k)
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 k, Some k, Some k) -> String)
-> (Some k, Some k, Some k)
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Some k, Some k, Some k) -> String
forall a. Show a => a -> String
show)
                  ( Gen (Some k, Some k, Some k)
-> ((Some k, Some k, Some k) -> Bool)
-> Gen (Some k, Some k, Some k)
forall key. Gen key -> (key -> Bool) -> Gen key
genSuchThat ((,,) (Some k -> Some k -> Some k -> (Some k, Some k, Some k))
-> Gen (Some k)
-> Gen (Some k -> Some k -> (Some k, Some k, Some k))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k. Testable k => Gen (Some k)
genSome @k Gen (Some k -> Some k -> (Some k, Some k, Some k))
-> Gen (Some k) -> Gen (Some k -> (Some k, Some k, Some k))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall k. Testable k => Gen (Some k)
genSome @k Gen (Some k -> (Some k, Some k, Some k))
-> Gen (Some k) -> Gen (Some k, Some k, Some k)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall k. Testable k => Gen (Some k)
genSome @k) \(Some @a, Some @b1, Some @b2) ->
                      forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ~~> b) => r) -> r
withTestObExp @b1 @b2 (forall a. TestableType a => Bool
isGenNonEmpty @(Rep (Exponential.ExpRep @k) a '(OP b1, b2)))
                  )
              p <- withTestObExp @b1 @b2 (genNamed @(Rep (Exponential.ExpRep @k) a '(OP b1, b2)) "p")
              pure $ SomeP @a @'(OP b1, b2) p
          )
          (\ @_ @'(OP b1, b2) TestingEqShow (Rep ExpRep a b) => r
r -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ~~> b) => r) -> r
withTestObExp @b1 @b2 r
TestOb (UN 'OP (Fst @ b) ~~> (Snd @ b)) => r
TestingEqShow (Rep ExpRep a b) => r
r)
    , String -> Property () -> TestTree
testProperty String
"Curry/uncurry is a natural isomorphism" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
        Some @a <- forall k. Testable k => Property (Some k)
genOb @k
        Some @b <- genOb
        Some @c <- genOb
        withTestOb2 @a @b $ withTestObExp @b @c $ do
          propIsoP
            (Exponential.curry @k @a @b @c)
            (Exponential.uncurry @b @c)
          Some @a' <- genOb @k
          Some @b' <- genOb
          Some @c' <- genOb
          f <- genNamed @(a' ~> a) "f"
          g <- genNamed @(b' ~> b) "g"
          h <- genNamed @(c ~> c') "h"
          withTestOb2 @a' @b' $ withTestObExp @b' @c' $ do
            let n = ((a ** a) ~> (a ** a))
-> (a ~> a) -> ((a ** a) ~> a) -> (a ** a) ~> a
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (a ~> b) -> 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 (a ~> a
f (a ~> a) -> (a ~> a) -> (a ** a) ~> (a ** a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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.** a ~> a
g) a ~> a
h
            let n' = (a ~> a)
-> ((a ~~> a) ~> (a ~~> a)) -> (a ~> (a ~~> a)) -> a ~> (a ~~> a)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (a ~> b) -> 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 a ~> a
f (a ~> a
h (a ~> a) -> (a ~> a) -> (a ~~> a) ~> (a ~~> a)
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.^^^ a ~> a
g)
            testEq
              "natural curry"
              "curry . n"
              (Exponential.curry @k @a' @b' @c' . n)
              "n' . curry"
              (n' . Exponential.curry @k @a @b @c)
            testEq
              "natural uncurry"
              "uncurry . n'"
              (Exponential.uncurry @b' @c' . n')
              "n . uncurry"
              (n . Exponential.uncurry @b @c)
    ]

propClosed_
  :: forall k
   . (Testable k, Exponential.Closed k, TestObIsOb k)
  => TestTree
propClosed_ :: forall k. (Testable k, Closed k, TestObIsOb k) => TestTree
propClosed_ =
  forall k.
(Testable k, Closed k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a ~~> b) => r) -> r)
-> TestTree
propClosed @k
    (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)
    (\ @a @b TestOb (a ~~> b) => r
r -> forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
Exponential.withObExp @k @a @b r
Ob (a ~~> b) => r
TestOb (a ~~> b) => r
r)

-- | Laws of a *-autonomous category: 'SA.dual' is a contravariant functor and, together with
-- 'SA.dualInv', establishes a bijection on hom-sets; 'SA.linDist'\/'SA.linDistInv' establish a
-- bijection @Hom(a ** b, Dual c) ≅ Hom(a, Dual (b ** c))@, natural in all three variables; and
-- 'SA.doubleNegIso' witnesses that double dualization is (naturally) isomorphic to the identity.
propStarAutonomous
  :: forall k
   . (Testable k, SA.StarAutonomous k, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> (forall (a :: k) r. (TestOb a) => ((TestOb (SA.Dual a)) => r) -> r)
  -> TestTree
propStarAutonomous :: forall k.
(Testable k, StarAutonomous k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r)
-> TestTree
propStarAutonomous forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r
withTestObDual = String -> Property () -> TestTree
testProperty String
"*-autonomous" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  Some @c <- genOb
  Some @a' <- genOb @k
  Some @b' <- genOb @k
  Some @c' <- genOb @k
  withTestObDual @a $
    withTestObDual @(SA.Dual a) $
      withTestObDual @b $
        withTestObDual @c $
          withTestObDual @c' $
            withTestOb2 @a @b $
              withTestOb2 @b @c $
                withTestOb2 @a' @b $
                  withTestOb2 @a @b' $
                    withTestOb2 @b' @c $
                      withTestOb2 @b @c' $
                        withTestObDual @(b M.** c) $
                          withTestObDual @(b' M.** c) $
                            withTestObDual @(b M.** c') $ do
                              f <- genNamed @(a ~> b) "f"
                              g <- genNamed @(b ~> c) "g"
                              g' <- genNamed @(SA.Dual b ~> SA.Dual a) "g"
                              p <- genNamed @(a M.** b ~> SA.Dual c) "p"
                              q <- genNamed @(a ~> SA.Dual (b M.** c)) "q"
                              fa <- genNamed @(a' ~> a) "f"
                              gb <- genNamed @(b' ~> b) "g"
                              hc <- genNamed @(c ~> c') "h"
                              p2 <- genNamed @(a M.** b ~> SA.Dual c') "p"

                              propIso' (SA.doubleNegIso @a)

                              -- dual is a contravariant functor
                              testEq "dual id" "dual id" (SA.dual @k @a @a (id @_ @a)) "id" id
                              testEq
                                "dual composition"
                                "dual (g . f)"
                                (SA.dual @k @a @c (g . f))
                                "dual f . dual g"
                                (SA.dual @k @a @b f . SA.dual @k @b @c g)

                              -- dual / dualInv establish a bijection on hom-sets
                              testEq
                                "dualInv (dual f)"
                                "dualInv (dual f)"
                                (SA.dualInv @k @b @a (SA.dual @k @a @b f))
                                "f"
                                f
                              testEq
                                "dual (dualInv g)"
                                "dual (dualInv g)"
                                (SA.dual @k @a @b (SA.dualInv @k @b @a g'))
                                "g"
                                g'

                              -- linDist / linDistInv establish a bijection Hom(a**b, Dual c) ≅ Hom(a, Dual (b**c))
                              testEq
                                "linDistInv (linDist p)"
                                "linDistInv (linDist p)"
                                (SA.linDistInv @k @a @b @c (SA.linDist @k @a @b @c p))
                                "p"
                                p
                              testEq
                                "linDist (linDistInv q)"
                                "linDist (linDistInv q)"
                                (SA.linDist @k @a @b @c (SA.linDistInv @k @a @b @c q))
                                "q"
                                q

                              -- naturality of linDist in a
                              testEq
                                "linDist naturality (a)"
                                "linDist p . f"
                                (SA.linDist @k @a @b @c p . fa)
                                "linDist (p . (f ** id))"
                                (SA.linDist @k @a' @b @c (p . (fa M.** obj @b)))

                              -- naturality of linDist in b
                              testEq
                                "linDist naturality (b)"
                                "dual (g ** id) . linDist p"
                                (SA.dual @k @(b' M.** c) @(b M.** c) (gb M.** obj @c) . SA.linDist @k @a @b @c p)
                                "linDist (p . (id ** g))"
                                (SA.linDist @k @a @b' @c (p . (obj @a M.** gb)))

                              -- naturality of linDist in c
                              testEq
                                "linDist naturality (c)"
                                "linDist (dual h . p)"
                                (SA.linDist @k @a @b @c (SA.dual @k @c @c' hc . p2))
                                "dual (id ** h) . linDist p"
                                (SA.dual @k @(b M.** c) @(b M.** c') (obj @b M.** hc) . SA.linDist @k @a @b @c' p2)

propStarAutonomous_
  :: forall k
   . (Testable k, SA.StarAutonomous k, TestObIsOb k)
  => TestTree
propStarAutonomous_ :: forall k. (Testable k, StarAutonomous k, TestObIsOb k) => TestTree
propStarAutonomous_ =
  (forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r)
-> TestTree
forall k.
(Testable k, StarAutonomous k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r)
-> TestTree
propStarAutonomous
    (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)
    (\ @a TestOb (Dual a) => r
r -> r
(Ob (Dual a), Ob (Dual a)) => r
TestOb (Dual a) => r
r ((Ob (Dual a), Ob (Dual a)) => r) -> (Dual a ~> Dual a) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
SA.dualObj @a)

-- | Laws of a compact closed category: 'CC.distribDual'\/'CC.combineDual' establish an
-- isomorphism @Dual (a ** b) ≅ Dual a ** Dual b@ and 'CC.dualUnit'\/'CC.dualUnitInv' establish
-- @Dual Unit ≅ Unit@ (i.e. 'SA.Dual' is a strong monoidal functor); and the yanking\/zigzag
-- identities witness that @a@ and @Dual a@ are genuinely dual to one another via
-- 'CC.dualityUnit'\/'CC.dualityCounit'.
propCompactClosed
  :: forall k
   . (Testable k, CC.CompactClosed k, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> (forall (a :: k) r. (TestOb a) => ((TestOb (SA.Dual a)) => r) -> r)
  -> TestTree
propCompactClosed :: forall k.
(Testable k, CompactClosed k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r)
-> TestTree
propCompactClosed forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r
withTestObDual = String -> Property () -> TestTree
testProperty String
"Compact closed" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb
  withTestObDual @a $
    withTestObDual @b $
      withTestObDual @(M.Unit @k) $
        withTestOb2 @a @b $
          withTestOb2 @(SA.Dual a) @(SA.Dual b) $
            withTestOb2 @a @(SA.Dual a) $
              withTestOb2 @(SA.Dual a) @a $
                withTestOb2 @a @M.Unit $
                  withTestOb2 @M.Unit @a $
                    withTestOb2 @(SA.Dual a) @M.Unit $
                      withTestOb2 @M.Unit @(SA.Dual a) $
                        withTestObDual @(a M.** b) $
                          withTestOb2 @(a M.** SA.Dual a) @a $
                            withTestOb2 @a @(SA.Dual a M.** a) $
                              withTestOb2 @(SA.Dual a M.** a) @(SA.Dual a) $
                                withTestOb2 @(SA.Dual a) @(a M.** SA.Dual a) $ do
                                  -- distribDual / combineDual establish an isomorphism Dual (a**b) ≅ Dual a ** Dual b
                                  testEq
                                    "combineDual . distribDual"
                                    "combineDual (distribDual p)"
                                    (CC.combineDual @a @b . CC.distribDual @k @a @b)
                                    "id"
                                    id
                                  testEq
                                    "distribDual . combineDual"
                                    "distribDual (combineDual p)"
                                    (CC.distribDual @k @a @b . CC.combineDual @a @b)
                                    "id"
                                    id

                                  -- dualUnit / dualUnitInv establish an isomorphism Dual Unit ≅ Unit
                                  testEq
                                    "dualUnit . dualUnitInv"
                                    "dualUnit . dualUnitInv"
                                    (CC.dualUnit @k . CC.dualUnitInv)
                                    "id"
                                    id
                                  testEq
                                    "dualUnitInv . dualUnit"
                                    "dualUnitInv . dualUnit"
                                    (CC.dualUnitInv . CC.dualUnit @k)
                                    "id"
                                    id

                                  -- yanking / zigzag identity for a
                                  testEq
                                    "zigzag (a)"
                                    "rightUnitor . (id ** dualityCounit) . assoc . (dualityUnit ** id) . leftUnitorInv"
                                    ( M.rightUnitor @k @a
                                        . (obj @a M.** CC.dualityCounit @a)
                                        . M.associator @k @a @(SA.Dual a) @a
                                        . (CC.dualityUnit @a M.** obj @a)
                                        . M.leftUnitorInv @k @a
                                    )
                                    "id"
                                    id

                                  -- yanking / zigzag identity for Dual a
                                  testEq
                                    "zigzag (Dual a)"
                                    "leftUnitor . (dualityCounit ** id) . assocInv . (id ** dualityUnit) . rightUnitorInv"
                                    ( M.leftUnitor @k @(SA.Dual a)
                                        . (CC.dualityCounit @a M.** obj @(SA.Dual a))
                                        . M.associatorInv @k @(SA.Dual a) @a @(SA.Dual a)
                                        . (obj @(SA.Dual a) M.** CC.dualityUnit @a)
                                        . M.rightUnitorInv @k @(SA.Dual a)
                                    )
                                    "id"
                                    id

propCompactClosed_
  :: forall k
   . (Testable k, CC.CompactClosed k, TestObIsOb k)
  => TestTree
propCompactClosed_ :: forall k. (Testable k, CompactClosed k, TestObIsOb k) => TestTree
propCompactClosed_ =
  (forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r)
-> TestTree
forall k.
(Testable k, CompactClosed k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) r. TestOb a => (TestOb (Dual a) => r) -> r)
-> TestTree
propCompactClosed
    (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)
    (\ @a TestOb (Dual a) => r
r -> r
(Ob (Dual a), Ob (Dual a)) => r
TestOb (Dual a) => r
r ((Ob (Dual a), Ob (Dual a)) => r) -> (Dual a ~> Dual a) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
SA.dualObj @a)

-- | Check that the object @m@ is a special commutative 'Hypergraph.Frobenius' algebra: it is a
-- 'Monoid.CommutativeMonoid' (via 'propCommutativeMonoid') and a 'Monoid.CocommutativeComonoid'
-- (via 'propCocommutativeComonoid'), and satisfies speciality (@mappend . comult = id@) and the
-- Frobenius condition. This is the structure a 'Hypergraph.Hypergraph' category supplies -- @'propHypergraph'@
-- samples an object and delegates here.
propFrobenius
  :: forall {k} m
   . ( Testable k
     , M.SymMonoidal k
     , Monoid.CommutativeMonoid (m :: k)
     , Monoid.CocommutativeComonoid m
     , TestOb m
     , TestOb (M.Unit @k)
     )
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> Property ()
propFrobenius :: forall {k} (m :: k).
(Testable k, SymMonoidal k, CommutativeMonoid m,
 CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propFrobenius forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 = do
  forall (m :: k).
(Testable k, CommutativeMonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
forall {k} (m :: k).
(Testable k, CommutativeMonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propCommutativeMonoid @m (\ @x @y TestOb (a ** b) => r
r -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @x @y r
TestOb (a ** b) => r
r)
  forall (m :: k).
(Testable k, CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
forall {k} (m :: k).
(Testable k, CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propCocommutativeComonoid @m (\ @x @y TestOb (a ** b) => r
r -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @x @y r
TestOb (a ** b) => r
r)
  forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @m @m ((TestOb (m ** m) => Property ()) -> Property ())
-> (TestOb (m ** m) => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$
    forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @(m M.** m) @m ((TestOb ((m ** m) ** m) => Property ()) -> Property ())
-> (TestOb ((m ** m) ** m) => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$ do
      let mu :: (m ** m) ~> m
mu = forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend @m
          delta :: m ~> (m ** m)
delta = forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
Monoid.comult @m
      String -> String -> (m ~> m) -> String -> (m ~> m) -> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq
        String
"speciality"
        String
"mappend . comult"
        ((m ** m) ~> m
mu ((m ** m) ~> m) -> (m ~> (m ** m)) -> m ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. m ~> (m ** m)
delta)
        String
"id"
        (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m)
      String
-> String
-> ((m ** m) ~> (m ** m))
-> String
-> ((m ** m) ~> (m ** m))
-> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq
        String
"Frobenius condition (left)"
        String
"(mappend ** id) . associatorInv . (id ** comult)"
        (((m ** m) ~> m
mu ((m ** m) ~> m) -> (m ~> m) -> ((m ** m) ** m) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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.** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m) (((m ** m) ** m) ~> (m ** m))
-> ((m ** m) ~> ((m ** m) ** m)) -> (m ** m) ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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 @m @m @m ((m ** (m ** m)) ~> ((m ** m) ** m))
-> ((m ** m) ~> (m ** (m ** m))) -> (m ** m) ~> ((m ** m) ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m (m ~> m) -> (m ~> (m ** m)) -> (m ** m) ~> (m ** (m ** m))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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.** m ~> (m ** m)
delta))
        String
"comult . mappend"
        (m ~> (m ** m)
delta (m ~> (m ** m)) -> ((m ** m) ~> m) -> (m ** m) ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (m ** m) ~> m
mu)
      String
-> String
-> ((m ** m) ~> (m ** m))
-> String
-> ((m ** m) ~> (m ** m))
-> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq
        String
"Frobenius condition (right)"
        String
"(id ** mappend) . associator . (comult ** id)"
        ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m (m ~> m) -> ((m ** m) ~> m) -> (m ** (m ** m)) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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.** (m ** m) ~> m
mu) ((m ** (m ** m)) ~> (m ** m))
-> ((m ** m) ~> (m ** (m ** m))) -> (m ** m) ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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 @m @m @m (((m ** m) ** m) ~> (m ** (m ** m)))
-> ((m ** m) ~> ((m ** m) ** m)) -> (m ** m) ~> (m ** (m ** m))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (m ~> (m ** m)
delta (m ~> (m ** m)) -> (m ~> m) -> (m ** m) ~> ((m ** m) ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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.** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m))
        String
"comult . mappend"
        (m ~> (m ** m)
delta (m ~> (m ** m)) -> ((m ** m) ~> m) -> (m ** m) ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (m ** m) ~> m
mu)

-- | Check 'propFrobenius' at randomly sampled objects.
propHypergraph
  :: forall k
   . (Testable k, M.SymMonoidal k, TestOb (M.Unit @k))
  => (forall (a :: k) r. (TestOb a) => ((Ob a, Hypergraph.Frobenius a) => r) -> r)
  -> (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
propHypergraph :: forall k.
(Testable k, SymMonoidal k, TestOb Unit) =>
(forall (a :: k) r. TestOb a => ((Ob a, Frobenius a) => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a ** b) => r) -> r)
-> TestTree
propHypergraph forall (a :: k) r. TestOb a => ((Ob a, Frobenius a) => r) -> r
withFrob forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 = String -> Property () -> TestTree
testProperty String
"Hypergraph (Frobenius supply)" (Property () -> TestTree) -> Property () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  withFrob @a (propFrobenius @a (\ @x @y TestOb (a ** b) => r
r -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @x @y r
TestOb (a ** b) => r
r))

propHypergraph_
  :: forall k
   . (Testable k, M.SymMonoidal k, TestObIsOb k, forall (a :: k). (TestOb a) => Hypergraph.Frobenius a)
  => TestTree
propHypergraph_ :: forall k.
(Testable k, SymMonoidal k, TestObIsOb k,
 forall (a :: k). TestOb a => Frobenius a) =>
TestTree
propHypergraph_ = forall k.
(Testable k, SymMonoidal k, TestOb Unit) =>
(forall (a :: k) r. TestOb a => ((Ob a, Frobenius a) => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a ** b) => r) -> r)
-> TestTree
propHypergraph @k (\(Ob a, Frobenius a) => r
r -> r
(Ob a, Frobenius a) => r
r) (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)

testProfunctor :: forall {j} {k} (p :: j +-> k). (TestableProfunctor p) => TestTree
testProfunctor :: forall {j} {k} (p :: j +-> k). TestableProfunctor p => TestTree
testProfunctor = String -> Property () -> TestTree
testProperty String
"Profunctor" (forall {j} {k} (p :: j +-> k). TestableProfunctor p => Property ()
forall (p :: j +-> k). TestableProfunctor p => Property ()
propProfunctor @p)

propProfunctor :: forall {j} {k} (p :: j +-> k). (TestableProfunctor p) => Property ()
propProfunctor :: forall {j} {k} (p :: j +-> k). TestableProfunctor p => Property ()
propProfunctor = forall {j} {k} (p :: j +-> k).
(Profunctor p, Testable j, Testable k) =>
Property (SomeProfunctorElt p)
-> (forall (a :: k) (b :: j) r.
    (TestOb a, TestOb b) =>
    (TestingEqShow (p a b) => r) -> r)
-> Property ()
forall (p :: j +-> k).
(Profunctor p, Testable j, Testable k) =>
Property (SomeProfunctorElt p)
-> (forall (a :: k) (b :: j) r.
    (TestOb a, TestOb b) =>
    (TestingEqShow (p a b) => r) -> r)
-> Property ()
propProfunctorWith @p (String -> Property (SomeProfunctorElt p)
forall {j} {k} (p :: j +-> k).
TestableProfunctor p =>
String -> Property (SomeProfunctorElt p)
genProfunctorElt String
"p") (\TestingEqShow (p a b) => r
r -> r
TestingEqShow (p a b) => r
r)

propProfunctorWith
  :: forall {j} {k} (p :: j +-> k)
   . (Profunctor p, Testable j, Testable k)
  => Property (SomeProfunctorElt p)
  -> (forall a b r. (TestOb a, TestOb b) => ((TestingEqShow (p a b)) => r) -> r)
  -> Property ()
propProfunctorWith :: forall {j} {k} (p :: j +-> k).
(Profunctor p, Testable j, Testable k) =>
Property (SomeProfunctorElt p)
-> (forall (a :: k) (b :: j) r.
    (TestOb a, TestOb b) =>
    (TestingEqShow (p a b) => r) -> r)
-> Property ()
propProfunctorWith Property (SomeProfunctorElt p)
genPro forall (a :: k) (b :: j) r.
(TestOb a, TestOb b) =>
(TestingEqShow (p a b) => r) -> r
withEqShow = do
  SomeP @a @b p <- Property (SomeProfunctorElt p)
genPro
  withEqShow @a @b $
    testEq "identity" "dimap id id p" (dimap id id p) "p" p
  Some @c <- genObSuchThat @k \(Some @c) -> forall a. TestableType a => Bool
isGenNonEmpty @(c ~> a)
  Some @d <- genObSuchThat @j \(Some @d) -> forall a. TestableType a => Bool
isGenNonEmpty @(b ~> d)
  f <- genNamed @(c ~> a) "f"
  g <- genNamed @(b ~> d) "g"
  withEqShow @c @d $
    testEq "interchange" "lmap f (rmap g p)" (lmap f (rmap g p)) "rmap g (lmap f p)" (rmap g (lmap f p))
  Some @e <- genObSuchThat @k \(Some @e) -> forall a. TestableType a => Bool
isGenNonEmpty @(e ~> c)
  Some @h <- genObSuchThat @j \(Some @h) -> forall a. TestableType a => Bool
isGenNonEmpty @(d ~> h)
  f' <- genNamed @(e ~> c) "f'"
  g' <- genNamed @(d ~> h) "g'"
  withEqShow @e @h $
    testEq
      "composition"
      "dimap (f . f') (g' . g) p"
      (dimap (f . f') (g' . g) p)
      "dimap f' g' (dimap f g p)"
      (dimap f' g' (dimap f g p))

-- | Check the functor laws of a 'Functor.Functor' @f@: @map id = id@ and @map (g . f) = map g . map
-- f@. The witness lifts 'TestOb' along @f@ (usually @\\ \@a r -> r@ when @'TestOb' (f a)@ follows
-- from @'TestOb' a@). Functors encoded as representable profunctors ('Functor.FunctorForRep') are
-- instead tested via their @'Proarrow.Profunctor.Representable.Rep'@ with 'propProfunctor', since
-- the profunctor laws on @Rep f@ are the functor laws on @f@.
propFunctor
  :: forall {k1} {k2} (f :: k1 -> k2)
   . (Functor.Functor f, Testable k1, Testable k2)
  => (forall (a :: k1) r. (TestOb a) => ((TestOb (f a)) => r) -> r)
  -> Property ()
propFunctor :: forall {k1} {k2} (f :: k1 -> k2).
(Functor f, Testable k1, Testable k2) =>
(forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r)
-> Property ()
propFunctor forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r
withTestObF = do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k1
  Some @b <- genObSuchThat @k1 \(Some @b) -> forall a. TestableType a => Bool
isGenNonEmpty @(a ~> b)
  Some @c <- genObSuchThat @k1 \(Some @c) -> forall a. TestableType a => Bool
isGenNonEmpty @(b ~> c)
  f <- genNamed @(a ~> b) "f"
  g <- genNamed @(b ~> c) "g"
  withTestObF @a $
    withTestObF @c $
      -- 'Functor.withObF' recovers @Ob (f a)@\/@Ob (f c)@ from the functor (GHC will not extract
      -- them from the quantified @Ob' (f a)@ superclass on its own)
      Functor.withObF @f @a $
        Functor.withObF @f @c $ do
          testEq "identity" "map id" (Functor.map @f (obj @a)) "id" (obj @(f a))
          testEq
            "composition"
            "map (g . f)"
            (Functor.map @f (g . f))
            "map g . map f"
            (Functor.map @f g . Functor.map @f f)

testFunctor
  :: forall {k1} {k2} (f :: k1 -> k2)
   . (Functor.Functor f, Testable k1, Testable k2)
  => (forall (a :: k1) r. (TestOb a) => ((TestOb (f a)) => r) -> r)
  -> TestTree
testFunctor :: forall {k1} {k2} (f :: k1 -> k2).
(Functor f, Testable k1, Testable k2) =>
(forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r)
-> TestTree
testFunctor forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r
withTestObF = String -> Property () -> TestTree
testProperty String
"Functor" (forall {k1} {k2} (f :: k1 -> k2).
(Functor f, Testable k1, Testable k2) =>
(forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r)
-> Property ()
forall (f :: k1 -> k2).
(Functor f, Testable k1, Testable k2) =>
(forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r)
-> Property ()
propFunctor @f (\ @a TestOb (f a) => r
r -> forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r
withTestObF @a r
TestOb (f a) => r
r))

testFunctor_
  :: forall {k1} {k2} (f :: k1 -> k2)
   . (Functor.Functor f, Testable k1, Testable k2, forall (a :: k1). (TestOb a) => TestOb' (f a))
  => TestTree
testFunctor_ :: forall {k1} {k2} (f :: k1 -> k2).
(Functor f, Testable k1, Testable k2,
 forall (a :: k1). TestOb a => TestOb' (f a)) =>
TestTree
testFunctor_ = forall {k1} {k2} (f :: k1 -> k2).
(Functor f, Testable k1, Testable k2) =>
(forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r)
-> TestTree
forall (f :: k1 -> k2).
(Functor f, Testable k1, Testable k2) =>
(forall (a :: k1) r. TestOb a => (TestOb (f a) => r) -> r)
-> TestTree
testFunctor @f (\TestOb (f a) => r
r -> r
TestOb (f a) => r
r)

propNaturalTransformation
  :: forall {j} {k} (p :: j +-> k) q. (TestableProfunctor p, TestableProfunctor q) => p :~> q -> Property ()
propNaturalTransformation :: forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(TestableProfunctor p, TestableProfunctor q) =>
(p :~> q) -> Property ()
propNaturalTransformation p :~> q
n = do
  SomeP @a @b p <- 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 <- genOb @k
  Some @d <- genOb @j
  f <- genNamed @(c ~> a) "f"
  g <- genNamed @(b ~> d) "g"
  testEq "naturality" "n (dimap f g p)" (n (dimap f g p)) "dimap f g (n p)" (dimap f g (n p))

-- | Check the 'Representable' laws of @p@: 'index' and 'tabulate' are mutually inverse (@p a b@ is
-- naturally isomorphic to @a '~>' p '%' b@), and that iso is natural --
-- @'index' ('dimap' f g p) = 'repMap' g '.' 'index' p '.' f@ -- which is what pins 'repMap' down as
-- the functorial action of the representing functor @p '%' -@. The witness lifts 'TestOb' along
-- @p '%' -@. Unlike the hom-level 'propAdjunction', this generates @p a b@ elements, so it needs @p@
-- to be an element-generatable 'TestableProfunctor'.
propRepresentable
  :: forall {j} {k} (p :: j +-> k)
   . (Representable p, TestableProfunctor p)
  => (forall (b :: j) r. (TestOb b) => ((TestOb (p % b)) => r) -> r)
  -> Property ()
propRepresentable :: forall {j} {k} (p :: j +-> k).
(Representable p, TestableProfunctor p) =>
(forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> Property ()
propRepresentable forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r
withTestObRep = do
  SomeP @a @b p <- 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"
  testEq "tabulate . index" "tabulate (index p)" (tabulate @p (index p)) "p" p
  withTestObRep @b @(Property ()) do
    f <- genNamed @(a ~> p % b) "f"
    testEq "index . tabulate" "index (tabulate f)" (index @p (tabulate @p @b @a f)) "f" f
  Some @c <- genObSuchThat @k \(Some @c) -> forall a. TestableType a => Bool
isGenNonEmpty @(c ~> a)
  Some @d <- genObSuchThat @j \(Some @d) -> forall a. TestableType a => Bool
isGenNonEmpty @(b ~> d)
  fc <- genNamed @(c ~> a) "f"
  gd <- genNamed @(b ~> d) "g"
  withTestObRep @d @(Property ()) do
    testEq
      "index naturality"
      "index (dimap f g p)"
      (index @p (dimap fc gd p))
      "repMap g . index p . f"
      (repMap @p gd . index @p p . fc)

testRepresentable
  :: forall {j} {k} (p :: j +-> k)
   . (Representable p, TestableProfunctor p)
  => (forall (b :: j) r. (TestOb b) => ((TestOb (p % b)) => r) -> r)
  -> TestTree
testRepresentable :: forall {j} {k} (p :: j +-> k).
(Representable p, TestableProfunctor p) =>
(forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> TestTree
testRepresentable forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r
withTestObRep = String -> Property () -> TestTree
testProperty String
"Representable" (forall {j} {k} (p :: j +-> k).
(Representable p, TestableProfunctor p) =>
(forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> Property ()
forall (p :: j +-> k).
(Representable p, TestableProfunctor p) =>
(forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> Property ()
propRepresentable @p (\ @b TestOb (p % b) => r
r -> forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r
withTestObRep @b r
TestOb (p % b) => r
r))

testRepresentable_
  :: forall {j} {k} (p :: j +-> k)
   . (Representable p, TestableProfunctor p, TestObIsOb k)
  => TestTree
testRepresentable_ :: forall {j} {k} (p :: j +-> k).
(Representable p, TestableProfunctor p, TestObIsOb k) =>
TestTree
testRepresentable_ = forall {j} {k} (p :: j +-> k).
(Representable p, TestableProfunctor p) =>
(forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> TestTree
forall (p :: j +-> k).
(Representable p, TestableProfunctor p) =>
(forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> TestTree
testRepresentable @p (\ @b TestOb (p % b) => r
r -> 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 @b r
Ob (p % b) => r
TestOb (p % b) => r
r)

-- | Check the 'Corepresentable' laws of @p@, dual to 'propRepresentable': 'coindex' and 'cotabulate'
-- are mutually inverse (@p a b@ is naturally isomorphic to @p '%%' a '~>' b@), and that iso is
-- natural -- @'coindex' ('dimap' f g p) = g '.' 'coindex' p '.' 'corepMap' f@, pinning down 'corepMap'
-- as the functorial action of the corepresenting functor @p '%%' -@. The witness lifts 'TestOb' along
-- @p '%%' -@.
propCorepresentable
  :: forall {j} {k} (p :: j +-> k)
   . (Corepresentable p, TestableProfunctor p)
  => (forall (a :: k) r. (TestOb a) => ((TestOb (p %% a)) => r) -> r)
  -> Property ()
propCorepresentable :: forall {j} {k} (p :: j +-> k).
(Corepresentable p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> Property ()
propCorepresentable forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r
withTestObCorep = do
  SomeP @a @b p <- 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"
  testEq "cotabulate . coindex" "cotabulate (coindex p)" (cotabulate @p (coindex p)) "p" p
  withTestObCorep @a @(Property ()) do
    f <- genNamed @(p %% a ~> b) "f"
    testEq "coindex . cotabulate" "coindex (cotabulate f)" (coindex @p (cotabulate @p @a @b f)) "f" f
  Some @c <- genObSuchThat @k \(Some @c) -> forall a. TestableType a => Bool
isGenNonEmpty @(c ~> a)
  Some @d <- genObSuchThat @j \(Some @d) -> forall a. TestableType a => Bool
isGenNonEmpty @(b ~> d)
  fc <- genNamed @(c ~> a) "f"
  gd <- genNamed @(b ~> d) "g"
  withTestObCorep @c @(Property ()) do
    testEq
      "coindex naturality"
      "coindex (dimap f g p)"
      (coindex @p (dimap fc gd p))
      "g . coindex p . corepMap f"
      (gd . coindex @p p . corepMap @p fc)

testCorepresentable
  :: forall {j} {k} (p :: j +-> k)
   . (Corepresentable p, TestableProfunctor p)
  => (forall (a :: k) r. (TestOb a) => ((TestOb (p %% a)) => r) -> r)
  -> TestTree
testCorepresentable :: forall {j} {k} (p :: j +-> k).
(Corepresentable p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> TestTree
testCorepresentable forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r
withTestObCorep = String -> Property () -> TestTree
testProperty String
"Corepresentable" (forall {j} {k} (p :: j +-> k).
(Corepresentable p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> Property ()
forall (p :: j +-> k).
(Corepresentable p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> Property ()
propCorepresentable @p (\ @a TestOb (p %% a) => r
r -> forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r
withTestObCorep @a r
TestOb (p %% a) => r
r))

testCorepresentable_
  :: forall {j} {k} (p :: j +-> k)
   . (Corepresentable p, TestableProfunctor p, TestObIsOb j)
  => TestTree
testCorepresentable_ :: forall {j} {k} (p :: j +-> k).
(Corepresentable p, TestableProfunctor p, TestObIsOb j) =>
TestTree
testCorepresentable_ = forall {j} {k} (p :: j +-> k).
(Corepresentable p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> TestTree
forall (p :: j +-> k).
(Corepresentable p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> TestTree
testCorepresentable @p (\ @a TestOb (p %% a) => r
r -> 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 @a r
Ob (p %% a) => r
TestOb (p %% a) => r
r)

-- | Check the adjunction laws of an 'Adjunction' @p@. An adjunction here is exactly a profunctor that
-- is both 'Representable' and 'Corepresentable' -- its left adjoint is @L = p '%%' -@ and its right
-- adjoint @R = p '%' -@ -- and it carries no laws of its own beyond theirs ('leftAdjunct'\/'rightAdjunct'
-- are just @'index' '.' 'cotabulate'@ and @'coindex' '.' 'tabulate'@). So this simply delegates to
-- 'propCorepresentable' (for @L@) and 'propRepresentable' (for @R@); the two witnesses lift 'TestOb'
-- along @L@ and @R@ respectively.
propAdjunction
  :: forall {j} {k} (p :: j +-> k)
   . (Adjunction p, TestableProfunctor p)
  => (forall (a :: k) r. (TestOb a) => ((TestOb (p %% a)) => r) -> r)
  -> (forall (b :: j) r. (TestOb b) => ((TestOb (p % b)) => r) -> r)
  -> Property ()
propAdjunction :: forall {j} {k} (p :: j +-> k).
(Adjunction p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> Property ()
propAdjunction forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r
withTestObL forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r
withTestObR = do
  forall {j} {k} (p :: j +-> k).
(Corepresentable p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> Property ()
forall (p :: j +-> k).
(Corepresentable p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> Property ()
propCorepresentable @p (\ @a TestOb (p %% a) => r
r -> forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r
withTestObL @a r
TestOb (p %% a) => r
r)
  forall {j} {k} (p :: j +-> k).
(Representable p, TestableProfunctor p) =>
(forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> Property ()
forall (p :: j +-> k).
(Representable p, TestableProfunctor p) =>
(forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> Property ()
propRepresentable @p (\ @b TestOb (p % b) => r
r -> forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r
withTestObR @b r
TestOb (p % b) => r
r)

testAdjunction
  :: forall {j} {k} (p :: j +-> k)
   . (Adjunction p, TestableProfunctor p)
  => (forall (a :: k) r. (TestOb a) => ((TestOb (p %% a)) => r) -> r)
  -> (forall (b :: j) r. (TestOb b) => ((TestOb (p % b)) => r) -> r)
  -> TestTree
testAdjunction :: forall {j} {k} (p :: j +-> k).
(Adjunction p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> TestTree
testAdjunction forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r
withTestObL forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r
withTestObR =
  String -> Property () -> TestTree
testProperty String
"Adjunction" (forall {j} {k} (p :: j +-> k).
(Adjunction p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> Property ()
forall (p :: j +-> k).
(Adjunction p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> Property ()
propAdjunction @p (\ @a TestOb (p %% a) => r
r -> forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r
withTestObL @a r
TestOb (p %% a) => r
r) (\ @b TestOb (p % b) => r
r -> forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r
withTestObR @b r
TestOb (p % b) => r
r))

testAdjunction_
  :: forall {j} {k} (p :: j +-> k)
   . (Adjunction p, TestableProfunctor p, TestObIsOb j, TestObIsOb k)
  => TestTree
testAdjunction_ :: forall {j} {k} (p :: j +-> k).
(Adjunction p, TestableProfunctor p, TestObIsOb j, TestObIsOb k) =>
TestTree
testAdjunction_ = forall {j} {k} (p :: j +-> k).
(Adjunction p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> TestTree
forall (p :: j +-> k).
(Adjunction p, TestableProfunctor p) =>
(forall (a :: k) r. TestOb a => (TestOb (p %% a) => r) -> r)
-> (forall (b :: j) r. TestOb b => (TestOb (p % b) => r) -> r)
-> TestTree
testAdjunction @p (\ @a TestOb (p %% a) => r
r -> 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 @a r
Ob (p %% a) => r
TestOb (p %% a) => r
r) (\ @b TestOb (p % b) => r
r -> 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 @b r
Ob (p % b) => r
TestOb (p % b) => r
r)

propIso :: forall {k} (a :: k) b. (Testable k, TestOb a, TestOb b) => a ~> b -> b ~> a -> Property ()
propIso :: forall {k} (a :: k) (b :: k).
(Testable k, TestOb a, TestOb b) =>
(a ~> b) -> (b ~> a) -> Property ()
propIso a ~> b
f b ~> a
g = do
  String -> String -> (b ~> b) -> String -> (b ~> b) -> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq String
"right inverse" String
"f . g" (a ~> b
f (a ~> b) -> (b ~> a) -> b ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b ~> a
g) String
"id" b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  String -> String -> (a ~> a) -> String -> (a ~> a) -> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq String
"left inverse" String
"g . f" (b ~> a
g (b ~> a) -> (a ~> b) -> a ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f) String
"id" a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

propIso'
  :: forall {k} c (a :: k) b
   . (Testable k, TestOb a, TestOb b, (Ob b) => c (ExOptic GetterFl b b), (Ob b) => c (ExOptic (Flip GetterFl) b b))
  => Optic c a a b b -> Property ()
propIso' :: forall {k} (c :: (k -> k -> Type) -> Constraint) (a :: k) (b :: k).
(Testable k, TestOb a, TestOb b, Ob b => c (ExOptic GetterFl b b),
 Ob b => c (ExOptic (Flip GetterFl) b b)) =>
Optic c a a b b -> Property ()
propIso' Optic c a a b b
o = (a ~> b) -> (b ~> a) -> Property ()
forall {k} (a :: k) (b :: k).
(Testable k, TestOb a, TestOb b) =>
(a ~> b) -> (b ~> a) -> Property ()
propIso (Optic c a a b b -> a ~> b
forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k,
 (Ob a, Ob b) => c (ExOptic GetterFl a b)) =>
Optic c s t a b -> s ~> a
view Optic c a a b b
o) (Optic c a a b b -> b ~> a
forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k,
 (Ob a, Ob b) => c (ExOptic (Flip GetterFl) a b)) =>
Optic c s t a b -> b ~> t
review Optic c a a b b
o)

propIsoP
  :: forall p q a b c d
   . (TestableTypeP p, TestableTypeP q, TestOb a, TestOb b, TestOb c, TestOb d)
  => (p a b -> q c d) -> (q c d -> p a b) -> Property ()
propIsoP :: forall {j} {k} {j} {k} (p :: j +-> k) (q :: j +-> k) (a :: k)
       (b :: j) (c :: k) (d :: j).
(TestableTypeP p, TestableTypeP q, TestOb a, TestOb b, TestOb c,
 TestOb d) =>
(p a b -> q c d) -> (q c d -> p a b) -> Property ()
propIsoP p a b -> q c d
f q c d -> p a b
g = do
  p <- forall a. TestableType a => String -> Property a
genNamed @(p a b) String
"p"
  testEq "left inverse" "g (f p)" (g (f p)) "p" p
  q <- genNamed @(q c d) "q"
  testEq "right inverse" "f (g q)" (f (g q)) "q" q

propNaturalIsoP
  :: forall {j} {k} (p :: j +-> k) q
   . (TestableProfunctor p, TestableTypeP p, TestableProfunctor q, TestableTypeP q)
  => (p :~> q) -> (q :~> p) -> Property ()
propNaturalIsoP :: forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(TestableProfunctor p, TestableTypeP p, TestableProfunctor q,
 TestableTypeP q) =>
(p :~> q) -> (q :~> p) -> Property ()
propNaturalIsoP p :~> q
f q :~> p
g = do
  Some @a <- forall k. Testable k => Property (Some k)
genOb @k
  Some @b <- genOb @j
  propIsoP @p @q @a @b f g
  propNaturalTransformation f
  propNaturalTransformation g

propMonoid
  :: forall {k} m
   . (Testable k, Monoid.Monoid (m :: k), TestOb m, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> Property ()
propMonoid :: forall {k} (m :: k).
(Testable k, Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propMonoid forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 =
  forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @M.Unit @m ((TestOb (Unit ** m) => Property ()) -> Property ())
-> (TestOb (Unit ** m) => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$
    forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @m @M.Unit ((TestOb (m ** Unit) => Property ()) -> Property ())
-> (TestOb (m ** Unit) => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$ do
      String
-> String
-> ((Unit ** m) ~> m)
-> String
-> ((Unit ** m) ~> m)
-> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq
        String
"left identity"
        String
"μ . (η ⊗ 1)"
        ((m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend ((m ** m) ~> m) -> ((Unit ** m) ~> (m ** m)) -> (Unit ** m) ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
Monoid.mempty @m (Unit ~> m) -> (m ~> m) -> (Unit ** m) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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.** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m))
        String
"λ"
        (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
M.leftUnitor @k @m)
      String
-> String
-> ((m ** Unit) ~> m)
-> String
-> ((m ** Unit) ~> m)
-> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq
        String
"right identity"
        String
"μ . (1 ⊗ η)"
        ((m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend ((m ** m) ~> m) -> ((m ** Unit) ~> (m ** m)) -> (m ** Unit) ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m (m ~> m) -> (Unit ~> m) -> (m ** Unit) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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.** forall (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
Monoid.mempty @m))
        String
"ρ"
        (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
M.rightUnitor @k @m)
      forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @m @m ((TestOb (m ** m) => Property ()) -> Property ())
-> (TestOb (m ** m) => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$ forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @(m M.** m) @m ((TestOb ((m ** m) ** m) => Property ()) -> Property ())
-> (TestOb ((m ** m) ** m) => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$ do
        String
-> String
-> (((m ** m) ** m) ~> m)
-> String
-> (((m ** m) ** m) ~> m)
-> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq
          String
"associativity"
          String
"μ . (μ ⊗ 1)"
          (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend @m ((m ** m) ~> m)
-> (((m ** m) ** m) ~> (m ** m)) -> ((m ** m) ** m) ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend @m ((m ** m) ~> m) -> (m ~> m) -> ((m ** m) ** m) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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.** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m))
          String
"μ . (1 ⊗ μ) . α"
          ((m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend ((m ** m) ~> m)
-> (((m ** m) ** m) ~> (m ** m)) -> ((m ** m) ** m) ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m (m ~> m) -> ((m ** m) ~> m) -> (m ** (m ** m)) ~> (m ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (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.** forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend @m) ((m ** (m ** m)) ~> (m ** m))
-> (((m ** m) ** m) ~> (m ** (m ** m)))
-> ((m ** m) ** m) ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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 @m @m @m)

propCommutativeMonoid
  :: forall {k} m
   . (Testable k, Monoid.CommutativeMonoid (m :: k), TestOb m, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> Property ()
propCommutativeMonoid :: forall {k} (m :: k).
(Testable k, CommutativeMonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propCommutativeMonoid forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 = do
  forall (m :: k).
(Testable k, Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
forall {k} (m :: k).
(Testable k, Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propMonoid @m (\ @x @y TestOb (a ** b) => r
r -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @x @y r
TestOb (a ** b) => r
r)
  forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @m @m ((TestOb (m ** m) => Property ()) -> Property ())
-> (TestOb (m ** m) => Property ()) -> Property ()
forall a b. (a -> b) -> a -> b
$
    String
-> String
-> ((m ** m) ~> m)
-> String
-> ((m ** m) ~> m)
-> Property ()
forall a.
TestingEqShow a =>
String -> String -> a -> String -> a -> Property ()
testEq
      String
"commutativity"
      String
"mappend . swap"
      (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend @m ((m ** m) ~> m) -> ((m ** m) ~> (m ** m)) -> (m ** m) ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
M.swap @k @m @m)
      String
"mappend"
      (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
Monoid.mappend @m)

propCocommutativeComonoid
  :: forall {k} m
   . (Testable k, Monoid.CocommutativeComonoid (m :: k), TestOb m, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> Property ()
propCocommutativeComonoid :: forall {k} (m :: k).
(Testable k, CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propCocommutativeComonoid forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 = do
  forall {k} (m :: k).
(Testable k, CommutativeMonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
forall (m :: OPPOSITE k).
(Testable (OPPOSITE k), CommutativeMonoid m, TestOb m,
 TestOb Unit) =>
(forall (a :: OPPOSITE k) (b :: OPPOSITE k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propCommutativeMonoid @(OP m) (\ @(OP x) @(OP y) TestOb (a ** b) => r
r -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
withTestOb2 @x @y r
TestOb (UN 'OP a ** UN 'OP b) => r
TestOb (a ** b) => r
r)

testMonoid
  :: forall {k} m
   . (Testable k, Monoid.Monoid (m :: k), TestOb m, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
testMonoid :: forall {k} (m :: k).
(Testable k, Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testMonoid forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f = String -> Property () -> TestTree
testProperty (String
"Monoid " String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => String
showOb @k @m) (forall (m :: k).
(Testable k, Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
forall {k} (m :: k).
(Testable k, Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propMonoid @m \ @a @b -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f @a @b)

testMonoid_
  :: forall {k} m
   . (Testable k, Monoid.Monoid (m :: k), TestObIsOb k)
  => TestTree
testMonoid_ :: forall {k} (m :: k).
(Testable k, Monoid m, TestObIsOb k) =>
TestTree
testMonoid_ = forall (m :: k).
(Testable k, Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
forall {k} (m :: k).
(Testable k, Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testMonoid @m (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)

testComonoid
  :: forall {k} m
   . (Testable k, Monoid.Comonoid (m :: k), TestOb m, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
testComonoid :: forall {k} (m :: k).
(Testable k, Comonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testComonoid forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f = String -> Property () -> TestTree
testProperty (String
"Comonoid " String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => String
showOb @k @m) (forall {k} (m :: k).
(Testable k, Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
forall (m :: OPPOSITE k).
(Testable (OPPOSITE k), Monoid m, TestOb m, TestOb Unit) =>
(forall (a :: OPPOSITE k) (b :: OPPOSITE k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propMonoid @(OP m) \ @(OP a) @(OP b) TestOb (a ** b) => r
r -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f @a @b r
TestOb (UN 'OP a ** UN 'OP b) => r
TestOb (a ** b) => r
r)

testComonoid_
  :: forall {k} m
   . (Testable k, Monoid.Comonoid (m :: k), TestObIsOb k)
  => TestTree
testComonoid_ :: forall {k} (m :: k).
(Testable k, Comonoid m, TestObIsOb k) =>
TestTree
testComonoid_ = forall (m :: k).
(Testable k, Comonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
forall {k} (m :: k).
(Testable k, Comonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testComonoid @m (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)

testCommutativeMonoid
  :: forall {k} m
   . (Testable k, Monoid.CommutativeMonoid (m :: k), TestOb m, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
testCommutativeMonoid :: forall {k} (m :: k).
(Testable k, CommutativeMonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testCommutativeMonoid forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f = String -> Property () -> TestTree
testProperty (String
"CommutativeMonoid " String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => String
showOb @k @m) (forall (m :: k).
(Testable k, CommutativeMonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
forall {k} (m :: k).
(Testable k, CommutativeMonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propCommutativeMonoid @m \ @a @b -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f @a @b)

testCommutativeMonoid_
  :: forall {k} m
   . (Testable k, Monoid.CommutativeMonoid (m :: k), TestObIsOb k)
  => TestTree
testCommutativeMonoid_ :: forall {k} (m :: k).
(Testable k, CommutativeMonoid m, TestObIsOb k) =>
TestTree
testCommutativeMonoid_ = forall (m :: k).
(Testable k, CommutativeMonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
forall {k} (m :: k).
(Testable k, CommutativeMonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testCommutativeMonoid @m (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)

testCocommutativeComonoid
  :: forall {k} m
   . (Testable k, Monoid.CocommutativeComonoid (m :: k), TestOb m, TestOb (M.Unit @k))
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
testCocommutativeComonoid :: forall {k} (m :: k).
(Testable k, CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testCocommutativeComonoid forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f = String -> Property () -> TestTree
testProperty (String
"CocommutativeComonoid " String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => String
showOb @k @m) (forall (m :: k).
(Testable k, CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
forall {k} (m :: k).
(Testable k, CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propCocommutativeComonoid @m \ @a @b -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f @a @b)

testCocommutativeComonoid_
  :: forall {k} m
   . (Testable k, Monoid.CocommutativeComonoid (m :: k), TestObIsOb k)
  => TestTree
testCocommutativeComonoid_ :: forall {k} (m :: k).
(Testable k, CocommutativeComonoid m, TestObIsOb k) =>
TestTree
testCocommutativeComonoid_ = forall (m :: k).
(Testable k, CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
forall {k} (m :: k).
(Testable k, CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testCocommutativeComonoid @m (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)

testFrobenius
  :: forall {k} (m :: k)
   . ( Testable k
     , Monoid.CommutativeMonoid m
     , Monoid.CocommutativeComonoid m
     , TestOb m
     , TestOb (M.Unit @k)
     )
  => (forall (a :: k) b r. (TestOb a, TestOb b) => ((TestOb (a M.** b)) => r) -> r)
  -> TestTree
testFrobenius :: forall {k} (m :: k).
(Testable k, CommutativeMonoid m, CocommutativeComonoid m,
 TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testFrobenius forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f = String -> Property () -> TestTree
testProperty (String
"Frobenius " String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall k (a :: k). (Testable k, TestOb a) => String
showOb @k @m) (forall (m :: k).
(Testable k, SymMonoidal k, CommutativeMonoid m,
 CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
forall {k} (m :: k).
(Testable k, SymMonoidal k, CommutativeMonoid m,
 CocommutativeComonoid m, TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> Property ()
propFrobenius @m \ @a @b -> forall (a :: k) (b :: k) r.
(TestOb a, TestOb b) =>
(TestOb (a ** b) => r) -> r
f @a @b)

testFrobenius_
  :: forall {k} (m :: k)
   . ( Testable k
     , Monoid.CommutativeMonoid m
     , Monoid.CocommutativeComonoid m
     , TestObIsOb k
     )
  => TestTree
testFrobenius_ :: forall {k} (m :: k).
(Testable k, CommutativeMonoid m, CocommutativeComonoid m,
 TestObIsOb k) =>
TestTree
testFrobenius_ = forall (m :: k).
(Testable k, CommutativeMonoid m, CocommutativeComonoid m,
 TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
forall {k} (m :: k).
(Testable k, CommutativeMonoid m, CocommutativeComonoid m,
 TestOb m, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> TestTree
testFrobenius @m (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)