{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LinearTypes #-}

module Control.Category.FreeCartesian where

import Prelude hiding ((.),id,curry)
import Control.Category.Constrained
import Data.Kind

instance (forall x y. (con x, con y) => Show (k x y)) => Show  (Cat k con a b) where
  show :: Cat k con a b -> [Char]
show Cat k con a b
x = forall a. Show a => Int -> a -> ShowS
showsPrec (-Int
1) Cat k con a b
x [Char]
""
  showsPrec :: Int -> Cat k con a b -> ShowS
showsPrec Int
d = \case
    Cat k con a b
I -> [Char] -> ShowS
showString [Char]
"id"
    Cat k con a b
P1 -> [Char] -> ShowS
showString [Char]
"π₁"
    Cat k con a b
P2 -> [Char] -> ShowS
showString [Char]
"π₂"
    Embed k a b
s -> [Char] -> ShowS
showString (forall a. Show a => a -> [Char]
show k a b
s)
    FreeCartesian k con b b
f :.: FreeCartesian k con a b
g -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
>  Int
0) (forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 FreeCartesian k con b b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" ∘ " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 FreeCartesian k con a b
g)
    FreeCartesian k con a b
f :▵: FreeCartesian k con a c
g -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> -Int
1) (forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 FreeCartesian k con a b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" ▵ " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 FreeCartesian k con a c
g)

showDbg :: Int -> Cat k con a b -> ShowS
showDbg :: forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
d = \case
    Embed k a b
_ -> [Char] -> ShowS
showString [Char]
"?"
    Cat k con a b
I -> [Char] -> ShowS
showString [Char]
"id"
    FreeCartesian k con b b
f :.: FreeCartesian k con a b
g -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Eq a => a -> a -> Bool
/= Int
0) (forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 FreeCartesian k con b b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" ∘ " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 FreeCartesian k con a b
g)
    FreeCartesian k con a b
f :▵: FreeCartesian k con a c
g -> Bool -> ShowS -> ShowS
showParen Bool
True (forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
2 FreeCartesian k con a b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [Char] -> ShowS
showString [Char]
" ▵ " forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
2 FreeCartesian k con a c
g)
    Cat k con a b
P2 -> [Char] -> ShowS
showString [Char]
"π₂"
    Cat k con a b
P1 -> [Char] -> ShowS
showString [Char]
"π₁"


parens :: [Char] -> [Char]
parens :: ShowS
parens [Char]
x = [Char]
"(" forall a. Semigroup a => a -> a -> a
<> [Char]
x forall a. Semigroup a => a -> a -> a
<> [Char]
")"

