-- |
-- 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
(>>>) = (k b c -> k a b -> k a c) -> k a b -> k b c -> k a c
forall a b c. (a -> b -> c) -> b -> a -> c
flip k b c -> k a b -> k a c
forall a b c.
(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
(.)
(<<<) :: (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
(<<<) = k b c -> k a b -> k a c
forall a b c.
(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 = (a b c -> a d d -> a (b, d) (c, d)
forall b b' c c'.
(ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
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 d d
forall a. Object a a => a a a
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 = (a d d
forall a. Object a a => a a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
ida d d -> a b c -> a (d, b) (d, c)
forall b b' c c'.
(ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
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')
***)
  (***) :: ( 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 = (a b c -> a d d -> a (b + d) (c + d)
forall b b' c c'.
(ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
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')
+++a d d
forall a. Object a a => a a a
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 = (a d d
forall a. Object a a => a a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
ida d d -> a b c -> a (d + b) (d + c)
forall b b' c c'.
(ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
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')
+++)
  (+++) :: ( 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 = k (a, b + c) ((a, b) + (a, c))
forall a b c.
(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))
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 = k ((a, b) + (a, c)) (a, b + c)
forall a b c.
(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)
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 = k (Bool, a) (a + a)
forall a.
(ObjectSum k a a, ObjectPair k Bool a) =>
k (Bool, a) (a + a)
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 = k (a + a) (Bool, a)
forall a.
(ObjectSum k a a, ObjectPair k Bool a) =>
k (a + a) (Bool, a)
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 = x -> a (UnitObject a) x
forall b x. (Object a b, ObjectPoint a x) => x -> a b x
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 = x -> a (UnitObject a) x
forall x. ObjectPoint a x => x -> a (UnitObject a) x
forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement x
x a (UnitObject a) x -> a b (UnitObject a) -> a b x
forall a b c.
(Object a a, Object a b, Object a c) =>
a b c -> a a b -> a 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
. a b (UnitObject a)
forall b. Object a b => a b (UnitObject a)
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 f (UnitObject f) x -> UnitObject f -> x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Tagged (f (UnitObject f) (UnitObject f)) (UnitObject f)
-> UnitObject f
forall {k} (s :: k) b. Tagged s b -> b
untag(Tagged (f (UnitObject f) (UnitObject f)) (UnitObject f)
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 = k b c -> k b c
forall a. Object (->) a => a -> a
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 = b -> b
b -> c
forall a. Object (->) a => a -> a
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 = Coercion b c
Coercion c c
forall a. Object Coercion a => Coercion a a
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 = ConstrainedCategory f o b c
ConstrainedCategory f o c c
forall a. Object (o ⊢ f) a => ConstrainedCategory f o a a
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 = f a b -> a -> b
forall b c.
(Object f b, Object f c, Object (->) b, Object (->) c) =>
f b c -> b -> 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 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) = f b c -> b -> c
forall b c.
(Object f b, Object f c, Object (->) b, Object (->) c) =>
f b c -> b -> 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 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) = f b c -> Discrete b c
forall b c.
(Object f b, Object f c, Object Discrete b, Object Discrete c) =>
f b c -> Discrete b 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 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 = Coercion b c -> b -> c
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 = (b -> c) -> (b, d) -> (c, d)
forall b c d. (b -> c) -> (b, d) -> (c, d)
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 = (b -> c) -> (d, b) -> (d, c)
forall b c d. (b -> c) -> (d, b) -> (d, c)
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')
(***) = (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall b c b' 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 = (b -> c) -> Either b d -> Either c d
forall b c d. (b -> c) -> Either b d -> Either c d
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 = (b -> c) -> Either d b -> Either d c
forall b c d. (b -> c) -> Either d b -> Either d c
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')
(+++) = (b -> c) -> (b' -> c') -> Either b b' -> Either c c'
forall b c b' c'.
(b -> c) -> (b' -> c') -> Either b b' -> Either 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')
(&&&) = (b -> c) -> (b -> c') -> b -> (c, c')
forall b 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 = () -> b -> ()
forall b x. (Object (->) b, ObjectPoint (->) x) => x -> b -> x
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
(|||) = (b -> c) -> (b' -> c) -> Either b b' -> c
forall b d c. (b -> d) -> (c -> d) -> Either b c -> d
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 = a -> Either a b
forall a b. a -> Either a b
Left a
a
  coSnd :: forall a b. ObjectSum (->) a b => b -> (a + b)
coSnd b
b = b -> Either a b
forall a b. b -> Either a b
Right b
b
  initial :: forall b. Object (->) b => ZeroObject (->) -> b
initial = Void -> b
ZeroObject (->) -> b
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) = (a, b) -> Either (a, b) (a, c)
forall a b. a -> Either a b
Left (a
a,b
b)
  distribute (a
a, Right c
c) = (a, c) -> Either (a, b) (a, 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, b -> b + c
forall a b. a -> Either a b
Left b
b)
  unDistribute (Right (a
a,c
c)) = (a
a, c -> b + c
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) = a -> Either a a
forall a b. a -> Either a b
Left a
a
  boolAsSwitch (Bool
True, a
a) = a -> Either 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 = x -> () -> x
x -> UnitObject (->) -> x
forall a b. a -> b -> a
Hask.const
  unit :: CatTagged (->) (UnitObject (->))
unit = () -> Tagged (() -> ()) ()
forall a. a -> Tagged (() -> ()) a
forall (f :: * -> *) a. Applicative f => a -> f a
Hask.pure ()
  const :: forall b x. (Object (->) b, ObjectPoint (->) x) => x -> b -> x
const = x -> b -> x
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)
fk (LFactor b) (LFactor c)
-> k (LFactor b') (LFactor c')
-> k (LFactor b, LFactor b') (LFactor c, LFactor c')
forall b b' c c'.
(ObjectPair k b b', ObjectPair k c c') =>
k b c -> k b' c' -> k (b, b') (c, c')
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')
***k (LFactor b') (LFactor c')
h) k (LFactor (b, b')) (LFactor (c, c'))
-> l (RFactor (b, b')) (RFactor (c, c'))
-> ProductCategory k l (b, b') (c, c')
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)
gl (RFactor b) (RFactor c)
-> l (RFactor b') (RFactor c')
-> l (RFactor b, RFactor b') (RFactor c, RFactor c')
forall b b' c c'.
(ObjectPair l b b', ObjectPair l c c') =>
l b c -> l b' c' -> l (b, b') (c, c')
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')
***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)
fk (LFactor b) (LFactor c)
-> k (LFactor b) (LFactor c')
-> k (LFactor b) (LFactor c, LFactor c')
forall b c c'.
(Object k b, ObjectPair k c c') =>
k b c -> k b c' -> k 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')
&&&k (LFactor b) (LFactor c')
h) k (LFactor b) (LFactor (c, c'))
-> l (RFactor b) (RFactor (c, c')) -> ProductCategory k l b (c, c')
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)
gl (RFactor b) (RFactor c)
-> l (RFactor b) (RFactor c')
-> l (RFactor b) (RFactor c, RFactor c')
forall b c c'.
(Object l b, ObjectPair l c c') =>
l b c -> l b c' -> l 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')
&&&l (RFactor b) (RFactor c')
i)
  terminal :: forall b. Object (k × l) b => (×) k l b (UnitObject (k × l))
terminal = k (LFactor b)
  (LFactor (ProductCatObj (UnitObject k) (UnitObject l)))
k (LFactor b) (UnitObject k)
forall b. Object k b => k b (UnitObject k)
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal k (LFactor b)
  (LFactor (ProductCatObj (UnitObject k) (UnitObject l)))
-> l (RFactor b)
     (RFactor (ProductCatObj (UnitObject k) (UnitObject l)))
-> ProductCategory
     k l b (ProductCatObj (UnitObject k) (UnitObject l))
forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: l (RFactor b)
  (RFactor (ProductCatObj (UnitObject k) (UnitObject l)))
l (RFactor b) (UnitObject l)
forall b. Object l b => l b (UnitObject l)
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 = k (LFactor x, LFactor y) (LFactor x)
k (LFactor (x, y)) (LFactor x)
forall x y. ObjectPair k x y => k (x, y) x
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst k (LFactor (x, y)) (LFactor x)
-> l (RFactor (x, y)) (RFactor x) -> ProductCategory k l (x, y) x
forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: l (RFactor x, RFactor y) (RFactor x)
l (RFactor (x, y)) (RFactor x)
forall x y. ObjectPair l x y => l (x, y) x
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 = k (LFactor x, LFactor y) (LFactor y)
k (LFactor (x, y)) (LFactor y)
forall x y. ObjectPair k x y => k (x, y) y
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd k (LFactor (x, y)) (LFactor y)
-> l (RFactor (x, y)) (RFactor y) -> ProductCategory k l (x, y) y
forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: l (RFactor x, RFactor y) (RFactor y)
l (RFactor (x, y)) (RFactor y)
forall x y. ObjectPair l x y => l (x, y) y
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 = ProductCatObj (UnitObject k) (UnitObject l)
-> Tagged
     ((×)
        k
        l
        (ProductCatObj (UnitObject k) (UnitObject l))
        (ProductCatObj (UnitObject k) (UnitObject l)))
     (ProductCatObj (UnitObject k) (UnitObject l))
forall {k} (s :: k) b. b -> Tagged s b
Tagged (ProductCatObj (UnitObject k) (UnitObject l)
 -> Tagged
      ((×)
         k
         l
         (ProductCatObj (UnitObject k) (UnitObject l))
         (ProductCatObj (UnitObject k) (UnitObject l)))
      (ProductCatObj (UnitObject k) (UnitObject l)))
-> ProductCatObj (UnitObject k) (UnitObject l)
-> Tagged
     ((×)
        k
        l
        (ProductCatObj (UnitObject k) (UnitObject l))
        (ProductCatObj (UnitObject k) (UnitObject l)))
     (ProductCatObj (UnitObject k) (UnitObject l))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ UnitObject k
-> UnitObject l -> ProductCatObj (UnitObject k) (UnitObject l)
forall a b. a -> b -> ProductCatObj a b
ProductCatObj UnitObject k
uk UnitObject l
ul
 where Tagged UnitObject k
uk = Tagged (k (UnitObject k) (UnitObject k)) (UnitObject k)
forall (a :: * -> * -> *).
WellPointed a =>
CatTagged a (UnitObject a)
unit :: Tagged (k (UnitObject k) (UnitObject k)) (UnitObject k)
       Tagged UnitObject l
ul = Tagged (l (UnitObject l) (UnitObject l)) (UnitObject l)
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 = Tagged
  ((×)
     k
     l
     (ProductCatObj (UnitObject k) (UnitObject l))
     (ProductCatObj (UnitObject k) (UnitObject l)))
  (ProductCatObj (UnitObject k) (UnitObject l))
CatTagged (k × l) (UnitObject (k × l))
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 = LFactor x -> k (LFactor b) (LFactor x)
forall b x. (Object k b, ObjectPoint k x) => x -> k b x
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (x -> LFactor x
forall t. IsProduct t => t -> LFactor t
lfactorProj x
c) k (LFactor b) (LFactor x)
-> l (RFactor b) (RFactor x) -> ProductCategory k l b x
forall (k :: * -> * -> *) (l :: * -> * -> *) p q.
k (LFactor p) (LFactor q)
-> l (RFactor p) (RFactor q) -> ProductCategory k l p q
:***: RFactor x -> l (RFactor b) (RFactor x)
forall b x. (Object l b, ObjectPoint l x) => x -> l b x
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (x -> RFactor x
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 = a b c -> (⊢) o a b c
forall (o :: * -> Constraint) (k :: * -> * -> *) a b.
(Category k, o a, o b) =>
k a b -> (⊢) o k a b
constrained (a b c -> (⊢) o a b c) -> (k b c -> a b c) -> k b c -> (⊢) o a b c
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> 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
. 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 = a (b, d) (c, d) -> (⊢) o a (b, d) (c, d)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a (b, d) (c, d) -> (⊢) o a (b, d) (c, d))
-> ((⊢) o a b c -> a (b, d) (c, d))
-> (⊢) o a b c
-> (⊢) o a (b, d) (c, d)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> 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
. a b c -> a (b, d) (c, d)
fs (a b c -> a (b, d) (c, d))
-> ((⊢) o a b c -> a b c) -> (⊢) o a b c -> a (b, d) (c, d)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> 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
. (⊢) o a b c -> a b 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 = a (d, b) (d, c) -> (⊢) o a (d, b) (d, c)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a (d, b) (d, c) -> (⊢) o a (d, b) (d, c))
-> ((⊢) o a b c -> a (d, b) (d, c))
-> (⊢) o a b c
-> (⊢) o a (d, b) (d, c)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> 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
. a b c -> a (d, b) (d, c)
sn (a b c -> a (d, b) (d, c))
-> ((⊢) o a b c -> a b c) -> (⊢) o a b c -> a (d, b) (d, c)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> 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
. (⊢) o a b c -> a b 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) = ((c, d) -> (b, d)) -> Op (b, d) (c, d)
forall a b. (b -> a) -> Op a b
Hask.Op (((c, d) -> (b, d)) -> Op (b, d) (c, d))
-> ((c, d) -> (b, d)) -> Op (b, d) (c, d)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (c -> b) -> (c, d) -> (b, d)
forall b d c.
(ObjectPair (->) b d, ObjectPair (->) c d) =>
(b -> c) -> (b, d) -> (c, d)
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) = ((d, c) -> (d, b)) -> Op (d, b) (d, c)
forall a b. (b -> a) -> Op a b
Hask.Op (((d, c) -> (d, b)) -> Op (d, b) (d, c))
-> ((d, c) -> (d, b)) -> Op (d, b) (d, c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (c -> b) -> (d, c) -> (d, b)
forall d b c.
(ObjectPair (->) d b, ObjectPair (->) d c) =>
(b -> c) -> (d, b) -> (d, c)
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 = ((c, c') -> (b, b')) -> Op (b, b') (c, c')
forall a b. (b -> a) -> Op a b
Hask.Op (((c, c') -> (b, b')) -> Op (b, b') (c, c'))
-> ((c, c') -> (b, b')) -> Op (b, b') (c, c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ c -> b
f (c -> b) -> (c' -> b') -> (c, c') -> (b, b')
forall b b' c c'.
(ObjectPair (->) b b', ObjectPair (->) c c') =>
(b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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) = ((c + d) -> b + d) -> Op (b + d) (c + d)
forall a b. (b -> a) -> Op a b
Hask.Op (((c + d) -> b + d) -> Op (b + d) (c + d))
-> ((c + d) -> b + d) -> Op (b + d) (c + d)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (c -> b) -> (c + d) -> b + d
forall b d c.
(ObjectSum (->) b d, ObjectSum (->) c d) =>
(b -> c) -> (b + d) -> (c + d)
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) = ((d + c) -> d + b) -> Op (d + b) (d + c)
forall a b. (b -> a) -> Op a b
Hask.Op (((d + c) -> d + b) -> Op (d + b) (d + c))
-> ((d + c) -> d + b) -> Op (d + b) (d + c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (c -> b) -> (d + c) -> d + b
forall d b c.
(ObjectSum (->) d b, ObjectSum (->) d c) =>
(b -> c) -> (d + b) -> (d + c)
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 = ((c + c') -> b + b') -> Op (b + b') (c + c')
forall a b. (b -> a) -> Op a b
Hask.Op (((c + c') -> b + b') -> Op (b + b') (c + c'))
-> ((c + c') -> b + b') -> Op (b + b') (c + c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ c -> b
f (c -> b) -> (c' -> b') -> (c + c') -> b + b'
forall b b' c c'.
(ObjectSum (->) b b', ObjectSum (->) c c') =>
(b -> c) -> (b' -> c') -> (b + b') -> (c + c')
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 = (a b c -> a (b, d) (c, d)) -> (⊢) o a b c -> (⊢) o a (b, d) (c, d)
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)
forall b d c.
(ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
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 = (a b c -> a (d, b) (d, c)) -> (⊢) o a b c -> (⊢) o a (d, b) (d, c)
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)
forall d b c.
(ObjectPair a d b, ObjectPair a d c) =>
a b c -> a (d, b) (d, c)
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 = a (b, b') (c, c') -> (⊢) o a (b, b') (c, c')
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a (b, b') (c, c') -> (⊢) o a (b, b') (c, c'))
-> a (b, b') (c, c') -> (⊢) o a (b, b') (c, c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a b c
a a b c -> a b' c' -> a (b, b') (c, c')
forall b b' c c'.
(ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
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 = a b (c, c') -> (⊢) o a b (c, c')
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a b (c, c') -> (⊢) o a b (c, c'))
-> a b (c, c') -> (⊢) o a b (c, c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a b c
a a b c -> a b c' -> a b (c, c')
forall b c c'.
(Object a b, ObjectPair a c c') =>
a b c -> a b c' -> 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')
&&& a b c'
b
  terminal :: forall b. Object (o ⊢ a) b => (⊢) o a b (UnitObject (o ⊢ a))
terminal = a b (UnitObject a) -> ConstrainedCategory a o b (UnitObject a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism a b (UnitObject a)
forall b. Object a b => a b (UnitObject a)
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 = a (x, y) x -> ConstrainedCategory a o (x, y) x
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism a (x, y) x
forall x y. ObjectPair a x y => a (x, y) x
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 = a (x, y) y -> ConstrainedCategory a o (x, y) y
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism a (x, y) y
forall x y. ObjectPair a x y => a (x, y) y
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 = a (UnitObject a) x -> (⊢) o a (UnitObject a) x
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a (UnitObject a) x -> (⊢) o a (UnitObject a) x)
-> a (UnitObject a) x -> (⊢) o a (UnitObject a) x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x -> a (UnitObject a) x
forall x. ObjectPoint a x => x -> a (UnitObject a) x
forall (a :: * -> * -> *) x.
(WellPointed a, ObjectPoint a x) =>
x -> a (UnitObject a) x
globalElement x
x
  unit :: CatTagged (o ⊢ a) (UnitObject (o ⊢ a))
unit = CatTagged (o ⊢ a) (UnitObject a)
CatTagged (o ⊢ a) (UnitObject (o ⊢ a))
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 = a b x -> (⊢) o a b x
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (a b x -> (⊢) o a b x) -> a b x -> (⊢) o a b x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x -> a b x
forall b x. (Object a b, ObjectPoint a x) => x -> a b x
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 = Tagged (a (UnitObject a) (UnitObject a)) (UnitObject a)
-> Tagged ((⊢) o a (UnitObject a) (UnitObject a)) (UnitObject a)
forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (a (UnitObject a) (UnitObject a)) (UnitObject a)
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 = (k b c -> a b c) -> k b c -> (⊢) o a b c
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
forall b c.
(Object k b, Object k c, Object a b, Object a c) =>
k b c -> a b 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


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 = k (b + d) (c + d) -> (⊢) o k (b + d) (c + d)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k (b + d) (c + d) -> (⊢) o k (b + d) (c + d))
-> ((⊢) o k b c -> k (b + d) (c + d))
-> (⊢) o k b c
-> (⊢) o k (b + d) (c + d)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> 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
. k b c -> k (b + d) (c + d)
fs (k b c -> k (b + d) (c + d))
-> ((⊢) o k b c -> k b c) -> (⊢) o k b c -> k (b + d) (c + d)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> 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
. (⊢) o k b c -> k b 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 = k (b + c) (b + d) -> (⊢) o k (b + c) (b + d)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k (b + c) (b + d) -> (⊢) o k (b + c) (b + d))
-> ((⊢) o k c d -> k (b + c) (b + d))
-> (⊢) o k c d
-> (⊢) o k (b + c) (b + d)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> 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
. k c d -> k (b + c) (b + d)
fs (k c d -> k (b + c) (b + d))
-> ((⊢) o k c d -> k c d) -> (⊢) o k c d -> k (b + c) (b + d)
forall a b c.
(Object (->) a, Object (->) b, Object (->) c) =>
(b -> c) -> (a -> b) -> 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
. (⊢) o k c d -> k c d
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 = (k b c -> k (b + d) (c + d))
-> (⊢) o k b c -> (⊢) o k (b + d) (c + d)
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)
forall b d c.
(ObjectSum k b d, ObjectSum k c d) =>
k b c -> k (b + d) (c + d)
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 = (k b c -> k (d + b) (d + c))
-> (⊢) o k b c -> (⊢) o k (d + b) (d + c)
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 b c -> k (d + b) (d + c)
forall d b c.
(ObjectSum k d b, ObjectSum k d c) =>
k b c -> k (d + b) (d + c)
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 = k (b + b') (c + c') -> (⊢) o k (b + b') (c + c')
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k (b + b') (c + c') -> (⊢) o k (b + b') (c + c'))
-> k (b + b') (c + c') -> (⊢) o k (b + b') (c + c')
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k b c
a k b c -> k b' c' -> k (b + b') (c + c')
forall b b' c c'.
(ObjectSum k b b', ObjectSum k c c') =>
k b c -> k b' c' -> k (b + b') (c + c')
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 = k (b + b') c -> (⊢) o k (b + b') c
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism (k (b + b') c -> (⊢) o k (b + b') c)
-> k (b + b') c -> (⊢) o k (b + b') c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k b c
a k b c -> k b' c -> k (b + b') c
forall b b' c.
(ObjectSum k b b', Object k c) =>
k b c -> k b' c -> k (b + b') c
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 = k (ZeroObject k) b -> ConstrainedCategory k o (ZeroObject k) b
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k (ZeroObject k) b
forall b. Object k b => k (ZeroObject k) b
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 = k a (a + b) -> ConstrainedCategory k o a (a + b)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k a (a + b)
forall a b. ObjectSum k a b => k a (a + b)
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 = k b (a + b) -> ConstrainedCategory k o b (a + b)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k b (a + b)
forall a b. ObjectSum k a b => k b (a + b)
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 = k (a, b + c) ((a, b) + (a, c))
-> ConstrainedCategory k o (a, b + c) ((a, b) + (a, c))
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k (a, b + c) ((a, b) + (a, c))
forall a b c.
(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))
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 = k ((a, b) + (a, c)) (a, b + c)
-> ConstrainedCategory k o ((a, b) + (a, c)) (a, b + c)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k ((a, b) + (a, c)) (a, b + c)
forall a b c.
(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)
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 = k (Bool, a) (a + a) -> ConstrainedCategory k o (Bool, a) (a + a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k (Bool, a) (a + a)
forall a.
(ObjectSum k a a, ObjectPair k Bool a) =>
k (Bool, a) (a + a)
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 = k (a + a) (Bool, a) -> ConstrainedCategory k o (a + a) (Bool, a)
forall (k :: * -> * -> *) (o :: * -> Constraint) a b.
k a b -> ConstrainedCategory k o a b
ConstrainedMorphism k (a + a) (Bool, a)
forall a.
(ObjectSum k a a, ObjectPair k Bool a) =>
k (a + a) (Bool, a)
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 = (Bool -> a) -> f Bool a
forall b c.
(Object (->) b, Object (->) c, Object f b, Object f c) =>
(b -> c) -> f b 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 ((Bool -> a) -> f Bool a) -> (Bool -> a) -> f Bool a
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Bool
c -> if Bool
c then f (UnitObject f) a -> a
forall (f :: * -> * -> *) x.
(WellPointed f, Function f, Object f x) =>
f (UnitObject f) x -> x
value f (UnitObject f) a
tv else f (UnitObject f) a -> a
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 = (Bool -> f a (f a a)) -> f Bool (f a (f a a))
forall b c.
(Object (->) b, Object (->) c, Object f b, Object f c) =>
(b -> c) -> f b 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 ((Bool -> f a (f a a)) -> f Bool (f a (f a a)))
-> (Bool -> f a (f a a)) -> f Bool (f a (f a a))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Bool
c -> (a -> f a a) -> f a (f a a)
forall b c.
(Object (->) b, Object (->) c, Object f b, Object f c) =>
(b -> c) -> f b 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 ((a -> f a a) -> f a (f a a)) -> (a -> f a a) -> f a (f a a)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \a
tv -> (a -> a) -> f a a
forall b c.
(Object (->) b, Object (->) c, Object f b, Object f c) =>
(b -> c) -> f b 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 ((a -> a) -> f a a) -> (a -> a) -> f a a
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)
       = k a d -> GenericAgent k a d
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (v :: k1).
k2 a v -> GenericAgent k2 a v
GenericAgent (k a d -> GenericAgent k a d) -> k a d -> GenericAgent k a d
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k (b, c) d
m k (b, c) d -> k a (b, c) -> k a d
forall a b c.
(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
. (k a b
v k a b -> k a c -> k a (b, c)
forall b c c'.
(Object k b, ObjectPair k c c') =>
k b c -> k b c' -> k 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')
&&& 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 = k a (UnitObject k) -> GenericAgent k a (UnitObject k)
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (v :: k1).
k2 a v -> GenericAgent k2 a v
GenericAgent k a (UnitObject k)
forall b. Object k b => k b (UnitObject k)
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 = GenericAgent k a b -> k a b
forall {k1} {k2} (k3 :: k1 -> k2 -> *) (a :: k1) (v :: k2).
GenericAgent k3 a v -> k3 a v
runGenericAgent GenericAgent k a b
b k a b -> k a c -> k a (b, c)
forall b c c'.
(Object k b, ObjectPair k c c') =>
k b c -> k b c' -> k 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')
&&& GenericAgent k a c -> k a c
forall {k1} {k2} (k3 :: k1 -> k2 -> *) (a :: k1) (v :: k2).
GenericAgent k3 a v -> k3 a v
runGenericAgent GenericAgent k a c
c
 where (GenericAgent k a b
b,GenericAgent k a c
c) = GenericAgent k a a -> (GenericAgent k a b, GenericAgent k a c)
forall q.
Object k q =>
GenericAgent k q a -> (GenericAgent k q b, GenericAgent k q c)
f (GenericAgent k a a -> (GenericAgent k a b, GenericAgent k a c))
-> GenericAgent k a a -> (GenericAgent k a b, GenericAgent k a c)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ k a a -> GenericAgent k a a
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (v :: k1).
k2 a v -> GenericAgent k2 a v
GenericAgent k a a
forall a. Object k a => k a a
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 = GenericAgent k (a, b) c -> k (a, b) c
forall {k1} {k2} (k3 :: k1 -> k2 -> *) (a :: k1) (v :: k2).
GenericAgent k3 a v -> k3 a v
runGenericAgent (GenericAgent k (a, b) c -> k (a, b) c)
-> GenericAgent k (a, b) c -> k (a, b) c
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ GenericAgent k (a, b) a
-> GenericAgent k (a, b) b -> GenericAgent k (a, b) c
forall q.
Object k q =>
GenericAgent k q a -> GenericAgent k q b -> GenericAgent k q c
f (k (a, b) a -> GenericAgent k (a, b) a
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (v :: k1).
k2 a v -> GenericAgent k2 a v
GenericAgent k (a, b) a
forall x y. ObjectPair k x y => k (x, y) x
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst) (k (a, b) b -> GenericAgent k (a, b) b
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (v :: k1).
k2 a v -> GenericAgent k2 a v
GenericAgent k (a, b) b
forall x y. ObjectPair k x y => k (x, y) y
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 = GenericAgent k (a, b) c -> k (a, b) c
forall {k1} {k2} (k3 :: k1 -> k2 -> *) (a :: k1) (v :: k2).
GenericAgent k3 a v -> k3 a v
runGenericAgent GenericAgent k (a, b) c
c k (a, b) c -> k (a, b) d -> k (a, b) (c, d)
forall b c c'.
(Object k b, ObjectPair k c c') =>
k b c -> k b c' -> k 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')
&&& GenericAgent k (a, b) d -> k (a, b) d
forall {k1} {k2} (k3 :: k1 -> k2 -> *) (a :: k1) (v :: k2).
GenericAgent k3 a v -> k3 a v
runGenericAgent GenericAgent k (a, b) d
d
 where (GenericAgent k (a, b) c
c,GenericAgent k (a, b) d
d) = GenericAgent k (a, b) a
-> GenericAgent k (a, b) b
-> (GenericAgent k (a, b) c, GenericAgent k (a, b) d)
forall q.
Object k q =>
GenericAgent k q a
-> GenericAgent k q b -> (GenericAgent k q c, GenericAgent k q d)
f (k (a, b) a -> GenericAgent k (a, b) a
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (v :: k1).
k2 a v -> GenericAgent k2 a v
GenericAgent k (a, b) a
forall x y. ObjectPair k x y => k (x, y) x
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst) (k (a, b) b -> GenericAgent k (a, b) b
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (v :: k1).
k2 a v -> GenericAgent k2 a v
GenericAgent k (a, b) b
forall x y. ObjectPair k x y => k (x, y) y
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 = k a x -> GenericAgent k a x
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (v :: k1).
k2 a v -> GenericAgent k2 a v
GenericAgent (k a x -> GenericAgent k a x) -> k a x -> GenericAgent k a x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x -> k a x
forall b x. (Object k b, ObjectPoint k x) => x -> k b x
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
_ = Coercion a b -> k a b
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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 a b
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
_ = Coercion b a -> k b a
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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
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 = Coercion a b -> k a b
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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 a b
crc k a b -> k b a -> k b b
forall a b c.
(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
. k a a
f k a a -> k b a -> k b a
forall a b c.
(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
. Coercion b a -> k b a
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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 a b -> Coercion b a
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 = Coercion a b -> k a b
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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 -> Coercion a b
forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a
sym Coercion b a
crc) k a b -> k b a -> k b b
forall a b c.
(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
. k a a
f k a a -> k b a -> k b a
forall a b c.
(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
. Coercion b a -> k b a
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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 = Coercion c d -> k c d
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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 c d
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion k c d -> k b c -> k b d
forall a b c.
(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
. k a c
f k a c -> k b a -> k b c
forall a b c.
(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
. Coercion b a -> k b a
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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
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 = Coercion c d -> k c d
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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 c d
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion k c d -> k b c -> k b d
forall a b c.
(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
. k a c
f k a c -> k b a -> k b c
forall a b c.
(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
. Coercion b a -> k b a
forall b c.
(Object Coercion b, Object Coercion c, Object k b, Object k c) =>
Coercion b c -> k b 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
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion