Proarrow equipments

0. Equipment.hs

{-# LANGUAGE
    GADTs
  , DataKinds
  , PolyKinds
  , TypeFamilies
  , TypeOperators
  , FlexibleContexts
  , UndecidableInstances
  , MultiParamTypeClasses
  , UndecidableSuperClasses
  #-}
module Equipment where

import Data.Kind (Constraint, Type)
import Data.Constraint (Dict(..))

infixl 6 |||
infixl 5 ===

type family (++) as bs where
  '[] ++ bs = bs
  (a ': as) ++ bs = a ': (as ++ bs)

data PRO pro arr = Pro pro | Companion arr | Conjoint arr

type ProSq' sq a b p = sq a a b b '[p] '[p] '[] '[]
type ProSq sq a b p = Square sq a a b b '[p] '[p] '[] '[]
type ArrSq' sq a b f = sq a b a b '[] '[] '[f] '[f]
type ArrSq sq a b f = Square sq a b a b '[] '[] '[f] '[f]

-- p(g, f)
type App p g f = '[ 'Companion f, 'Pro p, 'Conjoint g ]

data ArrowList sq (a :: obj) (b :: obj) (fs :: [arr]) where
  ArrNil :: Object sq a => ArrowList sq a a '[]
  ArrCons :: (Object sq a, Object sq b, ADom sq f ~ a, ACod sq f ~ b) => Arrow sq a b f -> ArrowList sq b c fs -> ArrowList sq a c (f ': fs)

singArr :: Equipment sq => Arrow sq a b f -> ArrowList sq a b '[f]
singArr f = case okArrow f of Dict -> ArrCons f ArrNil

appendArr :: ArrowList sq a b f -> ArrowList sq b c g -> ArrowList sq a c (f ++ g)
appendArr ArrNil g = g
appendArr (ArrCons f fs) g = ArrCons f (appendArr fs g)

data AProarrow sq (a :: obj) (b :: obj) (p :: PRO pro arr) where
  PRO :: Proarrow sq a b p -> AProarrow sq a b ('Pro p)
  COM :: Arrow sq a b f -> AProarrow sq a b ('Companion f)
  CON :: Arrow sq b a f -> AProarrow sq a b ('Conjoint f)

type family APDom sq p where
  APDom sq ('Pro p) = PDom sq p
  APDom sq ('Companion f) = ADom sq f
  APDom sq ('Conjoint f) = ACod sq f
type family APCod sq p where
  APCod sq ('Pro p) = PCod sq p
  APCod sq ('Companion f) = ACod sq f
  APCod sq ('Conjoint f) = ADom sq f

okAProarrow :: Equipment sq => AProarrow sq a b p -> Dict (Object sq a, Object sq b, APDom sq p ~ a, APCod sq p ~ b)
okAProarrow (PRO p) = case okProarrow p of Dict -> Dict
okAProarrow (COM f) = case okArrow f of Dict -> Dict
okAProarrow (CON f) = case okArrow f of Dict -> Dict

data ProarrowList sq (a :: obj) (b :: obj) (ps :: [PRO pro arr]) where
  ProNil :: Object sq a => ProarrowList sq a a '[]
  ProCons :: (Object sq a, Object sq b, APDom sq p ~ a, APCod sq p ~ b) => AProarrow sq a b p -> ProarrowList sq b c ps -> ProarrowList sq a c (p ': ps)

appendPro :: ProarrowList sq a b p -> ProarrowList sq b c q -> ProarrowList sq a c (p ++ q)
appendPro ProNil q = q
appendPro (ProCons p ps) q = ProCons p (appendPro ps q)

singPro :: Equipment sq => AProarrow sq a b p -> ProarrowList sq a b '[p]
singPro p = case okAProarrow p of Dict -> ProCons p ProNil

sing :: Equipment sq => (x -> AProarrow sq a b p) -> x -> ProarrowList sq a b '[p]
sing f x = singPro (f x)

data Square sq a b c d p q f g where
  Square :: (Object sq a, Object sq b, Object sq c, Object sq d) =>
    { srcPro :: ProarrowList sq a c p
    , tgtPro :: ProarrowList sq b d q
    , srcArr :: ArrowList sq a b f
    , tgtArr :: ArrowList sq c d g
    , innerSquare :: sq a b c d p q f g
    } -> Square sq a b c d p q f g

type family ObjKind sq where
  ObjKind (sq :: obj -> obj -> obj -> obj -> [PRO pro arr] -> [PRO pro arr] -> [arr] -> [arr] -> Type) = obj
type family ArrKind sq where
  ArrKind (sq :: obj -> obj -> obj -> obj -> [PRO pro arr] -> [PRO pro arr] -> [arr] -> [arr] -> Type) = arr
type family ProKind sq where
  ProKind (sq :: obj -> obj -> obj -> obj -> [PRO pro arr] -> [PRO pro arr] -> [arr] -> [arr] -> Type) = pro

-- sq a b c d p q f g:
-- A--f--B
-- |  v  |
-- p--@--q
-- |  v  |
-- C--g--D
class Equipment (sq :: obj -> obj -> obj -> obj -> [PRO pro arr] -> [PRO pro arr] -> [arr] -> [arr] -> Type) where

  type Object sq (a :: obj) :: Constraint

  data Arrow sq (a :: obj) (b :: obj) (f :: arr) :: *
  data Proarrow sq (a :: obj) (b :: obj) (p :: pro) :: *

  type ADom sq (f :: arr) :: obj
  type ACod sq (f :: arr) :: obj
  type PDom sq (p :: pro) :: obj
  type PCod sq (p :: pro) :: obj

  okArrow :: Arrow sq a b f -> Dict (Object sq a, Object sq b, ADom sq f ~ a, ACod sq f ~ b)
  okProarrow :: Proarrow sq a b p -> Dict (Object sq a, Object sq b, PDom sq p ~ a, PCod sq p ~ b)

  -- A-----A
  -- |     |
  -- |     |
  -- |     |
  -- A-----A
  object' :: Object sq a => sq a a a a '[] '[] '[] '[]

  -- +--f--+     +--h--+       +-f.h-+
  -- |  v  |     |  v  |       |  v  |
  -- p--@--q ||| q--@--r  ==>  p--@--r
  -- |  v  |     |  v  |       |  v  |
  -- +--g--+     +--i--+       +-g.i-+
  (|||~) :: Square sq a b c d p q f g -> Square sq b k d l q r h i -> sq a k c l p r (f ++ h) (g ++ i)

  -- +-----+
  -- |     |
  -- p-----p
  -- |     |
  -- +-----+
  idPro' :: AProarrow sq a b p -> ProSq' sq a b p

  -- +--f--+
  -- |  v  |
  -- p--@--q
  -- |  v  |
  -- +--g--+
  --   ===
  -- +--g--+
  -- |  v  |
  -- r--@--s
  -- |  v  |
  -- +--h--+
  --
  --   ==>
  --
  -- +--f--+
  -- p  v  q
  -- .--@--.
  -- r  v  s
  -- +--h--+
  (===~) :: Square sq a b c d p q f g -> Square sq c d k l r s g h -> sq a b k l (p ++ r) (q ++ s) f h

  -- +--f--+
  -- |  |  |
  -- |  v  |
  -- |  |  |
  -- +--f--+
  idArr' :: Arrow sq a b f -> ArrSq' sq a b f

  -- +-----+
  -- |     |
  -- |  /-<f
  -- |  v  |
  -- +--f--+
  fromRight' :: Arrow sq a b f -> sq a a a b '[] '[ 'Companion f ] '[] '[f]

  -- +--f--+
  -- |  v  |
  -- f<-/  |
  -- |     |
  -- +-----+
  toLeft' :: Arrow sq a b f -> sq a b b b '[ 'Companion f ] '[] '[f] '[]

  -- +--f--+
  -- |  v  |
  -- |  \->f
  -- |     |
  -- +-----+
  toRight' :: Arrow sq a b f -> sq a b a a '[] '[ 'Conjoint f ] '[f] '[]

  -- +-----+
  -- |     |
  -- f>-\  |
  -- |  v  |
  -- +--f--+
  fromLeft' :: Arrow sq a b f -> sq b b a b '[ 'Conjoint f ] '[] '[] '[f]


object :: Equipment sq => Object sq a => Square sq a a a a '[] '[] '[] '[]
object = Square ProNil ProNil ArrNil ArrNil object'

(|||) :: Equipment sq => Square sq a b c d p q f g -> Square sq b k d l q r h i -> Square sq a k c l p r (f ++ h) (g ++ i)
sql@(Square p _ f g _) ||| sqr@(Square _ r h i _) = Square p r (f `appendArr` h) (g `appendArr` i) $ sql |||~ sqr

idPro :: Equipment sq => AProarrow sq a b p -> ProSq sq a b p
idPro p = case okAProarrow p of Dict -> Square (singPro p) (singPro p) ArrNil ArrNil $ idPro' p

idsPro :: Equipment sq => ProarrowList sq a b ps -> Square sq a a b b ps ps '[] '[]
idsPro ProNil = object
idsPro (ProCons p ps) = idPro p === idsPro ps

(===) :: Equipment sq => Square sq a b c d p q f g -> Square sq c d k l r s g h -> Square sq a b k l (p ++ r) (q ++ s) f h
sqt@(Square p q f _ _) === sqb@(Square r s _ h _) = Square (p `appendPro` r) (q `appendPro` s) f h $ sqt ===~ sqb

idArr :: Equipment sq => Arrow sq a b f -> ArrSq sq a b f
idArr f = case okArrow f of Dict -> Square ProNil ProNil (singArr f) (singArr f) $ idArr' f

idsArr :: Equipment sq => ArrowList sq a b fs -> Square sq a b a b '[] '[] fs fs
idsArr ArrNil = object
idsArr (ArrCons f fs) = idArr f ||| idsArr fs

fromRight :: Equipment sq => Arrow sq a b f -> Square sq a a a b '[] '[ 'Companion f ] '[] '[f]
fromRight f = case okArrow f of Dict -> Square ProNil (sing COM f) ArrNil (singArr f) $ fromRight' f

toLeft :: Equipment sq => Arrow sq a b f -> Square sq a b b b '[ 'Companion f ] '[] '[f] '[]
toLeft f = case okArrow f of Dict -> Square (sing COM f) ProNil (singArr f) ArrNil $ toLeft' f

toRight :: Equipment sq => Arrow sq a b f -> Square sq a b a a '[] '[ 'Conjoint f ] '[f] '[]
toRight f = case okArrow f of Dict -> Square ProNil (sing CON f) (singArr f) ArrNil $ toRight' f

fromLeft :: Equipment sq => Arrow sq a b f -> Square sq b b a b '[ 'Conjoint f ] '[] '[] '[f]
fromLeft f = case okArrow f of Dict -> Square (sing CON f) ProNil ArrNil (singArr f) $ fromLeft' f

-- A--f--B
-- |  v  |
-- |  @  |
-- |  v  |
-- A--g--B
type NatSq sq a b f g = Square sq a b a b '[] '[] '[f] '[g]
natSq :: Equipment sq => Arrow sq a b f -> Arrow sq a b g -> sq a b a b '[] '[] '[f] '[g] -> NatSq sq a b f g
natSq f g n = case (okArrow f, okArrow g) of (Dict, Dict) -> Square ProNil ProNil (singArr f) (singArr g) n

-- +-----+
-- |  /-<f
-- |  v  |
-- f<-/  |
-- +-----+
companionPcomp :: Equipment sq => Arrow sq a b f -> ProSq sq a b ('Companion f)
companionPcomp f =
  fromRight f
  ===
  toLeft f

-- +---f-+
-- |   v |
-- | /</ |
-- | v   |
-- +-f---+
companionFcomp :: Equipment sq => Arrow sq a b f -> ArrSq sq a b f
companionFcomp f = fromRight f ||| toLeft f

-- +-----+
-- f>-\  |
-- |  v  |
-- |  \->f
-- +-----+
conjointPcomp :: Equipment sq => Arrow sq a b f -> ProSq sq b a ('Conjoint f)
conjointPcomp f =
  fromLeft f
  ===
  toRight f

-- +-f---+
-- | v   |
-- | \>\ |
-- |   v |
-- +---f-+
conjointFcomp :: Equipment sq => Arrow sq a b f -> ArrSq sq a b f
conjointFcomp f = toRight f ||| fromLeft f

-- +-----+
-- f>-\  |
-- |  v  |
-- f<-/  |
-- +-----+
uLeft :: Equipment sq => Arrow sq a b f -> Square sq b b b b '[ 'Conjoint f, 'Companion f ] '[] '[] '[]
uLeft f =
  fromLeft f
  ===
  toLeft f

-- +-----+
-- |  /-<f
-- |  v  |
-- |  \->f
-- +-----+
uRight :: Equipment sq => Arrow sq a b f -> Square sq a a a a '[] '[ 'Companion f, 'Conjoint f ] '[] '[]
uRight f =
  fromRight f
  ===
  toRight f


-- +--f--+
-- |  v  |
-- f<-/  |
-- q-----q
-- g>-\  |
-- |  v  |
-- +--g--+
filler :: Equipment sq => Proarrow sq b d q -> Arrow sq a b f -> Arrow sq c d g -> Square sq a b c d (App q g f) '[ 'Pro q ] '[f] '[g]
filler q f g = toLeft f === idPro (PRO q) === fromLeft g

-- +-f-h-+     +--f--+
-- | v v |     |  v <h
-- | \ / |     |  |/ |
-- p--@--q ==> p--@--q
-- | / \ |     |  |\ |
-- | v v |     |  v >i
-- +-g-i-+     +--g--+
factorizer :: Equipment sq => Square sq a b c d '[ 'Pro p ] '[ 'Pro q ] '[f, h] '[g, i] -> Square sq a (ACod sq f) c (ACod sq g) '[ 'Pro p ] (App q i h) '[f] '[g]
factorizer n@(Square _ _ (f `ArrCons` (h `ArrCons` ArrNil)) (g `ArrCons` (i `ArrCons` ArrNil)) _) =
  (idArr f ||| fromRight h) === n === (idArr g ||| toRight i)


-- +f-f-f+     +--f--+
-- |v v v|     f> v <f
-- | \|/ |     | \|/ |
-- p--@--q <=> p--@--q
-- | /|\ |     | /|\ |
-- |v v v|     g< v >g
-- +g-g-g+     +--g--+
centralLemma :: Equipment sq
  => Square sq a b c d '[ 'Pro p ] '[ 'Pro q ] '[f1, f2, f3] '[g1, g2, g3]
  -> Square sq (ADom sq f2) (ACod sq f2) (ADom sq g2) (ACod sq g2) '[ 'Conjoint f1, 'Pro p, 'Companion g1 ] '[ 'Companion f3, 'Pro q, 'Conjoint g3 ] '[f2] '[g2]
centralLemma n@(Square _ _ (f1 `ArrCons` (f2 `ArrCons` (f3 `ArrCons` ArrNil))) (g1 `ArrCons` (g2 `ArrCons` (g3 `ArrCons` ArrNil))) _) =
  fromLeft f1 ||| idArr f2 ||| fromRight f3
  ===
  n
  ===
  toLeft g1 ||| idArr g2 ||| toRight g3

centralLemma' :: Equipment sq
  => Square sq a b c d '[ 'Conjoint f1, 'Pro p, 'Companion g1 ] '[ 'Companion f3, 'Pro q, 'Conjoint g3] '[f2] '[g2]
  -> Square sq (PDom sq p) (PDom sq q) (PCod sq p) (PCod sq q) '[ 'Pro p ] '[ 'Pro q ] '[f1, f2, f3] '[g1, g2, g3]
centralLemma' n@(Square (CON f1 `ProCons` (PRO p `ProCons` (COM g1 `ProCons` ProNil))) (COM f3 `ProCons` (PRO q `ProCons` (CON g3 `ProCons` ProNil))) _ _ _) =
  (toRight f1 === idPro (PRO p) === fromRight g1) ||| n ||| (toLeft f3 === idPro (PRO q) === fromLeft g3)



data Adjunction sq a b f g = Adj
  (Arrow sq a b f)
  (Arrow sq b a g)
  -- +-----+
  -- |     |
  -- f<-@->g
  -- |     |
  -- +-----+
  (Square sq a a b b '[ 'Companion f ] '[ 'Conjoint g ] '[] '[])
  -- +-----+
  -- |     |
  -- g>-@-<f
  -- |     |
  -- +-----+
  (Square sq a a b b '[ 'Conjoint g ] '[ 'Companion f ] '[] '[])

