{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds #-}

-- |

-- Module      : OAlg.Category.Definition

-- Description : definition of categories

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- categories of morphisms. We adapted the concept of categories form 'Control.Category.Category' to

-- better cover our needs.

module OAlg.Category.Definition
  (
    -- * Category

    Category(..), cOne'
  , Sub(..), cOneSub, sub, sub', subG
  , Op2(..)

    -- | __Some basic definitions in the category @('->')@__

  , id
  , const
  , curry, uncurry, fst, snd
  , curry3, uncurry3

    -- * Cayleyan

  , Cayleyan2(..), Inv2(..), inv2
  , inv2Forget
  
    -- * Morphism

  , Morphism(..)
  , Homomorphous(..), tauHom, tauHomG, tau1Hom
  , eqlDomain, eqlRange, eqlEndo
  , eqlMorphism
  -- , toOp2Struct


    -- * Applicative

  , ApplicativeG(..)
  , Applicative1, amap1
  
    -- * Functorial

  , amapF
  , Functorial1, Functor1(..)
  , FunctorialG, FunctorG(..)
  
    -- * Transformables

  , TransformableObjectClass 

  , TransformableObjectClassTyp
  , TransformableGObjectClass
  , TransformableGObjectClassDomain
  , TransformableGObjectClassRange

  )
  where

import Data.Bool

import Data.Type.Equality
import Data.Typeable
import Data.Kind
import Data.Maybe
import Data.List ((++))

import OAlg.Data.Show
import OAlg.Data.Equal

import OAlg.Data.Either

import OAlg.Category.Applicative

import OAlg.Structure.Definition

--------------------------------------------------------------------------------

-- Defs -


-- | the identity map.

id :: x -> x
id :: forall x. x -> x
id = \x
x -> x
x

-- | the constant map given by a value in @__b__@.

--

-- __Property__ Let @y@ be in @__b__@ then for all @x@ in @__a__@ holds: @'const' y x@ is identical

-- to @y@.

const :: b -> a -> b
const :: forall b a. b -> a -> b
const b
b a
_ = b
b

-- | the first component of the pair.

fst :: (a,b) -> a
fst :: forall a b. (a, b) -> a
fst (a
a,b
_) = a
a

-- | the second component of the pair. 

snd :: (a,b) -> b
snd :: forall a b. (a, b) -> b
snd (a
_,b
b) = b
b

-- | currying a map.

curry :: ((a,b) -> c) -> a -> b -> c
curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
curry (a, b) -> c
f a
a b
b = (a, b) -> c
f (a
a,b
b)

-- | uncurrying a map.

uncurry :: (a -> b -> c) -> (a,b) -> c
uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> c
f (a
a,b
b) = a -> b -> c
f a
a b
b

-- | currying a map.

curry3 :: ((a,b,c) -> d) -> a -> b -> c -> d
curry3 :: forall a b c d. ((a, b, c) -> d) -> a -> b -> c -> d
curry3 (a, b, c) -> d
f a
a b
b c
c = (a, b, c) -> d
f (a
a,b
b,c
c)

-- | uncurrying a map.

uncurry3 :: (a -> b -> c -> d) -> (a,b,c) -> d
uncurry3 :: forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 a -> b -> c -> d
f (a
a,b
b,c
c) = a -> b -> c -> d
f a
a b
b c
c

--------------------------------------------------------------------------------

-- eqlDomain -


-- | gets for two 'Typeable' types @__x__@ and @__x'__@ and for two parameterized types maybe an

-- attest that the domain types are equal.

eqlDomain :: Struct Typ x -> Struct Typ x'
  -> m x y -> m x' y -> Maybe (x :~: x')
