-- |
-- Module      :  Control.Category.Constrained.Reified
-- Copyright   :  (c) 2016 Justus Sagemüller
-- License     :  GPL v3 (see COPYING)
-- Maintainer  :  (@) jsag $ hvl.no
-- 
-- 
-- GADTs that mirror the class hierarchy from 'Category' to (at the moment) 'Cartesian',
-- reifying all the available “free” composition operations.
-- 
-- These can be used as a “trivial base case“ for all kinds of categories:
-- it turns out these basic operations are often not so trivial to implement,
-- or only possible with stronger constraints than you'd like. For instance,
-- the category of affine mappings can only be implemented directly as a
-- category on /vector spaces/, because the identity mapping has /zero/ constant
-- offset.
-- 
-- By leaving the free compositions reified to runtime syntax trees, this problem
-- can be avoided. In other applications, you may not /need/ these cases,
-- but can still benefit from them for optimisation (composition with 'id' is
-- always trivial, and so on).

{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE UnicodeSyntax         #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE CPP                   #-}

module Control.Category.Constrained.Reified (
      -- * Reified versions of the category classes
         ReCategory(..)
       , ReCartesian(..)
       , ReMorphism(..)
       , RePreArrow(..)
       , ReWellPointed(..)
       ) where


import Prelude ()
import GHC.Exts (Constraint)

import Control.Category.Constrained.Prelude
import Control.Arrow.Constrained

import Data.Tagged


data ObjectWitness k α where
  IsObject :: Object k α => ObjectWitness k α

domObjWitness :: (Category k, Object k α) => k α β -> ObjectWitness k α
domObjWitness :: k α β -> ObjectWitness k α
domObjWitness k α β
_ = ObjectWitness k α
forall (k :: * -> * -> *) α. Object k α => ObjectWitness k α
IsObject
codomObjWitness :: (Category k, Object k β) => k α β -> ObjectWitness k β
codomObjWitness :: k α β -> ObjectWitness k β
codomObjWitness k α β
_ = ObjectWitness k β
forall (k :: * -> * -> *) α. Object k α => ObjectWitness k α
IsObject

withObjWitness :: ObjectWitness k γ -> (ObjectWitness k γ -> k α β) -> k α β
withObjWitness :: ObjectWitness k γ -> (ObjectWitness k γ -> k α β) -> k α β
withObjWitness ObjectWitness k γ
w ObjectWitness k γ -> k α β
f = ObjectWitness k γ -> k α β
f ObjectWitness k γ
w

data ObjPairWitness k α β where
  AreObjects :: ObjectPair k α β => ObjPairWitness k α β
data UnitObjWitness k u where
  IsUnitObj :: UnitObjWitness k (UnitObject k)






-- GHC-invoked CPP can't seem able to do token pasting, so invoke the
-- preprocessor manually to generate the GADTs.
-- @
--  $ cpp Control/Category/Constrained/Reified.hs 2> /dev/null | less
-- @
-- You can there copy-and paste the definitions of 'ReCategory' etc..
#ifndef __GLASGOW_HASKELL__
#  define GADTCPP
#endif

#ifdef GADTCPP
#  define RECATEGORY(C)                           \
    Re##C :: k α β -> Re##C k α β;                 \
    C##Id :: Object k α => Re##C k α α;             \
    C##Compo :: Object k β                           \
         => Re##C k α β -> Re##C k β γ -> Re##C k α γ
#else
#  define RECATEGORY(C)   \
    ReCategory :: k α β -> ReCategory k α β; CategoryId :: Object k α => ReCategory k α α; CategoryCompo :: Object k β => ReCategory k α β -> ReCategory k β γ -> ReCategory k α γ
#endif
data ReCategory (k :: * -> * -> *) (α :: *) (β :: *) where
    RECATEGORY(Category)

#define CATEGORYCOMPO \
  Id . f = f;          \
  g . Id = g

instance Category k => Category (ReCategory k) where
  type Object (ReCategory k) α = Object k α
  id :: ReCategory k a a
id = ReCategory k a a
forall (k :: * -> * -> *) α. Object k α => ReCategory k α α
CategoryId
  ReCategory k b c
CategoryId . :: ReCategory k b c -> ReCategory k a b -> ReCategory k a c
. ReCategory k a b
f = ReCategory k a b
ReCategory k a c
f
  ReCategory k b c
g . ReCategory k a b
CategoryId = ReCategory k a c
ReCategory k b c
g
  ReCategory k b c
g . ReCategory k a b
f = ReCategory k a b -> ReCategory k b c -> ReCategory k a c
forall (k :: * -> * -> *) β α γ.
Object k β =>
ReCategory k α β -> ReCategory k β γ -> ReCategory k α γ
CategoryCompo ReCategory k a b
f ReCategory k b c
g

  
instance HasAgent k => HasAgent (ReCategory k) where
  type AgentVal (ReCategory k) α ω = GenericAgent (ReCategory k) α ω
  alg :: (forall q.
 Object (ReCategory k) q =>
 AgentVal (ReCategory k) q a -> AgentVal (ReCategory k) q b)
-> ReCategory k a b
alg = (forall q.
 Object (ReCategory k) q =>
 AgentVal (ReCategory k) q a -> AgentVal (ReCategory k) q b)
-> ReCategory k a b
forall (k :: * -> * -> *) a b.
(HasAgent k, Object k a, Object k b) =>
(forall q. Object k q => GenericAgent k q a -> GenericAgent k q b)
-> k a b
genericAlg
  $~ :: ReCategory k b c
-> AgentVal (ReCategory k) a b -> AgentVal (ReCategory k) a c
($~) = ReCategory k b c
-> AgentVal (ReCategory k) a b -> AgentVal (ReCategory k) a c
forall (k :: * -> * -> *) a b c.
(HasAgent k, Object k a, Object k b, Object k c) =>
k b c -> GenericAgent k a b -> GenericAgent k a c
genericAgentMap
  

instance Category k => EnhancedCat (ReCategory k) k where arr :: k b c -> ReCategory k b c
arr = k b c -> ReCategory k b c
forall (k :: * -> * -> *) α β. k α β -> ReCategory k α β
ReCategory



#ifdef GADTCPP
#  define RECARTESIAN(C)                                          \
    RECATEGORY(C);                                                 \
    C##Swap :: (ObjectPair k α β, ObjectPair k β α)                 \
                => Re##C k (α,β) (β,α);                              \
    C##AttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) \
                => Re##C k α (α,u);                                    \
    C##DetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u)   \
                => Re##C k (α,u) α;                                      \
    C##Regroup :: ( ObjectPair k α β, ObjectPair k β γ                    \
                  , ObjectPair k α (β,γ), ObjectPair k (α,β) γ )           \
                => Re##C k (α,(β,γ)) ((α,β),γ);                             \
    C##Regroup_ :: ( ObjectPair k α β, ObjectPair k β γ                      \
                   , ObjectPair k α (β,γ), ObjectPair k (α,β) γ )             \
                => Re##C k ((α,β),γ) (α,(β,γ))
