{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Hom.Oriented.Definition

-- Description : definition of homomorphisms between oriented structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- definition of homomorphisms between 'Oriented' structures.

module OAlg.Hom.Oriented.Definition
  (
    -- * Homomorphism

    HomOriented(..), omap, IsoOrt, IsoOriented

    -- * Functorial

  , FunctorialHomOriented

    -- * IdHom

  , IdHom(..)

    -- * OpHom

  , OpHom(..)
  -- , OpHom(..), toOpHomOrt


    -- * HomOp

  , HomOp(..)

    -- * IsoOp

  , IsoOp(), PathHomOp, opPathOrt, isoFromOpOpOrt

    -- * IsoOpMap

  , IsoOpMap(), PathOpMap
  , OpMap(..)
  , toOp1Struct, fromOp1Struct

    -- ** Path

  , isoCoPath
  )
  where

import Control.Monad 

import Data.Typeable
import Data.List((++))

import OAlg.Prelude

import OAlg.Data.Constructable
import OAlg.Data.Reducible

import OAlg.Category.Path as C

import OAlg.Structure.Oriented as O
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.Additive
import OAlg.Structure.Distributive

import OAlg.Hom.Definition

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

-- HomOriented -


-- | type family of homomorphisms between 'Oriented' structures.

--

-- __Property__ Let @__h__@ be an instance of 'HomOriented', then

-- for all  @__a__@, @__b__@ and @f@ in @__h__@ @__a__@ @__b__@ and

-- @x@ in @__a__@ holds:  @'start' ('amap' f x) '==' 'pmap' f ('start' x)@ and

-- @'end' ('amap' f x) '==' 'pmap' f ('end' x)@.

--

-- We call such a @__h__@  a __/family of homomorphisms between oriented structures/__

-- and an entity @f@ in @__h__@ @__a__@ @__b__@ a

-- __/covariant oriented homomorphism/__ - or __/oriented homomorphism/__ for short -

-- __/between/__ @__a__@ __/and/__ @__b__@. A covariant oriented homomorphism @f@ in

-- @__h__ ('Op' __a__) __b__@ or @__h__ __a__ ('Op' __b__)@ will be called a

-- __/contravariant oriented homomorphism between/__ @__a__@ __/and/__ @__b__@.

--

-- __Note__

--

-- (1) As @__h__@ is an instance of @'EmbeddableMorphism' __h__ 'Ort'@ it follows

-- that for all @__a__@, @__b__@ and @f@ in @__h a b__@ holds:

-- @'tauHom' ('homomorphous' f) :: 'Homomorphous' 'Ort' __a__ __b__@ and thus @__a__@ and @__b__@ are

-- 'Oriented' structures! How to work with this concretely see the implementation of

-- 'OAlg.Proposition.Homomorphism.Multiplicative.prpHomOrt' where the property above

-- is stated.

--

-- (2) The constraint 'EmbeddableMorphismTyp' for a family @__h__@ of homomorphisms

-- between 'Oriented' structures ensures that the type @'OAlg.Category.Path.Path' __h__@

-- is a instances of 'OAlg.Data.Equal.Eq2'. 

class ( EmbeddableMorphism h Ort, Applicative h, Entity2 h
      , EmbeddableMorphismTyp h
      , Transformable1 Op (ObjectClass h)
      ) => HomOriented h where
  pmap :: h a b -> Point a -> Point b

instance HomOriented h => HomOriented (C.Path h) where
  pmap :: forall a b. Path h a b -> Point a -> Point b
pmap (IdPath Struct (ObjectClass h) a
_) Point a
p = Point a
p
  pmap (h y b
f :. Path h a y
pth) Point a
p = forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h y b
f forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap Path h a y
pth Point a
p

instance (HomOriented h, Transformable1 Op t, ForgetfulOrt t, ForgetfulTyp t, Typeable t)
  => HomOriented (Forget t h) where
  pmap :: forall a b. Forget t h a b -> Point a -> Point b
pmap (Forget h a b
h)      = forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a b
h

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

-- omap -


-- | the induced mapping of 'Orientation'.

omap :: HomOriented h => h a b -> Orientation (Point a) -> Orientation (Point b)
omap :: forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Orientation (Point a) -> Orientation (Point b)
omap h a b
h = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a b
h)

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

-- FunctorialHomOriented -


-- | functorial application on 'Oriented' structures.

--

-- __Properties__ Let @__h__@ be an instance of the class 'FunctorialHomOriented',

-- then holds:

--

-- (1) #FncHom1#For all types @__a__@ and

-- @s@ in @'Struct' ('ObjectClass' __h__) __a__@ holds: @'pmap' ('cOne' s) = 'id'@.

--

-- (2) #FncHom1#For all types @__a__@, @__b__@, @__c__@ and

-- @f@ in @__h__@ @__b__@ @__c__@, @g@ in @__h__@ @__a__@ @__b__@ holds:

-- @'pmap' (f '.' g) = 'pmap' f '.' 'pmap' g@.

class (Category h, Functorial h, HomOriented h) => FunctorialHomOriented h

instance FunctorialHomOriented h => FunctorialHomOriented (C.Path h)

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

-- Hom -


type instance Hom Ort h = HomOriented h

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

-- IsoOrt -


-- | @s@-isomoprhisms.

type IsoOrt s h = (FunctorialHomOriented h, Cayleyan2 h, Hom s h)

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

-- IsoOriented -


-- | isomorphisms between 'Oriented' structures.

type IsoOriented h = (FunctorialHomOriented h, Cayleyan2 h)

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

-- IdHom -


-- | identity morphism.

data IdHom s a b where
  IdHom :: Structure s a => IdHom s a a

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

-- IdHom - Morphism -


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

instance Transformable s t => EmbeddableMorphism (IdHom s) t

