-- |
-- Module      :  Control.Arrow.Constrained
-- Copyright   :  (c) 2013 Justus Sagemüller
-- License     :  GPL v3 (see COPYING)
-- Maintainer  :  (@) jsag $ hvl.no
-- 
-- Haskell's 'Arr.Arrow's, going back to [Hughes 2000], combine multiple ideas from
-- category theory:
-- 
-- * They expand upon cartesian categories, by offering ways to combine arrows between
--   simple objects to composite ones working on tuples (i.e. /products/) thereof.
-- 
-- * They constitute a \"profunctor\" interface, allowing to \"@fmap@\" both covariantly
--   over the second parameter, as well as contravariantly over the first. As in case
--   of "Control.Functor.Constrained", we wish the underlying category to fmap from
--   not to be limited to /Hask/, so 'Arrow' also has an extra parameter.
-- 
-- To facilitate these somewhat divergent needs, 'Arrow' is split up in three classes.
-- These do not even form an ordinary hierarchy, to allow categories to implement
-- only one /or/ the other aspect.
-- 
-- That's not the only significant difference of this module, compared to "Control.Arrow":
-- 
-- * Kleisli arrows are not defined here, but in "Control.Monad.Constrained".
--   Monads are really a much more specific concept than category arrows.
-- 
-- * Some extra utilities are included that don't apparently have much to
--   do with 'Arrow' at all, but require the expanded cartesian-category tools
--   and are therefore not in "Control.Category.Constrained".

