-- |
-- Module      : Data.Embedding
-- Copyright   : (c) Justus Sagemüller 2015
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveFoldable             #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE UnicodeSyntax              #-}
{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE PatternGuards              #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE DataKinds                  #-}

module Data.Embedding where

import qualified Prelude as Hask hiding(foldl)
import qualified Control.Applicative as Hask
import qualified Control.Monad       as Hask
import qualified Data.Foldable       as Hask


import Control.Category.Constrained.Prelude hiding ((^))
import Control.Arrow.Constrained




data Isomorphism c a b = Isomorphism { forall (c :: * -> * -> *) a b. Isomorphism c a b -> c a b
forwardIso :: c a b
                                     , forall (c :: * -> * -> *) a b. Isomorphism c a b -> c b a
backwardIso :: c b a }

infixr 0 $->$, $<-$
($->$) :: (Function c, Object c a, Object c b) => Isomorphism c a b -> a -> b
Isomorphism c a b
f c b a
_ $->$ :: forall (c :: * -> * -> *) a b.
(Function c, Object c a, Object c b) =>
Isomorphism c a b -> a -> b
$->$ a
x = c a b
f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a
x

($<-$) :: (Function c, Object c b, Object c a) => Isomorphism c a b -> b -> a
Isomorphism c a b
_ c b a
p $<-$ :: forall (c :: * -> * -> *) b a.
(Function c, Object c b, Object c a) =>
Isomorphism c a b -> b -> a
$<-$ b
y = c b a
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ b
y

fromInversePair :: c a b -> c b a -> Isomorphism c a b
fromInversePair :: forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
fromInversePair = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism

perfectInvert :: Isomorphism c a b -> Isomorphism c b a
perfectInvert :: forall (c :: * -> * -> *) a b.
Isomorphism c a b -> Isomorphism c b a
perfectInvert (Isomorphism c a b
f c b a
b) = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c b a
b c a b
f

instance (Category c) => Category (Isomorphism c) where
  type Object (Isomorphism c) a = Object c a
  id :: forall a. Object (Isomorphism c) a => Isomorphism c a a
id = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  Isomorphism c b c
e c c b
p . :: forall a b c.
(Object (Isomorphism c) a, Object (Isomorphism c) b,
 Object (Isomorphism c) c) =>
Isomorphism c b c -> Isomorphism c a b -> Isomorphism c a c
. Isomorphism c a b
f c b a
q = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism (c b c
eforall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
.c a b
f) (c b a
qforall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
.c c b
p)

instance (Cartesian c) => Cartesian (Isomorphism c) where
  type UnitObject (Isomorphism c) = UnitObject c
  type PairObjects (Isomorphism c) a b = PairObjects c a b
  swap :: forall a b.
(ObjectPair (Isomorphism c) a b, ObjectPair (Isomorphism c) b a) =>
Isomorphism c (a, b) (b, a)
swap = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: forall unit a.
(unit ~ UnitObject (Isomorphism c),
 ObjectPair (Isomorphism c) a unit) =>
Isomorphism c a (a, unit)
attachUnit = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit
  detachUnit :: forall unit a.
(unit ~ UnitObject (Isomorphism c),
 ObjectPair (Isomorphism c) a unit) =>
Isomorphism c (a, unit) a
detachUnit = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  regroup :: forall a b c.
(ObjectPair (Isomorphism c) a b, ObjectPair (Isomorphism c) b c,
 ObjectPair (Isomorphism c) a (b, c),
 ObjectPair (Isomorphism c) (a, b) c) =>
Isomorphism c (a, (b, c)) ((a, b), c)
regroup = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup'
  regroup' :: forall a b c.
(ObjectPair (Isomorphism c) a b, ObjectPair (Isomorphism c) b c,
 ObjectPair (Isomorphism c) a (b, c),
 ObjectPair (Isomorphism c) (a, b) c) =>
Isomorphism c ((a, b), c) (a, (b, c))
regroup' = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup' forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup

instance (CoCartesian c) => CoCartesian (Isomorphism c) where
  type ZeroObject (Isomorphism c) = ZeroObject c
  type SumObjects (Isomorphism c) a b = SumObjects c a b
  coSwap :: forall a b.
(ObjectSum (Isomorphism c) a b, ObjectSum (Isomorphism c) b a) =>
Isomorphism c (a + b) (b + a)
coSwap = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap
  attachZero :: forall a zero.
(Object (Isomorphism c) a, zero ~ ZeroObject (Isomorphism c),
 ObjectSum (Isomorphism c) a zero) =>
Isomorphism c a (a + zero)
attachZero = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero
  detachZero :: forall a zero.
(Object (Isomorphism c) a, zero ~ ZeroObject (Isomorphism c),
 ObjectSum (Isomorphism c) a zero) =>
Isomorphism c (a + zero) a
detachZero = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero
  coRegroup :: forall a c b.
(Object (Isomorphism c) a, Object (Isomorphism c) c,
 ObjectSum (Isomorphism c) a b, ObjectSum (Isomorphism c) b c,
 ObjectSum (Isomorphism c) a (b + c),
 ObjectSum (Isomorphism c) (a + b) c) =>
Isomorphism c (a + (b + c)) ((a + b) + c)
coRegroup = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k (a + (b + c)) ((a + b) + c)
coRegroup forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k ((a + b) + c) (a + (b + c))
coRegroup'
  coRegroup' :: forall a c b.
(Object (Isomorphism c) a, Object (Isomorphism c) c,
 ObjectSum (Isomorphism c) a b, ObjectSum (Isomorphism c) b c,
 ObjectSum (Isomorphism c) a (b + c),
 ObjectSum (Isomorphism c) (a + b) c) =>
Isomorphism c ((a + b) + c) (a + (b + c))
coRegroup' = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k ((a + b) + c) (a + (b + c))
coRegroup' forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k (a + (b + c)) ((a + b) + c)
coRegroup
  maybeAsSum :: forall u a.
(ObjectSum (Isomorphism c) u a, u ~ UnitObject (Isomorphism c),
 Object (Isomorphism c) (Maybe a)) =>
Isomorphism c (Maybe a) (u + a)
maybeAsSum = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum
  maybeFromSum :: forall u a.
(ObjectSum (Isomorphism c) u a, u ~ UnitObject (Isomorphism c),
 Object (Isomorphism c) (Maybe a)) =>
Isomorphism c (u + a) (Maybe a)
maybeFromSum = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum
  boolAsSum :: forall u.
(ObjectSum (Isomorphism c) u u, u ~ UnitObject (Isomorphism c),
 Object (Isomorphism c) Bool) =>
Isomorphism c Bool (u + u)
boolAsSum = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
boolFromSum
  boolFromSum :: forall u.
(ObjectSum (Isomorphism c) u u, u ~ UnitObject (Isomorphism c),
 Object (Isomorphism c) Bool) =>
Isomorphism c (u + u) Bool
boolFromSum = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
boolFromSum forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum

instance (Morphism c) => Morphism (Isomorphism c) where
  Isomorphism c b c
e c c b
p *** :: forall b b' c c'.
(ObjectPair (Isomorphism c) b b',
 ObjectPair (Isomorphism c) c c') =>
Isomorphism c b c
-> Isomorphism c b' c' -> Isomorphism c (b, b') (c, c')
*** Isomorphism c b' c'
f c c' b'
q = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism (c b c
eforall (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' c'
f) (c c b
pforall (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 c' b'
q)
  
instance (MorphChoice c) => MorphChoice (Isomorphism c) where
  Isomorphism c b c
e c c b
p +++ :: forall b b' c c'.
(ObjectSum (Isomorphism c) b b', ObjectSum (Isomorphism c) c c') =>
Isomorphism c b c
-> Isomorphism c b' c' -> Isomorphism c (b + b') (c + c')
+++ Isomorphism c b' c'
f c c' b'
q = forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism (c b c
eforall (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' c'
f) (c c b
pforall (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 c' b'
q)

instance (Category c) => EnhancedCat c (Isomorphism c) where 
  arr :: forall b c.
(Object (Isomorphism c) b, Object (Isomorphism c) c, Object c b,
 Object c c) =>
Isomorphism c b c -> c b c
arr = forall (c :: * -> * -> *) a b. Isomorphism c a b -> c a b
forwardIso

instance (Category c) => EnhancedCat (Embedding c) (Isomorphism c) where 
  arr :: forall b c.
(Object (Isomorphism c) b, Object (Isomorphism c) c,
 Object (Embedding c) b, Object (Embedding c) c) =>
Isomorphism c b c -> Embedding c b c
arr (Isomorphism c b c
f c c b
b) = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c b c
f c c b
b


    
-- | A pair of matching functions. The projection must be a left (but not necessarily right)
--   inverse of the embedding,
--   i.e. the cardinality of @a@ will have to be less or equal than the cardinality
--   of @b@.
data Embedding c a b = Embedding { forall (c :: * -> * -> *) a b. Embedding c a b -> c a b
embedding :: c a b
                                 , forall (c :: * -> * -> *) a b. Embedding c a b -> c b a
projection :: c b a
                                 }

fromEmbedProject :: c a b -- ^ Injective embedding
                 -> c b a -- ^ Surjective projection. Must be left inverse of embedding.
                 -> Embedding c a b
fromEmbedProject :: forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
fromEmbedProject = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding


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

(>-$) :: (Function c, Object c b, Object c a) => Embedding c a b -> b -> a
Embedding c a b
_ c b a
p >-$ :: forall (c :: * -> * -> *) b a.
(Function c, Object c b, Object c a) =>
Embedding c a b -> b -> a
>-$ b
y = c b a
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ b
y


instance (Category c) => Category (Embedding c) where
  type Object (Embedding c) a = Object c a
  id :: forall a. Object (Embedding c) a => Embedding c a a
id = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  Embedding c b c
e c c b
p . :: forall a b c.
(Object (Embedding c) a, Object (Embedding c) b,
 Object (Embedding c) c) =>
Embedding c b c -> Embedding c a b -> Embedding c a c
. Embedding c a b
f c b a
q = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (c b c
eforall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
.c a b
f) (c b a
qforall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
.c c b
p)

instance (Cartesian c) => Cartesian (Embedding c) where
  type UnitObject (Embedding c) = UnitObject c
  type PairObjects (Embedding c) a b = PairObjects c a b
  swap :: forall a b.
(ObjectPair (Embedding c) a b, ObjectPair (Embedding c) b a) =>
Embedding c (a, b) (b, a)
swap = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: forall unit a.
(unit ~ UnitObject (Embedding c),
 ObjectPair (Embedding c) a unit) =>
Embedding c a (a, unit)
attachUnit = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit
  detachUnit :: forall unit a.
(unit ~ UnitObject (Embedding c),
 ObjectPair (Embedding c) a unit) =>
Embedding c (a, unit) a
detachUnit = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  regroup :: forall a b c.
(ObjectPair (Embedding c) a b, ObjectPair (Embedding c) b c,
 ObjectPair (Embedding c) a (b, c),
 ObjectPair (Embedding c) (a, b) c) =>
Embedding c (a, (b, c)) ((a, b), c)
regroup = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup'
  regroup' :: forall a b c.
(ObjectPair (Embedding c) a b, ObjectPair (Embedding c) b c,
 ObjectPair (Embedding c) a (b, c),
 ObjectPair (Embedding c) (a, b) c) =>
Embedding c ((a, b), c) (a, (b, c))
regroup' = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup' forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup

instance (CoCartesian c) => CoCartesian (Embedding c) where
  type ZeroObject (Embedding c) = ZeroObject c
  type SumObjects (Embedding c) a b = SumObjects c a b
  coSwap :: forall a b.
(ObjectSum (Embedding c) a b, ObjectSum (Embedding c) b a) =>
Embedding c (a + b) (b + a)
coSwap = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap
  attachZero :: forall a zero.
(Object (Embedding c) a, zero ~ ZeroObject (Embedding c),
 ObjectSum (Embedding c) a zero) =>
Embedding c a (a + zero)
attachZero = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero
  detachZero :: forall a zero.
(Object (Embedding c) a, zero ~ ZeroObject (Embedding c),
 ObjectSum (Embedding c) a zero) =>
Embedding c (a + zero) a
detachZero = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero
  coRegroup :: forall a c b.
(Object (Embedding c) a, Object (Embedding c) c,
 ObjectSum (Embedding c) a b, ObjectSum (Embedding c) b c,
 ObjectSum (Embedding c) a (b + c),
 ObjectSum (Embedding c) (a + b) c) =>
Embedding c (a + (b + c)) ((a + b) + c)
coRegroup = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k (a + (b + c)) ((a + b) + c)
coRegroup forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k ((a + b) + c) (a + (b + c))
coRegroup'
  coRegroup' :: forall a c b.
(Object (Embedding c) a, Object (Embedding c) c,
 ObjectSum (Embedding c) a b, ObjectSum (Embedding c) b c,
 ObjectSum (Embedding c) a (b + c),
 ObjectSum (Embedding c) (a + b) c) =>
Embedding c ((a + b) + c) (a + (b + c))
coRegroup' = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k ((a + b) + c) (a + (b + c))
coRegroup' forall (k :: * -> * -> *) a c b.
(CoCartesian k, Object k a, Object k c, ObjectSum k a b,
 ObjectSum k b c, ObjectSum k a (b + c), ObjectSum k (a + b) c) =>
k (a + (b + c)) ((a + b) + c)
coRegroup
  maybeAsSum :: forall u a.
(ObjectSum (Embedding c) u a, u ~ UnitObject (Embedding c),
 Object (Embedding c) (Maybe a)) =>
Embedding c (Maybe a) (u + a)
maybeAsSum = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum
  maybeFromSum :: forall u a.
(ObjectSum (Embedding c) u a, u ~ UnitObject (Embedding c),
 Object (Embedding c) (Maybe a)) =>
Embedding c (u + a) (Maybe a)
maybeFromSum = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum
  boolAsSum :: forall u.
(ObjectSum (Embedding c) u u, u ~ UnitObject (Embedding c),
 Object (Embedding c) Bool) =>
Embedding c Bool (u + u)
boolAsSum = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
boolFromSum
  boolFromSum :: forall u.
(ObjectSum (Embedding c) u u, u ~ UnitObject (Embedding c),
 Object (Embedding c) Bool) =>
Embedding c (u + u) Bool
boolFromSum = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
boolFromSum forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum

instance (Morphism c) => Morphism (Embedding c) where
  Embedding c b c
e c c b
p *** :: forall b b' c c'.
(ObjectPair (Embedding c) b b', ObjectPair (Embedding c) c c') =>
Embedding c b c -> Embedding c b' c' -> Embedding c (b, b') (c, c')
*** Embedding c b' c'
f c c' b'
q = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (c b c
eforall (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' c'
f) (c c b
pforall (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 c' b'
q)
  
instance (MorphChoice c) => MorphChoice (Embedding c) where
  Embedding c b c
e c c b
p +++ :: forall b b' c c'.
(ObjectSum (Embedding c) b b', ObjectSum (Embedding c) c c') =>
Embedding c b c
-> Embedding c b' c' -> Embedding c (b + b') (c + c')
+++ Embedding c b' c'
f c c' b'
q = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (c b c
eforall (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' c'
f) (c c b
pforall (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 c' b'
q)

instance (Category c) => EnhancedCat c (Embedding c) where 
  arr :: forall b c.
(Object (Embedding c) b, Object (Embedding c) c, Object c b,
 Object c c) =>
Embedding c b c -> c b c
arr = forall (c :: * -> * -> *) a b. Embedding c a b -> c a b
embedding