instance ForgetfulTyp s => EmbeddableMorphismTyp (IdHom s)

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

-- IdHom - Entity -


deriving instance Show (IdHom s a b)
instance Show2 (IdHom s)

deriving instance Eq (IdHom s a b)
instance Eq2 (IdHom s)

instance Validable (IdHom s a b) where
  valid :: IdHom s a b -> Statement
valid IdHom s a b
IdHom = Statement
SValid
instance Validable2 (IdHom s)

instance (Typeable s, Typeable a, Typeable b) => Entity (IdHom s a b)
instance Typeable s => Entity2 (IdHom s)

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

-- IdHom - Category -


instance Category (IdHom s) where
  cOne :: forall x. Struct (ObjectClass (IdHom s)) x -> IdHom s x x
cOne Struct (ObjectClass (IdHom s)) x
Struct = forall s a. Structure s a => IdHom s a a
IdHom
  IdHom s y z
IdHom . :: forall y z x. IdHom s y z -> IdHom s x y -> IdHom s x z
. IdHom s x y
IdHom = forall s a. Structure s a => IdHom s a a
IdHom

instance Cayleyan2 (IdHom s) where
  invert2 :: forall x y. IdHom s x y -> IdHom s y x
invert2 IdHom s x y
IdHom = forall s a. Structure s a => IdHom s a a
IdHom

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

-- IdHom - HomOriented -


instance Applicative (IdHom s) where
  amap :: forall a b. IdHom s a b -> a -> b
amap IdHom s a b
IdHom = forall x. x -> x
id

instance Functorial (IdHom s)

instance (TransformableOp s,ForgetfulOrt s, ForgetfulTyp s, Typeable s)
  => HomOriented (IdHom s) where
  pmap :: forall a b. IdHom s a b -> Point a -> Point b
pmap IdHom s a b
IdHom = forall x. x -> x
id

instance (TransformableOp s, ForgetfulOrt s, ForgetfulTyp s, Typeable s)
  => FunctorialHomOriented (IdHom s)
--------------------------------------------------------------------------------

-- HomOp -


-- | some basic contravariant isomorphisms between @__s__@-structures with there 'invert2'.

data HomOp s a b where  
  FromOpOp  :: ( Structure s (Op (Op a))
               , Structure s a
               ) => HomOp s (Op (Op a)) a
  ToOpOp :: ( Structure s (Op (Op a))
            , Structure s a
            ) => HomOp s a (Op (Op a))
  OpPath    :: ( Structure s a
               , Structure s (Op (O.Path a))
               , Structure s (O.Path (Op a))
               ) => HomOp s (Op (O.Path a)) (O.Path (Op a))
  OpPathInv :: ( Structure s a
               , Structure s (Op (O.Path a))
               , Structure s (O.Path (Op a))
               ) => HomOp s (O.Path (Op a)) (Op (O.Path a)) 
  Opposite    :: ( Structure s (Op (Orientation p))
               , Structure s (Orientation p)
               ) => HomOp s (Op (Orientation p)) (Orientation p)
  OppositeInv :: ( Structure s (Op (Orientation p))
               , Structure s (Orientation p)
               ) => HomOp s (Orientation p) (Op (Orientation p))

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

-- invHomOp -


-- | the inverse morphism.

invHomOp :: HomOp s a b -> HomOp s b a
invHomOp :: forall s a b. HomOp s a b -> HomOp s b a
invHomOp HomOp s a b
h = case HomOp s a b
h of
  HomOp s a b
FromOpOp    -> forall s a.
(Structure s (Op (Op a)), Structure s a) =>
HomOp s a (Op (Op a))
ToOpOp
  HomOp s a b
ToOpOp      -> forall s a.
(Structure s (Op (Op a)), Structure s a) =>
HomOp s (Op (Op a)) a
FromOpOp

  HomOp s a b
OpPath      -> forall s x.
(Structure s x, Structure s (Op (Path x)),
 Structure s (Path (Op x))) =>
HomOp s (Path (Op x)) (Op (Path x))
OpPathInv
  HomOp s a b
OpPathInv   -> forall s x.
(Structure s x, Structure s (Op (Path x)),
 Structure s (Path (Op x))) =>
HomOp s (Op (Path x)) (Path (Op x))
OpPath

  HomOp s a b
Opposite    -> forall s x.
(Structure s (Op (Orientation x)), Structure s (Orientation x)) =>
HomOp s (Orientation x) (Op (Orientation x))
OppositeInv
  HomOp s a b
OppositeInv -> forall s x.
(Structure s (Op (Orientation x)), Structure s (Orientation x)) =>
HomOp s (Op (Orientation x)) (Orientation x)
Opposite
  
--------------------------------------------------------------------------------

-- HomOp - Morphism -


instance Morphism (HomOp s) where
  type ObjectClass (HomOp s) = s

  homomorphous :: forall x y. HomOp s x y -> Homomorphous (ObjectClass (HomOp s)) x y
homomorphous HomOp s x y
FromOpOp    = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous HomOp s x y
ToOpOp = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct

  homomorphous HomOp s x y
OpPath    = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous HomOp s x y
OpPathInv = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  
  homomorphous HomOp s x y
Opposite    = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous HomOp s x y
OppositeInv = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  
instance Transformable s t => EmbeddableMorphism (HomOp s) t
instance ForgetfulTyp s => EmbeddableMorphismTyp (HomOp s)

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

-- HomOp - Entity -


deriving instance Show (HomOp s a b)
instance Show2 (HomOp s)

deriving instance Eq (HomOp s a b)
instance Eq2 (HomOp s)

instance Validable (HomOp s a b) where
  valid :: HomOp s a b -> Statement
valid HomOp s a b
FromOpOp  = Statement
SValid
  valid HomOp s a b
