-- |
-- 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 { Isomorphism c a b -> c a b
forwardIso :: 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
_ $->$ :: Isomorphism c a b -> a -> b
$->$ a
x = c a b
f c a b -> a -> b
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 $<-$ :: Isomorphism c a b -> b -> a
$<-$ b
y = c b a
p c b a -> b -> a
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 :: c a b -> c b a -> Isomorphism c a b
fromInversePair = c a b -> c b a -> Isomorphism c a b
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 :: Isomorphism c a b -> Isomorphism c b a
perfectInvert (Isomorphism c a b
f c b a
b) = c b a -> c a b -> Isomorphism c b a
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 :: Isomorphism c a a
id = c a a -> c a a -> Isomorphism c a a
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id c a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  Isomorphism c b c
e c c b
p . :: Isomorphism c b c -> Isomorphism c a b -> Isomorphism c a c
. Isomorphism c a b
f c b a
q = c a c -> c c a -> Isomorphism c a c
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism (c b c
ec b c -> c a b -> c a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
.c a b
f) (c b a
qc b a -> c c b -> c c a
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
.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 :: Isomorphism c (a, b) (b, a)
swap = c (a, b) (b, a) -> c (b, a) (a, b) -> Isomorphism c (a, b) (b, a)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c (a, b) (b, a)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap c (b, a) (a, b)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: Isomorphism c a (a, unit)
attachUnit = c a (a, unit) -> c (a, unit) a -> Isomorphism c a (a, unit)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c a (a, unit)
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit c (a, unit) a
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit
  detachUnit :: Isomorphism c (a, unit) a
detachUnit = c (a, unit) a -> c a (a, unit) -> Isomorphism c (a, unit) a
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c (a, unit) a
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit c a (a, unit)
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  regroup :: Isomorphism c (a, (b, c)) ((a, b), c)
regroup = c (a, (b, c)) ((a, b), c)
-> c ((a, b), c) (a, (b, c))
-> Isomorphism c (a, (b, c)) ((a, b), c)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c (a, (b, c)) ((a, b), c)
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 c ((a, b), c) (a, (b, c))
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' :: Isomorphism c ((a, b), c) (a, (b, c))
regroup' = c ((a, b), c) (a, (b, c))
-> c (a, (b, c)) ((a, b), c)
-> Isomorphism c ((a, b), c) (a, (b, c))
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c ((a, b), c) (a, (b, c))
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' c (a, (b, c)) ((a, b), c)
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 :: Isomorphism c (a + b) (b + a)
coSwap = c (a + b) (b + a)
-> c (b + a) (a + b) -> Isomorphism c (a + b) (b + a)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c (a + b) (b + a)
forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap c (b + a) (a + b)
forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap
  attachZero :: Isomorphism c a (a + zero)
attachZero = c a (a + zero) -> c (a + zero) a -> Isomorphism c a (a + zero)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c a (a + zero)
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero c (a + zero) a
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero
  detachZero :: Isomorphism c (a + zero) a
detachZero = c (a + zero) a -> c a (a + zero) -> Isomorphism c (a + zero) a
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c (a + zero) a
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero c a (a + zero)
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero
  coRegroup :: Isomorphism c (a + (b + c)) ((a + b) + c)
coRegroup = c (a + (b + c)) ((a + b) + c)
-> c ((a + b) + c) (a + (b + c))
-> Isomorphism c (a + (b + c)) ((a + b) + c)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c (a + (b + c)) ((a + b) + c)
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 c ((a + b) + c) (a + (b + c))
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' :: Isomorphism c ((a + b) + c) (a + (b + c))
coRegroup' = c ((a + b) + c) (a + (b + c))
-> c (a + (b + c)) ((a + b) + c)
-> Isomorphism c ((a + b) + c) (a + (b + c))
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c ((a + b) + c) (a + (b + c))
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' c (a + (b + c)) ((a + b) + c)
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 :: Isomorphism c (Maybe a) (u + a)
maybeAsSum = c (Maybe a) (u + a)
-> c (u + a) (Maybe a) -> Isomorphism c (Maybe a) (u + a)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c (Maybe a) (u + a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum c (u + a) (Maybe a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum
  maybeFromSum :: Isomorphism c (u + a) (Maybe a)
maybeFromSum = c (u + a) (Maybe a)
-> c (Maybe a) (u + a) -> Isomorphism c (u + a) (Maybe a)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c (u + a) (Maybe a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum c (Maybe a) (u + a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum
  boolAsSum :: Isomorphism c Bool (u + u)
boolAsSum = c Bool (u + u) -> c (u + u) Bool -> Isomorphism c Bool (u + u)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c Bool (u + u)
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum c (u + u) Bool
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
boolFromSum
  boolFromSum :: Isomorphism c (u + u) Bool
boolFromSum = c (u + u) Bool -> c Bool (u + u) -> Isomorphism c (u + u) Bool
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism c (u + u) Bool
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
boolFromSum c Bool (u + u)
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 *** :: Isomorphism c b c
-> Isomorphism c b' c' -> Isomorphism c (b, b') (c, c')
*** Isomorphism c b' c'
f c c' b'
q = c (b, b') (c, c')
-> c (c, c') (b, b') -> Isomorphism c (b, b') (c, c')
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism (c b c
ec b c -> c b' c' -> c (b, b') (c, c')
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***c b' c'
f) (c c b
pc c b -> c c' b' -> c (c, c') (b, b')
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***c c' b'
q)
  
instance (MorphChoice c) => MorphChoice (Isomorphism c) where
  Isomorphism c b c
e c c b
p +++ :: Isomorphism c b c
-> Isomorphism c b' c' -> Isomorphism c (b + b') (c + c')
+++ Isomorphism c b' c'
f c c' b'
q = c (b + b') (c + c')
-> c (c + c') (b + b') -> Isomorphism c (b + b') (c + c')
forall (c :: * -> * -> *) a b. c a b -> c b a -> Isomorphism c a b
Isomorphism (c b c
ec b c -> c b' c' -> c (b + b') (c + c')
forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++c b' c'
f) (c c b
pc c b -> c c' b' -> c (c + c') (b + b')
forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++c c' b'
q)

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

instance (Category c) => EnhancedCat (Embedding c) (Isomorphism c) where 
  arr :: Isomorphism c b c -> Embedding c b c
arr (Isomorphism c b c
f c c b
b) = c b c -> c c b -> Embedding c b c
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 { Embedding c a b -> c a b
embedding :: 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 :: c a b -> c b a -> Embedding c a b
fromEmbedProject = c a b -> c b a -> Embedding c a b
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
_ $-> :: Embedding c a b -> a -> b
$-> a
x = c a b
f c a b -> a -> b
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 >-$ :: Embedding c a b -> b -> a
>-$ b
y = c b a
p c b a -> b -> a
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 :: Embedding c a a
id = c a a -> c a a -> Embedding c a a
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id c a a
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  Embedding c b c
e c c b
p . :: Embedding c b c -> Embedding c a b -> Embedding c a c
. Embedding c a b
f c b a
q = c a c -> c c a -> Embedding c a c
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (c b c
ec b c -> c a b -> c a c
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
.c a b
f) (c b a
qc b a -> c c b -> c c a
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
.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 :: Embedding c (a, b) (b, a)
swap = c (a, b) (b, a) -> c (b, a) (a, b) -> Embedding c (a, b) (b, a)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c (a, b) (b, a)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap c (b, a) (a, b)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: Embedding c a (a, unit)
attachUnit = c a (a, unit) -> c (a, unit) a -> Embedding c a (a, unit)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c a (a, unit)
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit c (a, unit) a
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit
  detachUnit :: Embedding c (a, unit) a
detachUnit = c (a, unit) a -> c a (a, unit) -> Embedding c (a, unit) a
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c (a, unit) a
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit c a (a, unit)
forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit
  regroup :: Embedding c (a, (b, c)) ((a, b), c)
regroup = c (a, (b, c)) ((a, b), c)
-> c ((a, b), c) (a, (b, c)) -> Embedding c (a, (b, c)) ((a, b), c)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c (a, (b, c)) ((a, b), c)
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 c ((a, b), c) (a, (b, c))
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' :: Embedding c ((a, b), c) (a, (b, c))
regroup' = c ((a, b), c) (a, (b, c))
-> c (a, (b, c)) ((a, b), c) -> Embedding c ((a, b), c) (a, (b, c))
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c ((a, b), c) (a, (b, c))
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' c (a, (b, c)) ((a, b), c)
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 :: Embedding c (a + b) (b + a)
coSwap = c (a + b) (b + a)
-> c (b + a) (a + b) -> Embedding c (a + b) (b + a)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c (a + b) (b + a)
forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap c (b + a) (a + b)
forall (k :: * -> * -> *) a b.
(CoCartesian k, ObjectSum k a b, ObjectSum k b a) =>
k (a + b) (b + a)
coSwap
  attachZero :: Embedding c a (a + zero)
attachZero = c a (a + zero) -> c (a + zero) a -> Embedding c a (a + zero)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c a (a + zero)
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero c (a + zero) a
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero
  detachZero :: Embedding c (a + zero) a
detachZero = c (a + zero) a -> c a (a + zero) -> Embedding c (a + zero) a
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c (a + zero) a
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k (a + zero) a
detachZero c a (a + zero)
forall (k :: * -> * -> *) a zero.
(CoCartesian k, Object k a, zero ~ ZeroObject k,
 ObjectSum k a zero) =>
k a (a + zero)
attachZero
  coRegroup :: Embedding c (a + (b + c)) ((a + b) + c)
coRegroup = c (a + (b + c)) ((a + b) + c)
-> c ((a + b) + c) (a + (b + c))
-> Embedding c (a + (b + c)) ((a + b) + c)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c (a + (b + c)) ((a + b) + c)
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 c ((a + b) + c) (a + (b + c))
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' :: Embedding c ((a + b) + c) (a + (b + c))
coRegroup' = c ((a + b) + c) (a + (b + c))
-> c (a + (b + c)) ((a + b) + c)
-> Embedding c ((a + b) + c) (a + (b + c))
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c ((a + b) + c) (a + (b + c))
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' c (a + (b + c)) ((a + b) + c)
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 :: Embedding c (Maybe a) (u + a)
maybeAsSum = c (Maybe a) (u + a)
-> c (u + a) (Maybe a) -> Embedding c (Maybe a) (u + a)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c (Maybe a) (u + a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum c (u + a) (Maybe a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum
  maybeFromSum :: Embedding c (u + a) (Maybe a)
maybeFromSum = c (u + a) (Maybe a)
-> c (Maybe a) (u + a) -> Embedding c (u + a) (Maybe a)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c (u + a) (Maybe a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (u + a) (Maybe a)
maybeFromSum c (Maybe a) (u + a)
forall (k :: * -> * -> *) u a.
(CoCartesian k, ObjectSum k u a, u ~ UnitObject k,
 Object k (Maybe a)) =>
k (Maybe a) (u + a)
maybeAsSum
  boolAsSum :: Embedding c Bool (u + u)
boolAsSum = c Bool (u + u) -> c (u + u) Bool -> Embedding c Bool (u + u)
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c Bool (u + u)
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k Bool (u + u)
boolAsSum c (u + u) Bool
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
boolFromSum
  boolFromSum :: Embedding c (u + u) Bool
boolFromSum = c (u + u) Bool -> c Bool (u + u) -> Embedding c (u + u) Bool
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding c (u + u) Bool
forall (k :: * -> * -> *) u.
(CoCartesian k, ObjectSum k u u, u ~ UnitObject k,
 Object k Bool) =>
k (u + u) Bool
boolFromSum c Bool (u + u)
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 *** :: Embedding c b c -> Embedding c b' c' -> Embedding c (b, b') (c, c')
*** Embedding c b' c'
f c c' b'
q = c (b, b') (c, c')
-> c (c, c') (b, b') -> Embedding c (b, b') (c, c')
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (c b c
ec b c -> c b' c' -> c (b, b') (c, c')
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***c b' c'
f) (c c b
pc c b -> c c' b' -> c (c, c') (b, b')
forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
***c c' b'
q)
  
instance (MorphChoice c) => MorphChoice (Embedding c) where
  Embedding c b c
e c c b
p +++ :: Embedding c b c
-> Embedding c b' c' -> Embedding c (b + b') (c + c')
+++ Embedding c b' c'
f c c' b'
q = c (b + b') (c + c')
-> c (c + c') (b + b') -> Embedding c (b + b') (c + c')
forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (c b c
ec b c -> c b' c' -> c (b + b') (c + c')
forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++c b' c'
f) (c c b
pc c b -> c c' b' -> c (c + c') (b + b')
forall (a :: * -> * -> *) b b' c c'.
(MorphChoice a, ObjectSum a b b', ObjectSum a c c') =>
a b c -> a b' c' -> a (b + b') (c + c')
+++c c' b'
q)

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