-- +---------+
-- |         |
-- | /<-@->\ |
-- | v     v |
-- +-f-----g-+
unitAdj :: Equipment sq => Adjunction sq a b f g -> Square sq a a a a '[] '[] '[] '[f, g]
unitAdj (Adj f g l _) = fromRight f ||| l ||| fromLeft g

-- +-g-----f-+
-- | v     v |
-- | \>-@-</ |
-- |         |
-- +---------+
counitAdj :: Equipment sq => Adjunction sq a b f g -> Square sq b b b b '[] '[] '[g, f] '[]
counitAdj (Adj f g _ r) = toRight g ||| r ||| toLeft f

-- +-------------f-+
-- | /<-@->\     | |
-- | v     v     | |
-- | |     \>-@-</ |
-- +-f-------------+
zigzagf :: Equipment sq => Adjunction sq a b f g -> ArrSq sq a b f
zigzagf adj@(Adj f _ _ _) =
  unitAdj adj ||| idArr f
  ===
  idArr f ||| counitAdj adj

-- +-g-------------+
-- | |     /<-@->\ |
-- | v     v     | |
-- | \>-@-</     | |
-- +-------------g-+
zigzagg :: Equipment sq => Adjunction sq a b f g -> ArrSq sq b a g
zigzagg adj@(Adj _ g _ _) =
  idArr g ||| unitAdj adj
  ===
  counitAdj adj ||| idArr g