_         = Statement
SValid
instance Validable2 (HomOp s)

instance (Typeable s, Typeable a, Typeable b) => Entity (HomOp s a b)
instance Typeable s => Entity2 (HomOp s)

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

-- HomOp - Hom -


instance ForgetfulOrt s => Applicative (HomOp s) where
  amap :: forall a b. HomOp s a b -> a -> b
amap HomOp s a b
FromOpOp (Op (Op b
x)) = b
x
  amap HomOp s a b
ToOpOp a
x             = forall x. x -> Op x
Op (forall x. x -> Op x
Op a
x)

  amap h :: HomOp s a b
h@HomOp s a b
OpPath (Op Path a
pth) = forall a (h :: * -> * -> *) b.
Struct Ort a -> h (Op (Path a)) b -> Path a -> Path (Op a)
toDualOrt (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall s a. HomOp s (Op (Path a)) (Path (Op a)) -> Struct s a
aStruct HomOp s a b
h)) HomOp s a b
h Path a
pth where
    aStruct :: HomOp s (Op (O.Path a)) (O.Path (Op a)) -> Struct s a
    aStruct :: forall s a. HomOp s (Op (Path a)) (Path (Op a)) -> Struct s a
aStruct HomOp s (Op (Path a)) (Path (Op a))
OpPath = forall s x. Structure s x => Struct s x
Struct
    
    toDualOrt :: Struct Ort a
      -> h (Op (O.Path a)) b -> O.Path a -> O.Path (Op a)
    toDualOrt :: forall a (h :: * -> * -> *) b.
Struct Ort a -> h (Op (Path a)) b -> Path a -> Path (Op a)
toDualOrt Struct Ort a
Struct h (Op (Path a)) b
_ = forall x. Dualisable x => x -> Dual x
toDual

  amap h :: HomOp s a b
h@HomOp s a b
OpPathInv a
pth' = forall a (h :: * -> * -> *) b.
Struct Ort a -> h (Path (Op a)) b -> Path (Op a) -> Op (Path a)
fromDualOrt (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall s a. HomOp s (Path (Op a)) (Op (Path a)) -> Struct s a
aStruct HomOp s a b
h)) HomOp s a b
h a
pth' where
    aStruct :: HomOp s (O.Path (Op a)) (Op (O.Path a)) -> Struct s a
    aStruct :: forall s a. HomOp s (Path (Op a)) (Op (Path a)) -> Struct s a
aStruct HomOp s (Path (Op a)) (Op (Path a))
OpPathInv = forall s x. Structure s x => Struct s x
Struct

    fromDualOrt :: Struct Ort a
      -> h (O.Path (Op a)) b -> O.Path (Op a) -> Op (O.Path a)
    fromDualOrt :: forall a (h :: * -> * -> *) b.
Struct Ort a -> h (Path (Op a)) b -> Path (Op a) -> Op (Path a)
fromDualOrt Struct Ort a
Struct h (Path (Op a)) b
_ = forall x. x -> Op x
Op forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. Dualisable x => Dual x -> x
fromDual

  amap HomOp s a b
Opposite (Op Orientation p
o) = forall p. Orientation p -> Orientation p
opposite Orientation p
o
  amap HomOp s a b
OppositeInv a
o = forall x. x -> Op x
Op (forall p. Orientation p -> Orientation p
opposite a
o)

instance (TransformableOp s, ForgetfulOrt s, ForgetfulTyp s, Typeable s)
  => HomOriented (HomOp s) where
  pmap :: forall a b. HomOp s a b -> Point a -> Point b
pmap HomOp s a b
FromOpOp    = forall x. x -> x
id
  pmap HomOp s a b
ToOpOp = forall x. x -> x
id

  pmap HomOp s a b
OpPath    = forall x. x -> x
id
  pmap HomOp s a b
OpPathInv = forall x. x -> x
id

  pmap HomOp s a b
Opposite    = forall x. x -> x
id
  pmap HomOp s a b
OppositeInv = forall x. x -> x
id
  
--------------------------------------------------------------------------------

-- PathHomOp -


-- | paths of 'HomOp'.

type PathHomOp s a b = C.Path (HomOp s) a b

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

-- IsoOp -


-- | isomorphisms induced by paths of 'HomOp'.

