{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE CPP                   #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE StandaloneDeriving    #-}
-- 'satisfy' experiment
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}

-- For Uncurriable:
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DefaultSignatures     #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# LANGUAGE NoStarIsType #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-inline-rule-shadowing #-}
{-# OPTIONS_GHC -Wno-unused-imports #-} -- TEMP

-- {-# OPTIONS_GHC -fconstraint-solver-iterations=10 #-}

{-# OPTIONS_GHC -Wno-orphans #-} -- For Catify

-- {-# OPTIONS_GHC -ddump-rules #-}

-- | Alternative interface to the class operations from ConCat.Category, so as
-- not to get inlined too eagerly to optimize.

#include "ConCat/Ops.inc"

module ConCat.AltCat (module ConCat.AltCat, module C, Finite, oops) where

import Prelude hiding (id,(.),curry,uncurry,const,unzip,zip,zipWith)
import qualified Prelude as P
import Control.Arrow (runKleisli)
import qualified Data.Tuple as P
import GHC.TypeLits
-- import qualified GHC.Exts
import GHC.Exts (Coercible,coerce,inline)
import Data.Constraint ((\\))
import Data.Proxy (Proxy)
import Data.Void

import Data.Pointed (Pointed)
import qualified Data.Pointed as Pointed
import qualified ConCat.Pointed as ConCatPointed
import qualified ConCat.Zip as ConCatZip
import qualified ConCat.MinMax as ConCatMinMax
import Data.Key (Zip(..))
import Data.Distributive (Distributive(..))
import Data.Functor.Rep (Representable(..),distributeRep)
-- import qualified Data.Functor.Rep as R
import Control.Newtype.Generics (Newtype(..))
-- import Debug.Trace
#ifdef VectorSized
import Data.Proxy (Proxy(..))
import GHC.TypeLits (KnownNat,natVal)
#endif
import Data.Finite (Finite)
import Data.Vector.Sized (Vector)

import ConCat.Misc
  ( (:*),(:+),(:^),Binop, unzip,PseudoFun(..),oops,type (&&),type (&+&)
  , result, C1,C2,C3,C4,C5,C6, int )
import ConCat.Rep hiding (Rep)
import qualified ConCat.Rep as R
import ConCat.Additive
import qualified ConCat.Category as C
import ConCat.Satisfy
import ConCat.Known

import ConCat.Category
  ( Category, Ok,Ok2,Ok3,Ok4,Ok5,Ok6, Ok', (<~), (~>), Show2(..)
  , AssociativePCat, BraidedPCat, MBraidedPCat, ProductCat, Prod, MonoidalPCat, MProductCat
  , AssociativeSCat, BraidedSCat, CoproductCat, Coprod, MCoproductCat
  , MonoidalSCat, CoproductPCat, CoprodP, MCoproductPCat, TracedCat
  , Additive1(..), OkAdd(..), AbelianCat, ScalarCat, LinearCat
  , OkIxProd(..), IxMonoidalPCat, IxProductCat, IxCoproductPCat
  -- , OkIxCoprod(..), IxMonoidalSCat, IxCoproductCat
  , DistribCat
  , ClosedCat, Exp
  , TerminalCat, Unit{-, lunit, runit, constFun-}, OkUnit, CoterminalCat, Counit, constFun2, unitFun, unUnitFun
  , UnitCat
  , ConstCat, ConstObj, lconst, rconst
  , DelayCat, LoopCat
  , BiCCC
  , BoolCat, BoolOf
  , NumCat, IntegralCat, FractionalCat, FloatingCat, RealFracCat, FromIntegralCat
  , EqCat, okTT, OrdCat, MinMaxCat, EnumCat, IfCat, IfT, RepCat
  , CoerceCat, UnknownCat, BottomCat
  -- , Arr, ArrayCat
  , TransitiveCon(..)
  , U2(..), (:**:)(..)
  , type (|-)(..), (<+), OkProd,okProd, OkCoprod,okCoprod, OkExp, okExp
  , OpCon(..),Sat(..) -- ,FunctorC(..)
  , yes1, forkCon, joinCon, inForkCon
  -- Functor-level. To be removed.
  , OkFunctor(..),FunctorCat,Strong,ZipCat,ZapCat,PointedCat{-,SumCat-},AddCat
  , TraversableCat,DistributiveCat,RepresentableCat
  , MinMaxFunctorCat, MinMaxFFunctorCat
  , FiniteCat
  , fmap', liftA2' 
  -- 
  -- , crossSecondFirst
  )

-- | Dummy identity function to trigger rewriting of non-inlining operations to
-- inling operations.
reveal :: (a `k` b) -> (a `k` b)
reveal :: forall (k :: Type -> Type -> Type) a b. k a b -> k a b
reveal k a b
f = k a b
f

-- | Dummy identity function to delay rewriting of non-inlining operations to
-- inling operations.
conceal :: (a `k` b) -> (a `k` b)
conceal :: forall (k :: Type -> Type -> Type) a b. k a b -> k a b
conceal k a b
f = k a b
f

{-# INLINE [0] reveal #-}
{-# INLINE [0] conceal #-}

{-# RULES
"reveal/conceal" forall f. reveal (conceal f) = f
"conceal/reveal" forall f. conceal (reveal f) = f
 #-}

-- TODO: replace reveal & conceal definitions by oops, and see if we ever don't
-- remove them.

infixr 9 .
Op0(id,(Category k, Ok k a) => a `k` a)
Ip2(.,forall k b c a. (Category k, Ok3 k a b c) => (b `k` c) -> (a `k` b) -> (a `k` c))

Op1(lassocP,forall k a b c  . (AssociativePCat k, Ok3 k a b c) => Prod k a (Prod k b c) `k` Prod k (Prod k a b) c)
Op1(rassocP,forall k a b c  . (AssociativePCat k, Ok3 k a b c) => Prod k (Prod k a b) c `k` Prod k a (Prod k b c))

Op0(swapP,forall k a b. (BraidedPCat k, Ok2 k a b) => Prod k a b `k` Prod k b a)

infixr 3 ***, &&&

Ip2(***    ,forall k a b c d. (MonoidalPCat k, Ok4 k a b c d) => (a `k` c) -> (b `k` d) -> (Prod k a b `k` Prod k c d))
Op1(first  ,forall k a c b  . (MonoidalPCat k, Ok3 k a b c) => (a `k` c) -> (Prod k a b `k` Prod k c b))
Op1(second ,forall k a b d  . (MonoidalPCat k, Ok3 k a b d) => (b `k` d) -> (Prod k a b `k` Prod k a d))

secondFirst :: forall k a b d. (MonoidalPCat k, BraidedPCat k, Ok3 k a b d) => b `k` d -> (a :* b) `k` (a :* d)
secondFirst :: forall (k :: Type -> Type -> Type) a b d.
(MonoidalPCat k, BraidedPCat k, Ok3 k a b d) =>
k b d -> k (a :* b) (a :* d)
secondFirst k b d
g = k (d :* a) (a :* d)
forall (k :: Type -> Type -> Type) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod k a b) (Prod k b a)
swapP k (d :* a) (a :* d) -> k (a :* b) (d :* a) -> k (a :* b) (a :* d)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k b d -> k (b :* a) (d :* a)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first k b d
g k (b :* a) (d :* a) -> k (a :* b) (b :* a) -> k (a :* b) (d :* a)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k (a :* b) (b :* a)
forall (k :: Type -> Type -> Type) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod k a b) (Prod k b a)
swapP
                (Con (Sat (Ok k) (a :* b)) => k (a :* b) (a :* d))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> k (a :* b) (a :* d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b
                (Con (Sat (Ok k) (b :* a)) => k (a :* b) (a :* d))
-> ((Sat (Ok k) b && Sat (Ok k) a) |- Sat (Ok k) (b :* a))
-> k (a :* b) (a :* d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b @a
                (Con (Sat (Ok k) (a :* d)) => k (a :* b) (a :* d))
-> ((Sat (Ok k) a && Sat (Ok k) d) |- Sat (Ok k) (a :* d))
-> k (a :* b) (a :* d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @d
                (Con (Sat (Ok k) (d :* a)) => k (a :* b) (a :* d))
-> ((Sat (Ok k) d && Sat (Ok k) a) |- Sat (Ok k) (d :* a))
-> k (a :* b) (a :* d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @d @a
{-# INLINE secondFirst #-}

crossSecondFirst :: forall k a b c d. (MonoidalPCat k, Ok4 k a b c d)
                 => a `k` c -> b `k` d -> (a :* b) `k` (c :* d)
k a c
f crossSecondFirst :: forall (k :: Type -> Type -> Type) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod k a b) (Prod k c d)
`crossSecondFirst` k b d
g = k b d -> k (c :* b) (c :* d)
forall (k :: Type -> Type -> Type) a b d.
(MonoidalPCat k, Ok3 k a b d) =>
k b d -> k (Prod k a b) (Prod k a d)
second k b d
g k (c :* b) (c :* d) -> k (a :* b) (c :* b) -> k (a :* b) (c :* d)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a c -> k (a :* b) (c :* b)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first k a c
f
                         (Con (Sat (Ok k) (a :* b)) => k (a :* b) (c :* d))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> k (a :* b) (c :* d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b
                         (Con (Sat (Ok k) (c :* b)) => k (a :* b) (c :* d))
-> ((Sat (Ok k) c && Sat (Ok k) b) |- Sat (Ok k) (c :* b))
-> k (a :* b) (c :* d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @c @b
                         (Con (Sat (Ok k) (c :* d)) => k (a :* b) (c :* d))
-> ((Sat (Ok k) c && Sat (Ok k) d) |- Sat (Ok k) (c :* d))
-> k (a :* b) (c :* d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @c @d
{-# INLINE crossSecondFirst #-}

Op0(exl,(ProductCat k, Ok2 k a b) => Prod k a b `k` a)
Op0(exr,(ProductCat k, Ok2 k a b) => Prod k a b `k` b)
Op0(dup,forall k a. (ProductCat k, Ok k a) => a `k` Prod k a a)
-- Ip2(&&&,forall k a c d. (ProductCat k, Ok3 k a c d) => (a `k` c) -> (a `k` d) -> (a `k` Prod k c d))

(&&&) :: forall k a c d. (MProductCat k, Ok3 k a c d)
      => (a `k` c) -> (a `k` d) -> (a `k` Prod k c d)
k a c
f &&& :: forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& k a d
g = (k a c
f k a c -> k a d -> k (a :* a) (c :* d)
forall (k :: Type -> Type -> Type) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod k a b) (Prod k c d)
*** k a d
g) k (a :* a) (c :* d) -> k a (a :* a) -> k a (c :* d)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a (a :* a)
forall (k :: Type -> Type -> Type) a.
(ProductCat k, Ok k a) =>
k a (Prod k a a)
dup
  (Con (Sat (Ok k) (a :* a)) => k a (c :* d))
-> ((Sat (Ok k) a && Sat (Ok k) a) |- Sat (Ok k) (a :* a))
-> k a (c :* d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @a
  (Con (Sat (Ok k) (c :* d)) => k a (c :* d))
-> ((Sat (Ok k) c && Sat (Ok k) d) |- Sat (Ok k) (c :* d))
-> k a (c :* d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @c @d
-- for some reason, plain INLINE doesn't do anything
{-# INLINE [0] (&&&) #-}

-- Op1(unfork, forall k a c d. (ProductCat k, Ok3 k a c d) => (a `k` Prod k c d) -> (a `k` c, a `k` d))

Op1(lassocS,forall k a b c. (AssociativeSCat k, Ok3 k a b c) => Coprod k a (Coprod k b c) `k` Coprod k (Coprod k a b) c)
Op1(rassocS,forall k a b c. (AssociativeSCat k, Ok3 k a b c) => Coprod k (Coprod k a b) c `k` Coprod k a (Coprod k b c))

Op0(swapS,forall k a b. (BraidedSCat k, Ok2 k a b) => Coprod k a b `k` Coprod k b a)

infixr 2 +++, |||

Ip2(+++    ,forall k a b c d. (MonoidalSCat k, Ok4 k a b c d) => (c `k` a) -> (d `k` b) -> (Coprod k c d `k` Coprod k a b))
Op1(left   ,forall k a c b  . (MonoidalSCat k, Ok3 k a b c) => (a `k` c) -> (Coprod k a b `k` Coprod k c b))
Op1(right  ,forall k a b d  . (MonoidalSCat k, Ok3 k a b d) => (b `k` d) -> (Coprod k a b `k` Coprod k a d))

Op0(inl,(CoproductCat k, Ok2 k a b) => a `k` Coprod k a b)
Op0(inr,(CoproductCat k, Ok2 k a b) => b `k` Coprod k a b)
Op0(jam,(CoproductCat k, Ok k a) => Coprod k a a `k` a)

Ip2(|||,forall k a c d. (MCoproductCat k, Ok3 k a c d) => (c `k` a) -> (d `k` a) -> (Coprod k c d `k` a))

rightLeft :: forall k a b d. (MCoproductCat k, BraidedSCat k, Ok3 k a b d)
          => b `k` d -> (a :+ b) `k` (a :+ d)
rightLeft :: forall (k :: Type -> Type -> Type) a b d.
(MCoproductCat k, BraidedSCat k, Ok3 k a b d) =>
k b d -> k (a :+ b) (a :+ d)
rightLeft k b d
g = k (d :+ a) (a :+ d)
forall (k :: Type -> Type -> Type) a b.
(BraidedSCat k, Ok2 k a b) =>
k (Coprod k a b) (Coprod k b a)
swapS k (d :+ a) (a :+ d) -> k (a :+ b) (d :+ a) -> k (a :+ b) (a :+ d)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k b d -> k (b :+ a) (d :+ a)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalSCat k, Ok3 k a b c) =>
k a c -> k (Coprod k a b) (Coprod k c b)
left k b d
g k (b :+ a) (d :+ a) -> k (a :+ b) (b :+ a) -> k (a :+ b) (d :+ a)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k (a :+ b) (b :+ a)
forall (k :: Type -> Type -> Type) a b.
(BraidedSCat k, Ok2 k a b) =>
k (Coprod k a b) (Coprod k b a)
swapS
              (Con (Sat (Ok k) (a :+ b)) => k (a :+ b) (a :+ d))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :+ b))
-> k (a :+ b) (a :+ d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a @b
              (Con (Sat (Ok k) (b :+ a)) => k (a :+ b) (a :+ d))
-> ((Sat (Ok k) b && Sat (Ok k) a) |- Sat (Ok k) (b :+ a))
-> k (a :+ b) (a :+ d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @b @a
              (Con (Sat (Ok k) (a :+ d)) => k (a :+ b) (a :+ d))
-> ((Sat (Ok k) a && Sat (Ok k) d) |- Sat (Ok k) (a :+ d))
-> k (a :+ b) (a :+ d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a @d
              (Con (Sat (Ok k) (d :+ a)) => k (a :+ b) (a :+ d))
-> ((Sat (Ok k) d && Sat (Ok k) a) |- Sat (Ok k) (d :+ a))
-> k (a :+ b) (a :+ d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @d @a

plusRightLeft :: forall k a b c d. (MCoproductCat k, Ok4 k a b c d)
              => a `k` c -> b `k` d -> (a :+ b) `k` (c :+ d)
k a c
f plusRightLeft :: forall (k :: Type -> Type -> Type) a b c d.
(MCoproductCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (a :+ b) (c :+ d)
`plusRightLeft` k b d
g = k b d -> k (c :+ b) (c :+ d)
forall (k :: Type -> Type -> Type) a b d.
(MonoidalSCat k, Ok3 k a b d) =>
k b d -> k (Coprod k a b) (Coprod k a d)
right k b d
g k (c :+ b) (c :+ d) -> k (a :+ b) (c :+ b) -> k (a :+ b) (c :+ d)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a c -> k (a :+ b) (c :+ b)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalSCat k, Ok3 k a b c) =>
k a c -> k (Coprod k a b) (Coprod k c b)
left k a c
f
                   (Con (Sat (Ok k) (a :+ b)) => k (a :+ b) (c :+ d))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :+ b))
-> k (a :+ b) (c :+ d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a @b
                   (Con (Sat (Ok k) (c :+ b)) => k (a :+ b) (c :+ d))
-> ((Sat (Ok k) c && Sat (Ok k) b) |- Sat (Ok k) (c :+ b))
-> k (a :+ b) (c :+ d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @c @b
                   (Con (Sat (Ok k) (c :+ d)) => k (a :+ b) (c :+ d))
-> ((Sat (Ok k) c && Sat (Ok k) d) |- Sat (Ok k) (c :+ d))
-> k (a :+ b) (c :+ d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @c @d

Op0(lunit, (UnitCat k, Ok k a) => a `k` Prod k (Unit k) a)
Op0(lcounit, (UnitCat k, Ok k a) => Prod k (Unit k) a `k` a)
Op0(runit, (UnitCat k, Ok k a) => a `k` Prod k a (Unit k))
Op0(rcounit, (UnitCat k, Ok k a) => Prod k a (Unit k) `k` a)

Op0(zeroC, forall k a b. (AbelianCat k, Ok2 k a b) => a `k` b)
Op0(plusC, forall k a b. (AbelianCat k, Ok2 k a b) => Binop (a `k` b))

Op0(inlP,(CoproductPCat k, Ok2 k a b) => a `k` CoprodP k a b)
Op0(inrP,(CoproductPCat k, Ok2 k a b) => b `k` CoprodP k a b)
Op0(jamP,(CoproductPCat k, Ok k a) => CoprodP k a a `k` a)

-- Temporary workaround. See ConCat.Category comments.
infixr 2 ||||
Ip2(||||,forall k a c d. (MCoproductPCat k, Ok3 k a c d) => (c `k` a) -> (d `k` a) -> (CoprodP k c d `k` a))

-- Op0(swapPS,forall k a b. (CoproductPCat k, Ok2 k a b) => CoprodP k a b `k` CoprodP k b a)

-- Op1(leftD ,forall k a aa b. (CoproductPCat k, Ok3 k a b aa) => (a `k` aa) -> (CoprodP k a b `k` CoprodP k aa b))
-- Op1(rightD,forall k a b bb. (CoproductPCat k, Ok3 k a b bb) => (b `k` bb) -> (CoprodP k a b `k` CoprodP k a bb))
-- Op1(lassocSD,forall k a b c. (CoproductPCat k, Ok3 k a b c) => CoprodP k a (CoprodP k b c) `k` CoprodP k (CoprodP k a b) c)
-- Op1(rassocSD,forall k a b c. (CoproductPCat k, Ok3 k a b c) => CoprodP k (CoprodP k a b) c `k` CoprodP k a (CoprodP k b c))

Op1(crossF, (IxMonoidalPCat k h, Ok2 k a b) => h (a `k` b) -> (h a `k` h b))

Op0(exF   , (IxProductCat k h, Ok  k a  ) => h (h a `k` a))
Op1(forkF , (IxProductCat k h, Ok2 k a b) => h (a `k` b) -> (a `k` h b))
Op0(replF , (IxProductCat k h, Ok  k a  ) => a `k` h a)

fmapC' :: (IxProductCat k h, Representable h, Zip h, Pointed h, Ok2 k a b) => (a `k` b) -> (h a `k` h b)
fmapC' :: forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b.
(IxProductCat k h, Representable h, Zip h, Pointed h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC' = h (k a b) -> k (h a) (h b)
forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b.
(IxMonoidalPCat k h, Ok2 k a b) =>
h (k a b) -> k (h a) (h b)
crossF (h (k a b) -> k (h a) (h b))
-> (k a b -> h (k a b)) -> k a b -> k (h a) (h b)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a b -> h (k a b)
forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
(IxProductCat k h, Ok k a) =>
k a (h a)
replF

class    (IxProductCat k h, Functor h, Ok2 k a b) => OkFork h a b k
instance (IxProductCat k h, Functor h, Ok2 k a b) => OkFork h a b k

-- Potential superclass cycle for ‘OkFork’
--   one of whose superclass constraints is headed by a type family:
--     ‘Ok k a’
-- Use UndecidableSuperClasses to accept this

#if 1
{-# RULES

"toCcc'/forkF" forall (fs :: h (a -> b)).
  toCcc' (forkF fs) = satisfy2 @(OkFork h a b) (forkF (toCcc' <$> fs))

 #-}
#endif

Op0(inPF  , (IxCoproductPCat k h, Ok  k a  ) => h (a `k` h a))
Op1(joinPF, (IxCoproductPCat k h, Ok2 k a b) => h (b `k` a) -> (h b `k` a))
-- Op1(plusPF, (IxCoproductPCat k h, Ok2 k a b) => h (b `k` a) -> (h b `k` h a))
Op0(jamPF , (IxCoproductPCat k h, Ok  k a  ) => h a `k` a)

-- Op1(plusF, (IxMonoidalSCat k n, Ok2 k a b) => (h (b `k` a)) -> ((n , b) `k` (n , a)))

-- Op0(inF  , (IxCoproductCat k n, Ok  k a  ) => h (a `k` (n , a)))
-- Op1(joinF, (IxCoproductCat k n, Ok2 k a b) => (h (b `k` a)) -> ((n , b) `k` a))
-- Op0(jamF , (IxCoproductCat k n, Ok  k a  ) => (n , a) `k` a)

Op0(scale,(ScalarCat k a => a -> (a `k` a)))

-- Catify(sumA, jamPF)

#if 0

-- | Generalized matrix
infixr 1 :--*
type (p :--* q) u = q (p u)

linearApp' :: forall k p q u v. ( IxCoproductPCat k p, IxProductCat k q, Additive v, Ok2 k u v
                                , Functor q)
           => (p :--* q) (u `k` v) -> (p u `k` q v)
linearApp' = forkF . fmap joinPF <+ okIxProd @k @p @u
{-# INLINE linearApp' #-}

linearApp :: forall k p q s. ( IxCoproductPCat k p, IxProductCat k q, ScalarCat k s, Additive s, Ok k s
                             , Functor p, Functor q)
          => (p :--* q) s -> (p s `k` q s)
linearApp = linearApp' . (fmap.fmap) scale
{-# INLINE linearApp #-}

#endif

Op0(apply,forall k a b. (ClosedCat k, Ok2 k a b) => Prod k (Exp k a b) a `k` b)
Op1(curry,(ClosedCat k, Ok3 k a b c) => (Prod k a b `k` c) -> (a `k` Exp k b c))
Op1(uncurry,forall k a b c. (ClosedCat k, Ok3 k a b c) => (a `k` Exp k b c)  -> (Prod k a b `k` c))

Op0(distl,forall k a u v. (DistribCat k, Ok3 k a u v) => Prod k a (Coprod k u v) `k` Coprod k (Prod k a u) (Prod k a v))
Op0(distr,forall k u v b. (DistribCat k, Ok3 k u v b) => Prod k (Coprod k u v) b `k` Coprod k (Prod k u b) (Prod k v b))

Op0(it,(TerminalCat k, Ok k a) => a `k` Unit k)
Op0(ti,(CoterminalCat k, Ok k a) => Counit k `k` a)

Op(const,(ConstCat k b, Ok k a) => b -> (a `k` ConstObj k b))
Op(unitArrow,(ConstCat k b, Ok k (Unit k)) => b -> (Unit k `k` ConstObj k b))

Op(trace, (TracedCat k, Ok3 k a b c) => ((a :* c) `k` (b :* c)) -> (a `k` b))

Op(delay,(DelayCat k, Ok k a) => a -> (a `k` a))

Op(loop,(LoopCat k, Ok3 k s a b) => ((a :* s) `k` (b :* s)) -> (a `k` b))

{-# RULES
-- "inOp unitArrow" forall b. reveal (unitArrow b) = C.unitArrow b
"inOp const" forall b. reveal (const b) = C.const b
 #-}

Op0(notC,BoolCat k => BoolOf k `k` BoolOf k)
Op0(andC,BoolCat k => Prod k (BoolOf k) (BoolOf k) `k` BoolOf k)
Op0(orC,BoolCat k => Prod k (BoolOf k) (BoolOf k) `k` BoolOf k)
Op0(xorC,BoolCat k => Prod k (BoolOf k) (BoolOf k) `k` BoolOf k)

Op0(equal,EqCat k a => Prod k a a `k` BoolOf k)
Op0(notEqual,EqCat k a => Prod k a a `k` BoolOf k)

Op0(lessThan,OrdCat k a => Prod k a a `k` BoolOf k)
Op0(greaterThan,OrdCat k a => Prod k a a `k` BoolOf k)
Op0(lessThanOrEqual,OrdCat k a => Prod k a a `k` BoolOf k)
Op0(greaterThanOrEqual,OrdCat k a => Prod k a a `k` BoolOf k)

Op0(minC, (MinMaxCat k a, Ok k a) => Prod k a a `k` a)
Op0(maxC, (MinMaxCat k a, Ok k a) => Prod k a a `k` a)

Op0(succC,EnumCat k a => a `k` a)
Op0(predC,EnumCat k a => a `k` a)

Op0(bottomC,BottomCat k a b => a `k` b)

Op0(ifC,IfCat k a => Prod k (BoolOf k) (Prod k a a) `k` a)

Op0(unknownC,UnknownCat k a b => a `k` b)

Op0(reprC,RepCat k a r => a `k` r)
Op0(abstC,RepCat k a r => r `k` a)

Op0(coerceC,(CoerceCat k a b) => a `k` b)

-- -- Hack to prevent inlining/rewrite loop for reboxing.
-- #undef OPINLINE
-- #define OPINLINE NOINLINE

Op0(negateC,NumCat k a => a `k` a)
Op0(addC,NumCat k a => Prod k a a `k` a)
Op0(subC,NumCat k a => Prod k a a `k` a)
Op0(mulC,NumCat k a => Prod k a a `k` a)
Op0(powIC,(NumCat k a, Ok k Int) => Prod k a Int `k` a)

Op0(divC,IntegralCat k a => Prod k a a `k` a)
Op0(modC,IntegralCat k a => Prod k a a `k` a)
Op0(divModC, (MProductCat k, IntegralCat k a, Ok k a) => Prod k a a `k` Prod k a a)

Op0(recipC,FractionalCat k a => a `k` a)
Op0(divideC,FractionalCat k a => Prod k a a `k` a)

Op0(floorC,RealFracCat k a b => a `k` b)
Op0(ceilingC,RealFracCat k a b => a `k` b)
Op0(truncateC,RealFracCat k a b => a `k` b)

Op0(expC,FloatingCat k a => a `k` a)
Op0(logC,FloatingCat k a => a `k` a)
Op0(cosC,FloatingCat k a => a `k` a)
Op0(sinC,FloatingCat k a => a `k` a)
Op0(sqrtC,FloatingCat k a => a `k` a)
Op0(tanhC,FloatingCat k a => a `k` a)
-- Op0(powC,FloatingCat k a => a `k` a)

Op0(fromIntegralC,FromIntegralCat k a b => a `k` b)

-- Unnecessary but helpful to track NOINLINE choice
-- Op(constFun,forall k p a b. (ClosedCat k, Ok3 k p a b) => (a `k` b) -> (p `k` Exp k a b))

bottomRep :: forall k a b r.
  (Category k, RepCat k b r, BottomCat k a r, Ok3 k a b r) => a `k` b
bottomRep :: forall (k :: Type -> Type -> Type) a b r.
(Category k, RepCat k b r, BottomCat k a r, Ok3 k a b r) =>
k a b
bottomRep = forall (k :: Type -> Type -> Type) a r. RepCat k a r => k r a
abstC @k @b @r k r b -> k a r -> k a b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a r
forall (k :: Type -> Type -> Type) a b. BottomCat k a b => k a b
bottomC

-- lunit :: (ProductCat k, TerminalCat k, Ok k a) => a `k` Prod k (Unit k) a
-- lunit = it &&& id

-- runit :: (ProductCat k, TerminalCat k, Ok k a) => a `k` Prod k a (Unit k)
-- runit = id &&& it

constFun :: forall k p a b. (ClosedCat k, Ok3 k p a b)
         => (a `k` b) -> (p `k` Exp k a b)
constFun :: forall (k :: Type -> Type -> Type) p a b.
(ClosedCat k, Ok3 k p a b) =>
k a b -> k p (Exp k a b)
constFun k a b
f = k (p :* a) b -> k p (Exp k a b)
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k (Prod k a b) c -> k a (Exp k b c)
curry (k a b
f k a b -> k (p :* a) a -> k (p :* a) b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k (p :* a) a
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr) (Con (Sat (Ok k) (p :* a)) => k p (Exp k a b))
-> ((Sat (Ok k) p && Sat (Ok k) a) |- Sat (Ok k) (p :* a))
-> k p (Exp k a b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @p @a
{-# INLINE constFun #-}
-- {-# OPINLINE constFun #-}
-- OpRule1(constFun)

funConst :: forall k a b. (ClosedCat k, TerminalCat k, UnitCat k, Ok2 k a b)
         => (() `k` (a -> b)) -> (a `k` b)
funConst :: forall (k :: Type -> Type -> Type) a b.
(ClosedCat k, TerminalCat k, UnitCat k, Ok2 k a b) =>
k () (a -> b) -> k a b
funConst k () (a -> b)
f = k () (a -> b) -> k (() :* a) b
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp k b c) -> k (Prod k a b) c
uncurry k () (a -> b)
f k (() :* a) b -> k a (() :* a) -> k a b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a (() :* a)
forall (k :: Type -> Type -> Type) a.
(UnitCat k, Ok k a) =>
k a (Prod k () a)
lunit (Con (Sat (Ok k) (() :* a)) => k a b)
-> ((Sat (Ok k) () && Sat (Ok k) a) |- Sat (Ok k) (() :* a))
-> k a b
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(Unit k) @a

#if 0

#ifdef VectorSized

Op0(array, ArrayCat k n b => Exp k (Finite n) b `k` Arr n b)
Op0(arrAt, ArrayCat k n b => Prod k (Arr n b) (Finite n) `k` b)

at :: (ArrayCat k n b, ClosedCat k, Ok3 k (Finite n) b (Arr n b))
   => Arr n b `k` Exp k (Finite n) b
at = curry arrAt
-- {-# OPINLINE at #-}

natV :: forall n. KnownNat n => Integer
natV = natVal (Proxy @n)

#else

Op0(array, ArrayCat k a b => Exp k a b `k` Arr a b)
Op0(arrAt, ArrayCat k a b => Prod k (Arr a b) a `k` b)
-- Op0(at   , ArrayCat k a b => Arr a b `k` Exp k a b)

at :: (ArrayCat k a b, ClosedCat k, Ok3 k a b (Arr a b))
   => Arr a b `k` Exp k a b
at = curry arrAt
-- {-# OPINLINE at #-}

#endif

#endif

-- TODO: Consider moving all of the auxiliary functions (like constFun) here.
-- Rename "ConCat.Category" to something like "ConCat.Category.Class" and
-- "ConCat.AltCat" to "ConCat.Category".
-- 
-- Maybe move some of the methods with defaults out of the classes, e.g.,
-- "lassocP" and maybe "dup" and "jam".

pair :: forall k a b. (ClosedCat k, Ok2 k a b) => a `k` Exp k b (Prod k a b)
pair :: forall (k :: Type -> Type -> Type) a b.
(ClosedCat k, Ok2 k a b) =>
k a (Exp k b (Prod k a b))
pair = k (a :* b) (a :* b) -> k a (Exp k b (a :* b))
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k (Prod k a b) c -> k a (Exp k b c)
curry k (a :* b) (a :* b)
forall (k :: Type -> Type -> Type) a. (Category k, Ok k a) => k a a
id (Con (Sat (Ok k) (a :* b)) => k a (Exp k b (a :* b)))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> k a (Exp k b (a :* b))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b

{-# RULES
"toCcc' fmap" toCcc' fmap = fmap
 #-}

{--------------------------------------------------------------------
    Automatic uncurrying
--------------------------------------------------------------------}

-- Note: I'm not using yet. I think it needs to go before ccc.
-- Alternatively, generalize from (->) to ClosedCat.

-- | Repeatedly uncurried version of a -> b
class Uncurriable k a b where
  type UncDom a b
  type UncRan a b
  type UncDom a b = a
  type UncRan a b = b
  uncurries :: (a `k` b) -> (UncDom a b `k` UncRan a b)
  -- default uncurries :: (a `k` b) -> (a `k` b)
  default uncurries :: (UncDom a b ~ a, UncRan a b ~ b) =>
                       (a `k` b) -> (UncDom a b `k` UncRan a b)
  -- uncurries = id
  -- uncurries = P.id
  uncurries k a b
f = k a b
k (UncDom a b) (UncRan a b)
f
  -- experiment
  fiddly_foo_unc :: k a b -> ()
  fiddly_foo_unc = () -> k a b -> ()
forall (k :: Type -> Type -> Type) b a.
(ConstCat k b, Ok k a) =>
b -> k a b
const ()
  {-# INLINE uncurries #-}

instance (ClosedCat k, Uncurriable k (a :* b) c, Ok3 k a b c)
      => Uncurriable k a (b -> c) where
  type UncDom a (b -> c) = UncDom (a :* b) c
  type UncRan a (b -> c) = UncRan (a :* b) c
  -- uncurries = uncurries C.. uncurry
  uncurries :: k a (b -> c) -> k (UncDom a (b -> c)) (UncRan a (b -> c))
uncurries = k (a :* b) c -> k (UncDom (a :* b) c) (UncRan (a :* b) c)
forall (k :: Type -> Type -> Type) a b.
Uncurriable k a b =>
k a b -> k (UncDom a b) (UncRan a b)
uncurries (k (a :* b) c -> k (UncDom (a :* b) c) (UncRan (a :* b) c))
-> (k a (b -> c) -> k (a :* b) c)
-> k a (b -> c)
-> k (UncDom (a :* b) c) (UncRan (a :* b) c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. k a (b -> c) -> k (a :* b) c
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp k b c) -> k (Prod k a b) c
uncurry
  -- uncurries f = uncurries (uncurry f)
  {-# INLINE uncurries #-}

--     • The constraint ‘Uncurriable k (a :* b) c’
--         is no smaller than the instance head
--       (Use UndecidableInstances to permit this)

-- I get better inlining and simplification with explicit uncurries
-- definitions and specific INLINE pragmas.

#define UncId(t) \
instance Uncurriable k a (t) where uncurries f = f ; {-# INLINE uncurries #-}

UncId(())
UncId(Bool)
UncId(Int)
UncId(Float)
UncId(Double)
UncId(c :* d)
UncId(c :+ d)

-- | Pseudo function to trigger rewriting to TOCCC form.
toCcc' :: forall k a b. (a -> b) -> (a `k` b)
toCcc' :: forall (k :: Type -> Type -> Type) a b. (a -> b) -> k a b
toCcc' a -> b
_ = String -> k a b
forall b. String -> b
oops String
"toCcc' called"
{-# NOINLINE toCcc' #-}

-- | Internal function, annotated with available dictionaries
toCcc'' :: forall k a b ev . ev -> (a -> b) -> (a `k` b)
toCcc'' :: forall (k :: Type -> Type -> Type) a b ev. ev -> (a -> b) -> k a b
toCcc'' ev
_ = String -> (a -> b) -> k a b
forall b. String -> b
oops String
"toCcc'' called"
{-# NOINLINE toCcc'' #-}

-- | Pseudo function to stop rewriting from TOCCC form.
unCcc' :: forall k a b. (a `k` b) -> (a -> b)
unCcc' :: forall (k :: Type -> Type -> Type) a b. k a b -> a -> b
unCcc' k a b
_ = String -> a -> b
forall b. String -> b
oops String
"unCcc' called"
{-# NOINLINE unCcc' #-}

-- Prevent the plugin from messing with these ones.
{-# ANN toCcc' (PseudoFun 1) #-}
{-# ANN unCcc' (PseudoFun 1) #-}

{-# RULES

"toCcc'/unCcc'" forall f. toCcc' (unCcc' f) = f
"unCcc'/toCcc'" forall f. unCcc' (toCcc' f) = f

 #-}

-- | Pseudo function to trigger rewriting to CCC form, plus a 'reveal' for
-- inlining.
toCcc :: forall k a b. (a -> b) -> (a `k` b)
toCcc :: forall (k :: Type -> Type -> Type) a b. (a -> b) -> k a b
toCcc a -> b
f = k a b -> k a b
forall (k :: Type -> Type -> Type) a b. k a b -> k a b
reveal ((a -> b) -> k a b
forall (k :: Type -> Type -> Type) a b. (a -> b) -> k a b
toCcc' a -> b
f)
-- toCcc f = toCcc' f  -- Try doing without reveal/conceal
{-# INLINE toCcc #-}

-- 2017-09-24
{-# DEPRECATED ccc "ccc is now called toCcc" #-}
ccc :: forall k a b. (a -> b) -> (a `k` b)
ccc :: forall (k :: Type -> Type -> Type) a b. (a -> b) -> k a b
ccc a -> b
f = (a -> b) -> k a b
forall (k :: Type -> Type -> Type) a b. (a -> b) -> k a b
toCcc a -> b
f
{-# INLINE ccc #-}

-- | Pseudo function to stop rewriting from CCC form.
unCcc :: forall k a b. (a `k` b) -> (a -> b)
unCcc :: forall (k :: Type -> Type -> Type) a b. k a b -> a -> b
unCcc k a b
f = k a b -> a -> b
forall (k :: Type -> Type -> Type) a b. k a b -> a -> b
unCcc' (k a b -> k a b
forall (k :: Type -> Type -> Type) a b. k a b -> k a b
conceal k a b
f)
-- unCcc f = unCcc' f  -- Try doing without reveal/conceal
{-# INLINE unCcc #-}

{--------------------------------------------------------------------
    Rewrite rules
--------------------------------------------------------------------}

id2 :: forall k a b. (MonoidalPCat k, Ok2 k a b) => (a :* b) `k` (a :* b)
id2 :: forall (k :: Type -> Type -> Type) a b.
(MonoidalPCat k, Ok2 k a b) =>
k (a :* b) (a :* b)
id2 = k (a :* b) (a :* b)
Con (Sat (Ok k) (a :* b)) => k (a :* b) (a :* b)
forall (k :: Type -> Type -> Type) a. (Category k, Ok k a) => k a a
id (Con (Sat (Ok k) (a :* b)) => k (a :* b) (a :* b))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> k (a :* b) (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b

#if 1
{-# RULES

"g . id" forall g. g . id = g
"id . f" forall f. id . f = f

-- Experiment: systematically right-associate
-- We could go either way, but this choice reduces parentheses.
"(.) assoc right" forall f g h. (h . g) . f = h . (g . f)

"exl . dup" exl . dup = id
"exr . dup" exr . dup = id

"exl/&&&" forall f g. exl . (f &&& g) = f
"exr/&&&" forall f g. exr . (f &&& g) = g

"exl/&&& (b)" forall f g h. exl . (f &&& g) . h = f . h
"exr/&&& (b)" forall f g h. exr . (f &&& g) . h = g . h

-- Unnecessary with right-associating composition
"exl2/&&&" forall f g h. (h . exl) . (f &&& g) = h . f
"exr2/&&&" forall f g h. (h . exr) . (f &&& g) = h . g

"exl3/&&&" forall f g h k. (h . (k . exl)) . (f &&& g) = h . k . f
"exr3/&&&" forall f g h k. (h . (k . exr)) . (f &&& g) = h . k . g

"f . h &&& g . h" forall (f :: a `k` c) (g :: a `k` d) h.
  f . h &&& g . h = (f &&& g) . h <+ okProd @k @c @d

"id &&& id" id &&& id = dup
"id *** id" id *** id = id2

-- -- Specializations with f == id and/or g == id
-- "h &&& h    " forall (h :: a `k` b)               . h &&& h     = (id &&& id) . h <+ okProd @k @b @b
-- "h &&& g . h" forall (g :: b `k` d) (h :: a `k` b). h &&& g . h = (id &&& g ) . h <+ okProd @k @b @d
-- "f . h &&& h" forall (f :: b `k` c) (h :: a `k` b). f . h &&& h = (f  &&& id) . h <+ okProd @k @c @b

-- Oops! the h &&& h rule generates id &&& id, which also matches the rule.

"exl &&& exr" exl &&& exr = id

"(h *** k) . (f &&& g)" forall f g h k. (h *** k) . (f &&& g) = h . f &&& k . g

-- "(f &&& const y) . h" forall y f h. (f &&& const y) . h = f . h &&& const y
-- "(const x &&& g) . h" forall x g h. (const x &&& g) . h = const x &&& g . h

-- "(k . (f &&& const y)) . h" forall y f h k. (k . (f &&& const y)) . h = k . (f . h &&& const y)
-- "(k . (const x &&& g)) . h" forall x g h k. (k . (const x &&& g)) . h = k . (const x &&& g . h)

"uncurry (curry f)" forall f. uncurry (curry f) = f
"curry (uncurry g)" forall g. curry (uncurry g) = g

"constFun 0" forall g f. apply . (curry (g . exr) &&& f) = g . f

"constFun 1" forall f. apply . (curry exr &&& f) = f

"constFun 3" forall f x. apply . (curry (const x) &&& f) = const x

-- Experiment: same rules but via constFun

"constFun' 0" forall g f. apply . (constFun g &&& f) = g . f

-- "foo1" forall (f :: a `k` c) (g :: a `k` d) h.
--   apply . (curry h . f &&& g) = h . (f &&& g) <+ okProd @k @c @d

-- -- The next one leads to a role error when I chain toCcc calls. To investigate.
-- "foo2" forall (g :: a `k` d) h.
--   apply . (curry h &&& g) = h . (id &&& g) <+ okProd @k @a @d

-- "toCcc apply-compose-fork1" forall (f :: a `k` c) (g :: a `k` d) h.
--   apply . (h . f &&& g) = uncurry h . (f &&& g) <+ okProd @k @c @d

-- -- This rule is especially helpful in eliminating uses of apply and curry.
-- "apply-compose-fork2" forall (g :: a `k` d) h.
--   apply . (h &&& g) = uncurry h . (id &&& g) <+ okProd @k @a @d

-- Warning: this rule may be dangerous. Note that `apply == uncurry id`, so if
-- `h == id`, then we aren't making progress.

-- "uncurry . constFun" forall (f :: p -> q). uncurry (constFun f) = f . exr

"curry apply" curry apply = id

-- -- experiment
-- "constFun id" constFun id = curry exr

-- -- This rule helps expose some product rewrites.
-- -- Will we want the opposite for coproducts?
-- "(h . g) . f" forall f g h. (h . g) . f = h . (g . f)

-- "constFun 1" forall f. apply . (curry (f . exr) &&& id) = f

-- "constFun 2" apply . (curry exr &&& id) = id

-- "constFun 3" forall x. apply . (curry (const x) &&& id) = const x

-- "apply . (curry f . exl &&& exr)" forall f .
--   apply . (curry f . exl &&& exr) = f

"second h . (f &&& g)" forall h f g. second h . (f &&& g) = f &&& h . g

"apply . (curry exr &&& f)" forall f.
  apply . (curry exr &&& f) = f

-- "if True"  forall f g. ifC . (const True  *** (f *** g) . dup) . dup = f
-- "if False" forall f g. ifC . (const False *** (f *** g) . dup) . dup = g

#if 0
-- Prelude versions of categorical ops

"toCcc Prelude id" toCcc P.id = toCcc id
"toCcc Prelude (.)" forall g f. toCcc (g P.. f) = toCcc (g . f)

"toCcc Prelude (,)" toCcc (,) = toCcc pair
"toCcc Prelude fst" toCcc fst = toCcc exl
"toCcc Prelude snd" toCcc snd = toCcc exr
"toCcc Prelude swap" toCcc P.swap = toCcc swapP

"toCcc Prelude Left" toCcc Left = toCcc inl
"toCcc Prelude Right" toCcc Right = toCcc inl
"toCcc Prelude either" toCcc either = toCcc (|||)

"toCcc Prelude curry" forall f. toCcc (P.curry f) = toCcc (curry f)
"toCcc Prelude uncurry" forall f.  toCcc (P.uncurry f) = toCcc (uncurry f)

"toCcc Prelude const" forall x. toCcc (P.const x) = toCcc (const x)

#endif

-- Use this one for now.
"toCcc Prelude const" forall x. toCcc (P.const x) = toCcc (\ _ -> x)

#if 0

-- I've commented out the class-ops, since they'll get expanded away early via
-- auto-generated built-in rules.

"toCcc Control.Category id" toCcc A.id = toCcc id
"toCcc Control.Category (.)" forall g f. toCcc (g A.. f) = toCcc (g . f)

"toCcc Arrow (&&&)" forall f g. toCcc (f A.&&& g) = toCcc (f &&& g)
"toCcc Arrow (***)" forall f g. toCcc (f A.*** g) = toCcc (f *** g)
"toCcc Arrow first" forall f. toCcc (A.first f) = toCcc (first f)
"toCcc Arrow second" forall g. toCcc (A.second g) = toCcc (second g)

"toCcc Arrow (|||)" forall f g. toCcc (f A.||| g) = toCcc (f ||| g)
"toCcc Arrow (+++)" forall f g. toCcc (f A.+++ g) = toCcc (f +++ g)
"toCcc Arrow left" forall f. toCcc (A.left f) = toCcc (left f)
"toCcc Arrow right" forall g. toCcc (A.right g) = toCcc (right g)

#endif

"const x . f" forall x f. const x . f = const x

-- ConstCat k a && ConstCat k b doesn't entail that ConstCat k (a :* b). I could
-- require that implication to hold via a superclass constraint of `ConstCat k
-- t` using my `OpCon` entailment technique. However, that constraint may be too
-- onerous for some categories.

-- "const a &&& const b" forall a b . const a &&& const b = const (a,b)

-- -- Leads to a loop involving foo2. To investigate.
-- "uncurry id" uncurry id = apply

-- "curry apply" curry apply = id

"toCcc P.curry" forall f. toCcc (P.curry f) = toCcc (curry f)
"toCcc P.uncurry" forall f. toCcc (P.uncurry f) = toCcc (uncurry f)

-- "uncurry pair" uncurry pair = id

"abstC . reprC" abstC . reprC = id
"reprC . abstC" reprC . abstC = id

-- -- "repair" forall c. (exl c, exr c) = c
-- -- GHC objects to the previous form. The next one passes, but will it fire?
-- -- Don't use. Rely on categorical rules instead.
-- "re-pair" forall c. (,) (exl c) (exr c) = c

-- Applies only to (->):
"f . const x" forall f x. f . const x = const (f x)

-- "coerceC = id" coerceC = id  -- when types match

-- "coerceC . coerceC" coerceC . coerceC = coco

-- "coerceC . coerceC" coerceC . coerceC = snd coco'

 #-}
#endif

idProd :: forall k a b. (Category k, OkProd k, Ok2 k a b) => (a :* b) `k` (a :* b)
idProd :: forall (k :: Type -> Type -> Type) a b.
(Category k, OkProd k, Ok2 k a b) =>
k (a :* b) (a :* b)
idProd = k (a :* b) (a :* b)
Con (Sat (Ok k) (a :* b)) => k (a :* b) (a :* b)
forall (k :: Type -> Type -> Type) a. (Category k, Ok k a) => k a a
id (Con (Sat (Ok k) (a :* b)) => k (a :* b) (a :* b))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> k (a :* b) (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b
{-# INLINE idProd #-}

{-# RULES  

"first id" first id = idProd
"second id" second id = idProd
-- With just id on the RHS: Could not deduce: Ok k (Prod k c b) arising from a use of ‘id’.

"lassocP . rassocP" lassocP . rassocP = id
"lassocP . rassocP . f" forall f. lassocP . rassocP . f = f

"rassocP . lassocP" rassocP . lassocP = id
"rassocP . lassocP . f" forall f. rassocP . lassocP . f = f

"swapP . swapP" swapP . swapP = id

-- TODO: xyzS versions. Or unify MonoidalPCat and MonoidalSCat.

 #-}

#if 0

{-# RULES

-- "arrAt . arr" forall g f. atArr . (array . g &&& f) = atArr g f

--    opt_univ fell into a hole {awmL}

-- Oddly, this alternative works:

"arrAt . arr" forall g f. uncurry at . (array . g &&& f) = atArr g f

-- "at . arr" at . array = id
-- "arr . at" array . at = id

 #-}

-- I may have stumbled onto a hack for writing GHC rewrite rules whose RHSs
-- impose stronger constraints than their LHSs. In the RHS: add an inlining
-- synonym for the identity arrow that introduces the extra constraints. I think
-- the simplifier will inline and eliminate the identity synonym while leaving
-- the constraint behind.

atArr :: forall k i a b. (ClosedCat k, Ok3 k i a b)
      => (a `k` Exp k i b) -> (a `k` i) -> (a `k` b)
atArr g f = apply . (g &&& f)
  <+ okProd @k @(Exp k i b) @i
  <+ okExp @k @i @b

#endif

coco :: forall k a b c. (CoerceCat k a b, CoerceCat k b c, TransitiveCon (CoerceCat k))
     => (a `k` c)
coco :: forall (k :: Type -> Type -> Type) a b c.
(CoerceCat k a b, CoerceCat k b c, TransitiveCon (CoerceCat k)) =>
k a c
coco = k a c
CoerceCat k a c => k a c
forall (k :: Type -> Type -> Type) a b. CoerceCat k a b => k a b
coerceC (CoerceCat k a c => k a c)
-> ((CoerceCat k a b, CoerceCat k b c) :- CoerceCat k a c) -> k a c
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> k -> Constraint) (a :: k) (b :: k)
       (c :: k).
TransitiveCon con =>
(con a b, con b c) :- con a c
forall (con :: Type -> Type -> Constraint) a b c.
TransitiveCon con =>
(con a b, con b c) :- con a c
trans @(CoerceCat k) @a @b @c

-- The problem is that coco gives no way to relate b.

coco' :: forall k a b c. (CoerceCat k a b, CoerceCat k b c, TransitiveCon (CoerceCat k))
      => b :* (a `k` c)
coco' :: forall (k :: Type -> Type -> Type) a b c.
(CoerceCat k a b, CoerceCat k b c, TransitiveCon (CoerceCat k)) =>
b :* k a c
coco' = (b
forall a. HasCallStack => a
undefined, (k a c
CoerceCat k a c => k a c
forall (k :: Type -> Type -> Type) a b. CoerceCat k a b => k a b
coerceC (CoerceCat k a c => k a c)
-> ((CoerceCat k a b, CoerceCat k b c) :- CoerceCat k a c) -> k a c
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (con :: k -> k -> Constraint) (a :: k) (b :: k)
       (c :: k).
TransitiveCon con =>
(con a b, con b c) :- con a c
forall (con :: Type -> Type -> Constraint) a b c.
TransitiveCon con =>
(con a b, con b c) :- con a c
trans @(CoerceCat k) @a @b @c))

-- Experiment

-- -- lassocP' :: Prod k a (Prod k b c) `k` Prod k (Prod k a b) c
-- lassocP' :: (a,(b,c)) `k` ((a,b),c)
-- lassocP' = ccc (\ (a,(b,c)) -> ((a,b),c))

{--------------------------------------------------------------------
    Some orphan instances
--------------------------------------------------------------------}

-- For some (->) instances, we'll want to use late-inlining synonyms

#ifndef VectorSized

deriving instance Functor  (Arr i)
deriving instance Foldable (Arr i)

instance Distributive (Arr i) where
  distribute :: forall f a. Functor f => f (Arr i a) -> Arr i (f a)
  distribute = distributeRep
  {-# INLINE distribute #-}

instance Representable (Arr i) where
  type Rep (Arr i) = i
  tabulate = array
  index = at
  {-# INLINE tabulate #-}
  {-# INLINE index #-}

-- instance Pointed (Arr i) where
--   point = error "point on Arr i: not yet implemented"

instance Zip (Arr i) where
  zipWith = error "zipWith on Arr i: not yet implemented"

-- zeroArr :: Num a => Arr i a
-- zeroArr = error "zeroArr: not yet implemented"

instance Pointed (Arr i) where
  point = error "point on Arr i: not yet implemented"

#endif

-- {-# RULES "ccc (->)" forall f. toCcc' f = f #-}

Op1(fmapC   , (FunctorCat k h, Ok2 k a b) => (a `k` b) -> (h a `k` h b))
Op0(unzipC  , (FunctorCat k h, Ok2 k a b) => h (a :* b) `k` (h a :* h b))
Op0(zipC    , (ZipCat k h    , Ok2 k a b) => (h a :* h b) `k` h (a :* b))
Op0(strength, (Strong k h    , Ok2 k a b) => (a :* h b) `k` h (a :* b))
Op0(pointC  , (PointedCat k h a)          => a `k` h a)
Op0(sumAC   , (AddCat k h a)              => h a `k` a)
Op0(minimumC, (MinMaxFunctorCat k h a, OkFunctor k h, Ok k a) => h a `k` a)
Op0(maximumC, (MinMaxFunctorCat k h a, OkFunctor k h, Ok k a) => h a `k` a)
Op0(minimumCF, (MinMaxFFunctorCat k h a, OkFunctor k h, Ok k a) => h a -> (a :*  (h a `k` a)))
Op0(maximumCF, (MinMaxFFunctorCat k h a, OkFunctor k h, Ok k a) => h a -> (a :*  (h a `k` a)))
  
-- Op0(ixSumAC , (IxSummableCat k n a)       => (a :^ n) `k` a)
-- Op0(sumC  , (SumCat k h a)              => h a `k` a)

Catify(fmap , fmapC)
-- Catify(fmap , fmapIdT)  -- experiment

Catify(unzip, unzipC)
Catify(zip  , curry zipC)
Catify(Pointed.point, pointC)
Catify(ConCatPointed.point, pointC)
Catify(sumA , sumAC)

zipWithC :: Zip h => (a -> b -> c) -> (h a -> h b -> h c)
zipWithC :: forall (h :: Type -> Type) a b c.
Zip h =>
(a -> b -> c) -> h a -> h b -> h c
zipWithC a -> b -> c
f = (Prod (->) (h a) (h b) -> h c) -> h a -> h b -> h c
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k (Prod k a b) c -> k a (Exp k b c)
curry ((Prod (->) a b -> c) -> h (Prod (->) a b) -> h c
forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC ((a -> b -> c) -> Prod (->) a b -> c
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp k b c) -> k (Prod k a b) c
uncurry a -> b -> c
f) (h (Prod (->) a b) -> h c)
-> (Prod (->) (h a) (h b) -> h (Prod (->) a b))
-> Prod (->) (h a) (h b)
-> h c
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Prod (->) (h a) (h b) -> h (Prod (->) a b)
forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b.
(ZipCat k h, Ok2 k a b) =>
k (h a :* h b) (h (a :* b))
zipC)
-- This version inlines too early, thus precenting ghc from
-- seeing curry . uncrry / uncurry . curry
-- zipWithC f = P.curry (fmap (P.uncurry f) . P.uncurry zip)
{-# INLINE zipWithC #-}

-- zipWithC f as bs = fmapC (uncurry f) (zipC (as,bs))

Catify(zipWith, zipWithC)

-- Experiment
Catify(pointNI, pointC)
Catify(zipWithNI, zipWithC)

Catify(ConCatZip.zipWith, zipWithC)
Catify(ConCatZip.zip, curry zipC)

Catify(ConCatMinMax.minimum, minimumC)
Catify(ConCatMinMax.maximum, maximumC)

#if 0
unzipC :: forall k h a b. (FunctorCat k h, TerminalCat k, ClosedCat k, Ok2 k a b)
       => h (a :* b) `k` (h a :* h b)
unzipC = fmapC exl &&& fmapC exr
           <+ okFunctor @k @h @(a :* b)
           <+ okFunctor @k @h @a
           <+ okFunctor @k @h @b
           <+ okProd    @k @a @b
{-# INLINE unzipC #-}
#endif

#if 0
-- See 2017-12-27 notes
zapC :: forall k h a b.
        (FunctorCat k h, ZipCat k h, TerminalCat k, ClosedCat k, Ok2 k a b)
     => (h (a -> b) :* h a) `k` h b
zapC = fmapC apply . zipC
         <+ okFunctor @k @h @((a -> b) :* a)
         <+ okProd    @k    @(h (a -> b)) @(h a)
         <+ okFunctor @k @h @(a -> b)
         <+ okFunctor @k @h @a
         <+ okFunctor @k @h @b
         <+ okProd    @k    @(a -> b) @a
         <+ okExp     @k    @a @b
{-# INLINE zapC #-}

-- TODO: define zapC via zipWithC
#else
Op1(zapC, (ZapCat k h, Ok2 k a b) => h (a `k` b) -> (h a `k` h b))
-- Translation for zap? Maybe like fmap's.
-- Catify(zap, zapC)  -- 2017-12-27 notes
Catify(ConCatZip.zap, zapC)
-- Catify(Aliases.zap, zapC)
#endif

-- TODO: Is there any value to defining utility functions like unzipC and zapC
-- in categorical generality? Maybe define only for functions, but still using
-- the categorical building blocks. Later extend to other categories by
-- translation, at which point the Ok constraints will be checked anyway.

fmapId :: forall k h a. (Category k, FunctorCat k h, Ok k a) => h a `k` h a
fmapId :: forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
(Category k, FunctorCat k h, Ok k a) =>
k (h a) (h a)
fmapId = k (h a) (h a)
Con (Sat (Ok k) (h a)) => k (h a) (h a)
forall (k :: Type -> Type -> Type) a. (Category k, Ok k a) => k a a
id (Con (Sat (Ok k) (h a)) => k (h a) (h a))
-> (Sat (Ok k) a |- Sat (Ok k) (h a)) -> k (h a) (h a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @h @a

{-# RULES
"fmapC id" fmapC id = fmapId
"fmapC compose" forall g f. fmapC g . fmapC f = fmapC (g . f)
 #-}

unzipFmapFork :: forall k h a b c.
                 (MProductCat k, Ok3 k a b c, FunctorCat k h)
              => (a `k` b) -> (a `k` c) -> (h a `k` (h b :* h c))
unzipFmapFork :: forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b c.
(MProductCat k, Ok3 k a b c, FunctorCat k h) =>
k a b -> k a c -> k (h a) (h b :* h c)
unzipFmapFork k a b
f k a c
g = k a b -> k (h a) (h b)
forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC k a b
f k (h a) (h b) -> k (h a) (h c) -> k (h a) (h b :* h c)
forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& k a c -> k (h a) (h c)
forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC k a c
g
  (Con (Sat (Ok k) (h a)) => k (h a) (h b :* h c))
-> (Sat (Ok k) a |- Sat (Ok k) (h a)) -> k (h a) (h b :* h c)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @h @a
  (Con (Sat (Ok k) (h b)) => k (h a) (h b :* h c))
-> (Sat (Ok k) b |- Sat (Ok k) (h b)) -> k (h a) (h b :* h c)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @h @b
  (Con (Sat (Ok k) (h c)) => k (h a) (h b :* h c))
-> (Sat (Ok k) c |- Sat (Ok k) (h c)) -> k (h a) (h b :* h c)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @h @c
{-# INLINE unzipFmapFork #-}

-- constPoint :: forall k h a z.
--       (FunctorCat k h, Pointed h, Ok2 k a z, ConstCat k (h a))
--    => a -> (z `k` h a)
-- constPoint a = const (pointC a <+ okFunctor @k @h @a)

-- constPoint :: forall k h a z. (ConstCat k a, PointedCat k h a, Ok2 k a z)
--            => a -> (z `k` h a)
-- constPoint a = pointC . const a <+ okFunctor @k @h @a

-- foo :: Zip h => (b :* c -> d) -> (a -> b) -> h a -> (h c -> h d)
-- foo g f = curry (fmapC g . zipC) . fmap f

-- zipWithFmap :: forall k h a b c d.
--                (ClosedCat k, FunctorCat k h, ZipCat k h, Ok4 k a b c d)
--             => ((b :* c) `k` d) -> (a `k` b) -> (h a `k` (h c -> h d))
-- zipWithFmap g f = curry (fmapC (uncurry (curry g . f)) . zipC)
--   <+ okFunctor @k @h @(a :* c)
--   <+ okProd @k @(h a) @(h c)
--   <+ okProd @k @a @c
--   <+ okExp  @k @c @d
--   <+ okFunctor @k @h @a
--   <+ okFunctor @k @h @c
--   <+ okFunctor @k @h @d
-- {-# INLINE zipWithFmap #-}

{-# RULES

"unzipC . zipC" unzipC . zipC = id

-- -- Fail. Needs ZipCat on RHS but not LHS.
-- "fmap (f &&& g)" forall f g. fmapC (f &&& g) = zipC . (fmapC f &&& fmapC g)

-- -- Less modular, but uses ZipCat on LHS. Needs Ok constraints on right.
-- "unzipC . fmapC (f &&& g)" forall f g. unzipC . fmapC (f &&& g) = fmapC f &&& fmapC g

-- unzipC . fmapC (f &&& g) = fmapC f &&& fmapC g
-- Use an external definition to get RHS Ok constraints.
-- GHC isn't inlining that definition, so force it.
"unzipC . fmapC (f &&& g)" forall f g.
   unzipC . fmapC (f &&& g) = inline unzipFmapFork f g

-- "fmapC (constFun f)" forall f.
--   fmapC (constFun f) = constFun (pointC f)

-- Do I need to inline constFun, at least on the left?

-- -- *Applying* pointC restricts to functions

-- -- RHS needs PointedCat
-- "fmapC (constFun f)" forall f.
--   fmapC (curry (f . exr)) = pointC . constFun f

-- -- Seems iffy for staging. RHS needs Pointed.
-- "fmapC (constFun f)" forall f. fmapC (constFun f) = const (point f)

-- -- Needs RHS constraints
-- "fmapC (const a)" forall a. fmapC (const a) = const (pointC a)

-- "fmapC (const a)" forall a. fmapC (const a) = constPoint a

-- "zipWith g . fmap f" forall f g .
--   curry (fmapC g . zipC) . fmapC f = fmapC (uncurry (g . f)) . zipC

-- -- 2017-11-05 notes
-- "zipWith g . fmap f" forall f g .
--   -- zipWith g . fmap f = zipWith (g . f)
--   curry (fmapC g . zipC) . fmapC f = inline zipWithFmap g f
--   -- curry (fmapC g . zipC) . fmapC f = curry (fmapC (uncurry (curry g . f)) . zipC)

-- 2017-11-05 notes
"constFun (fmap f)" forall f .
  curry (fmap (f . exr) . zipC) = inline constFun (fmap f)

-- -- 2017-11-06 notes
-- "constFun (fmap f)" forall f .
--   curry (fmapC (f . exr) . zipC) = constFun (fmapC f)

 #-}



#if 0
-- Experiment

idCon :: forall con k a b. con k => (a `k` b) -> (a `k` b)
idCon f = f
{-# INLINE idCon #-}

{-# RULES
"idCon test a" fmapC id = fmapId
"idCon test b" idCon @ProductCat (fmapC id) = fmapId
 #-}

-- Too bad. The idCon appears in the rule's LHS.

#endif

Op0(sequenceAC, (TraversableCat k t f, Ok k a) => t (f a) `k` f (t a))
Op0(distributeC, (DistributiveCat k g f, Ok k a) => f (g a) `k` g (f a))
Op0(tabulateC  , (RepresentableCat k f , Ok k a) => (Rep f -> a) `k` f a)
Op0(indexC     , (RepresentableCat k f , Ok k a) => f a `k` (Rep f -> a))

Catify(sequenceA, sequenceAC)
Catify(distribute, distributeC)
Catify(tabulate  , tabulateC)
Catify(index     , indexC)

traverseC ::
  forall k t f a b.
  ( Category k,
    FunctorCat k t,
    OkFunctor k f,
    TraversableCat k t f,
    Ok k a,
    Ok k b
  ) =>
  a `k` f b ->
  t a `k` f (t b)
traverseC :: forall (k :: Type -> Type -> Type) (t :: Type -> Type)
       (f :: Type -> Type) a b.
(Category k, FunctorCat k t, OkFunctor k f, TraversableCat k t f,
 Ok k a, Ok k b) =>
k a (f b) -> k (t a) (f (t b))
traverseC k a (f b)
f =
  k (t (f b)) (f (t b))
forall (k :: Type -> Type -> Type) (t :: Type -> Type)
       (f :: Type -> Type) a.
(TraversableCat k t f, Ok k a) =>
k (t (f a)) (f (t a))
sequenceAC k (t (f b)) (f (t b)) -> k (t a) (t (f b)) -> k (t a) (f (t b))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a (f b) -> k (t a) (t (f b))
forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC k a (f b)
f
    (Con (Sat (Ok k) (t (f b))) => k (t a) (f (t b)))
-> (Sat (Ok k) (f b) |- Sat (Ok k) (t (f b))) -> k (t a) (f (t b))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @t @(f b)
    (Con (Sat (Ok k) (f (t b))) => k (t a) (f (t b)))
-> (Sat (Ok k) (t b) |- Sat (Ok k) (f (t b))) -> k (t a) (f (t b))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @f @(t b)
    (Con (Sat (Ok k) (t a)) => k (t a) (f (t b)))
-> (Sat (Ok k) a |- Sat (Ok k) (t a)) -> k (t a) (f (t b))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @t @a
    (Con (Sat (Ok k) (t b)) => k (t a) (f (t b)))
-> (Sat (Ok k) b |- Sat (Ok k) (t b)) -> k (t a) (f (t b))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @t @b
    (Con (Sat (Ok k) (f b)) => k (t a) (f (t b)))
-> (Sat (Ok k) b |- Sat (Ok k) (f b)) -> k (t a) (f (t b))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkFunctor k h =>
Ok' k a |- Ok' k (h a)
okFunctor @k @f @b
{-# INLINE traverseC #-}

Catify(traverse, traverseC)

collectC :: (Distributive g, Functor f) => (a -> g b) -> f a -> g (f b)
collectC :: forall (g :: Type -> Type) (f :: Type -> Type) a b.
(Distributive g, Functor f) =>
(a -> g b) -> f a -> g (f b)
collectC a -> g b
f = f (g b) -> g (f b)
forall (g :: Type -> Type) (f :: Type -> Type) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
forall (f :: Type -> Type) a. Functor f => f (g a) -> g (f a)
distribute (f (g b) -> g (f b)) -> (f a -> f (g b)) -> f a -> g (f b)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a -> g b) -> f a -> f (g b)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> g b
f
-- collectC f = distributeC . fmapC f
{-# INLINE collectC #-}

Catify(collect, collectC)

Op0(unFinite     , (FiniteCat k, KnownNat n) => Finite n `k` Int)
Op0(unsafeFinite , (FiniteCat k, KnownNat n) => Int `k` Finite n)

{-# RULES
"unFinite . unsafeFinite" unFinite . unsafeFinite = id
"unsafeFinite . unFinite" unsafeFinite . unFinite = id
 #-}

-- TODO: Maybe move the following utilities to ConCat.TArr or elsewhere. 

combineZero  :: Void -> Finite 0
combineZero :: Void -> Finite 0
combineZero = Void -> Finite 0
forall a. Void -> a
absurd
{-# INLINE combineZero #-}

separateZero :: Finite 0 -> Void
separateZero :: Finite 0 -> Void
separateZero = String -> Finite 0 -> Void
forall a. HasCallStack => String -> a
error String
"no Finite 0"  -- Hm.
{-# INLINE separateZero #-}

combineOne   :: () -> Finite 1
combineOne :: () -> Finite 1
combineOne () = Int -> Finite 1
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k Int (Finite n)
unsafeFinite Int
0
{-# INLINE combineOne #-}

separateOne  :: Finite 1 -> ()
separateOne :: Finite 1 -> ()
separateOne = () -> Finite 1 -> ()
forall (k :: Type -> Type -> Type) b a.
(ConstCat k b, Ok k a) =>
b -> k a b
const ()
{-# INLINE separateOne #-}

type KnownNat2 m n = (KnownNat m, KnownNat n)

combineSum :: forall m n. KnownNat2 m n
           => (Finite m :+ Finite n) -> Finite (m + n)
combineSum :: forall (m :: Nat) (n :: Nat).
KnownNat2 m n =>
(Finite m :+ Finite n) -> Finite (m + n)
combineSum (Left  Finite m
l) = Int -> Finite (m + n)
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k Int (Finite n)
unsafeFinite (Finite m -> Int
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k (Finite n) Int
unFinite Finite m
l)          (KnownNat (m + n) => Finite (m + n))
-> (KnownNat2 m n :- KnownNat (m + n)) -> Finite (m + n)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) :- KnownNat (m + n)
knownAdd @m @n
combineSum (Right Finite n
k) = Int -> Finite (m + n)
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k Int (Finite n)
unsafeFinite (forall (n :: Nat). KnownNat n => Int
int @m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Finite n -> Int
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k (Finite n) Int
unFinite Finite n
k) (KnownNat (m + n) => Finite (m + n))
-> (KnownNat2 m n :- KnownNat (m + n)) -> Finite (m + n)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) :- KnownNat (m + n)
knownAdd @m @n
{-# INLINE combineSum #-}

separateSum :: forall m n. KnownNat2 m n
            => Finite (m + n) -> (Finite m :+ Finite n)
separateSum :: forall (m :: Nat) (n :: Nat).
KnownNat2 m n =>
Finite (m + n) -> Finite m :+ Finite n
separateSum (KnownNat (m + n) => Finite (m + n) -> Int
Finite (m + n) -> Int
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k (Finite n) Int
unFinite (KnownNat (m + n) => Finite (m + n) -> Int)
-> (KnownNat2 m n :- KnownNat (m + n)) -> Finite (m + n) -> Int
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) :- KnownNat (m + n)
knownAdd @m @n -> Int
x)
  | Int
x Int -> Int -> BoolOf k
forall a. Ord a => a -> a -> BoolOf k
< Int
m     = Finite m -> Either (Finite m) (Finite n)
forall a b. a -> Either a b
Left  (Int -> Finite m
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k Int (Finite n)
unsafeFinite Int
x)
  | BoolOf k
otherwise = Finite n -> Either (Finite m) (Finite n)
forall a b. b -> Either a b
Right (Int -> Finite n
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k Int (Finite n)
unsafeFinite (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m))
 where
   m :: Int
m = forall (n :: Nat). KnownNat n => Int
int @m
{-# INLINE separateSum #-}

combineProd :: forall m n. KnownNat2 m n
            => (Finite m :* Finite n) -> Finite (m * n)
combineProd :: forall (m :: Nat) (n :: Nat).
KnownNat2 m n =>
(Finite m :* Finite n) -> Finite (m * n)
combineProd (Finite m -> Int
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k (Finite n) Int
unFinite -> Int
l, Finite n -> Int
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k (Finite n) Int
unFinite -> Int
k) =
  Int -> Finite (m * n)
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k Int (Finite n)
unsafeFinite (forall (n :: Nat). KnownNat n => Int
int @n Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k) (KnownNat (m * n) => Finite (m * n))
-> (KnownNat2 m n :- KnownNat (m * n)) -> Finite (m * n)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) :- KnownNat (m * n)
knownMul @m @n
{-# INLINE combineProd #-}

separateProd :: forall m n. KnownNat2 m n
             => Finite (m * n) -> (Finite m :* Finite n)
separateProd :: forall (m :: Nat) (n :: Nat).
KnownNat2 m n =>
Finite (m * n) -> Finite m :* Finite n
separateProd (KnownNat (m * n) => Finite (m * n) -> Int
Finite (m * n) -> Int
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k (Finite n) Int
unFinite (KnownNat (m * n) => Finite (m * n) -> Int)
-> (KnownNat2 m n :- KnownNat (m * n)) -> Finite (m * n) -> Int
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) :- KnownNat (m * n)
knownMul @m @n -> Int
x) =
  (Int -> Finite m
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k Int (Finite n)
unsafeFinite Int
q, Int -> Finite n
forall (k :: Type -> Type -> Type) (n :: Nat).
(FiniteCat k, KnownNat n) =>
k Int (Finite n)
unsafeFinite Int
r)
 where
   (Int
q,Int
r) = Int
x Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
`divMod` forall (n :: Nat). KnownNat n => Int
int @n
{-# INLINE separateProd #-}

{-# RULES

"fmap id" uncurry fmapC . (curry exr &&& id) = id

 #-}

{-# RULES

"uncurry (,)" uncurry (,) = id

#-}

-- type Strong k h a = (ProductCat k, ZipCat k h, PointedCat k h a)

-- -- Functorial strength
-- strength :: forall k h a b. (Strong k h a, Ok2 k a b)
--          => (a :* h b) `k` h (a :* b)
-- strength = zipC . first pointC
--   <+ okProd @k @(h a) @(h b)
--   <+ okProd @k @a @(h b)
--   <+ okFunctor @k @h @(a :* b)
--   <+ okFunctor @k @h @a
--   <+ okFunctor @k @h @b
--   <+ okProd @k @a @b

-- -- Move to Translators
-- -- Functorial strength
-- strength :: (Zip h, Pointed h) => a :* h b -> h (a :* b)
-- strength = zipC . first pointC


-- TODO: does a (->)-specific strength suffice? Maybe it's used only
-- Translators. If so, define it there, or skip it and use @zipC . first pointC@
-- directly.

-- -- Names are in transition

-- tabulateC :: ArrayCat k n b => Exp k (Finite n) b `k` Arr n b
-- tabulateC = array

-- indexC :: ArrayCat k n b => Arr n b `k` Exp k (Finite n) b
-- indexC = curry arrAt


-- Variant of 'distributeRep' from Data.Functor.Rep
-- TODO: Generalize from Vector.

-- distributeRepC :: ( -- Representable f, Functor w,
--                     f ~ Vector n, KnownNat n, Representable w
--                   )
--                => w (f a) -> f (w a)

-- distributeRepC :: ( -- Representable f, Functor w,
--                     w ~ Vector n, KnownNat n -- , Representable w
--                   )
--                => w (f a) -> f (w a)

-- distributeRepC wf = tabulateC (\k -> fmapC (`indexC` k) wf)

type Diagonal h = (Representable h, Eq (Rep h))

diag :: Diagonal h => a -> a -> h (h a)
diag :: forall (h :: Type -> Type) a. Diagonal h => a -> a -> h (h a)
diag a
z a
o =
  -- tabulateC (\ i -> tabulateC (\ j -> if i == j then o else z))
  -- tabulateC (\ i -> tabulateC (\ j -> if equal (i,j) then o else z))
  (Rep h -> h a) -> h (h a)
forall a. (Rep h -> a) -> h a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (\ Rep h
i -> (Rep h -> a) -> h a
forall a. (Rep h -> a) -> h a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (\ Rep h
j -> if Rep h
i Rep h -> Rep h -> BoolOf k
forall a. Eq a => a -> a -> BoolOf k
== Rep h
j then a
o else a
z))
{-# INLINE diag #-}

-- TODO: retry diag as a single tabulateC on h :.: h.

-- HACK: the equal here is to postpone dealing with equality on sum types just yet.
-- See notes from 2017-10-15.
-- TODO: remove and test, now that we're translating (==) early (via Catify).

{--------------------------------------------------------------------
    
--------------------------------------------------------------------}

unitIf :: forall k. (TerminalCat k, BoolCat k) => IfT k (Unit k)
unitIf :: forall (k :: Type -> Type -> Type).
(TerminalCat k, BoolCat k) =>
IfT k ()
unitIf = IfT k ()
Con (Sat (Ok k) (BoolOf k :* (() :* ()))) => IfT k ()
forall (k :: Type -> Type -> Type) a.
(TerminalCat k, Ok k a) =>
k a ()
it
  (Con (Sat (Ok k) (BoolOf k :* (() :* ()))) => IfT k ())
-> ((Sat (Ok k) (BoolOf k) && Sat (Ok k) (() :* ()))
    |- Sat (Ok k) (BoolOf k :* (() :* ())))
-> IfT k ()
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @Bool @(() :* ())
  (Con (Sat (Ok k) (() :* ())) => IfT k ())
-> ((Sat (Ok k) () && Sat (Ok k) ()) |- Sat (Ok k) (() :* ()))
-> IfT k ()
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @() @()

-- okIf :: forall k a. BoolCat k => Ok' k a |- Ok' k (Prod k (BoolOf k) (Prod k a a)) && Ok' k (Prod k a a)
-- okIf = inOpR' @(Prod k) @(Ok' k) @(BoolOf k) @a @a . Entail (Sub Dict)

-- okIf :: forall k a. BoolCat k => Ok' k a |- Ok' k (Bool :* (a :* a)) && Ok' k (a :* a)
-- okIf = inOpR' @(Prod k) @(Ok' k) @(BoolOf k) @a @a . Entail (Sub Dict)

prodIf :: forall k a b. (MonoidalPCat k, IfCat k a, IfCat k b) => IfT k (a :* b)
prodIf :: forall (k :: Type -> Type -> Type) a b.
(MonoidalPCat k, IfCat k a, IfCat k b) =>
IfT k (a :* b)
prodIf = (k (BoolOf k :* (a :* a)) a
forall (k :: Type -> Type -> Type) a.
IfCat k a =>
k (Prod k (BoolOf k) (Prod k a a)) a
ifC k (BoolOf k :* (a :* a)) a
-> k (BoolOf k :* ((a :* b) :* (a :* b))) (BoolOf k :* (a :* a))
-> k (BoolOf k :* ((a :* b) :* (a :* b))) a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k ((a :* b) :* (a :* b)) (a :* a)
-> k (BoolOf k :* ((a :* b) :* (a :* b))) (BoolOf k :* (a :* a))
forall (k :: Type -> Type -> Type) a b d.
(MonoidalPCat k, Ok3 k a b d) =>
k b d -> k (Prod k a b) (Prod k a d)
second (k (a :* b) a -> k ((a :* b) :* (a :* b)) (a :* a)
forall (k :: Type -> Type -> Type) a c.
(MonoidalPCat k, Ok2 k a c) =>
k a c -> k (Prod k a a) (Prod k c c)
twiceP k (a :* b) a
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl)) k (BoolOf k :* ((a :* b) :* (a :* b))) a
-> k (BoolOf k :* ((a :* b) :* (a :* b))) b -> IfT k (a :* b)
forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& (k (BoolOf k :* (b :* b)) b
forall (k :: Type -> Type -> Type) a.
IfCat k a =>
k (Prod k (BoolOf k) (Prod k a a)) a
ifC k (BoolOf k :* (b :* b)) b
-> k (BoolOf k :* ((a :* b) :* (a :* b))) (BoolOf k :* (b :* b))
-> k (BoolOf k :* ((a :* b) :* (a :* b))) b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k ((a :* b) :* (a :* b)) (b :* b)
-> k (BoolOf k :* ((a :* b) :* (a :* b))) (BoolOf k :* (b :* b))
forall (k :: Type -> Type -> Type) a b d.
(MonoidalPCat k, Ok3 k a b d) =>
k b d -> k (Prod k a b) (Prod k a d)
second (k (a :* b) b -> k ((a :* b) :* (a :* b)) (b :* b)
forall (k :: Type -> Type -> Type) a c.
(MonoidalPCat k, Ok2 k a c) =>
k a c -> k (Prod k a a) (Prod k c c)
twiceP k (a :* b) b
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr))
  (Con (Sat (Ok k) (BoolOf k :* ((a :* b) :* (a :* b)))) =>
 IfT k (a :* b))
-> ((Sat (Ok k) (BoolOf k) && Sat (Ok k) ((a :* b) :* (a :* b)))
    |- Sat (Ok k) (BoolOf k :* ((a :* b) :* (a :* b))))
-> IfT k (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @Bool @((a :* b) :* (a :* b))
  (Con (Sat (Ok k) ((a :* b) :* (a :* b))) => IfT k (a :* b))
-> ((Sat (Ok k) (a :* b) && Sat (Ok k) (a :* b))
    |- Sat (Ok k) ((a :* b) :* (a :* b)))
-> IfT k (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a :* b) @(a :* b)
  (Con (Sat (Ok k) (BoolOf k :* (b :* b))) => IfT k (a :* b))
-> ((Sat (Ok k) (BoolOf k) && Sat (Ok k) (b :* b))
    |- Sat (Ok k) (BoolOf k :* (b :* b)))
-> IfT k (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @Bool @(b :* b)
  (Con (Sat (Ok k) (BoolOf k :* (a :* a))) => IfT k (a :* b))
-> ((Sat (Ok k) (BoolOf k) && Sat (Ok k) (a :* a))
    |- Sat (Ok k) (BoolOf k :* (a :* a)))
-> IfT k (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @Bool @(a :* a)
  (Con (Sat (Ok k) (b :* b)) => IfT k (a :* b))
-> ((Sat (Ok k) b && Sat (Ok k) b) |- Sat (Ok k) (b :* b))
-> IfT k (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b @b
  (Con (Sat (Ok k) (a :* b)) => IfT k (a :* b))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> IfT k (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b
  (Con (Sat (Ok k) (a :* a)) => IfT k (a :* b))
-> ((Sat (Ok k) a && Sat (Ok k) a) |- Sat (Ok k) (a :* a))
-> IfT k (a :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @a

#if 0

   prodIf
== \ (c,((a,b),(a',b'))) -> (ifC (c,(a,a')), ifC (c,(b,b')))
== (\ (c,((a,b),(a',b'))) -> ifC (c,(a,a'))) &&& ...
== (ifC . (\ (c,((a,b),(a',b'))) -> (c,(a,a')))) &&& ...
== (ifC . second (\ ((a,b),(a',b')) -> (a,a'))) &&& ...
== (ifC . second (twiceP exl)) &&& (ifC . second (twiceP exr))

#endif

funIf :: forall k a b. (MonoidalPCat k, ClosedCat k, Ok k a, IfCat k b) => IfT k (a -> b)
funIf :: forall (k :: Type -> Type -> Type) a b.
(MonoidalPCat k, ClosedCat k, Ok k a, IfCat k b) =>
IfT k (a -> b)
funIf = k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) b -> IfT k (a -> b)
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k (Prod k a b) c -> k a (Exp k b c)
curry (k (BoolOf k :* (b :* b)) b
forall (k :: Type -> Type -> Type) a.
IfCat k a =>
k (Prod k (BoolOf k) (Prod k a a)) a
ifC k (BoolOf k :* (b :* b)) b
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a)
     (BoolOf k :* (b :* b))
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (k (BoolOf k :* ((a -> b) :* (a -> b))) (BoolOf k)
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl k (BoolOf k :* ((a -> b) :* (a -> b))) (BoolOf k)
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a)
     (BoolOf k :* ((a -> b) :* (a -> b)))
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) (BoolOf k)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a)
  (BoolOf k :* ((a -> b) :* (a -> b)))
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) (BoolOf k)
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) (b :* b)
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a)
     (BoolOf k :* (b :* b))
forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& (k ((a -> b) :* a) b
forall (k :: Type -> Type -> Type) a b.
(ClosedCat k, Ok2 k a b) =>
k (Prod k (Exp k a b) a) b
apply k ((a -> b) :* a) b
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) ((a -> b) :* a)
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. IfT k (a -> b)
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) ((a -> b) :* a)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first (k ((a -> b) :* (a -> b)) (a -> b)
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl k ((a -> b) :* (a -> b)) (a -> b)
-> k (BoolOf k :* ((a -> b) :* (a -> b))) ((a -> b) :* (a -> b))
-> IfT k (a -> b)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k (BoolOf k :* ((a -> b) :* (a -> b))) ((a -> b) :* (a -> b))
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr) k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) b
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) b
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) (b :* b)
forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& k ((a -> b) :* a) b
forall (k :: Type -> Type -> Type) a b.
(ClosedCat k, Ok2 k a b) =>
k (Prod k (Exp k a b) a) b
apply k ((a -> b) :* a) b
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) ((a -> b) :* a)
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. IfT k (a -> b)
-> k ((BoolOf k :* ((a -> b) :* (a -> b))) :* a) ((a -> b) :* a)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first (k ((a -> b) :* (a -> b)) (a -> b)
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr k ((a -> b) :* (a -> b)) (a -> b)
-> k (BoolOf k :* ((a -> b) :* (a -> b))) ((a -> b) :* (a -> b))
-> IfT k (a -> b)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k (BoolOf k :* ((a -> b) :* (a -> b))) ((a -> b) :* (a -> b))
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr))))
  (Con (Sat (Ok k) ((BoolOf k :* ((a -> b) :* (a -> b))) :* a)) =>
 IfT k (a -> b))
-> ((Sat (Ok k) (BoolOf k :* ((a -> b) :* (a -> b)))
     && Sat (Ok k) a)
    |- Sat (Ok k) ((BoolOf k :* ((a -> b) :* (a -> b))) :* a))
-> IfT k (a -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(Bool :* ((a -> b) :* (a -> b))) @a
  (Con (Sat (Ok k) (BoolOf k :* ((a -> b) :* (a -> b)))) =>
 IfT k (a -> b))
-> ((Sat (Ok k) (BoolOf k) && Sat (Ok k) ((a -> b) :* (a -> b)))
    |- Sat (Ok k) (BoolOf k :* ((a -> b) :* (a -> b))))
-> IfT k (a -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @Bool @((a -> b) :* (a -> b))
  (Con (Sat (Ok k) (BoolOf k :* (b :* b))) => IfT k (a -> b))
-> ((Sat (Ok k) (BoolOf k) && Sat (Ok k) (b :* b))
    |- Sat (Ok k) (BoolOf k :* (b :* b)))
-> IfT k (a -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @Bool @(b :* b)
  (Con (Sat (Ok k) ((a -> b) :* (a -> b))) => IfT k (a -> b))
-> ((Sat (Ok k) (a -> b) && Sat (Ok k) (a -> b))
    |- Sat (Ok k) ((a -> b) :* (a -> b)))
-> IfT k (a -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a -> b) @(a -> b)
  (Con (Sat (Ok k) ((a -> b) :* a)) => IfT k (a -> b))
-> ((Sat (Ok k) (a -> b) && Sat (Ok k) a)
    |- Sat (Ok k) ((a -> b) :* a))
-> IfT k (a -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a -> b) @a
  (Con (Sat (Ok k) (a -> b)) => IfT k (a -> b))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a -> b))
-> IfT k (a -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkExp k =>
(Ok' k a && Ok' k b) |- Ok' k (Exp k a b)
okExp @k @a @b
  (Con (Sat (Ok k) (b :* b)) => IfT k (a -> b))
-> ((Sat (Ok k) b && Sat (Ok k) b) |- Sat (Ok k) (b :* b))
-> IfT k (a -> b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b @b

           -- <+ okProd @k @(Prod k (BoolOf k) (Prod k (Exp k a b) (Exp k a b))) @a
           -- <+ okIf @k @(Exp k a b)
           -- <+ okProd @k @(Exp k a b) @a
           -- <+ okExp @k @a @b
           -- <+ okIf @k @b

#if 0

   funIf
== \ (c,(f,f')) -> \ a -> ifC (c,(f a,f' a))
== curry (\ ((c,(f,f')),a) -> ifC (c,(f a,f' a)))
== curry (ifC . \ ((c,(f,f')),a) -> (c,(f a,f' a)))
== curry (ifC . (exl.exl &&& \ ((c,(f,f')),a) -> (f a,f' a)))
== curry (ifC . (exl.exl &&& ((\ ((c,(f,f')),a) -> f a) &&& (\ ((c,(f,f')),a) -> f' a))))
== curry (ifC . (exl.exl &&& (apply (first (exl.exr)) &&& (apply (first (exl.exr))))))

#endif

repIf :: forall k a r. (RepCat k a r, MProductCat k, Ok k a, IfCat k r)
      => IfT k a
repIf :: forall (k :: Type -> Type -> Type) a r.
(RepCat k a r, MProductCat k, Ok k a, IfCat k r) =>
IfT k a
repIf = forall (k :: Type -> Type -> Type) a r. RepCat k a r => k r a
abstC @k @a @r k r a -> k (BoolOf k :* (a :* a)) r -> IfT k a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k (BoolOf k :* (r :* r)) r
forall (k :: Type -> Type -> Type) a.
IfCat k a =>
k (Prod k (BoolOf k) (Prod k a a)) a
ifC k (BoolOf k :* (r :* r)) r
-> k (BoolOf k :* (a :* a)) (BoolOf k :* (r :* r))
-> k (BoolOf k :* (a :* a)) r
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k (a :* a) (r :* r)
-> k (BoolOf k :* (a :* a)) (BoolOf k :* (r :* r))
forall (k :: Type -> Type -> Type) a b d.
(MonoidalPCat k, Ok3 k a b d) =>
k b d -> k (Prod k a b) (Prod k a d)
second (k a r -> k (a :* a) (r :* r)
forall (k :: Type -> Type -> Type) a c.
(MonoidalPCat k, Ok2 k a c) =>
k a c -> k (Prod k a a) (Prod k c c)
twiceP k a r
forall (k :: Type -> Type -> Type) a r. RepCat k a r => k a r
reprC)
        (Con (Sat (Ok k) (BoolOf k :* (r :* r))) => IfT k a)
-> ((Sat (Ok k) (BoolOf k) && Sat (Ok k) (r :* r))
    |- Sat (Ok k) (BoolOf k :* (r :* r)))
-> IfT k a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(BoolOf k) @(Prod k r r)
        (Con (Sat (Ok k) (r :* r)) => IfT k a)
-> ((Sat (Ok k) r && Sat (Ok k) r) |- Sat (Ok k) (r :* r))
-> IfT k a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @r @r
        (Con (Sat (Ok k) (BoolOf k :* (a :* a))) => IfT k a)
-> ((Sat (Ok k) (BoolOf k) && Sat (Ok k) (a :* a))
    |- Sat (Ok k) (BoolOf k :* (a :* a)))
-> IfT k a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(BoolOf k) @(Prod k a a)
        (Con (Sat (Ok k) (a :* a)) => IfT k a)
-> ((Sat (Ok k) a && Sat (Ok k) a) |- Sat (Ok k) (a :* a))
-> IfT k a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @a

#if 0
   repIf
== \ (c,(a,a')) -> abstC (ifC (c,(reprC a,reprC a')))
== \ (c,(a,a')) -> abstC (ifC (c,(twiceP reprC (a,a'))))
== \ (c,(a,a')) -> abstC (ifC (second (twiceP reprC) (c,((a,a')))))
== abstC . ifC . second (twiceP reprC)
#endif

{--------------------------------------------------------------------
    Misc utilities
--------------------------------------------------------------------}

-- TODO: Finish moving utilities from Category to here

transposeP :: forall k a b c d. (MProductCat k, Ok4 k a b c d)
           => Prod k (Prod k a b) (Prod k c d) `k` Prod k (Prod k a c) (Prod k b d)
transposeP :: forall (k :: Type -> Type -> Type) a b c d.
(MProductCat k, Ok4 k a b c d) =>
k (Prod k (Prod k a b) (Prod k c d))
  (Prod k (Prod k a c) (Prod k b d))
transposeP = (k (Prod k a b) a
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exlk (Prod k a b) a
-> k (Prod k (Prod k a b) (Prod k c d)) (Prod k a b)
-> k (Prod k (Prod k a b) (Prod k c d)) a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.k (Prod k (Prod k a b) (Prod k c d)) (Prod k a b)
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl k (Prod k (Prod k a b) (Prod k c d)) a
-> k (Prod k (Prod k a b) (Prod k c d)) c
-> k (Prod k (Prod k a b) (Prod k c d)) (a :* c)
forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& k (Prod k c d) c
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exlk (Prod k c d) c
-> k (Prod k (Prod k a b) (Prod k c d)) (Prod k c d)
-> k (Prod k (Prod k a b) (Prod k c d)) c
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.k (Prod k (Prod k a b) (Prod k c d)) (Prod k c d)
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr) k (Prod k (Prod k a b) (Prod k c d)) (a :* c)
-> k (Prod k (Prod k a b) (Prod k c d)) (Prod k b d)
-> k (Prod k (Prod k a b) (Prod k c d))
     (Prod k (a :* c) (Prod k b d))
forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& (k (Prod k a b) b
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exrk (Prod k a b) b
-> k (Prod k (Prod k a b) (Prod k c d)) (Prod k a b)
-> k (Prod k (Prod k a b) (Prod k c d)) b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.k (Prod k (Prod k a b) (Prod k c d)) (Prod k a b)
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl k (Prod k (Prod k a b) (Prod k c d)) b
-> k (Prod k (Prod k a b) (Prod k c d)) d
-> k (Prod k (Prod k a b) (Prod k c d)) (Prod k b d)
forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& k (Prod k c d) d
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exrk (Prod k c d) d
-> k (Prod k (Prod k a b) (Prod k c d)) (Prod k c d)
-> k (Prod k (Prod k a b) (Prod k c d)) d
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.k (Prod k (Prod k a b) (Prod k c d)) (Prod k c d)
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr)
  (Con (Sat (Ok k) (Prod k (Prod k a b) (Prod k c d))) =>
 k (Prod k (Prod k a b) (Prod k c d))
   (Prod k (a :* c) (Prod k b d)))
-> ((Sat (Ok k) (Prod k a b) && Sat (Ok k) (Prod k c d))
    |- Sat (Ok k) (Prod k (Prod k a b) (Prod k c d)))
-> k (Prod k (Prod k a b) (Prod k c d))
     (Prod k (a :* c) (Prod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(Prod k a b) @(Prod k c d)
  (Con (Sat (Ok k) (Prod k c d)) =>
 k (Prod k (Prod k a b) (Prod k c d))
   (Prod k (a :* c) (Prod k b d)))
-> ((Sat (Ok k) c && Sat (Ok k) d) |- Sat (Ok k) (Prod k c d))
-> k (Prod k (Prod k a b) (Prod k c d))
     (Prod k (a :* c) (Prod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @c @d
  (Con (Sat (Ok k) (Prod k a b)) =>
 k (Prod k (Prod k a b) (Prod k c d))
   (Prod k (a :* c) (Prod k b d)))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (Prod k a b))
-> k (Prod k (Prod k a b) (Prod k c d))
     (Prod k (a :* c) (Prod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b
  (Con (Sat (Ok k) (Prod k b d)) =>
 k (Prod k (Prod k a b) (Prod k c d))
   (Prod k (a :* c) (Prod k b d)))
-> ((Sat (Ok k) b && Sat (Ok k) d) |- Sat (Ok k) (Prod k b d))
-> k (Prod k (Prod k a b) (Prod k c d))
     (Prod k (a :* c) (Prod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b @d
  (Con (Sat (Ok k) (a :* c)) =>
 k (Prod k (Prod k a b) (Prod k c d))
   (Prod k (a :* c) (Prod k b d)))
-> ((Sat (Ok k) a && Sat (Ok k) c) |- Sat (Ok k) (a :* c))
-> k (Prod k (Prod k a b) (Prod k c d))
     (Prod k (a :* c) (Prod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @c
{-# INLINE transposeP #-}

-- TODO: define transposeP without MonoidalPCat.

-- (a :* b) :* (c :* d) -> (a :* c) -> (b :* d)

-- (a :* b) :* (c :* d)
-- ((a :* b) :* c) :* d
-- (a :* (b :* c)) :* d
-- (a :* (c :* b)) :* d
-- ((a :* c) :* b) :* d
-- (a :* c) :* (b :* d)

-- | Convenient alias for @uncurry '(&&&)'@
fork :: forall k a c d. (MProductCat k, Ok3 k a c d) 
     => (a `k` c) :* (a `k` d) -> (a `k` Prod k c d)
fork :: forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
(k a c :* k a d) -> k a (Prod k c d)
fork = (k a c -> Exp (->) (k a d) (k a (c :* d)))
-> (k a c, k a d) -> k a (c :* d)
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp k b c) -> k (Prod k a b) c
uncurry k a c -> Exp (->) (k a d) (k a (c :* d))
forall (k :: Type -> Type -> Type) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
(&&&)
{-# INLINE fork #-}

-- | Inverse to @uncurry '(&&&)'@
unfork :: forall k a c d. (ProductCat k, Ok3 k a c d) 
       => (a `k` Prod k c d) -> (a `k` c) :* (a `k` d)
unfork :: forall (k :: Type -> Type -> Type) a c d.
(ProductCat k, Ok3 k a c d) =>
k a (Prod k c d) -> k a c :* k a d
unfork k a (Prod k c d)
f = (k (Prod k c d) c
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl k (Prod k c d) c -> k a (Prod k c d) -> k a c
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a (Prod k c d)
f, k (Prod k c d) d
forall (k :: Type -> Type -> Type) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr k (Prod k c d) d -> k a (Prod k c d) -> k a d
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a (Prod k c d)
f)  (Con (Sat (Ok k) (Prod k c d)) => (k a c, k a d))
-> ((Sat (Ok k) c && Sat (Ok k) d) |- Sat (Ok k) (Prod k c d))
-> (k a c, k a d)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @c @d
{-# INLINE unfork #-}

-- | Convenient alias for @uncurry '(|||)'@
join :: forall k a c d. (MCoproductCat k, Ok3 k a c d) 
     => (c `k` a) :* (d `k` a) -> (Coprod k c d `k` a)
join :: forall (k :: Type -> Type -> Type) a c d.
(MCoproductCat k, Ok3 k a c d) =>
(k c a :* k d a) -> k (Coprod k c d) a
join = (k c a -> Exp (->) (k d a) (k (c :+ d) a))
-> (k c a, k d a) -> k (c :+ d) a
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp k b c) -> k (Prod k a b) c
uncurry k c a -> Exp (->) (k d a) (k (c :+ d) a)
forall (k :: Type -> Type -> Type) a c d.
(MCoproductCat k, Ok3 k a c d) =>
k c a -> k d a -> k (Coprod k c d) a
(|||)
{-# INLINE join #-}

-- | Inverse to @uncurry '(|||)'@
unjoin :: forall k a c d. (CoproductCat k, Ok3 k a c d)
       => (Coprod k c d `k` a) -> (c `k` a) :* (d `k` a)
unjoin :: forall (k :: Type -> Type -> Type) a c d.
(CoproductCat k, Ok3 k a c d) =>
k (Coprod k c d) a -> k c a :* k d a
unjoin k (Coprod k c d) a
f = (k (Coprod k c d) a
f k (Coprod k c d) a -> k c (Coprod k c d) -> k c a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k c (Coprod k c d)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k a (Coprod k a b)
inl, k (Coprod k c d) a
f k (Coprod k c d) a -> k d (Coprod k c d) -> k d a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k d (Coprod k c d)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k b (Coprod k a b)
inr) (Con (Sat (Ok k) (Coprod k c d)) => (k c a, k d a))
-> ((Sat (Ok k) c && Sat (Ok k) d) |- Sat (Ok k) (Coprod k c d))
-> (k c a, k d a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @c @d
{-# INLINE unjoin #-}

-- | Convenient alias for @uncurry '(||||)'@
joinP :: forall k a c d. (MCoproductPCat k, Ok3 k a c d, Additive a)
     => (c `k` a) :* (d `k` a) -> (Prod k c d `k` a)
joinP :: forall (k :: Type -> Type -> Type) a c d.
(MCoproductPCat k, Ok3 k a c d, Additive a) =>
(k c a :* k d a) -> k (Prod k c d) a
joinP = (k c a -> Exp (->) (k d a) (k (c :* d) a))
-> (k c a, k d a) -> k (c :* d) a
forall (k :: Type -> Type -> Type) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp k b c) -> k (Prod k a b) c
uncurry k c a -> Exp (->) (k d a) (k (c :* d) a)
forall (k :: Type -> Type -> Type) a c d.
(MCoproductPCat k, Ok3 k a c d) =>
k c a -> k d a -> k (CoprodP k c d) a
(||||)
{-# INLINE joinP #-}

-- | Inverse to @uncurry '(||||)'@
unjoinP :: forall k a c d. (MCoproductPCat k, C3 Additive a c d, Ok3 k a c d)
        => ((c :* d) `k` a) -> (c `k` a) :* (d `k` a)
unjoinP :: forall (k :: Type -> Type -> Type) a c d.
(MCoproductPCat k, C3 Additive a c d, Ok3 k a c d) =>
k (c :* d) a -> k c a :* k d a
unjoinP k (c :* d) a
cda = (k (c :* d) a
cda k (c :* d) a -> k c (c :* d) -> k c a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k c (c :* d)
forall (k :: Type -> Type -> Type) a b.
(CoproductPCat k, Ok2 k a b) =>
k a (CoprodP k a b)
inlP, k (c :* d) a
cda k (c :* d) a -> k d (c :* d) -> k d a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k d (c :* d)
forall (k :: Type -> Type -> Type) a b.
(CoproductPCat k, Ok2 k a b) =>
k b (CoprodP k a b)
inrP)
            (Con (Sat (Ok k) (c :* d)) => (k c a, k d a))
-> ((Sat (Ok k) c && Sat (Ok k) d) |- Sat (Ok k) (c :* d))
-> (k c a, k d a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @c @d
{-# INLINE unjoinP #-}

-- Warning: unjoinP probably increases computation, as it turns one cda use into
-- two uses with sparser arguments. It seems very similar to sampling a linear
-- function on a basis.

-- | Inverse to 'joinPF'
unjoinPF :: forall k h a b. (IxCoproductPCat k h, Functor h, Ok2 k a b)
         => (h b `k` a) -> h (b `k` a)
unjoinPF :: forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b.
(IxCoproductPCat k h, Functor h, Ok2 k a b) =>
k (h b) a -> h (k b a)
unjoinPF k (h b) a
hba = (k b (h b) -> k b a) -> h (k b (h b)) -> h (k b a)
forall a b. (a -> b) -> h a -> h b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (k (h b) a
hba k (h b) a -> k b (h b) -> k b a
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.) h (k b (h b))
forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
(IxCoproductPCat k h, Ok k a) =>
h (k a (h a))
inPF  (Con (Sat (Ok k) (h b)) => h (k b a))
-> (Sat (Ok k) b |- Sat (Ok k) (h b)) -> h (k b a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
okIxProd @k @h @b
{-# INLINE unjoinPF #-}

-- | Inverse to 'forkF'
unforkF :: forall k h a b. (IxProductCat k h, Functor h, Ok2 k a b) 
        => (a `k` h b) -> h (a `k` b)
unforkF :: forall (k :: Type -> Type -> Type) (h :: Type -> Type) a b.
(IxProductCat k h, Functor h, Ok2 k a b) =>
k a (h b) -> h (k a b)
unforkF k a (h b)
ahb = (k (h b) b -> k a b) -> h (k (h b) b) -> h (k a b)
forall a b. (a -> b) -> h a -> h b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (k (h b) b -> k a (h b) -> k a b
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a (h b)
ahb) h (k (h b) b)
forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
(IxProductCat k h, Ok k a) =>
h (k (h a) a)
exF  (Con (Sat (Ok k) (h b)) => h (k a b))
-> (Sat (Ok k) b |- Sat (Ok k) (h b)) -> h (k a b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) (h :: Type -> Type) a.
OkIxProd k h =>
Ok' k a |- Ok' k (h a)
okIxProd @k @h @b
{-# INLINE unforkF #-}

-- | Inverse to 'distl': @(a * u) + (a * v) --> a * (u + v)@
undistl :: forall k a u v. (MonoidalPCat k, MCoproductCat k, Ok3 k a u v)
        => ((a :* u) :+ (a :* v)) `k` (a :* (u :+ v))
undistl :: forall (k :: Type -> Type -> Type) a u v.
(MonoidalPCat k, MCoproductCat k, Ok3 k a u v) =>
k ((a :* u) :+ (a :* v)) (a :* (u :+ v))
undistl = k u (u :+ v) -> k (a :* u) (a :* (u :+ v))
forall (k :: Type -> Type -> Type) a b d.
(MonoidalPCat k, Ok3 k a b d) =>
k b d -> k (Prod k a b) (Prod k a d)
second k u (u :+ v)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k a (Coprod k a b)
inl k (a :* u) (a :* (u :+ v))
-> k (a :* v) (a :* (u :+ v))
-> k ((a :* u) :+ (a :* v)) (a :* (u :+ v))
forall (k :: Type -> Type -> Type) a c d.
(MCoproductCat k, Ok3 k a c d) =>
k c a -> k d a -> k (Coprod k c d) a
||| k v (u :+ v) -> k (a :* v) (a :* (u :+ v))
forall (k :: Type -> Type -> Type) a b d.
(MonoidalPCat k, Ok3 k a b d) =>
k b d -> k (Prod k a b) (Prod k a d)
second k v (u :+ v)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k b (Coprod k a b)
inr
  (Con (Sat (Ok k) (a :* (u :+ v))) =>
 k ((a :* u) :+ (a :* v)) (a :* (u :+ v)))
-> ((Sat (Ok k) a && Sat (Ok k) (u :+ v))
    |- Sat (Ok k) (a :* (u :+ v)))
-> k ((a :* u) :+ (a :* v)) (a :* (u :+ v))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @(u :+ v)
  (Con (Sat (Ok k) (u :+ v)) =>
 k ((a :* u) :+ (a :* v)) (a :* (u :+ v)))
-> ((Sat (Ok k) u && Sat (Ok k) v) |- Sat (Ok k) (u :+ v))
-> k ((a :* u) :+ (a :* v)) (a :* (u :+ v))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @u @v
  (Con (Sat (Ok k) (a :* u)) =>
 k ((a :* u) :+ (a :* v)) (a :* (u :+ v)))
-> ((Sat (Ok k) a && Sat (Ok k) u) |- Sat (Ok k) (a :* u))
-> k ((a :* u) :+ (a :* v)) (a :* (u :+ v))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @u (Con (Sat (Ok k) (a :* v)) =>
 k ((a :* u) :+ (a :* v)) (a :* (u :+ v)))
-> ((Sat (Ok k) a && Sat (Ok k) v) |- Sat (Ok k) (a :* v))
-> k ((a :* u) :+ (a :* v)) (a :* (u :+ v))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @v
{-# INLINE undistl #-}

-- | Inverse to 'distr': @(u * b) + (v * b) --> (u + v) * b@
undistr :: forall k u v b. (MonoidalPCat k, MCoproductCat k, Ok3 k u v b)
        => ((u :* b) :+ (v :* b)) `k` ((u :+ v) :* b)
undistr :: forall (k :: Type -> Type -> Type) u v b.
(MonoidalPCat k, MCoproductCat k, Ok3 k u v b) =>
k ((u :* b) :+ (v :* b)) ((u :+ v) :* b)
undistr = k u (u :+ v) -> k (u :* b) ((u :+ v) :* b)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first k u (u :+ v)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k a (Coprod k a b)
inl k (u :* b) ((u :+ v) :* b)
-> k (v :* b) ((u :+ v) :* b)
-> k ((u :* b) :+ (v :* b)) ((u :+ v) :* b)
forall (k :: Type -> Type -> Type) a c d.
(MCoproductCat k, Ok3 k a c d) =>
k c a -> k d a -> k (Coprod k c d) a
||| k v (u :+ v) -> k (v :* b) ((u :+ v) :* b)
forall (k :: Type -> Type -> Type) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first k v (u :+ v)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k b (Coprod k a b)
inr
  (Con (Sat (Ok k) ((u :+ v) :* b)) =>
 k ((u :* b) :+ (v :* b)) ((u :+ v) :* b))
-> ((Sat (Ok k) (u :+ v) && Sat (Ok k) b)
    |- Sat (Ok k) ((u :+ v) :* b))
-> k ((u :* b) :+ (v :* b)) ((u :+ v) :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(u :+ v) @b
  (Con (Sat (Ok k) (u :+ v)) =>
 k ((u :* b) :+ (v :* b)) ((u :+ v) :* b))
-> ((Sat (Ok k) u && Sat (Ok k) v) |- Sat (Ok k) (u :+ v))
-> k ((u :* b) :+ (v :* b)) ((u :+ v) :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @u @v
  (Con (Sat (Ok k) (u :* b)) =>
 k ((u :* b) :+ (v :* b)) ((u :+ v) :* b))
-> ((Sat (Ok k) u && Sat (Ok k) b) |- Sat (Ok k) (u :* b))
-> k ((u :* b) :+ (v :* b)) ((u :+ v) :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @u @b (Con (Sat (Ok k) (v :* b)) =>
 k ((u :* b) :+ (v :* b)) ((u :+ v) :* b))
-> ((Sat (Ok k) v && Sat (Ok k) b) |- Sat (Ok k) (v :* b))
-> k ((u :* b) :+ (v :* b)) ((u :+ v) :* b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @v @b
{-# INLINE undistr #-}

inDistr :: forall k a b c d w z. (MonoidalPCat k, MCoproductCat k, DistribCat k, Ok6 k a b c d w z)
        => (((a :* w) :+ (b :* w)) `k` ((c :* z) :+ (d :* z)))
        -> (((a :+ b) :* w) `k` ((c :+ d) :* z))
inDistr :: forall (k :: Type -> Type -> Type) a b c d w z.
(MonoidalPCat k, MCoproductCat k, DistribCat k,
 Ok6 k a b c d w z) =>
k ((a :* w) :+ (b :* w)) ((c :* z) :+ (d :* z))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
inDistr k ((a :* w) :+ (b :* w)) ((c :* z) :+ (d :* z))
f = k ((c :* z) :+ (d :* z)) ((c :+ d) :* z)
forall (k :: Type -> Type -> Type) u v b.
(MonoidalPCat k, MCoproductCat k, Ok3 k u v b) =>
k ((u :* b) :+ (v :* b)) ((u :+ v) :* b)
undistr k ((c :* z) :+ (d :* z)) ((c :+ d) :* z)
-> k ((a :+ b) :* w) ((c :* z) :+ (d :* z))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k ((a :* w) :+ (b :* w)) ((c :* z) :+ (d :* z))
f k ((a :* w) :+ (b :* w)) ((c :* z) :+ (d :* z))
-> k ((a :+ b) :* w) ((a :* w) :+ (b :* w))
-> k ((a :+ b) :* w) ((c :* z) :+ (d :* z))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k ((a :+ b) :* w) ((a :* w) :+ (b :* w))
forall (k :: Type -> Type -> Type) u v b.
(DistribCat k, Ok3 k u v b) =>
k (Prod k (Coprod k u v) b) (Coprod k (Prod k u b) (Prod k v b))
distr
  (Con (Sat (Ok k) ((c :* z) :+ (d :* z))) =>
 k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) (c :* z) && Sat (Ok k) (d :* z))
    |- Sat (Ok k) ((c :* z) :+ (d :* z)))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @(c :* z) @(d :* z)
  (Con (Sat (Ok k) (c :* z)) => k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) c && Sat (Ok k) z) |- Sat (Ok k) (c :* z))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @c @z (Con (Sat (Ok k) (d :* z)) => k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) d && Sat (Ok k) z) |- Sat (Ok k) (d :* z))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @d @z
  (Con (Sat (Ok k) ((a :+ b) :* w)) =>
 k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) (a :+ b) && Sat (Ok k) w)
    |- Sat (Ok k) ((a :+ b) :* w))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a :+ b) @w (Con (Sat (Ok k) ((c :+ d) :* z)) =>
 k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) (c :+ d) && Sat (Ok k) z)
    |- Sat (Ok k) ((c :+ d) :* z))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(c :+ d) @z
  (Con (Sat (Ok k) (a :+ b)) => k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :+ b))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a @b (Con (Sat (Ok k) (c :+ d)) => k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) c && Sat (Ok k) d) |- Sat (Ok k) (c :+ d))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @c @d
  (Con (Sat (Ok k) ((a :* w) :+ (b :* w))) =>
 k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) (a :* w) && Sat (Ok k) (b :* w))
    |- Sat (Ok k) ((a :* w) :+ (b :* w)))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @(a :* w) @(b :* w)
  (Con (Sat (Ok k) (a :* w)) => k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) a && Sat (Ok k) w) |- Sat (Ok k) (a :* w))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @w (Con (Sat (Ok k) (b :* w)) => k ((a :+ b) :* w) ((c :+ d) :* z))
-> ((Sat (Ok k) b && Sat (Ok k) w) |- Sat (Ok k) (b :* w))
-> k ((a :+ b) :* w) ((c :+ d) :* z)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b @w
{-# INLINE inDistr #-}

-- | Apply to both parts of a product
twiceP :: (MonoidalPCat k, Ok2 k a c)
       => (a `k` c) -> Prod k a a `k` (Prod k c c)
twiceP :: forall (k :: Type -> Type -> Type) a c.
(MonoidalPCat k, Ok2 k a c) =>
k a c -> k (Prod k a a) (Prod k c c)
twiceP k a c
f = k a c
f k a c -> k a c -> k (Prod k a a) (Prod k c c)
forall (k :: Type -> Type -> Type) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod k a b) (Prod k c d)
*** k a c
f
{-# INLINE twiceP #-}

-- | Operate on left-associated form
inLassocP :: forall k a b c a' b' c'.
             -- Needs :set -fconstraint-solver-iterations=5 or greater:
             (AssociativePCat k, Ok6 k a b c a' b' c')
          => Prod k (Prod k a b) c `k` Prod k (Prod k a' b') c'
          -> Prod k a (Prod k b c) `k` (Prod k a' (Prod k b' c'))
inLassocP :: forall (k :: Type -> Type -> Type) a b c a' b' c'.
(AssociativePCat k, Ok6 k a b c a' b' c') =>
k (Prod k (Prod k a b) c) (Prod k (Prod k a' b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
inLassocP = k (Prod k (a' :* b') c') (Prod k a' (Prod k b' c'))
forall (k :: Type -> Type -> Type) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
rassocP k (Prod k (a' :* b') c') (Prod k a' (Prod k b' c'))
-> k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
forall (k :: Type -> Type -> Type) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
lassocP
          (Con (Sat (Ok k) (Prod k a (Prod k b c))) =>
 k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
 -> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c')))
-> ((Sat (Ok k) a && Sat (Ok k) (Prod k b c))
    |- Sat (Ok k) (Prod k a (Prod k b c)))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a  @(b  :* c ) (Con (Sat (Ok k) (Prod k b c)) =>
 k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
 -> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c')))
-> ((Sat (Ok k) b && Sat (Ok k) c) |- Sat (Ok k) (Prod k b c))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b  @c
          (Con (Sat (Ok k) (Prod k a' (Prod k b' c'))) =>
 k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
 -> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c')))
-> ((Sat (Ok k) a' && Sat (Ok k) (Prod k b' c'))
    |- Sat (Ok k) (Prod k a' (Prod k b' c')))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a' @(b' :* c') (Con (Sat (Ok k) (Prod k b' c')) =>
 k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
 -> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c')))
-> ((Sat (Ok k) b' && Sat (Ok k) c') |- Sat (Ok k) (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b' @c'
          (Con (Sat (Ok k) (Prod k (Prod k a b) c)) =>
 k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
 -> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c')))
-> ((Sat (Ok k) (Prod k a b) && Sat (Ok k) c)
    |- Sat (Ok k) (Prod k (Prod k a b) c))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a  :* b ) @c  (Con (Sat (Ok k) (Prod k a b)) =>
 k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
 -> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c')))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (Prod k a b))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a  @b 
          (Con (Sat (Ok k) (Prod k (a' :* b') c')) =>
 k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
 -> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c')))
-> ((Sat (Ok k) (a' :* b') && Sat (Ok k) c')
    |- Sat (Ok k) (Prod k (a' :* b') c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a' :* b') @c' (Con (Sat (Ok k) (a' :* b')) =>
 k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
 -> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c')))
-> ((Sat (Ok k) a' && Sat (Ok k) b') |- Sat (Ok k) (a' :* b'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a' @b'
{-# INLINE inLassocP #-}

-- | Operate on right-associated form
inRassocP :: forall a b c a' b' c' k.
             (AssociativePCat k, Ok6 k a b c a' b' c')
          => Prod k a (Prod k b c) `k` (Prod k a' (Prod k b' c'))
          -> Prod k (Prod k a b) c `k` Prod k (Prod k a' b') c'
inRassocP :: forall a b c a' b' c' (k :: Type -> Type -> Type).
(AssociativePCat k, Ok6 k a b c a' b' c') =>
k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (Prod k a' b') c')
inRassocP = k (Prod k a' (Prod k b' c')) (Prod k (a' :* b') c')
forall (k :: Type -> Type -> Type) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
lassocP k (Prod k a' (Prod k b' c')) (Prod k (a' :* b') c')
-> k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
forall (k :: Type -> Type -> Type) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
rassocP
          (Con (Sat (Ok k) (Prod k a (Prod k b c))) =>
 k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
 -> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c'))
-> ((Sat (Ok k) a && Sat (Ok k) (Prod k b c))
    |- Sat (Ok k) (Prod k a (Prod k b c)))
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a  @(b  :* c ) (Con (Sat (Ok k) (Prod k b c)) =>
 k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
 -> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c'))
-> ((Sat (Ok k) b && Sat (Ok k) c) |- Sat (Ok k) (Prod k b c))
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b  @c
          (Con (Sat (Ok k) (Prod k a' (Prod k b' c'))) =>
 k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
 -> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c'))
-> ((Sat (Ok k) a' && Sat (Ok k) (Prod k b' c'))
    |- Sat (Ok k) (Prod k a' (Prod k b' c')))
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a' @(b' :* c') (Con (Sat (Ok k) (Prod k b' c')) =>
 k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
 -> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c'))
-> ((Sat (Ok k) b' && Sat (Ok k) c') |- Sat (Ok k) (Prod k b' c'))
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b' @c'
          (Con (Sat (Ok k) (Prod k (Prod k a b) c)) =>
 k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
 -> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c'))
-> ((Sat (Ok k) (Prod k a b) && Sat (Ok k) c)
    |- Sat (Ok k) (Prod k (Prod k a b) c))
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a  :* b ) @c  (Con (Sat (Ok k) (Prod k a b)) =>
 k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
 -> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c'))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (Prod k a b))
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a  @b 
          (Con (Sat (Ok k) (Prod k (a' :* b') c')) =>
 k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
 -> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c'))
-> ((Sat (Ok k) (a' :* b') && Sat (Ok k) c')
    |- Sat (Ok k) (Prod k (a' :* b') c'))
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a' :* b') @c' (Con (Sat (Ok k) (a' :* b')) =>
 k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
 -> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c'))
-> ((Sat (Ok k) a' && Sat (Ok k) b') |- Sat (Ok k) (a' :* b'))
-> k (Prod k a (Prod k b c)) (Prod k a' (Prod k b' c'))
-> k (Prod k (Prod k a b) c) (Prod k (a' :* b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a' @b'
{-# INLINE inRassocP #-}

-- TODO: move twiceP, inLassocP, inRassocP to AltCat

-- | Apply to both parts of a coproduct
twiceS :: (MonoidalSCat k, Ok2 k a c)
       => (a `k` c) -> Coprod k a a `k` (Coprod k c c)
twiceS :: forall (k :: Type -> Type -> Type) a c.
(MonoidalSCat k, Ok2 k a c) =>
k a c -> k (Coprod k a a) (Coprod k c c)
twiceS k a c
f = k a c
f k a c -> k a c -> k (Coprod k a a) (Coprod k c c)
forall (k :: Type -> Type -> Type) a b c d.
(MonoidalSCat k, Ok4 k a b c d) =>
k c a -> k d b -> k (Coprod k c d) (Coprod k a b)
+++ k a c
f

-- | Operate on left-associated form
inLassocS :: forall k a b c a' b' c'.
             (AssociativeSCat k, Ok6 k a b c a' b' c')
          => Coprod k (Coprod k a b) c `k` Coprod k (Coprod k a' b') c'
          -> Coprod k a (Coprod k b c) `k` (Coprod k a' (Coprod k b' c'))
inLassocS :: forall (k :: Type -> Type -> Type) a b c a' b' c'.
(AssociativeSCat k, Ok6 k a b c a' b' c') =>
k (Coprod k (Coprod k a b) c) (Coprod k (Coprod k a' b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
inLassocS = k (Coprod k (a' :+ b') c') (Coprod k a' (Coprod k b' c'))
forall (k :: Type -> Type -> Type) a b c.
(AssociativeSCat k, Ok3 k a b c) =>
k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
rassocS k (Coprod k (a' :+ b') c') (Coprod k a' (Coprod k b' c'))
-> k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
forall (k :: Type -> Type -> Type) a b c.
(AssociativeSCat k, Ok3 k a b c) =>
k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
lassocS
          (Con (Sat (Ok k) (Coprod k a (Coprod k b c))) =>
 k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
 -> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c')))
-> ((Sat (Ok k) a && Sat (Ok k) (Coprod k b c))
    |- Sat (Ok k) (Coprod k a (Coprod k b c)))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a  @(b  :+ c ) (Con (Sat (Ok k) (Coprod k b c)) =>
 k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
 -> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c')))
-> ((Sat (Ok k) b && Sat (Ok k) c) |- Sat (Ok k) (Coprod k b c))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @b  @c
          (Con (Sat (Ok k) (Coprod k a' (Coprod k b' c'))) =>
 k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
 -> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c')))
-> ((Sat (Ok k) a' && Sat (Ok k) (Coprod k b' c'))
    |- Sat (Ok k) (Coprod k a' (Coprod k b' c')))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a' @(b' :+ c') (Con (Sat (Ok k) (Coprod k b' c')) =>
 k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
 -> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c')))
-> ((Sat (Ok k) b' && Sat (Ok k) c')
    |- Sat (Ok k) (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @b' @c'
          (Con (Sat (Ok k) (Coprod k (Coprod k a b) c)) =>
 k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
 -> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c')))
-> ((Sat (Ok k) (Coprod k a b) && Sat (Ok k) c)
    |- Sat (Ok k) (Coprod k (Coprod k a b) c))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @(a  :+ b ) @c  (Con (Sat (Ok k) (Coprod k a b)) =>
 k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
 -> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c')))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (Coprod k a b))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a  @b 
          (Con (Sat (Ok k) (Coprod k (a' :+ b') c')) =>
 k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
 -> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c')))
-> ((Sat (Ok k) (a' :+ b') && Sat (Ok k) c')
    |- Sat (Ok k) (Coprod k (a' :+ b') c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @(a' :+ b') @c' (Con (Sat (Ok k) (a' :+ b')) =>
 k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
 -> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c')))
-> ((Sat (Ok k) a' && Sat (Ok k) b') |- Sat (Ok k) (a' :+ b'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a' @b'
{-# INLINE inLassocS #-}

-- | Operate on right-associated form
inRassocS :: forall a b c a' b' c' k.
             (AssociativeSCat k, Ok6 k a b c a' b' c')
          => Coprod k a (Coprod k b c) `k` (Coprod k a' (Coprod k b' c'))
          -> Coprod k (Coprod k a b) c `k` Coprod k (Coprod k a' b') c'
inRassocS :: forall a b c a' b' c' (k :: Type -> Type -> Type).
(AssociativeSCat k, Ok6 k a b c a' b' c') =>
k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (Coprod k a' b') c')
inRassocS = k (Coprod k a' (Coprod k b' c')) (Coprod k (a' :+ b') c')
forall (k :: Type -> Type -> Type) a b c.
(AssociativeSCat k, Ok3 k a b c) =>
k (Coprod k a (Coprod k b c)) (Coprod k (Coprod k a b) c)
lassocS k (Coprod k a' (Coprod k b' c')) (Coprod k (a' :+ b') c')
-> k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
forall (k :: Type -> Type -> Type) a b a' b'.
(Category k, Oks k '[a, b, a', b']) =>
k b b' -> k a' a -> k a b -> k a' b'
<~ k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
forall (k :: Type -> Type -> Type) a b c.
(AssociativeSCat k, Ok3 k a b c) =>
k (Coprod k (Coprod k a b) c) (Coprod k a (Coprod k b c))
rassocS
          (Con (Sat (Ok k) (Coprod k a (Coprod k b c))) =>
 k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
 -> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c'))
-> ((Sat (Ok k) a && Sat (Ok k) (Coprod k b c))
    |- Sat (Ok k) (Coprod k a (Coprod k b c)))
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a  @(b  :+ c ) (Con (Sat (Ok k) (Coprod k b c)) =>
 k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
 -> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c'))
-> ((Sat (Ok k) b && Sat (Ok k) c) |- Sat (Ok k) (Coprod k b c))
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @b  @c
          (Con (Sat (Ok k) (Coprod k a' (Coprod k b' c'))) =>
 k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
 -> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c'))
-> ((Sat (Ok k) a' && Sat (Ok k) (Coprod k b' c'))
    |- Sat (Ok k) (Coprod k a' (Coprod k b' c')))
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a' @(b' :+ c') (Con (Sat (Ok k) (Coprod k b' c')) =>
 k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
 -> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c'))
-> ((Sat (Ok k) b' && Sat (Ok k) c')
    |- Sat (Ok k) (Coprod k b' c'))
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @b' @c'
          (Con (Sat (Ok k) (Coprod k (Coprod k a b) c)) =>
 k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
 -> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c'))
-> ((Sat (Ok k) (Coprod k a b) && Sat (Ok k) c)
    |- Sat (Ok k) (Coprod k (Coprod k a b) c))
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @(a  :+ b ) @c  (Con (Sat (Ok k) (Coprod k a b)) =>
 k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
 -> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c'))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (Coprod k a b))
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a  @b 
          (Con (Sat (Ok k) (Coprod k (a' :+ b') c')) =>
 k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
 -> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c'))
-> ((Sat (Ok k) (a' :+ b') && Sat (Ok k) c')
    |- Sat (Ok k) (Coprod k (a' :+ b') c'))
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @(a' :+ b') @c' (Con (Sat (Ok k) (a' :+ b')) =>
 k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
 -> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c'))
-> ((Sat (Ok k) a' && Sat (Ok k) b') |- Sat (Ok k) (a' :+ b'))
-> k (Coprod k a (Coprod k b c)) (Coprod k a' (Coprod k b' c'))
-> k (Coprod k (Coprod k a b) c) (Coprod k (a' :+ b') c')
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a' @b'
{-# INLINE inRassocS #-}

transposeS :: forall k a b c d. (MCoproductCat k, Ok4 k a b c d)
           => Coprod k (Coprod k a b) (Coprod k c d) `k` Coprod k (Coprod k a c) (Coprod k b d)
transposeS :: forall (k :: Type -> Type -> Type) a b c d.
(MCoproductCat k, Ok4 k a b c d) =>
k (Coprod k (Coprod k a b) (Coprod k c d))
  (Coprod k (Coprod k a c) (Coprod k b d))
transposeS = (k (a :+ c) (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k a (Coprod k a b)
inlk (a :+ c) (Coprod k (a :+ c) (Coprod k b d))
-> k a (a :+ c) -> k a (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.k a (a :+ c)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k a (Coprod k a b)
inl k a (Coprod k (a :+ c) (Coprod k b d))
-> k b (Coprod k (a :+ c) (Coprod k b d))
-> k (Coprod k a b) (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) a c d.
(MCoproductCat k, Ok3 k a c d) =>
k c a -> k d a -> k (Coprod k c d) a
||| k (Coprod k b d) (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k b (Coprod k a b)
inrk (Coprod k b d) (Coprod k (a :+ c) (Coprod k b d))
-> k b (Coprod k b d) -> k b (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.k b (Coprod k b d)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k a (Coprod k a b)
inl) k (Coprod k a b) (Coprod k (a :+ c) (Coprod k b d))
-> k (Coprod k c d) (Coprod k (a :+ c) (Coprod k b d))
-> k (Coprod k (Coprod k a b) (Coprod k c d))
     (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) a c d.
(MCoproductCat k, Ok3 k a c d) =>
k c a -> k d a -> k (Coprod k c d) a
||| (k (a :+ c) (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k a (Coprod k a b)
inlk (a :+ c) (Coprod k (a :+ c) (Coprod k b d))
-> k c (a :+ c) -> k c (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.k c (a :+ c)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k b (Coprod k a b)
inr k c (Coprod k (a :+ c) (Coprod k b d))
-> k d (Coprod k (a :+ c) (Coprod k b d))
-> k (Coprod k c d) (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) a c d.
(MCoproductCat k, Ok3 k a c d) =>
k c a -> k d a -> k (Coprod k c d) a
||| k (Coprod k b d) (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k b (Coprod k a b)
inrk (Coprod k b d) (Coprod k (a :+ c) (Coprod k b d))
-> k d (Coprod k b d) -> k d (Coprod k (a :+ c) (Coprod k b d))
forall (k :: Type -> Type -> Type) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.k d (Coprod k b d)
forall (k :: Type -> Type -> Type) a b.
(CoproductCat k, Ok2 k a b) =>
k b (Coprod k a b)
inr)
  (Con (Sat (Ok k) (Coprod k (a :+ c) (Coprod k b d))) =>
 k (Coprod k (Coprod k a b) (Coprod k c d))
   (Coprod k (a :+ c) (Coprod k b d)))
-> ((Sat (Ok k) (a :+ c) && Sat (Ok k) (Coprod k b d))
    |- Sat (Ok k) (Coprod k (a :+ c) (Coprod k b d)))
-> k (Coprod k (Coprod k a b) (Coprod k c d))
     (Coprod k (a :+ c) (Coprod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @(Coprod k a c) @(Coprod k b d)
  (Con (Sat (Ok k) (Coprod k c d)) =>
 k (Coprod k (Coprod k a b) (Coprod k c d))
   (Coprod k (a :+ c) (Coprod k b d)))
-> ((Sat (Ok k) c && Sat (Ok k) d) |- Sat (Ok k) (Coprod k c d))
-> k (Coprod k (Coprod k a b) (Coprod k c d))
     (Coprod k (a :+ c) (Coprod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @c @d
  (Con (Sat (Ok k) (Coprod k a b)) =>
 k (Coprod k (Coprod k a b) (Coprod k c d))
   (Coprod k (a :+ c) (Coprod k b d)))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (Coprod k a b))
-> k (Coprod k (Coprod k a b) (Coprod k c d))
     (Coprod k (a :+ c) (Coprod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a @b
  (Con (Sat (Ok k) (Coprod k b d)) =>
 k (Coprod k (Coprod k a b) (Coprod k c d))
   (Coprod k (a :+ c) (Coprod k b d)))
-> ((Sat (Ok k) b && Sat (Ok k) d) |- Sat (Ok k) (Coprod k b d))
-> k (Coprod k (Coprod k a b) (Coprod k c d))
     (Coprod k (a :+ c) (Coprod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @b @d
  (Con (Sat (Ok k) (a :+ c)) =>
 k (Coprod k (Coprod k a b) (Coprod k c d))
   (Coprod k (a :+ c) (Coprod k b d)))
-> ((Sat (Ok k) a && Sat (Ok k) c) |- Sat (Ok k) (a :+ c))
-> k (Coprod k (Coprod k a b) (Coprod k c d))
     (Coprod k (a :+ c) (Coprod k b d))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: Type -> Type -> Type) a b.
OkCoprod k =>
(Ok' k a && Ok' k b) |- Ok' k (Coprod k a b)
okCoprod @k @a @c
{-# INLINE transposeS #-}

-- TODO: define transposeS without MonoidalSCat.