#else
#  define RECARTESIAN(C) \
    ReCartesian :: k α β -> ReCartesian k α β; CartesianId :: Object k α => ReCartesian k α α; CartesianCompo :: Object k β => ReCartesian k α β -> ReCartesian k β γ -> ReCartesian k α γ; CartesianSwap :: (ObjectPair k α β, ObjectPair k β α) => ReCartesian k (α,β) (β,α); CartesianAttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReCartesian k α (α,u); CartesianDetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReCartesian k (α,u) α; CartesianRegroup :: ( ObjectPair k α β, ObjectPair k β γ , ObjectPair k α (β,γ), ObjectPair k (α,β) γ ) => ReCartesian k (α,(β,γ)) ((α,β),γ); CartesianRegroup_ :: ( ObjectPair k α β, ObjectPair k β γ , ObjectPair k α (β,γ), ObjectPair k (α,β) γ ) => ReCartesian k ((α,β),γ) (α,(β,γ))
#endif
data ReCartesian (k :: * -> * -> *) (α :: *) (β :: *) where
    RECARTESIAN(Cartesian)

#define CARTESIANCOMPO   \
  Swap . Swap = id;       \
  Regroup . Regroup' = id; \
  Regroup' . Regroup = id;  \
  CATEGORYCOMPO

instance Cartesian k => Category (ReCartesian k) where
  type Object (ReCartesian k) a = Object k a
  id :: ReCartesian k a a
id = ReCartesian k a a
forall (k :: * -> * -> *) α. Object k α => ReCartesian k α α
CartesianId
  ReCartesian k b c
CartesianSwap . :: ReCartesian k b c -> ReCartesian k a b -> ReCartesian k a c
. ReCartesian k a b
CartesianSwap = ReCartesian k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReCartesian k b c
CartesianRegroup . ReCartesian k a b
CartesianRegroup_ = ReCartesian k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReCartesian k b c
CartesianRegroup_ . ReCartesian k a b
CartesianRegroup = ReCartesian k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReCartesian k b c
CartesianId . ReCartesian k a b
f = ReCartesian k a b
ReCartesian k a c
f
  ReCartesian k b c
g . ReCartesian k a b
CartesianId = ReCartesian k a c
ReCartesian k b c
g
  ReCartesian k b c
g . ReCartesian k a b
f = ReCartesian k a b -> ReCartesian k b c -> ReCartesian k a c
forall (k :: * -> * -> *) β α γ.
Object k β =>
ReCartesian k α β -> ReCartesian k β γ -> ReCartesian k α γ
CartesianCompo ReCartesian k a b
f ReCartesian k b c
g

instance Cartesian k => Cartesian (ReCartesian k) where
  type PairObjects (ReCartesian k) α β = PairObjects k α β
  type UnitObject (ReCartesian k) = UnitObject k
  swap :: ReCartesian k (a, b) (b, a)
swap = ReCartesian k (a, b) (b, a)
forall (k :: * -> * -> *) α β.
(ObjectPair k α β, ObjectPair k β α) =>
ReCartesian k (α, β) (β, α)
CartesianSwap
  attachUnit :: ReCartesian k a (a, unit)
attachUnit = ReCartesian k a (a, unit)
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
ReCartesian k α (α, u)
CartesianAttachUnit
  detachUnit :: ReCartesian k (a, unit) a
detachUnit = ReCartesian k (a, unit) a
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
ReCartesian k (α, u) α
CartesianDetachUnit
  regroup :: ReCartesian k (a, (b, c)) ((a, b), c)
regroup = ReCartesian k (a, (b, c)) ((a, b), c)
forall (k :: * -> * -> *) α β α.
(ObjectPair k α β, ObjectPair k β α, ObjectPair k α (β, α),
 ObjectPair k (α, β) α) =>
ReCartesian k (α, (β, α)) ((α, β), α)
CartesianRegroup
  regroup' :: ReCartesian k ((a, b), c) (a, (b, c))