newtype IsoOp s a b = IsoOp (PathHomOp s a b)
  deriving (Int -> IsoOp s a b -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s a b. Int -> IsoOp s a b -> ShowS
forall s a b. [IsoOp s a b] -> ShowS
forall s a b. IsoOp s a b -> String
showList :: [IsoOp s a b] -> ShowS
$cshowList :: forall s a b. [IsoOp s a b] -> ShowS
show :: IsoOp s a b -> String
$cshow :: forall s a b. IsoOp s a b -> String
showsPrec :: Int -> IsoOp s a b -> ShowS
$cshowsPrec :: forall s a b. Int -> IsoOp s a b -> ShowS
Show,forall a b. IsoOp s a b -> String
forall s a b. IsoOp s a b -> String
forall (h :: * -> * -> *). (forall a b. h a b -> String) -> Show2 h
show2 :: forall a b. IsoOp s a b -> String
$cshow2 :: forall s a b. IsoOp s a b -> String
Show2,IsoOp s a b -> Statement
forall a. (a -> Statement) -> Validable a
forall s a b. IsoOp s a b -> Statement
valid :: IsoOp s a b -> Statement
$cvalid :: forall s a b. IsoOp s a b -> Statement
Validable,forall x y. IsoOp s x y -> Statement
forall s a b. IsoOp s a b -> Statement
forall (h :: * -> * -> *).
(forall x y. h x y -> Statement) -> Validable2 h
valid2 :: forall x y. IsoOp s x y -> Statement
$cvalid2 :: forall s a b. IsoOp s a b -> Statement
Validable2,IsoOp s a b -> IsoOp s a b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s a b. ForgetfulTyp s => IsoOp s a b -> IsoOp s a b -> Bool
/= :: IsoOp s a b -> IsoOp s a b -> Bool
$c/= :: forall s a b. ForgetfulTyp s => IsoOp s a b -> IsoOp s a b -> Bool
== :: IsoOp s a b -> IsoOp s a b -> Bool
$c== :: forall s a b. ForgetfulTyp s => IsoOp s a b -> IsoOp s a b -> Bool
Eq,forall s x y. ForgetfulTyp s => IsoOp s x y -> IsoOp s x y -> Bool
forall x y. IsoOp s x y -> IsoOp s x y -> Bool
forall (h :: * -> * -> *).
(forall x y. h x y -> h x y -> Bool) -> Eq2 h
eq2 :: forall x y. IsoOp s x y -> IsoOp s x y -> Bool
$ceq2 :: forall s x y. ForgetfulTyp s => IsoOp s x y -> IsoOp s x y -> Bool
Eq2,forall a. Show a -> Eq a -> Validable a -> Typeable a -> Entity a
forall {s} {a} {b}.
(ForgetfulTyp s, Typeable s, Typeable a, Typeable b) =>
Eq (IsoOp s a b)
forall {s} {a} {b}.
(ForgetfulTyp s, Typeable s, Typeable a, Typeable b) =>
Show (IsoOp s a b)
forall {s} {a} {b}.
(ForgetfulTyp s, Typeable s, Typeable a, Typeable b) =>
Typeable (IsoOp s a b)
forall {s} {a} {b}.
(ForgetfulTyp s, Typeable s, Typeable a, Typeable b) =>
Validable (IsoOp s a b)
Entity,forall {s}. (ForgetfulTyp s, Typeable s) => Typeable (IsoOp s)
forall {s}. (ForgetfulTyp s, Typeable s) => Eq2 (IsoOp s)
forall {s}. (ForgetfulTyp s, Typeable s) => Show2 (IsoOp s)
forall {s}. (ForgetfulTyp s, Typeable s) => Validable2 (IsoOp s)
forall (h :: * -> * -> *).
Show2 h -> Eq2 h -> Validable2 h -> Typeable h -> Entity2 h
Entity2)

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

-- IsoOp - Constructable -


-- | reducing paths of 'HomOp'.

rdcPathHomOp :: PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp :: forall s a b. PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp PathHomOp s a b
pth = case PathHomOp s a b
pth of
  HomOp s y b
