-- |
-- 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 :: forall (k :: * -> * -> *) α β.
(Category k, Object k α) =>
k α β -> ObjectWitness k α
domObjWitness k α β
_ = forall (k :: * -> * -> *) α. Object k α => ObjectWitness k α
IsObject
codomObjWitness :: (Category k, Object k β) => k α β -> ObjectWitness k β
codomObjWitness :: forall (k :: * -> * -> *) β α.
(Category k, Object k β) =>
k α β -> ObjectWitness k β
codomObjWitness k α β
_ = forall (k :: * -> * -> *) α. Object k α => ObjectWitness k α
IsObject

withObjWitness :: ObjectWitness k γ -> (ObjectWitness k γ -> k α β) -> k α β
withObjWitness :: forall (k :: * -> * -> *) γ α β.
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 :: forall a. Object (ReCategory k) a => ReCategory k a a
id = forall (k :: * -> * -> *) α. Object k α => ReCategory k α α
CategoryId
  ReCategory k b c
CategoryId . :: forall a b c.
(Object (ReCategory k) a, Object (ReCategory k) b,
 Object (ReCategory k) c) =>
ReCategory k b c -> ReCategory k a b -> ReCategory k a c
. ReCategory k a b
f = ReCategory k a b
f
  ReCategory k b c
g . ReCategory k a b
CategoryId = ReCategory k b c
g
  ReCategory k b c
g . ReCategory k a b
f = 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 a b.
(Object (ReCategory k) a, Object (ReCategory k) b) =>
(forall q.
 Object (ReCategory k) q =>
 AgentVal (ReCategory k) q a -> AgentVal (ReCategory k) q b)
-> ReCategory k a b
alg = 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
  $~ :: forall a b c.