regroup' = ReCartesian k ((a, b), c) (a, (b, c))
forall (k :: * -> * -> *) α β γ.
(ObjectPair k α β, ObjectPair k β γ, ObjectPair k α (β, γ),
 ObjectPair k (α, β) γ) =>
ReCartesian k ((α, β), γ) (α, (β, γ))
CartesianRegroup_
  
  
instance (HasAgent k, Cartesian k) => HasAgent (ReCartesian k) where
  type AgentVal (ReCartesian k) α ω = GenericAgent (ReCartesian k) α ω
  alg :: (forall q.
 Object (ReCartesian k) q =>
 AgentVal (ReCartesian k) q a -> AgentVal (ReCartesian k) q b)
-> ReCartesian k a b
alg = (forall q.
 Object (ReCartesian k) q =>
 AgentVal (ReCartesian k) q a -> AgentVal (ReCartesian k) q b)
-> ReCartesian k a b
forall (k :: * -> * -> *) a b.
(HasAgent k, Object k a, Object k b) =>
(forall q. Object k q => GenericAgent k q a -> GenericAgent k q b)
-> k a b
genericAlg
  $~ :: ReCartesian k b c
-> AgentVal (ReCartesian k) a b -> AgentVal (ReCartesian k) a c
($~) = ReCartesian k b c
-> AgentVal (ReCartesian k) a b -> AgentVal (ReCartesian k) a c
forall (k :: * -> * -> *) a b c.
(HasAgent k, Object k a, Object k b, Object k c) =>
k b c -> GenericAgent k a b -> GenericAgent k a c
genericAgentMap
  
  
instance Cartesian k => EnhancedCat (ReCartesian k) k where arr :: k b c -> ReCartesian k b c
arr = k b c -> ReCartesian k b c
forall (k :: * -> * -> *) α β. k α β -> ReCartesian k α β
ReCartesian


#ifdef GADTCPP
#  define REMORPHISM(C)                                \
    RECARTESIAN(C);                                     \
    C##Par :: (ObjectPair k α γ, ObjectPair k β δ)       \
              => Re##C k α β -> Re##C k γ δ -> Re##C k (α,γ) (β,δ)
#else
#  define REMORPHISM(C)  \
    ReMorphism :: k α β -> ReMorphism k α β; MorphismId :: Object k α => ReMorphism k α α; MorphismCompo :: Object k β => ReMorphism k α β -> ReMorphism k β γ -> ReMorphism k α γ; MorphismSwap :: (ObjectPair k α β, ObjectPair k β α) => ReMorphism k (α,β) (β,α); MorphismAttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReMorphism k α (α,u); MorphismDetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReMorphism k (α,u) α; MorphismRegroup :: ( ObjectPair k α β, ObjectPair k β γ , ObjectPair k α (β,γ), ObjectPair k (α,β) γ ) => ReMorphism k (α,(β,γ)) ((α,β),γ); MorphismRegroup_ :: ( ObjectPair k α β, ObjectPair k β γ , ObjectPair k α (β,γ), ObjectPair k (α,β) γ ) => ReMorphism k ((α,β),γ) (α,(β,γ)); MorphismPar :: (ObjectPair k α γ, ObjectPair k β δ) => ReMorphism k α β -> ReMorphism k γ δ -> ReMorphism k (α,γ) (β,δ)
#endif
data ReMorphism (k :: * -> * -> *) (α :: *) (β :: *) where
    REMORPHISM(Morphism)

#define MORPHISMCOMPO               \
  (f:***g) . (h:***i) = f.h *** g.i; \
  CARTESIANCOMPO

instance Morphism k => Category (ReMorphism k) where
  type Object (ReMorphism k) a = Object k a
  id :: ReMorphism k a a
id = ReMorphism k a a
forall (k :: * -> * -> *) α. Object k α => ReMorphism k α α
MorphismId
  (ReMorphism k α β
f`MorphismPar`ReMorphism k γ δ
g) . :: ReMorphism k b c -> ReMorphism k a b -> ReMorphism k a c
. (ReMorphism k α β
h`MorphismPar`ReMorphism k γ δ
i) = ReMorphism k α β
fReMorphism k α β -> ReMorphism k α α -> ReMorphism k α β
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
.ReMorphism k α α
ReMorphism k α β
h ReMorphism k α β -> ReMorphism k γ δ -> ReMorphism k (α, γ) (β, δ)
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')
*** ReMorphism k γ δ
gReMorphism k γ δ -> ReMorphism k γ γ -> ReMorphism k γ δ
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
.ReMorphism k γ γ
ReMorphism k γ δ
i
  ReMorphism k b c
MorphismSwap . ReMorphism k a b
MorphismSwap = ReMorphism k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReMorphism k b c
MorphismRegroup . ReMorphism k a b
MorphismRegroup_ = ReMorphism k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReMorphism k b c
MorphismRegroup_ . ReMorphism k a b
MorphismRegroup = ReMorphism k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReMorphism k b c
MorphismId . ReMorphism k a b
f = ReMorphism k a b
ReMorphism k a c
f
  ReMorphism k b c
g . ReMorphism k a b
MorphismId = ReMorphism k a c
ReMorphism k b c
g
  ReMorphism k b c
g . ReMorphism k a b
f = ReMorphism k a b -> ReMorphism k b c -> ReMorphism k a c
forall (k :: * -> * -> *) β α γ.
Object k β =>
ReMorphism k α β -> ReMorphism k β γ -> ReMorphism k α γ
MorphismCompo ReMorphism k a b
f ReMorphism k b c
g