FromOpOp :. HomOp s y y
ToOpOp :. Path (HomOp s) a y
p -> forall x. x -> Rdc x
reducesTo Path (HomOp s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall s a b. PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp
  HomOp s y b
ToOpOp :. HomOp s y y
FromOpOp :. Path (HomOp s) a y
p -> forall x. x -> Rdc x
reducesTo Path (HomOp s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall s a b. PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp

  HomOp s y b
OpPath :. HomOp s y y
OpPathInv :. Path (HomOp s) a y
p -> forall x. x -> Rdc x
reducesTo Path (HomOp s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall s a b. PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp
  HomOp s y b
OpPathInv :. HomOp s y y
OpPath :. Path (HomOp s) a y
p -> forall x. x -> Rdc x
reducesTo Path (HomOp s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall s a b. PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp
  
  HomOp s y b
Opposite :. HomOp s y y
OppositeInv :. Path (HomOp s) a y
p -> forall x. x -> Rdc x
reducesTo Path (HomOp s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall s a b. PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp
  HomOp s y b
OppositeInv :. HomOp s y y
Opposite :. Path (HomOp s) a y
p -> forall x. x -> Rdc x
reducesTo Path (HomOp s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall s a b. PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp
  
  HomOp s y b
h :. Path (HomOp s) a y
p              -> forall s a b. PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp Path (HomOp s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (HomOp s y b
hforall (m :: * -> * -> *) x z x. m x z -> Path m x x -> Path m x z
:.))
  PathHomOp s a b
p                   -> forall (m :: * -> *) a. Monad m => a -> m a
return PathHomOp s a b
p

instance Reducible (PathHomOp s a b) where
  reduce :: PathHomOp s a b -> PathHomOp s a b
reduce = forall x. (x -> Rdc x) -> x -> x
reduceWith forall s a b. PathHomOp s a b -> Rdc (PathHomOp s a b)
rdcPathHomOp

instance Exposable (IsoOp s a b) where
  type Form (IsoOp s a b) = PathHomOp s a b
  form :: IsoOp s a b -> Form (IsoOp s a b)
form (IsoOp PathHomOp s a b
p) = PathHomOp s a b
p
  
instance Constructable (IsoOp s a b) where
  make :: Form (IsoOp s a b) -> IsoOp s a b
make Form (IsoOp s a b)
p = forall s a b. PathHomOp s a b -> IsoOp s a b
IsoOp (forall e. Reducible e => e -> e
reduce Form (IsoOp s a b)
p)

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

-- IsoOp - Cayleyan2 -


instance Morphism (IsoOp s) where
  type ObjectClass (IsoOp s) = s
  homomorphous :: forall x y. IsoOp s x y -> Homomorphous (ObjectClass (IsoOp s)) x y
homomorphous = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous 

instance Transformable s t => EmbeddableMorphism (IsoOp s) t
instance ForgetfulTyp s => EmbeddableMorphismTyp (IsoOp s)

instance Category (IsoOp s) where
  cOne :: forall x. Struct (ObjectClass (IsoOp s)) x -> IsoOp s x x
cOne Struct (ObjectClass (IsoOp s)) x
o  = forall s a b. PathHomOp s a b -> IsoOp s a b
IsoOp (forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct (ObjectClass (IsoOp s)) x
o)
  IsoOp PathHomOp s y z
f . :: forall y z x. IsoOp s y z -> IsoOp s x y -> IsoOp s x z
. IsoOp PathHomOp s x y
g = forall x. Constructable x => Form x -> x
make (PathHomOp s y z
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. PathHomOp s x y
g)

instance ForgetfulTyp s => Cayleyan2 (IsoOp s) where
  invert2 :: forall x y. IsoOp s x y -> IsoOp s y x
invert2 (IsoOp PathHomOp s x y
p) = forall s a b. PathHomOp s a b -> IsoOp s a b
IsoOp (forall (m :: * -> * -> *) (f :: * -> * -> *) x y.
(Morphism m, Morphism f) =>
(forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u)
-> (forall u v. m u v -> f v u) -> Path m x y -> Path f y x
reverse forall x. x -> x
id forall s a b. HomOp s a b -> HomOp s b a
invHomOp PathHomOp s x y
p)

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

-- IsoOp - Hom -


instance ForgetfulOrt s => Applicative (IsoOp s) where
  amap :: forall a b. IsoOp s a b -> a -> b
amap = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap

instance (TransformableOp s, ForgetfulOrt s, ForgetfulTyp s, Typeable s)
  => HomOriented (IsoOp s) where
  pmap :: forall a b. IsoOp s a b -> Point a -> Point b
pmap = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap

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

-- IsoOp - Functorial -


instance ForgetfulOrt s => Functorial (IsoOp s)
instance (TransformableOp s, ForgetfulOrt s, ForgetfulTyp s, Typeable s)
  => FunctorialHomOriented (IsoOp s)

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

-- opPathOrt -


-- | the induced isomorphism given by 'OpPath'.

opPathOrt :: Oriented a => IsoOp Ort (Op (O.Path a)) (O.Path (Op a)) 
opPathOrt :: forall a. Oriented a => IsoOp Ort (Op (Path a)) (Path (Op a))
opPathOrt = forall x. Constructable x => Form x -> x
make (forall s x.
(Structure s x, Structure s (Op (Path x)),
 Structure s (Path (Op x))) =>
HomOp s (Op (Path x)) (Path (Op x))
OpPath forall (m :: * -> * -> *) x z x. m x z -> Path m x x -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath forall s x. Structure s x => Struct s x
Struct) 

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

-- isoFromOpOpOrt -


-- | the induced isomorphism of 'Oriented' structures given by 'FromOpOp'.

--

-- __Examples__

--

-- @

-- let tOS = invert2 (isoFromOpOpOrt :: IsoOp Ort (Op (Op OS)) OS)

-- let f = isoFromOpOpOrt :: Oriented a =>IsoOp Ort (Op (Op a)) a

-- let t = invert2 f

-- @

--

-- >>> tOS

-- IsoOp Path[ToOpOp]

--

-- >>> t . t . tOS

-- IsoOp Path[ToOpOp,ToOpOp,ToOpOp]

--

-- >>> f . f . t . f . t . tOS

-- IsoOp Path[]

--

-- >>> f . f . t . f . t . tOS == cOne Struct

-- True

isoFromOpOpOrt :: Oriented a => IsoOp Ort (Op (Op a)) a
isoFromOpOpOrt :: forall a. Oriented a => IsoOp Ort (Op (Op a)) a
isoFromOpOpOrt = forall x. Constructable x => Form x -> x
make (forall s a.
(Structure s (Op (Op a)), Structure s a) =>
HomOp s (Op (Op a)) a
FromOpOp forall (m :: * -> * -> *) x z x. m x z -> Path m x x -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath forall s x. Structure s x => Struct s x
Struct)

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

-- OpMap -


-- | contravariant @__s__@-isomorphisms between @__f__ __x__@ and @__f__ ('Op' __x__)@.

data OpMap f s a b where
  
  -- | contravariant @__s__@-isomorphism from __@f x@__ to @__f__ ('Op' __x__)@.

  ToOp1 :: (Structure s (Op (f x)), Structure s (f (Op x)), Structure s x)
    => OpMap f s (Op (f x)) (f (Op x))
    
  -- | the inverse of 'ToOp1'.

  FromOp1 :: (Structure s (Op (f x)), Structure s (f (Op x)), Structure s x)
    => OpMap f s (f (Op x)) (Op (f x))

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

-- toOp1Struct -


-- | structural attest for 'ToOp1'.

toOp1Struct :: OpMap f s (Op (f x)) (f (Op x)) -> Struct s x
toOp1Struct :: forall (f :: * -> *) s x.
OpMap f s (Op (f x)) (f (Op x)) -> Struct s x
toOp1Struct OpMap f s (Op (f x)) (f (Op x))
ToOp1 = forall s x. Structure s x => Struct s x
Struct
toOp1Struct OpMap f s (Op (f x)) (f (Op x))
f     = forall a e. Exception e => e -> a
throw forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ String -> AlgebraicException
InvalidData forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Show a => a -> String
show OpMap f s (Op (f x)) (f (Op x))
f

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

-- fromOp1Struct -


-- | structural attest for 'FromOp1'.

fromOp1Struct :: OpMap f s (f (Op x)) (Op (f x)) -> Struct s x
fromOp1Struct :: forall (f :: * -> *) s x.
OpMap f s (f (Op x)) (Op (f x)) -> Struct s x
fromOp1Struct OpMap f s (f (Op x)) (Op (f x))
FromOp1 = forall s x. Structure s x => Struct s x
Struct
fromOp1Struct OpMap f s (f (Op x)) (Op (f x))
f       = forall a e. Exception e => e -> a
throw forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ String -> AlgebraicException
InvalidData forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Show a => a -> String
show OpMap f s (f (Op x)) (Op (f x))
f

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

-- invOpMap -


-- | the inverse morphism.

invOpMap :: OpMap f s a b -> OpMap f s b a
invOpMap :: forall (f :: * -> *) s a b. OpMap f s a b -> OpMap f s b a
invOpMap OpMap f s a b
h = case OpMap f s a b
h of
  OpMap f s a b
ToOp1   -> forall s (f :: * -> *) x.
(Structure s (Op (f x)), Structure s (f (Op x)), Structure s x) =>
OpMap f s (f (Op x)) (Op (f x))
FromOp1
  OpMap f s a b
FromOp1 -> forall s (f :: * -> *) x.
(Structure s (Op (f x)), Structure s (f (Op x)), Structure s x) =>
OpMap f s (Op (f x)) (f (Op x))
ToOp1

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

-- OpMap - Morphism -


instance Morphism (OpMap f s) where
  type ObjectClass (OpMap f s) = s
  homomorphous :: forall x y.
OpMap f s x y -> Homomorphous (ObjectClass (OpMap f s)) x y
homomorphous OpMap f s x y
ToOp1   = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous OpMap f s x y
FromOp1 = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct

instance Transformable s t => EmbeddableMorphism (OpMap f s) t
instance ForgetfulTyp s => EmbeddableMorphismTyp (OpMap f s)

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

-- OpMap - Entity -


deriving instance Show (OpMap f s a b)
instance Show2 (OpMap f s)

deriving instance Eq (OpMap f s a b)
instance Eq2 (OpMap f s)

instance Validable (OpMap f s a b) where
  valid :: OpMap f s a b -> Statement
valid OpMap f s a b
ToOp1 = Statement
SValid
  valid OpMap f s a b
_     = Statement
SValid
instance Validable2 (OpMap f s)

instance (Typeable f, Typeable s, Typeable a, Typeable b) => Entity (OpMap f s a b)
instance (Typeable f, Typeable s) => Entity2 (OpMap f s)

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

-- PathOpMap -


-- | paths of 'OpMap'.

type PathOpMap f s = C.Path (OpMap f s)

-- | isomorphisms induced by paths of 'OpMap'.

newtype IsoOpMap f s a b = IsoOpMap (PathOpMap f s a b)
  deriving (Int -> IsoOpMap f s a b -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (f :: * -> *) s a b. Int -> IsoOpMap f s a b -> ShowS
forall (f :: * -> *) s a b. [IsoOpMap f s a b] -> ShowS
forall (f :: * -> *) s a b. IsoOpMap f s a b -> String
showList :: [IsoOpMap f s a b] -> ShowS
$cshowList :: forall (f :: * -> *) s a b. [IsoOpMap f s a b] -> ShowS
show :: IsoOpMap f s a b -> String
$cshow :: forall (f :: * -> *) s a b. IsoOpMap f s a b -> String
showsPrec :: Int -> IsoOpMap f s a b -> ShowS
$cshowsPrec :: forall (f :: * -> *) s a b. Int -> IsoOpMap f s a b -> ShowS
Show,forall a b. IsoOpMap f s a b -> String
forall (f :: * -> *) s a b. IsoOpMap f s a b -> String
forall (h :: * -> * -> *). (forall a b. h a b -> String) -> Show2 h
show2 :: forall a b. IsoOpMap f s a b -> String
$cshow2 :: forall (f :: * -> *) s a b. IsoOpMap f s a b -> String
Show2,IsoOpMap f s a b -> Statement
forall a. (a -> Statement) -> Validable a
forall (f :: * -> *) s a b. IsoOpMap f s a b -> Statement
valid :: IsoOpMap f s a b -> Statement
$cvalid :: forall (f :: * -> *) s a b. IsoOpMap f s a b -> Statement
Validable,forall x y. IsoOpMap f s x y -> Statement
forall (f :: * -> *) s a b. IsoOpMap f s a b -> Statement
forall (h :: * -> * -> *).
(forall x y. h x y -> Statement) -> Validable2 h
valid2 :: forall x y. IsoOpMap f s x y -> Statement
$cvalid2 :: forall (f :: * -> *) s a b. IsoOpMap f s a b -> Statement
Validable2,IsoOpMap f s a b -> IsoOpMap f s a b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (f :: * -> *) s a b.
ForgetfulTyp s =>
IsoOpMap f s a b -> IsoOpMap f s a b -> Bool
/= :: IsoOpMap f s a b -> IsoOpMap f s a b -> Bool
$c/= :: forall (f :: * -> *) s a b.
ForgetfulTyp s =>
IsoOpMap f s a b -> IsoOpMap f s a b -> Bool
== :: IsoOpMap f s a b -> IsoOpMap f s a b -> Bool
$c== :: forall (f :: * -> *) s a b.
ForgetfulTyp s =>
IsoOpMap f s a b -> IsoOpMap f s a b -> Bool
Eq,forall x y. IsoOpMap f s x y -> IsoOpMap f s x y -> Bool
forall (f :: * -> *) s x y.
ForgetfulTyp s =>
IsoOpMap f s x y -> IsoOpMap f s x y -> Bool
forall (h :: * -> * -> *).
(forall x y. h x y -> h x y -> Bool) -> Eq2 h
eq2 :: forall x y. IsoOpMap f s x y -> IsoOpMap f s x y -> Bool
$ceq2 :: forall (f :: * -> *) s x y.
ForgetfulTyp s =>
IsoOpMap f s x y -> IsoOpMap f s x y -> Bool
Eq2,forall a. Show a -> Eq a -> Validable a -> Typeable a -> Entity a
forall {f :: * -> *} {s} {a} {b}.
(ForgetfulTyp s, Typeable f, Typeable s, Typeable a, Typeable b) =>
Eq (IsoOpMap f s a b)
forall {f :: * -> *} {s} {a} {b}.
(ForgetfulTyp s, Typeable f, Typeable s, Typeable a, Typeable b) =>
Show (IsoOpMap f s a b)
forall {f :: * -> *} {s} {a} {b}.
(ForgetfulTyp s, Typeable f, Typeable s, Typeable a, Typeable b) =>
Typeable (IsoOpMap f s a b)
forall {f :: * -> *} {s} {a} {b}.
(ForgetfulTyp s, Typeable f, Typeable s, Typeable a, Typeable b) =>
Validable (IsoOpMap f s a b)
Entity,forall {f :: * -> *} {s}.
(ForgetfulTyp s, Typeable f, Typeable s) =>
Typeable (IsoOpMap f s)
forall {f :: * -> *} {s}.
(ForgetfulTyp s, Typeable f, Typeable s) =>
Eq2 (IsoOpMap f s)
forall {f :: * -> *} {s}.
(ForgetfulTyp s, Typeable f, Typeable s) =>
Show2 (IsoOpMap f s)
forall {f :: * -> *} {s}.
(ForgetfulTyp s, Typeable f, Typeable s) =>
Validable2 (IsoOpMap f s)
forall (h :: * -> * -> *).
Show2 h -> Eq2 h -> Validable2 h -> Typeable h -> Entity2 h
Entity2)

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

-- IsoOpMap - Constructable -


rdcPathOpMap :: PathOpMap f s a b -> Rdc (PathOpMap f s a b)
rdcPathOpMap :: forall (f :: * -> *) s a b.
PathOpMap f s a b -> Rdc (PathOpMap f s a b)
rdcPathOpMap PathOpMap f s a b
pth = case PathOpMap f s a b
pth of
  OpMap f s y b
ToOp1 :. OpMap f s y y
FromOp1 :. Path (OpMap f s) a y
p -> forall x. x -> Rdc x
reducesTo Path (OpMap f s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) s a b.
PathOpMap f s a b -> Rdc (PathOpMap f s a b)
rdcPathOpMap
  OpMap f s y b
FromOp1 :. OpMap f s y y
ToOp1 :. Path (OpMap f s) a y
p -> forall x. x -> Rdc x
reducesTo Path (OpMap f s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) s a b.
PathOpMap f s a b -> Rdc (PathOpMap f s a b)
rdcPathOpMap
  OpMap f s y b
h :. Path (OpMap f s) a y
p                -> forall (f :: * -> *) s a b.
PathOpMap f s a b -> Rdc (PathOpMap f s a b)
rdcPathOpMap Path (OpMap f s) a y
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (OpMap f s y b
hforall (m :: * -> * -> *) x z x. m x z -> Path m x x -> Path m x z
:.))
  PathOpMap f s a b
p                     -> forall (m :: * -> *) a. Monad m => a -> m a
return PathOpMap f s a b
p

instance Reducible (PathOpMap f s a b) where
  reduce :: PathOpMap f s a b -> PathOpMap f s a b
reduce = forall x. (x -> Rdc x) -> x -> x
reduceWith forall (f :: * -> *) s a b.
PathOpMap f s a b -> Rdc (PathOpMap f s a b)
rdcPathOpMap

instance Exposable (IsoOpMap f s a b) where
  type Form (IsoOpMap f s a b) = PathOpMap f s a b
  form :: IsoOpMap f s a b -> Form (IsoOpMap f s a b)
form (IsoOpMap PathOpMap f s a b
p) = PathOpMap f s a b
p

instance Constructable (IsoOpMap f s a b) where
  make :: Form (IsoOpMap f s a b) -> IsoOpMap f s a b
make Form (IsoOpMap f s a b)
p = forall (f :: * -> *) s a b. PathOpMap f s a b -> IsoOpMap f s a b
IsoOpMap (forall e. Reducible e => e -> e
reduce Form (IsoOpMap f s a b)
p)

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

-- IsoOpMap - Cayleyan2 -


instance Morphism (IsoOpMap f s) where
  type ObjectClass (IsoOpMap f s) = s
  homomorphous :: forall x y.
IsoOpMap f s x y -> Homomorphous (ObjectClass (IsoOpMap f s)) x y
homomorphous = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous

instance Transformable s t => EmbeddableMorphism (IsoOpMap f s) t
instance ForgetfulTyp s => EmbeddableMorphismTyp (IsoOpMap f s)

instance Category (IsoOpMap f s) where
  cOne :: forall x. Struct (ObjectClass (IsoOpMap f s)) x -> IsoOpMap f s x x
cOne Struct (ObjectClass (IsoOpMap f s)) x
o = forall (f :: * -> *) s a b. PathOpMap f s a b -> IsoOpMap f s a b
IsoOpMap (forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct (ObjectClass (IsoOpMap f s)) x
o)
  IsoOpMap PathOpMap f s y z
f . :: forall y z x.
IsoOpMap f s y z -> IsoOpMap f s x y -> IsoOpMap f s x z
. IsoOpMap PathOpMap f s x y
g = forall x. Constructable x => Form x -> x
make (PathOpMap f s y z
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. PathOpMap f s x y
g)

instance ForgetfulTyp s => Cayleyan2 (IsoOpMap f s) where
  invert2 :: forall x y. IsoOpMap f s x y -> IsoOpMap f s y x
invert2 (IsoOpMap PathOpMap f s x y
p) = forall (f :: * -> *) s a b. PathOpMap f s a b -> IsoOpMap f s a b
IsoOpMap (forall (m :: * -> * -> *) (f :: * -> * -> *) x y.
(Morphism m, Morphism f) =>
(forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u)
-> (forall u v. m u v -> f v u) -> Path m x y -> Path f y x
reverse forall x. x -> x
id forall (f :: * -> *) s a b. OpMap f s a b -> OpMap f s b a
invOpMap PathOpMap f s x y
p)

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

-- OpMap Path s - Hom -


instance ForgetfulOrt s => Applicative (OpMap O.Path s) where
  amap :: forall a b. OpMap Path s a b -> a -> b
amap h :: OpMap Path s a b
h@OpMap Path s a b
ToOp1 = forall x. Struct Ort x -> Op (Path x) -> Path (Op x)
coPath (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall (f :: * -> *) s x.
OpMap f s (Op (f x)) (f (Op x)) -> Struct s x
toOp1Struct OpMap Path s a b
h)) where
    coPath :: Struct Ort x -> Op (O.Path x) -> O.Path (Op x)
    coPath :: forall x. Struct Ort x -> Op (Path x) -> Path (Op x)
coPath Struct Ort x
Struct = forall x. Dualisable x => x -> Dual x
toDual forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. Op x -> x
fromOp

  amap h :: OpMap Path s a b
h@OpMap Path s a b
FromOp1 = forall x. Struct Ort x -> Path (Op x) -> Op (Path x)
coPathInv (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall (f :: * -> *) s x.
OpMap f s (f (Op x)) (Op (f x)) -> Struct s x
fromOp1Struct OpMap Path s a b
h)) where
    coPathInv :: Struct Ort x -> O.Path (Op x) -> Op (O.Path x)
    coPathInv :: forall x. Struct Ort x -> Path (Op x) -> Op (Path x)
coPathInv Struct Ort x
Struct = forall x. x -> Op x
Op forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. Dualisable x => Dual x -> x
fromDual

instance (TransformableOp s, ForgetfulOrt s, ForgetfulTyp s, Typeable s)
  => HomOriented (OpMap O.Path s) where
  pmap :: forall a b. OpMap Path s a b -> Point a -> Point b
pmap OpMap Path s a b
ToOp1 = forall x. x -> x
id
  pmap OpMap Path s a b
FromOp1 = forall x. x -> x
id

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

-- IsoOpMap Path s - Hom -


instance ForgetfulOrt s => Applicative (IsoOpMap O.Path s) where
  amap :: forall a b. IsoOpMap Path s a b -> a -> b
amap = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap

instance (TransformableOp s, ForgetfulOrt s, ForgetfulTyp s, Typeable s)
  => HomOriented (IsoOpMap O.Path s) where pmap :: forall a b. IsoOpMap Path s a b -> Point a -> Point b
pmap = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap
                                           
--------------------------------------------------------------------------------

-- IsoOpMap Path s - Functorial -


instance ForgetfulOrt s => Functorial (IsoOpMap O.Path s)

instance (TransformableOp s, ForgetfulOrt s, ForgetfulTyp s, Typeable s)
  => FunctorialHomOriented (IsoOpMap O.Path s)

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

-- isoCoPath -


-- | contravariant isomorphism from @'O.Path' __x__@ to @'O.Path' ('Op'__x__)@ .

isoCoPath :: Oriented x => IsoOpMap O.Path Ort (Op (O.Path x)) (O.Path (Op x))
isoCoPath :: forall x.
Oriented x =>
IsoOpMap Path Ort (Op (Path x)) (Path (Op x))
isoCoPath = forall x. Constructable x => Form x -> x
make (forall s (f :: * -> *) x.
(Structure s (Op (f x)), Structure s (f (Op x)), Structure s x) =>
OpMap f s (Op (f x)) (f (Op x))
ToOp1 forall (m :: * -> * -> *) x z x. m x z -> Path m x x -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath forall s x. Structure s x => Struct s x
Struct)

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

-- OpHom -


-- | induced homomorphism on 'Op'.

data OpHom h x y where
  OpHom :: Transformable1 Op (ObjectClass h) => h x y -> OpHom h (Op x) (Op y)

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

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

instance Validable2 h => Validable2 (OpHom h) where
  valid2 :: forall x y. OpHom h x y -> Statement
valid2 (OpHom h x y
h) = forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 h x y
h

instance Entity2 h => Entity2 (OpHom h)

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

-- OpHom - Hom -


instance Morphism h => Morphism (OpHom h) where
  type ObjectClass (OpHom h) = ObjectClass h
  homomorphous :: forall x y. OpHom h x y -> Homomorphous (ObjectClass (OpHom h)) x y
homomorphous (OpHom h x y
h) = forall (f :: * -> *) s x y.
Transformable1 f s =>
Homomorphous s x y -> Homomorphous s (f x) (f y)
tau1Hom (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h)
  
instance Applicative h => Applicative (OpHom h) where
  amap :: forall a b. OpHom h a b -> a -> b
amap (OpHom h x y
h) (Op x
x) = forall x. x -> Op x
Op (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h x y
h x
x)
  
instance EmbeddableMorphism h Ort    => EmbeddableMorphism (OpHom h) Ort
instance EmbeddableMorphism h Typ    => EmbeddableMorphism (OpHom h) Typ
instance EmbeddableMorphism h Mlt    => EmbeddableMorphism (OpHom h) Mlt
instance EmbeddableMorphism h Fbr    => EmbeddableMorphism (OpHom h) Fbr
instance EmbeddableMorphism h FbrOrt => EmbeddableMorphism (OpHom h) FbrOrt
instance EmbeddableMorphism h Add    => EmbeddableMorphism (OpHom h) Add
instance EmbeddableMorphism h Dst    => EmbeddableMorphism (OpHom h) Dst

instance EmbeddableMorphismTyp h => EmbeddableMorphismTyp (OpHom h)

instance HomOriented h => HomOriented (OpHom h) where
  pmap :: forall a b. OpHom h a b -> Point a -> Point b
pmap (OpHom h x y
h) = forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h x y
h