{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
module Data.Profunctor.Cocartesian.Free(
    -- * The free 'Cocartesian' profunctors
    FreeCocartesian(..),
    liftF, foldFree,
    emptyF, sumF, sumDayF,

    -- * Newtype wrapper
    ForgetCocartesian(..),
) where

import Data.Void (Void, absurd)
import Data.Profunctor (Profunctor(..), (:->))
import Data.Profunctor.Cartesian
import Data.Profunctor.Monad
import Data.Profunctor.Day

-- * Free Cocartesian

-- | @FreeCocartesian p@ is a 'Cartesian' profunctor freely generated from
--   a mere @Profunctor p@.
data FreeCocartesian p a b =
    Neutral (a -> Void)
  | Cons (Day Either p (FreeCocartesian p) a b)
  deriving (forall a b.
 (a -> b) -> FreeCocartesian p a a -> FreeCocartesian p a b)
-> (forall a b.
    a -> FreeCocartesian p a b -> FreeCocartesian p a a)
-> Functor (FreeCocartesian p a)
forall a b. a -> FreeCocartesian p a b -> FreeCocartesian p a a
forall a b.
(a -> b) -> FreeCocartesian p a a -> FreeCocartesian p a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (p :: * -> * -> *) a a b.
a -> FreeCocartesian p a b -> FreeCocartesian p a a
forall (p :: * -> * -> *) a a b.
(a -> b) -> FreeCocartesian p a a -> FreeCocartesian p a b
$cfmap :: forall (p :: * -> * -> *) a a b.
(a -> b) -> FreeCocartesian p a a -> FreeCocartesian p a b
fmap :: forall a b.
(a -> b) -> FreeCocartesian p a a -> FreeCocartesian p a b
$c<$ :: forall (p :: * -> * -> *) a a b.
a -> FreeCocartesian p a b -> FreeCocartesian p a a
<$ :: forall a b. a -> FreeCocartesian p a b -> FreeCocartesian p a a
Functor

instance Profunctor (FreeCocartesian p) where
    dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> FreeCocartesian p b c -> FreeCocartesian p a d
dimap a -> b
f c -> d
g FreeCocartesian p b c
fp = case FreeCocartesian p b c
fp of
        Neutral b -> Void
a -> (a -> Void) -> FreeCocartesian p a d
forall (p :: * -> * -> *) a b. (a -> Void) -> FreeCocartesian p a b
Neutral (b -> Void
a (b -> Void) -> (a -> b) -> a -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)
        Cons Day Either p (FreeCocartesian p) b c
ps' -> Day Either p (FreeCocartesian p) a d -> FreeCocartesian p a d
forall (p :: * -> * -> *) a b.
Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
Cons ((a -> b)
-> (c -> d)
-> Day Either p (FreeCocartesian p) b c
-> Day Either p (FreeCocartesian p) a d
forall a b c d.
(a -> b)
-> (c -> d)
-> Day Either p (FreeCocartesian p) b c
-> Day Either p (FreeCocartesian p) a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> b
f c -> d
g Day Either p (FreeCocartesian p) b c
ps')

instance ProfunctorFunctor FreeCocartesian where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeCocartesian p :-> FreeCocartesian q
promap p :-> q
pq FreeCocartesian p a b
ps = case FreeCocartesian p a b
ps of
    Neutral a -> Void
a -> (a -> Void) -> FreeCocartesian q a b
forall (p :: * -> * -> *) a b. (a -> Void) -> FreeCocartesian p a b
Neutral a -> Void
a
    Cons (Day p a1 b1
p FreeCocartesian p a2 b2
ps' a -> Either a1 a2
opA Either b1 b2 -> b
opB) -> Day Either q (FreeCocartesian q) a b -> FreeCocartesian q a b
forall (p :: * -> * -> *) a b.
Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
Cons (Day Either q (FreeCocartesian q) a b -> FreeCocartesian q a b)
-> Day Either q (FreeCocartesian q) a b -> FreeCocartesian q a b
forall a b. (a -> b) -> a -> b
$ q a1 b1
-> FreeCocartesian q a2 b2
-> (a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> Day Either q (FreeCocartesian q) a b
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day (p a1 b1 -> q a1 b1
p :-> q
pq p a1 b1
p) ((p :-> q) -> FreeCocartesian p :-> FreeCocartesian q
forall {k} {k1} (t :: (* -> * -> *) -> k -> k1 -> *)
       (p :: * -> * -> *) (q :: * -> * -> *).
(ProfunctorFunctor t, Profunctor p) =>
(p :-> q) -> t p :-> t q
forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeCocartesian p :-> FreeCocartesian q
promap p a b -> q a b
p :-> q
pq FreeCocartesian p a2 b2
ps') a -> Either a1 a2
opA Either b1 b2 -> b
opB

emptyF :: FreeCocartesian p Void b
emptyF :: forall (p :: * -> * -> *) b. FreeCocartesian p Void b
emptyF = (Void -> Void) -> FreeCocartesian p Void b
forall (p :: * -> * -> *) a b. (a -> Void) -> FreeCocartesian p a b
Neutral Void -> Void
forall a. a -> a
id

sumDayF :: Day Either (FreeCocartesian p) (FreeCocartesian p) :-> FreeCocartesian p
sumDayF :: forall (p :: * -> * -> *) a b.
Day Either (FreeCocartesian p) (FreeCocartesian p) a b
-> FreeCocartesian p a b
sumDayF (Day (Neutral a1 -> Void
z) FreeCocartesian p a2 b2
qs a -> Either a1 a2
opA Either b1 b2 -> b
opB) = (a -> a2)
-> (b2 -> b) -> FreeCocartesian p a2 b2 -> FreeCocartesian p a b
forall a b c d.
(a -> b)
-> (c -> d) -> FreeCocartesian p b c -> FreeCocartesian p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((a1 -> a2) -> (a2 -> a2) -> Either a1 a2 -> a2
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Void -> a2
forall a. Void -> a
absurd (Void -> a2) -> (a1 -> Void) -> a1 -> a2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a1 -> Void
z) a2 -> a2
forall a. a -> a
id (Either a1 a2 -> a2) -> (a -> Either a1 a2) -> a -> a2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either a1 a2
opA) (Either b1 b2 -> b
opB (Either b1 b2 -> b) -> (b2 -> Either b1 b2) -> b2 -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b2 -> Either b1 b2
forall a b. b -> Either a b
Right) FreeCocartesian p a2 b2
qs
sumDayF (Day (Cons Day Either p (FreeCocartesian p) a1 b1
ps) FreeCocartesian p a2 b2
qs a -> Either a1 a2
opA Either b1 b2 -> b
opB) = Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
forall (p :: * -> * -> *) a b.
Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
Cons (Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b)
-> Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
forall a b. (a -> b) -> a -> b
$ (Day Either (FreeCocartesian p) (FreeCocartesian p)
 :-> FreeCocartesian p)
-> Day
     Either p (Day Either (FreeCocartesian p) (FreeCocartesian p))
   :-> Day Either p (FreeCocartesian p)
forall (q :: * -> * -> *) (q' :: * -> * -> *) (t :: * -> * -> *)
       (p :: * -> * -> *).
(q :-> q') -> Day t p q :-> Day t p q'
promap2 Day Either (FreeCocartesian p) (FreeCocartesian p) a b
-> FreeCocartesian p a b
Day Either (FreeCocartesian p) (FreeCocartesian p)
:-> FreeCocartesian p
forall (p :: * -> * -> *) a b.
Day Either (FreeCocartesian p) (FreeCocartesian p) a b
-> FreeCocartesian p a b
sumDayF (Day
   Either p (Day Either (FreeCocartesian p) (FreeCocartesian p)) a b
 -> Day Either p (FreeCocartesian p) a b)
-> Day
     Either p (Day Either (FreeCocartesian p) (FreeCocartesian p)) a b
-> Day Either p (FreeCocartesian p) a b
forall a b. (a -> b) -> a -> b
$ Day
  Either (Day Either p (FreeCocartesian p)) (FreeCocartesian p) a b
-> Day
     Either p (Day Either (FreeCocartesian p) (FreeCocartesian p)) a b
Day Either (Day Either p (FreeCocartesian p)) (FreeCocartesian p)
:-> Day
      Either p (Day Either (FreeCocartesian p) (FreeCocartesian p))
forall (t :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *)
       (r :: * -> * -> *).
Assoc t =>
Day t (Day t p q) r :-> Day t p (Day t q r)
assocDay (Day Either p (FreeCocartesian p) a1 b1
-> FreeCocartesian p a2 b2
-> (a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> Day
     Either (Day Either p (FreeCocartesian p)) (FreeCocartesian p) a b
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day Day Either p (FreeCocartesian p) a1 b1
ps FreeCocartesian p a2 b2
qs a -> Either a1 a2
opA Either b1 b2 -> b
opB)

sumF :: FreeCocartesian p a b -> FreeCocartesian p a' b' -> FreeCocartesian p (Either a a') (Either b b')
sumF :: forall (p :: * -> * -> *) a b a' b'.
FreeCocartesian p a b
-> FreeCocartesian p a' b'
-> FreeCocartesian p (Either a a') (Either b b')
sumF FreeCocartesian p a b
ps FreeCocartesian p a' b'
qs = Day
  Either
  (FreeCocartesian p)
  (FreeCocartesian p)
  (Either a a')
  (Either b b')
-> FreeCocartesian p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b.
Day Either (FreeCocartesian p) (FreeCocartesian p) a b
-> FreeCocartesian p a b
sumDayF (FreeCocartesian p a b
-> FreeCocartesian p a' b'
-> (Either a a' -> Either a a')
-> (Either b b' -> Either b b')
-> Day
     Either
     (FreeCocartesian p)
     (FreeCocartesian p)
     (Either a a')
     (Either b b')
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day FreeCocartesian p a b
ps FreeCocartesian p a' b'
qs Either a a' -> Either a a'
forall a. a -> a
id Either b b' -> Either b b'
forall a. a -> a
id)

instance Profunctor p => Cocartesian (FreeCocartesian p) where
    proEmpty :: forall b. FreeCocartesian p Void b
proEmpty = FreeCocartesian p Void b
forall (p :: * -> * -> *) b. FreeCocartesian p Void b
emptyF
    proSum :: forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> FreeCocartesian p a1 b1
-> FreeCocartesian p a2 b2
-> FreeCocartesian p a b
proSum a -> Either a1 a2
opA Either b1 b2 -> b
opB FreeCocartesian p a1 b1
ps FreeCocartesian p a2 b2
qs = Day Either (FreeCocartesian p) (FreeCocartesian p) a b
-> FreeCocartesian p a b
forall (p :: * -> * -> *) a b.
Day Either (FreeCocartesian p) (FreeCocartesian p) a b
-> FreeCocartesian p a b
sumDayF (FreeCocartesian p a1 b1
-> FreeCocartesian p a2 b2
-> (a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> Day Either (FreeCocartesian p) (FreeCocartesian p) a b
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day FreeCocartesian p a1 b1
ps FreeCocartesian p a2 b2
qs a -> Either a1 a2
opA Either b1 b2 -> b
opB)

-- * ProfunctorMonad structures

liftF :: p :-> FreeCocartesian p
liftF :: forall (p :: * -> * -> *) a b. p a b -> FreeCocartesian p a b
liftF p a b
p = Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
forall (p :: * -> * -> *) a b.
Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
Cons (Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b)
-> Day Either p (FreeCocartesian p) a b -> FreeCocartesian p a b
forall a b. (a -> b) -> a -> b
$ p a b
-> FreeCocartesian p Void Void
-> (a -> Either a Void)
-> (Either b Void -> b)
-> Day Either p (FreeCocartesian p) a b
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day p a b
p FreeCocartesian p Void Void
forall (p :: * -> * -> *) b. FreeCocartesian p Void b
emptyF a -> Either a Void
forall a b. a -> Either a b
Left ((b -> b) -> (Void -> b) -> Either b Void -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
id Void -> b
forall a. Void -> a
absurd)

foldFree :: (Cocartesian q) => (p :-> q) -> FreeCocartesian p :-> q
foldFree :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFree p :-> q
handle FreeCocartesian p a b
ps = case FreeCocartesian p a b
ps of
    Neutral a -> Void
z -> (a -> Void) -> q Void b -> q a b
forall a b c. (a -> b) -> q b c -> q a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> Void
z q Void b
forall b. q Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
    Cons (Day p a1 b1
p FreeCocartesian p a2 b2
ps' a -> Either a1 a2
opA Either b1 b2 -> b
opB) -> (a -> Either a1 a2)
-> (Either b1 b2 -> b) -> q (Either a1 a2) (Either b1 b2) -> q a b
forall a b c d. (a -> b) -> (c -> d) -> q b c -> q a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> Either a1 a2
opA Either b1 b2 -> b
opB (p a1 b1 -> q a1 b1
p :-> q
handle p a1 b1
p q a1 b1 -> q a2 b2 -> q (Either a1 a2) (Either b1 b2)
forall a b a' b'. q a b -> q a' b' -> q (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ (p :-> q) -> FreeCocartesian p :-> q
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFree p a b -> q a b
p :-> q
handle FreeCocartesian p a2 b2
ps')

instance ProfunctorMonad FreeCocartesian where
    proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> FreeCocartesian p
proreturn = p a b -> FreeCocartesian p a b
forall (p :: * -> * -> *) a b. p a b -> FreeCocartesian p a b
liftF
    projoin :: forall (p :: * -> * -> *).
Profunctor p =>
FreeCocartesian (FreeCocartesian p) :-> FreeCocartesian p
projoin = (FreeCocartesian p :-> FreeCocartesian p)
-> FreeCocartesian (FreeCocartesian p) :-> FreeCocartesian p
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFree FreeCocartesian p a b -> FreeCocartesian p a b
forall a. a -> a
FreeCocartesian p :-> FreeCocartesian p
id

-- * Utility newtype wrappers

-- | Forgets 'Cocartesian' instance from a 'Profunctor'.
newtype ForgetCocartesian p a b = ForgetCocartesian { forall (p :: * -> * -> *) a b. ForgetCocartesian p a b -> p a b
recallCocartesian :: p a b }
  deriving newtype ((forall a b.
 (a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian p a b)
-> (forall a b.
    a -> ForgetCocartesian p a b -> ForgetCocartesian p a a)
-> Functor (ForgetCocartesian p a)
forall a b. a -> ForgetCocartesian p a b -> ForgetCocartesian p a a
forall a b.
(a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian p a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (p :: * -> * -> *) a a b.
Functor (p a) =>
a -> ForgetCocartesian p a b -> ForgetCocartesian p a a
forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian p a b
$cfmap :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian p a b
fmap :: forall a b.
(a -> b) -> ForgetCocartesian p a a -> ForgetCocartesian p a b
$c<$ :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
a -> ForgetCocartesian p a b -> ForgetCocartesian p a a
<$ :: forall a b. a -> ForgetCocartesian p a b -> ForgetCocartesian p a a
Functor, (forall a b c d.
 (a -> b)
 -> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d)
-> (forall a b c.
    (a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c)
-> (forall b c a.
    (b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible c b =>
    q b c -> ForgetCocartesian p a b -> ForgetCocartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible b a =>
    ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c)
-> Profunctor (ForgetCocartesian p)
forall a b c.
(a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c
forall b c a.
(b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c
forall a b c d.
(a -> b)
-> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d
forall a b c (q :: * -> * -> *).
Coercible b a =>
ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> ForgetCocartesian p a b -> ForgetCocartesian p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b)
-> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> ForgetCocartesian p a b -> ForgetCocartesian p a c
forall (p :: * -> * -> *).
(forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d)
-> (forall a b c. (a -> b) -> p b c -> p a c)
-> (forall b c a. (b -> c) -> p a b -> p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible c b =>
    q b c -> p a b -> p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible b a =>
    p b c -> q a b -> p a c)
-> Profunctor p
$cdimap :: forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b)
-> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d
dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> ForgetCocartesian p b c -> ForgetCocartesian p a d
$clmap :: forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c
lmap :: forall a b c.
(a -> b) -> ForgetCocartesian p b c -> ForgetCocartesian p a c
$crmap :: forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c
rmap :: forall b c a.
(b -> c) -> ForgetCocartesian p a b -> ForgetCocartesian p a c
$c#. :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> ForgetCocartesian p a b -> ForgetCocartesian p a c
#. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> ForgetCocartesian p a b -> ForgetCocartesian p a c
$c.# :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c
.# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
ForgetCocartesian p b c -> q a b -> ForgetCocartesian p a c
Profunctor, Profunctor (ForgetCocartesian p)
Profunctor (ForgetCocartesian p) =>
(forall a. ForgetCocartesian p a ())
-> (forall a a1 a2 b1 b2 b.
    (a -> (a1, a2))
    -> ((b1, b2) -> b)
    -> ForgetCocartesian p a1 b1
    -> ForgetCocartesian p a2 b2
    -> ForgetCocartesian p a b)
-> (forall a b a' b'.
    ForgetCocartesian p a b
    -> ForgetCocartesian p a' b'
    -> ForgetCocartesian p (a, a') (b, b'))
-> (forall a b b'.
    ForgetCocartesian p a b
    -> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b'))
-> (forall (n :: Nat) a b.
    KnownNat n =>
    ForgetCocartesian p a b
    -> ForgetCocartesian p (Finite n -> a) (Finite n -> b))
-> Cartesian (ForgetCocartesian p)
forall (n :: Nat) a b.
KnownNat n =>
ForgetCocartesian p a b
-> ForgetCocartesian p (Finite n -> a) (Finite n -> b)
forall a. ForgetCocartesian p a ()
forall a b b'.
ForgetCocartesian p a b
-> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b')
forall a b a' b'.
ForgetCocartesian p a b
-> ForgetCocartesian p a' b' -> ForgetCocartesian p (a, a') (b, b')
forall a a1 a2 b1 b2 b.
(a -> (a1, a2))
-> ((b1, b2) -> b)
-> ForgetCocartesian p a1 b1
-> ForgetCocartesian p a2 b2
-> ForgetCocartesian p a b
forall (p :: * -> * -> *).
Profunctor p =>
(forall a. p a ())
-> (forall a a1 a2 b1 b2 b.
    (a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b)
-> (forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b'))
-> (forall a b b'. p a b -> p a b' -> p a (b, b'))
-> (forall (n :: Nat) a b.
    KnownNat n =>
    p a b -> p (Finite n -> a) (Finite n -> b))
-> Cartesian p
forall (p :: * -> * -> *).
Cartesian p =>
Profunctor (ForgetCocartesian p)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
ForgetCocartesian p a b
-> ForgetCocartesian p (Finite n -> a) (Finite n -> b)
forall (p :: * -> * -> *) a.
Cartesian p =>
ForgetCocartesian p a ()
forall (p :: * -> * -> *) a b b'.
Cartesian p =>
ForgetCocartesian p a b
-> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
ForgetCocartesian p a b
-> ForgetCocartesian p a' b' -> ForgetCocartesian p (a, a') (b, b')
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2))
-> ((b1, b2) -> b)
-> ForgetCocartesian p a1 b1
-> ForgetCocartesian p a2 b2
-> ForgetCocartesian p a b
$cproUnit :: forall (p :: * -> * -> *) a.
Cartesian p =>
ForgetCocartesian p a ()
proUnit :: forall a. ForgetCocartesian p a ()
$cproProduct :: forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2))
-> ((b1, b2) -> b)
-> ForgetCocartesian p a1 b1
-> ForgetCocartesian p a2 b2
-> ForgetCocartesian p a b
proProduct :: forall a a1 a2 b1 b2 b.
(a -> (a1, a2))
-> ((b1, b2) -> b)
-> ForgetCocartesian p a1 b1
-> ForgetCocartesian p a2 b2
-> ForgetCocartesian p a b
$c*** :: forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
ForgetCocartesian p a b
-> ForgetCocartesian p a' b' -> ForgetCocartesian p (a, a') (b, b')
*** :: forall a b a' b'.
ForgetCocartesian p a b
-> ForgetCocartesian p a' b' -> ForgetCocartesian p (a, a') (b, b')
$c&&& :: forall (p :: * -> * -> *) a b b'.
Cartesian p =>
ForgetCocartesian p a b
-> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b')
&&& :: forall a b b'.
ForgetCocartesian p a b
-> ForgetCocartesian p a b' -> ForgetCocartesian p a (b, b')
$cproPower :: forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
ForgetCocartesian p a b
-> ForgetCocartesian p (Finite n -> a) (Finite n -> b)
proPower :: forall (n :: Nat) a b.
KnownNat n =>
ForgetCocartesian p a b
-> ForgetCocartesian p (Finite n -> a) (Finite n -> b)
Cartesian)
  -- DO NOT add "deriving Cocartesian" clause!