instance Morphism k => Cartesian (ReMorphism k) where
  type PairObjects (ReMorphism k) α β = PairObjects k α β
  type UnitObject (ReMorphism k) = UnitObject k
  swap :: ReMorphism k (a, b) (b, a)
swap = ReMorphism k (a, b) (b, a)
forall (k :: * -> * -> *) α β.
(ObjectPair k α β, ObjectPair k β α) =>
ReMorphism k (α, β) (β, α)
MorphismSwap
  attachUnit :: ReMorphism k a (a, unit)
attachUnit = ReMorphism k a (a, unit)
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
ReMorphism k α (α, u)
MorphismAttachUnit
  detachUnit :: ReMorphism k (a, unit) a
detachUnit = ReMorphism k (a, unit) a
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
ReMorphism k (α, u) α
MorphismDetachUnit
  regroup :: ReMorphism k (a, (b, c)) ((a, b), c)
regroup = ReMorphism k (a, (b, c)) ((a, b), c)
forall (k :: * -> * -> *) α β α.
(ObjectPair k α β, ObjectPair k β α, ObjectPair k α (β, α),
 ObjectPair k (α, β) α) =>
ReMorphism k (α, (β, α)) ((α, β), α)
MorphismRegroup
  regroup' :: ReMorphism k ((a, b), c) (a, (b, c))
regroup' = ReMorphism k ((a, b), c) (a, (b, c))
forall (k :: * -> * -> *) α β α.
(ObjectPair k α β, ObjectPair k β α, ObjectPair k α (β, α),
 ObjectPair k (α, β) α) =>
ReMorphism k ((α, β), α) (α, (β, α))
MorphismRegroup_
  
instance Morphism k => Morphism (ReMorphism k) where
  *** :: ReMorphism k b c
-> ReMorphism k b' c' -> ReMorphism k (b, b') (c, c')
(***) = ReMorphism k b c
-> ReMorphism k b' c' -> ReMorphism k (b, b') (c, c')
forall (k :: * -> * -> *) α γ β δ.
(ObjectPair k α γ, ObjectPair k β δ) =>
ReMorphism k α β -> ReMorphism k γ δ -> ReMorphism k (α, γ) (β, δ)
MorphismPar

instance (HasAgent k, Morphism k) => HasAgent (ReMorphism k) where
  type AgentVal (ReMorphism k) α ω = GenericAgent (ReMorphism k) α ω
  alg :: (forall q.
 Object (ReMorphism k) q =>
 AgentVal (ReMorphism k) q a -> AgentVal (ReMorphism k) q b)
-> ReMorphism k a b
alg = (forall q.
 Object (ReMorphism k) q =>
 AgentVal (ReMorphism k) q a -> AgentVal (ReMorphism k) q b)
-> ReMorphism k a b
forall (k :: * -> * -> *) a b.
(HasAgent k, Object k a, Object k b) =>
(forall q. Object k q => GenericAgent k q a -> GenericAgent k q b)
-> k a b
genericAlg
  $~ :: ReMorphism k b c
-> AgentVal (ReMorphism k) a b -> AgentVal (ReMorphism k) a c
($~) = ReMorphism k b c
-> AgentVal (ReMorphism k) a b -> AgentVal (ReMorphism k) a c
forall (k :: * -> * -> *) a b c.
(HasAgent k, Object k a, Object k b, Object k c) =>
k b c -> GenericAgent k a b -> GenericAgent k a c
genericAgentMap

  
instance Morphism k => EnhancedCat (ReMorphism k) k where arr :: k b c -> ReMorphism k b c
arr = k b c -> ReMorphism k b c
forall (k :: * -> * -> *) α β. k α β -> ReMorphism k α β
ReMorphism




#ifdef GADTCPP
#  define REPREARROW(C)                                    \
    REMORPHISM(C);                                          \
    C##Fanout :: (Object k α, ObjectPair k β γ)              \
            => Re##C k α β -> Re##C k α γ -> Re##C k α (β,γ); \
    C##Terminal :: Object k α => Re##C k α (UnitObject k);     \
    C##Fst :: ObjectPair k α β => Re##C k (α,β) α;              \
    C##Snd :: ObjectPair k α β => Re##C k (α,β) β
#else
#  define REPREARROW(C) \
    RePreArrow :: k α β -> RePreArrow k α β; PreArrowId :: Object k α => RePreArrow k α α; PreArrowCompo :: Object k β => RePreArrow k α β -> RePreArrow k β γ -> RePreArrow k α γ; PreArrowSwap :: (ObjectPair k α β, ObjectPair k β α) => RePreArrow k (α,β) (β,α); PreArrowAttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => RePreArrow k α (α,u); PreArrowDetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => RePreArrow k (α,u) α; PreArrowRegroup :: ( ObjectPair k α β, ObjectPair k β γ , ObjectPair k α (β,γ), ObjectPair k (α,β) γ ) => RePreArrow k (α,(β,γ)) ((α,β),γ); PreArrowRegroup_ :: ( ObjectPair k α β, ObjectPair k β γ , ObjectPair k α (β,γ), ObjectPair k (α,β) γ ) => RePreArrow k ((α,β),γ) (α,(β,γ)); PreArrowPar :: (ObjectPair k α γ, ObjectPair k β δ) => RePreArrow k α β -> RePreArrow k γ δ -> RePreArrow k (α,γ) (β,δ); PreArrowFanout :: (Object k α, ObjectPair k β γ) => RePreArrow k α β -> RePreArrow k α γ -> RePreArrow k α (β,γ); PreArrowTerminal :: Object k α => RePreArrow k α (UnitObject k); PreArrowFst :: ObjectPair k α β => RePreArrow k (α,β) α; PreArrowSnd :: ObjectPair k α β => RePreArrow k (α,β) β
#endif
data RePreArrow (k :: * -> * -> *) (α :: *) (β :: *) where
    REPREARROW(PreArrow)

#define PREARROWCOMPO      \
  Terminal . _ = terminal;  \
  Fst . (f:&&&_) = f;        \
  Snd . (_:&&&g) = g;         \
  Fst . (f:***_) = f . fst;    \
  Snd . (_:***g) = g . snd;     \
  MORPHISMCOMPO

instance PreArrow k => Category (RePreArrow k) where
  type Object (RePreArrow k) a = Object k a
  id :: RePreArrow k a a
id = RePreArrow k a a
forall (k :: * -> * -> *) α. Object k α => RePreArrow k α α
PreArrowId
  RePreArrow k b c
PreArrowTerminal . :: RePreArrow k b c -> RePreArrow k a b -> RePreArrow k a c
. RePreArrow k a b
_ = RePreArrow k a c
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
  RePreArrow k b c
PreArrowFst . (RePreArrow k a β
f`PreArrowFanout`RePreArrow k a γ
_) = RePreArrow k a c
RePreArrow k a β
f
  RePreArrow k b c
PreArrowSnd . (RePreArrow k a β
_`PreArrowFanout`RePreArrow k a γ
g) = RePreArrow k a c
RePreArrow k a γ
g
  RePreArrow k b c
PreArrowFst . (RePreArrow k α β
f`PreArrowPar`RePreArrow k γ δ
_) = RePreArrow k α β
f RePreArrow k α β -> RePreArrow k (α, γ) α -> RePreArrow k (α, γ) β
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
. RePreArrow k (α, γ) α
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst
  RePreArrow k b c
PreArrowSnd . (RePreArrow k α β
_`PreArrowPar`RePreArrow k γ δ
g) = RePreArrow k γ δ
g RePreArrow k γ δ -> RePreArrow k (α, γ) γ -> RePreArrow k (α, γ) δ
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
. RePreArrow k (α, γ) γ
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd
  (RePreArrow k α β
f`PreArrowPar`RePreArrow k γ δ
g) . (RePreArrow k α β
h`PreArrowPar`RePreArrow k γ δ
i) = RePreArrow k α β
fRePreArrow k α β -> RePreArrow k α α -> RePreArrow k α β
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
.RePreArrow k α α
RePreArrow k α β
h RePreArrow k α β -> RePreArrow k γ δ -> RePreArrow k (α, γ) (β, δ)
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')
*** RePreArrow k γ δ
gRePreArrow k γ δ -> RePreArrow k γ γ -> RePreArrow k γ δ
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
.RePreArrow k γ γ
RePreArrow k γ δ
i
  RePreArrow k b c
PreArrowSwap . RePreArrow k a b
PreArrowSwap = RePreArrow k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  RePreArrow k b c
PreArrowRegroup . RePreArrow k a b
PreArrowRegroup_ = RePreArrow k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  RePreArrow k b c
PreArrowRegroup_ . RePreArrow k a b
PreArrowRegroup = RePreArrow k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  RePreArrow k b c
PreArrowId . RePreArrow k a b
f = RePreArrow k a b
RePreArrow k a c
f
  RePreArrow k b c
g . RePreArrow k a b
PreArrowId = RePreArrow k a c
RePreArrow k b c
g
  RePreArrow k b c
g . RePreArrow k a b
f = RePreArrow k a b -> RePreArrow k b c -> RePreArrow k a c
forall (k :: * -> * -> *) β α γ.
Object k β =>
RePreArrow k α β -> RePreArrow k β γ -> RePreArrow k α γ
PreArrowCompo RePreArrow k a b
f RePreArrow k b c
g

instance PreArrow k => Cartesian (RePreArrow k) where
  type PairObjects (RePreArrow k) α β = PairObjects k α β
  type UnitObject (RePreArrow k) = UnitObject k
  swap :: RePreArrow k (a, b) (b, a)
swap = RePreArrow k (a, b) (b, a)
forall (k :: * -> * -> *) α β.
(ObjectPair k α β, ObjectPair k β α) =>
RePreArrow k (α, β) (β, α)
PreArrowSwap
  attachUnit :: RePreArrow k a (a, unit)
attachUnit = RePreArrow k a (a, unit)
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
RePreArrow k α (α, u)
PreArrowAttachUnit
  detachUnit :: RePreArrow k (a, unit) a
detachUnit = RePreArrow k (a, unit) a
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
RePreArrow k (α, u) α
PreArrowDetachUnit
  regroup :: RePreArrow k (a, (b, c)) ((a, b), c)
regroup = RePreArrow k (a, (b, c)) ((a, b), c)
forall (k :: * -> * -> *) α β α.
(ObjectPair k α β, ObjectPair k β α, ObjectPair k α (β, α),
 ObjectPair k (α, β) α) =>
RePreArrow k (α, (β, α)) ((α, β), α)
PreArrowRegroup
  regroup' :: RePreArrow k ((a, b), c) (a, (b, c))
regroup' = RePreArrow k ((a, b), c) (a, (b, c))
forall (k :: * -> * -> *) α β α.
(ObjectPair k α β, ObjectPair k β α, ObjectPair k α (β, α),
 ObjectPair k (α, β) α) =>
RePreArrow k ((α, β), α) (α, (β, α))
PreArrowRegroup_
  
instance PreArrow k => Morphism (RePreArrow k) where
  *** :: RePreArrow k b c
-> RePreArrow k b' c' -> RePreArrow k (b, b') (c, c')
(***) = RePreArrow k b c
-> RePreArrow k b' c' -> RePreArrow k (b, b') (c, c')
forall (k :: * -> * -> *) α γ β β.
(ObjectPair k α γ, ObjectPair k β β) =>
RePreArrow k α β -> RePreArrow k γ β -> RePreArrow k (α, γ) (β, β)
PreArrowPar

instance PreArrow k => PreArrow (RePreArrow k) where
  &&& :: RePreArrow k b c -> RePreArrow k b c' -> RePreArrow k b (c, c')
(&&&) = RePreArrow k b c -> RePreArrow k b c' -> RePreArrow k b (c, c')
forall (k :: * -> * -> *) α β γ.
(Object k α, ObjectPair k β γ) =>
RePreArrow k α β -> RePreArrow k α γ -> RePreArrow k α (β, γ)
PreArrowFanout
  terminal :: RePreArrow k b (UnitObject (RePreArrow k))
terminal = RePreArrow k b (UnitObject (RePreArrow k))
forall (k :: * -> * -> *) α.
Object k α =>
RePreArrow k α (UnitObject k)
PreArrowTerminal
  fst :: RePreArrow k (x, y) x
fst = RePreArrow k (x, y) x
forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
RePreArrow k (α, β) α
PreArrowFst
  snd :: RePreArrow k (x, y) y
snd = RePreArrow k (x, y) y
forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
RePreArrow k (α, β) β
PreArrowSnd

instance (HasAgent k, PreArrow k) => HasAgent (RePreArrow k) where
  type AgentVal (RePreArrow k) α ω = GenericAgent (RePreArrow k) α ω
  alg :: (forall q.
 Object (RePreArrow k) q =>
 AgentVal (RePreArrow k) q a -> AgentVal (RePreArrow k) q b)
-> RePreArrow k a b
alg = (forall q.
 Object (RePreArrow k) q =>
 AgentVal (RePreArrow k) q a -> AgentVal (RePreArrow k) q b)
-> RePreArrow k a b
forall (k :: * -> * -> *) a b.
(HasAgent k, Object k a, Object k b) =>
(forall q. Object k q => GenericAgent k q a -> GenericAgent k q b)
-> k a b
genericAlg
  $~ :: RePreArrow k b c
-> AgentVal (RePreArrow k) a b -> AgentVal (RePreArrow k) a c
($~) = RePreArrow k b c
-> AgentVal (RePreArrow k) a b -> AgentVal (RePreArrow k) a c
forall (k :: * -> * -> *) a b c.
(HasAgent k, Object k a, Object k b, Object k c) =>
k b c -> GenericAgent k a b -> GenericAgent k a c
genericAgentMap


instance PreArrow k => EnhancedCat (RePreArrow k) k where arr :: k b c -> RePreArrow k b c
arr = k b c -> RePreArrow k b c
forall (k :: * -> * -> *) α β. k α β -> RePreArrow k α β
RePreArrow




#ifdef GADTCPP
#  define REWELLPOINTED(C)                                       \
    REPREARROW(C);                                                \
    C##Const :: (Object k ν, ObjectPoint k α) => α -> Re##C k ν α
#else
#  define REWELLPOINTED(C) \
    ReWellPointed :: k α β -> ReWellPointed k α β; WellPointedId :: Object k α => ReWellPointed k α α; WellPointedCompo :: Object k β => ReWellPointed k α β -> ReWellPointed k β γ -> ReWellPointed k α γ; WellPointedSwap :: (ObjectPair k α β, ObjectPair k β α) => ReWellPointed k (α,β) (β,α); WellPointedAttachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReWellPointed k α (α,u); WellPointedDetachUnit :: (Object k α, UnitObject k ~ u, ObjectPair k α u) => ReWellPointed k (α,u) α; WellPointedRegroup :: ( ObjectPair k α β, ObjectPair k β γ , ObjectPair k α (β,γ), ObjectPair k (α,β) γ ) => ReWellPointed k (α,(β,γ)) ((α,β),γ); WellPointedRegroup_ :: ( ObjectPair k α β, ObjectPair k β γ , ObjectPair k α (β,γ), ObjectPair k (α,β) γ ) => ReWellPointed k ((α,β),γ) (α,(β,γ)); WellPointedPar :: (ObjectPair k α γ, ObjectPair k β δ) => ReWellPointed k α β -> ReWellPointed k γ δ -> ReWellPointed k (α,γ) (β,δ); WellPointedFanout :: (Object k α, ObjectPair k β γ) => ReWellPointed k α β -> ReWellPointed k α γ -> ReWellPointed k α (β,γ); WellPointedTerminal :: Object k α => ReWellPointed k α (UnitObject k); WellPointedFst :: ObjectPair k α β => ReWellPointed k (α,β) α; WellPointedSnd :: ObjectPair k α β => ReWellPointed k (α,β) β; WellPointedConst :: (Object k ν, ObjectPoint k α) => α -> ReWellPointed k ν α
#endif
data ReWellPointed (k :: * -> * -> *) (α :: *) (β :: *) where
    REWELLPOINTED(WellPointed)


