{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Adjunction.Limes
-- Description : mapping of limits under adjunctions
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- mapping of 'OAlg.Limes.Limits.Limits' under 'Adjunction's.
module OAlg.Adjunction.Limes
  (
    -- * Multiplicative
    lmPrjMap, lmInjMap
    
    -- * Distributive
  , lmPrjMapDst, lmInjMapDst

  ) where

import Data.Typeable

import OAlg.Prelude

import OAlg.Category.Dualisable
import OAlg.Category.SDuality

import OAlg.Data.Either
import OAlg.Data.Proxy

import OAlg.Entity.Diagram
import OAlg.Entity.FinList

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Distributive

import OAlg.Hom

import OAlg.Adjunction.Definition hiding (coAdjunctionOp)

import OAlg.Limes.Cone
import OAlg.Limes.Definition

--------------------------------------------------------------------------------
-- homDisjMlt -

homDisjMlt :: HomMultiplicative h => h x y -> Variant2 Covariant (HomDisj Mlt Op h) x y
homDisjMlt :: forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
homDisjMlt = h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
forall (h :: * -> * -> *) s x y (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (HomDisj s o h) x y
homDisj

--------------------------------------------------------------------------------
-- adjHomDisj' -

adjHomDisj' ::
  ( HomMultiplicative h
  , Transformable (ObjectClass h) s
  )
  => q s o -> Adjunction h x y -> Adjunction (Variant2 Covariant (HomDisj s o h)) x y
adjHomDisj' :: forall (h :: * -> * -> *) s (q :: * -> (* -> *) -> *) (o :: * -> *)
       x y.
(HomMultiplicative h, Transformable (ObjectClass h) s) =>
q s o
-> Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
adjHomDisj' q s o
_ = Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
forall (h :: * -> * -> *) s x y (o :: * -> *).
(HomMultiplicative h, Transformable (ObjectClass h) s) =>
Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
adjHomDisj

--------------------------------------------------------------------------------
-- lmPrjMap -

-- | blabla
--
-- @
--              l
--          <------- 
--        x          y
--          -------->
--              r
-- @
--
lmPrjMapGStruct ::
  ( NaturalConic h c s Projective d t n m
  , s ~ Mlt
  ) 
  => Struct s x
  -> Adjunction (Variant2 Covariant h) x y
  -> LimesG c s Projective d t n m x -> LimesG c s Projective d t n m y
lmPrjMapGStruct :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y.
(NaturalConic h c s 'Projective d t n m, s ~ Mlt) =>
Struct s x
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Projective d t n m x
-> LimesG c s 'Projective d t n m y
lmPrjMapGStruct Struct s x
Struct adj :: Adjunction (Variant2 'Covariant h) x y
adj@(Adjunction (Covariant2 h y x
l) (Covariant2 h x y
r) Point y -> y
_ Point x -> x
_)
  (LimesProjective c s 'Projective d t n m x
xLim Cone s 'Projective d t n m x -> x
xUniv) = c s 'Projective d t n m y
-> (Cone s 'Projective d t n m y -> y)
-> LimesG c s 'Projective d t n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective c s 'Projective d t n m y
yLim Cone s 'Projective d t n m y -> y
yUniv where

  xDgm :: d t n m x
xDgm     = Cone s 'Projective d t n m x -> d t n m x
Cone Mlt 'Projective d t n m x -> d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> d t n m a
diagrammaticObject (Cone s 'Projective d t n m x -> d t n m x)
-> Cone s 'Projective d t n m x -> d t n m x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c s 'Projective d t n m x -> Cone s 'Projective d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone c s 'Projective d t n m x
xLim
  xDgmPnts :: FinList n (Point x)
xDgmPnts = Diagram t n m x -> FinList n (Point x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints (Diagram t n m x -> FinList n (Point x))
-> Diagram t n m x -> FinList n (Point x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d t n m x -> Diagram t n m x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d t n m x
xDgm
  
  SDualBi (Right1 (ConeG c s 'Projective d t n m y
yLim)) = h x y
-> SDualBi (ConeG c Mlt 'Projective d t n m) x
-> SDualBi (ConeG c Mlt 'Projective d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
r (Either1
  (Dual1 (ConeG c s 'Projective d t n m))
  (ConeG c s 'Projective d t n m)
  x
-> SDualBi (ConeG c s 'Projective d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG c s 'Projective d t n m x
-> Either1
     (ConeG c Mlt 'Injective d (Dual t) n m)
     (ConeG c s 'Projective d t n m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (c s 'Projective d t n m x -> ConeG c s 'Projective d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
c s p d t n m x -> ConeG c s p d t n m x
ConeG c s 'Projective d t n m x
xLim)))

  yUniv :: Cone s 'Projective d t n m y -> y
yUniv (ConeProjective d t n m y
_ Point y
yTip FinList n y
fs) = Adjunction (Variant2 'Covariant h) x y -> Point y -> x -> y
forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point c -> d -> c
adjr Adjunction (Variant2 'Covariant h) x y
adj Point y
yTip (Cone s 'Projective d t n m x -> x
xUniv Cone s 'Projective d t n m x
Cone Mlt 'Projective d t n m x
xCn) where
    -- from ConeProjective _ cTip fs is valid, eligible and ajd is valid follows
    -- that xCn is valid and eligible!
    fs' :: FinList n x
fs'  = ((Point x, y) -> x) -> FinList n (Point x, y) -> FinList n x
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 ((Point x -> y -> x) -> (Point x, y) -> x
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Adjunction (Variant2 'Covariant h) x y -> Point x -> y -> x
forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point d -> c -> d
adjl Adjunction (Variant2 'Covariant h) x y
adj)) (FinList n (Point x)
xDgmPnts FinList n (Point x) -> FinList n y -> FinList n (Point x, y)
forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` FinList n y
fs)
    xCn :: Cone Mlt 'Projective d t n m x
xCn  = d t n m x
-> Point x -> FinList n x -> Cone Mlt 'Projective d t n m x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective d t n m x
xDgm (h y x -> Point y -> Point x
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h y x
l Point y
yTip) FinList n x
fs'

lmPrjMapStruct :: HomMultiplicative h
  => Struct Mlt d
  -> Adjunction h d c
  -> Limes Mlt Projective t n m d -> Limes Mlt Projective t n m c
lmPrjMapStruct :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicative h =>
Struct Mlt d
-> Adjunction h d c
-> Limes Mlt 'Projective t n m d
-> Limes Mlt 'Projective t n m c
lmPrjMapStruct Struct Mlt d
s Adjunction h d c
adj Limes Mlt 'Projective t n m d
l = case Limes Mlt 'Projective t n m d -> Dual (Dual t) :~: t
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d) =>
LimesG c s p d t n m x -> Dual (Dual t) :~: t
lmDiagramTypeRefl Limes Mlt 'Projective t n m d
l of
  Dual (Dual t) :~: t
Refl -> Struct Mlt d
-> Adjunction (Variant2 'Covariant (HomDisj Mlt Op h)) d c
-> Limes Mlt 'Projective t n m d
-> Limes Mlt 'Projective t n m c
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y.
(NaturalConic h c s 'Projective d t n m, s ~ Mlt) =>
Struct s x
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Projective d t n m x
-> LimesG c s 'Projective d t n m y
lmPrjMapGStruct Struct Mlt d
s (Proxy2 Mlt Op
-> Adjunction h d c
-> Adjunction (Variant2 'Covariant (HomDisj Mlt Op h)) d c
forall (h :: * -> * -> *) s (q :: * -> (* -> *) -> *) (o :: * -> *)
       x y.
(HomMultiplicative h, Transformable (ObjectClass h) s) =>
q s o
-> Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
adjHomDisj' (Proxy2 Mlt Op
forall {k} {k1} (a :: k) (b :: k1). Proxy2 a b
Proxy2 :: Proxy2 Mlt Op) Adjunction h d c
adj) Limes Mlt 'Projective t n m d
l 

{-

old implementation, keep it for the moment!!!!

lmPrjMapStruct Struct adj@(Adjunction l r _ _) (LimesProjective dLim dUniv)
  = LimesProjective cLim cUniv where

  dDgm = diagram $ diagrammaticObject dLim
  
  -- cLim = cnMap r dLim
  Covariant2 rCov = homDisjMlt r
  SDualBi (Right1 cLim) = case dgTypeRefl dDgm of Refl -> amapF rCov (SDualBi (Right1 dLim))
  
  cUniv (ConeProjective _ cTip fs) = adjr adj cTip (dUniv dCone) where
    -- from ConeProjective _ cTip fs is eligible and ajd is valid follows
    -- that dCone is eligible!
    dCone = ConeProjective dDgm (pmap l cTip) fs'
    fs' = amap1 (uncurry (adjl adj)) (dgPoints dDgm `zip` fs)
-}


-- | mapping a projective limes under an adjunction.
lmPrjMap :: HomMultiplicative h
  => Adjunction h d c -> Limes Mlt Projective t n m d -> Limes Mlt Projective t n m c
lmPrjMap :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicative h =>
Adjunction h d c
-> Limes Mlt 'Projective t n m d -> Limes Mlt 'Projective t n m c
lmPrjMap adj :: Adjunction h d c
adj@(Adjunction h c d
_ h d c
r Point c -> c
_ Point d -> d
_) = Struct Mlt d
-> Adjunction h d c
-> Limes Mlt 'Projective t n m d
-> Limes Mlt 'Projective t n m c
forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicative h =>
Struct Mlt d
-> Adjunction h d c
-> Limes Mlt 'Projective t n m d
-> Limes Mlt 'Projective t n m c
lmPrjMapStruct (Struct (ObjectClass h) d -> Struct Mlt d
forall x. Struct (ObjectClass h) x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (h d c -> Struct (ObjectClass h) d
forall x y. h x y -> Struct (ObjectClass h) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h d c
r)) Adjunction h d c
adj

--------------------------------------------------------------------------------
-- lmInjMap -

lmInjMapGStruct ::
  ( NaturalConic (Inv2 h) c s Injective d t n m
  , NaturalConic (Inv2 h) c s Projective d (Dual t) n m
  , NaturalConic h c s Projective d (Dual t) n m
  , s ~ Mlt
  )
  => Struct s y
  -> Variant2 Contravariant (Inv2 h) x (Op x)
  -> Variant2 Contravariant (Inv2 h) y (Op y)
  -> Adjunction (Variant2 Covariant h) x y
  -> LimesG c s Injective d t n m y -> LimesG c s Injective d t n m x
lmInjMapGStruct :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') y x.
(NaturalConic (Inv2 h) c s 'Injective d t n m,
 NaturalConic (Inv2 h) c s 'Projective d (Dual t) n m,
 NaturalConic h c s 'Projective d (Dual t) n m, s ~ Mlt) =>
Struct s y
-> Variant2 'Contravariant (Inv2 h) x (Op x)
-> Variant2 'Contravariant (Inv2 h) y (Op y)
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Injective d t n m y
-> LimesG c s 'Injective d t n m x
lmInjMapGStruct Struct s y
sy xOp :: Variant2 'Contravariant (Inv2 h) x (Op x)
xOp@(Contravariant2 Inv2 h x (Op x)
ixOp) yOp :: Variant2 'Contravariant (Inv2 h) y (Op y)
yOp@(Contravariant2 Inv2 h y (Op y)
iyOp) Adjunction (Variant2 'Covariant h) x y
adj LimesG c s 'Injective d t n m y
yLmInj = LimesG c s 'Injective d t n m x
xLmInj where
  adj' :: Adjunction (Variant2 'Covariant h) (Op y) (Op x)
adj'                    = Variant2 'Contravariant (Inv2 h) x (Op x)
-> Variant2 'Contravariant (Inv2 h) y (Op y)
-> Adjunction (Variant2 'Covariant h) x y
-> Adjunction (Variant2 'Covariant h) (Op y) (Op x)
forall (h :: * -> * -> *) x x' y y'.
FunctorialOriented h =>
Variant2 'Contravariant (Inv2 h) x x'
-> Variant2 'Contravariant (Inv2 h) y y'
-> Adjunction (Variant2 'Covariant h) x y
-> Adjunction (Variant2 'Covariant h) y' x'
adjMapCnt Variant2 'Contravariant (Inv2 h) x (Op x)
xOp Variant2 'Contravariant (Inv2 h) y (Op y)
yOp Adjunction (Variant2 'Covariant h) x y
adj  -- :: Adjunctin (Variant2 Covariant h) (Op y) (Op x)
  SDualBi (Left1 Dual1 (LimesG c Mlt 'Injective d t n m) (Op y)
yLmPrj') = Inv2 h y (Op y)
-> SDualBi (LimesG c Mlt 'Injective d t n m) y
-> SDualBi (LimesG c Mlt 'Injective d t n m) (Op y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 h y (Op y)
iyOp (Either1
  (Dual1 (LimesG c s 'Injective d t n m))
  (LimesG c s 'Injective d t n m)
  y
-> SDualBi (LimesG c s 'Injective d t n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s 'Injective d t n m y
-> Either1
     (LimesG c Mlt 'Projective d (Dual t) n m)
     (LimesG c s 'Injective d t n m)
     y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LimesG c s 'Injective d t n m y
yLmInj))
  xLmPrj' :: LimesG c s 'Projective d (Dual t) n m (Op x)
xLmPrj'                 = Struct s (Op y)
-> Adjunction (Variant2 'Covariant h) (Op y) (Op x)
-> LimesG c s 'Projective d (Dual t) n m (Op y)
-> LimesG c s 'Projective d (Dual t) n m (Op x)
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y.
(NaturalConic h c s 'Projective d t n m, s ~ Mlt) =>
Struct s x
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Projective d t n m x
-> LimesG c s 'Projective d t n m y
lmPrjMapGStruct (Struct s y -> Struct s (Op y)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct s y
sy) Adjunction (Variant2 'Covariant h) (Op y) (Op x)
adj' Dual1 (LimesG c Mlt 'Injective d t n m) (Op y)
LimesG c s 'Projective d (Dual t) n m (Op y)
yLmPrj'
  SDualBi (Right1 LimesG c s 'Injective d t n m x
xLmInj) = Inv2 h (Op x) x
-> SDualBi (LimesG c Mlt 'Injective d t n m) (Op x)
-> SDualBi (LimesG c Mlt 'Injective d t n m) x
forall x y.
Inv2 h x y
-> SDualBi (LimesG c Mlt 'Injective d t n m) x
-> SDualBi (LimesG c Mlt 'Injective d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Inv2 h x (Op x) -> Inv2 h (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x (Op x)
ixOp) (Either1
  (Dual1 (LimesG c Mlt 'Injective d t n m))
  (LimesG c Mlt 'Injective d t n m)
  (Op x)
-> SDualBi (LimesG c Mlt 'Injective d t n m) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s 'Projective d (Dual t) n m (Op x)
-> Either1
     (LimesG c s 'Projective d (Dual t) n m)
     (LimesG c Mlt 'Injective d t n m)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 LimesG c s 'Projective d (Dual t) n m (Op x)
xLmPrj'))

-- | mapping a injective limes under an adjunction.
lmInjMap :: HomMultiplicative h
  => Adjunction h d c -> Limes Mlt Injective t n m c -> Limes Mlt Injective t n m d
lmInjMap :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicative h =>
Adjunction h d c
-> Limes Mlt 'Injective t n m c -> Limes Mlt 'Injective t n m d
lmInjMap Adjunction h d c
adj Limes Mlt 'Injective t n m c
l = case Limes Mlt 'Injective t n m c -> Dual (Dual t) :~: t
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d) =>
LimesG c s p d t n m x -> Dual (Dual t) :~: t
lmDiagramTypeRefl Limes Mlt 'Injective t n m c
l of
  Dual (Dual t) :~: t
Refl -> Struct Mlt c
-> Variant2 'Contravariant (Inv2 (HomDisj Mlt Op h)) d (Op d)
-> Variant2 'Contravariant (Inv2 (HomDisj Mlt Op h)) c (Op c)
-> Adjunction (Variant2 'Covariant (HomDisj Mlt Op h)) d c
-> Limes Mlt 'Injective t n m c
-> Limes Mlt 'Injective t n m d
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') y x.
(NaturalConic (Inv2 h) c s 'Injective d t n m,
 NaturalConic (Inv2 h) c s 'Projective d (Dual t) n m,
 NaturalConic h c s 'Projective d (Dual t) n m, s ~ Mlt) =>
Struct s y
-> Variant2 'Contravariant (Inv2 h) x (Op x)
-> Variant2 'Contravariant (Inv2 h) y (Op y)
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Injective d t n m y
-> LimesG c s 'Injective d t n m x
lmInjMapGStruct Struct Mlt c
sc (Struct Mlt d
-> Variant2 'Contravariant (Inv2 (HomDisj Mlt Op h)) d (Op d)
forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj Struct Mlt d
sd) (Struct Mlt c
-> Variant2 'Contravariant (Inv2 (HomDisj Mlt Op h)) c (Op c)
forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj Struct Mlt c
sc) (Adjunction h d c
-> Adjunction (Variant2 'Covariant (HomDisj Mlt Op h)) d c
forall (h :: * -> * -> *) s x y (o :: * -> *).
(HomMultiplicative h, Transformable (ObjectClass h) s) =>
Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
adjHomDisj Adjunction h d c
adj) Limes Mlt 'Injective t n m c
l where
            Struct Mlt d
sd :>: Struct Mlt c
sc = Adjunction h d c -> Homomorphous Mlt d c
forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Homomorphous Mlt d c
adjHomMlt Adjunction h d c
adj

--------------------------------------------------------------------------------
-- lmPrjMapDst -

lmPrjMapDstGStruct ::
  ( HomDistributiveDisjunctive h
  , NaturalConic h c s Projective d t n m
  , s ~ Dst
  ) 
  => Struct s x
  -> Adjunction (Variant2 Covariant h) x y
  -> LimesG c s Projective d t n m x -> LimesG c s Projective d t n m y
lmPrjMapDstGStruct :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y.
(HomDistributiveDisjunctive h,
 NaturalConic h c s 'Projective d t n m, s ~ Dst) =>
Struct s x
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Projective d t n m x
-> LimesG c s 'Projective d t n m y
lmPrjMapDstGStruct Struct s x
Struct adj :: Adjunction (Variant2 'Covariant h) x y
adj@(Adjunction (Covariant2 h y x
_) (Covariant2 h x y
r) Point y -> y
_ Point x -> x
_)
  (LimesProjective c s 'Projective d t n m x
xLim Cone s 'Projective d t n m x -> x
xUniv) = c s 'Projective d t n m y
-> (Cone s 'Projective d t n m y -> y)
-> LimesG c s 'Projective d t n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective c s 'Projective d t n m y
yLim Cone s 'Projective d t n m y -> y
yUniv where

  xDgm :: d t n m x
xDgm     = Cone s 'Projective d t n m x -> d t n m x
Cone Dst 'Projective d t n m x -> d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> d t n m a
diagrammaticObject (Cone s 'Projective d t n m x -> d t n m x)
-> Cone s 'Projective d t n m x -> d t n m x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c s 'Projective d t n m x -> Cone s 'Projective d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone c s 'Projective d t n m x
xLim
  xDgmPnts :: FinList n (Point x)
xDgmPnts = Diagram t n m x -> FinList n (Point x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints (Diagram t n m x -> FinList n (Point x))
-> Diagram t n m x -> FinList n (Point x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d t n m x -> Diagram t n m x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d t n m x
xDgm
  
  SDualBi (Right1 (ConeG c s 'Projective d t n m y
yLim)) = h x y
-> SDualBi (ConeG c Dst 'Projective d t n m) x
-> SDualBi (ConeG c Dst 'Projective d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
r (Either1
  (Dual1 (ConeG c s 'Projective d t n m))
  (ConeG c s 'Projective d t n m)
  x
-> SDualBi (ConeG c s 'Projective d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG c s 'Projective d t n m x
-> Either1
     (ConeG c Dst 'Injective d (Dual t) n m)
     (ConeG c s 'Projective d t n m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (c s 'Projective d t n m x -> ConeG c s 'Projective d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
c s p d t n m x -> ConeG c s p d t n m x
ConeG c s 'Projective d t n m x
xLim)))

  yUniv :: Cone s 'Projective d t n m y -> y
yUniv (ConeKernel d ('Parallel 'LeftToRight) ('S N1) m y
_ y
f) = Adjunction (Variant2 'Covariant h) x y -> Point y -> x -> y
forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point c -> d -> c
adjr Adjunction (Variant2 'Covariant h) x y
adj Point y
yTip (Cone s 'Projective d t n m x -> x
xUniv Cone s 'Projective d t n m x
Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m x
xCn) where
    -- from ConeProjective _ cTip fs is valid, eligible and ajd is valid follows
    -- that xCn is valid and eligible!
    yTip :: Point y
yTip = y -> Point y
forall q. Oriented q => q -> Point q
start y
f 
    f' :: x
f'   = Adjunction (Variant2 'Covariant h) x y -> Point x -> y -> x
forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point d -> c -> d
adjl Adjunction (Variant2 'Covariant h) x y
adj (FinList (N1 + 1) (Point x) -> Point x
forall (n :: N') a. FinList (n + 1) a -> a
head FinList n (Point x)
FinList (N1 + 1) (Point x)
xDgmPnts) y
f
    xCn :: Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m x
xCn  = d ('Parallel 'LeftToRight) ('S N1) m x
-> x -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel d t n m x
d ('Parallel 'LeftToRight) ('S N1) m x
xDgm x
f'

{-
-- old implementation

lmPrjMapDstStruct :: Hom Dst h => Struct Dst d -> Adjunction h d c
  -> Limes Dst Projective t n m d -> Limes Dst Projective t n m c
lmPrjMapDstStruct Struct adj@(Adjunction _ r _ _)
  (LimesProjective dLim@(ConeKernel _ _) dUniv) = LimesProjective cLim cUniv where

  dDgm = cnDiagram dLim

  cLim = cnMap r dLim

  cUniv (ConeKernel _ x) = adjr adj (start x) (dUniv dCone) where
    dCone = ConeKernel dDgm (adjl adj (head $ dgPoints dDgm) x)
-}

lmPrjMapDstStruct :: HomDistributive h
  => Struct Dst d
  -> Adjunction h d c
  -> Limes Dst Projective t n m d -> Limes Dst Projective t n m c
lmPrjMapDstStruct :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
HomDistributive h =>
Struct Dst d
-> Adjunction h d c
-> Limes Dst 'Projective t n m d
-> Limes Dst 'Projective t n m c
lmPrjMapDstStruct Struct Dst d
s Adjunction h d c
adj Limes Dst 'Projective t n m d
l = case Limes Dst 'Projective t n m d -> Dual (Dual t) :~: t
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d) =>
LimesG c s p d t n m x -> Dual (Dual t) :~: t
lmDiagramTypeRefl Limes Dst 'Projective t n m d
l of
  Dual (Dual t) :~: t
Refl -> Struct Dst d
-> Adjunction (Variant2 'Covariant (HomDisj Dst Op h)) d c
-> Limes Dst 'Projective t n m d
-> Limes Dst 'Projective t n m c
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y.
(HomDistributiveDisjunctive h,
 NaturalConic h c s 'Projective d t n m, s ~ Dst) =>
Struct s x
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Projective d t n m x
-> LimesG c s 'Projective d t n m y
lmPrjMapDstGStruct Struct Dst d
s (Proxy2 Dst Op
-> Adjunction h d c
-> Adjunction (Variant2 'Covariant (HomDisj Dst Op h)) d c
forall (h :: * -> * -> *) s (q :: * -> (* -> *) -> *) (o :: * -> *)
       x y.
(HomMultiplicative h, Transformable (ObjectClass h) s) =>
q s o
-> Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
adjHomDisj' (Proxy2 Dst Op
forall {k} {k1} (a :: k) (b :: k1). Proxy2 a b
Proxy2 :: Proxy2 Dst Op) Adjunction h d c
adj) Limes Dst 'Projective t n m d
l

-- | mapping a projective limes under an adjunction.
lmPrjMapDst :: HomDistributive h
  => Adjunction h d c -> Limes Dst Projective t n m d -> Limes Dst Projective t n m c
lmPrjMapDst :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
HomDistributive h =>
Adjunction h d c
-> Limes Dst 'Projective t n m d -> Limes Dst 'Projective t n m c
lmPrjMapDst adj :: Adjunction h d c
adj@(Adjunction h c d
_ h d c
r Point c -> c
_ Point d -> d
_) = Struct Dst d
-> Adjunction h d c
-> Limes Dst 'Projective t n m d
-> Limes Dst 'Projective t n m c
forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
HomDistributive h =>
Struct Dst d
-> Adjunction h d c
-> Limes Dst 'Projective t n m d
-> Limes Dst 'Projective t n m c
lmPrjMapDstStruct (Struct (ObjectClass h) d -> Struct Dst d
forall x. Struct (ObjectClass h) x -> Struct Dst x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (h d c -> Struct (ObjectClass h) d
forall x y. h x y -> Struct (ObjectClass h) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h d c
r)) Adjunction h d c
adj 

--------------------------------------------------------------------------------
-- lmInjMapDst -

lmInjMapDstGStruct ::
  ( HomDistributiveDisjunctive h
  , NaturalConicBi (Inv2 h) c s Injective d t n m
  , NaturalConic h c s Projective d (Dual t) n m
  , s ~ Dst
  )
  => Struct s y
  -> Variant2 Contravariant (Inv2 h) x (Op x)
  -> Variant2 Contravariant (Inv2 h) y (Op y)
  -> Adjunction (Variant2 Covariant h) x y
  -> LimesG c s Injective d t n m y -> LimesG c s Injective d t n m x
lmInjMapDstGStruct :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') y x.
(HomDistributiveDisjunctive h,
 NaturalConicBi (Inv2 h) c s 'Injective d t n m,
 NaturalConic h c s 'Projective d (Dual t) n m, s ~ Dst) =>
Struct s y
-> Variant2 'Contravariant (Inv2 h) x (Op x)
-> Variant2 'Contravariant (Inv2 h) y (Op y)
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Injective d t n m y
-> LimesG c s 'Injective d t n m x
lmInjMapDstGStruct Struct s y
sy xOp :: Variant2 'Contravariant (Inv2 h) x (Op x)
xOp@(Contravariant2 Inv2 h x (Op x)
ixOp) yOp :: Variant2 'Contravariant (Inv2 h) y (Op y)
yOp@(Contravariant2 Inv2 h y (Op y)
iyOp) Adjunction (Variant2 'Covariant h) x y
adj LimesG c s 'Injective d t n m y
yLmInj = LimesG c s 'Injective d t n m x
xLmInj where
  adj' :: Adjunction (Variant2 'Covariant h) (Op y) (Op x)
adj'                    = Variant2 'Contravariant (Inv2 h) x (Op x)
-> Variant2 'Contravariant (Inv2 h) y (Op y)
-> Adjunction (Variant2 'Covariant h) x y
-> Adjunction (Variant2 'Covariant h) (Op y) (Op x)
forall (h :: * -> * -> *) x x' y y'.
FunctorialOriented h =>
Variant2 'Contravariant (Inv2 h) x x'
-> Variant2 'Contravariant (Inv2 h) y y'
-> Adjunction (Variant2 'Covariant h) x y
-> Adjunction (Variant2 'Covariant h) y' x'
adjMapCnt Variant2 'Contravariant (Inv2 h) x (Op x)
xOp Variant2 'Contravariant (Inv2 h) y (Op y)
yOp Adjunction (Variant2 'Covariant h) x y
adj  -- :: Adjunctin (Variant2 Covariant h) (Op y) (Op x)
  SDualBi (Left1 Dual1 (LimesG c Dst 'Injective d t n m) (Op y)
yLmPrj') = Inv2 h y (Op y)
-> SDualBi (LimesG c Dst 'Injective d t n m) y
-> SDualBi (LimesG c Dst 'Injective d t n m) (Op y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 h y (Op y)
iyOp (Either1
  (Dual1 (LimesG c s 'Injective d t n m))
  (LimesG c s 'Injective d t n m)
  y
-> SDualBi (LimesG c s 'Injective d t n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s 'Injective d t n m y
-> Either1
     (LimesG c Dst 'Projective d (Dual t) n m)
     (LimesG c s 'Injective d t n m)
     y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LimesG c s 'Injective d t n m y
yLmInj))
  xLmPrj' :: LimesG c s 'Projective d (Dual t) n m (Op x)
xLmPrj'                 = Struct s (Op y)
-> Adjunction (Variant2 'Covariant h) (Op y) (Op x)
-> LimesG c s 'Projective d (Dual t) n m (Op y)
-> LimesG c s 'Projective d (Dual t) n m (Op x)
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y.
(HomDistributiveDisjunctive h,
 NaturalConic h c s 'Projective d t n m, s ~ Dst) =>
Struct s x
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Projective d t n m x
-> LimesG c s 'Projective d t n m y
lmPrjMapDstGStruct (Struct s y -> Struct s (Op y)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct s y
sy) Adjunction (Variant2 'Covariant h) (Op y) (Op x)
adj' Dual1 (LimesG c Dst 'Injective d t n m) (Op y)
LimesG c s 'Projective d (Dual t) n m (Op y)
yLmPrj'
  SDualBi (Right1 LimesG c s 'Injective d t n m x
xLmInj) = Inv2 h (Op x) x
-> SDualBi (LimesG c Dst 'Injective d t n m) (Op x)
-> SDualBi (LimesG c Dst 'Injective d t n m) x
forall x y.
Inv2 h x y
-> SDualBi (LimesG c Dst 'Injective d t n m) x
-> SDualBi (LimesG c Dst 'Injective d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Inv2 h x (Op x) -> Inv2 h (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x (Op x)
ixOp) (Either1
  (Dual1 (LimesG c Dst 'Injective d t n m))
  (LimesG c Dst 'Injective d t n m)
  (Op x)
-> SDualBi (LimesG c Dst 'Injective d t n m) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s 'Projective d (Dual t) n m (Op x)
-> Either1
     (LimesG c s 'Projective d (Dual t) n m)
     (LimesG c Dst 'Injective d t n m)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 LimesG c s 'Projective d (Dual t) n m (Op x)
xLmPrj'))

-- | mapping an injective limes according to a given 'Adjunction'.
lmInjMapDst :: HomDistributive h
  => Adjunction h d c -> Limes Dst Injective t n m c -> Limes Dst Injective t n m d
lmInjMapDst :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
HomDistributive h =>
Adjunction h d c
-> Limes Dst 'Injective t n m c -> Limes Dst 'Injective t n m d
lmInjMapDst Adjunction h d c
adj Limes Dst 'Injective t n m c
l = case Limes Dst 'Injective t n m c -> Dual (Dual t) :~: t
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d) =>
LimesG c s p d t n m x -> Dual (Dual t) :~: t
lmDiagramTypeRefl Limes Dst 'Injective t n m c
l of
  Dual (Dual t) :~: t
Refl -> Struct Dst c
-> Variant2 'Contravariant (Inv2 (HomDisj Dst Op h)) d (Op d)
-> Variant2 'Contravariant (Inv2 (HomDisj Dst Op h)) c (Op c)
-> Adjunction (Variant2 'Covariant (HomDisj Dst Op h)) d c
-> Limes Dst 'Injective t n m c
-> Limes Dst 'Injective t n m d
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') y x.
(HomDistributiveDisjunctive h,
 NaturalConicBi (Inv2 h) c s 'Injective d t n m,
 NaturalConic h c s 'Projective d (Dual t) n m, s ~ Dst) =>
Struct s y
-> Variant2 'Contravariant (Inv2 h) x (Op x)
-> Variant2 'Contravariant (Inv2 h) y (Op y)
-> Adjunction (Variant2 'Covariant h) x y
-> LimesG c s 'Injective d t n m y
-> LimesG c s 'Injective d t n m x
lmInjMapDstGStruct Struct Dst c
sc (Struct Dst d
-> Variant2 'Contravariant (Inv2 (HomDisj Dst Op h)) d (Op d)
forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj Struct Dst d
sd) (Struct Dst c
-> Variant2 'Contravariant (Inv2 (HomDisj Dst Op h)) c (Op c)
forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj Struct Dst c
sc) (Adjunction h d c
-> Adjunction (Variant2 'Covariant (HomDisj Dst Op h)) d c
forall (h :: * -> * -> *) s x y (o :: * -> *).
(HomMultiplicative h, Transformable (ObjectClass h) s) =>
Adjunction h x y
-> Adjunction (Variant2 'Covariant (HomDisj s o h)) x y
adjHomDisj Adjunction h d c
adj) Limes Dst 'Injective t n m c
l where
            Struct Dst d
sd :>: Struct Dst c
sc = Adjunction h d c -> Homomorphous Dst d c
forall (h :: * -> * -> *) d c.
HomDistributive h =>
Adjunction h d c -> Homomorphous Dst d c
adjHomDst Adjunction h d c
adj