class (Equipment sq, Object sq a) => Monoid sq m a where
  unit :: Arrow sq a a m ->  sq a a a a '[] '[] '[]     '[m]
  mult :: Arrow sq a a m -> sq a a a a '[] '[] '[m, m] '[m]

class (Equipment sq, Object sq a) => Promonoid sq m a where
  prounit :: AProarrow sq a a m -> sq a a a a '[]     '[m] '[] '[]
  promult :: AProarrow sq a a m -> sq a a a a '[m, m] '[m] '[] '[]

class Equipment (E k) => ECategory (k :: c0 -> Type) where

  type E k :: obj -> obj -> obj -> obj -> [PRO pro arr] -> [PRO pro arr] -> [arr] -> [arr] -> Type
  type CO k (a :: c0) :: obj
  type CP k (a :: c0) (b :: c0) :: pro

  ehom :: k a -> k b -> ProSq sq (CO k a) (CO k b) (CP k a b)
  eid :: k a -> sq (CO k a) (CO k a) (CO k a) (CO k a) '[] '[CP k a a] '[] '[]
  ecomp :: k a -> k b -> k c -> sq (CO k a) (CO k a) (CO k c) (CO k c) '[CP k a b, CP k b c] '[CP k a c] '[] '[]


-- "yoneda" embedding of e: |e|
yHom :: Equipment sq => Arrow sq a e f -> Arrow sq b e g -> Square sq a a b b '[ 'Companion f, 'Conjoint g ] '[ 'Companion f, 'Conjoint g ] '[] '[]
yHom f g = idPro (COM f) === idPro (CON g)

yId :: Equipment sq => Arrow sq a e f -> Square sq a a a a '[] '[ 'Companion f, 'Conjoint f ] '[] '[]
yId = uRight

yComp :: Equipment sq => Arrow sq a e f -> Arrow sq b e g -> Arrow sq c e h
      -> Square sq a a c c '[ 'Companion f, 'Conjoint g, 'Companion g, 'Conjoint h] '[ 'Companion f, 'Conjoint h ] '[] '[]
yComp f g h = idPro (COM f) === uLeft g === idPro (CON h)

-- identity: (yId === yHom) ||| yComp  =  yHom  =  (yHom === yId) ||| yComp
-- associativity: (yHom === yComp) ||| yComp  =  (yComp === yHom) ||| yComp



class Equipment sq => HasWLimits sq j c where
  type WLimit sq j c (f :: ArrKind sq) :: ArrKind sq
  wlimitArr :: AProarrow sq d a j -> Arrow sq d c f -> Arrow sq a c (WLimit sq j c f)
  wlimit' :: AProarrow sq d a j -> Arrow sq d c f -> sq d c a c '[j] '[] '[f] '[WLimit sq j c f]
  wlimitFactorizer' :: Square sq d c a c '[j] '[] '[f] '[h] -> sq a c a c '[] '[] '[WLimit sq j c f] '[h]