eqlDomain :: forall x x' (m :: * -> * -> *) y.
Struct Typ x
-> Struct Typ x' -> m x y -> m x' y -> Maybe (x :~: x')
eqlDomain Struct Typ x
Struct Struct Typ x'
Struct m x y
_ m x' y
_ = Maybe (x :~: x')
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

--------------------------------------------------------------------------------

-- eqlRange -


-- | gets for two 'Typeable' types @__y__@ and @__y'__@ and for two parameterized types maybe an

-- attest that the range types are equal.

eqlRange :: Struct Typ y -> Struct Typ y'
  -> m x y -> m x y' -> Maybe (y :~: y')
eqlRange :: forall y y' (m :: * -> * -> *) x.
Struct Typ y
-> Struct Typ y' -> m x y -> m x y' -> Maybe (y :~: y')
eqlRange Struct Typ y
Struct Struct Typ y'
Struct m x y
_ m x y'
_ = Maybe (y :~: y')
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

--------------------------------------------------------------------------------

-- eqlMorphism -


-- | gets maybe an attest that the two given morphisms types are equal. 

eqlMorphism :: Typeable m
  => Struct Typ x -> Struct Typ x'
  -> Struct Typ y -> Struct Typ y'
  -> m x y -> m x' y' -> Maybe (m x y :~: m x' y')
eqlMorphism :: forall (m :: * -> * -> *) x x' y y'.
Typeable m =>
Struct Typ x
-> Struct Typ x'
-> Struct Typ y
-> Struct Typ y'
-> m x y
-> m x' y'
-> Maybe (m x y :~: m x' y')
eqlMorphism Struct Typ x
Struct Struct Typ x'
Struct Struct Typ y
Struct Struct Typ y'
Struct m x y
_ m x' y'
_ = Maybe (m x y :~: m x' y')
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

--------------------------------------------------------------------------------

-- eqlEndo -


-- | maybe endomorphism.

eqlEndo :: Struct Typ x -> Struct Typ y -> h x y -> Maybe (x :~: y)
eqlEndo :: forall x y (h :: * -> * -> *).
Struct Typ x -> Struct Typ y -> h x y -> Maybe (x :~: y)
eqlEndo Struct Typ x
Struct Struct Typ y
Struct h x y
_ = Maybe (x :~: y)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT

--------------------------------------------------------------------------------

-- Homomorphous -


infix 5 :>:

-- | attest that both @__x__@ and @__y__@ have homomorphous structures, i.e.

--   both admit the same constraints given by the parameter @s@.

data Homomorphous s x y = Struct s x :>: Struct s y deriving (Int -> Homomorphous s x y -> ShowS
[Homomorphous s x y] -> ShowS
Homomorphous s x y -> String
(Int -> Homomorphous s x y -> ShowS)
-> (Homomorphous s x y -> String)
-> ([Homomorphous s x y] -> ShowS)
-> Show (Homomorphous s x y)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s x y. Int -> Homomorphous s x y -> ShowS
forall s x y. [Homomorphous s x y] -> ShowS
forall s x y. Homomorphous s x y -> String
$cshowsPrec :: forall s x y. Int -> Homomorphous s x y -> ShowS
showsPrec :: Int -> Homomorphous s x y -> ShowS
$cshow :: forall s x y. Homomorphous s x y -> String
show :: Homomorphous s x y -> String
$cshowList :: forall s x y. [Homomorphous s x y] -> ShowS
showList :: [Homomorphous s x y] -> ShowS
Show,Homomorphous s x y -> Homomorphous s x y -> Bool
(Homomorphous s x y -> Homomorphous s x y -> Bool)
-> (Homomorphous s x y -> Homomorphous s x y -> Bool)
-> Eq (Homomorphous s x y)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s x y. Homomorphous s x y -> Homomorphous s x y -> Bool
$c== :: forall s x y. Homomorphous s x y -> Homomorphous s x y -> Bool
== :: Homomorphous s x y -> Homomorphous s x y -> Bool
$c/= :: forall s x y. Homomorphous s x y -> Homomorphous s x y -> Bool
/= :: Homomorphous s x y -> Homomorphous s x y -> Bool
Eq)

instance Show2 (Homomorphous m)
instance Eq2 (Homomorphous m)

--------------------------------------------------------------------------------

-- tauHom -


-- | transforming homomorphous structural attests. 

tauHom :: Transformable s t => Homomorphous s x y -> Homomorphous t x y
tauHom :: forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (Struct s x
d :>: Struct s y
r) = Struct s x -> Struct t x
forall x. Struct s x -> Struct t x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
d Struct t x -> Struct t y -> Homomorphous t x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct s y -> Struct t y
forall x. Struct s x -> Struct t x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s y
r

--------------------------------------------------------------------------------

-- tauHomG -


-- | transforming homomorphous structural attests.

tauHomG :: TransformableG t u v => Homomorphous u x y -> Homomorphous v (t x) (t y)
tauHomG :: forall (t :: * -> *) u v x y.
TransformableG t u v =>
Homomorphous u x y -> Homomorphous v (t x) (t y)
tauHomG (Struct u x
d :>: Struct u y
r) = Struct u x -> Struct v (t x)
forall x. Struct u x -> Struct v (t x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG Struct u x
d Struct v (t x) -> Struct v (t y) -> Homomorphous v (t x) (t y)
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct u y -> Struct v (t y)
forall x. Struct u x -> Struct v (t x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG Struct u y
r

--------------------------------------------------------------------------------

-- tau1Hom -


-- | transforming homomorphous structural attests. 

tau1Hom :: Transformable1 f s => Homomorphous s x y -> Homomorphous s (f x) (f y)
tau1Hom :: forall (f :: * -> *) s x y.
Transformable1 f s =>
Homomorphous s x y -> Homomorphous s (f x) (f y)
tau1Hom (Struct s x
sx:>:Struct s y
sy) = Struct s x -> Struct s (f x)
forall (f :: * -> *) s x.
Transformable1 f s =>
Struct s x -> Struct s (f x)
tau1 Struct s x
sx Struct s (f x) -> Struct s (f y) -> Homomorphous s (f x) (f y)
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct s y -> Struct s (f y)
forall (f :: * -> *) s x.
Transformable1 f s =>
Struct s x -> Struct s (f x)
tau1 Struct s y
sy

--------------------------------------------------------------------------------

-- Morphism -


-- | morphism.

class Morphism m where
  {-# MINIMAL homomorphous | (domain,range) #-}

  -- | the object class.

  type ObjectClass m

  -- | attests, that the types @__x__@ and @__y__@ fulfill the constraints given

  -- by @'Homomorphous' ('ObjectClass' __m__) __x__ __y__@, i.e both fulfill the constraints

  -- given by @'Structure' ('ObjectClass' __m__) __x__@ and @'Structure' ('ObjectClass' __m__) __y__@

  -- respectively.

  homomorphous :: m x y -> Homomorphous (ObjectClass m) x y
  homomorphous m x y
m = m x y -> Struct (ObjectClass m) x
forall x y. m x y -> Struct (ObjectClass m) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain m x y
m Struct (ObjectClass m) x
-> Struct (ObjectClass m) y -> Homomorphous (ObjectClass m) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: m x y -> Struct (ObjectClass m) y
forall x y. m x y -> Struct (ObjectClass m) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range m x y
m

  -- | attests that the domain type @__x__@ fulfills the constraints given

  -- by @'Structure' ('ObjectClass' __m__) __x__@.

  domain :: m x y -> Struct (ObjectClass m) x
  domain m x y
m = Struct (ObjectClass m) x
d where Struct (ObjectClass m) x
d :>: Struct (ObjectClass m) y
_ = m x y -> Homomorphous (ObjectClass m) x y
forall x y. m x y -> Homomorphous (ObjectClass m) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous m x y
m

  -- | attests that the range type @__y__@ fulfills the constraints given

  -- by @'Structure' ('ObjectClass' __m__) __y__@.

  range  :: m x y -> Struct (ObjectClass m) y
  range m x y
m = Struct (ObjectClass m) y
r where Struct (ObjectClass m) x
_ :>: Struct (ObjectClass m) y
r = m x y -> Homomorphous (ObjectClass m) x y
forall x y. m x y -> Homomorphous (ObjectClass m) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous m x y
m

instance Morphism (Homomorphous s) where
  type ObjectClass (Homomorphous s) = s
  homomorphous :: forall x y.
Homomorphous s x y
-> Homomorphous (ObjectClass (Homomorphous s)) x y
homomorphous = Homomorphous s x y -> Homomorphous s x y
Homomorphous s x y
-> Homomorphous (ObjectClass (Homomorphous s)) x y
forall x. x -> x
id

instance Morphism (->) where
  type ObjectClass (->) = Type
  homomorphous :: forall x y. (x -> y) -> Homomorphous (ObjectClass (->)) x y
homomorphous x -> y
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct Struct (*) x -> Struct (*) y -> Homomorphous (*) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (*) y
forall s x. Structure s x => Struct s x
Struct

--------------------------------------------------------------------------------

-- Category -


infixr 9 .

-- | category of morphisms.

--

--   __Properties__ Let __@c@__ be a type instance of the class 'Category', then

--   holds:

--

--  (1) #Cat1#For all types __@x@__, __@y@__ and @f@ in __@c@__ __@x@__ __@y@__ holds:

--      @'cOne' ('range' f) '.' f 'OAlg.Data.EqualExtensional..=.' f@ and

--      @f '.' 'cOne' ('domain' f) 'OAlg.Data.EqualExtensional..=.' f@.

--

--  (1) #Cat2#For all types __@w@__, __@x@__, __@y@__, __@z@__

--      and @f@ in __@c@__ __@x@__ __@w@__, @g@ in __@c@__ __@y@__ __@x@__,

--      @h@ in __@c@__ __@z@__ __@y@__ holds:

--      @f '.' (g '.' h) 'OAlg.Data.EqualExtensional..=.' (f '.' g) '.' h@. 

class Morphism c => Category c where
  -- | the identity morphism for an eligible __@x@__.

  cOne :: Struct (ObjectClass c) x -> c x x
  (.) :: c y z -> c x y -> c x z

--------------------------------------------------------------------------------

-- cOne' -


-- | prefixing a proxy.

cOne' :: Category c => p c -> Struct (ObjectClass c) x -> c x x
cOne' :: forall (c :: * -> * -> *) (p :: (* -> * -> *) -> *) x.
Category c =>
p c -> Struct (ObjectClass c) x -> c x x
cOne' p c
_ = Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne

--------------------------------------------------------------------------------

-- Category - Instance -


instance Category (Homomorphous s) where
  cOne :: forall x.
Struct (ObjectClass (Homomorphous s)) x -> Homomorphous s x x
cOne Struct (ObjectClass (Homomorphous s)) x
s = Struct s x
Struct (ObjectClass (Homomorphous s)) x
s Struct s x -> Struct s x -> Homomorphous s x x
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct s x
Struct (ObjectClass (Homomorphous s)) x
s
  (Struct s y
Struct :>: Struct s z
c) . :: forall y z x.
Homomorphous s y z -> Homomorphous s x y -> Homomorphous s x z
. (Struct s x
a :>: Struct s y
Struct) = Struct s x
aStruct s x -> Struct s z -> Homomorphous s x z
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>:Struct s z
c

instance Category (->) where
  cOne :: forall x. Struct (ObjectClass (->)) x -> x -> x
cOne Struct (ObjectClass (->)) x
Struct = \x
x -> x
x
  y -> z
f . :: forall y z x. (y -> z) -> (x -> y) -> x -> z
. x -> y
g = \x
x -> y -> z
f (x -> y
g x
x)

--------------------------------------------------------------------------------

-- FunctorialG -


-- | functorials from @'Category' __a__@ to @'Category' __b__@ according to the

-- type function @__t__@.

--

--   __Properties__ Let @'FunctorialG' __f a b__@, the holdst: 

--

--   (1) For all @__x__@ and  @s@ in @'Struct' ('ObjectClass' __a__) __x__@ holds:

--   @'amapG' ('cOne' s) 'OAlg.Data.EqualExtensional..=.' 'cOne' ('tauG' s)@.

--

--   (1) For all __@x@__, __@y@__, __@z@__ and @f@ in __@c@__ __@y@__ __@z@__,

--   @g@ in __@c@__ __@x@__ __@y@__ holds:

--   @'amapG' (f '.' g) 'OAlg.Data.EqualExtensional..=.' 'amapG' f '.' 'amapG' g@. 

class ( Category a, Category b, ApplicativeG t a b
      , TransformableG t (ObjectClass a) (ObjectClass b)
      ) => FunctorialG t a b

--------------------------------------------------------------------------------

-- amapF -


-- | functorial application.

amapF :: FunctorialG t a b => a x y -> b (t x) (t y)
amapF :: forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF = a x y -> b (t x) (t y)
forall x y. a x y -> b (t x) (t y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG

--------------------------------------------------------------------------------

-- Op2 -


-- | Predicat for the opposite of a two parametrized type @__h__@ where

--   the two parameters @__x__@ and @__y__@ are switched

newtype Op2 h x y = Op2 (h y x)

instance Show2 h => Show2 (Op2 h) where
  show2 :: forall a b. Op2 h a b -> String
show2 (Op2 h b a
h) = String
"Op2[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ h b a -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h b a
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

instance Eq2 h => Eq2 (Op2 h) where
  eq2 :: forall x y. Op2 h x y -> Op2 h x y -> Bool
eq2 (Op2 h y x
f) (Op2 h y x
g) = h y x -> h y x -> Bool
forall x y. h x y -> h x y -> Bool
forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 h y x
f h y x
g 

--------------------------------------------------------------------------------

-- toOp2Struct -


-- | transforming a 'Struct' where __@p@__ serves only as a proxy for __@m@__ and will not

--   be evaluated.

toOp2Struct :: p m -> Struct (ObjectClass m) x -> Struct (ObjectClass (Op2 m)) x
toOp2Struct :: forall (p :: (* -> * -> *) -> *) (m :: * -> * -> *) x.
p m -> Struct (ObjectClass m) x -> Struct (ObjectClass (Op2 m)) x
toOp2Struct p m
_ = Struct (ObjectClass m) x -> Struct (ObjectClass m) x
Struct (ObjectClass m) x -> Struct (ObjectClass (Op2 m)) x
forall x. x -> x
id

--------------------------------------------------------------------------------

-- Op2 - Instance -


instance Morphism h => Morphism (Op2 h) where
  type ObjectClass (Op2 h) = ObjectClass h
  domain :: forall x y. Op2 h x y -> Struct (ObjectClass (Op2 h)) x
domain (Op2 h y x
h) = h y x -> Struct (ObjectClass h) x
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h y x
h
  range :: forall x y. Op2 h x y -> Struct (ObjectClass (Op2 h)) y
range (Op2 h y x
h) = h y x -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h y x
h
  
instance Category c => Category (Op2 c) where
  cOne :: forall x. Struct (ObjectClass (Op2 c)) x -> Op2 c x x
cOne Struct (ObjectClass (Op2 c)) x
s = c x x -> Op2 c x x
forall (h :: * -> * -> *) x y. h y x -> Op2 h x y
Op2 (Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne Struct (ObjectClass c) x
Struct (ObjectClass (Op2 c)) x
s)
  Op2 c z y
f . :: forall y z x. Op2 c y z -> Op2 c x y -> Op2 c x z
. Op2 c y x
g = c z x -> Op2 c x z
forall (h :: * -> * -> *) x y. h y x -> Op2 h x y
Op2 (c y x
g c y x -> c z y -> c z x
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c z y
f)

--------------------------------------------------------------------------------

-- FunctorG -


-- | attest of being 'FunctorialG'.

data FunctorG t a b where
  FunctorG :: FunctorialG t a b => FunctorG t a b
  
--------------------------------------------------------------------------------

-- Functorial1 -


-- | functorials form @__c__@ to @('->')@ according to @__f__@.

type Functorial1 c f = FunctorialG f c (->)

--------------------------------------------------------------------------------

-- Functor1 -


-- | attest of being 'Functorial1' for the 'Category' __c__ to the 'Category' @('->')@ according

-- to @__f__@.

data Functor1 c f where
  Functor1 :: Functorial1 c f => Functor1 c f

--------------------------------------------------------------------------------

-- TransformableObjectClass -


-- | helper class to avoid undecided instances.

class Transformable s (ObjectClass c) => TransformableObjectClass s c

instance Transformable s Type => TransformableObjectClass s (->)

--------------------------------------------------------------------------------

-- Sub -


-- | sub category of @__c__@ according to the 'ObjectClass' @__s__@, whereas maintaining the

-- applicative behavior of @__c__@.

data Sub s c x y where
  Sub :: (Structure s x, Structure s y) => c x y -> Sub s c x y 

instance Morphism (Sub s c) where
  type ObjectClass (Sub s c) = s
  homomorphous :: forall x y. Sub s c x y -> Homomorphous (ObjectClass (Sub s c)) x y
homomorphous (Sub c x y
_) = Struct s x
forall s x. Structure s x => Struct s x
Struct Struct s x -> Struct s y -> Homomorphous s x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct s y
forall s x. Structure s x => Struct s x
Struct

instance ApplicativeG f h (->) => ApplicativeG f (Sub t h) (->) where amapG :: forall x y. Sub t h x y -> f x -> f y
amapG (Sub h x y
h) = h x y -> f x -> f y
forall x y. h x y -> f x -> f y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h
instance (FunctorialG f c (->), TransformableObjectClass s c) => FunctorialG f (Sub s c) (->)

--------------------------------------------------------------------------------

-- cOneSub -


-- | restricting 'cOne'.

cOneSub :: (Category c, t ~ ObjectClass c) => Struct s x -> Struct t x -> Sub s c x x
cOneSub :: forall (c :: * -> * -> *) t s x.
(Category c, t ~ ObjectClass c) =>
Struct s x -> Struct t x -> Sub s c x x
cOneSub Struct s x
Struct = c x x -> Sub s c x x
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub (c x x -> Sub s c x x)
-> (Struct t x -> c x x) -> Struct t x -> Sub s c x x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct t x -> c x x
Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne

instance (Category c, TransformableObjectClass s c) => Category (Sub s c) where
  cOne :: forall x. Struct (ObjectClass (Sub s c)) x -> Sub s c x x
cOne Struct (ObjectClass (Sub s c)) x
s = Struct s x -> Struct (ObjectClass c) x -> Sub s c x x
forall (c :: * -> * -> *) t s x.
(Category c, t ~ ObjectClass c) =>
Struct s x -> Struct t x -> Sub s c x x
cOneSub Struct s x
Struct (ObjectClass (Sub s c)) x
s (Struct s x -> Struct (ObjectClass c) x
forall x. Struct s x -> Struct (ObjectClass c) x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
Struct (ObjectClass (Sub s c)) x
s)
  Sub c y z
f . :: forall y z x. Sub s c y z -> Sub s c x y -> Sub s c x z
. Sub c x y
g = c x z -> Sub s c x z
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub (c y z
f c y z -> c x y -> c x z
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
g)

--------------------------------------------------------------------------------

-- sub -


-- | restricting a morphism.

sub' :: Homomorphous s x y -> h x y -> Sub s h x y
sub' :: forall s x y (h :: * -> * -> *).
Homomorphous s x y -> h x y -> Sub s h x y
sub' (Struct s x
Struct:>:Struct s y
Struct) = h x y -> Sub s h x y
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub

-- | restricting a morphism.

sub :: (Morphism h, Transformable (ObjectClass h) s) => h x y -> Sub s h x y
sub :: forall (h :: * -> * -> *) s x y.
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Sub s h x y
sub h x y
h = Homomorphous s x y -> h x y -> Sub s h x y
forall s x y (h :: * -> * -> *).
Homomorphous s x y -> h x y -> Sub s h x y
sub' (Homomorphous (ObjectClass h) x y -> Homomorphous s x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h x y -> Homomorphous (ObjectClass h) x y
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h)) h x y
h

--------------------------------------------------------------------------------

-- subG -


subG' :: ApplicativeG d a b => Homomorphous t (d x) (d y) -> a x y -> Sub t b (d x) (d y)
subG' :: forall (d :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) t x y.
ApplicativeG d a b =>
Homomorphous t (d x) (d y) -> a x y -> Sub t b (d x) (d y)
subG' (Struct t (d x)
Struct:>:Struct t (d y)
Struct) a x y
h = b (d x) (d y) -> Sub t b (d x) (d y)
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub (a x y -> b (d x) (d y)
forall x y. a x y -> b (d x) (d y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG a x y
h)

-- | the induced embedding.

subG :: (ApplicativeG d a b, TransformableG d s t)
  => Sub s a x y -> Sub t b (d x) (d y)
subG :: forall (d :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) s t x y.
(ApplicativeG d a b, TransformableG d s t) =>
Sub s a x y -> Sub t b (d x) (d y)
subG a' :: Sub s a x y
a'@(Sub a x y
a) = Homomorphous t (d x) (d y) -> a x y -> Sub t b (d x) (d y)
forall (d :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) t x y.
ApplicativeG d a b =>
Homomorphous t (d x) (d y) -> a x y -> Sub t b (d x) (d y)
subG' (Homomorphous s x y -> Homomorphous t (d x) (d y)
forall (t :: * -> *) u v x y.
TransformableG t u v =>
Homomorphous u x y -> Homomorphous v (t x) (t y)
tauHomG (Sub s a x y -> Homomorphous (ObjectClass (Sub s a)) x y
forall x y. Sub s a x y -> Homomorphous (ObjectClass (Sub s a)) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous Sub s a x y
a')) a x y
a

instance (ApplicativeG d a b, TransformableG d s t)
  => ApplicativeG d (Sub s a) (Sub t b) where
  amapG :: forall x y. Sub s a x y -> Sub t b (d x) (d y)
amapG = Sub s a x y -> Sub t b (d x) (d y)
forall (d :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) s t x y.
(ApplicativeG d a b, TransformableG d s t) =>
Sub s a x y -> Sub t b (d x) (d y)
subG

instance ( FunctorialG d a b
         , TransformableObjectClass s a, TransformableObjectClass t b
         , TransformableG d s t
         )
  => FunctorialG d (Sub s a) (Sub t b)

--------------------------------------------------------------------------------

-- TransformableGObjectClass -


-- | helper class to avoid undecided instances.

class TransformableG t (ObjectClass a) (ObjectClass b) => TransformableGObjectClass t a b

instance TransformableGObjectClass t a (->)

--------------------------------------------------------------------------------

-- Cayleyan2 -


-- | category of isomorphisms.

--

--  __Property__ Let __@c@__ be a type instance of 'Cayleyan2', then holds:

--  For all types __@x@__, __@y@__ and @f@ in __@c@__ __@x@__ __@y@__ holds:

--

--  (1) @('invert2' f '.' f) == 'cOne' ('domain' f)@ and

--  @(f '.' 'invert2' f) == 'cOne' ('range' f)@ where @(==) = 'eq2'@.

class (Category c, Eq2 c) => Cayleyan2 c where
  invert2 :: c x y -> c y x

instance Cayleyan2 c => Cayleyan2 (Op2 c) where
  invert2 :: forall x y. Op2 c x y -> Op2 c y x
invert2 (Op2 c y x
f) = c x y -> Op2 c y x
forall (h :: * -> * -> *) x y. h y x -> Op2 h x y
Op2 (c y x -> c x y
forall x y. c x y -> c y x
forall (c :: * -> * -> *) x y. Cayleyan2 c => c x y -> c y x
invert2 c y x
f)
  
--------------------------------------------------------------------------------

-- Cayleyan2 - Instance -


instance Cayleyan2 (Homomorphous m) where
  invert2 :: forall x y. Homomorphous m x y -> Homomorphous m y x
invert2 (Struct m x
d :>: Struct m y
r) = Struct m y
r Struct m y -> Struct m x -> Homomorphous m y x
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct m x
d  

--------------------------------------------------------------------------------

-- Inv2 -


-- | predicate for invertible morphisms within a category @__c__@.

--

-- __Property__ Let @'Inv2' f f'@ be in @'Inv2' __c__ __x__ __y__@ for a @'Category' __c__@ with

-- @'Eq2' __c__@, then holds:

--

-- (1) @f' '.' f 'OAlg.Data.EqualExtensional..=.' 'cOne' ('domain' f)@.

--

-- (2) @f '.' f' 'OAlg.Data.EqualExtensional..=.' 'cOne' ('range' f)@.

data Inv2 c x y = Inv2 (c x y) (c y x) deriving (Int -> Inv2 c x y -> ShowS
[Inv2 c x y] -> ShowS
Inv2 c x y -> String
(Int -> Inv2 c x y -> ShowS)
-> (Inv2 c x y -> String)
-> ([Inv2 c x y] -> ShowS)
-> Show (Inv2 c x y)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (c :: * -> * -> *) x y.
(Show (c x y), Show (c y x)) =>
Int -> Inv2 c x y -> ShowS
forall (c :: * -> * -> *) x y.
(Show (c x y), Show (c y x)) =>
[Inv2 c x y] -> ShowS
forall (c :: * -> * -> *) x y.
(Show (c x y), Show (c y x)) =>
Inv2 c x y -> String
$cshowsPrec :: forall (c :: * -> * -> *) x y.
(Show (c x y), Show (c y x)) =>
Int -> Inv2 c x y -> ShowS
showsPrec :: Int -> Inv2 c x y -> ShowS
$cshow :: forall (c :: * -> * -> *) x y.
(Show (c x y), Show (c y x)) =>
Inv2 c x y -> String
show :: Inv2 c x y -> String
$cshowList :: forall (c :: * -> * -> *) x y.
(Show (c x y), Show (c y x)) =>
[Inv2 c x y] -> ShowS
showList :: [Inv2 c x y] -> ShowS
Show, Inv2 c x y -> Inv2 c x y -> Bool
(Inv2 c x y -> Inv2 c x y -> Bool)
-> (Inv2 c x y -> Inv2 c x y -> Bool) -> Eq (Inv2 c x y)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (c :: * -> * -> *) x y.
(Eq (c x y), Eq (c y x)) =>
Inv2 c x y -> Inv2 c x y -> Bool
$c== :: forall (c :: * -> * -> *) x y.
(Eq (c x y), Eq (c y x)) =>
Inv2 c x y -> Inv2 c x y -> Bool
== :: Inv2 c x y -> Inv2 c x y -> Bool
$c/= :: forall (c :: * -> * -> *) x y.
(Eq (c x y), Eq (c y x)) =>
Inv2 c x y -> Inv2 c x y -> Bool
/= :: Inv2 c x y -> Inv2 c x y -> Bool
Eq)

instance Eq2 c => Eq2 (Inv2 c) where
  eq2 :: forall x y. Inv2 c x y -> Inv2 c x y -> Bool
eq2 (Inv2 c x y
f c y x
g) (Inv2 c x y
f' c y x
g') = c x y -> c x y -> Bool
forall x y. c x y -> c x y -> Bool
forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 c x y
f c x y
f' Bool -> Bool -> Bool
&& c y x -> c y x -> Bool
forall x y. c x y -> c x y -> Bool
forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 c y x
g c y x
g'
  
instance Morphism c => Morphism (Inv2 c) where
  type ObjectClass (Inv2 c) = ObjectClass c
  homomorphous :: forall x y. Inv2 c x y -> Homomorphous (ObjectClass (Inv2 c)) x y
homomorphous (Inv2 c x y
f c y x
_) = c x y -> Homomorphous (ObjectClass c) x y
forall x y. c x y -> Homomorphous (ObjectClass c) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous c x y
f

instance Category c => Category (Inv2 c) where
  cOne :: forall x. Struct (ObjectClass (Inv2 c)) x -> Inv2 c x x
cOne Struct (ObjectClass (Inv2 c)) x
s = c x x -> c x x -> Inv2 c x x
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 c x x
o c x x
o where o :: c x x
o = Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne Struct (ObjectClass c) x
Struct (ObjectClass (Inv2 c)) x
s
  Inv2 c y z
f c z y
g . :: forall y z x. Inv2 c y z -> Inv2 c x y -> Inv2 c x z
. Inv2 c x y
f' c y x
g' = c x z -> c z x -> Inv2 c x z
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 (c y z
f c y z -> c x y -> c x z
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
f') (c y x
g' c y x -> c z y -> c z x
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c z y
g)

instance (Category c, Eq2 c) => Cayleyan2 (Inv2 c) where
  invert2 :: forall x y. Inv2 c x y -> Inv2 c y x
invert2 = Inv2 c x y -> Inv2 c y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2

--------------------------------------------------------------------------------

-- inv2 -


-- | the inverse.

inv2 :: Inv2 c x y -> Inv2 c y x
inv2 :: forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 (Inv2 c x y
f c y x
g) = c y x -> c x y -> Inv2 c y x
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 c y x
g c x y
f

--------------------------------------------------------------------------------

-- inv2Forget -


-- | forgetting the restriction to 'Sub'.

inv2Forget :: Inv2 (Sub s h) x y -> Inv2 h x y
inv2Forget :: forall s (h :: * -> * -> *) x y. Inv2 (Sub s h) x y -> Inv2 h x y
inv2Forget (Inv2 (Sub h x y
t) (Sub h y x
f)) = h x y -> h y x -> Inv2 h x y
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 h x y
t h y x
f

--------------------------------------------------------------------------------

-- Either2 - Morphism -


instance (Morphism f, Morphism g, ObjectClass f ~ ObjectClass g)
  => Morphism (Either2 f g) where
  
  type ObjectClass (Either2 f g) = ObjectClass f
  
  domain :: forall x y. Either2 f g x y -> Struct (ObjectClass (Either2 f g)) x
domain (Left2 f x y
f) = f x y -> Struct (ObjectClass f) x
forall x y. f x y -> Struct (ObjectClass f) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain f x y
f
  domain (Right2 g x y
g) = g x y -> Struct (ObjectClass g) x
forall x y. g x y -> Struct (ObjectClass g) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain g x y
g

  range :: forall x y. Either2 f g x y -> Struct (ObjectClass (Either2 f g)) y
range (Left2 f x y
f) = f x y -> Struct (ObjectClass f) y
forall x y. f x y -> Struct (ObjectClass f) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range f x y
f
  range (Right2 g x y
g) = g x y -> Struct (ObjectClass g) y
forall x y. g x y -> Struct (ObjectClass g) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range g x y
g

--------------------------------------------------------------------------------

-- TransformableObjectClassTyp -


-- | helper class to avoid undecided instances.

--

-- __Example__ By declaring an instance

-- @instance (..,'Transformable' ('ObjectClass' m) 'Typ',..) => C m@ for a @'Morphism' __m__@

-- and a class @__C__@ one will get the compiler error:

--

-- @

--    • Illegal use of type family ‘ObjectClass’

--        in the constraint ‘Transformable (ObjectClass m) Typ’

--      (Use UndecidableInstances to permit this)

-- @

-- To avoid this error use this instance declaration:

-- @instance (..,'TransformableObjectClassTyp' m),..) => C m@ which will solve the problem!

class Transformable (ObjectClass m) Typ => TransformableObjectClassTyp m

--------------------------------------------------------------------------------

-- TransformableGObjectClassDomain -


-- | helper class to avoid undecided instances.

class TransformableG d (ObjectClass a) t => TransformableGObjectClassDomain d a t


--------------------------------------------------------------------------------

-- TransformableGObjectClassRange -


-- | helper class to avoid undecided instances.

class TransformableG d s (ObjectClass c) => TransformableGObjectClassRange d s c

instance TransformableGObjectClassRange d s (->)