    {-# LANGUAGE CPP #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE QuantifiedConstraints #-}
    {-# LANGUAGE RankNTypes #-}

    #ifndef HAVE_COMONAD

    module Hedgehog.Classes.Comonad () where

    #else

    module Hedgehog.Classes.Comonad (comonadLaws) where

    import Control.Comonad

    import Hedgehog
    import Hedgehog.Classes.Common

    -- | Tests the following 'Comonad' laws:
    --
    -- [__Extend/Extract Identity__]: @'extend' 'extract' ≡ 'id'@
    -- [__Extract/Extend__]: @'extract' '.' 'extend' f ≡ f@
    -- [__Extend/Extend__]: @'extend' f '.' 'extend' g ≡ 'extend' (f '.' 'extend' g)@
    -- [__Extract Right Identity__]: @f '=>=' 'extract' ≡ f@
    -- [__Extract Left Identity__]: @'extract' '=>=' f ≡ f@
    -- [__Cokleisli Associativity__]: @(f '=>=' g) '=>=' h ≡ f '=>=' (g '=>=' h)@
    -- [__Extract/Duplicate Identity__]: @'extract' '.' 'duplicate' ≡ 'id'@
    -- [__Fmap Extract/Duplicate Identity__]: @'fmap' 'extract' '.' 'duplicate' ≡ 'id'@
    -- [__Double Duplication__]: @'duplicate' '.' 'duplicate' ≡ 'fmap' 'duplicate' '.' 'duplicate'@
    -- [__Extend/Fmap . Duplicate Identity__]: @'extend' f ≡ 'fmap' f '.' 'duplicate'@
    -- [__Duplicate/Extend id Identity__]: @'duplicate' ≡ 'extend' 'id'@
    -- [__Fmap/Extend Extract__]: @'fmap' f ≡ 'extend' (f '.' 'extract')@
    -- [__Fmap/LiftW Isomorphism__]: @'fmap' ≡ 'liftW'@
    comonadLaws ::
      ( Comonad f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Laws
    comonadLaws :: forall (f :: * -> *).
    (Comonad f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Laws
    comonadLaws forall x. Gen x -> Gen (f x)
    gen = String -> [(String, Property)] -> Laws
    Laws String
    "Comonad"
      [ (String
    "Extend/Extract Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    extendExtractIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Extract/Extend", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    extractExtend Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Extend/Extend", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    extendExtend Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Extract Right Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    extractRightIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Extract Left Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    extractLeftIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Cokleisli Associativity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    cokleisliAssociativity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Extract/Duplicate Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    extractDuplicateIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Fmap Extract/Duplicate Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    fmapExtractDuplicateIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Double Duplication", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    doubleDup Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Extend/Fmap . Duplicate Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    extendDuplicate Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Duplicate/Extend id Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    duplicateExtendId Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Fmap/Extend Extract", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    fmapExtendExtract Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Fmap/LiftW Isomorphism", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). ComonadProp f
    fmapLiftW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      ]

    type ComonadProp f =
      ( Comonad f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property

    extendExtractIdentity :: forall f. ComonadProp f
    extendExtractIdentity :: forall (f :: * -> *). ComonadProp f
    extendExtractIdentity forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs :: f Integer
    lhs = (f Integer -> Integer) -> f Integer -> f Integer
    forall a b. (f a -> b) -> f a -> f b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend f Integer -> Integer
    forall a. f a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract f Integer
    x
      let rhs :: f Integer
    rhs = f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Extend/Extract Identity", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "extend extract" String -> String -> String
    `congruency` String
    "id"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "extend extract x" String -> String -> String
    `congruency` String
    "x, where"
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx f Integer
    lhs f Integer
    rhs Context
    ctx

    extractExtend :: forall f. ComonadProp f
    extractExtend :: forall (f :: * -> *). ComonadProp f
    extractExtend forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      LinearEquationW f
    k <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
    -> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall a b. (a -> b) -> a -> b
    $ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
    forall (w :: * -> *).
    Comonad w =>
    (forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
    genLinearEquationW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    fgen
      let k' :: f Integer -> Integer
    k' = LinearEquationW f -> f Integer -> Integer
    forall (w :: * -> *).
    Comonad w =>
    LinearEquationW w -> w Integer -> Integer
    runLinearEquationW LinearEquationW f
    k
      let lhs :: Integer
    lhs = f Integer -> Integer
    forall a. f a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract (f Integer -> Integer)
    -> (f Integer -> f Integer) -> f Integer -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (f Integer -> Integer) -> f Integer -> f Integer
    forall a b. (f a -> b) -> f a -> f b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend f Integer -> Integer
    k' (f Integer -> Integer) -> f Integer -> Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let rhs :: Integer
    rhs = f Integer -> Integer
    k' f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Extract/Extend", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "extract . extend f" String -> String -> String
    `congruency` String
    "f"
            , lawContextReduced :: String
    lawContextReduced = Integer -> Integer -> String
    forall a. Show a => a -> a -> String
    reduced Integer
    lhs Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "extract . extend f $ x" String -> String -> String
    `congruency` String
    "f x, where"
                , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquationW f -> String
    forall a. Show a => a -> String
    show LinearEquationW f
    k
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      Integer -> Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx Integer
    lhs Integer
    rhs Context
    ctx

    extendExtend :: forall f. ComonadProp f
    extendExtend :: forall (f :: * -> *). ComonadProp f
    extendExtend forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      LinearEquationW f
    f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
    -> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall a b. (a -> b) -> a -> b
    $ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
    forall (w :: * -> *).
    Comonad w =>
    (forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
    genLinearEquationW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    fgen
      LinearEquationW f
    g' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
    -> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall a b. (a -> b) -> a -> b
    $ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
    forall (w :: * -> *).
    Comonad w =>
    (forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
    genLinearEquationW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    fgen
      let f :: f Integer -> Integer
    f = LinearEquationW f -> f Integer -> Integer
    forall (w :: * -> *).
    Comonad w =>
    LinearEquationW w -> w Integer -> Integer
    runLinearEquationW LinearEquationW f
    f'
      let g :: f Integer -> Integer
    g = LinearEquationW f -> f Integer -> Integer
    forall (w :: * -> *).
    Comonad w =>
    LinearEquationW w -> w Integer -> Integer
    runLinearEquationW LinearEquationW f
    g'
      let lhs :: f Integer
    lhs = (f Integer -> Integer) -> f Integer -> f Integer
    forall a b. (f a -> b) -> f a -> f b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend f Integer -> Integer
    f (f Integer -> f Integer)
    -> (f Integer -> f Integer) -> f Integer -> f Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (f Integer -> Integer) -> f Integer -> f Integer
    forall a b. (f a -> b) -> f a -> f b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend f Integer -> Integer
    g (f Integer -> f Integer) -> f Integer -> f Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let rhs :: f Integer
    rhs = (f Integer -> Integer) -> f Integer -> f Integer
    forall a b. (f a -> b) -> f a -> f b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend (f Integer -> Integer
    f (f Integer -> Integer)
    -> (f Integer -> f Integer) -> f Integer -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (f Integer -> Integer) -> f Integer -> f Integer
    forall a b. (f a -> b) -> f a -> f b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend f Integer -> Integer
    g) f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Extend/Extend", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "extend f . extend g" String -> String -> String
    `congruency` String
    "extend (f . extend g)"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "extend f . extend g $ x" String -> String -> String
    `congruency` String
    "extend (f . extend g) $ x, where"
                , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquationW f -> String
    forall a. Show a => a -> String
    show LinearEquationW f
    f'
                , String
    "g = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquationW f -> String
    forall a. Show a => a -> String
    show LinearEquationW f
    g'
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx f Integer
    lhs f Integer
    rhs Context
    ctx

    extractRightIdentity :: forall f. ComonadProp f
    extractRightIdentity :: forall (f :: * -> *). ComonadProp f
    extractRightIdentity forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      LinearEquationW f
    f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
    -> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall a b. (a -> b) -> a -> b
    $ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
    forall (w :: * -> *).
    Comonad w =>
    (forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
    genLinearEquationW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    fgen
      let f :: f Integer -> Integer
    f = LinearEquationW f -> f Integer -> Integer
    forall (w :: * -> *).
    Comonad w =>
    LinearEquationW w -> w Integer -> Integer
    runLinearEquationW LinearEquationW f
    f'
      let lhs :: Integer
    lhs = f Integer -> Integer
    f (f Integer -> Integer)
    -> (f Integer -> Integer) -> f Integer -> Integer
    forall (w :: * -> *) a b c.
    Comonad w =>
    (w a -> b) -> (w b -> c) -> w a -> c
    =>= f Integer -> Integer
    forall a. f a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract (f Integer -> Integer) -> f Integer -> Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let rhs :: Integer
    rhs = f Integer -> Integer
    f f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Extract Cokleisli Right Identity", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "f =>= extract" String -> String -> String
    `congruency` String
    "f"
            , lawContextReduced :: String
    lawContextReduced = Integer -> Integer -> String
    forall a. Show a => a -> a -> String
    reduced Integer
    lhs Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "f =>= extract $ x" String -> String -> String
    `congruency` String
    "f x, where"
                , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquationW f -> String
    forall a. Show a => a -> String
    show LinearEquationW f
    f'
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      Integer -> Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx Integer
    lhs Integer
    rhs Context
    ctx

    extractLeftIdentity :: forall f. ComonadProp f
    extractLeftIdentity :: forall (f :: * -> *). ComonadProp f
    extractLeftIdentity forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      LinearEquationW f
    f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
    -> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall a b. (a -> b) -> a -> b
    $ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
    forall (w :: * -> *).
    Comonad w =>
    (forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
    genLinearEquationW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    fgen
      let f :: f Integer -> Integer
    f = LinearEquationW f -> f Integer -> Integer
    forall (w :: * -> *).
    Comonad w =>
    LinearEquationW w -> w Integer -> Integer
    runLinearEquationW LinearEquationW f
    f'
      let lhs :: Integer
    lhs = f Integer -> Integer
    forall a. f a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract (f Integer -> Integer)
    -> (f Integer -> Integer) -> f Integer -> Integer
    forall (w :: * -> *) a b c.
    Comonad w =>
    (w a -> b) -> (w b -> c) -> w a -> c
    =>= f Integer -> Integer
    f (f Integer -> Integer) -> f Integer -> Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let rhs :: Integer
    rhs = f Integer -> Integer
    f f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Extract Cokleisli Left Identity", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "extract =>= f" String -> String -> String
    `congruency` String
    "f"
            , lawContextReduced :: String
    lawContextReduced = Integer -> Integer -> String
    forall a. Show a => a -> a -> String
    reduced Integer
    lhs Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "extract =>= f $ x" String -> String -> String
    `congruency` String
    "f x, where"
                , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquationW f -> String
    forall a. Show a => a -> String
    show LinearEquationW f
    f'
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      Integer -> Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx Integer
    lhs Integer
    rhs Context
    ctx

    cokleisliAssociativity :: forall f. ComonadProp f
    cokleisliAssociativity :: forall (f :: * -> *). ComonadProp f
    cokleisliAssociativity forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      LinearEquationW f
    f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
    -> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall a b. (a -> b) -> a -> b
    $ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
    forall (w :: * -> *).
    Comonad w =>
    (forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
    genLinearEquationW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    fgen
      LinearEquationW f
    g' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
    -> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall a b. (a -> b) -> a -> b
    $ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
    forall (w :: * -> *).
    Comonad w =>
    (forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
    genLinearEquationW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    fgen
      LinearEquationW f
    h' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
    -> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall a b. (a -> b) -> a -> b
    $ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
    forall (w :: * -> *).
    Comonad w =>
    (forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
    genLinearEquationW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    fgen
      let f :: f Integer -> Integer
    f = LinearEquationW f -> f Integer -> Integer
    forall (w :: * -> *).
    Comonad w =>
    LinearEquationW w -> w Integer -> Integer
    runLinearEquationW LinearEquationW f
    f'
      let g :: f Integer -> Integer
    g = LinearEquationW f -> f Integer -> Integer
    forall (w :: * -> *).
    Comonad w =>
    LinearEquationW w -> w Integer -> Integer
    runLinearEquationW LinearEquationW f
    g'
      let h :: f Integer -> Integer
    h = LinearEquationW f -> f Integer -> Integer
    forall (w :: * -> *).
    Comonad w =>
    LinearEquationW w -> w Integer -> Integer
    runLinearEquationW LinearEquationW f
    h'
      let lhs :: Integer
    lhs = (f Integer -> Integer
    f (f Integer -> Integer)
    -> (f Integer -> Integer) -> f Integer -> Integer
    forall (w :: * -> *) a b c.
    Comonad w =>
    (w a -> b) -> (w b -> c) -> w a -> c
    =>= f Integer -> Integer
    g) (f Integer -> Integer)
    -> (f Integer -> Integer) -> f Integer -> Integer
    forall (w :: * -> *) a b c.
    Comonad w =>
    (w a -> b) -> (w b -> c) -> w a -> c
    =>= f Integer -> Integer
    h (f Integer -> Integer) -> f Integer -> Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let rhs :: Integer
    rhs = f Integer -> Integer
    f (f Integer -> Integer)
    -> (f Integer -> Integer) -> f Integer -> Integer
    forall (w :: * -> *) a b c.
    Comonad w =>
    (w a -> b) -> (w b -> c) -> w a -> c
    =>= (f Integer -> Integer
    g (f Integer -> Integer)
    -> (f Integer -> Integer) -> f Integer -> Integer
    forall (w :: * -> *) a b c.
    Comonad w =>
    (w a -> b) -> (w b -> c) -> w a -> c
    =>= f Integer -> Integer
    h) (f Integer -> Integer) -> f Integer -> Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Cokleisli Associativity", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "(f =>= g) =>= h" String -> String -> String
    `congruency` String
    "f =>= (g =>= h)"
            , lawContextReduced :: String
    lawContextReduced = Integer -> Integer -> String
    forall a. Show a => a -> a -> String
    reduced Integer
    lhs Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "(f =>= g) =>= h $ x" String -> String -> String
    `congruency` String
    "f =>= (g =>= h) $ x, where"
                , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquationW f -> String
    forall a. Show a => a -> String
    show LinearEquationW f
    f'
                , String
    "g = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquationW f -> String
    forall a. Show a => a -> String
    show LinearEquationW f
    g'
                , String
    "h = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquationW f -> String
    forall a. Show a => a -> String
    show LinearEquationW f
    h'
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      Integer -> Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx Integer
    lhs Integer
    rhs Context
    ctx

    extractDuplicateIdentity :: forall f. ComonadProp f
    extractDuplicateIdentity :: forall (f :: * -> *). ComonadProp f
    extractDuplicateIdentity forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs :: f Integer
    lhs = f (f Integer) -> f Integer
    forall a. f a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract (f (f Integer) -> f Integer)
    -> (f Integer -> f (f Integer)) -> f Integer -> f Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f Integer -> f (f Integer)
    forall a. f a -> f (f a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate (f Integer -> f Integer) -> f Integer -> f Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let rhs :: f Integer
    rhs = f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Extract/Duplicate Identity", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "extract . duplicate" String -> String -> String
    `congruency` String
    "id"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "extract . duplicate $ x" String -> String -> String
    `congruency` String
    "x, where"
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx f Integer
    lhs f Integer
    rhs Context
    ctx

    fmapExtractDuplicateIdentity :: forall f. ComonadProp f
    fmapExtractDuplicateIdentity :: forall (f :: * -> *). ComonadProp f
    fmapExtractDuplicateIdentity forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs :: f Integer
    lhs = (f Integer -> Integer) -> f (f Integer) -> f Integer
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap f Integer -> Integer
    forall a. f a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract (f (f Integer) -> f Integer)
    -> (f Integer -> f (f Integer)) -> f Integer -> f Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f Integer -> f (f Integer)
    forall a. f a -> f (f a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate (f Integer -> f Integer) -> f Integer -> f Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let rhs :: f Integer
    rhs = f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Fmap Extract/Duplicate Identity", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "fmap extract . duplicate" String -> String -> String
    `congruency` String
    "id"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "fmap extract . duplicate $ x" String -> String -> String
    `congruency` String
    "x, where"
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx f Integer
    lhs f Integer
    rhs Context
    ctx

    doubleDup :: forall f. ComonadProp f
    doubleDup :: forall (f :: * -> *). ComonadProp f
    doubleDup forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs :: f (f (f Integer))
    lhs = f (f Integer) -> f (f (f Integer))
    forall a. f a -> f (f a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate (f (f Integer) -> f (f (f Integer)))
    -> (f Integer -> f (f Integer)) -> f Integer -> f (f (f Integer))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f Integer -> f (f Integer)
    forall a. f a -> f (f a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate (f Integer -> f (f (f Integer))) -> f Integer -> f (f (f Integer))
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let rhs :: f (f (f Integer))
    rhs = (f Integer -> f (f Integer)) -> f (f Integer) -> f (f (f Integer))
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap f Integer -> f (f Integer)
    forall a. f a -> f (f a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate (f (f Integer) -> f (f (f Integer)))
    -> (f Integer -> f (f Integer)) -> f Integer -> f (f (f Integer))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f Integer -> f (f Integer)
    forall a. f a -> f (f a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate (f Integer -> f (f (f Integer))) -> f Integer -> f (f (f Integer))
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Double Duplicate", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "duplicate . duplicate" String -> String -> String
    `congruency` String
    "fmap duplicate . duplicate"
            , lawContextReduced :: String
    lawContextReduced = f (f (f Integer)) -> f (f (f Integer)) -> String
    forall a. Show a => a -> a -> String
    reduced f (f (f Integer))
    lhs f (f (f Integer))
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "duplicate . duplicate $ x" String -> String -> String
    `congruency` String
    "fmap duplicate . duplicate $ x, where"
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      f (f (f Integer))
    -> f (f (f Integer)) -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx f (f (f Integer))
    lhs f (f (f Integer))
    rhs Context
    ctx

    extendDuplicate :: forall f. ComonadProp f
    extendDuplicate :: forall (f :: * -> *). ComonadProp f
    extendDuplicate forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      LinearEquationW f
    f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
    -> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
    forall a b. (a -> b) -> a -> b
    $ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
    forall (w :: * -> *).
    Comonad w =>
    (forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
    genLinearEquationW Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    fgen
      let f :: f Integer -> Integer
    f = LinearEquationW f -> f Integer -> Integer
    forall (w :: * -> *).
    Comonad w =>
    LinearEquationW w -> w Integer -> Integer
    runLinearEquationW LinearEquationW f
    f'
      let lhs :: f Integer
    lhs = (f Integer -> Integer) -> f Integer -> f Integer
    forall a b. (f a -> b) -> f a -> f b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend f Integer -> Integer
    f (f Integer -> f Integer) -> f Integer -> f Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let rhs :: f Integer
    rhs = (f Integer -> Integer) -> f (f Integer) -> f Integer
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap f Integer -> Integer
    f (f (f Integer) -> f Integer)
    -> (f Integer -> f (f Integer)) -> f Integer -> f Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f Integer -> f (f Integer)
    forall a. f a -> f (f a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate (f Integer -> f Integer) -> f Integer -> f Integer
    forall a b. (a -> b) -> a -> b
    $ f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Extend/Fmap Duplicate", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "extend f" String -> String -> String
    `congruency` String
    "fmap f . duplicate"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "extend f x" String -> String -> String
    `congruency` String
    "fmap f . duplicate $ x, where"
                , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquationW f -> String
    forall a. Show a => a -> String
    show LinearEquationW f
    f'
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx f Integer
    lhs f Integer
    rhs Context
    ctx

    duplicateExtendId :: forall f. ComonadProp f
    duplicateExtendId :: forall (f :: * -> *). ComonadProp f
    duplicateExtendId forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs :: f (f Integer)
    lhs = f Integer -> f (f Integer)
    forall a. f a -> f (f a)
    forall (w :: * -> *) a. Comonad w => w a -> w (w a)
    duplicate f Integer
    x
      let rhs :: f (f Integer)
    rhs = (f Integer -> f Integer) -> f Integer -> f (f Integer)
    forall a b. (f a -> b) -> f a -> f b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend f Integer -> f Integer
    forall a. a -> a
    id f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Duplicate/Extend Id", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "duplicate" String -> String -> String
    `congruency` String
    "extend id"
            , lawContextReduced :: String
    lawContextReduced = f (f Integer) -> f (f Integer) -> String
    forall a. Show a => a -> a -> String
    reduced f (f Integer)
    lhs f (f Integer)
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "duplicate x" String -> String -> String
    `congruency` String
    "extend id x, where"
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      f (f Integer) -> f (f Integer) -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx f (f Integer)
    lhs f (f Integer)
    rhs Context
    ctx

    fmapExtendExtract :: forall f. ComonadProp f
    fmapExtendExtract :: forall (f :: * -> *). ComonadProp f
    fmapExtendExtract forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x :: f Integer <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      LinearEquation
    f' <- Gen LinearEquation -> PropertyT IO LinearEquation
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen LinearEquation
    genLinearEquation
      let f :: Integer -> Integer
    f = LinearEquation -> Integer -> Integer
    runLinearEquation LinearEquation
    f'
      let lhs :: f Integer
    lhs = (Integer -> Integer) -> f Integer -> f Integer
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Integer -> Integer
    f f Integer
    x
      let rhs :: f Integer
    rhs = (f Integer -> Integer) -> f Integer -> f Integer
    forall a b. (f a -> b) -> f a -> f b
    forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
    extend (Integer -> Integer
    f (Integer -> Integer)
    -> (f Integer -> Integer) -> f Integer -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f Integer -> Integer
    forall a. f a -> a
    forall (w :: * -> *) a. Comonad w => w a -> a
    extract) f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Fmap/Extend Extract", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "fmap f" String -> String -> String
    `congruency` String
    "extend (f . extract)"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "fmap f x" String -> String -> String
    `congruency` String
    "extend (f . extract) x, where"
                , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquation -> String
    forall a. Show a => a -> String
    show LinearEquation
    f'
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx f Integer
    lhs f Integer
    rhs Context
    ctx

    fmapLiftW :: forall f. ComonadProp f
    fmapLiftW :: forall (f :: * -> *). ComonadProp f
    fmapLiftW forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      f Integer
    x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      LinearEquation
    f' <- Gen LinearEquation -> PropertyT IO LinearEquation
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen LinearEquation
    genLinearEquation
      let f :: Integer -> Integer
    f = LinearEquation -> Integer -> Integer
    runLinearEquation LinearEquation
    f'
      let lhs :: f Integer
    lhs = (Integer -> Integer) -> f Integer -> f Integer
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Integer -> Integer
    f f Integer
    x
      let rhs :: f Integer
    rhs = (Integer -> Integer) -> f Integer -> f Integer
    forall (w :: * -> *) a b. Comonad w => (a -> b) -> w a -> w b
    liftW Integer -> Integer
    f f Integer
    x
      let ctx :: Context
    ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Fmap/LiftW", lawContextTcName :: String
    lawContextTcName = String
    "Comonad"
            , lawContextLawBody :: String
    lawContextLawBody = String
    "fmap" String -> String -> String
    `congruency` String
    "liftW"
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp = [String] -> String
    lawWhere
                [ String
    "fmap f x" String -> String -> String
    `congruency` String
    "liftW f x, where"
                , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ LinearEquation -> String
    forall a. Show a => a -> String
    show LinearEquation
    f'
                , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x
                ]
            }
      f Integer -> f Integer -> Context -> PropertyT IO ()
    forall (m :: * -> *) a.
    (MonadTest m, HasCallStack, Eq a, Show a) =>
    a -> a -> Context -> m ()
    heqCtx f Integer
    lhs f Integer
    rhs Context
    ctx

    #endif