#define WELLPOINTEDCOMPO  \
  Const c . _ = const c;   \
  PREARROWCOMPO

instance WellPointed k => Category (ReWellPointed k) where
  type Object (ReWellPointed k) a = Object k a
  id :: ReWellPointed k a a
id = ReWellPointed k a a
forall (k :: * -> * -> *) α. Object k α => ReWellPointed k α α
WellPointedId
  WellPointedConst c
c . :: ReWellPointed k b c -> ReWellPointed k a b -> ReWellPointed k a c
. ReWellPointed k a b
_ = c -> ReWellPointed k a c
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const c
c
  ReWellPointed k b c
WellPointedTerminal . ReWellPointed k a b
_ = ReWellPointed k a c
forall (a :: * -> * -> *) b.
(PreArrow a, Object a b) =>
a b (UnitObject a)
terminal
  ReWellPointed k b c
WellPointedFst . (ReWellPointed k a β
f`WellPointedFanout`ReWellPointed k a γ
_) = ReWellPointed k a c
ReWellPointed k a β
f
  ReWellPointed k b c
WellPointedSnd . (ReWellPointed k a β
_`WellPointedFanout`ReWellPointed k a γ
g) = ReWellPointed k a c
ReWellPointed k a γ
g
  ReWellPointed k b c
WellPointedFst . (ReWellPointed k α β
f`WellPointedPar`ReWellPointed k γ δ
_) = ReWellPointed k α β
f ReWellPointed k α β
-> ReWellPointed k (α, γ) α -> ReWellPointed k (α, γ) β
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
. ReWellPointed k (α, γ) α
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst
  ReWellPointed k b c
WellPointedSnd . (ReWellPointed k α β
_`WellPointedPar`ReWellPointed k γ δ
g) = ReWellPointed k γ δ
g ReWellPointed k γ δ
-> ReWellPointed k (α, γ) γ -> ReWellPointed k (α, γ) δ
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
. ReWellPointed k (α, γ) γ
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd
  (ReWellPointed k α β
f`WellPointedPar`ReWellPointed k γ δ
g) . (ReWellPointed k α β
h`WellPointedPar`ReWellPointed k γ δ
i) = ReWellPointed k α β
fReWellPointed k α β -> ReWellPointed k α α -> ReWellPointed k α β
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
.ReWellPointed k α α
ReWellPointed k α β
h ReWellPointed k α β
-> ReWellPointed k γ δ -> ReWellPointed k (α, γ) (β, δ)
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')
*** ReWellPointed k γ δ
gReWellPointed k γ δ -> ReWellPointed k γ γ -> ReWellPointed k γ δ
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
.ReWellPointed k γ γ
ReWellPointed k γ δ
i
  ReWellPointed k b c
WellPointedSwap . ReWellPointed k a b
WellPointedSwap = ReWellPointed k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReWellPointed k b c
WellPointedRegroup . ReWellPointed k a b
WellPointedRegroup_ = ReWellPointed k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReWellPointed k b c
WellPointedRegroup_ . ReWellPointed k a b
WellPointedRegroup = ReWellPointed k a c
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReWellPointed k b c
WellPointedId . ReWellPointed k a b
f = ReWellPointed k a b
ReWellPointed k a c
f
  ReWellPointed k b c
g . ReWellPointed k a b
WellPointedId = ReWellPointed k a c
ReWellPointed k b c
g
  ReWellPointed k b c
g . ReWellPointed k a b
f = ReWellPointed k a b -> ReWellPointed k b c -> ReWellPointed k a c
forall (k :: * -> * -> *) β α γ.
Object k β =>
ReWellPointed k α β -> ReWellPointed k β γ -> ReWellPointed k α γ
WellPointedCompo ReWellPointed k a b
f ReWellPointed k b c
g

instance WellPointed k => Cartesian (ReWellPointed k) where
  type PairObjects (ReWellPointed k) α β = PairObjects k α β
  type UnitObject (ReWellPointed k) = UnitObject k
  swap :: ReWellPointed k (a, b) (b, a)
swap = ReWellPointed k (a, b) (b, a)
forall (k :: * -> * -> *) α β.
(ObjectPair k α β, ObjectPair k β α) =>
ReWellPointed k (α, β) (β, α)
WellPointedSwap
  attachUnit :: ReWellPointed k a (a, unit)
attachUnit = ReWellPointed k a (a, unit)
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
ReWellPointed k α (α, u)
WellPointedAttachUnit
  detachUnit :: ReWellPointed k (a, unit) a
detachUnit = ReWellPointed k (a, unit) a
forall (k :: * -> * -> *) α u.
(Object k α, UnitObject k ~ u, ObjectPair k α u) =>
ReWellPointed k (α, u) α
WellPointedDetachUnit
  regroup :: ReWellPointed k (a, (b, c)) ((a, b), c)
regroup = ReWellPointed k (a, (b, c)) ((a, b), c)
forall (k :: * -> * -> *) α β α.
(ObjectPair k α β, ObjectPair k β α, ObjectPair k α (β, α),
 ObjectPair k (α, β) α) =>
ReWellPointed k (α, (β, α)) ((α, β), α)
WellPointedRegroup
  regroup' :: ReWellPointed k ((a, b), c) (a, (b, c))
regroup' = ReWellPointed k ((a, b), c) (a, (b, c))
forall (k :: * -> * -> *) α β α.
(ObjectPair k α β, ObjectPair k β α, ObjectPair k α (β, α),
 ObjectPair k (α, β) α) =>