(Object (ReCategory k) a, Object (ReCategory k) b,
 Object (ReCategory k) 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 :: forall b c.
(Object k b, Object k c, Object (ReCategory k) b,
 Object (ReCategory k) c) =>
k b c -> ReCategory k b c
arr = 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 :: forall a. Object (ReCartesian k) a => ReCartesian k a a
id = forall (k :: * -> * -> *) α. Object k α => ReCartesian k α α
CartesianId
  ReCartesian k b c
CartesianSwap . :: forall a b c.
(Object (ReCartesian k) a, Object (ReCartesian k) b,
 Object (ReCartesian k) c) =>
ReCartesian k b c -> ReCartesian k a b -> ReCartesian k a c
. ReCartesian k a b
CartesianSwap = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReCartesian k b c
CartesianRegroup . ReCartesian k a b
CartesianRegroup_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReCartesian k b c
CartesianRegroup_ . ReCartesian k a b
CartesianRegroup = 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
f
  ReCartesian k b c
g . ReCartesian k a b
CartesianId = ReCartesian k b c
g
  ReCartesian k b c
g . ReCartesian k a b
f = 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 :: forall a b.
(ObjectPair (ReCartesian k) a b, ObjectPair (ReCartesian k) b a) =>
ReCartesian k (a, b) (b, a)
swap = forall (k :: * -> * -> *) α γ.
(ObjectPair k α γ, ObjectPair k γ α) =>
ReCartesian k (α, γ) (γ, α)
CartesianSwap
  attachUnit :: forall unit a.
(unit ~ UnitObject (ReCartesian k),
 ObjectPair (ReCartesian k) a unit) =>
ReCartesian k a (a, unit)
attachUnit = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
ReCartesian k α (α, α)
CartesianAttachUnit
  detachUnit :: forall unit a.
(unit ~ UnitObject (ReCartesian k),
 ObjectPair (ReCartesian k) a unit) =>
ReCartesian k (a, unit) a
detachUnit = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
ReCartesian k (α, α) α
CartesianDetachUnit
  regroup :: forall a b c.
(ObjectPair (ReCartesian k) a b, ObjectPair (ReCartesian k) b c,
 ObjectPair (ReCartesian k) a (b, c),
 ObjectPair (ReCartesian k) (a, b) c) =>
ReCartesian k (a, (b, c)) ((a, b), c)
regroup = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
ReCartesian k (α, (γ, β)) ((α, γ), β)
CartesianRegroup
  regroup' :: forall a b c.
(ObjectPair (ReCartesian k) a b, ObjectPair (ReCartesian k) b c,
 ObjectPair (ReCartesian k) a (b, c),
 ObjectPair (ReCartesian k) (a, b) c) =>
ReCartesian k ((a, b), c) (a, (b, c))
regroup' = 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 a b.
(Object (ReCartesian k) a, Object (ReCartesian k) b) =>
(forall q.
 Object (ReCartesian k) q =>
 AgentVal (ReCartesian k) q a -> AgentVal (ReCartesian k) q b)
-> ReCartesian k a b
alg = 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
  $~ :: forall a b c.
(Object (ReCartesian k) a, Object (ReCartesian k) b,
 Object (ReCartesian k) 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 :: forall b c.
(Object k b, Object k c, Object (ReCartesian k) b,
 Object (ReCartesian k) c) =>
k b c -> ReCartesian k b c
arr = 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 :: forall a. Object (ReMorphism k) a => ReMorphism k a a
id = forall (k :: * -> * -> *) α. Object k α => ReMorphism k α α
MorphismId
  (ReMorphism k α β
f`MorphismPar`ReMorphism k γ δ
g) . :: forall a b c.
(Object (ReMorphism k) a, Object (ReMorphism k) b,
 Object (ReMorphism k) c) =>
ReMorphism k b c -> ReMorphism k a b -> ReMorphism k a c
. (ReMorphism k α β
h`MorphismPar`ReMorphism k γ δ
i) = ReMorphism k α β
fforall κ (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 α β
h 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 γ δ
gforall κ (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 γ δ
i
  ReMorphism k b c
MorphismSwap . ReMorphism k a b
MorphismSwap = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReMorphism k b c
MorphismRegroup . ReMorphism k a b
MorphismRegroup_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReMorphism k b c
MorphismRegroup_ . ReMorphism k a b
MorphismRegroup = 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
f
  ReMorphism k b c
g . ReMorphism k a b
MorphismId = ReMorphism k b c
g
  ReMorphism k b c
g . ReMorphism k a b
f = 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 :: forall a b.
(ObjectPair (ReMorphism k) a b, ObjectPair (ReMorphism k) b a) =>
ReMorphism k (a, b) (b, a)
swap = forall (k :: * -> * -> *) α γ.
(ObjectPair k α γ, ObjectPair k γ α) =>
ReMorphism k (α, γ) (γ, α)
MorphismSwap
  attachUnit :: forall unit a.
(unit ~ UnitObject (ReMorphism k),
 ObjectPair (ReMorphism k) a unit) =>
ReMorphism k a (a, unit)
attachUnit = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
ReMorphism k α (α, α)
MorphismAttachUnit
  detachUnit :: forall unit a.
(unit ~ UnitObject (ReMorphism k),
 ObjectPair (ReMorphism k) a unit) =>
ReMorphism k (a, unit) a
detachUnit = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
ReMorphism k (α, α) α
MorphismDetachUnit
  regroup :: forall a b c.
(ObjectPair (ReMorphism k) a b, ObjectPair (ReMorphism k) b c,
 ObjectPair (ReMorphism k) a (b, c),
 ObjectPair (ReMorphism k) (a, b) c) =>
ReMorphism k (a, (b, c)) ((a, b), c)
regroup = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
ReMorphism k (α, (γ, β)) ((α, γ), β)
MorphismRegroup
  regroup' :: forall a b c.
(ObjectPair (ReMorphism k) a b, ObjectPair (ReMorphism k) b c,
 ObjectPair (ReMorphism k) a (b, c),
 ObjectPair (ReMorphism k) (a, b) c) =>
ReMorphism k ((a, b), c) (a, (b, c))
regroup' = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
ReMorphism k ((α, γ), β) (α, (γ, β))
MorphismRegroup_
  
instance Morphism k => Morphism (ReMorphism k) where
  *** :: forall b b' c c'.
(ObjectPair (ReMorphism k) b b', ObjectPair (ReMorphism k) 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 a b.
(Object (ReMorphism k) a, Object (ReMorphism k) b) =>
(forall q.
 Object (ReMorphism k) q =>
 AgentVal (ReMorphism k) q a -> AgentVal (ReMorphism k) q b)
-> ReMorphism k a b
alg = 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
  $~ :: forall a b c.
(Object (ReMorphism k) a, Object (ReMorphism k) b,
 Object (ReMorphism k) 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 :: forall b c.
(Object k b, Object k c, Object (ReMorphism k) b,
 Object (ReMorphism k) c) =>
k b c -> ReMorphism k b c
arr = 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 :: forall a. Object (RePreArrow k) a => RePreArrow k a a
id = forall (k :: * -> * -> *) α. Object k α => RePreArrow k α α
PreArrowId
  RePreArrow k b c
PreArrowTerminal . :: forall a b c.
(Object (RePreArrow k) a, Object (RePreArrow k) b,
 Object (RePreArrow k) c) =>
RePreArrow k b c -> RePreArrow k a b -> RePreArrow k a c
. RePreArrow k a b
_ = 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 β
f
  RePreArrow k b c
PreArrowSnd . (RePreArrow k a β
_`PreArrowFanout`RePreArrow k a γ
g) = RePreArrow k a γ
g
  RePreArrow k b c
PreArrowFst . (RePreArrow k α β
f`PreArrowPar`RePreArrow k γ δ
_) = RePreArrow k α β
f forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) 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 forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) 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 α β
fforall κ (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 α β
h 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 γ δ
gforall κ (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 γ δ
i
  RePreArrow k b c
PreArrowSwap . RePreArrow k a b
PreArrowSwap = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  RePreArrow k b c
PreArrowRegroup . RePreArrow k a b
PreArrowRegroup_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  RePreArrow k b c
PreArrowRegroup_ . RePreArrow k a b
PreArrowRegroup = 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
f
  RePreArrow k b c
g . RePreArrow k a b
PreArrowId = RePreArrow k b c
g
  RePreArrow k b c
g . RePreArrow k a b
f = 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 :: forall a b.
(ObjectPair (RePreArrow k) a b, ObjectPair (RePreArrow k) b a) =>
RePreArrow k (a, b) (b, a)
swap = forall (k :: * -> * -> *) α γ.
(ObjectPair k α γ, ObjectPair k γ α) =>
RePreArrow k (α, γ) (γ, α)
PreArrowSwap
  attachUnit :: forall unit a.
(unit ~ UnitObject (RePreArrow k),
 ObjectPair (RePreArrow k) a unit) =>
RePreArrow k a (a, unit)
attachUnit = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
RePreArrow k α (α, α)
PreArrowAttachUnit
  detachUnit :: forall unit a.
(unit ~ UnitObject (RePreArrow k),
 ObjectPair (RePreArrow k) a unit) =>
RePreArrow k (a, unit) a
detachUnit = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
RePreArrow k (α, α) α
PreArrowDetachUnit
  regroup :: forall a b c.
(ObjectPair (RePreArrow k) a b, ObjectPair (RePreArrow k) b c,
 ObjectPair (RePreArrow k) a (b, c),
 ObjectPair (RePreArrow k) (a, b) c) =>
RePreArrow k (a, (b, c)) ((a, b), c)
regroup = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
RePreArrow k (α, (γ, β)) ((α, γ), β)
PreArrowRegroup
  regroup' :: forall a b c.
(ObjectPair (RePreArrow k) a b, ObjectPair (RePreArrow k) b c,
 ObjectPair (RePreArrow k) a (b, c),
 ObjectPair (RePreArrow k) (a, b) c) =>
RePreArrow k ((a, b), c) (a, (b, c))
regroup' = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
RePreArrow k ((α, γ), β) (α, (γ, β))
PreArrowRegroup_
  
instance PreArrow k => Morphism (RePreArrow k) where
  *** :: forall b b' c c'.
(ObjectPair (RePreArrow k) b b', ObjectPair (RePreArrow k) 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
  &&& :: forall b c c'.
(Object (RePreArrow k) b, ObjectPair (RePreArrow k) 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 :: forall b.
Object (RePreArrow k) b =>
RePreArrow k b (UnitObject (RePreArrow k))
terminal = forall (k :: * -> * -> *) α.
Object k α =>
RePreArrow k α (UnitObject k)
PreArrowTerminal
  fst :: forall x y. ObjectPair (RePreArrow k) x y => RePreArrow k (x, y) x
fst = forall (k :: * -> * -> *) α α.
ObjectPair k α α =>
RePreArrow k (α, α) α
PreArrowFst
  snd :: forall x y. ObjectPair (RePreArrow k) x y => RePreArrow k (x, y) y
snd = 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 a b.
(Object (RePreArrow k) a, Object (RePreArrow k) b) =>
(forall q.
 Object (RePreArrow k) q =>
 AgentVal (RePreArrow k) q a -> AgentVal (RePreArrow k) q b)
-> RePreArrow k a b
alg = 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
  $~ :: forall a b c.
(Object (RePreArrow k) a, Object (RePreArrow k) b,
 Object (RePreArrow k) 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 :: forall b c.
(Object k b, Object k c, Object (RePreArrow k) b,
 Object (RePreArrow k) c) =>
k b c -> RePreArrow k b c
arr = 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 :: forall a. Object (ReWellPointed k) a => ReWellPointed k a a
id = forall (k :: * -> * -> *) α. Object k α => ReWellPointed k α α
WellPointedId
  WellPointedConst c
c . :: forall a b c.
(Object (ReWellPointed k) a, Object (ReWellPointed k) b,
 Object (ReWellPointed k) c) =>
ReWellPointed k b c -> ReWellPointed k a b -> ReWellPointed k a c
. ReWellPointed k a b
_ = 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
_ = 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 β
f
  ReWellPointed k b c
WellPointedSnd . (ReWellPointed k a β
_`WellPointedFanout`ReWellPointed k a γ
g) = ReWellPointed k a γ
g
  ReWellPointed k b c
WellPointedFst . (ReWellPointed k α β
f`WellPointedPar`ReWellPointed k γ δ
_) = ReWellPointed k α β
f forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) 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 forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) 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 α β
fforall κ (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 α β
h 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 γ δ
gforall κ (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 γ δ
i
  ReWellPointed k b c
WellPointedSwap . ReWellPointed k a b
WellPointedSwap = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReWellPointed k b c
WellPointedRegroup . ReWellPointed k a b
WellPointedRegroup_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  ReWellPointed k b c
WellPointedRegroup_ . ReWellPointed k a b
WellPointedRegroup = 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
f
  ReWellPointed k b c
g . ReWellPointed k a b
WellPointedId = ReWellPointed k b c
g
  ReWellPointed k b c
g . ReWellPointed k a b
f = 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 :: forall a b.
(ObjectPair (ReWellPointed k) a b,
 ObjectPair (ReWellPointed k) b a) =>
ReWellPointed k (a, b) (b, a)
swap = forall (k :: * -> * -> *) α γ.
(ObjectPair k α γ, ObjectPair k γ α) =>
ReWellPointed k (α, γ) (γ, α)
WellPointedSwap
  attachUnit :: forall unit a.
(unit ~ UnitObject (ReWellPointed k),
 ObjectPair (ReWellPointed k) a unit) =>
ReWellPointed k a (a, unit)
attachUnit = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
ReWellPointed k α (α, α)
WellPointedAttachUnit
  detachUnit :: forall unit a.
(unit ~ UnitObject (ReWellPointed k),
 ObjectPair (ReWellPointed k) a unit) =>
ReWellPointed k (a, unit) a
detachUnit = forall (k :: * -> * -> *) α α.
(Object k α, UnitObject k ~ α, ObjectPair k α α) =>
ReWellPointed k (α, α) α
WellPointedDetachUnit
  regroup :: forall a b c.
(ObjectPair (ReWellPointed k) a b,
 ObjectPair (ReWellPointed k) b c,
 ObjectPair (ReWellPointed k) a (b, c),
 ObjectPair (ReWellPointed k) (a, b) c) =>
ReWellPointed k (a, (b, c)) ((a, b), c)
regroup = forall (k :: * -> * -> *) α γ β.
(ObjectPair k α γ, ObjectPair k γ β, ObjectPair k α (γ, β),
 ObjectPair k (α, γ) β) =>
ReWellPointed k (α, (γ, β)) ((α, γ), β)
WellPointedRegroup
  regroup' :: forall a b c.
(ObjectPair (ReWellPointed k) a b,
 ObjectPair (ReWellPointed k) b c,
 ObjectPair (ReWellPointed k) a (b, c),
 ObjectPair (ReWellPointed k) (a, b) c) =>
ReWellPointed k ((a, b), c) (a, (b, c))
regroup' = 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 *** :: forall b b' c c'.
(ObjectPair (ReWellPointed k) b b',
 ObjectPair (ReWellPointed k) c c') =>
ReWellPointed k b c
-> ReWellPointed k b' c' -> ReWellPointed k (b, b') (c, c')
*** ReWellPointed k b' c'
g = 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 &&& :: forall b c c'.
(Object (ReWellPointed k) b, ObjectPair (ReWellPointed k) c c') =>
ReWellPointed k b c
-> ReWellPointed k b c' -> ReWellPointed k b (c, c')
&&& ReWellPointed k b c'
g = forall (k :: * -> * -> *) α α γ.
(Object k α, ObjectPair k α γ) =>
ReWellPointed k α α
-> ReWellPointed k α γ -> ReWellPointed k α (α, γ)
WellPointedFanout ReWellPointed k b c
f ReWellPointed k b c'
g
  terminal :: forall b.
Object (ReWellPointed k) b =>
ReWellPointed k b (UnitObject (ReWellPointed k))
terminal = forall (k :: * -> * -> *) α.
Object k α =>
ReWellPointed k α (UnitObject k)
WellPointedTerminal
  fst :: forall x y.
ObjectPair (ReWellPointed k) x y =>
ReWellPointed k (x, y) x
fst = forall (k :: * -> * -> *) α α.
ObjectPair k α α =>
ReWellPointed k (α, α) α
WellPointedFst
  snd :: forall x y.
ObjectPair (ReWellPointed k) x y =>
ReWellPointed k (x, y) y
snd = forall (k :: * -> * -> *) α β.
ObjectPair k α β =>
ReWellPointed k (α, β) β
WellPointedSnd

instance WellPointed k => WellPointed (ReWellPointed k) where
  type PointObject (ReWellPointed k) α = PointObject k α
  const :: forall b x.
(Object (ReWellPointed k) b, ObjectPoint (ReWellPointed k) x) =>
x -> ReWellPointed k b x
const = forall (k :: * -> * -> *) ν α.
(Object k ν, ObjectPoint k α) =>
α -> ReWellPointed k ν α
WellPointedConst
  unit :: CatTagged (ReWellPointed k) (UnitObject (ReWellPointed k))
unit = forall (k :: * -> * -> *).
WellPointed k =>
CatTagged (ReWellPointed k) (UnitObject k)
u
   where u :: ∀ k . WellPointed k => CatTagged (ReWellPointed k) (UnitObject k)
         u :: forall (k :: * -> * -> *).
WellPointed k =>
CatTagged (ReWellPointed k) (UnitObject k)
u = forall {k} (s :: k) b. b -> Tagged s b
Tagged UnitObject k
u' where Tagged UnitObject k
u' = 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 a b.
(Object (ReWellPointed k) a, Object (ReWellPointed k) b) =>
(forall q.
 Object (ReWellPointed k) q =>
 AgentVal (ReWellPointed k) q a -> AgentVal (ReWellPointed k) q b)
-> ReWellPointed k a b
alg = 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
  $~ :: forall a b c.
(Object (ReWellPointed k) a, Object (ReWellPointed k) b,
 Object (ReWellPointed k) 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 :: forall b c.
(Object k b, Object k c, Object (ReWellPointed k) b,
 Object (ReWellPointed k) c) =>
k b c -> ReWellPointed k b c
arr = forall (k :: * -> * -> *) α β. k α β -> ReWellPointed k α β
ReWellPointed