{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}

-- |

-- Module      : OAlg.Data.HomCo

-- Description : mapping between an object and its co-object.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- mapping between an object @m@ in @__m x__@ and its co-object, where @'Dual1' __m___ ~ __m__@.

module OAlg.Data.HomCo
  (
    -- * Category

    HomCo(), toCo, fromCo, sHomCo
  , PathCo(..), rdcCoToFromCo, rdcCoToFromDual, rdcPathCo
  , MorCo(..), mcoStruct

    -- * Functor

  , ApplicativeMorCo, FunctorialHomCo, FunctorHomCo(..)

    -- * Iso

  , isoCo, IsoCo

    -- * X

  , xscHomCo
  
    -- * Proposition

  , prpFunctorialHomCo
  )
  where

import Control.Monad

import OAlg.Prelude

import OAlg.Category.SDuality
import OAlg.Category.Dualisable
import OAlg.Category.Path
import OAlg.Category.Unify

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

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

-- MorCo -


-- | morphism to and from the co-cobject.

data MorCo m s o x y where
  ToCo   :: (Structure s x, TransformableG m s s, TransformableG o s s)
         => MorCo m s o (o (m x)) (m (o x))
  FromCo :: (Structure s x, TransformableG m s s, TransformableG o s s)
         => MorCo m s o (m (o x)) (o (m x))

deriving instance Show (MorCo m s o x y)
instance Show2 (MorCo m s o)

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

-- mcoStruct -


-- | whitness that @__x__@ is a @__s__@ structure.

mcoStruct :: MorCo m s o (i (j x)) y -> Struct s x
mcoStruct :: forall (m :: * -> *) s (o :: * -> *) (i :: * -> *) (j :: * -> *) x
       y.
MorCo m s o (i (j x)) y -> Struct s x
mcoStruct MorCo m s o (i (j x)) y
ToCo   = Struct s x
forall s x. Structure s x => Struct s x
Struct
mcoStruct MorCo m s o (i (j x)) y
FromCo = Struct s x
forall s x. Structure s x => Struct s x
Struct

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

-- tauCo -


-- | propagating the @__s__@ structure on @__x__@ to its co-object.

