{-# 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
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
-> c b a
-> 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