{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Data.Profunctor.Cartesian.Free(
    -- * The free 'Cartesian' profunctor
    FreeCartesian(..),
    liftF,
    foldFree,

    -- * Newtype wrapper
    ForgetCartesian(..),

    -- * Utility functions
    assocTup, unassocTup,
) where

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

-- * The free 'Cartesian' profunctor

-- | The free 'Cartesian' profunctor.
data FreeCartesian p a b =
    Neutral b
  | Cons (Day (,) p (FreeCartesian p) a b)
  deriving (forall a b.
 (a -> b) -> FreeCartesian p a a -> FreeCartesian p a b)
-> (forall a b. a -> FreeCartesian p a b -> FreeCartesian p a a)
-> Functor (FreeCartesian p a)
forall a b. a -> FreeCartesian p a b -> FreeCartesian p a a
forall a b. (a -> b) -> FreeCartesian p a a -> FreeCartesian 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 -> FreeCartesian p a b -> FreeCartesian p a a
forall (p :: * -> * -> *) a a b.
(a -> b) -> FreeCartesian p a a -> FreeCartesian p a b
$cfmap :: forall (p :: * -> * -> *) a a b.
(a -> b) -> FreeCartesian p a a -> FreeCartesian p a b
fmap :: forall a b. (a -> b) -> FreeCartesian p a a -> FreeCartesian p a b
$c<$ :: forall (p :: * -> * -> *) a a b.
a -> FreeCartesian p a b -> FreeCartesian p a a
<$ :: forall a b. a -> FreeCartesian p a b -> FreeCartesian p a a
Functor

instance Applicative (FreeCartesian p a) where
  pure :: forall a. a -> FreeCartesian p a a
pure = a -> FreeCartesian p a a
forall (p :: * -> * -> *) b a. Cartesian p => b -> p a b
pureDefault
  liftA2 :: forall a b c.
(a -> b -> c)
-> FreeCartesian p a a
-> FreeCartesian p a b
-> FreeCartesian p a c
liftA2 = (a -> b -> c)
-> FreeCartesian p a a
-> FreeCartesian p a b
-> FreeCartesian p a c
forall (p :: * -> * -> *) a b c x.
Cartesian p =>
(a -> b -> c) -> p x a -> p x b -> p x c
liftA2Default

instance Profunctor (FreeCartesian p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> FreeCartesian p b c -> FreeCartesian p a d
dimap a -> b
_ c -> d
g (Neutral c
b) = d -> FreeCartesian p a d
forall (p :: * -> * -> *) a a. a -> FreeCartesian p a a
Neutral (c -> d
g c
b)
  dimap a -> b
f c -> d
g (Cons Day (,) p (FreeCartesian p) b c
ps')  = Day (,) p (FreeCartesian p) a d -> FreeCartesian p a d
forall (p :: * -> * -> *) a b.
Day (,) p (FreeCartesian p) a b -> FreeCartesian p a b
Cons ((a -> b)
-> (c -> d)
-> Day (,) p (FreeCartesian p) b c
-> Day (,) p (FreeCartesian p) a d
forall a b c d.
(a -> b)
-> (c -> d)
-> Day (,) p (FreeCartesian p) b c
-> Day (,) p (FreeCartesian 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 (,) p (FreeCartesian p) b c
ps')

instance Cartesian (FreeCartesian p) where
    proUnit :: forall a. FreeCartesian p a ()
proUnit = () -> FreeCartesian p a ()
forall (p :: * -> * -> *) a a. a -> FreeCartesian p a a
Neutral ()
    Neutral b
b *** :: forall a b a' b'.
FreeCartesian p a b
-> FreeCartesian p a' b' -> FreeCartesian p (a, a') (b, b')
*** FreeCartesian p a' b'
qs = ((a, a') -> a')
-> (b' -> (b, b'))
-> FreeCartesian p a' b'
-> FreeCartesian p (a, a') (b, b')
forall a b c d.
(a -> b) -> (c -> d) -> FreeCartesian p b c -> FreeCartesian p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (a, a') -> a'
forall a b. (a, b) -> b
snd (b
b,) FreeCartesian p a' b'
qs
    Cons (Day p a1 b1
p FreeCartesian p a2 b2
ps a -> (a1, a2)
opA (b1, b2) -> b
opB) *** FreeCartesian p a' b'
qs = Day (,) p (FreeCartesian p) (a, a') (b, b')
-> FreeCartesian p (a, a') (b, b')
forall (p :: * -> * -> *) a b.
Day (,) p (FreeCartesian p) a b -> FreeCartesian p a b
Cons (Day (,) p (FreeCartesian p) (a, a') (b, b')
 -> FreeCartesian p (a, a') (b, b'))
-> Day (,) p (FreeCartesian p) (a, a') (b, b')
-> FreeCartesian p (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ p a1 b1
-> FreeCartesian p (a2, a') (b2, b')
-> ((a, a') -> (a1, (a2, a')))
-> ((b1, (b2, b')) -> (b, b'))
-> Day (,) p (FreeCartesian p) (a, a') (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 p a1 b1
p (FreeCartesian p a2 b2
ps FreeCartesian p a2 b2
-> FreeCartesian p a' b' -> FreeCartesian p (a2, a') (b2, b')
forall a b a' b'.
FreeCartesian p a b
-> FreeCartesian p a' b' -> FreeCartesian p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** FreeCartesian p a' b'
qs) (((a1, a2), a') -> (a1, (a2, a'))
forall a b c. ((a, b), c) -> (a, (b, c))
assocTup (((a1, a2), a') -> (a1, (a2, a')))
-> ((a, a') -> ((a1, a2), a')) -> (a, a') -> (a1, (a2, a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> (a1, a2)) -> (a, a') -> ((a1, a2), a')
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> (a1, a2)
opA) (((b1, b2) -> b) -> ((b1, b2), b') -> (b, b')
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (b1, b2) -> b
opB (((b1, b2), b') -> (b, b'))
-> ((b1, (b2, b')) -> ((b1, b2), b')) -> (b1, (b2, b')) -> (b, b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b1, (b2, b')) -> ((b1, b2), b')
forall a b c. (a, (b, c)) -> ((a, b), c)
unassocTup)

assocTup :: ((a,b), c) -> (a, (b,c))
assocTup :: forall a b c. ((a, b), c) -> (a, (b, c))
assocTup ((a
a,b
b), c
c) = (a
a, (b
b,c
c))

unassocTup :: (a, (b,c)) ->  ((a,b), c)
unassocTup :: forall a b c. (a, (b, c)) -> ((a, b), c)
unassocTup (a
a, (b
b,c
c)) = ((a
a,b
b), c
c)

liftF :: p :-> FreeCartesian p
liftF :: forall (p :: * -> * -> *) a b. p a b -> FreeCartesian p a b
liftF p a b
p = Day (,) p (FreeCartesian p) a b -> FreeCartesian p a b
forall (p :: * -> * -> *) a b.
Day (,) p (FreeCartesian p) a b -> FreeCartesian p a b
Cons (Day (,) p (FreeCartesian p) a b -> FreeCartesian p a b)
-> Day (,) p (FreeCartesian p) a b -> FreeCartesian p a b
forall a b. (a -> b) -> a -> b
$ p a b
-> FreeCartesian p () ()
-> (a -> (a, ()))
-> ((b, ()) -> b)
-> Day (,) p (FreeCartesian 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 FreeCartesian p () ()
forall a. FreeCartesian p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit (, ()) (b, ()) -> b
forall a b. (a, b) -> a
fst

foldFree :: Cartesian q => (p :-> q) -> FreeCartesian p :-> q
foldFree :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Cartesian q =>
(p :-> q) -> FreeCartesian p :-> q
foldFree p :-> q
_ (Neutral b
b) = (() -> b) -> q a () -> q a b
forall b c a. (b -> c) -> q a b -> q a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap (b -> () -> b
forall a b. a -> b -> a
const b
b) q a ()
forall a. q a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
foldFree p :-> q
handle (Cons Day (,) p (FreeCartesian p) a b
ps) = (p :-> q)
-> (FreeCartesian p :-> q) -> Day (,) p (FreeCartesian p) :-> q
forall (r :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *).
Cartesian r =>
(p :-> r) -> (q :-> r) -> Day (,) p q :-> r
prodDay p a b -> q a b
p :-> q
handle ((p :-> q) -> FreeCartesian p :-> q
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cartesian q =>
(p :-> q) -> FreeCartesian p :-> q
foldFree p a b -> q a b
p :-> q
handle) Day (,) p (FreeCartesian p) a b
ps

instance ProfunctorFunctor FreeCartesian where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> FreeCartesian p :-> FreeCartesian q
promap p :-> q
pq FreeCartesian p a b
ps = case FreeCartesian p a b
ps of
    Neutral b
b -> b -> FreeCartesian q a b
forall (p :: * -> * -> *) a a. a -> FreeCartesian p a a
Neutral b
b
    Cons (Day p a1 b1
p FreeCartesian p a2 b2
ps' a -> (a1, a2)
opA (b1, b2) -> b
opB) -> Day (,) q (FreeCartesian q) a b -> FreeCartesian q a b
forall (p :: * -> * -> *) a b.
Day (,) p (FreeCartesian p) a b -> FreeCartesian p a b
Cons (q a1 b1
-> FreeCartesian q a2 b2
-> (a -> (a1, a2))
-> ((b1, b2) -> b)
-> Day (,) q (FreeCartesian 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) -> FreeCartesian p :-> FreeCartesian 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) -> FreeCartesian p :-> FreeCartesian q
promap p a b -> q a b
p :-> q
pq FreeCartesian p a2 b2
ps') a -> (a1, a2)
opA (b1, b2) -> b
opB)

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

-- | Forgets 'Cartesian' instance from a 'Profunctor'.
newtype ForgetCartesian p a b = ForgetCartesian { forall (p :: * -> * -> *) a b. ForgetCartesian p a b -> p a b
recallCartesian :: p a b }
  deriving newtype ((forall a b.
 (a -> b) -> ForgetCartesian p a a -> ForgetCartesian p a b)
-> (forall a b.
    a -> ForgetCartesian p a b -> ForgetCartesian p a a)
-> Functor (ForgetCartesian p a)
forall a b. a -> ForgetCartesian p a b -> ForgetCartesian p a a
forall a b.
(a -> b) -> ForgetCartesian p a a -> ForgetCartesian 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 -> ForgetCartesian p a b -> ForgetCartesian p a a
forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> ForgetCartesian p a a -> ForgetCartesian p a b
$cfmap :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
(a -> b) -> ForgetCartesian p a a -> ForgetCartesian p a b
fmap :: forall a b.
(a -> b) -> ForgetCartesian p a a -> ForgetCartesian p a b
$c<$ :: forall (p :: * -> * -> *) a a b.
Functor (p a) =>
a -> ForgetCartesian p a b -> ForgetCartesian p a a
<$ :: forall a b. a -> ForgetCartesian p a b -> ForgetCartesian p a a
Functor, (forall a b c d.
 (a -> b)
 -> (c -> d) -> ForgetCartesian p b c -> ForgetCartesian p a d)
-> (forall a b c.
    (a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c)
-> (forall b c a.
    (b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible c b =>
    q b c -> ForgetCartesian p a b -> ForgetCartesian p a c)
-> (forall a b c (q :: * -> * -> *).
    Coercible b a =>
    ForgetCartesian p b c -> q a b -> ForgetCartesian p a c)
-> Profunctor (ForgetCartesian p)
forall a b c.
(a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c
forall b c a.
(b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c
forall a b c d.
(a -> b)
-> (c -> d) -> ForgetCartesian p b c -> ForgetCartesian p a d
forall a b c (q :: * -> * -> *).
Coercible b a =>
ForgetCartesian p b c -> q a b -> ForgetCartesian p a c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> ForgetCartesian p a b -> ForgetCartesian p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b)
-> (c -> d) -> ForgetCartesian p b c -> ForgetCartesian p a d
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
ForgetCartesian p b c -> q a b -> ForgetCartesian p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> ForgetCartesian p a b -> ForgetCartesian 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) -> ForgetCartesian p b c -> ForgetCartesian p a d
dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> ForgetCartesian p b c -> ForgetCartesian p a d
$clmap :: forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c
lmap :: forall a b c.
(a -> b) -> ForgetCartesian p b c -> ForgetCartesian p a c
$crmap :: forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c
rmap :: forall b c a.
(b -> c) -> ForgetCartesian p a b -> ForgetCartesian p a c
$c#. :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> ForgetCartesian p a b -> ForgetCartesian p a c
#. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> ForgetCartesian p a b -> ForgetCartesian p a c
$c.# :: forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
ForgetCartesian p b c -> q a b -> ForgetCartesian p a c
.# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
ForgetCartesian p b c -> q a b -> ForgetCartesian p a c
Profunctor, Profunctor (ForgetCartesian p)
Profunctor (ForgetCartesian p) =>
(forall b. ForgetCartesian p Void b)
-> (forall a a1 a2 b1 b2 b.
    (a -> Either a1 a2)
    -> (Either b1 b2 -> b)
    -> ForgetCartesian p a1 b1
    -> ForgetCartesian p a2 b2
    -> ForgetCartesian p a b)
-> (forall a b a' b'.
    ForgetCartesian p a b
    -> ForgetCartesian p a' b'
    -> ForgetCartesian p (Either a a') (Either b b'))
-> (forall a b a'.
    ForgetCartesian p a b
    -> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b)
-> (forall (n :: Nat) a b.
    KnownNat n =>
    ForgetCartesian p a b
    -> ForgetCartesian p (Finite n, a) (Finite n, b))
-> Cocartesian (ForgetCartesian p)
forall (n :: Nat) a b.
KnownNat n =>
ForgetCartesian p a b
-> ForgetCartesian p (Finite n, a) (Finite n, b)
forall b. ForgetCartesian p Void b
forall a b a'.
ForgetCartesian p a b
-> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b
forall a b a' b'.
ForgetCartesian p a b
-> ForgetCartesian p a' b'
-> ForgetCartesian p (Either a a') (Either b b')
forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> ForgetCartesian p a1 b1
-> ForgetCartesian p a2 b2
-> ForgetCartesian p a b
forall (p :: * -> * -> *).
Profunctor p =>
(forall b. p Void b)
-> (forall a a1 a2 b1 b2 b.
    (a -> Either a1 a2)
    -> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b)
-> (forall a b a' b'.
    p a b -> p a' b' -> p (Either a a') (Either b b'))
-> (forall a b a'. p a b -> p a' b -> p (Either a a') b)
-> (forall (n :: Nat) a b.
    KnownNat n =>
    p a b -> p (Finite n, a) (Finite n, b))
-> Cocartesian p
forall (p :: * -> * -> *).
Cocartesian p =>
Profunctor (ForgetCartesian p)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cocartesian p, KnownNat n) =>
ForgetCartesian p a b
-> ForgetCartesian p (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) b.
Cocartesian p =>
ForgetCartesian p Void b
forall (p :: * -> * -> *) a b a'.
Cocartesian p =>
ForgetCartesian p a b
-> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
ForgetCartesian p a b
-> ForgetCartesian p a' b'
-> ForgetCartesian p (Either a a') (Either b b')
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cocartesian p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> ForgetCartesian p a1 b1
-> ForgetCartesian p a2 b2
-> ForgetCartesian p a b
$cproEmpty :: forall (p :: * -> * -> *) b.
Cocartesian p =>
ForgetCartesian p Void b
proEmpty :: forall b. ForgetCartesian p Void b
$cproSum :: forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cocartesian p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> ForgetCartesian p a1 b1
-> ForgetCartesian p a2 b2
-> ForgetCartesian p a b
proSum :: forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b)
-> ForgetCartesian p a1 b1
-> ForgetCartesian p a2 b2
-> ForgetCartesian p a b
$c+++ :: forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
ForgetCartesian p a b
-> ForgetCartesian p a' b'
-> ForgetCartesian p (Either a a') (Either b b')
+++ :: forall a b a' b'.
ForgetCartesian p a b
-> ForgetCartesian p a' b'
-> ForgetCartesian p (Either a a') (Either b b')
$c||| :: forall (p :: * -> * -> *) a b a'.
Cocartesian p =>
ForgetCartesian p a b
-> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b
||| :: forall a b a'.
ForgetCartesian p a b
-> ForgetCartesian p a' b -> ForgetCartesian p (Either a a') b
$cproTimes :: forall (p :: * -> * -> *) (n :: Nat) a b.
(Cocartesian p, KnownNat n) =>
ForgetCartesian p a b
-> ForgetCartesian p (Finite n, a) (Finite n, b)
proTimes :: forall (n :: Nat) a b.
KnownNat n =>
ForgetCartesian p a b
-> ForgetCartesian p (Finite n, a) (Finite n, b)
Cocartesian)
  -- DO NOT add "deriving Cartesian" clause!