ReWellPointed k ((α, β), α) (α, (β, α))
WellPointedRegroup_
  
instance WellPointed k => Morphism (ReWellPointed k) where
  -- Const c *** Const d = const (c,d)
  -- f@Terminal *** g@Terminal = tpar f g
  --  where tpar :: ∀ k α β . (WellPointed k, ObjectPair k α β)
  --           => ReWellPointed k α (UnitObject k) -> ReWellPointed k β (UnitObject k)
  --               -> ReWellPointed k (α,β) (UnitObject k, UnitObject k)
  --        tpar Terminal Terminal = const (u, u)
  --         where Tagged u = unit :: CatTagged k (UnitObject k)
  ReWellPointed k b c
f *** :: ReWellPointed k b c
-> ReWellPointed k b' c' -> ReWellPointed k (b, b') (c, c')
*** ReWellPointed k b' c'
g = ReWellPointed k b c
-> ReWellPointed k b' c' -> ReWellPointed k (b, b') (c, c')
forall (k :: * -> * -> *) α γ β β.
(ObjectPair k α γ, ObjectPair k β β) =>
ReWellPointed k α β
-> ReWellPointed k γ β -> ReWellPointed k (α, γ) (β, β)
WellPointedPar ReWellPointed k b c
f ReWellPointed k b' c'
g

instance WellPointed k => PreArrow (ReWellPointed k) where
  -- Const c &&& Const d = const (c,d)
  ReWellPointed k b c
f &&& :: ReWellPointed k b c
-> ReWellPointed k b c' -> ReWellPointed k b (c, c')
&&& ReWellPointed k b c'
g = ReWellPointed k b c
-> ReWellPointed k b c' -> ReWellPointed k b (c, c')
forall (k :: * -> * -> *) α β γ.
(Object k α, ObjectPair k β γ) =>
ReWellPointed k α β
-> ReWellPointed k α γ -> ReWellPointed k α (β, γ)
WellPointedFanout ReWellPointed k b c
f ReWellPointed k b c'
g
  terminal :: ReWellPointed k b (UnitObject (ReWellPointed k))
terminal = ReWellPointed k b (UnitObject (ReWellPointed k))
forall (k :: * -> * -> *) α.
Object k α =>
ReWellPointed k α (UnitObject k)
WellPointedTerminal
  fst :: ReWellPointed k (x, y) x
fst = ReWellPointed k (x, y) x
forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
ReWellPointed k (α, β) α
WellPointedFst
  snd :: ReWellPointed k (x, y) y
snd = ReWellPointed k (x, y) y
forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
ReWellPointed k (α, β) β
WellPointedSnd

instance WellPointed k => WellPointed (ReWellPointed k) where
  type PointObject (ReWellPointed k) α = PointObject k α
  const :: x -> ReWellPointed k b x
const = x -> ReWellPointed k b x
forall (k :: * -> * -> *) ν α.
(Object k ν, ObjectPoint k α) =>
α -> ReWellPointed k ν α
WellPointedConst
  unit :: CatTagged (ReWellPointed k) (UnitObject (ReWellPointed k))
unit = CatTagged (ReWellPointed k) (UnitObject (ReWellPointed k))
forall (k :: * -> * -> *).
WellPointed k =>
CatTagged (ReWellPointed k) (UnitObject k)
u
   where u :: ∀ k . WellPointed k => CatTagged (ReWellPointed k) (UnitObject k)
         u :: CatTagged (ReWellPointed k) (UnitObject k)
u = UnitObject k
-> Tagged
     (ReWellPointed k (UnitObject k) (UnitObject k)) (UnitObject k)
forall k (s :: k) b. b -> Tagged s b
Tagged UnitObject k
u' where Tagged UnitObject k
u' = Tagged (k (UnitObject k) (UnitObject k)) (UnitObject k)
forall (a :: * -> * -> *).
WellPointed a =>
CatTagged a (UnitObject a)
unit :: CatTagged k (UnitObject k)
  
  
instance (HasAgent k, WellPointed k) => HasAgent (ReWellPointed k) where
  type AgentVal (ReWellPointed k) α ω = GenericAgent (ReWellPointed k) α ω
  alg :: (forall q.
 Object (ReWellPointed k) q =>
 AgentVal (ReWellPointed k) q a -> AgentVal (ReWellPointed k) q b)
-> ReWellPointed k a b
alg = (forall q.
 Object (ReWellPointed k) q =>
 AgentVal (ReWellPointed k) q a -> AgentVal (ReWellPointed k) q b)
-> ReWellPointed k a b
forall (k :: * -> * -> *) a b.
(HasAgent k, Object k a, Object k b) =>
(forall q. Object k q => GenericAgent k q a -> GenericAgent k q b)
-> k a b
genericAlg
  $~ :: ReWellPointed k b c
-> AgentVal (ReWellPointed k) a b -> AgentVal (ReWellPointed k) a c
($~) = ReWellPointed k b c
-> AgentVal (ReWellPointed k) a b -> AgentVal (ReWellPointed k) a c
forall (k :: * -> * -> *) a b c.
(HasAgent k, Object k a, Object k b, Object k c) =>
k b c -> GenericAgent k a b -> GenericAgent k a c
genericAgentMap


instance WellPointed k => EnhancedCat (ReWellPointed k) k where arr :: k b c -> ReWellPointed k b c
arr = k b c -> ReWellPointed k b c
forall (k :: * -> * -> *) α β. k α β -> ReWellPointed k α β
ReWellPointed