mapGenerators :: (con a, con b) => (forall x y. (con x, con y) => k x y -> k' x y) -> Cat k con a b -> Cat k' con a b
mapGenerators :: forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f = \case
  Cat k con a b
I -> forall (k :: * -> * -> *) (con :: * -> Constraint) a.
FreeCartesian k con a a
I
  Embed k a b
g -> forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
k a b -> FreeCartesian k con a b
Embed (forall x y. (con x, con y) => k x y -> k' x y
f k a b
g)
  FreeCartesian k con b b
a :.: FreeCartesian k con a b
b -> forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f FreeCartesian k con b b
a forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f FreeCartesian k con a b
b
  Cat k con a b
P1 -> forall (con :: * -> Constraint) b (k :: * -> * -> *) a.
con b =>
FreeCartesian k con (a ⊗ b) a
P1
  Cat k con a b
P2 -> forall (con :: * -> Constraint) b (k :: * -> * -> *) b.
con b =>
FreeCartesian k con (b ⊗ b) b
P2
  FreeCartesian k con a b
a :▵: FreeCartesian k con a c
b -> forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f FreeCartesian k con a b
a forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
FreeCartesian k con a b
-> FreeCartesian k con a c -> FreeCartesian k con a (b ⊗ c)
:▵: forall (con :: * -> Constraint) a b (k :: * -> * -> *)
       (k' :: * -> * -> *).
(con a, con b) =>
(forall x y. (con x, con y) => k x y -> k' x y)
-> Cat k con a b -> Cat k' con a b
mapGenerators forall x y. (con x, con y) => k x y -> k' x y
f FreeCartesian k con a c
b
  Cat k con a b
x -> forall a. HasCallStack => [Char] -> a
error (forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 Cat k con a b
x [Char]
" (Free.mapGenerators)")

type Cat = FreeCartesian

data FreeCartesian k {-<-} (con :: Type -> Constraint) {->-} a b where
  I      :: FreeCartesian k {-<-}con{->-} a a
  (:.:)  :: {-<-}con b => {->-} FreeCartesian k {-<-}con{->-} b c -> FreeCartesian k {-<-}con{->-} a b
         -> FreeCartesian k {-<-}con{->-} a c
  Embed  :: {-<-}(con a, con b) => {->-}k a b -> FreeCartesian k {-<-}con{->-} a b
  (:▵:)  :: {-<-}(con a, con b, con c) => {->-}FreeCartesian k {-<-}con {->-}a b -> FreeCartesian k {-<-}con{->-} a c
         -> FreeCartesian k {-<-}con{->-} a (b ⊗ c)
  P1     :: {-<-}con b => {->-} FreeCartesian k {-<-}con{->-} (a ⊗ b) a
  P2     :: {-<-}con a => {->-} FreeCartesian k {-<-}con{->-} (a ⊗ b) b {-<-}

assocRight :: (Cat k obj x y) -> (Cat k obj x y)
assocRight :: forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocRight (FreeCartesian k obj b y
a :.: (forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocRight -> (FreeCartesian k obj b b
b :.: FreeCartesian k obj x b
c))) = (FreeCartesian k obj b y
a forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: FreeCartesian k obj b b
b) forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: FreeCartesian k obj x b
c
assocRight FreeCartesian k obj x y
x = FreeCartesian k obj x y
x

rightView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c
rightView :: forall (obj :: * -> Constraint) a c (k :: * -> * -> *).
(obj a, obj c) =>
Cat k obj a c -> Cat k obj a c
rightView (forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocRight -> (FreeCartesian k obj b c
a :.: FreeCartesian k obj a b
b)) = FreeCartesian k obj b c
a forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: FreeCartesian k obj a b
b
rightView Cat k obj a c
x = forall (k :: * -> * -> *) (con :: * -> Constraint) a.
FreeCartesian k con a a
I forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: Cat k obj a c
x

assocLeft :: (Cat k obj x y) -> (Cat k obj x y)
assocLeft :: forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocLeft ((forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocLeft -> (FreeCartesian k obj b y
a :.: FreeCartesian k obj b b
b)) :.: FreeCartesian k obj x b
c) = FreeCartesian k obj b y
a forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: (FreeCartesian k obj b b
b forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: FreeCartesian k obj x b
c)
assocLeft FreeCartesian k obj x y
x = FreeCartesian k obj x y
x

leftView :: (obj a, obj c) => (Cat k obj a c) -> Cat k obj a c
leftView :: forall (obj :: * -> Constraint) a c (k :: * -> * -> *).
(obj a, obj c) =>
Cat k obj a c -> Cat k obj a c
leftView (forall (k :: * -> * -> *) (obj :: * -> Constraint) x y.
Cat k obj x y -> Cat k obj x y
assocLeft -> (FreeCartesian k obj b c
a :.: FreeCartesian k obj a b
b)) = FreeCartesian k obj b c
a forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: FreeCartesian k obj a b
b
leftView Cat k obj a c
x = Cat k obj a c
x forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: forall (k :: * -> * -> *) (con :: * -> Constraint) a.
FreeCartesian k con a a
I

pattern (:>:) ::  (obj x, obj y) => (obj b)  => Cat k obj b y -> Cat k obj x b -> Cat k obj x y
pattern f $b:>: :: forall (obj :: * -> Constraint) x y (k :: * -> * -> *) b.
(obj x, obj y, obj b) =>
Cat k obj b y -> Cat k obj x b -> Cat k obj x y
$m:>: :: forall {r} {obj :: * -> Constraint} {x} {y} {k :: * -> * -> *}.
(obj x, obj y) =>
Cat k obj x y
-> (forall {b}. obj b => Cat k obj b y -> Cat k obj x b -> r)
-> ((# #) -> r)
-> r
:>: g <- (rightView -> f :.: g)
  where Cat k obj b y
f :>: Cat k obj x b
g = Cat k obj b y
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat k obj x b
g

pattern (:<:) ::  (obj x, obj y) => (obj b) => (Cat k obj b y) -> (Cat k obj x b) -> Cat k obj x y
pattern f $b:<: :: forall (obj :: * -> Constraint) x y (k :: * -> * -> *) b.
(obj x, obj y, obj b) =>
Cat k obj b y -> Cat k obj x b -> Cat k obj x y
$m:<: :: forall {r} {obj :: * -> Constraint} {x} {y} {k :: * -> * -> *}.
(obj x, obj y) =>
Cat k obj x y
-> (forall {b}. obj b => Cat k obj b y -> Cat k obj x b -> r)
-> ((# #) -> r)
-> r
:<: g <- (leftView -> f :.: g)
  where Cat k obj b y
f :<: Cat k obj x b
g = Cat k obj b y
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat k obj x b
g

evalCartesian :: forall k a b con f.
              (ProdObj con, forall x y. (con x, con y) => con (x,y), con (),
               con ~ Obj k, Obj k a, Obj k b, Cartesian f, Obj f ~ con) =>
              (forall α β. (con α, con β) => k α β -> f α β)  ->
              Cat k (Obj k) a b -> f a b
evalCartesian :: forall (k :: * -> * -> *) a b (con :: * -> Constraint)
       (f :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Obj k a, Obj k b, Cartesian f, Obj f ~ con) =>
(forall α β. (con α, con β) => k α β -> f α β)
-> Cat k (Obj k) a b -> f a b
evalCartesian forall α β. (con α, con β) => k α β -> f α β
embed = \case
  Cat k (Obj k) a b
I -> forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
  (FreeCartesian k (Obj k) b b
f :.: FreeCartesian k (Obj k) a b
g) -> forall (k :: * -> * -> *) a b (con :: * -> Constraint)
       (f :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Obj k a, Obj k b, Cartesian f, Obj f ~ con) =>
(forall α β. (con α, con β) => k α β -> f α β)
-> Cat k (Obj k) a b -> f a b
evalCartesian forall α β. (con α, con β) => k α β -> f α β
embed FreeCartesian k (Obj k) b b
f forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b (con :: * -> Constraint)
       (f :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Obj k a, Obj k b, Cartesian f, Obj f ~ con) =>
(forall α β. (con α, con β) => k α β -> f α β)
-> Cat k (Obj k) a b -> f a b
evalCartesian forall α β. (con α, con β) => k α β -> f α β
embed FreeCartesian k (Obj k) a b
g
  (Embed k a b
φ) -> forall α β. (con α, con β) => k α β -> f α β
embed k a b
φ
  Cat k (Obj k) a b
P1 -> forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl
  Cat k (Obj k) a b
P2 -> forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr
  FreeCartesian k (Obj k) a b
f :▵: FreeCartesian k (Obj k) a c
g -> forall (k :: * -> * -> *) a b (con :: * -> Constraint)
       (f :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Obj k a, Obj k b, Cartesian f, Obj f ~ con) =>
(forall α β. (con α, con β) => k α β -> f α β)
-> Cat k (Obj k) a b -> f a b
evalCartesian forall α β. (con α, con β) => k α β -> f α β
embed FreeCartesian k (Obj k) a b
f forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ forall (k :: * -> * -> *) a b (con :: * -> Constraint)
       (f :: * -> * -> *).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Obj k a, Obj k b, Cartesian f, Obj f ~ con) =>
(forall α β. (con α, con β) => k α β -> f α β)
-> Cat k (Obj k) a b -> f a b
evalCartesian forall α β. (con α, con β) => k α β -> f α β
embed FreeCartesian k (Obj k) a c
g
  

instance Category (Cat k con) where
  type Obj (Cat k con) = con
  id :: forall a. Obj (Cat k con) a => Cat k con a a
id = forall (k :: * -> * -> *) (con :: * -> Constraint) a.
FreeCartesian k con a a
I
  FreeCartesian k con b c
I ∘ :: forall a b c.
(Obj (Cat k con) a, Obj (Cat k con) b, Obj (Cat k con) c) =>
Cat k con b c -> Cat k con a b -> Cat k con a c
∘ Cat k con a b
x = Cat k con a b
x
  FreeCartesian k con b c
x ∘ Cat k con a b
I = FreeCartesian k con b c
x
  FreeCartesian k con b c
P1 ∘ (FreeCartesian k con a b
f :▵: FreeCartesian k con a c
_) = FreeCartesian k con a b
f
  FreeCartesian k con b c
P2 ∘ (FreeCartesian k con a b
_ :▵: FreeCartesian k con a c
g) = FreeCartesian k con a c
g
  FreeCartesian k con b c
x ∘ Cat k con a b
y = FreeCartesian k con b c
x forall (con :: * -> Constraint) b (k :: * -> * -> *) c a.
con b =>
FreeCartesian k con b c
-> FreeCartesian k con a b -> FreeCartesian k con a c
:.: Cat k con a b
y
 

instance ({-<-}ProdObj con, con (), forall a b. (con a, con b) => con (a,b), {->-}Monoidal k) =>  Monoidal (FreeCartesian k {-<-}con{->-}) {-<-}where
  FreeCartesian k con a b
f × :: forall a b c d.
(Obj (FreeCartesian k con) a, Obj (FreeCartesian k con) b,
 Obj (FreeCartesian k con) c, Obj (FreeCartesian k con) d) =>
FreeCartesian k con a b
-> FreeCartesian k con c d -> FreeCartesian k con (a ⊗ c) (b ⊗ d)
× FreeCartesian k con c d
g = forall (k :: * -> * -> *) b1 b2 b3 c.
(Obj k (b1 ⊗ b2), Obj k b3, Obj k c, Obj k b1, Obj k b2,
 Cartesian k) =>
k b1 b3 -> k b2 c -> k (b1 ⊗ b2) (b3 ⊗ c)
cartesianCross FreeCartesian k con a b
f FreeCartesian k con c d
g
  assoc :: forall a b c.
(Obj (FreeCartesian k con) a, Obj (FreeCartesian k con) b,
 Obj (FreeCartesian k con) c) =>
FreeCartesian k con ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc = forall a b c (k :: * -> * -> *).
(Obj k a, Obj k b, Obj k c, Cartesian k) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
cartesianAssoc
  assoc' :: forall a b c.
(Obj (FreeCartesian k con) a, Obj (FreeCartesian k con) b,
 Obj (FreeCartesian k con) c) =>
FreeCartesian k con (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' = forall a b c (k :: * -> * -> *).
(Obj k a, Obj k b, Obj k c, Cartesian k) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
cartesianAssoc'
  swap :: forall a b.
(Obj (FreeCartesian k con) a, Obj (FreeCartesian k con) b) =>
FreeCartesian k con (a ⊗ b) (b ⊗ a)
swap = forall a b (k :: * -> * -> *).
(Obj k a, Obj k b, Cartesian k) =>
k (a ⊗ b) (b ⊗ a)
cartesianSwap
  unitor :: forall a.
Obj (FreeCartesian k con) a =>
FreeCartesian k con a (a ⊗ ())
unitor = forall a (k :: * -> * -> *).
(Obj k a, Obj k (), Cartesian k) =>
k a (a ⊗ ())
cartesianUnitor
  unitor' :: forall a.
Obj (FreeCartesian k con) a =>
FreeCartesian k con (a ⊗ ()) a
unitor' = forall a (k :: * -> * -> *).
(Obj k a, Obj k (), Cartesian k) =>
k (a ⊗ ()) a
cartesianUnitor'{->-}
instance ({-<-}ProdObj con, con (), forall a b. (con a, con b) => con (a,b),{->-} Monoidal k) => Cartesian (FreeCartesian k {-<-}con{->-}) {-<-}where
  exl :: forall a b.
O2 (FreeCartesian k con) a b =>
FreeCartesian k con (a ⊗ b) a
exl = forall (con :: * -> Constraint) b (k :: * -> * -> *) a.
con b =>
FreeCartesian k con (a ⊗ b) a
P1
  exr :: forall a b.
O2 (FreeCartesian k con) a b =>
FreeCartesian k con (a ⊗ b) b
exr = forall (con :: * -> Constraint) b (k :: * -> * -> *) b.
con b =>
FreeCartesian k con (b ⊗ b) b
P2
  dup :: forall a.
(Obj (FreeCartesian k con) a, Obj (FreeCartesian k con) (a ⊗ a)) =>
FreeCartesian k con a (a ⊗ a)
dup = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
FreeCartesian k con a b
-> FreeCartesian k con a c -> FreeCartesian k con a (b ⊗ c)
:▵: forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
  ▵ :: forall a b c.
(Obj (FreeCartesian k con) a, Obj (FreeCartesian k con) b,
 Obj (FreeCartesian k con) c) =>
FreeCartesian k con a b
-> FreeCartesian k con a c -> FreeCartesian k con a (b ⊗ c)
(▵) = forall (con :: * -> Constraint) a b c (k :: * -> * -> *).
(con a, con b, con c) =>
FreeCartesian k con a b
-> FreeCartesian k con a c -> FreeCartesian k con a (b ⊗ c)
(:▵:){->-}