{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Helper.CCC (toCCC, lam, ($), lift, pattern (:&), left, right, either, FreeCCC, InitF, TermF, type (*), type (+), FK(..)) where

import Data.Kind (Constraint)
import Prelude (type (~))
import Prelude qualified as P

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Object (Obj, obj)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv, swapProd
  )
import Proarrow.Object.Exponential (BiCCC, CCC, Closed (..), curry, eval, lower, uncurry)
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))

class (CCC k) => Cast (x :: k) y where
  cast :: x ~> y

instance {-# OVERLAPPABLE #-} (CCC k, Cast b a, b && i ~ t, Ob b, Ob i) => Cast (t :: k) a where
  cast :: t ~> a
cast = b ~> a
forall k (x :: k) (y :: k). Cast x y => x ~> y
cast (b ~> a) -> (t ~> b) -> t ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @b @i

instance (CCC k, Ob a) => Cast (a :: k) a where
  cast :: a ~> a
cast = a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

lam
  :: forall {k} a b i
   . (CCC k, Ob i, Ob a, Ob b)
  => ((forall (x :: k). (Cast x (i && a)) => x ~> a) -> (i && a) ~> b)
  -> (i :: k) ~> (a ~~> b)
lam :: forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam (forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b
f = forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @i @a @b ((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b
f x ~> a
forall (x :: k). Cast x (i && a) => x ~> a
snd_)
  where
    snd_ :: forall x. (Cast x (i && a)) => x ~> a
    snd_ :: forall (x :: k). Cast x (i && a) => x ~> a
snd_ = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @i @a ((i && a) ~> a) -> (x ~> (i && a)) -> x ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (x :: k) (y :: k). Cast x y => x ~> y
cast @k @x @(i && a)

($) :: forall {k} i a b. (CCC k, Ob b) => (i :: k) ~> (a ~~> b) -> i ~> a -> i ~> b
$ :: forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob b) =>
(i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
($) i ~> (a ~~> b)
f i ~> a
a = forall (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval @a @b (((a ~~> b) ** a) ~> b) -> (i ~> ((a ~~> b) ** a)) -> i ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (i ~> (a ~~> b)
f (i ~> (a ~~> b)) -> (i ~> a) -> i ~> ((a ~~> b) && a)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& i ~> a
a) ((Ob i, Ob a) => i ~> b) -> (i ~> a) -> i ~> b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ i ~> a
a

lift :: forall {k} (i :: k) a b. (CCC k) => a ~> b -> i ~> a -> i ~> b
lift :: forall {k} (i :: k) (a :: k) (b :: k).
CCC k =>
(a ~> b) -> (i ~> a) -> i ~> b
lift = (a ~> b) -> (i ~> a) -> i ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
(.)

fstSnd :: forall {k} (i :: k) a b. (CCC k, Ob a, Ob b) => i ~> a && b -> (i ~> a, i ~> b)
fstSnd :: forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> (a && b)) -> (i ~> a, i ~> b)
fstSnd i ~> (a && b)
f = (((a && b) ~> a) -> (i ~> (a && b)) -> i ~> a
forall {k} (i :: k) (a :: k) (b :: k).
CCC k =>
(a ~> b) -> (i ~> a) -> i ~> b
lift (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @b) i ~> (a && b)
f, ((a && b) ~> b) -> (i ~> (a && b)) -> i ~> b
forall {k} (i :: k) (a :: k) (b :: k).
CCC k =>
(a ~> b) -> (i ~> a) -> i ~> b
lift (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b) i ~> (a && b)
f)

pattern (:&) :: forall {k} i a b. (CCC k, Ob (a :: k), Ob b) => (i ~> a) -> (i ~> b) -> i ~> a && b
pattern x $m:& :: forall {r} {k} {i :: k} {a :: k} {b :: k}.
(CCC k, Ob a, Ob b) =>
(i ~> (a && b)) -> ((i ~> a) -> (i ~> b) -> r) -> ((# #) -> r) -> r
$b:& :: forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& y <- (fstSnd @i @a @b -> (x, y))
  where
    i ~> a
x :& i ~> b
y = i ~> a
x (i ~> a) -> (i ~> b) -> i ~> (a && b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& i ~> b
y

{-# COMPLETE (:&) #-}

left :: forall {k} a b i. (HasBinaryCoproducts k, Ob (a :: k), Ob b) => (i ~> a) -> i ~> a || b
left :: forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> a) -> i ~> (a || b)
left i ~> a
x = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b (a ~> (a || b)) -> (i ~> a) -> i ~> (a || b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. i ~> a
x

right :: forall {k} a b i. (HasBinaryCoproducts k, Ob (a :: k), Ob b) => (i ~> b) -> i ~> a || b
right :: forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> b) -> i ~> (a || b)
right i ~> b
x = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b (b ~> (a || b)) -> (i ~> b) -> i ~> (a || b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. i ~> b
x

either
  :: forall {k} a b c i
   . (HasBinaryCoproducts k, CCC k, Ob (a :: k), Ob b, Ob c)
  => i ~> a ~~> c
  -> i ~> b ~~> c
  -> i ~> (a || b) ~~> c
either :: forall {k} (a :: k) (b :: k) (c :: k) (i :: k).
(HasBinaryCoproducts k, CCC k, Ob a, Ob b, Ob c) =>
(i ~> (a ~~> c)) -> (i ~> (b ~~> c)) -> i ~> ((a || b) ~~> c)
either i ~> (a ~~> c)
f i ~> (b ~~> c)
g = forall (a :: k) (b :: k) (c :: k).
(CCC k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(CCC k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
swapExp @(a || b) @i @c (forall (a :: k) (b :: k) (c :: k).
(CCC k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(CCC k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
swapExp @i @a @c i ~> (a ~~> c)
f (a ~> (i ~~> c)) -> (b ~> (i ~~> c)) -> (a || b) ~> (i ~~> c)
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| forall (a :: k) (b :: k) (c :: k).
(CCC k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(CCC k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
swapExp @i @b @c i ~> (b ~~> c)
g) ((Ob i, Ob (a ~~> c)) => i ~> ((a || b) ~~> c))
-> (i ~> (a ~~> c)) -> i ~> ((a || b) ~~> c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ i ~> (a ~~> c)
f

swapExp :: forall {k} (a :: k) b c. (CCC k, Ob b, Ob c) => a ~> b ~~> c -> b ~> a ~~> c
swapExp :: forall {k} (a :: k) (b :: k) (c :: k).
(CCC k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
swapExp a ~> (b ~~> c)
f = forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @b @a @c (forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @a @b @c a ~> (b ~~> c)
f ((a ** b) ~> c) -> ((b ** a) ~> (a ** b)) -> (b ** a) ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @_ @b @a) ((Ob a, Ob (b ~~> c)) => b ~> (a ~~> c))
-> (a ~> (b ~~> c)) -> b ~> (a ~~> c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (b ~~> c)
f

data FK k = F k
type instance UN F (F a) = a

infixr 2 -->

data family InitF :: k
data family TermF :: k
data family (+) (a :: k) (b :: k) :: k
data family (*) (a :: k) (b :: k) :: k
data family (-->) (a :: k) (b :: k) :: k

data FreeCCC :: CAT (FK k) where
  Id :: (Ob a) => FreeCCC a a
  Comp :: FreeCCC b c -> FreeCCC a b -> FreeCCC a c
  Ini :: (Ob a) => FreeCCC InitF a
  Ter :: (Ob a) => FreeCCC a TermF
  Lft :: (Ob a, Ob b) => FreeCCC a (a + b)
  Rgt :: (Ob a, Ob b) => FreeCCC b (a + b)
  Sum :: FreeCCC a c -> FreeCCC b c -> FreeCCC (a + b) c
  Fst :: (Ob a, Ob b) => FreeCCC (a * b) a
  Snd :: (Ob a, Ob b) => FreeCCC (a * b) b
  Prd :: FreeCCC a b -> FreeCCC a c -> FreeCCC a (b * c)
  Curry :: (Ob a, Ob b) => FreeCCC (a * b) c -> FreeCCC a (b --> c)
  Uncurry :: (Ob b, Ob c) => FreeCCC a (b --> c) -> FreeCCC (a * b) c
  Ex :: FreeCCC b y -> FreeCCC x a -> FreeCCC (a --> b) (x --> y)

instance P.Show (FreeCCC a b) where
  show :: FreeCCC a b -> String
show FreeCCC a b
Id = String
"id"
  show (Comp FreeCCC b b
f FreeCCC a b
g) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC b b -> String
forall a. Show a => a -> String
P.show FreeCCC b b
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" . " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC a b -> String
forall a. Show a => a -> String
P.show FreeCCC a b
g String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show FreeCCC a b
Ini = String
"initiate"
  show FreeCCC a b
Ter = String
"terminate"
  show FreeCCC a b
Lft = String
"lft"
  show FreeCCC a b
Rgt = String
"rgt"
  show (Sum FreeCCC a b
f FreeCCC b b
g) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC a b -> String
forall a. Show a => a -> String
P.show FreeCCC a b
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" ||| " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC b b -> String
forall a. Show a => a -> String
P.show FreeCCC b b
g String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show FreeCCC a b
Fst = String
"fst"
  show FreeCCC a b
Snd = String
"snd"
  show (Prd FreeCCC a b
f FreeCCC a c
g) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC a b -> String
forall a. Show a => a -> String
P.show FreeCCC a b
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" &&& " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC a c -> String
forall a. Show a => a -> String
P.show FreeCCC a c
g String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Curry FreeCCC (a * b) c
f) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
"curry " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC (a * b) c -> String
forall a. Show a => a -> String
P.show FreeCCC (a * b) c
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Uncurry FreeCCC a (b --> b)
f) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
"uncurry " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC a (b --> b) -> String
forall a. Show a => a -> String
P.show FreeCCC a (b --> b)
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"
  show (Ex FreeCCC b y
f FreeCCC x a
g) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
"ex " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC b y -> String
forall a. Show a => a -> String
P.show FreeCCC b y
f String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ FreeCCC x a -> String
forall a. Show a => a -> String
P.show FreeCCC x a
g String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
")"

type family FromFree (t :: FK k) :: k where
  FromFree (F a) = a
  FromFree InitF = InitialObject
  FromFree TermF = TerminalObject
  FromFree (a + b) = FromFree a || FromFree b
  FromFree (a * b) = FromFree a && FromFree b
  FromFree (a --> b) = FromFree a ~~> FromFree b

type IsFK :: forall {k}. FK k -> Constraint
class IsFK (a :: FK k) where
  fkId :: a ~> a
  fromFreeObj :: Obj (FromFree a)
instance (CategoryOf k, Ob a) => IsFK (F (a :: k)) where
  fkId :: 'F a ~> 'F a
fkId = 'F a ~> 'F a
FreeCCC ('F a) ('F a)
forall {k} (a :: FK k). Ob a => FreeCCC a a
Id
  fromFreeObj :: Obj (FromFree ('F a))
fromFreeObj = a ~> a
Obj (FromFree ('F a))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (HasInitialObject k) => IsFK (InitF :: FK k) where
  fkId :: InitF ~> InitF
fkId = InitF ~> InitF
FreeCCC InitF InitF
forall {k} (a :: FK k). Ob a => FreeCCC InitF a
Ini
  fromFreeObj :: Obj (FromFree InitF)
fromFreeObj = Obj InitialObject
Obj (FromFree InitF)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
instance (HasTerminalObject k) => IsFK (TermF :: FK k) where
  fkId :: TermF ~> TermF
fkId = TermF ~> TermF
FreeCCC TermF TermF
forall {k} (a :: FK k). Ob a => FreeCCC a TermF
Ter
  fromFreeObj :: Obj (FromFree TermF)
fromFreeObj = Obj TerminalObject
Obj (FromFree TermF)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
instance (HasBinaryCoproducts k, IsFK a, IsFK b) => IsFK (a + b :: FK k) where
  fkId :: (a + b) ~> (a + b)
fkId = FreeCCC a (a + b) -> FreeCCC b (a + b) -> FreeCCC (a + b) (a + b)
forall {k} (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a c -> FreeCCC (b + a) c
Sum FreeCCC a (a + b)
forall {k} (a :: FK k) (b :: FK k).
(Ob a, Ob b) =>
FreeCCC a (a + b)
Lft FreeCCC b (a + b)
forall {k} (b :: FK k) (b :: FK k).
(Ob b, Ob b) =>
FreeCCC b (b + b)
Rgt
  fromFreeObj :: Obj (FromFree (a + b))
fromFreeObj = forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a Obj (FromFree a)
-> (FromFree b ~> FromFree b)
-> (FromFree a || FromFree b) ~> (FromFree a || FromFree b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
instance (HasBinaryProducts k, IsFK a, IsFK b) => IsFK (a * b :: FK k) where
  fkId :: (a * b) ~> (a * b)
fkId = FreeCCC (a * b) a -> FreeCCC (a * b) b -> FreeCCC (a * b) (a * b)
forall {k} (a :: FK k) (b :: FK k) (a :: FK k).
FreeCCC a b -> FreeCCC a a -> FreeCCC a (b * a)
Prd FreeCCC (a * b) a
forall {k} (a :: FK k) (b :: FK k).
(Ob a, Ob b) =>
FreeCCC (a * b) a
Fst FreeCCC (a * b) b
forall {k} (b :: FK k) (b :: FK k).
(Ob b, Ob b) =>
FreeCCC (b * b) b
Snd
  fromFreeObj :: Obj (FromFree (a * b))
fromFreeObj = forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a Obj (FromFree a)
-> (FromFree b ~> FromFree b)
-> (FromFree a && FromFree b) ~> (FromFree a && FromFree b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b
instance (Closed k, IsFK a, IsFK b) => IsFK (a --> b :: FK k) where
  fkId :: (a --> b) ~> (a --> b)
fkId = FreeCCC b b -> FreeCCC a a -> FreeCCC (a --> b) (a --> b)
forall {k} (b :: FK k) (a :: FK k) (x :: FK k) (a :: FK k).
FreeCCC b a -> FreeCCC x a -> FreeCCC (a --> b) (x --> a)
Ex b ~> b
FreeCCC b b
forall {k} (a :: FK k). IsFK a => a ~> a
fkId a ~> a
FreeCCC a a
forall {k} (a :: FK k). IsFK a => a ~> a
fkId
  fromFreeObj :: Obj (FromFree (a --> b))
fromFreeObj = forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b Obj (FromFree b)
-> (FromFree a ~> FromFree a)
-> (FromFree a ~~> FromFree b) ~> (FromFree a ~~> FromFree b)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a
instance (BiCCC k) => Profunctor (FreeCCC :: CAT (FK k)) where
  dimap :: forall (c :: FK k) (a :: FK k) (b :: FK k) (d :: FK k).
(c ~> a) -> (b ~> d) -> FreeCCC a b -> FreeCCC c d
dimap = (c ~> a) -> (b ~> d) -> FreeCCC a b -> FreeCCC c d
FreeCCC c a -> FreeCCC b d -> FreeCCC a b -> FreeCCC c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a b
Id = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Comp FreeCCC b b
f FreeCCC a b
g = r
(Ob a, Ob b) => r
(Ob b, Ob b) => r
r ((Ob b, Ob b) => r) -> FreeCCC b b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC b b
f ((Ob a, Ob b) => r) -> FreeCCC a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a b
g
  (Ob a, Ob b) => r
r \\ FreeCCC a b
Ini = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ FreeCCC a b
Ter = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ FreeCCC a b
Lft = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ FreeCCC a b
Rgt = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Sum FreeCCC a b
f FreeCCC b b
g = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> FreeCCC a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a b
f ((Ob b, Ob b) => r) -> FreeCCC b b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC b b
g
  (Ob a, Ob b) => r
r \\ FreeCCC a b
Fst = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ FreeCCC a b
Snd = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Prd FreeCCC a b
f FreeCCC a c
g = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> FreeCCC a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a b
f ((Ob a, Ob c) => r) -> FreeCCC a c -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a c
g
  (Ob a, Ob b) => r
r \\ Curry FreeCCC (a * b) c
f = r
(Ob a, Ob b) => r
(Ob (a * b), Ob c) => r
r ((Ob (a * b), Ob c) => r) -> FreeCCC (a * b) c -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC (a * b) c
f
  (Ob a, Ob b) => r
r \\ Uncurry FreeCCC a (b --> b)
f = r
(Ob a, Ob b) => r
(Ob a, Ob (b --> b)) => r
r ((Ob a, Ob (b --> b)) => r) -> FreeCCC a (b --> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a (b --> b)
f
  (Ob a, Ob b) => r
r \\ Ex FreeCCC b y
f FreeCCC x a
g = r
(Ob a, Ob b) => r
(Ob b, Ob y) => r
r ((Ob b, Ob y) => r) -> FreeCCC b y -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC b y
f ((Ob x, Ob a) => r) -> FreeCCC x a -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC x a
g
instance (BiCCC k) => Promonad (FreeCCC :: CAT (FK k)) where
  id :: forall (a :: FK k). Ob a => FreeCCC a a
id = a ~> a
FreeCCC a a
forall {k} (a :: FK k). IsFK a => a ~> a
fkId
  FreeCCC b c
Id . :: forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. FreeCCC a b
r = FreeCCC a b
FreeCCC a c
r
  Comp FreeCCC b c
l1 FreeCCC b b
l2 . FreeCCC a b
r = FreeCCC b c
l1 FreeCCC b c -> FreeCCC a b -> FreeCCC a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. (FreeCCC b b
l2 FreeCCC b b -> FreeCCC a b -> FreeCCC a b
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. FreeCCC a b
r)
  FreeCCC b c
l . FreeCCC a b
Id = FreeCCC b c
FreeCCC a c
l
  FreeCCC b c
l . FreeCCC a b
r = case FreeCCC a b
r of
    Comp FreeCCC b b
r1 FreeCCC a b
r2 -> case FreeCCC b c -> FreeCCC b b -> FreeCCC b c
forall (b :: FK k) (c :: FK k) (a :: FK k).
BiCCC k =>
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
simplify FreeCCC b c
l FreeCCC b b
r1 of
      Comp FreeCCC b c
a FreeCCC b b
b -> FreeCCC b c -> FreeCCC a b -> FreeCCC a c
forall {k} (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
Comp FreeCCC b c
a (FreeCCC b b -> FreeCCC a b -> FreeCCC a b
forall {k} (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
Comp FreeCCC b b
b FreeCCC a b
r2)
      FreeCCC b c
a -> FreeCCC b c -> FreeCCC a b -> FreeCCC a c
forall {k} (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
Comp FreeCCC b c
a FreeCCC a b
r2
    FreeCCC a b
_ -> FreeCCC b c -> FreeCCC a b -> FreeCCC a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
BiCCC k =>
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
simplify FreeCCC b c
l FreeCCC a b
r
    where
      simplify :: (BiCCC k) => FreeCCC (b :: FK k) c -> FreeCCC a b -> FreeCCC a c
      simplify :: forall (b :: FK k) (c :: FK k) (a :: FK k).
BiCCC k =>
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
simplify FreeCCC b c
Fst (Prd FreeCCC a b
f FreeCCC a c
_) = FreeCCC a c
FreeCCC a b
f
      simplify FreeCCC b c
Snd (Prd FreeCCC a b
_ FreeCCC a c
g) = FreeCCC a c
FreeCCC a c
g
      simplify FreeCCC b c
Ter FreeCCC a b
g = FreeCCC a c
FreeCCC a TermF
(Ob a, Ob b) => FreeCCC a c
forall {k} (a :: FK k). Ob a => FreeCCC a TermF
Ter ((Ob a, Ob b) => FreeCCC a c) -> FreeCCC a b -> FreeCCC a c
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a b
g
      simplify FreeCCC b c
f FreeCCC a b
Ini = FreeCCC a c
FreeCCC InitF c
(Ob b, Ob c) => FreeCCC a c
forall {k} (a :: FK k). Ob a => FreeCCC InitF a
Ini ((Ob b, Ob c) => FreeCCC a c) -> FreeCCC b c -> FreeCCC a c
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC b c
f
      simplify (Ex FreeCCC b y
f FreeCCC x a
g) (Ex FreeCCC b y
h FreeCCC x a
i) = FreeCCC b y -> FreeCCC x a -> FreeCCC (a --> b) (x --> y)
forall {k} (b :: FK k) (a :: FK k) (x :: FK k) (a :: FK k).
FreeCCC b a -> FreeCCC x a -> FreeCCC (a --> b) (x --> a)
Ex (FreeCCC b y
f FreeCCC b y -> FreeCCC b b -> FreeCCC b y
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. FreeCCC b b
FreeCCC b y
h) (FreeCCC x a
i FreeCCC x a -> FreeCCC x x -> FreeCCC x a
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. FreeCCC x a
FreeCCC x x
g)
      simplify (Prd FreeCCC b b
f FreeCCC b c
g) FreeCCC a b
h = FreeCCC a b -> FreeCCC a c -> FreeCCC a (b * c)
forall {k} (a :: FK k) (b :: FK k) (a :: FK k).
FreeCCC a b -> FreeCCC a a -> FreeCCC a (b * a)
Prd (FreeCCC b b
f FreeCCC b b -> FreeCCC a b -> FreeCCC a b
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. FreeCCC a b
h) (FreeCCC b c
g FreeCCC b c -> FreeCCC a b -> FreeCCC a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. FreeCCC a b
h)
      simplify FreeCCC b c
f (Sum FreeCCC a b
g FreeCCC b b
h) = FreeCCC a c -> FreeCCC b c -> FreeCCC (a + b) c
forall {k} (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a c -> FreeCCC (b + a) c
Sum (FreeCCC b c
f FreeCCC b c -> FreeCCC a b -> FreeCCC a c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. FreeCCC a b
g) (FreeCCC b c
f FreeCCC b c -> FreeCCC b b -> FreeCCC b c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. FreeCCC b b
h)
      simplify FreeCCC b c
f FreeCCC a b
g = FreeCCC b c -> FreeCCC a b -> FreeCCC a c
forall {k} (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
Comp FreeCCC b c
f FreeCCC a b
g
instance (BiCCC k) => CategoryOf (FK k) where
  type (~>) = FreeCCC
  type Ob (a :: FK k) = IsFK a
instance (BiCCC k) => HasInitialObject (FK k) where
  type InitialObject = InitF
  initiate :: forall (a :: FK k). Ob a => InitialObject ~> a
initiate = InitialObject ~> a
FreeCCC InitF a
forall {k} (a :: FK k). Ob a => FreeCCC InitF a
Ini
instance (BiCCC k) => HasTerminalObject (FK k) where
  type TerminalObject = TermF
  terminate :: forall (a :: FK k). Ob a => a ~> TerminalObject
terminate = a ~> TerminalObject
FreeCCC a TermF
forall {k} (a :: FK k). Ob a => FreeCCC a TermF
Ter
instance (BiCCC k) => HasBinaryCoproducts (FK k) where
  type a || b = a + b
  lft :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => a ~> (a || b)
lft = a ~> (a || b)
FreeCCC a (a + b)
forall {k} (a :: FK k) (b :: FK k).
(Ob a, Ob b) =>
FreeCCC a (a + b)
Lft
  rgt :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => b ~> (a || b)
rgt = b ~> (a || b)
FreeCCC b (a + b)
forall {k} (b :: FK k) (b :: FK k).
(Ob b, Ob b) =>
FreeCCC b (b + b)
Rgt
  x ~> a
FreeCCC x a
Lft ||| :: forall (x :: FK k) (a :: FK k) (y :: FK k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
FreeCCC y (x + b)
Rgt = (x || y) ~> a
FreeCCC (x + y) (x + y)
forall {k} (a :: FK k). Ob a => FreeCCC a a
Id
  x ~> a
l ||| y ~> a
r = FreeCCC x a -> FreeCCC y a -> FreeCCC (x + y) a
forall {k} (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a c -> FreeCCC (b + a) c
Sum x ~> a
FreeCCC x a
l y ~> a
FreeCCC y a
r
instance (BiCCC k) => HasBinaryProducts (FK k) where
  type a && b = a * b
  fst :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => (a && b) ~> a
fst = (a && b) ~> a
FreeCCC (a * b) a
forall {k} (a :: FK k) (b :: FK k).
(Ob a, Ob b) =>
FreeCCC (a * b) a
Fst
  snd :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => (a && b) ~> b
snd = (a && b) ~> b
FreeCCC (a * b) b
forall {k} (b :: FK k) (b :: FK k).
(Ob b, Ob b) =>
FreeCCC (b * b) b
Snd
  a ~> x
FreeCCC a x
Fst &&& :: forall (a :: FK k) (x :: FK k) (y :: FK k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
FreeCCC (x * b) y
Snd = a ~> (x && y)
FreeCCC (x * y) (x * y)
forall {k} (a :: FK k). Ob a => FreeCCC a a
Id
  a ~> x
l &&& a ~> y
r = FreeCCC a x -> FreeCCC a y -> FreeCCC a (x * y)
forall {k} (a :: FK k) (b :: FK k) (a :: FK k).
FreeCCC a b -> FreeCCC a a -> FreeCCC a (b * a)
Prd a ~> x
FreeCCC a x
l a ~> y
FreeCCC a y
r
instance (BiCCC k) => MonoidalProfunctor (FreeCCC :: CAT (FK k)) where
  par0 :: FreeCCC Unit Unit
par0 = FreeCCC Unit Unit
FreeCCC TermF TermF
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FK k). Ob a => FreeCCC a a
id
  par :: forall (x1 :: FK k) (x2 :: FK k) (y1 :: FK k) (y2 :: FK k).
FreeCCC x1 x2 -> FreeCCC y1 y2 -> FreeCCC (x1 ** y1) (x2 ** y2)
par = (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
FreeCCC x1 x2 -> FreeCCC y1 y2 -> FreeCCC (x1 ** y1) (x2 ** y2)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: FK k) (b :: FK k) (x :: FK k) (y :: FK k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
(***)
instance (BiCCC k) => Monoidal (FK k) where
  type Unit = TerminalObject
  type a ** b = a && b
  leftUnitor :: forall (a :: FK k). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && a) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: FK k). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
a ~> (TerminalObject && a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: FK k). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
(a && TerminalObject) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: FK k). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
a ~> (a && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: FK k) (b :: FK k) (c :: FK k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = ((a ** b) ** c) ~> (a ** (b ** c))
((a && b) && c) ~> (a && (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd
  associatorInv :: forall (a :: FK k) (b :: FK k) (c :: FK k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ** (b ** c)) ~> ((a ** b) ** c)
(a && (b && c)) ~> ((a && b) && c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv
instance (BiCCC k) => Closed (FK k) where
  type a ~~> b = a --> b
  curry' :: forall (a :: FK k) (b :: FK k) (c :: FK k).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' Obj a
_ Obj b
_ (Uncurry FreeCCC a (b --> c)
f) = a ~> (b ~~> c)
FreeCCC a (b --> c)
f
  curry' Obj a
_ Obj b
_ (Comp FreeCCC b c
f (Uncurry FreeCCC a (b --> b)
g)) = (b ~> c
FreeCCC b c
f (b ~> c) -> Obj b -> (b ~~> b) ~> (b ~~> c)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall (b :: FK k) (y :: FK k) (x :: FK k) (a :: FK k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Obj b
FreeCCC b b
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FK k). Ob a => FreeCCC a a
id) FreeCCC (b --> b) (b --> c)
-> FreeCCC a (b --> b) -> FreeCCC a (b --> c)
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. FreeCCC a (b --> b)
g
  curry' Obj a
a Obj b
b (a ** b) ~> c
f = FreeCCC (a * b) c -> FreeCCC a (b --> c)
forall {k} (a :: FK k) (b :: FK k) (a :: FK k).
(Ob a, Ob b) =>
FreeCCC (a * b) a -> FreeCCC a (b --> a)
Curry (a ** b) ~> c
FreeCCC (a * b) c
f ((Ob a, Ob a) => FreeCCC a (b --> c))
-> FreeCCC a a -> FreeCCC a (b --> c)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ Obj a
FreeCCC a a
a ((Ob b, Ob b) => FreeCCC a (b --> c))
-> FreeCCC b b -> FreeCCC a (b --> c)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ Obj b
FreeCCC b b
b
  uncurry' :: forall (b :: FK k) (c :: FK k) (a :: FK k).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' Obj b
_ Obj c
_ (Curry FreeCCC (a * b) c
f) = (a ** b) ~> c
FreeCCC (a * b) c
f
  uncurry' Obj b
_ Obj c
_ (Comp (Curry FreeCCC (b * b) c
f) FreeCCC a b
g) = FreeCCC (b * b) c
f FreeCCC (b * b) c -> FreeCCC (a * b) (b * b) -> FreeCCC (a * b) c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FK k) (c :: FK k) (a :: FK k).
FreeCCC b c -> FreeCCC a b -> FreeCCC a c
. (a ~> b
FreeCCC a b
g (a ~> b) -> Obj b -> (a && b) ~> (b && b)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: FK k) (b :: FK k) (x :: FK k) (y :: FK k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** Obj b
FreeCCC b b
forall {k} (a :: FK k). Ob a => FreeCCC a a
Id)
  uncurry' Obj b
a Obj c
b a ~> (b ~~> c)
f = FreeCCC a (b --> c) -> FreeCCC (a * b) c
forall {k} (b :: FK k) (c :: FK k) (a :: FK k).
(Ob b, Ob c) =>
FreeCCC a (b --> c) -> FreeCCC (a * b) c
Uncurry a ~> (b ~~> c)
FreeCCC a (b --> c)
f ((Ob b, Ob b) => FreeCCC (a * b) c)
-> FreeCCC b b -> FreeCCC (a * b) c
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ Obj b
FreeCCC b b
a ((Ob c, Ob c) => FreeCCC (a * b) c)
-> FreeCCC c c -> FreeCCC (a * b) c
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ Obj c
FreeCCC c c
b
  b ~> y
FreeCCC b y
Id ^^^ :: forall (b :: FK k) (y :: FK k) (x :: FK k) (a :: FK k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ x ~> a
FreeCCC x a
Id = (a ~~> b) ~> (x ~~> y)
FreeCCC (x --> b) (x --> b)
forall {k} (a :: FK k). Ob a => FreeCCC a a
Id
  b ~> y
l ^^^ x ~> a
r = FreeCCC b y -> FreeCCC x a -> FreeCCC (a --> b) (x --> y)
forall {k} (b :: FK k) (a :: FK k) (x :: FK k) (a :: FK k).
FreeCCC b a -> FreeCCC x a -> FreeCCC (a --> b) (x --> a)
Ex b ~> y
FreeCCC b y
l x ~> a
FreeCCC x a
r

fromFree :: (BiCCC k, Ob a, Ob b) => FreeCCC (a :: FK k) b -> FromFree a ~> FromFree b
fromFree :: forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree (Id @a) = forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a
fromFree (Comp FreeCCC b b
f FreeCCC a b
g) = FreeCCC b b -> FromFree b ~> FromFree b
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC b b
f (FromFree b ~> FromFree b)
-> (FromFree a ~> FromFree b) -> FromFree a ~> FromFree b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. FreeCCC a b -> FromFree a ~> FromFree b
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC a b
g ((Ob b, Ob b) => FromFree a ~> FromFree b)
-> FreeCCC b b -> FromFree a ~> FromFree b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC b b
f
fromFree (Ini @a) = (FromFree b ~> FromFree b) -> InitialObject ~> FromFree b
forall (a' :: k) (a :: k). (a' ~> a) -> InitialObject ~> a
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
initiate' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a)
fromFree (Ter @a) = Obj (FromFree a) -> FromFree a ~> TerminalObject
forall (a :: k) (a' :: k). (a ~> a') -> a ~> TerminalObject
forall k (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
terminate' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a)
fromFree (Lft @a @b) = Obj (FromFree a)
-> Obj (FromFree b) -> FromFree a ~> (FromFree a || FromFree b)
forall (a :: k) (a' :: k) (b :: k).
(a ~> a') -> Obj b -> a ~> (a' || b)
forall k (a :: k) (a' :: k) (b :: k).
HasBinaryCoproducts k =>
(a ~> a') -> Obj b -> a ~> (a' || b)
lft' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b)
fromFree (Rgt @a @b) = Obj (FromFree a)
-> Obj (FromFree a) -> FromFree a ~> (FromFree a || FromFree a)
forall (a :: k) (b :: k) (b' :: k).
Obj a -> (b ~> b') -> b ~> (a || b')
forall k (a :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
Obj a -> (b ~> b') -> b ~> (a || b')
rgt' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b)
fromFree (Sum FreeCCC a b
f FreeCCC b b
g) = (FreeCCC a b -> FromFree a ~> FromFree b
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC a b
f (FromFree a ~> FromFree b)
-> (FromFree b ~> FromFree b)
-> (FromFree a || FromFree b) ~> FromFree b
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FreeCCC b b -> FromFree b ~> FromFree b
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC b b
g) ((Ob a, Ob b) => (FromFree a || FromFree b) ~> FromFree b)
-> FreeCCC a b -> (FromFree a || FromFree b) ~> FromFree b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a b
f ((Ob b, Ob b) => (FromFree a || FromFree b) ~> FromFree b)
-> FreeCCC b b -> (FromFree a || FromFree b) ~> FromFree b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC b b
g
fromFree (Fst @a @b) = (FromFree b ~> FromFree b)
-> Obj (FromFree b) -> (FromFree b && FromFree b) ~> FromFree b
forall (a :: k) (a' :: k) (b :: k).
(a ~> a') -> Obj b -> (a && b) ~> a'
forall k (a :: k) (a' :: k) (b :: k).
HasBinaryProducts k =>
(a ~> a') -> Obj b -> (a && b) ~> a'
fst' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b)
fromFree (Snd @a @b) = Obj (FromFree a)
-> (FromFree b ~> FromFree b)
-> (FromFree a && FromFree b) ~> FromFree b
forall (a :: k) (b :: k) (b' :: k).
Obj a -> (b ~> b') -> (a && b) ~> b'
forall k (a :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
Obj a -> (b ~> b') -> (a && b) ~> b'
snd' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b)
fromFree (Prd FreeCCC a b
f FreeCCC a c
g) = (FreeCCC a b -> FromFree a ~> FromFree b
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC a b
f (FromFree a ~> FromFree b)
-> (FromFree a ~> FromFree c)
-> FromFree a ~> (FromFree b && FromFree c)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& FreeCCC a c -> FromFree a ~> FromFree c
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC a c
g) ((Ob a, Ob b) => FromFree a ~> (FromFree b && FromFree c))
-> FreeCCC a b -> FromFree a ~> (FromFree b && FromFree c)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a b
f ((Ob a, Ob c) => FromFree a ~> (FromFree b && FromFree c))
-> FreeCCC a c -> FromFree a ~> (FromFree b && FromFree c)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a c
g
fromFree (Curry @a @b FreeCCC (a * b) c
f) = Obj (FromFree a)
-> Obj (FromFree b)
-> ((FromFree a ** FromFree b) ~> FromFree c)
-> FromFree a ~> (FromFree b ~~> FromFree c)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
forall k (a :: k) (b :: k) (c :: k).
Closed k =>
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @a) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b) (FreeCCC (a * b) c -> FromFree (a * b) ~> FromFree c
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC (a * b) c
f) ((Ob (a * b), Ob c) => FromFree a ~> (FromFree b ~~> FromFree c))
-> FreeCCC (a * b) c -> FromFree a ~> (FromFree b ~~> FromFree c)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC (a * b) c
f
fromFree (Uncurry @b @c FreeCCC a (b --> b)
f) = Obj (FromFree b)
-> (FromFree b ~> FromFree b)
-> (FromFree a ~> (FromFree b ~~> FromFree b))
-> (FromFree a ** FromFree b) ~> FromFree b
forall (b :: k) (c :: k) (a :: k).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
forall k (b :: k) (c :: k) (a :: k).
Closed k =>
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @b) (forall {k} (a :: FK k). IsFK a => Obj (FromFree a)
forall (a :: FK k). IsFK a => Obj (FromFree a)
fromFreeObj @c) (FreeCCC a (b --> b) -> FromFree a ~> FromFree (b --> b)
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC a (b --> b)
f) ((Ob a, Ob (b --> b)) => (FromFree a && FromFree b) ~> FromFree b)
-> FreeCCC a (b --> b) -> (FromFree a && FromFree b) ~> FromFree b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC a (b --> b)
f
fromFree (Ex FreeCCC b y
f FreeCCC x a
g) = FreeCCC b y -> FromFree b ~> FromFree y
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC b y
f (FromFree b ~> FromFree y)
-> (FromFree x ~> FromFree a)
-> (FromFree a ~~> FromFree b) ~> (FromFree x ~~> FromFree y)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ FreeCCC x a -> FromFree x ~> FromFree a
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree FreeCCC x a
g ((Ob b, Ob y) =>
 (FromFree a ~~> FromFree b) ~> (FromFree x ~~> FromFree y))
-> FreeCCC b y
-> (FromFree a ~~> FromFree b) ~> (FromFree x ~~> FromFree y)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC b y
f ((Ob x, Ob a) =>
 (FromFree a ~~> FromFree b) ~> (FromFree x ~~> FromFree y))
-> FreeCCC x a
-> (FromFree a ~~> FromFree b) ~> (FromFree x ~~> FromFree y)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FK k) (b :: FK k) r.
((Ob a, Ob b) => r) -> FreeCCC a b -> r
\\ FreeCCC x a
g

-- | Adapted from Phil Freeman: https://blog.functorial.com/posts/2017-10-08-HOAS-CCCs.html
toCCC :: forall {k} a b. (BiCCC k) => (Ob (a :: FK k), Ob b) => (TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC :: forall {k} (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC = FreeCCC a b -> FromFree a ~> FromFree b
forall k (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
FreeCCC a b -> FromFree a ~> FromFree b
fromFree (FreeCCC a b -> FromFree a ~> FromFree b)
-> (FreeCCC TermF (a --> b) -> FreeCCC a b)
-> FreeCCC TermF (a --> b)
-> FromFree a ~> FromFree b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Unit ~> (a ~~> b)) -> a ~> b
FreeCCC TermF (a --> b) -> FreeCCC a b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
(Unit ~> (a ~~> b)) -> a ~> b
lower

-- debug :: (a :: FK ()) ~> b -> P.String
-- debug = P.show

-- test1 :: forall {k} (a :: k) b. (BiCCC k, Ob (a :: k), Ob b) => a ~> b || a
-- test1 = toCCC @(F a) @(F b + F a) (lam \x -> right x)
-- test2 :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => a && b ~> b && a
-- test2 = toCCC @(F a * F b) @(F b * F a) (lam \(x :& y) -> (y :& x))
-- test4 :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => a ~> b ~~> (a && b)
-- test4 = toCCC @(F a) @(F b --> F a * F b) (lam \x -> lam \y -> (x :& y))
-- test5 :: forall {k} (a :: k) b. (BiCCC k, Ob a, Ob b) => (a && b) ~> (b && a)
-- test5 = toCCC @(F a * F b) @(F b * F a) (lam \(a :& b) -> lam (\c -> (b :& c)) $ a)
-- test6 :: forall {k} a b c. (BiCCC k, Ob (a :: k), Ob b, Ob c) => b ~~> a ~~> b ~~> c ~> a ~~> b ~~> c
-- test6 = toCCC @(F b --> F a --> F b --> F c) @(F a --> F b --> F c) (lam (\x -> lam (\y -> lam (\z -> (x $ z) $ y $ z))))
-- test7 :: forall {k} a b. (BiCCC k, Ob (a :: k), Ob b) => (a || b) ~> (b || a)
-- test7 = toCCC @(F a + F b) @(F b + F a) (lam \x -> either (lam \y -> right y) (lam \y -> left y) $ x)
-- test8 :: forall {k} (a :: k) b c. (BiCCC k, Ob a, Ob b, Ob c) => a && (b || c) ~> (a && b) || (a && c)
-- test8 =
--   toCCC @(F a * (F b + F c)) @((F a * F b) + (F a * F c))
--     (lam \(a :& bc) -> either (lam \b -> lam \a' -> left (a' :& b)) (lam \c -> lam \a' -> right (a' :& c)) $ bc $ a)