{-# LANGUAGE ConstraintKinds              #-}
{-# LANGUAGE TypeFamilies                 #-}
{-# LANGUAGE FunctionalDependencies       #-}
{-# LANGUAGE TupleSections                #-}
{-# LANGUAGE ScopedTypeVariables          #-}
{-# LANGUAGE UnicodeSyntax                #-}
{-# LANGUAGE FlexibleInstances            #-}
{-# LANGUAGE FlexibleContexts             #-}
{-# LANGUAGE UndecidableInstances         #-}
{-# LANGUAGE CPP                          #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses      #-}
#endif
{-# LANGUAGE TypeOperators                #-}
{-# LANGUAGE RankNTypes                   #-}
{-# LANGUAGE AllowAmbiguousTypes          #-}


module Control.Arrow.Constrained (
    -- * The Arrow type classes
      Arrow, Morphism(..), PreArrow(..), WellPointed(..),ObjectPoint, EnhancedCat(..)
    -- * Dual / "choice" arrows
    , ArrowChoice, MorphChoice(..), PreArrChoice(..)
    -- * Distributive law between sum- and product objects
    , SPDistribute(..) 
    -- * Function-like categories
    , Function, ($)
    -- * Alternative composition notation
    , (>>>), (<<<)
    -- * Proxies for cartesian categories
    , CartesianAgent(..)
    , genericAgentCombine, genericUnit, genericAlg1to2, genericAlg2to1, genericAlg2to2
    , PointAgent(..), genericPoint
    -- * Misc utility
    -- ** Conditionals
    , choose, ifThenElse
    -- ** Coercions
    , follow, flout, pretend, swallow, pretendLike, swallowLike
    ) where

import Prelude hiding (id, const, fst, snd, (.), ($), Functor(..), Monad(..), (=<<))
import Control.Category.Constrained
import qualified Control.Category.Hask as Hask

import GHC.Exts (Constraint)
import Data.Tagged
import Data.Void
import Data.CategoryObject.Product

import Data.Coerce
import Data.Type.Coercion

import qualified Control.Arrow as Arr

import Control.Category.Discrete

import qualified Data.Functor.Contravariant as Hask

infixr 1 >>>, <<<
infixr 3 &&&, ***

(>>>) :: (Category k, Object k a, Object k b, Object k c) 
             => k a b -> k b c -> k a c
>>> :: forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
(>>>) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
(.)
(<<<) :: (Category k, Object k a, Object k b, Object k c) 
             => k b c -> k a b -> k a c
<<< :: forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
(<<<) = forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
(.)

class (Cartesian a) => Morphism a where
  first :: ( ObjectPair a b d, ObjectPair a c d )
         => a b c -> a (b, d) (c, d)
  first = (forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id)
  second :: ( ObjectPair a d b, ObjectPair a d c )
         => a b c -> a (d, b) (d, c)
  second = (forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
idforall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***)
  (***) :: ( ObjectPair a b b', ObjectPair a c c' )
         => a b c -> a b' c' -> a (b,b') (c,c')

-- | Dual to 'Morphism', dealing with sums instead of products.
class (CoCartesian a) => MorphChoice a where
  left :: ( ObjectSum a b d, ObjectSum a c d )
         => a b c -> a (b+d) (c+d)
  left = (forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id)
  right :: ( ObjectSum a d b, ObjectSum a d c )
         => a b c -> a (d+b) (d+c)
  right = (forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
idforall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++)
  (+++) :: ( ObjectSum a b b', ObjectSum a c c' )
         => a b c -> a b' c' -> a (b+b') (c+c')



-- | Unlike 'first', 'second', '***' and 'arr', the fanout operation '&&&' has an
--   intrinsic notion of \"direction\": it is basically equivalent to precomposing
--   the result of '***' with a @b -> (b,b)@, but that is only available
--   for arrows that generalise ordinary functions, in their native direction.
--   (@(b,b) ->b@ is specific to semigroups.) It is for this reason the only constituent
--   class of 'Arrow' that actually has \"arrow\" in its name.
-- 
--   In terms of category theory, this \"direction\" reflects the distinction
--   between /initial-/ and /terminal objects/. The latter are more interesting,
--   basically what 'UnitObject' is useful for. It gives rise to the tuple
--   selector morphisms as well.
class (Morphism a) => PreArrow a where
  (&&&) :: ( Object a b, ObjectPair a c c' )
         => a b c -> a b c' -> a b (c,c')
  terminal :: ( Object a b ) => a b (UnitObject a)
  fst :: (ObjectPair a x y) => a (x,y) x
  snd :: (ObjectPair a x y) => a (x,y) y

infixr 2 |||
-- | Dual to 'PreArrow', this class deals with the vacuous initial (zero) objects,
--   but also more usefully with choices / sums.
--   This represents the most part of 'Hask.ArrowChoice'.
class (MorphChoice k) => PreArrChoice k where
  (|||) :: ( ObjectSum k b b', Object k c )
         => k b c -> k b' c -> k (b+b') c
  -- | This is basically 'absurd'.
  initial :: ( Object k b ) => k (ZeroObject k) b
  -- | Perhaps @lft@ and @rgt@ would be more consequent names, but likely more confusing as well.
  coFst :: (ObjectSum k a b) => k a (a+b)
  coSnd :: (ObjectSum k a b) => k b (a+b)


-- | Like in arithmetics, the distributive law
--   @a &#x22c5; (b + c) &#x2248; (a &#x22c5; b) + (a &#x22c5; c)@
--   holds for Haskell types &#x2013; in the usual isomorphism sense. But like many such
--   isomorphisms that are trivial to inline in /Hask/, this is not necessarily the case
--   for general categories.
class (PreArrow k, PreArrChoice k) => SPDistribute k where
  distribute :: ( ObjectSum k (a,b) (a,c), ObjectPair k a (b+c)
                , ObjectSum k b c, PairObjects k a b, PairObjects k a c )
         => k (a, b+c) ((a,b)+(a,c))
  unDistribute :: ( ObjectSum k (a,b) (a,c), ObjectPair k a (b+c)
                  , ObjectSum k b c, PairObjects k a b, PairObjects k a c )
         => k ((a,b)+(a,c)) (a, b+c)
  boolAsSwitch :: ( ObjectSum k a a, ObjectPair k Bool a ) => k (Bool,a) (a+a)
  boolFromSwitch :: ( ObjectSum k a a, ObjectPair k Bool a ) => k (a+a) (Bool,a)
-- boolFromSwitch = (boolFromSum <<< terminal +++ terminal) &&& (id ||| id)

instance ( SPDistribute k 
         , ObjectSum k (a,b) (a,c), ObjectPair k a (b+c)
         , ObjectSum k b c, PairObjects k a b, PairObjects k a c
         ) => Isomorphic k (a, b+c) ((a,b)+(a,c)) where
  iso :: k (a, b + c) ((a, b) + (a, c))
iso = forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
 ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k (a, b + c) ((a, b) + (a, c))
distribute
instance ( SPDistribute k 
         , ObjectSum k (a,b) (a,c), ObjectPair k a (b+c)
         , ObjectSum k b c, PairObjects k a b, PairObjects k a c
         ) => Isomorphic k ((a,b)+(a,c)) (a, b+c) where
  iso :: k ((a, b) + (a, c)) (a, b + c)
iso = forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
 ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k ((a, b) + (a, c)) (a, b + c)
unDistribute
instance ( SPDistribute k 
         , ObjectSum k a a, ObjectPair k Bool a
         ) => Isomorphic k (Bool, a) (a+a) where
  iso :: k (Bool, a) (a + a)
iso = forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (Bool, a) (a + a)
boolAsSwitch
instance ( SPDistribute k 
         , ObjectSum k a a, ObjectPair k Bool a
         ) => Isomorphic k (a+a) (Bool, a) where
  iso :: k (a + a) (Bool, a)
iso = forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (a + a) (Bool, a)
boolFromSwitch

 

-- | 'WellPointed' expresses the relation between your category's objects
--   and the values of the Haskell data types (which is, after all, what objects are
--   in this library). Specifically, this class allows you to \"point\" on
--   specific objects, thus making out a value of that type as a point of the object.
--   
--   Perhaps easier than thinking about what that's supposed to mean is noting
--   this class contains 'const'. Thus 'WellPointed' is /almost/ the
--   traditional 'Hask.Arrow': it lets you express all the natural transformations
--   and inject constant values, only you can't just promote arbitrary functions
--   to arrows of the category.
--   
--   Unlike with 'Morphism' and 'PreArrow', a literal dual of 'WellPointed' does
--   not seem useful.
class (PreArrow a, ObjectPoint a (UnitObject a)) => WellPointed a where
  {-# MINIMAL unit, (globalElement | const) #-}
  type PointObject a x :: Constraint
  type PointObject a x = ()
  globalElement :: (ObjectPoint a x) => x -> a (UnitObject a) x
  globalElement = forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const
  unit :: CatTagged a (UnitObject a)
  const :: (Object a b, ObjectPoint a x) 
            => x -> a b x
  const x
x = forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement x
x forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal

type ObjectPoint k a = (Object k a, PointObject k a)
  
-- -- | 'WellPointed' does not have a useful literal dual.
-- class (PreArrChoice a, ObjectPoint a (ZeroObject a)) => WellChosen a where
--   type ChoiceObject a x :: Constraint
--   type ChoiceObject a x = ()
--   localElement :: (ObjectChoice a x) => a x (ZeroObject a) -> (x -> b
--   zero :: CatTagged a (ZeroObject a)
--   doomed :: (Object a b, ObjectChoice a x) 
--             => x -> a x b
--   doomed x = globalElement x . initial
-- 
-- type ObjectChoice k a = (Object k a, ChoiceObject k x)
-- 
value :: forall f x . (WellPointed f, Function f, Object f x)
           => f (UnitObject f) x -> x
value :: forall (f :: * -> * -> *) x.
(WellPointed f, Function f, Object f x) =>
f (UnitObject f) x -> x
value f (UnitObject f) x
f = f (UnitObject f) x
f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall {k} (s :: k) b. Tagged s b -> b
untag(forall (a :: * -> * -> *).
WellPointed a =>
CatTagged a (UnitObject a)
unit :: Tagged (f (UnitObject f) (UnitObject f)) (UnitObject f))



-- | @'EnhancedCat' a k@ means that the subcategory of @k@ whose objects are also
--   objects of @a@ is a subcategory of @a@. This works like
--   'Control.Category.Constrained.Reified.EnhancedCat'', but
--   does not require @'Object' k ⊆ 'Object' a@.
class (Category a, Category k) => EnhancedCat a k where
  arr :: (Object k b, Object k c, Object a b, Object a c)
         => k b c -> a b c
instance (Category k) => EnhancedCat k k where
  arr :: forall b c.
(Object k b, Object k c, Object k b, Object k c) =>
k b c -> k b c
arr = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id

instance EnhancedCat (->) Discrete where
  arr :: forall b c.
(Object Discrete b, Object Discrete c, Object (->) b,
 Object (->) c) =>
Discrete b c -> b -> c
arr Discrete b c
Refl = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance EnhancedCat Coercion Discrete where
  arr :: forall b c.
(Object Discrete b, Object Discrete c, Object Coercion b,
 Object Coercion c) =>
Discrete b c -> Coercion b c
arr Discrete b c
Refl = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance Category f => EnhancedCat (o⊢f) Discrete where
  arr :: forall b c.
(Object Discrete b, Object Discrete c, Object (o ⊢ f) b,
 Object (o ⊢ f) c) =>
Discrete b c -> (⊢) o f b c
arr Discrete b c
Refl = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id

-- | Many categories have as morphisms essentially /functions with extra properties/:
--   group homomorphisms, linear maps, continuous functions...
-- 
--   It makes sense to generalise the notion of function application to these
--   morphisms; we can't do that for the simple juxtaposition writing @f x@,
--   but it is possible for the function-application operator @$@.
-- 
--   This is particularly useful for 'ConstrainedCategory' versions of Hask,
--   where after all the morphisms are /nothing but functions/.
type Function f = EnhancedCat (->) f

infixr 0 $
($) :: (Function f, Object f a, Object f b) => f a b -> a -> b
f a b
f $ :: forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a
x = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr f a b
f a
x

instance (Function f) => EnhancedCat (->) (o⊢f) where
  arr :: forall b c.
(Object (o ⊢ f) b, Object (o ⊢ f) c, Object (->) b,
 Object (->) c) =>
(⊢) o f b c -> b -> c
arr (ConstrainedMorphism f b c
q) = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr f b c
q
instance (EnhancedCat Discrete f) => EnhancedCat Discrete (o⊢f) where
  arr :: forall b c.
(Object (o ⊢ f) b, Object (o ⊢ f) c, Object Discrete b,
 Object Discrete c) =>
(⊢) o f b c -> Discrete b c
arr (ConstrainedMorphism f b c
q) = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr f b c
q

instance EnhancedCat (->) Coercion where
  arr :: forall b c.
(Object Coercion b, Object Coercion c, Object (->) b,
 Object (->) c) =>
Coercion b c -> b -> c
arr = forall a b. Coercion a b -> a -> b
coerceWith



type Arrow a k = (WellPointed a, EnhancedCat a k)
type ArrowChoice a k = (WellPointed a, PreArrChoice a, EnhancedCat a k)

instance Morphism (->) where
  first :: forall b d c.
(ObjectPair (->) b d, ObjectPair (->) c d) =>
(b -> c) -> (b, d) -> (c, d)
first = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
Arr.first
  second :: forall d b c.
(ObjectPair (->) d b, ObjectPair (->) d c) =>
(b -> c) -> (d, b) -> (d, c)
second = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
Arr.second
  *** :: forall b b' c c'.
(ObjectPair (->) b b', ObjectPair (->) c c') =>
(b -> c) -> (b' -> c') -> (b, b') -> (c, c')
(***) = forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
(Arr.***)
instance MorphChoice (->) where
  left :: forall b d c.
(ObjectSum (->) b d, ObjectSum (->) c d) =>
(b -> c) -> (b + d) -> (c + d)
left = forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
Arr.left
  right :: forall d b c.
(ObjectSum (->) d b, ObjectSum (->) d c) =>
(b -> c) -> (d + b) -> (d + c)
right = forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
Arr.right
  +++ :: forall b b' c c'.
(ObjectSum (->) b b', ObjectSum (->) c c') =>
(b -> c) -> (b' -> c') -> (b + b') -> (c + c')
(+++) = forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
(Arr.+++)
instance PreArrow (->) where
  &&& :: forall b c c'.
(Object (->) b, ObjectPair (->) c c') =>
(b -> c) -> (b -> c') -> b -> (c, c')
(&&&) = forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
(Arr.&&&)
  fst :: forall x y. ObjectPair (->) x y => (x, y) -> x
fst (x
a,y
_) = x
a
  snd :: forall x y. ObjectPair (->) x y => (x, y) -> y
snd (x
_,y
b) = y
b
  terminal :: forall b. Object (->) b => b -> UnitObject (->)
terminal = forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ()
instance PreArrChoice (->) where
  ||| :: forall b b' c.
(ObjectSum (->) b b', Object (->) c) =>
(b -> c) -> (b' -> c) -> (b + b') -> c
(|||) = forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
(Arr.|||)
  coFst :: forall a b. ObjectSum (->) a b => a -> (a + b)
coFst a
a = forall a b. a -> Either a b
Left a
a
  coSnd :: forall a b. ObjectSum (->) a b => b -> (a + b)
coSnd b
b = forall a b. b -> Either a b
Right b
b
  initial :: forall b. Object (->) b => ZeroObject (->) -> b
initial = forall a. Void -> a
absurd
instance SPDistribute (->) where
  distribute :: forall a b c.
(ObjectSum (->) (a, b) (a, c), ObjectPair (->) a (b + c),
 ObjectSum (->) b c, PairObjects (->) a b, PairObjects (->) a c) =>
(a, b + c) -> ((a, b) + (a, c))
distribute (a
a, Left b
b) = forall a b. a -> Either a b
Left (a
a,b
b)
  distribute (a
a, Right c
c) = forall a b. b -> Either a b
Right (a
a,c
c)
  unDistribute :: forall a b c.
(ObjectSum (->) (a, b) (a, c), ObjectPair (->) a (b + c),
 ObjectSum (->) b c, PairObjects (->) a b, PairObjects (->) a c) =>
((a, b) + (a, c)) -> (a, b + c)
unDistribute (Left (a
a,b
b)) = (a
a, forall a b. a -> Either a b
Left b
b)
  unDistribute (Right (a
a,c
c)) = (a
a, forall a b. b -> Either a b
Right c
c)
  boolAsSwitch :: forall a.
(ObjectSum (->) a a, ObjectPair (->) Bool a) =>
(Bool, a) -> (a + a)
boolAsSwitch (Bool
False, a
a) = forall a b. a -> Either a b
Left a
a
  boolAsSwitch (Bool
True, a
a) = forall a b. b -> Either a b
Right a
a
  boolFromSwitch :: forall a.
(ObjectSum (->) a a, ObjectPair (->) Bool a) =>
(a + a) -> (Bool, a)
boolFromSwitch (Left a
a) = (Bool
False, a
a)
  boolFromSwitch (Right a
a) = (Bool
True, a
a)
instance WellPointed (->) where
  globalElement :: forall x. ObjectPoint (->) x => x -> UnitObject (->) -> x
globalElement = forall a b. a -> b -> a
Hask.const
  unit :: CatTagged (->) (UnitObject (->))
unit = forall (f :: * -> *) a. Applicative f => a -> f a
Hask.pure ()
  const :: forall b x. (Object (->) b, ObjectPoint (->) x) => x -> b -> x
const = forall a b. a -> b -> a
Hask.const

instance (Morphism k, Morphism l) => Morphism (k×l) where
  (k (LFactor b) (LFactor c)
f:***:l (RFactor b) (RFactor c)
g) *** :: forall b b' c c'.
(ObjectPair (k × l) b b', ObjectPair (k × l) c c') =>
(×) k l b c -> (×) k l b' c' -> (×) k l (b, b') (c, c')
*** (k (LFactor b') (LFactor c')
h:***:l (RFactor b') (RFactor c')
i) = (k (LFactor b) (LFactor c)
fforall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***k (LFactor b') (LFactor c')
h) forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: (l (RFactor b) (RFactor c)
gforall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***l (RFactor b') (RFactor c')
i)
instance (PreArrow k, PreArrow l) => PreArrow (k×l) where
  (k (LFactor b) (LFactor c)
f:***:l (RFactor b) (RFactor c)
g) &&& :: forall b c c'.
(Object (k × l) b, ObjectPair (k × l) c c') =>
(×) k l b c -> (×) k l b c' -> (×) k l b (c, c')
&&& (k (LFactor b) (LFactor c')
h:***:l (RFactor b) (RFactor c')
i) = (k (LFactor b) (LFactor c)
fforall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&&k (LFactor b) (LFactor c')
h) forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: (l (RFactor b) (RFactor c)
gforall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&&l (RFactor b) (RFactor c')
i)
  terminal :: forall b. Object (k × l) b => (×) k l b (UnitObject (k × l))
terminal = forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
  fst :: forall x y. ObjectPair (k × l) x y => (×) k l (x, y) x
fst = forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst
  snd :: forall x y. ObjectPair (k × l) x y => (×) k l (x, y) y
snd = forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd

prodCatUnit :: ∀ k l . (WellPointed k, WellPointed l)
      => Tagged ((k×l) (ProductCatObj (UnitObject k) (UnitObject l))
                       (ProductCatObj (UnitObject k) (UnitObject l)))
                (ProductCatObj (UnitObject k) (UnitObject l))
prodCatUnit :: forall (k :: * -> * -> *) (l :: * -> * -> *).
(WellPointed k, WellPointed l) =>
Tagged
  ((×)
     k
     l
     (ProductCatObj (UnitObject k) (UnitObject l))
     (ProductCatObj (UnitObject k) (UnitObject l)))
  (ProductCatObj (UnitObject k) (UnitObject l))
prodCatUnit = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b. a -> b -> ProductCatObj a b
ProductCatObj UnitObject k
uk UnitObject l
ul
 where Tagged UnitObject k
uk = forall (a :: * -> * -> *).
WellPointed a =>
CatTagged a (UnitObject a)
unit :: Tagged (k (UnitObject k) (UnitObject k)) (UnitObject k)
       Tagged UnitObject l
ul = forall (a :: * -> * -> *).
WellPointed a =>
CatTagged a (UnitObject a)
unit :: Tagged (l (UnitObject l) (UnitObject l)) (UnitObject l)

instance (WellPointed k, WellPointed l) => WellPointed (k×l) where
  type PointObject (k×l) o = (PointObject k (LFactor o), PointObject l (RFactor o))
  unit :: CatTagged (k × l) (UnitObject (k × l))
unit = forall (k :: * -> * -> *) (l :: * -> * -> *).
(WellPointed k, WellPointed l) =>
Tagged
  ((×)
     k
     l
     (ProductCatObj (UnitObject k) (UnitObject l))
     (ProductCatObj (UnitObject k) (UnitObject l)))
  (ProductCatObj (UnitObject k) (UnitObject l))
prodCatUnit
  const :: forall b x.
(Object (k × l) b, ObjectPoint (k × l) x) =>
x -> (×) k l b x
const x
c = forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (forall t. IsProduct t => t -> LFactor t
lfactorProj x
c) forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (forall t. IsProduct t => t -> RFactor t
rfactorProj x
c)

constrainedArr :: (Category k, Category a, o b, o c ) => ( k b c ->    a  b c )
                                                        -> k b c -> (o⊢a) b c
constrainedArr :: forall (k :: * -> * -> *) (a :: * -> * -> *) (o :: * -> Constraint)
       b c.
(Category k, Category a, o b, o c) =>
(k b c -> a b c) -> k b c -> (⊢) o a b c
constrainedArr k b c -> a b c
ar = forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
(Category k, o a, o b) =>
k a b -> (⊢) o k a b
constrained forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b c -> a b c
ar

constrainedFirst :: ( Category a, Cartesian a, ObjectPair a b d, ObjectPair a c d )
  => (    a  b c ->    a  (b, d) (c, d) )
    -> (o⊢a) b c -> (o⊢a) (b, d) (c, d)
constrainedFirst :: forall (a :: * -> * -> *) b d c (o :: * -> Constraint).
(Category a, Cartesian a, ObjectPair a b d, ObjectPair a c d) =>
(a b c -> a (b, d) (c, d)) -> (⊢) o a b c -> (⊢) o a (b, d) (c, d)
constrainedFirst a b c -> a (b, d) (c, d)
fs = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a b c -> a (b, d) (c, d)
fs forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained
  
constrainedSecond :: ( Category a, Cartesian a, ObjectPair a d b, ObjectPair a d c )
  => (    a  b c ->    a  (d, b) (d, c) )
    -> (o⊢a) b c -> (o⊢a) (d, b) (d, c)
constrainedSecond :: forall (a :: * -> * -> *) d b c (o :: * -> Constraint).
(Category a, Cartesian a, ObjectPair a d b, ObjectPair a d c) =>
(a b c -> a (d, b) (d, c)) -> (⊢) o a b c -> (⊢) o a (d, b) (d, c)
constrainedSecond a b c -> a (d, b) (d, c)
sn = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. a b c -> a (d, b) (d, c)
sn forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained

instance Morphism Hask.Op where
  first :: forall b d c.
(ObjectPair Op b d, ObjectPair Op c d) =>
Op b c -> Op (b, d) (c, d)
first (Hask.Op c -> b
f) = forall a b. (b -> a) -> Op a b
Hask.Op forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first c -> b
f
  second :: forall d b c.
(ObjectPair Op d b, ObjectPair Op d c) =>
Op b c -> Op (d, b) (d, c)
second (Hask.Op c -> b
f) = forall a b. (b -> a) -> Op a b
Hask.Op forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) d b c.
(Morphism a, ObjectPair a d b, ObjectPair a d c) =>
a b c -> a (d, b) (d, c)
second c -> b
f
  Hask.Op c -> b
f *** :: forall b b' c c'.
(ObjectPair Op b b', ObjectPair Op c c') =>
Op b c -> Op b' c' -> Op (b, b') (c, c')
*** Hask.Op c' -> b'
g = forall a b. (b -> a) -> Op a b
Hask.Op forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ c -> b
f forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
*** c' -> b'
g
instance MorphChoice Hask.Op where
  left :: forall b d c.
(ObjectSum Op b d, ObjectSum Op c d) =>
Op b c -> Op (b + d) (c + d)
left (Hask.Op c -> b
f) = forall a b. (b -> a) -> Op a b
Hask.Op forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b d c.
(MorphChoice a, ObjectSum a b d, ObjectSum a c d) =>
a b c -> a (b + d) (c + d)
left c -> b
f
  right :: forall d b c.
(ObjectSum Op d b, ObjectSum Op d c) =>
Op b c -> Op (d + b) (d + c)
right (Hask.Op c -> b
f) = forall a b. (b -> a) -> Op a b
Hask.Op forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) d b c.
(MorphChoice a, ObjectSum a d b, ObjectSum a d c) =>
a b c -> a (d + b) (d + c)
right c -> b
f
  Hask.Op c -> b
f +++ :: forall b b' c c'.
(ObjectSum Op b b', ObjectSum Op c c') =>
Op b c -> Op b' c' -> Op (b + b') (c + c')
+++ Hask.Op c' -> b'
g = forall a b. (b -> a) -> Op a b
Hask.Op forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ c -> b
f forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++ c' -> b'
g

instance (Morphism a, o (UnitObject a)) => Morphism (o⊢a) where
  first :: forall b d c.
(ObjectPair (o ⊢ a) b d, ObjectPair (o ⊢ a) c d) =>
(⊢) o a b c -> (⊢) o a (b, d) (c, d)
first = forall (a :: * -> * -> *) b d c (o :: * -> Constraint).
(Category a, Cartesian a, ObjectPair a b d, ObjectPair a c d) =>
(a b c -> a (b, d) (c, d)) -> (⊢) o a b c -> (⊢) o a (b, d) (c, d)
constrainedFirst forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first
  second :: forall d b c.
(ObjectPair (o ⊢ a) d b, ObjectPair (o ⊢ a) d c) =>
(⊢) o a b c -> (⊢) o a (d, b) (d, c)
second = forall (a :: * -> * -> *) d b c (o :: * -> Constraint).
(Category a, Cartesian a, ObjectPair a d b, ObjectPair a d c) =>
(a b c -> a (d, b) (d, c)) -> (⊢) o a b c -> (⊢) o a (d, b) (d, c)
constrainedSecond forall (a :: * -> * -> *) d b c.
(Morphism a, ObjectPair a d b, ObjectPair a d c) =>
a b c -> a (d, b) (d, c)
second
  ConstrainedMorphism a b c
a *** :: forall b b' c c'.
(ObjectPair (o ⊢ a) b b', ObjectPair (o ⊢ a) c c') =>
(⊢) o a b c -> (⊢) o a b' c' -> (⊢) o a (b, b') (c, c')
*** ConstrainedMorphism a b' c'
b = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a b c
a forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a b' c'
b
  
instance (PreArrow a, o (UnitObject a)) => PreArrow (o⊢a) where
  ConstrainedMorphism a b c
a &&& :: forall b c c'.
(Object (o ⊢ a) b, ObjectPair (o ⊢ a) c c') =>
(⊢) o a b c -> (⊢) o a b c' -> (⊢) o a b (c, c')
&&& ConstrainedMorphism a b c'
b = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a b c
a forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& a b c'
b
  terminal :: forall b. Object (o ⊢ a) b => (⊢) o a b (UnitObject (o ⊢ a))
terminal = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
  fst :: forall x y. ObjectPair (o ⊢ a) x y => (⊢) o a (x, y) x
fst = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst
  snd :: forall x y. ObjectPair (o ⊢ a) x y => (⊢) o a (x, y) y
snd = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd

instance (WellPointed a, o (UnitObject a)) => WellPointed (o⊢a) where
  type PointObject (o⊢a) x = PointObject a x
  globalElement :: forall x.
ObjectPoint (o ⊢ a) x =>
x -> (⊢) o a (UnitObject (o ⊢ a)) x
globalElement x
x = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement x
x
  unit :: CatTagged (o ⊢ a) (UnitObject (o ⊢ a))
unit = forall (a :: * -> * -> *) (o :: * -> Constraint).
(WellPointed a, o (UnitObject a)) =>
CatTagged (o ⊢ a) (UnitObject a)
cstrCatUnit
  const :: forall b x.
(Object (o ⊢ a) b, ObjectPoint (o ⊢ a) x) =>
x -> (⊢) o a b x
const x
x = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const x
x

cstrCatUnit :: forall a o . (WellPointed a, o (UnitObject a))
        => CatTagged (o⊢a) (UnitObject a)
cstrCatUnit :: forall (a :: * -> * -> *) (o :: * -> Constraint).
(WellPointed a, o (UnitObject a)) =>
CatTagged (o ⊢ a) (UnitObject a)
cstrCatUnit = forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (forall (a :: * -> * -> *).
WellPointed a =>
CatTagged a (UnitObject a)
unit :: CatTagged a (UnitObject a))
  
instance (EnhancedCat a k, o (UnitObject a))
            => EnhancedCat (o⊢a) k where
  arr :: forall b c.
(Object k b, Object k c, Object (o ⊢ a) b, Object (o ⊢ a) c) =>
k b c -> (⊢) o a b c
arr = forall (k :: * -> * -> *) (a :: * -> * -> *) (o :: * -> Constraint)
       b c.
(Category k, Category a, o b, o c) =>
(k b c -> a b c) -> k b c -> (⊢) o a b c
constrainedArr forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr


constrainedLeft :: ( CoCartesian k, ObjectSum k b d, ObjectSum k c d )
  => (    k  b c ->    k  (b+d) (c+d) )
    -> (o⊢k) b c -> (o⊢k) (b+d) (c+d)
constrainedLeft :: forall (k :: * -> * -> *) b d c (o :: * -> Constraint).
(CoCartesian k, ObjectSum k b d, ObjectSum k c d) =>
(k b c -> k (b + d) (c + d))
-> (⊢) o k b c -> (⊢) o k (b + d) (c + d)
constrainedLeft k b c -> k (b + d) (c + d)
fs = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k b c -> k (b + d) (c + d)
fs forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained
  
constrainedRight :: ( CoCartesian k, ObjectSum k b c, ObjectSum k b d )
  => (    k  c d ->    k  (b+c) (b+d) )
    -> (o⊢k) c d -> (o⊢k) (b+c) (b+d)
constrainedRight :: forall (k :: * -> * -> *) b c d (o :: * -> Constraint).
(CoCartesian k, ObjectSum k b c, ObjectSum k b d) =>
(k c d -> k (b + c) (b + d))
-> (⊢) o k c d -> (⊢) o k (b + c) (b + d)
constrainedRight k c d -> k (b + c) (b + d)
fs = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k c d -> k (b + c) (b + d)
fs forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
Category k =>
(⊢) o k a b -> k a b
unconstrained

instance (MorphChoice k, o (ZeroObject k)) => MorphChoice (o⊢k) where
  left :: forall b d c.
(ObjectSum (o ⊢ k) b d, ObjectSum (o ⊢ k) c d) =>
(⊢) o k b c -> (⊢) o k (b + d) (c + d)
left = forall (k :: * -> * -> *) b d c (o :: * -> Constraint).
(CoCartesian k, ObjectSum k b d, ObjectSum k c d) =>
(k b c -> k (b + d) (c + d))
-> (⊢) o k b c -> (⊢) o k (b + d) (c + d)
constrainedLeft forall (a :: * -> * -> *) b d c.
(MorphChoice a, ObjectSum a b d, ObjectSum a c d) =>
a b c -> a (b + d) (c + d)
left
  right :: forall d b c.
(ObjectSum (o ⊢ k) d b, ObjectSum (o ⊢ k) d c) =>
(⊢) o k b c -> (⊢) o k (d + b) (d + c)
right = forall (k :: * -> * -> *) b c d (o :: * -> Constraint).
(CoCartesian k, ObjectSum k b c, ObjectSum k b d) =>
(k c d -> k (b + c) (b + d))
-> (⊢) o k c d -> (⊢) o k (b + c) (b + d)
constrainedRight forall (a :: * -> * -> *) d b c.
(MorphChoice a, ObjectSum a d b, ObjectSum a d c) =>
a b c -> a (d + b) (d + c)
right
  ConstrainedMorphism k b c
a +++ :: forall b b' c c'.
(ObjectSum (o ⊢ k) b b', ObjectSum (o ⊢ k) c c') =>
(⊢) o k b c -> (⊢) o k b' c' -> (⊢) o k (b + b') (c + c')
+++ ConstrainedMorphism k b' c'
b = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k b c
a forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++ k b' c'
b
  
instance (PreArrChoice k, o (ZeroObject k)) => PreArrChoice (o⊢k) where
  ConstrainedMorphism k b c
a ||| :: forall b b' c.
(ObjectSum (o ⊢ k) b b', Object (o ⊢ k) c) =>
(⊢) o k b c -> (⊢) o k b' c -> (⊢) o k (b + b') c
||| ConstrainedMorphism k b' c
b = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k b c
a forall (k :: * -> * -> *) b b' c.
(PreArrChoice k, ObjectSum k b b', Object k c) =>
k b c -> k b' c -> k (b + b') c
||| k b' c
b
  initial :: forall b. Object (o ⊢ k) b => (⊢) o k (ZeroObject (o ⊢ k)) b
initial = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) b.
(PreArrChoice k, Object k b) =>
k (ZeroObject k) b
initial
  coFst :: forall a b. ObjectSum (o ⊢ k) a b => (⊢) o k a (a + b)
coFst = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k a (a + b)
coFst
  coSnd :: forall a b. ObjectSum (o ⊢ k) a b => (⊢) o k b (a + b)
coSnd = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a b.
(PreArrChoice k, ObjectSum k a b) =>
k b (a + b)
coSnd

instance (SPDistribute k, o (ZeroObject k), o (UnitObject k))
     => SPDistribute (o⊢k) where
  distribute :: forall a b c.
(ObjectSum (o ⊢ k) (a, b) (a, c), ObjectPair (o ⊢ k) a (b + c),
 ObjectSum (o ⊢ k) b c, PairObjects (o ⊢ k) a b,
 PairObjects (o ⊢ k) a c) =>
(⊢) o k (a, b + c) ((a, b) + (a, c))
distribute = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
 ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k (a, b + c) ((a, b) + (a, c))
distribute
  unDistribute :: forall a b c.
(ObjectSum (o ⊢ k) (a, b) (a, c), ObjectPair (o ⊢ k) a (b + c),
 ObjectSum (o ⊢ k) b c, PairObjects (o ⊢ k) a b,
 PairObjects (o ⊢ k) a c) =>
(⊢) o k ((a, b) + (a, c)) (a, b + c)
unDistribute = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a b c.
(SPDistribute k, ObjectSum k (a, b) (a, c), ObjectPair k a (b + c),
 ObjectSum k b c, PairObjects k a b, PairObjects k a c) =>
k ((a, b) + (a, c)) (a, b + c)
unDistribute
  boolAsSwitch :: forall a.
(ObjectSum (o ⊢ k) a a, ObjectPair (o ⊢ k) Bool a) =>
(⊢) o k (Bool, a) (a + a)
boolAsSwitch = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (Bool, a) (a + a)
boolAsSwitch
  boolFromSwitch :: forall a.
(ObjectSum (o ⊢ k) a a, ObjectPair (o ⊢ k) Bool a) =>
(⊢) o k (a + a) (Bool, a)
boolFromSwitch = forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism forall (k :: * -> * -> *) a.
(SPDistribute k, ObjectSum k a a, ObjectPair k Bool a) =>
k (a + a) (Bool, a)
boolFromSwitch
  


-- | Basically 'ifThenElse' with inverted argument order, and
--   \"morphismised\" arguments.
choose :: (Arrow f (->), Function f, Object f Bool, Object f a)
     => f (UnitObject f) a  -- ^ \"'False'\" value
     -> f (UnitObject f) a  -- ^ \"'True'\" value
     -> f Bool           a
choose :: forall (f :: * -> * -> *) a.
(Arrow f (->), Function f, Object f Bool, Object f a) =>
f (UnitObject f) a -> f (UnitObject f) a -> f Bool a
choose f (UnitObject f) a
fv f (UnitObject f) a
tv = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Bool
c -> if Bool
c then forall (f :: * -> * -> *) x.
(WellPointed f, Function f, Object f x) =>
f (UnitObject f) x -> x
value f (UnitObject f) a
tv else forall (f :: * -> * -> *) x.
(WellPointed f, Function f, Object f x) =>
f (UnitObject f) x -> x
value f (UnitObject f) a
fv

ifThenElse :: ( EnhancedCat f (->), Function f
              , Object f Bool, Object f a, Object f (f a a), Object f (f a (f a a))
              ) => Bool `f` (a `f` (a `f` a))
ifThenElse :: forall (f :: * -> * -> *) a.
(EnhancedCat f (->), Function f, Object f Bool, Object f a,
 Object f (f a a), Object f (f a (f a a))) =>
f Bool (f a (f a a))
ifThenElse = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Bool
c -> forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \a
tv -> forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \a
fv -> if Bool
c then a
tv else a
fv

 


genericAgentCombine :: ( HasAgent k, PreArrow k
                       , Object k a, ObjectPair k b c, Object k d )
     => k (b,c) d -> GenericAgent k a b -> GenericAgent k a c -> GenericAgent k a d
genericAgentCombine :: forall (k :: * -> * -> *) a b c d.
(HasAgent k, PreArrow k, Object k a, ObjectPair k b c,
 Object k d) =>
k (b, c) d
-> GenericAgent k a b -> GenericAgent k a c -> GenericAgent k a d
genericAgentCombine k (b, c) d
m (GenericAgent k a b
v) (GenericAgent k a c
w)
       = forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (b, c) d
m forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. (k a b
v forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& k a c
w)
  
genericUnit :: ( PreArrow k, HasAgent k, Object k a )
        => GenericAgent k a (UnitObject k)
genericUnit :: forall (k :: * -> * -> *) a.
(PreArrow k, HasAgent k, Object k a) =>
GenericAgent k a (UnitObject k)
genericUnit = forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal


class (Morphism k, HasAgent k) => CartesianAgent k where
  alg1to2 :: ( Object k a, ObjectPair k b c
          ) => (forall q . Object k q
                 => AgentVal k q a -> (AgentVal k q b, AgentVal k q c) )
               -> k a (b,c)
  alg2to1 :: ( ObjectPair k a b, Object k c
          ) => (forall q . Object k q
                 => AgentVal k q a -> AgentVal k q b -> AgentVal k q c )
               -> k (a,b) c
  alg2to2 :: ( ObjectPair k a b, ObjectPair k c d
          ) => (forall q . Object k q
                 => AgentVal k q a -> AgentVal k q b -> (AgentVal k q c, AgentVal k q d) )
               -> k (a,b) (c,d)

genericAlg1to2 :: ( PreArrow k, u ~ UnitObject k
                  , Object k a, ObjectPair k b c
                  ) => ( forall q . Object k q
                      => GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c) )
               -> k a (b,c)
genericAlg1to2 :: forall (k :: * -> * -> *) u a b c.
(PreArrow k, u ~ UnitObject k, Object k a, ObjectPair k b c) =>
(forall q.
 Object k q =>
 GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c))
-> k a (b, c)
genericAlg1to2 forall q.
Object k q =>
GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c)
f = forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent GenericAgent k a b
b forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent GenericAgent k a c
c
 where (GenericAgent k a b
b,GenericAgent k a c
c) = forall q.
Object k q =>
GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c)
f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
genericAlg2to1 :: ( PreArrow k, u ~ UnitObject k
                  , ObjectPair k a u, ObjectPair k a b, ObjectPair k b u, ObjectPair k b a
                  ) => ( forall q . Object k q
                      => GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c )
               -> k (a,b) c
genericAlg2to1 :: forall (k :: * -> * -> *) u a b c.
(PreArrow k, u ~ UnitObject k, ObjectPair k a u, ObjectPair k a b,
 ObjectPair k b u, ObjectPair k b a) =>
(forall q.
 Object k q =>
 GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c)
-> k (a, b) c
genericAlg2to1 forall q.
Object k q =>
GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c
f = forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall q.
Object k q =>
GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c
f (forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst) (forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd)
genericAlg2to2 :: ( PreArrow k, u ~ UnitObject k
                  , ObjectPair k a u, ObjectPair k a b, ObjectPair k c d
                  , ObjectPair k b u, ObjectPair k b a
                  ) => ( forall q . Object k q
                      => GenericAgent k q a -> GenericAgent k q b 
                         -> (GenericAgent k q c, GenericAgent k q d) )
               -> k (a,b) (c,d)
genericAlg2to2 :: forall (k :: * -> * -> *) u a b c d.
(PreArrow k, u ~ UnitObject k, ObjectPair k a u, ObjectPair k a b,
 ObjectPair k c d, ObjectPair k b u, ObjectPair k b a) =>
(forall q.
 Object k q =>
 GenericAgent k q a
 -> GenericAgent k q b -> (GenericAgent k q c, GenericAgent k q d))
-> k (a, b) (c, d)
genericAlg2to2 forall q.
Object k q =>
GenericAgent k q a
-> GenericAgent k q b -> (GenericAgent k q c, GenericAgent k q d)
f = forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent GenericAgent k (a, b) c
c forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
GenericAgent k a v -> k a v
runGenericAgent GenericAgent k (a, b) d
d
 where (GenericAgent k (a, b) c
c,GenericAgent k (a, b) d
d) = forall q.
Object k q =>
GenericAgent k q a
-> GenericAgent k q b -> (GenericAgent k q c, GenericAgent k q d)
f (forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst) (forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd)


class (HasAgent k, AgentVal k a x ~ p a x) 
           => PointAgent p k a x | p -> k where
  point :: (Object k a, Object k x) => x -> p a x

genericPoint :: ( WellPointed k, Object k a, ObjectPoint k x )
       => x -> GenericAgent k a x
genericPoint :: forall (k :: * -> * -> *) a x.
(WellPointed k, Object k a, ObjectPoint k x) =>
x -> GenericAgent k a x
genericPoint x
x = forall {k} {k} (k :: k -> k -> *) (a :: k) (v :: k).
k a v -> GenericAgent k a v
GenericAgent forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const x
x



-- | Imitate a type change in a different category. This is usually possible
--   for type changes that are no-ops at runtime, in particular for newtype wrappers.
follow :: (EnhancedCat k Coercion, Coercible a b, Object k a, Object k b)
                 => p a b -> k a b
follow :: forall (k :: * -> * -> *) a b (p :: * -> * -> *).
(EnhancedCat k Coercion, Coercible a b, Object k a, Object k b) =>
p a b -> k a b
follow p a b
_ = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

-- | The opposite of 'follow'.
flout :: (EnhancedCat k Coercion, Coercible b a, Object k a, Object k b)
                 => p a b -> k b a
flout :: forall (k :: * -> * -> *) b a (p :: * -> * -> *).
(EnhancedCat k Coercion, Coercible b a, Object k a, Object k b) =>
p a b -> k b a
flout p a b
_ = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

-- | Wrap an endomorphism in inverse coercions, to have it work on any type
--   that's representationally equivalent to the one in the morphism's signature.
--   This is a specialised version of 'pretendLike'.
pretend :: (EnhancedCat k Coercion, Object k a, Object k b)
                  => Coercion a b -> k a a -> k b b
pretend :: forall (k :: * -> * -> *) a b.
(EnhancedCat k Coercion, Object k a, Object k b) =>
Coercion a b -> k a a -> k b b
pretend Coercion a b
crc k a a
f = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr Coercion a b
crc forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a a
f forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr (forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a
sym Coercion a b
crc)

-- | Equivalent to @'pretend' . 'sym'@.
swallow :: (EnhancedCat k Coercion, Object k a, Object k b)
                  => Coercion b a -> k a a -> k b b
swallow :: forall (k :: * -> * -> *) a b.
(EnhancedCat k Coercion, Object k a, Object k b) =>
Coercion b a -> k a a -> k b b
swallow Coercion b a
crc k a a
f = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr (forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a
sym Coercion b a
crc) forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a a
f forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr Coercion b a
crc

-- | This works much like <http://hackage.haskell.org/package/newtype-0.2/docs/Control-Newtype.html#v:over over>:
--   wrap a morphism in any coercions required so the result types match.
--   This will often be too polymorphic for the type checker; consider using the
--   more explicit 'follow' and 'flout'.
pretendLike :: ( EnhancedCat k Coercion, Coercible b a, Coercible c d
               , Object k a, Object k b, Object k c, Object k d )
                   => p c d -> k a c -> k b d
pretendLike :: forall (k :: * -> * -> *) b a c d (p :: * -> * -> *).
(EnhancedCat k Coercion, Coercible b a, Coercible c d, Object k a,
 Object k b, Object k c, Object k d) =>
p c d -> k a c -> k b d
pretendLike p c d
_ k a c
f = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a c
f forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion


-- | Generalised coercion analogue of
--   <http://hackage.haskell.org/package/newtype-0.2/docs/Control-Newtype.html#v:under under>.
swallowLike :: ( EnhancedCat k Coercion, Coercible b a, Coercible c d
               , Object k a, Object k b, Object k c, Object k d )
                   => p b a -> k a c -> k b d
swallowLike :: forall (k :: * -> * -> *) b a c d (p :: * -> * -> *).
(EnhancedCat k Coercion, Coercible b a, Coercible c d, Object k a,
 Object k b, Object k c, Object k d) =>
p b a -> k a c -> k b d
swallowLike p b a
_ k a c
f = forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. k a c
f forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion