{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Entity.Slice.Sliced

-- Description : oriented structures with a distinguished point.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- 'Oriented' structures with a distinguished 'Point'.

module OAlg.Entity.Slice.Sliced
  (
    -- * Sliced

    Sliced(..), sliceIndex

    -- * Hom

    
    -- ** Oriented

  , HomSlicedOriented, Sld
  , sliceIndexDomain, sliceIndexRange
  , sldHom
  , toDualOpOrtSld, toDualOpOrtSld'

    -- ** Multiplicative

  , HomSlicedMultiplicative
  , toDualOpMltSld, toDualOpMltSld'

    -- ** Distributive

  , HomSlicedDistributive
  , toDualOpDstSld, toDualOpDstSld'
  
    -- * Proposition

  , prpHomSlicedOriented

  ) where

import Data.Kind
import Data.Typeable

import OAlg.Prelude

import OAlg.Data.Singleton

import OAlg.Structure.Oriented hiding (Path(..))
import OAlg.Structure.Multiplicative
import OAlg.Structure.Distributive
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive

import OAlg.Hom.Definition
import OAlg.Hom.Oriented
import OAlg.Hom.Multiplicative
import OAlg.Hom.Distributive

import OAlg.Data.Symbol

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

-- Sliced -


-- | Slicing 'Oriented' structures at a distinguished 'Point', given by the type of the index

--  __@i@__. 

--

--  __Note__ The constraint @'Singleton1' __i__@ ensures that the distinguished point

--  depends only on the type __@i c@__.

class (Entity1 i, Singleton1 i, Oriented c) => Sliced i c where
  -- | the distingueished point of the given index type @__i__@.

  slicePoint :: i c -> Point c

instance Sliced i c => Sliced i (Op c) where
  slicePoint :: i (Op c) -> Point (Op c)
slicePoint i (Op c)
i = i (Op c) -> Point c -> Point (Op c)
forall c (f :: * -> *) (p :: * -> *).
(Point c ~ Point (f c)) =>
p (f c) -> Point c -> Point (f c)
to i (Op c)
i (Point c -> Point c) -> Point c -> Point c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ i c -> Point c
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint (i c -> Point c) -> i c -> Point c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ i (Op c) -> i c
forall (i :: * -> *) (f :: * -> *) c.
Singleton1 i =>
i (f c) -> i c
fo i (Op c)
i where
    
    fo :: Singleton1 i => i (f c) -> i c
    fo :: forall (i :: * -> *) (f :: * -> *) c.
Singleton1 i =>
i (f c) -> i c
fo i (f c)
_ = i c
forall x. i x
forall (s :: * -> *) x. Singleton1 s => s x
unit1

    to :: Point c ~ Point (f c) => p (f c) -> Point c -> Point (f c)
    to :: forall c (f :: * -> *) (p :: * -> *).
(Point c ~ Point (f c)) =>
p (f c) -> Point c -> Point (f c)
to p (f c)
_ = Point c -> Point c
Point c -> Point (f c)
forall x. x -> x
id

instance Sliced Proxy OS where
  slicePoint :: Proxy OS -> Point OS
slicePoint Proxy OS
_ = Symbol
Point OS
P

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

-- sliceIndex -


-- | the slice index according to the proxy type.

sliceIndex :: Sliced i x => q i x -> i x
sliceIndex :: forall (i :: * -> *) x (q :: (* -> *) -> * -> *).
Sliced i x =>
q i x -> i x
sliceIndex q i x
_ = i x
forall x. i x
forall (s :: * -> *) x. Singleton1 s => s x
unit1

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

-- Sld -


-- | type index for 'Sliced' structures.

data Sld (i :: Type -> Type)

type instance Structure (Sld i) x = Sliced i x

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

-- HomSlicedOriented -


-- | homomorphisms between 'Sliced' structures, i.e homomorphisms between 'Oriented' structures where

-- 'pmap' preserves the distinguished point.

--

-- __Property__ Let @'HomSlicedOriented' __i__ __h__@, then holds:

--

-- (1) For all @__x__@, @__y__@ and @h@ in @__h x y__@ holds:

-- @'pmap' h px '==' py@, where @px = 'slicePoint' '$' 'sliceIndexDomain' '$' 'sldHom' q h@,

-- @py = 'slicePoint' '$' 'sliceIndexRange' '$' 'sldHom' q h@ and @q@ is any proxy in @__q i__@.

class (HomOrientedDisjunctive h, Transformable (ObjectClass h) (Sld i)) => HomSlicedOriented i h

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

-- sliceIndexDomain -

-- | the slice index for the 'domain'.

sliceIndexDomain :: Homomorphous (Sld i) x y -> i x
sliceIndexDomain :: forall (i :: * -> *) x y. Homomorphous (Sld i) x y -> i x
sliceIndexDomain (Struct (Sld i) x
Struct :>: Struct (Sld i) y
_) = i x
forall x. i x
forall (s :: * -> *) x. Singleton1 s => s x
unit1

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

-- sliceIndexRange -


-- | the slice index for the 'range'.

sliceIndexRange :: Homomorphous (Sld i) x y -> i y
sliceIndexRange :: forall (i :: * -> *) x y. Homomorphous (Sld i) x y -> i y
sliceIndexRange (Struct (Sld i) x
_ :>: Struct (Sld i) y
Struct) = i y
forall x. i x
forall (s :: * -> *) x. Singleton1 s => s x
unit1

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

-- sldHom -


-- | the induced homomorphous structure.

sldHom :: HomSlicedOriented i h => q i -> h x y -> Homomorphous (Sld i) x y
sldHom :: forall (i :: * -> *) (h :: * -> * -> *) (q :: (* -> *) -> *) x y.
HomSlicedOriented i h =>
q i -> h x y -> Homomorphous (Sld i) x y
sldHom q i
_ h x y
h = Homomorphous (ObjectClass h) x y -> Homomorphous (Sld i) 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)

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

-- prpHomSlicedOriented -


relHomSlicedOriented :: (HomSlicedOriented i h, Show2 h)
  => Homomorphous Ort x y -> Homomorphous (Sld i) x y -> h x y -> Statement
relHomSlicedOriented :: forall (i :: * -> *) (h :: * -> * -> *) x y.
(HomSlicedOriented i h, Show2 h) =>
Homomorphous Ort x y
-> Homomorphous (Sld i) x y -> h x y -> Statement
relHomSlicedOriented (Struct Ort x
Struct:>:Struct Ort y
Struct) hSld :: Homomorphous (Sld i) x y
hSld@(Struct (Sld i) x
Struct:>:Struct (Sld i) y
Struct) h x y
h
  = (h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h Point x
px Point y -> Point y -> Bool
forall a. Eq a => a -> a -> Bool
== Point y
py) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [ String
"h"String -> String -> Parameter
:=h x y -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h x y
h
                                 , String
"px"String -> String -> Parameter
:= Point x -> String
forall a. Show a => a -> String
show Point x
px
                                 , String
"py"String -> String -> Parameter
:=Point y -> String
forall a. Show a => a -> String
show Point y
py
                                 ] 
    where
      px :: Point x
px = i x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint (i x -> Point x) -> i x -> Point x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Homomorphous (Sld i) x y -> i x
forall (i :: * -> *) x y. Homomorphous (Sld i) x y -> i x
sliceIndexDomain Homomorphous (Sld i) x y
hSld
      py :: Point y
py = i y -> Point y
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint (i y -> Point y) -> i y -> Point y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Homomorphous (Sld i) x y -> i y
forall (i :: * -> *) x y. Homomorphous (Sld i) x y -> i y
sliceIndexRange Homomorphous (Sld i) x y
hSld

-- | validity according to 'HomSlicedOriented'.

prpHomSlicedOriented :: (HomSlicedOriented i h, Show2 h)
  => q i -> h x y -> Statement
prpHomSlicedOriented :: forall (i :: * -> *) (h :: * -> * -> *) (q :: (* -> *) -> *) x y.
(HomSlicedOriented i h, Show2 h) =>
q i -> h x y -> Statement
prpHomSlicedOriented q i
q h x y
h = String -> Label
Prp String
"HomSlicedOriented"
  Label -> Statement -> Statement
:<=>: Homomorphous Ort x y
-> Homomorphous (Sld i) x y -> h x y -> Statement
forall (i :: * -> *) (h :: * -> * -> *) x y.
(HomSlicedOriented i h, Show2 h) =>
Homomorphous Ort x y
-> Homomorphous (Sld i) x y -> h x y -> Statement
relHomSlicedOriented (Homomorphous (ObjectClass h) x y -> Homomorphous Ort x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (Homomorphous (ObjectClass h) x y -> Homomorphous Ort x y)
-> Homomorphous (ObjectClass h) x y -> Homomorphous Ort x y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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) (q i -> h x y -> Homomorphous (Sld i) x y
forall (i :: * -> *) (h :: * -> * -> *) (q :: (* -> *) -> *) x y.
HomSlicedOriented i h =>
q i -> h x y -> Homomorphous (Sld i) x y
sldHom q i
q h x y
h) h x y
h

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

-- IsoO - HomSlicedOriented -


instance Transformable (s,Sld i) Type where tau :: forall x. Struct (s, Sld i) x -> Struct (*) x
tau Struct (s, Sld i) x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct

instance TransformableType (s,Sld i)

instance Transformable (s,Sld i) (Sld i) where tau :: forall x. Struct (s, Sld i) x -> Struct (Sld i) x
tau = Struct (s, Sld i) x -> Struct (Sld i) x
forall s t x. Struct (s, t) x -> Struct t x
tauSnd

instance Transformable s Ort => Transformable (s,Sld i) Ort where tau :: forall x. Struct (s, Sld i) x -> Struct Ort x
tau = Struct s x -> Struct Ort x
forall x. Struct s x -> Struct Ort x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Ort x)
-> (Struct (s, Sld i) x -> Struct s x)
-> Struct (s, Sld i) x
-> Struct Ort 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, Sld i) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance Transformable s Ort => TransformableOrt (s,Sld i)

instance Transformable s Mlt => Transformable (s,Sld i) Mlt where tau :: forall x. Struct (s, Sld i) x -> Struct Mlt x
tau = Struct s x -> Struct Mlt x
forall x. Struct s x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Mlt x)
-> (Struct (s, Sld i) x -> Struct s x)
-> Struct (s, Sld i) x
-> Struct Mlt 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, Sld i) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance TransformableMlt s => TransformableMlt (s,Sld i)

instance Transformable s Fbr => Transformable (s,Sld i) Fbr where tau :: forall x. Struct (s, Sld i) x -> Struct Fbr x
tau = Struct s x -> Struct Fbr x
forall x. Struct s x -> Struct Fbr x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Fbr x)
-> (Struct (s, Sld i) x -> Struct s x)
-> Struct (s, Sld i) x
-> Struct Fbr 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, Sld i) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance TransformableFbr s => TransformableFbr (s,Sld i)

instance Transformable s Add => Transformable (s,Sld i) Add where tau :: forall x. Struct (s, Sld i) x -> Struct Add x
tau = Struct s x -> Struct Add x
forall x. Struct s x -> Struct Add x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Add x)
-> (Struct (s, Sld i) x -> Struct s x)
-> Struct (s, Sld i) x
-> Struct Add 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, Sld i) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance TransformableAdd s => TransformableAdd (s,Sld i)

instance Transformable s FbrOrt => Transformable (s,Sld i) FbrOrt where tau :: forall x. Struct (s, Sld i) x -> Struct FbrOrt x
tau = Struct s x -> Struct FbrOrt x
forall x. Struct s x -> Struct FbrOrt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct FbrOrt x)
-> (Struct (s, Sld i) x -> Struct s x)
-> Struct (s, Sld i) x
-> Struct FbrOrt 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, Sld i) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance TransformableFbrOrt s => TransformableFbrOrt (s,Sld i)

instance Transformable s Dst => Transformable (s,Sld i) Dst where tau :: forall x. Struct (s, Sld i) x -> Struct Dst x
tau = Struct s x -> Struct Dst x
forall x. Struct s x -> Struct Dst x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Dst x)
-> (Struct (s, Sld i) x -> Struct s x)
-> Struct (s, Sld i) x
-> Struct Dst 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, Sld i) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance TransformableDst s => TransformableDst (s,Sld i)


instance TransformableG Op (Sld i) (Sld i) where tauG :: forall x. Struct (Sld i) x -> Struct (Sld i) (Op x)
tauG Struct (Sld i) x
Struct = Struct (Sld i) (Op x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableG Op (s,Sld i) (Sld i) where tauG :: forall x. Struct (s, Sld i) x -> Struct (Sld i) (Op x)
tauG = Struct (Sld i) x -> Struct (Sld i) (Op x)
forall x. Struct (Sld i) x -> Struct (Sld i) (Op x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG (Struct (Sld i) x -> Struct (Sld i) (Op x))
-> (Struct (s, Sld i) x -> Struct (Sld i) x)
-> Struct (s, Sld i) x
-> Struct (Sld i) (Op 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, Sld i) x -> Struct (Sld i) x
forall s t x. Struct (s, t) x -> Struct t x
tauSnd

instance TransformableOp (Ort,Sld i)
instance TransformableGRefl Op (Ort,Sld i)

instance TransformableOp (Mlt,Sld i)
instance TransformableGRefl Op (Mlt,Sld i)

instance TransformableOp (Dst,Sld i)
instance TransformableGRefl Op (Dst,Sld i)

instance Transformable (s,Sld i) s
  => TransformableObjectClass (s,Sld i) (HomDisjEmpty s Op)

instance
  ( Transformable s Ort
  , TransformableOp (s,Sld i)
  )
  => HomSlicedOriented i (HomDisjEmpty (s,Sld i) Op)

instance (CategoryDisjunctive h, HomSlicedOriented i h) => HomSlicedOriented i (Inv2 h)

instance
  ( TransformableOrt s
  , TransformableType s
  , TransformableOp s
  ) => HomSlicedOriented i (Sub (s,Sld i) (HomDisjEmpty s Op))

instance
  ( TransformableOrt s
  , TransformableType s
  , TransformableOp s
  )
  => HomSlicedOriented i (Sub (s,Sld i) (IsoO s Op))

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

-- toDualOpOrtSld -


-- | contravariant isomorphism on 'Sliced' 'Oriented' structures. 

toDualOpOrtSld :: Sliced i x => Variant2 Contravariant (IsoO (Ort,Sld i) Op) x (Op x)
toDualOpOrtSld :: forall (i :: * -> *) x.
Sliced i x =>
Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x)
toDualOpOrtSld = Struct (Ort, Sld i) x
-> Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO Struct (Ort, Sld i) x
forall s x. Structure s x => Struct s x
Struct

-- | contravariant isomorphism on 'Sliced' 'Oriented' structures according to the proxy type.

toDualOpOrtSld' :: Sliced i x => q i -> Variant2 Contravariant (IsoO (Ort, Sld i) Op) x (Op x)
toDualOpOrtSld' :: forall (i :: * -> *) x (q :: (* -> *) -> *).
Sliced i x =>
q i -> Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x)
toDualOpOrtSld' q i
_ = Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x)
forall (i :: * -> *) x.
Sliced i x =>
Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x)
toDualOpOrtSld

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

-- HomSlicedMultiplicative -


-- | disjunctive multiplicative homomorphism respecting the slice structure.

type HomSlicedMultiplicative i h = (HomSlicedOriented i h, HomMultiplicativeDisjunctive h)

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

-- toDualOpMltSld -


-- | contravariant isomorphism on 'Sliced' 'Multiplicative' structures. 

toDualOpMltSld :: (Sliced i x, Multiplicative x)
  => Variant2 Contravariant (IsoO (Mlt,Sld i) Op) x (Op x)
toDualOpMltSld :: forall (i :: * -> *) x.
(Sliced i x, Multiplicative x) =>
Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x)
toDualOpMltSld = Struct (Mlt, Sld i) x
-> Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO Struct (Mlt, Sld i) x
forall s x. Structure s x => Struct s x
Struct

-- | contravariant isomorphism on 'Sliced' 'Multiplicative' structures according to the proxy type.

toDualOpMltSld' :: (Sliced i x, Multiplicative x)
  => q i -> Variant2 Contravariant (IsoO (Mlt,Sld i) Op) x (Op x)
toDualOpMltSld' :: forall (i :: * -> *) x (q :: (* -> *) -> *).
(Sliced i x, Multiplicative x) =>
q i -> Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x)
toDualOpMltSld' q i
_ = Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x)
forall (i :: * -> *) x.
(Sliced i x, Multiplicative x) =>
Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x)
toDualOpMltSld

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

-- HomSlicedDistributive -


-- | disjunctive distributive homomorphism respecting the slice structure.

type HomSlicedDistributive i h = (HomSlicedOriented i h, HomDistributiveDisjunctive h)

-- | contravariant isomorphism on 'Sliced' 'Distributive' structures. 

toDualOpDstSld :: (Sliced i x, Distributive x)
  => Variant2 Contravariant (IsoO (Dst,Sld i) Op) x (Op x)
toDualOpDstSld :: forall (i :: * -> *) x.
(Sliced i x, Distributive x) =>
Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
toDualOpDstSld = Struct (Dst, Sld i) x
-> Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO Struct (Dst, Sld i) x
forall s x. Structure s x => Struct s x
Struct

-- | contravariant isomorphism on 'Sliced' 'Distributive' structures according to the proxy type.

toDualOpDstSld' :: (Sliced i x, Distributive x)
  => q i -> Variant2 Contravariant (IsoO (Dst,Sld i) Op) x (Op x)
toDualOpDstSld' :: forall (i :: * -> *) x (q :: (* -> *) -> *).
(Sliced i x, Distributive x) =>
q i -> Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
toDualOpDstSld' q i
_  = Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
forall (i :: * -> *) x.
(Sliced i x, Distributive x) =>
Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
toDualOpDstSld