tauCo :: (TransformableG m s s, TransformableG o s s) => Struct s x -> Struct s (m (o x))
tauCo :: forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> Struct s (m (o x))
tauCo = Struct s (o x) -> Struct s (m (o x))
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO (Struct s (o x) -> Struct s (m (o x)))
-> (Struct s x -> Struct s (o x))
-> Struct s x
-> Struct s (m (o 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 s x -> Struct s (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO

instance Morphism (MorCo m s o) where
  type ObjectClass (MorCo m s o) = s
  homomorphous :: forall x y.
MorCo m s o x y -> Homomorphous (ObjectClass (MorCo m s o)) x y
homomorphous MorCo m s o x y
ToCo   = Struct s x -> Struct s (o (m x))
forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> Struct s (m (o x))
tauCo 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 x -> Struct s (m (o x))
forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> Struct s (m (o x))
tauCo Struct s x
forall s x. Structure s x => Struct s x
Struct
  homomorphous MorCo m s o x y
FromCo = Struct s x -> Struct s (m (o x))
forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> Struct s (m (o x))
tauCo 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 x -> Struct s (o (m x))
forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> Struct s (m (o x))
tauCo Struct s x
forall s x. Structure s x => Struct s x
Struct

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

-- toCo -


-- | to the co-object.

toCo :: (TransformableG m s s, TransformableG o s s)
  => Struct s x -> MorCo m s o (o (m x)) (m (o x))
toCo :: forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> MorCo m s o (o (m x)) (m (o x))
toCo Struct s x
Struct = MorCo m s o (o (m x)) (m (o x))
forall s x (m :: * -> *) (o :: * -> *).
(Structure s x, TransformableG m s s, TransformableG o s s) =>
MorCo m s o (o (m x)) (m (o x))
ToCo

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

-- fromCo -


-- | from the co-cobject.

fromCo :: (TransformableG m s s, TransformableG o s s)
  => Struct s x -> MorCo m s o (m (o x)) (o (m x))
fromCo :: forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> MorCo m s o (m (o x)) (o (m x))
fromCo Struct s x
Struct = MorCo m s o (m (o x)) (o (m x))
forall s x (m :: * -> *) (o :: * -> *).
(Structure s x, TransformableG m s s, TransformableG o s s) =>
MorCo m s o (m (o x)) (o (m x))
FromCo

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

-- PathCo -


-- | path of 'SMorphism' over 'MorCo'.

newtype PathCo m s o x y = PathCo (Path (SMorphism s s o (MorCo m s o)) x y)
  deriving (Int -> PathCo m s o x y -> ShowS
[PathCo m s o x y] -> ShowS
PathCo m s o x y -> String
(Int -> PathCo m s o x y -> ShowS)
-> (PathCo m s o x y -> String)
-> ([PathCo m s o x y] -> ShowS)
-> Show (PathCo m s o x y)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (m :: * -> *) s (o :: * -> *) x y.
Int -> PathCo m s o x y -> ShowS
forall (m :: * -> *) s (o :: * -> *) x y.
[PathCo m s o x y] -> ShowS
forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> String
$cshowsPrec :: forall (m :: * -> *) s (o :: * -> *) x y.
Int -> PathCo m s o x y -> ShowS
showsPrec :: Int -> PathCo m s o x y -> ShowS
$cshow :: forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> String
show :: PathCo m s o x y -> String
$cshowList :: forall (m :: * -> *) s (o :: * -> *) x y.
[PathCo m s o x y] -> ShowS
showList :: [PathCo m s o x y] -> ShowS
Show)

instance Show2 (PathCo m s o)

-- | reducing a path according to the rules:

--

-- (1) @'SCov' 'ToCo' ':.' 'SCov' 'FromCo' ':.' p'@ reduces to @p'@.

--

-- (2) @'SCov' 'FromCo' ':.' 'SCov' 'ToCo' ':.' p'@ reduces to @p'@.

rdcCoToFromCo :: PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcCoToFromCo :: forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcCoToFromCo (PathCo Path (SMorphism s s o (MorCo m s o)) x y
p) = case Path (SMorphism s s o (MorCo m s o)) x y
p of
  SCov MorCo m s o y1 y
ToCo :. SCov MorCo m s o y1 y1
FromCo :. Path (SMorphism s s o (MorCo m s o)) x y1
p' -> PathCo m s o x y1 -> Rdc (PathCo m s o x y1)
forall x. x -> Rdc x
reducesTo (Path (SMorphism s s o (MorCo m s o)) x y1 -> PathCo m s o x y1
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo Path (SMorphism s s o (MorCo m s o)) x y1
p')    Rdc (PathCo m s o x y1)
-> (PathCo m s o x y1 -> Rdc (PathCo m s o x y))
-> Rdc (PathCo m s o x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PathCo m s o x y1 -> Rdc (PathCo m s o x y)
PathCo m s o x y1 -> Rdc (PathCo m s o x y1)
forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcCoToFromCo
  SCov MorCo m s o y1 y
FromCo :. SCov MorCo m s o y1 y1
ToCo :. Path (SMorphism s s o (MorCo m s o)) x y1
p' -> PathCo m s o x y1 -> Rdc (PathCo m s o x y1)
forall x. x -> Rdc x
reducesTo (Path (SMorphism s s o (MorCo m s o)) x y1 -> PathCo m s o x y1
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo Path (SMorphism s s o (MorCo m s o)) x y1
p')    Rdc (PathCo m s o x y1)
-> (PathCo m s o x y1 -> Rdc (PathCo m s o x y))
-> Rdc (PathCo m s o x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PathCo m s o x y1 -> Rdc (PathCo m s o x y)
PathCo m s o x y1 -> Rdc (PathCo m s o x y1)
forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcCoToFromCo  
  SMorphism s s o (MorCo m s o) y1 y
p' :. Path (SMorphism s s o (MorCo m s o)) x y1
p''                      -> PathCo m s o x y1 -> Rdc (PathCo m s o x y1)
forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcCoToFromCo (Path (SMorphism s s o (MorCo m s o)) x y1 -> PathCo m s o x y1
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo Path (SMorphism s s o (MorCo m s o)) x y1
p'')
                                Rdc (PathCo m s o x y1)
-> (PathCo m s o x y1 -> Rdc (PathCo m s o x y))
-> Rdc (PathCo m s o x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(PathCo Path (SMorphism s s o (MorCo m s o)) x y1
p'') -> PathCo m s o x y -> Rdc (PathCo m s o x y)
forall x. x -> Rdc x
forall (m :: * -> *) a. Monad m => a -> m a
return (Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo (SMorphism s s o (MorCo m s o) y1 y
p' SMorphism s s o (MorCo m s o) y1 y
-> Path (SMorphism s s o (MorCo m s o)) x y1
-> Path (SMorphism s s o (MorCo m s o)) x y
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Path (SMorphism s s o (MorCo m s o)) x y1
p''))
  Path (SMorphism s s o (MorCo m s o)) x y
_                              -> PathCo m s o x y -> Rdc (PathCo m s o x y)
forall x. x -> Rdc x
forall (m :: * -> *) a. Monad m => a -> m a
return (Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo Path (SMorphism s s o (MorCo m s o)) x y
p)

-- | reducing a 'PathCo' according to 'rdcPathSMorphism'.

rdcCoToFromDual :: PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcCoToFromDual :: forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcCoToFromDual (PathCo Path (SMorphism s s o (MorCo m s o)) x y
p) = Path (SMorphism s s o (MorCo m s o)) x y
-> Rdc (Path (SMorphism s s o (MorCo m s o)) x y)
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
rdcPathSMorphism Path (SMorphism s s o (MorCo m s o)) x y
p Rdc (Path (SMorphism s s o (MorCo m s o)) x y)
-> (Path (SMorphism s s o (MorCo m s o)) x y
    -> Action RdcState (PathCo m s o x y))
-> Action RdcState (PathCo m s o x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PathCo m s o x y -> Action RdcState (PathCo m s o x y)
forall x. x -> Rdc x
forall (m :: * -> *) a. Monad m => a -> m a
return (PathCo m s o x y -> Action RdcState (PathCo m s o x y))
-> (Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y)
-> Path (SMorphism s s o (MorCo m s o)) x y
-> Action RdcState (PathCo m s o x y)
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
. Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo

-- | applying the rules of 'rdcCoToFromCo' and 'rdcCoToFromDual'.

rdcPathCo :: PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcPathCo :: forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcPathCo = PathCo m s o x y -> Rdc (PathCo m s o x y)
forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcCoToFromCo (PathCo m s o x y -> Rdc (PathCo m s o x y))
-> (PathCo m s o x y -> Rdc (PathCo m s o x y))
-> PathCo m s o x y
-> Rdc (PathCo m s o x y)
forall x. (x -> Rdc x) -> (x -> Rdc x) -> x -> Rdc x
>>>= PathCo m s o x y -> Rdc (PathCo m s o x y)
forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcCoToFromDual

instance Reducible (PathCo m s o x y) where reduce :: PathCo m s o x y -> PathCo m s o x y
reduce = (PathCo m s o x y -> Rdc (PathCo m s o x y))
-> PathCo m s o x y -> PathCo m s o x y
forall x. (x -> Rdc x) -> x -> x
reduceWith PathCo m s o x y -> Rdc (PathCo m s o x y)
forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> Rdc (PathCo m s o x y)
rdcPathCo

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

-- HomCo -


-- | homomorphism for applications of objects @__m__@ over @__x__@.

newtype HomCo m s o x y = HomCo (PathCo m s o x y)
  deriving (Int -> HomCo m s o x y -> ShowS
[HomCo m s o x y] -> ShowS
HomCo m s o x y -> String
(Int -> HomCo m s o x y -> ShowS)
-> (HomCo m s o x y -> String)
-> ([HomCo m s o x y] -> ShowS)
-> Show (HomCo m s o x y)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (m :: * -> *) s (o :: * -> *) x y.
Int -> HomCo m s o x y -> ShowS
forall (m :: * -> *) s (o :: * -> *) x y.
[HomCo m s o x y] -> ShowS
forall (m :: * -> *) s (o :: * -> *) x y. HomCo m s o x y -> String
$cshowsPrec :: forall (m :: * -> *) s (o :: * -> *) x y.
Int -> HomCo m s o x y -> ShowS
showsPrec :: Int -> HomCo m s o x y -> ShowS
$cshow :: forall (m :: * -> *) s (o :: * -> *) x y. HomCo m s o x y -> String
show :: HomCo m s o x y -> String
$cshowList :: forall (m :: * -> *) s (o :: * -> *) x y.
[HomCo m s o x y] -> ShowS
showList :: [HomCo m s o x y] -> ShowS
Show)

instance Show2 (HomCo m s o)

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

-- Constructable -


instance Exposable (HomCo m s o x y) where
  type Form (HomCo m s o x y) = PathCo m s o x y
  form :: HomCo m s o x y -> Form (HomCo m s o x y)
form (HomCo PathCo m s o x y
p) = Form (HomCo m s o x y)
PathCo m s o x y
p

instance Constructable (HomCo m s o x y) where make :: Form (HomCo m s o x y) -> HomCo m s o x y
make = PathCo m s o x y -> HomCo m s o x y
forall (m :: * -> *) s (o :: * -> *) x y.
PathCo m s o x y -> HomCo m s o x y
HomCo (PathCo m s o x y -> HomCo m s o x y)
-> (PathCo m s o x y -> PathCo m s o x y)
-> PathCo m s o x y
-> HomCo m s o x y
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
. PathCo m s o x y -> PathCo m s o x y
forall e. Reducible e => e -> e
reduce

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

-- sHomCo -


-- | functorial projection to 'HomCo'.

sHomCo :: SHom s s o (MorCo m s o) x y -> HomCo m s o x y
sHomCo :: forall s (o :: * -> *) (m :: * -> *) x y.
SHom s s o (MorCo m s o) x y -> HomCo m s o x y
sHomCo = Form (HomCo m s o x y) -> HomCo m s o x y
PathCo m s o x y -> HomCo m s o x y
forall x. Constructable x => Form x -> x
make (PathCo m s o x y -> HomCo m s o x y)
-> (SHom s s o (MorCo m s o) x y -> PathCo m s o x y)
-> SHom s s o (MorCo m s o) x y
-> HomCo m s o x y
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
. Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo (Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y)
-> (SHom s s o (MorCo m s o) x y
    -> Path (SMorphism s s o (MorCo m s o)) x y)
-> SHom s s o (MorCo m s o) x y
-> PathCo m s o x y
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
. SHom s s o (MorCo m s o) x y -> Form (SHom s s o (MorCo m s o) x y)
SHom s s o (MorCo m s o) x y
-> Path (SMorphism s s o (MorCo m s o)) x y
forall x. Exposable x => x -> Form x
form

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

-- Category -


instance Morphism (HomCo m s o) where
  type ObjectClass (HomCo m s o) = s
  homomorphous :: forall x y.
HomCo m s o x y -> Homomorphous (ObjectClass (HomCo m s o)) x y
homomorphous (HomCo (PathCo Path (SMorphism s s o (MorCo m s o)) x y
p)) = Path (SMorphism s s o (MorCo m s o)) x y
-> Homomorphous
     (ObjectClass (Path (SMorphism s s o (MorCo m s o)))) x y
forall x y.
Path (SMorphism s s o (MorCo m s o)) x y
-> Homomorphous
     (ObjectClass (Path (SMorphism s s o (MorCo m s o)))) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous Path (SMorphism s s o (MorCo m s o)) x y
p

instance Category (HomCo m s o) where
  cOne :: forall x. Struct (ObjectClass (HomCo m s o)) x -> HomCo m s o x x
cOne = Form (HomCo m s o x x) -> HomCo m s o x x
PathCo m s o x x -> HomCo m s o x x
forall x. Constructable x => Form x -> x
make (PathCo m s o x x -> HomCo m s o x x)
-> (Struct s x -> PathCo m s o x x)
-> Struct s x
-> HomCo m s o 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
. Path (SMorphism s s o (MorCo m s o)) x x -> PathCo m s o x x
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo (Path (SMorphism s s o (MorCo m s o)) x x -> PathCo m s o x x)
-> (Struct s x -> Path (SMorphism s s o (MorCo m s o)) x x)
-> Struct s x
-> PathCo m s o 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 s x -> Path (SMorphism s s o (MorCo m s o)) x x
Struct (ObjectClass (Path (SMorphism s s o (MorCo m s o)))) x
-> Path (SMorphism s s o (MorCo m s o)) x x
forall x.
Struct (ObjectClass (Path (SMorphism s s o (MorCo m s o)))) x
-> Path (SMorphism s s o (MorCo m s o)) x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne

  HomCo (PathCo Path (SMorphism s s o (MorCo m s o)) y z
f) . :: forall y z x. HomCo m s o y z -> HomCo m s o x y -> HomCo m s o x z
. HomCo (PathCo Path (SMorphism s s o (MorCo m s o)) x y
g) = Form (HomCo m s o x z) -> HomCo m s o x z
forall x. Constructable x => Form x -> x
make (Path (SMorphism s s o (MorCo m s o)) x z -> PathCo m s o x z
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo (Path (SMorphism s s o (MorCo m s o)) y z
f Path (SMorphism s s o (MorCo m s o)) y z
-> Path (SMorphism s s o (MorCo m s o)) x y
-> Path (SMorphism s s o (MorCo m s o)) x z
forall y z x.
Path (SMorphism s s o (MorCo m s o)) y z
-> Path (SMorphism s s o (MorCo m s o)) x y
-> Path (SMorphism s s o (MorCo m s o)) x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Path (SMorphism s s o (MorCo m s o)) x y
g))

instance Disjunctive (HomCo m s o x y) where variant :: HomCo m s o x y -> Variant
variant (HomCo (PathCo Path (SMorphism s s o (MorCo m s o)) x y
p)) = Path (SMorphism s s o (MorCo m s o)) x y -> Variant
forall x. Disjunctive x => x -> Variant
variant Path (SMorphism s s o (MorCo m s o)) x y
p
instance Disjunctive2 (HomCo m s o)
instance CategoryDisjunctive (HomCo m s o)

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

-- IsoCo -


-- | isomorphism for 'HomCo'.

type IsoCo m s o = Inv2 (HomCo m s o)

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

-- isoCo -


isoCoStruct :: (TransformableG m s s, TransformableG o s s)
  => Struct s (m x) -> Struct s (o (m x)) -> Struct s (m (o x))
  -> Struct s x -> Variant2 Contravariant (IsoCo m s o) (m x) (m (o x))
isoCoStruct :: forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s (m x)
-> Struct s (o (m x))
-> Struct s (m (o x))
-> Struct s x
-> Variant2 'Contravariant (IsoCo m s o) (m x) (m (o x))
isoCoStruct sm :: Struct s (m x)
sm@Struct s (m x)
Struct Struct s (o (m x))
Struct smo :: Struct s (m (o x))
smo@Struct s (m (o x))
Struct Struct s x
Struct = IsoCo m s o (m x) (m (o x))
-> Variant2 'Contravariant (IsoCo m s o) (m x) (m (o x))
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (HomCo m s o (m x) (m (o x))
-> HomCo m s o (m (o x)) (m x) -> IsoCo m s o (m x) (m (o x))
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 HomCo m s o (m x) (m (o x))
t HomCo m s o (m (o x)) (m x)
f) where
  t :: HomCo m s o (m x) (m (o x))
t = Form (HomCo m s o (m x) (m (o x))) -> HomCo m s o (m x) (m (o x))
forall x. Constructable x => Form x -> x
make (Path (SMorphism s s o (MorCo m s o)) (m x) (m (o x))
-> PathCo m s o (m x) (m (o x))
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo (MorCo m s o (o (m x)) (m (o x))
-> SMorphism s s o (MorCo m s o) (o (m x)) (m (o x))
forall (h :: * -> * -> *) s x y r (o :: * -> *).
Transformable (ObjectClass h) s =>
h x y -> SMorphism r s o h x y
SCov MorCo m s o (o (m x)) (m (o x))
forall s x (m :: * -> *) (o :: * -> *).
(Structure s x, TransformableG m s s, TransformableG o s s) =>
MorCo m s o (o (m x)) (m (o x))
ToCo SMorphism s s o (MorCo m s o) (o (m x)) (m (o x))
-> Path (SMorphism s s o (MorCo m s o)) (m x) (o (m x))
-> Path (SMorphism s s o (MorCo m s o)) (m x) (m (o x))
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. SMorphism s s o (MorCo m s o) (m x) (o (m x))
forall s x (o :: * -> *) r (h :: * -> * -> *).
(Structure s x, Structure s (o x)) =>
SMorphism r s o h x (o x)
SToDual SMorphism s s o (MorCo m s o) (m x) (o (m x))
-> Path (SMorphism s s o (MorCo m s o)) (m x) (m x)
-> Path (SMorphism s s o (MorCo m s o)) (m x) (o (m x))
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Struct (ObjectClass (SMorphism s s o (MorCo m s o))) (m x)
-> Path (SMorphism s s o (MorCo m s o)) (m x) (m x)
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct s (m x)
Struct (ObjectClass (SMorphism s s o (MorCo m s o))) (m x)
sm))
  f :: HomCo m s o (m (o x)) (m x)
f = Form (HomCo m s o (m (o x)) (m x)) -> HomCo m s o (m (o x)) (m x)
forall x. Constructable x => Form x -> x
make (Path (SMorphism s s o (MorCo m s o)) (m (o x)) (m x)
-> PathCo m s o (m (o x)) (m x)
forall (m :: * -> *) s (o :: * -> *) x y.
Path (SMorphism s s o (MorCo m s o)) x y -> PathCo m s o x y
PathCo (SMorphism s s o (MorCo m s o) (o (m x)) (m x)
forall s y (o :: * -> *) r (h :: * -> * -> *).
(Structure s y, Structure s (o y)) =>
SMorphism r s o h (o y) y
SFromDual SMorphism s s o (MorCo m s o) (o (m x)) (m x)
-> Path (SMorphism s s o (MorCo m s o)) (m (o x)) (o (m x))
-> Path (SMorphism s s o (MorCo m s o)) (m (o x)) (m x)
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. MorCo m s o (m (o x)) (o (m x))
-> SMorphism s s o (MorCo m s o) (m (o x)) (o (m x))
forall (h :: * -> * -> *) s x y r (o :: * -> *).
Transformable (ObjectClass h) s =>
h x y -> SMorphism r s o h x y
SCov MorCo m s o (m (o x)) (o (m x))
forall s x (m :: * -> *) (o :: * -> *).
(Structure s x, TransformableG m s s, TransformableG o s s) =>
MorCo m s o (m (o x)) (o (m x))
FromCo SMorphism s s o (MorCo m s o) (m (o x)) (o (m x))
-> Path (SMorphism s s o (MorCo m s o)) (m (o x)) (m (o x))
-> Path (SMorphism s s o (MorCo m s o)) (m (o x)) (o (m x))
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Struct (ObjectClass (SMorphism s s o (MorCo m s o))) (m (o x))
-> Path (SMorphism s s o (MorCo m s o)) (m (o x)) (m (o x))
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct s (m (o x))
Struct (ObjectClass (SMorphism s s o (MorCo m s o))) (m (o x))
smo)) 

-- | contravariant isomorphism.

isoCo ::(TransformableG m s s, TransformableG o s s)
  => Struct s x -> Variant2 Contravariant (IsoCo m s o) (m x) (m (o x))
isoCo :: forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> Variant2 'Contravariant (IsoCo m s o) (m x) (m (o x))
isoCo Struct s x
s = Struct s (m x)
-> Struct s (o (m x))
-> Struct s (m (o x))
-> Struct s x
-> Variant2 'Contravariant (IsoCo m s o) (m x) (m (o x))
forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s (m x)
-> Struct s (o (m x))
-> Struct s (m (o x))
-> Struct s x
-> Variant2 'Contravariant (IsoCo m s o) (m x) (m (o x))
isoCoStruct (Struct s x -> Struct s (m x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct s x
s) (Struct s (m x) -> Struct s (o (m x))
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO (Struct s (m x) -> Struct s (o (m x)))
-> Struct s (m x) -> Struct s (o (m x))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct s x -> Struct s (m x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct s x
s) (Struct s (o x) -> Struct s (m (o x))
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO (Struct s (o x) -> Struct s (m (o x)))
-> Struct s (o x) -> Struct s (m (o x))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct s x -> Struct s (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct s x
s) Struct s x
s

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

-- ApplicativeMorCo -


-- | helper class to avoid undecidable instances.

class ApplicativeG d (MorCo m s o) c => ApplicativeMorCo d m s o c

instance
  ( ApplicativeMorCo d m s o (->)
  , DualisableG s (->) o d
  )
  => ApplicativeG d (HomCo m s o) (->) where
  amapG :: forall x y. HomCo m s o x y -> d x -> d y
amapG (HomCo (PathCo Path (SMorphism s s o (MorCo m s o)) x y
p)) d x
d = d y
d' where SVal d y
d' = Path (SMorphism s s o (MorCo m s o)) x y -> SVal d x -> SVal d y
forall x y.
Path (SMorphism s s o (MorCo m s o)) x y -> SVal d x -> SVal d y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Path (SMorphism s s o (MorCo m s o)) x y
p (d x -> SVal d x
forall (d :: * -> *) x. d x -> SVal d x
SVal d x
d)  

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

-- FunctorialHomCo -


-- | functorial predicat for 'HomCo'.

--

-- __Properties__ Let @'FunctorialHomCo' __d s m o c__@, then for all @__x__@

-- and @s@ in @'Struct' __s x__@ holds:

--

-- (1) @'amapG' ('fromCo' s) '.'  'amapG' ('toCo' s) '.=.' 'cOneDOM' f s@.

--

-- (2) @'amapG' ('toCo' s) '.' 'amapG' ('fromCo' s)  '.=.' 'cOneDMO' f s@.

--

-- where @f@ is anay proxy in @__q d s m o c__@.

class
  ( Category c
  , ApplicativeMorCo d m s o c
  , TransformableG m s s, TransformableG o s s
  , TransformableG d s (ObjectClass c)
  ) => FunctorialHomCo d m s o c

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

-- FunctorHomCo -


-- | whiteness of being 'FunctorialHomCo'.

data FunctorHomCo d m s o c where
  FunctorHomCo :: FunctorialHomCo d m s o c => FunctorHomCo d m s o c
  
--------------------------------------------------------------------------------

-- prpFunctorialHomCo -


cOneDOM :: FunctorHomCo d m s o c -> Struct s x -> c (d (o (m x))) (d (o (m x)))
cOneDOM :: forall (d :: * -> *) (m :: * -> *) s (o :: * -> *)
       (c :: * -> * -> *) x.
FunctorHomCo d m s o c
-> Struct s x -> c (d (o (m x))) (d (o (m x)))
cOneDOM FunctorHomCo d m s o c
FunctorHomCo = Struct (ObjectClass c) (d (o (m x)))
-> c (d (o (m x))) (d (o (m 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) (d (o (m x)))
 -> c (d (o (m x))) (d (o (m x))))
-> (Struct s x -> Struct (ObjectClass c) (d (o (m x))))
-> Struct s x
-> c (d (o (m x))) (d (o (m 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 s (o (m x)) -> Struct (ObjectClass c) (d (o (m x)))
forall x. Struct s x -> Struct (ObjectClass c) (d x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG (Struct s (o (m x)) -> Struct (ObjectClass c) (d (o (m x))))
-> (Struct s x -> Struct s (o (m x)))
-> Struct s x
-> Struct (ObjectClass c) (d (o (m 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 s (m x) -> Struct s (o (m x))
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO (Struct s (m x) -> Struct s (o (m x)))
-> (Struct s x -> Struct s (m x))
-> Struct s x
-> Struct s (o (m 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 s x -> Struct s (m x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO

cOneDMO :: FunctorHomCo d m s o c -> Struct s x -> c (d (m (o x))) (d (m (o x)))
cOneDMO :: forall (d :: * -> *) (m :: * -> *) s (o :: * -> *)
       (c :: * -> * -> *) x.
FunctorHomCo d m s o c
-> Struct s x -> c (d (m (o x))) (d (m (o x)))
cOneDMO FunctorHomCo d m s o c
FunctorHomCo = Struct (ObjectClass c) (d (m (o x)))
-> c (d (m (o x))) (d (m (o 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) (d (m (o x)))
 -> c (d (m (o x))) (d (m (o x))))
-> (Struct s x -> Struct (ObjectClass c) (d (m (o x))))
-> Struct s x
-> c (d (m (o x))) (d (m (o 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 s (m (o x)) -> Struct (ObjectClass c) (d (m (o x)))
forall x. Struct s x -> Struct (ObjectClass c) (d x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG (Struct s (m (o x)) -> Struct (ObjectClass c) (d (m (o x))))
-> (Struct s x -> Struct s (m (o x)))
-> Struct s x
-> Struct (ObjectClass c) (d (m (o 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 s (o x) -> Struct s (m (o x))
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO(Struct s (o x) -> Struct s (m (o x)))
-> (Struct s x -> Struct s (o x))
-> Struct s x
-> Struct s (m (o 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 s x -> Struct s (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO

relFunctorialHomCo :: EqExt c => FunctorHomCo d m s o c -> Struct s x -> Statement
relFunctorialHomCo :: forall (c :: * -> * -> *) (d :: * -> *) (m :: * -> *) s
       (o :: * -> *) x.
EqExt c =>
FunctorHomCo d m s o c -> Struct s x -> Statement
relFunctorialHomCo f :: FunctorHomCo d m s o c
f@FunctorHomCo d m s o c
FunctorHomCo Struct s x
s
  = [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (MorCo m s o (m (o x)) (o (m x)) -> c (d (m (o x))) (d (o (m x)))
forall x y. MorCo m s o x y -> c (d x) (d y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Struct s x -> MorCo m s o (m (o x)) (o (m x))
forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> MorCo m s o (m (o x)) (o (m x))
fromCo Struct s x
s) c (d (m (o x))) (d (o (m x)))
-> c (d (o (m x))) (d (m (o x))) -> c (d (o (m x))) (d (o (m 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
.  MorCo m s o (o (m x)) (m (o x)) -> c (d (o (m x))) (d (m (o x)))
forall x y. MorCo m s o x y -> c (d x) (d y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Struct s x -> MorCo m s o (o (m x)) (m (o x))
forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> MorCo m s o (o (m x)) (m (o x))
toCo Struct s x
s) c (d (o (m x))) (d (o (m x)))
-> c (d (o (m x))) (d (o (m x))) -> Statement
forall x y. c x y -> c x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. FunctorHomCo d m s o c
-> Struct s x -> c (d (o (m x))) (d (o (m x)))
forall (d :: * -> *) (m :: * -> *) s (o :: * -> *)
       (c :: * -> * -> *) x.
FunctorHomCo d m s o c
-> Struct s x -> c (d (o (m x))) (d (o (m x)))
cOneDOM FunctorHomCo d m s o c
f Struct s x
s)
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (MorCo m s o (o (m x)) (m (o x)) -> c (d (o (m x))) (d (m (o x)))
forall x y. MorCo m s o x y -> c (d x) (d y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Struct s x -> MorCo m s o (o (m x)) (m (o x))
forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> MorCo m s o (o (m x)) (m (o x))
toCo Struct s x
s) c (d (o (m x))) (d (m (o x)))
-> c (d (m (o x))) (d (o (m x))) -> c (d (m (o x))) (d (m (o 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
. MorCo m s o (m (o x)) (o (m x)) -> c (d (m (o x))) (d (o (m x)))
forall x y. MorCo m s o x y -> c (d x) (d y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Struct s x -> MorCo m s o (m (o x)) (o (m x))
forall (m :: * -> *) s (o :: * -> *) x.
(TransformableG m s s, TransformableG o s s) =>
Struct s x -> MorCo m s o (m (o x)) (o (m x))
fromCo Struct s x
s)  c (d (m (o x))) (d (m (o x)))
-> c (d (m (o x))) (d (m (o x))) -> Statement
forall x y. c x y -> c x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. FunctorHomCo d m s o c
-> Struct s x -> c (d (m (o x))) (d (m (o x)))
forall (d :: * -> *) (m :: * -> *) s (o :: * -> *)
       (c :: * -> * -> *) x.
FunctorHomCo d m s o c
-> Struct s x -> c (d (m (o x))) (d (m (o x)))
cOneDMO FunctorHomCo d m s o c
f Struct s x
s)
        ]

-- | validity according to 'FunctorialHomCo'.

prpFunctorialHomCo :: EqExt c => FunctorHomCo d m s o c -> Struct s x -> Statement
prpFunctorialHomCo :: forall (c :: * -> * -> *) (d :: * -> *) (m :: * -> *) s
       (o :: * -> *) x.
EqExt c =>
FunctorHomCo d m s o c -> Struct s x -> Statement
prpFunctorialHomCo FunctorHomCo d m s o c
m Struct s x
s = String -> Label
Prp String
"FunctoiralCo" Label -> Statement -> Statement
:<=>: FunctorHomCo d m s o c -> Struct s x -> Statement
forall (c :: * -> * -> *) (d :: * -> *) (m :: * -> *) s
       (o :: * -> *) x.
EqExt c =>
FunctorHomCo d m s o c -> Struct s x -> Statement
relFunctorialHomCo FunctorHomCo d m s o c
m Struct s x
s

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

-- FunctorialG -


instance (FunctorialHomCo d m s o (->) , DualisableG s (->) o d)
  => FunctorialG d (HomCo m s o) (->)

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

-- xHomCo -


-- | random variable for some composable 'HomCo's.

xscHomCo :: TransformableG o s s
  => N -> X (SomeObjectClass (HomCo m s o)) -> X (SomeMorphism (MorCo m s o))
  -> X (SomeCmpb2 (HomCo m s o))
xscHomCo :: forall (o :: * -> *) s (m :: * -> *).
TransformableG o s s =>
N
-> X (SomeObjectClass (HomCo m s o))
-> X (SomeMorphism (MorCo m s o))
-> X (SomeCmpb2 (HomCo m s o))
xscHomCo N
n X (SomeObjectClass (HomCo m s o))
xsoHomCo X (SomeMorphism (MorCo m s o))
xsmMorCo
  = (SomeCmpb2 (SHom s s o (MorCo m s o)) -> SomeCmpb2 (HomCo m s o))
-> X (SomeCmpb2 (SHom s s o (MorCo m s o)))
-> X (SomeCmpb2 (HomCo m s o))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (SHom s s o (MorCo m s o)) -> SomeCmpb2 (HomCo m s o)
forall s (o :: * -> *) (m :: * -> *).
SomeCmpb2 (SHom s s o (MorCo m s o)) -> SomeCmpb2 (HomCo m s o)
soce (X (SomeCmpb2 (SHom s s o (MorCo m s o)))
 -> X (SomeCmpb2 (HomCo m s o)))
-> X (SomeCmpb2 (SHom s s o (MorCo m s o)))
-> X (SomeCmpb2 (HomCo m s o))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N
-> X (SomeObjectClass (SHom s s o (MorCo m s o)))
-> X (SomeMorphism (MorCo m s o))
-> X (SomeCmpb2 (SHom s s o (MorCo m s o)))
forall (h :: * -> * -> *) s (o :: * -> *) r.
(Morphism h, Transformable (ObjectClass h) s,
 Transformable1 o s) =>
N
-> X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism h)
-> X (SomeCmpb2 (SHom r s o h))
xSctSomeCmpb2 N
n ((SomeObjectClass (HomCo m s o)
 -> SomeObjectClass (SHom s s o (MorCo m s o)))
-> X (SomeObjectClass (HomCo m s o))
-> X (SomeObjectClass (SHom s s o (MorCo m s o)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeObjectClass (HomCo m s o)
-> SomeObjectClass (SHom s s o (MorCo m s o))
forall (m :: * -> *) s (o :: * -> *).
SomeObjectClass (HomCo m s o)
-> SomeObjectClass (SHom s s o (MorCo m s o))
socSHom X (SomeObjectClass (HomCo m s o))
xsoHomCo) X (SomeMorphism (MorCo m s o))
xsmMorCo where
  
  socSHom :: SomeObjectClass (HomCo m s o) -> SomeObjectClass (SHom s s o (MorCo m s o))
  socSHom :: forall (m :: * -> *) s (o :: * -> *).
SomeObjectClass (HomCo m s o)
-> SomeObjectClass (SHom s s o (MorCo m s o))
socSHom (SomeObjectClass Struct (ObjectClass (HomCo m s o)) x
o) = Struct (ObjectClass (SHom s s o (MorCo m s o))) x
-> SomeObjectClass (SHom s s o (MorCo m s o))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass Struct (ObjectClass (SHom s s o (MorCo m s o))) x
Struct (ObjectClass (HomCo m s o)) x
o

  soce :: SomeCmpb2 (SHom s s o (MorCo m s o)) -> SomeCmpb2 (HomCo m s o)
  soce :: forall s (o :: * -> *) (m :: * -> *).
SomeCmpb2 (SHom s s o (MorCo m s o)) -> SomeCmpb2 (HomCo m s o)
soce (SomeCmpb2 SHom s s o (MorCo m s o) y z
f SHom s s o (MorCo m s o) x y
g) = HomCo m s o y z -> HomCo m s o x y -> SomeCmpb2 (HomCo m s o)
forall (c :: * -> * -> *) y z x. c y z -> c x y -> SomeCmpb2 c
SomeCmpb2 (SHom s s o (MorCo m s o) y z -> HomCo m s o y z
forall s (o :: * -> *) (m :: * -> *) x y.
SHom s s o (MorCo m s o) x y -> HomCo m s o x y
sHomCo SHom s s o (MorCo m s o) y z
f) (SHom s s o (MorCo m s o) x y -> HomCo m s o x y
forall s (o :: * -> *) (m :: * -> *) x y.
SHom s s o (MorCo m s o) x y -> HomCo m s o x y
sHomCo SHom s s o (MorCo m s o) x y
g)