{-# 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 -> String
show Cat k con a b
x = Int -> Cat k con a b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (-Int
1) Cat k con a b
x String
""
  showsPrec :: Int -> Cat k con a b -> ShowS
showsPrec Int
d = \case
    Cat k con a b
I -> String -> ShowS
showString String
"id"
    Cat k con a b
E -> String -> ShowS
showString String
"ε"
    Cat k con a b
P1 -> String -> ShowS
showString String
"π₁"
    Cat k con a b
P2 -> String -> ShowS
showString String
"π₂"
    Embed k a b
s -> String -> ShowS
showString (k a b -> String
forall a. Show a => a -> String
show k a b
s)
    FreeCartesian k con b b
f :.: FreeCartesian k con a b
g -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>  Int
0) (Int -> FreeCartesian k con b b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 FreeCartesian k con b b
f ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" ∘ " ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> FreeCartesian k con a b -> ShowS
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> -Int
1) (Int -> FreeCartesian k con a b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 FreeCartesian k con a b
f ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" ▵ " ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> FreeCartesian k con a c -> ShowS
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
_ -> String -> ShowS
showString String
"?"
    Cat k con a b
I -> String -> ShowS
showString String
"id"
    FreeCartesian k con b b
f :.: FreeCartesian k con a b
g -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0) (Int -> FreeCartesian k con b b -> ShowS
forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 FreeCartesian k con b b
f ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" ∘ " ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> FreeCartesian k con a b -> ShowS
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 (Int -> FreeCartesian k con a b -> ShowS
forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
2 FreeCartesian k con a b
f ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. String -> ShowS
showString String
" ▵ " ShowS -> ShowS -> ShowS
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Int -> FreeCartesian k con a c -> ShowS
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 -> String -> ShowS
showString String
"π₂"
    Cat k con a b
P1 -> String -> ShowS
showString String
"π₁"
    Cat k con a b
E -> String -> ShowS
showString String
"ε"


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

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 -> Cat k' con a b
forall (k :: * -> * -> *) (con :: * -> Constraint) a.
FreeCartesian k con a a
I
  Embed k a b
g -> k' a b -> Cat k' con a b
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
k a b -> FreeCartesian k con a b
Embed (k a b -> k' a b
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 x y. (con x, con y) => k x y -> k' x y)
-> FreeCartesian k con b b -> Cat k' con 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 Cat k' con b b -> FreeCartesian k' con a b -> Cat k' con a 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
:.: (forall x y. (con x, con y) => k x y -> k' x y)
-> FreeCartesian k con a b -> FreeCartesian k' con a 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
b
  Cat k con a b
E -> Cat k' con a b
forall (k :: * -> * -> *) (con :: * -> Constraint) a.
FreeCartesian k con a ()
E
  Cat k con a b
P1 -> Cat k' con a b
forall (con :: * -> Constraint) b (k :: * -> * -> *) a.
con b =>
FreeCartesian k con (a ⊗ b) a
P1
  Cat k con a b
P2 -> Cat k' con a b
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 x y. (con x, con y) => k x y -> k' x y)
-> FreeCartesian k con a b -> Cat k' con a 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 Cat 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)
:▵: (forall x y. (con x, con y) => k x y -> k' x y)
-> FreeCartesian k con a c -> 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 c
b
  Cat k con a b
x -> String -> Cat k' con a b
forall a. HasCallStack => String -> a
error (Int -> Cat k con a b -> ShowS
forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 Cat k con a b
x String
" (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 {-<-}
  E      :: FreeCartesian k con a () {->-}

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 :.: (FreeCartesian k obj x b -> FreeCartesian k obj x b
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 FreeCartesian k obj b y
-> FreeCartesian k obj b b -> FreeCartesian k obj b y
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) FreeCartesian k obj b y
-> FreeCartesian k obj x b -> FreeCartesian k obj x y
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 (Cat k obj a c -> Cat k obj a c
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 FreeCartesian k obj b c -> FreeCartesian k obj a b -> Cat k obj a c
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 = FreeCartesian k obj c c
forall (k :: * -> * -> *) (con :: * -> Constraint) a.
FreeCartesian k con a a
I FreeCartesian k obj c c -> Cat k obj a c -> Cat k obj a c
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 ((FreeCartesian k obj b y -> FreeCartesian k obj b y
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 FreeCartesian k obj b y
-> FreeCartesian k obj x b -> FreeCartesian k obj x y
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 FreeCartesian k obj b b
-> FreeCartesian k obj x b -> FreeCartesian k obj x 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 (Cat k obj a c -> Cat k obj a c
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 FreeCartesian k obj b c -> FreeCartesian k obj a b -> Cat k obj a c
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 Cat k obj a c -> FreeCartesian k obj a a -> Cat k obj a c
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 a
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)
-> (Void# -> 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 Cat k obj b y -> Cat k obj x b -> FreeCartesian k obj x y
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)
-> (Void# -> 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 Cat k obj b y -> Cat k obj x b -> FreeCartesian k obj x y
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 -> f a b
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 α β. (con α, con β) => k α β -> f α β)
-> FreeCartesian k (Obj k) b b -> f b b
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 f b b -> f a b -> f a b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. (forall α β. (con α, con β) => k α β -> f α β)
-> FreeCartesian k (Obj k) a b -> f a b
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
φ) -> k a b -> f a b
forall α β. (con α, con β) => k α β -> f α β
embed k a b
φ
  Cat k (Obj k) a b
P1 -> f a b
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl
  Cat k (Obj k) a b
P2 -> f a b
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr
  Cat k (Obj k) a b
E -> f a b
forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
dis
  FreeCartesian k (Obj k) a b
f :▵: FreeCartesian k (Obj k) a c
g -> (forall α β. (con α, con β) => k α β -> f α β)
-> FreeCartesian k (Obj k) a b -> f a b
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 f a b -> f a c -> f a (b, c)
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 α β. (con α, con β) => k α β -> f α β)
-> FreeCartesian k (Obj k) a c -> f 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 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 = FreeCartesian k con a a
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
FreeCartesian k con a c
x
  FreeCartesian k con b c
x ∘ Cat k con a b
I = FreeCartesian k con a c
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 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
FreeCartesian k con a c
g
  FreeCartesian k con b c
x ∘ Cat k con a b
y = FreeCartesian k con b c
x FreeCartesian k con b c -> Cat k con a b -> FreeCartesian k con a c
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 = FreeCartesian k con a b
-> FreeCartesian k con c d -> FreeCartesian k con (a ⊗ c) (b ⊗ d)
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 = FreeCartesian k con ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
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' = FreeCartesian k con (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
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 = FreeCartesian k con (a ⊗ b) (b ⊗ a)
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 = FreeCartesian k con a (a ⊗ ())
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' = FreeCartesian k con (a ⊗ ()) a
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 = FreeCartesian k con (a ⊗ b) a
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 = FreeCartesian k con (a ⊗ b) b
forall (con :: * -> Constraint) b (k :: * -> * -> *) b.
con b =>
FreeCartesian k con (b ⊗ b) b
P2
  dis :: forall a. Obj (FreeCartesian k con) a => FreeCartesian k con a ()
dis = FreeCartesian k con a ()
forall (k :: * -> * -> *) (con :: * -> Constraint) a.
FreeCartesian k con a ()
E
  dup :: forall a.
(Obj (FreeCartesian k con) a, Obj (FreeCartesian k con) (a ⊗ a)) =>
FreeCartesian k con a (a ⊗ a)
dup = FreeCartesian k con a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id FreeCartesian k con a a
-> FreeCartesian k con a a -> FreeCartesian k con a (a ⊗ 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)
:▵: FreeCartesian k con a a
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)
(▵) = 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)
(:▵:){->-}