wlimit :: HasWLimits sq j c => AProarrow sq d a j -> Arrow sq d c f -> Square sq d c a c '[j] '[] '[f] '[WLimit sq j c f]
wlimit j f = case (okAProarrow j, okArrow f) of
  (Dict, Dict) -> case okArrow (wlimitArr j f) of
    Dict -> Square (j `ProCons` ProNil) ProNil (f `ArrCons` ArrNil) (wlimitArr j f `ArrCons` ArrNil) (wlimit' j f)

wlimitFactorizer
  :: HasWLimits sq j c
  => Square sq d c a c '[j] '[] '[f] '[h]
  -> Square sq a c a c '[ ] '[] '[WLimit sq j c f] '[h]
wlimitFactorizer sq@(Square (j `ProCons` ProNil) _ (f `ArrCons` ArrNil) h _)
  = case okArrow (wlimitArr j f) of
      Dict -> Square ProNil ProNil (wlimitArr j f `ArrCons` ArrNil) h (wlimitFactorizer' sq)

-- D--f--C
-- |  v  |
-- J-\|  |
-- |  @  |
-- K-/   |
-- |     |
-- C-----C

-- D--f--C
-- |  v  |
-- J--@  |
-- |  v  |
-- A--l--C

-- A--l--C
-- |  v  |
-- K--@  |
-- |     |
-- C-----C

-- Pro(J o K, C(1, d)) ~= Pro(K, C(1, l))

1. Equipment-hask.hs

{-# LANGUAGE RankNTypes, TypeOperators, TypeFamilies, GADTs, DataKinds #-}
import Equipment
  
import Data.Profunctor (Profunctor(..), Star(..), Costar(..))
import qualified Data.Profunctor.Composition as P
import Data.Singletons.Prelude.List (type (++))
import Data.Constraint (Dict(..))

-- +--f--+
-- |  v  |
-- p--@--q
-- |  v  |
-- +--g--+
newtype HaskSq (k0 :: * -> * -> *) (k1 :: * -> * -> *) (k2 :: * -> * -> *) (k3 :: * -> * -> *) p q f g = 
  HaskSq { runHaskSq :: forall a b. PList p a b -> PList q (FList g a) (FList f b) }

-- FList '[f, g, h] a ~= h (g (f a))
data FList (fs :: [* -> *]) (a :: *) where
  Identity :: { runIdentity :: a } -> FList '[] a
  Compose :: { getCompose :: FList fs (f a) } -> FList (f ': fs) a

arrmap :: ArrowList HaskSq k l fs -> (a -> b) -> FList fs a -> FList fs b
arrmap ArrNil f = Identity . f . runIdentity
arrmap (ArrCons ArrDict fl) f = Compose . arrmap fl (fmap f) . getCompose

fappend :: ArrowList HaskSq k1 k2 f -> ArrowList HaskSq k3 k4 g -> FList g (FList f a) -> FList (f ++ g) a
fappend ArrNil g = arrmap g runIdentity
fappend (ArrCons _ fs) g = Compose . fappend fs g . arrmap g getCompose

funappend :: ArrowList HaskSq k1 k2 f -> ArrowList HaskSq k3 k4 g -> FList (f ++ g) a -> FList g (FList f a)
funappend ArrNil g = arrmap g Identity
funappend (ArrCons _ fs) g = arrmap g Compose . funappend fs g . getCompose


type family ToProfunctor (p :: PRO (* -> * -> *) (* -> *)) :: * -> * -> * where
  ToProfunctor ('Pro p) = p
  ToProfunctor ('Companion f) = Star f
  ToProfunctor ('Conjoint f) = Costar f

isProfunctor :: AProarrow HaskSq a b p -> Dict (Profunctor (ToProfunctor p))
isProfunctor (PRO ProDict) = Dict
isProfunctor (COM ArrDict) = Dict
isProfunctor (CON ArrDict) = Dict

data PList (ps :: [PRO (* -> * -> *) (* -> *)]) (a :: *) (b :: *) where
  Hom :: (a -> b) -> PList '[] a b
  Procompose :: ToProfunctor p x b -> PList ps a x -> PList (p ': ps) a b

promap :: ProarrowList HaskSq k l ps -> (c -> a) -> (b -> d) -> PList ps a b -> PList ps c d
promap ProNil l r (Hom f) = Hom (r . f . l)
promap (ProCons dict pl) l r (Procompose p ps) = case isProfunctor dict of Dict -> Procompose (rmap r p) (promap pl l id ps)

pappend :: ProarrowList HaskSq k1 k2 p -> ProarrowList HaskSq k3 k4 q -> P.Procompose (PList p) (PList q) a b -> PList (p ++ q) a b
pappend ProNil ql (P.Procompose (Hom f) q) = promap ql id f q
pappend (ProCons _ pl) ql (P.Procompose (Procompose p ps) q) = Procompose p (pappend pl ql (P.Procompose ps q))

punappend :: ProarrowList HaskSq k1 k2 p -> ProarrowList HaskSq k3 k4 q -> PList (p ++ q) a b -> P.Procompose (PList p) (PList q) a b
punappend ProNil _ q = P.Procompose (Hom id) q
punappend (ProCons _ pl) ql (Procompose p pq) = case punappend pl ql pq of P.Procompose ps q -> P.Procompose (Procompose p ps) q

instance Equipment HaskSq where

  type Object HaskSq k = ()
  data Arrow HaskSq a b f where ArrDict :: Functor f => Arrow HaskSq (->) (->) f
  data Proarrow HaskSq a b p where ProDict :: Profunctor p => Proarrow HaskSq (->) (->) p
  okArrow ArrDict = Dict
  okProarrow ProDict = Dict

  type ADom HaskSq f = (->)
  type ACod HaskSq f = (->)
  type PDom HaskSq p = (->)
  type PCod HaskSq p = (->)
  
  object' = HaskSq $ promap ProNil runIdentity Identity
  Square _ _ f g (HaskSq pq) |||~ Square _ r h i (HaskSq qr) = HaskSq $ promap r (funappend g i) (fappend f h) . qr . pq
  idPro' p = HaskSq $ promap (singPro p) runIdentity Identity
  Square p q _ _ (HaskSq pq) ===~ Square r s _ _ (HaskSq rs) = 
    HaskSq $ \pr -> case punappend p r pr of P.Procompose pp rr -> pappend q s (P.Procompose (pq pp) (rs rr))
  idArr' ArrDict = HaskSq $ \(Hom f) -> Hom (arrmap (singArr ArrDict) f)
  fromRight' ArrDict = HaskSq $ \(Hom f) -> Procompose (Star (fmap (Identity . f) . runIdentity . getCompose)) (Hom id)
  toLeft' ArrDict = HaskSq $ \(Procompose (Star f) (Hom g)) -> Hom (Compose . Identity . f . g . runIdentity)
  toRight' ArrDict = HaskSq $ \(Hom f) -> Procompose (Costar (Compose . Identity . fmap (f . runIdentity))) (Hom id)
  fromLeft' ArrDict = HaskSq $ \(Procompose (Costar f) (Hom g)) -> Hom (Identity . f . fmap g . runIdentity . getCompose)

natHaskSq :: (Functor f, Functor g) => (forall a. g a -> f a) -> NatSq HaskSq (->) (->) f g
natHaskSq n = natSq ArrDict ArrDict $ HaskSq $ \(Hom f) -> Hom $ Compose . Identity . fmap f . n . runIdentity . getCompose

2. Equipment-cat.hs

{-# LANGUAGE
    GADTs
  , DataKinds
  , RankNTypes
  , TypeFamilies
  , TypeOperators
  , BlockArguments
  , PatternSynonyms
  , FlexibleContexts
  , FlexibleInstances
  , UndecidableInstances
  , QuantifiedConstraints
  , MultiParamTypeClasses
  #-}
import Prelude ()
import Equipment
import Data.Category
import Data.Category.Functor hiding (Star, pattern Star, Costar, pattern Costar)
import Data.Category.NaturalTransformation (Nat(Nat), (!), natId)
import Data.Category.Product
import Data.Category.Limit
import Data.Category.KanExtension

import Data.Constraint (Dict(..), (\\))

-- A--f--B
-- |  v  |
-- p--@--q
-- |  v  |
-- C--g--D
data CatSq a b c d p q f g where
  CatSq :: (forall x y. Obj (Op c :**: a) (x, y) -> ProarrowList CatSq a c p :% (x, y) -> ProarrowList CatSq b d q :% (ArrowList CatSq c d g :% x, ArrowList CatSq a b f :% y))
         -> CatSq a b c d p q f g


type family FApp d fs a where
  FApp d '[] a = a
  FApp d (f ': fs) a = ArrowList CatSq (Cod f) d fs :% (f :% a)

instance (Category c, Category d) => Functor (ArrowList CatSq c d fs) where
  type Dom (ArrowList CatSq c d fs) = c
  type Cod (ArrowList CatSq c d fs) = d
  type ArrowList CatSq c d fs :% a = FApp d fs a
  ArrNil % f = f
  ArrCons (A f) fs % h = fs % (f % h)

fappend :: (Functor (ArrowList CatSq d e g), Dom (ArrowList CatSq d e g) ~ d, Cod (ArrowList CatSq d e g) ~ e)
        => ArrowList CatSq c d f -> ArrowList CatSq d e g -> Obj c a -> e (ArrowList CatSq d e g :% (ArrowList CatSq c d f :% a)) (ArrowList CatSq c e (f ++ g) :% a)
fappend ArrNil g a = g % a
fappend (ArrCons (A f) fs) g a = fappend fs g (f % a)

funappend :: (Functor (ArrowList CatSq d e g), Dom (ArrowList CatSq d e g) ~ d, Cod (ArrowList CatSq d e g) ~ e)
          => ArrowList CatSq c d f -> ArrowList CatSq d e g -> Obj c a -> e (ArrowList CatSq c e (f ++ g) :% a) (ArrowList CatSq d e g :% (ArrowList CatSq c d f :% a))
funappend ArrNil g a = g % a
funappend (ArrCons (A f) fs) g a = funappend fs g (f % a)


type family PDom' c where PDom' (Op b :**: a) = a
type family PCod' c where PCod' (Op b :**: a) = b
type family PApp d (ps :: [PRO * *]) where
  PApp d '[] = d
  PApp d (p ': ps) = Procompose (AProarrow CatSq (APDom CatSq p) (APCod CatSq p) p) (ProarrowList CatSq (APCod CatSq p) d ps)

data Procompose p q a b where
  Procompose :: (Dom p ~ (Op d :**: c), Dom q ~ (Op e :**: d)) => Obj d x -> p :% (x, b) -> q :% (a, x) -> Procompose p q a b

instance (Category c, Category d) => Functor (ProarrowList CatSq c d ps) where
  type Dom (ProarrowList CatSq c d ps) = Op d :**: c
  type Cod (ProarrowList CatSq c d ps) = (->)
  type ProarrowList CatSq c d ps :% (a, b) = PApp d ps a b
  ProNil % (Op l :**: r) = \f -> r . f . l
  ProCons p ps % (Op l :**: r) = \(Procompose x pax paxb) -> Procompose x ((p % (Op x :**: r)) pax) ((ps % (Op l :**: x)) paxb)

type family APApp p a where
  APApp ('Pro q) a = q :% a
  APApp ('Companion f) (a, b) = Cod f a (f :% b)
  APApp ('Conjoint f) (a, b) = Cod f (f :% a) b

instance (Category c, Category d) => Functor (AProarrow CatSq c d p) where
  type Dom (AProarrow CatSq c d p) = Op d :**: c
  type Cod (AProarrow CatSq c d p) = (->)
  type AProarrow CatSq c d p :% a = APApp p a
  PRO (P p) % a = p % a
  COM (A f) % (Op g :**: h) = \i -> (f % h) . i . g
  CON (A f) % (Op g :**: h) = \i -> h . i . (f % g)

data Proof c d ps a b where Proof :: (Dom (ProarrowList CatSq c d ps) ~ (Op d :**: c)) => { unProof :: ProarrowList CatSq c d ps :% (a, b) } -> Proof c d ps a b
pappend :: (Functor (ProarrowList CatSq d e q), Dom (ProarrowList CatSq d e q) ~ (Op e :**: d), Cod (ProarrowList CatSq d e q) ~ (->))
        => ProarrowList CatSq c d p -> ProarrowList CatSq d e q -> Obj (Op e :**: c) (a, b)
        -> Procompose (ProarrowList CatSq c d p) (ProarrowList CatSq d e q) a b -> Proof c e (p ++ q) a b
pappend ProNil q (Op a :**: _) (Procompose _ xb qax) = Proof ((q % (Op a :**: xb)) qax)
pappend (ProCons _ ps) q (Op a :**: _) (Procompose x (Procompose y pyb psxy) qax) =
  case pappend ps q (Op a :**: y) (Procompose x psxy qax) of
    Proof psqay -> Proof (Procompose y pyb psqay)

punappend :: (Functor (ProarrowList CatSq d e q), Dom (ProarrowList CatSq d e q) ~ (Op e :**: d), Cod (ProarrowList CatSq d e q) ~ (->))
          => ProarrowList CatSq c d p -> ProarrowList CatSq d e q -> Obj (Op e :**: c) (a, b)
          -> ProarrowList CatSq c e (p ++ q) :% (a, b) -> Procompose (ProarrowList CatSq c d p) (ProarrowList CatSq d e q) a b
punappend ProNil _ (Op _ :**: b) pq = Procompose b b pq
punappend (ProCons _ ps) q (Op a :**: _) (Procompose x pxb pqax) =
  case punappend ps q (Op a :**: x) pqax of
    Procompose y psyx qay -> Procompose y (Procompose x pxb psyx) qay


instance Equipment CatSq where

  type Object CatSq k = Category k
  data Arrow CatSq a b f where
    A :: (Functor f, Dom f ~ a, Cod f ~ b) => f -> Arrow CatSq a b f
  data Proarrow CatSq a b p where
    P :: (Functor p, Cod p ~ (->), Dom p ~ (Op b :**: a), Category a, Category b) => p -> Proarrow CatSq a b p
  okArrow (A _) = Dict
  okProarrow (P _) = Dict

  type ADom CatSq f = Dom f
  type ACod CatSq f = Cod f
  type PDom CatSq p = PDom' (Dom p)
  type PCod CatSq p = PCod' (Dom p)

  object' = CatSq (\_ f -> f)
  Square _ _ f g (CatSq pq) |||~ Square _ r h i (CatSq qr) =
    CatSq (\o@(Op x :**: y) -> r % (Op (funappend g i x) :**: fappend f h y) . qr (Op (g % x) :**: (f % y)) . pq o)
  idPro' _ = CatSq (\_ f -> f)
  Square p q f g (CatSq pq) ===~ Square r s _ h (CatSq rs) =
    CatSq (\o@(Op x :**: y) pr -> case punappend p r o pr of
      Procompose z pzy rxz -> unProof (pappend q s (Op (h % x) :**: (f % y)) (Procompose (g % z) (pq (Op z :**: y) pzy) (rs (Op x :**: z) rxz))))
  idArr' (A f) = CatSq (\_ -> (f %))
  fromRight' (A f) = CatSq (\_ h -> let fh = f % h in Procompose (src fh) fh (src fh))
  toLeft' (A _) = CatSq (\_ (Procompose _ g h) -> g . h)
  toRight' (A f) = CatSq (\_ h -> Procompose (tgt h) (f % tgt h) h)
  fromLeft' (A f) = CatSq (\_ (Procompose _ g h) -> g . f % h)

natCatSq :: (Category c, Category d) => Nat c d g f -> NatSq CatSq c d f g
natCatSq n@(Nat g f _) = natSq (A f) (A g) (CatSq (\_ -> (n !)))

limitSq :: HasLimits j k => Arrow CatSq j k f -> NatSq CatSq j k f (ConstF f (Limit f))
limitSq (A f) = natCatSq (limit (natId f))

instance HasRightKan p k => HasWLimits CatSq ('Companion p) k where
  type WLimit CatSq ('Companion p) k f = RanFam p k f
  wlimitArr (COM (A p)) (A f) = case ranF p (natId f) of (Nat l _ _) -> A l
  wlimit' (COM (A p)) (A f) = CatSq \(_ :**: y) (Procompose _ apy xa) -> let n = ran p (natId f) in (n ! y) . (ranF' n ! (apy . xa))
  wlimitFactorizer' (Square (COM (A p) `ProCons` ProNil) _ (A f `ArrCons` ArrNil) (A h `ArrCons` ArrNil) (CatSq sq))
    = CatSq \_ -> (ranFactorizer (Nat (h :.: p) f \z -> let pz = p % z in sq (Op pz :**: z) (Procompose pz pz pz)) !)


class (Functor f, (f :% a) ~ a, (f :% b) ~ b) => IdOnObj f a b where
  idOnObjDict :: f -> Dom f a b -> Dict ((f :% a) ~ a, (f :% b) ~ b)
instance (Functor f, (f :% a) ~ a, (f :% b) ~ b) => IdOnObj f a b where
  idOnObjDict _ _ = Dict

data IdOnObjAsPromonad f = IdOnObjAsPromonad f

instance (Functor f, forall a b. IdOnObj f a b) => Functor (IdOnObjAsPromonad f) where
  type Dom (IdOnObjAsPromonad f) = Op (Dom f) :**: Dom f
  type Cod (IdOnObjAsPromonad f) = (->)
  type IdOnObjAsPromonad f :% (a, b) = Cod f a b
  IdOnObjAsPromonad f % (Op g :**: h) = \m ->
    f % h . m . f % g \\ idOnObjDict f g \\ idOnObjDict f h

instance (Functor f, k ~ Dom f, forall a b. IdOnObj f a b) => Promonoid CatSq ('Pro (IdOnObjAsPromonad f)) k where
  prounit (PRO (P (IdOnObjAsPromonad f)))
    = CatSq (\(Op x :**: _) xy ->
        Procompose x (f % xy) x \\ idOnObjDict f xy)
  promult (PRO (P (IdOnObjAsPromonad f)))
    = CatSq (\(Op x :**: _) (Procompose _z zy (Procompose _w wz xw)) ->
        Procompose x ((zy . wz . f % xw)) x \\ idOnObjDict f xw)

3. Equipment-diagram.hs

{-# LANGUAGE
    GADTs
  , DataKinds
  , InstanceSigs
  , TypeFamilies
  , TypeOperators
  , KindSignatures
  , FlexibleContexts
  , TypeApplications
  , AllowAmbiguousTypes
  , ScopedTypeVariables
  #-}

import Equipment hiding ((===), (|||))
import qualified Equipment as E
import Data.Constraint (Dict(..))

import GHC.Types (type Nat)
import Diagrams.Prelude
import Diagrams.Backend.SVG.CmdLine
import Data.Colour (Colour)
import Data.Colour.SRGB (sRGB24)

data Pt = Pt Nat Nat

data DiaSq (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat) (p :: [PRO Pt Pt]) (q :: [PRO Pt Pt]) (f :: [Pt]) (g :: [Pt]) where
  DiaSq :: { runDiaSq :: Diagram B } -> DiaSq a b c d p q f g

fromSquare :: Square DiaSq a b c d p q f g -> Diagram B
fromSquare = runDiaSq . innerSquare

class HasColor (n :: Nat) where color :: Colour Double
instance HasColor 0 where color = sRGB24 245 168 158
instance HasColor 1 where color = sRGB24 245 234 159
instance HasColor 2 where color = sRGB24 170 150 198
instance HasColor 3 where color = sRGB24 154 208 163
instance HasColor 4 where color = sRGB24 211 166 203
instance HasColor 5 where color = sRGB24 165 219 225
instance HasColor 6 where color = sRGB24 189 190 192
instance HasColor 7 where color = sRGB24 219 164 122

instance Equipment DiaSq where
  type Object DiaSq n = HasColor n
  data Arrow DiaSq a b f where ArrDict :: (HasColor a, HasColor b) => Arrow DiaSq a b ('Pt a b)
  data Proarrow DiaSq a b p where ProDict :: (HasColor a, HasColor b) => Proarrow DiaSq a b ('Pt a b)
  type ADom DiaSq ('Pt a b) = a
  type ACod DiaSq ('Pt a b) = b
  type PDom DiaSq ('Pt a b) = a
  type PCod DiaSq ('Pt a b) = b
  okArrow ArrDict = Dict
  okProarrow ProDict = Dict

  a |||~ b = DiaSq (fromSquare a ||| fromSquare b)
  a ===~ b = DiaSq (fromSquare a === fromSquare b)

  object' :: forall a. Object DiaSq a => DiaSq a a a a '[] '[] '[] '[]
  object' = DiaSq (square 1 # fc (color @a) # lw none)
  idPro' :: forall a b p. AProarrow DiaSq a b p -> ProSq' DiaSq a b p
  idPro' p = case okAProarrow p of Dict -> DiaSq $ hrule 1 # lwG 0.02 <> centerY (rect 1 0.5 # fc (color @a) # lw none === rect 1 0.5 # fc (color @b) # lw none)
  idArr' :: forall a b f. Arrow DiaSq a b f -> ArrSq' DiaSq a b f
  idArr' ArrDict = DiaSq $ vrule 1 # lwG 0.02 <> centerX (rect 0.5 1 # fc (color @a) # lw none ||| rect 0.5 1 # fc (color @b) # lw none)
  fromRight' :: forall a b f. Arrow DiaSq a b f -> DiaSq a a a b '[] '[ 'Companion f ] '[] '[f]
  fromRight' ArrDict = DiaSq $ mkCorner (color @a) (color @b)
  toLeft' :: forall a b f. Arrow DiaSq a b f -> DiaSq a b b b '[ 'Companion f ] '[] '[f] '[]
  toLeft' ArrDict = DiaSq $ rotate (1/2 @@ turn) $ mkCorner (color @b) (color @a)
  toRight' :: forall a b f. Arrow DiaSq a b f -> DiaSq a b a a '[] '[ 'Conjoint f ] '[f] '[]
  toRight' ArrDict = DiaSq $ rotate (1/4 @@ turn) $ mkCorner (color @a) (color @b)
  fromLeft' :: forall a b f. Arrow DiaSq a b f -> DiaSq b b a b '[ 'Conjoint f ] '[] '[] '[f]
  fromLeft' ArrDict = DiaSq $ rotate (3/4 @@ turn) $ mkCorner (color @b) (color @a)

mkCorner :: Colour Double -> Colour Double -> Diagram B
mkCorner a b = translate (r2 (0.5, -0.5)) (scale 0.5 (arc yDir (1/4 @@ turn) # lwG 0.02) <> wedge 0.5 yDir (1/4 @@ turn) # fc b # lw none) <> square 1 # fc a # lw none

mk2Cellpqfg :: forall a b c d. (HasColor a, HasColor b, HasColor c, HasColor d) => Square DiaSq a b c d '[ 'Pro ('Pt a c) ] '[ 'Pro ('Pt b d) ] '[ 'Pt a b ] '[ 'Pt c d ]
mk2Cellpqfg = Square (sing PRO ProDict) (sing PRO ProDict) (singArr ArrDict) (singArr ArrDict) . DiaSq $ 
  circle 0.05 # lwG 0.02 # fc white <>
  hrule 1 # lwG 0.02 <> vrule 1 # lwG 0.02 <>
  center ((square 0.5 # fc (color @a) ||| square 0.5 # fc (color @b)) === (square 0.5 # fc (color @c) ||| square 0.5 # fc (color @d))) # lw none

mk2Cellpq :: forall a b p q. (HasColor a, HasColor b) => ProarrowList DiaSq a b p -> ProarrowList DiaSq a b q -> Square DiaSq a a b b p q '[] '[]
mk2Cellpq p q = Square p q ArrNil ArrNil . DiaSq $
  circle 0.05 # lwG 0.02 # fc white <>
  hrule 1 # lwG 0.02 <>
  center (rect 1 0.5 # fc (color @a) === rect 1 0.5 # fc (color @b)) # lw none

test0 :: ProSq DiaSq 0 1 ('Pro ('Pt 0 1))
test0 = idPro (PRO ProDict)

test1 :: ProSq DiaSq 1 0 ('Pro ('Pt 1 0))
test1 = idPro (PRO ProDict)

test2 :: Square DiaSq 0 0 0 1 '[] '[ 'Companion ('Pt 0 1) ] '[] '[ 'Pt 0 1 ]
test2 = fromRight ArrDict

test3 :: (q ~ 'Pt 1 3, f ~ 'Pt 0 1, g ~ 'Pt 2 3) => Square DiaSq 0 1 2 3 (App q g f) '[ 'Pro q ] '[f] '[g]
test3 = filler ProDict ArrDict ArrDict

test4 :: Square DiaSq 0 1 2 3 '[ 'Pro ('Pt 0 2) ] '[ 'Pro ('Pt 1 3) ] '[ 'Pt 0 1] '[ 'Pt 2 3]
test4 = mk2Cellpqfg

test5 :: Square DiaSq 1 4 3 6 '[ 'Pro ('Pt 1 3) ] '[ 'Pro ('Pt 4 6) ] '[ 'Pt 1 4] '[ 'Pt 3 6]
test5 = mk2Cellpqfg

test6 :: Square DiaSq 4 5 6 7 '[ 'Pro ('Pt 4 6) ] '[ 'Pro ('Pt 5 7) ] '[ 'Pt 4 5] '[ 'Pt 6 7]
test6 = mk2Cellpqfg

adj :: Adjunction DiaSq 0 1 ('Pt 0 1) ('Pt 1 0)
adj = Adj ArrDict ArrDict (mk2Cellpq (sing COM ArrDict) (sing CON ArrDict)) (mk2Cellpq (sing CON ArrDict) (sing COM ArrDict))

main :: IO ()
main = mainWith (fromSquare (centralLemma (test4 E.||| test5 E.||| test6)))

4. FreeEquipment.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NamedFieldPuns #-}
module FreeEquipment where

import Equipment
import Data.Category
import Data.Category.Functor
import Data.Category.Product
import Data.Category.Monoidal
import Data.Constraint (Dict(..), (\\))
import Data.Kind (Type)
import Data.Void (Void)
import Prelude hiding ((.))

type family Combine f as where
  Combine f '[] = Unit f
  Combine f (a ': as) = f :% (a, Combine f as)

type ObjList f = ArrowList (Free f) () ()

combine :: TensorProduct f => f -> ObjList f as -> Obj (Cod f) (Combine f as)
combine f ArrNil = unitObject f
combine f (ArrCons (A a) as) = f % (a :**: combine f as)

combineAppend :: TensorProduct f => f -> ObjList f as -> ObjList f bs -> Cod f (f :% (Combine f as, Combine f bs)) (Combine f (as ++ bs))
combineAppend = combineAppend -- TODO

combineAppend1 :: TensorProduct f => f -> ObjList f as -> Obj (Cod f) b -> Cod f (f :% (Combine f as, b)) (Combine f (as ++ '[b]))
combineAppend1 = combineAppend1 -- TODO

combineAppend' :: TensorProduct f => f -> ObjList f as -> ObjList f bs -> Cod f (Combine f (as ++ bs)) (f :% (Combine f as, Combine f bs))
combineAppend' = combineAppend' -- TODO

combineAppend1' :: TensorProduct f => f -> ObjList f as -> Obj (Cod f) b -> Cod f (Combine f (as ++ '[b])) (f :% (Combine f as, b))
combineAppend1' = combineAppend1' -- TODO


data Free f o1 o2 o3 o4 (ps :: [PRO Void Type]) (qs :: [PRO Void Type]) as bs where
  Unit :: Free f () () () () '[] '[] as as
  Lift :: ObjList f pl
       -> ObjList f g
       -> Cod f (Combine f g) (Combine f h)
       -> ObjList f h
       -> ObjList f pr
       -> Free f () () () () r s (pl ++ h ++ pr) i
       -> Free f () () () () r s (pl ++ g ++ pr) i
  FromRight
    :: ObjList f pl
    -> Obj (Cod f) a
    -> Free f () () () () r s (pl ++ '[a]) i
    -> Free f () () () () r ('Companion a ': s) pl i
  ToRight
    :: ObjList f pl
    -> Obj (Cod f) a
    -> Free f () () () () r s pl i
    -> Free f () () () () r ('Conjoint a ': s) (pl ++ '[a]) i
  FromLeft
    :: Obj (Cod f) a
    -> ObjList f pr
    -> Free f () () () () r s ('[a] ++ pr) i
    -> Free f () () () () ('Conjoint a ': r) s pr i
  ToLeft
    :: Obj (Cod f) a
    -> ObjList f pr
    -> Free f () () () () r s pr i
    -> Free f () () () () ('Companion a ': r) s ('[a] ++ pr) i

-- vertical composition
append :: Free f () () () () p q g h -> Free f () () () () r s h i -> Free f () () () () (p ++ r) (q ++ s) g i
append Unit bs = bs
append (Lift pl g arr h pr as) bs = Lift pl g arr h pr (append as bs)
append (FromRight pl a as) bs = FromRight pl a (append as bs)
append (ToRight pl a as) bs = ToRight pl a (append as bs)
append (ToLeft a pr as) bs = ToLeft a pr (append as bs)
append (FromLeft a pr as) bs = FromLeft a pr (append as bs)

-- horizontal composition
connect
  :: TensorProduct f
  => ObjList f g
  -> ObjList f i
  -> Free f () () () () p q g h
  -> Free f () () () () q r i j
  -> Free f () () () () p r (g ++ i) (h ++ j)
connect _ _ Unit Unit = Unit
connect _ i (Lift pl gm arr hm pr as) bs
  = Lift pl gm arr hm (appendArr pr i) (connect (appendArr (appendArr pl hm) pr) i as bs)
    \\ appendAssocPrf (appendArr pl gm) pr i
    \\ appendAssocPrf (appendArr pl hm) pr i
connect _ i (ToLeft  a pr as) bs
  = ToLeft a (appendArr pr i) (connect pr i as bs)
connect _ i (FromLeft a pr as) bs
  = FromLeft a (appendArr pr i) (connect (ArrCons (A a) pr) i as bs)
connect g _ as (Lift ql im arr jm qr bs)
  = Lift (appendArr g ql) im arr jm qr (connect g (appendArr (appendArr ql jm) qr) as bs)
    \\ appendAssocPrf g ql im
    \\ appendAssocPrf g (appendArr ql im) qr
    \\ appendAssocPrf g ql jm
    \\ appendAssocPrf g (appendArr ql jm) qr
connect g _ as (ToRight ql a bs)
  = ToRight (appendArr g ql) a (connect g ql as bs)
  \\ appendAssocPrf g ql (singArr (A a))
connect g _ as (FromRight ql a bs)
  = FromRight (appendArr g ql) a (connect g (appendArr ql (singArr (A a))) as bs)
  \\ appendAssocPrf g ql (singArr (A a))
connect _ _ (FromRight pl a as) (ToLeft _ qr bs)
  = connect (appendArr pl (singArr (A a))) qr as bs
  \\ appendAssocPrf pl (singArr (A a)) qr
connect _ _ (ToRight pl a as) (FromLeft _ qr bs)
  = connect pl (appendArr (singArr (A a)) qr) as bs
  \\ appendAssocPrf pl (singArr (A a)) qr

appendNilPrf :: ObjList f as -> Dict (as ~ (as ++ '[]))
appendNilPrf ArrNil = Dict
appendNilPrf (ArrCons _ as) = Dict \\ appendNilPrf as

appendAssocPrf
  :: ObjList f as
  -> ObjList f bs
  -> ObjList f cs
  -> Dict (((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs)))
appendAssocPrf ArrNil _ _ = Dict
appendAssocPrf (ArrCons _ as) bs cs = Dict \\ appendAssocPrf as bs cs

pad
  :: TensorProduct f => f
  -> ObjList f pl
  -> ObjList f g
  -> Cod f (Combine f g) (Combine f h)
  -> ObjList f h
  -> ObjList f pr
  -> Cod f (Combine f (pl ++ g ++ pr)) (Combine f (pl ++ h ++ pr))
pad = pad

toArrow :: TensorProduct f => f -> ObjList f bs -> Free f () () () () '[] '[] as bs -> Cod f (Combine f as) (Combine f bs)
toArrow f bs (Lift pl g arr h pr as) = toArrow f bs as . pad f pl g arr h pr
toArrow f bs Unit = pad f ArrNil ArrNil (unitObject f) ArrNil bs

lift
  :: ObjList f as
  -> ObjList f bs
  -> Cod f (Combine f as) (Combine f bs)
  -> Square (Free f) () () () () '[] '[] as bs
lift as bs arr = Square ProNil ProNil as bs (Lift ArrNil as arr bs ArrNil Unit \\ appendNilPrf as \\ appendNilPrf bs)

instance TensorProduct f => Equipment (Free f) where

  type Object (Free f) a = a ~ ()

  data Arrow (Free f) o1 o2 a where
    A :: Obj (Cod f) a -> Arrow (Free f) () () a
  data Proarrow (Free f) o1 o2 p -- only conjoints and companions

  type ADom (Free f) a = ()
  type ACod (Free f) a = ()
  type PDom (Free f) p = ()
  type PCod (Free f) p = ()

  okArrow (A _) = Dict
  okProarrow = \case

  object' = Unit

  f@Square{} |||~ g@Square{} = connect (srcArr f) (srcArr g) (innerSquare f) (innerSquare g)
  f@Square{} ===~ g@Square{} = innerSquare f `append` innerSquare g

  idPro' (PRO p) = case p of {}
  idPro' (CON a@A{}) = fromLeft' a `append` toRight' a
  idPro' (COM a@A{}) = fromRight' a `append` toLeft' a

  idArr' A{} = Unit

  fromRight' (A a) = FromRight ArrNil a Unit
  toLeft' (A a) = ToLeft a ArrNil Unit
  toRight' (A a) = ToRight ArrNil a Unit
  fromLeft' (A a) = FromLeft a ArrNil Unit

data Simpified f (ps :: [PRO Void Type]) (qs :: [PRO Void Type]) as bs where
  Nil
    :: ObjList f g
    -> Cod f (Combine f g) (Combine f h)
    -> ObjList f h
    -> Simpified f '[] '[] g h
  SFromRight
    :: ObjList f g
    -> Cod f (Combine f g) (Combine f h)
    -> ObjList f h
    -> Obj (Cod f) a
    -> Simpified f r s (h ++ '[a]) i
    -> Simpified f r ('Companion a ': s) g i
  SToRight
    :: ObjList f g
    -> Cod f (Combine f g) (Combine f (h ++ '[a]))
    -> ObjList f h
    -> Obj (Cod f) a
    -> Simpified f r s h i
    -> Simpified f r ('Conjoint a ': s) g i
  SFromLeft
    :: Obj (Cod f) a
    -> ObjList f g
    -> Cod f (Combine f g) (Combine f h)
    -> ObjList f h
    -> Simpified f r s ('[a] ++ h) i
    -> Simpified f ('Conjoint a ': r) s g i
  SToLeft
    :: Obj (Cod f) a
    -> ObjList f g
    -> Cod f (Combine f g) (Combine f ('[a] ++ h))
    -> ObjList f h
    -> Simpified f r s h i
    -> Simpified f ('Companion a ': r) s g i

data Optic f a b c d where
  Optic :: Cod f ~ k => Obj k m -> Obj k c -> Obj k d -> k a (f :% (m, c)) -> k (f :% (m, d)) b -> Optic f a b c d

toLens
  :: forall a b c d f. TensorProduct f => f
  -> Simpified f '[ 'Conjoint a, 'Companion b ] '[ 'Conjoint c, 'Companion d ] '[] '[]
  -> Optic f a b c d
toLens f s0 = case s0 of
  SFromLeft a _ alpha0 _ s1 -> case s1 of
    SToRight _ alpha1 m' c s2 -> case s2 of
      SFromRight g arr_f h d s3 -> case s3 of
        SToLeft b _ beta0 _ s4 -> case s4 of
          Nil _ beta1 _ -> Optic (combine f m') c d
                              (combineAppend1' f g c . alpha1 . f % (a :**: alpha0) . rightUnitorInv f a)
                              (rightUnitor f b . f % (b :**: beta1) . beta0 . combineAppend1 f h d . f % (arr_f :**: d))


fromLens
  :: TensorProduct f => f
  -> Optic f a b c d
  -> Square (Free f) () () () () '[ 'Conjoint a, 'Companion b ] '[ 'Conjoint c, 'Companion d ] '[] '[]
fromLens f (Optic m' c' d' amc mdb) =
  fromLeft a
  ===
  amcSq
  ===
  (mSq ||| (toRight c
            ===
            fromRight d))
  ===
  mdbSq
  ===
  toLeft b
  where
    a' = src amc
    b' = tgt mdb
    a = A a'
    b = A b'
    m = A m'
    c = A c'
    d = A d'
    mSq = lift (singArr m) (singArr m) (f % (m' :**: unitObject f))
    amcSq = lift (singArr a) (ArrCons m (singArr c)) (f % (m' :**: rightUnitorInv f c') . amc . rightUnitor f a')
    mdbSq = lift (ArrCons m (singArr d)) (singArr b) (rightUnitorInv f b' . mdb . f % (m' :**: rightUnitor f d'))