{-# LANGUAGE NoImplicitPrelude #-}

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

{-# LANGUAGE RankNTypes, PolyKinds #-}


-- |

-- Module      : OAlg.Entity.Slice.Liftable

-- Description : liftable slices.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- liftable slices.

module OAlg.Entity.Slice.Liftable
  (

    -- * Liftables

    Liftable(..), lift, lftbBase
  , lftMapS, lftMapCov, lftMapCnt
  -- , LiftableStruct(..)

  
    -- * Limes

    -- ** Cone

  , LiftableCone(..), lftcLiftable
  , lftcMapS, lftcMapCov, lftcMapCnt
  
    -- ** Kernel

  , LiftableKernels, LiftableKernel
  , lftlKernel
  
    -- ** Cokernel

  , LiftableCokernels, LiftableCokernel
  , lftlCokernel

    -- * Proposition

  , relLiftable

    -- * Exception

  , LiftableException(..)

  ) where

import Control.Monad

import Data.Typeable

import OAlg.Prelude

import OAlg.Category.SDuality
import OAlg.Category.NaturalTransformable

import OAlg.Data.Either
import OAlg.Data.Singleton

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative as M
import OAlg.Structure.Distributive

import OAlg.Hom.Oriented

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

import OAlg.Entity.Natural hiding ((++))
import OAlg.Entity.Diagram

import OAlg.Entity.Slice.Sliced
import OAlg.Entity.Slice.Definition

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

-- LiftableException -


-- | liftable exceptions which are sub exceptions of 'SomeOAlgException'.

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

instance Exception LiftableException where
  toException :: LiftableException -> SomeException
toException   = LiftableException -> SomeException
forall e. Exception e => e -> SomeException
oalgExceptionToException
  fromException :: SomeException -> Maybe LiftableException
fromException = SomeException -> Maybe LiftableException
forall e. Exception e => SomeException -> Maybe e
oalgExceptionFromException

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

-- Liftable -


-- | liftable slices.

--

-- __Property__ Let @l@ be in @'Liftable' __p i x__@ for an @__i__@-sliced 'Multiplicative'

-- structure @__x__@, then holds:

--

-- (1) If @l@ matches @'LiftableProjective' x lft@, then holds:

-- For all @t@ in @'Slice' 'To' __i x__@ holds:

--

--     (1) If @'start' x '/=' 'start' ('slice' t)@ then the evaluation of @lft t@ ends up in a

--     'NotLiftable'-exception.

--

--     (2) If @'start' x '==' 'start' ('slice' t)@ then holds: Let @t' = lft t@ in

--

--         (1) @t'@ is 'valid'.

--

--         (2) @'start' ('slice' t') '==' 'end' x@,

--

--         (3) @'slice' t '==' 'slice' t' 'OAlg.Structure.Multiplicative.Definition.*' x@.

--

-- (2) If @l@ matches @'LiftableInjective' x lft@, then holds:

-- For all @f@ in @'Slice' 'From' __i x__@ holds:

--

--     (1) If @'end' x '/=' 'end' ('slice' f)@ then the evaluation of @lft f@ ends up in a

--     'NotLiftable'-exception.

--

--     (2) If @'end' x '==' 'end' ('slice' f)@, then holds: Let @f' = lft f@ in

--

--         (1) @f'@ is 'valid'.

--

--         (2) @'end' ('slice' f') '==' 'start' x@.

--

--         (3) @'slice' f '==' x 'OAlg.Structure.Multiplicative.Definition.*' 'slice' f'@.

--

data Liftable p i x where
  LiftableProjective :: Sliced i x => x -> (Slice To i x -> Slice To i x) -> Liftable Projective i x
  LiftableInjective  :: Sliced i x => x -> (Slice From i x -> Slice From i x) -> Liftable Injective i x

instance Show x => Show (Liftable s i x) where
  show :: Liftable s i x -> String
show (LiftableProjective x
x Slice 'To i x -> Slice 'To i x
_) = [String] -> String
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join [String
"LiftableProjective (",x -> String
forall a. Show a => a -> String
show x
x,String
") lft"]
  show (LiftableInjective x
x Slice 'From i x -> Slice 'From i x
_)  = [String] -> String
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join [String
"LiftableInjective (",x -> String
forall a. Show a => a -> String
show x
x,String
") lft"]

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

-- lftMapCov -


lftMapCovStruct :: (CategoryDisjunctive h, HomSlicedMultiplicative i h)
  => Struct (Sld i) y -> Variant2 Covariant (Inv2 h) x y -> Liftable p i x -> Liftable p i y
lftMapCovStruct :: forall (h :: * -> * -> *) (i :: * -> *) y x (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Struct (Sld i) y
-> Variant2 'Covariant (Inv2 h) x y
-> Liftable p i x
-> Liftable p i y
lftMapCovStruct Struct (Sld i) y
Struct (Covariant2 Inv2 h x y
i) (LiftableProjective x
x Slice 'To i x -> Slice 'To i x
xLft) = y -> (Slice 'To i y -> Slice 'To i y) -> Liftable 'Projective i y
forall (i :: * -> *) x.
Sliced i x =>
x -> (Slice 'To i x -> Slice 'To i x) -> Liftable 'Projective i x
LiftableProjective y
y Slice 'To i y -> Slice 'To i y
yLft where
  y :: y
y    = Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Inv2 h x y
i x
x
  yLft :: Slice 'To i y -> Slice 'To i y
yLft = Variant2 'Covariant (Inv2 h) x y -> Slice 'To i x -> Slice 'To i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov (Inv2 h x y -> Variant2 'Covariant (Inv2 h) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 Inv2 h x y
i) (Slice 'To i x -> Slice 'To i y)
-> (Slice 'To i y -> Slice 'To i x)
-> Slice 'To i y
-> Slice 'To i 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
. Slice 'To i x -> Slice 'To i x
xLft (Slice 'To i x -> Slice 'To i x)
-> (Slice 'To i y -> Slice 'To i x)
-> Slice 'To i y
-> Slice 'To i 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
. Variant2 'Covariant (Inv2 h) y x -> Slice 'To i y -> Slice 'To i x
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov (Inv2 h y x -> Variant2 'Covariant (Inv2 h) y x
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (Inv2 h y x -> Variant2 'Covariant (Inv2 h) y x)
-> Inv2 h y x -> Variant2 'Covariant (Inv2 h) y x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i)
lftMapCovStruct Struct (Sld i) y
Struct (Covariant2 Inv2 h x y
i) (LiftableInjective x
x Slice 'From i x -> Slice 'From i x
xLft) = y
-> (Slice 'From i y -> Slice 'From i y) -> Liftable 'Injective i y
forall (i :: * -> *) x.
Sliced i x =>
x
-> (Slice 'From i x -> Slice 'From i x) -> Liftable 'Injective i x
LiftableInjective y
y Slice 'From i y -> Slice 'From i y
yLft where
  y :: y
y    = Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Inv2 h x y
i x
x
  yLft :: Slice 'From i y -> Slice 'From i y
yLft = Variant2 'Covariant (Inv2 h) x y
-> Slice 'From i x -> Slice 'From i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov (Inv2 h x y -> Variant2 'Covariant (Inv2 h) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 Inv2 h x y
i) (Slice 'From i x -> Slice 'From i y)
-> (Slice 'From i y -> Slice 'From i x)
-> Slice 'From i y
-> Slice 'From i 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
. Slice 'From i x -> Slice 'From i x
xLft (Slice 'From i x -> Slice 'From i x)
-> (Slice 'From i y -> Slice 'From i x)
-> Slice 'From i y
-> Slice 'From i 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
. Variant2 'Covariant (Inv2 h) y x
-> Slice 'From i y -> Slice 'From i x
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov (Inv2 h y x -> Variant2 'Covariant (Inv2 h) y x
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (Inv2 h y x -> Variant2 'Covariant (Inv2 h) y x)
-> Inv2 h y x -> Variant2 'Covariant (Inv2 h) y x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i)

-- | covariant mapping of 'Liftable'.

lftMapCov :: (CategoryDisjunctive h, HomSlicedMultiplicative i h)
  => Variant2 Covariant (Inv2 h) x y -> Liftable p i x -> Liftable p i y
lftMapCov :: forall (h :: * -> * -> *) (i :: * -> *) x y (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Variant2 'Covariant (Inv2 h) x y
-> Liftable p i x -> Liftable p i y
lftMapCov Variant2 'Covariant (Inv2 h) x y
h = Struct (Sld i) y
-> Variant2 'Covariant (Inv2 h) x y
-> Liftable p i x
-> Liftable p i y
forall (h :: * -> * -> *) (i :: * -> *) y x (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Struct (Sld i) y
-> Variant2 'Covariant (Inv2 h) x y
-> Liftable p i x
-> Liftable p i y
lftMapCovStruct (Struct (ObjectClass h) y -> Struct (Sld i) y
forall x. Struct (ObjectClass h) x -> Struct (Sld i) x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Variant2 'Covariant (Inv2 h) x y
-> Struct (ObjectClass (Variant2 'Covariant (Inv2 h))) y
forall x y.
Variant2 'Covariant (Inv2 h) x y
-> Struct (ObjectClass (Variant2 'Covariant (Inv2 h))) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Covariant (Inv2 h) x y
h)) Variant2 'Covariant (Inv2 h) x y
h

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

-- lftMapCnt -


lftMapCntStruct :: (CategoryDisjunctive h, HomSlicedMultiplicative i h)
  => Struct (Sld i) y -> Variant2 Contravariant (Inv2 h) x y -> Liftable p i x -> Liftable (Dual p) i y
lftMapCntStruct :: forall (h :: * -> * -> *) (i :: * -> *) y x (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Struct (Sld i) y
-> Variant2 'Contravariant (Inv2 h) x y
-> Liftable p i x
-> Liftable (Dual p) i y
lftMapCntStruct Struct (Sld i) y
Struct (Contravariant2 Inv2 h x y
i) (LiftableProjective x
x Slice 'To i x -> Slice 'To i x
xLft) = y
-> (Slice 'From i y -> Slice 'From i y) -> Liftable 'Injective i y
forall (i :: * -> *) x.
Sliced i x =>
x
-> (Slice 'From i x -> Slice 'From i x) -> Liftable 'Injective i x
LiftableInjective y
y Slice 'From i y -> Slice 'From i y
Slice 'From i y -> Slice (Dual 'To) i y
yLft where
  y :: y
y    = Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Inv2 h x y
i x
x
  yLft :: Slice 'From i y -> Slice (Dual 'To) i y
yLft = Variant2 'Contravariant (Inv2 h) x y
-> Slice 'To i x -> Slice (Dual 'To) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt (Inv2 h x y -> Variant2 'Contravariant (Inv2 h) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 Inv2 h x y
i) (Slice 'To i x -> Slice (Dual 'To) i y)
-> (Slice 'From i y -> Slice 'To i x)
-> Slice 'From i y
-> Slice (Dual 'To) i 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
. Slice 'To i x -> Slice 'To i x
xLft (Slice 'To i x -> Slice 'To i x)
-> (Slice 'From i y -> Slice 'To i x)
-> Slice 'From i y
-> Slice 'To i 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
. Variant2 'Contravariant (Inv2 h) y x
-> Slice 'From i y -> Slice (Dual 'From) i x
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt (Inv2 h y x -> Variant2 'Contravariant (Inv2 h) y x
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (Inv2 h y x -> Variant2 'Contravariant (Inv2 h) y x)
-> Inv2 h y x -> Variant2 'Contravariant (Inv2 h) y x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i)
lftMapCntStruct Struct (Sld i) y
Struct (Contravariant2 Inv2 h x y
i) (LiftableInjective x
x Slice 'From i x -> Slice 'From i x
xLft) = y -> (Slice 'To i y -> Slice 'To i y) -> Liftable 'Projective i y
forall (i :: * -> *) x.
Sliced i x =>
x -> (Slice 'To i x -> Slice 'To i x) -> Liftable 'Projective i x
LiftableProjective y
y Slice 'To i y -> Slice 'To i y
Slice 'To i y -> Slice (Dual 'From) i y
yLft where
  y :: y
y    = Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Inv2 h x y
i x
x
  yLft :: Slice 'To i y -> Slice (Dual 'From) i y
yLft = Variant2 'Contravariant (Inv2 h) x y
-> Slice 'From i x -> Slice (Dual 'From) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt (Inv2 h x y -> Variant2 'Contravariant (Inv2 h) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 Inv2 h x y
i) (Slice 'From i x -> Slice (Dual 'From) i y)
-> (Slice 'To i y -> Slice 'From i x)
-> Slice 'To i y
-> Slice (Dual 'From) i 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
. Slice 'From i x -> Slice 'From i x
xLft (Slice 'From i x -> Slice 'From i x)
-> (Slice 'To i y -> Slice 'From i x)
-> Slice 'To i y
-> Slice 'From i 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
. Variant2 'Contravariant (Inv2 h) y x
-> Slice 'To i y -> Slice (Dual 'To) i x
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt (Inv2 h y x -> Variant2 'Contravariant (Inv2 h) y x
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (Inv2 h y x -> Variant2 'Contravariant (Inv2 h) y x)
-> Inv2 h y x -> Variant2 'Contravariant (Inv2 h) y x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i)

-- | contravariant mapping of 'Liftable'.

lftMapCnt :: (CategoryDisjunctive h, HomSlicedMultiplicative i h)
  => Variant2 Contravariant (Inv2 h) x y -> Liftable p i x -> Liftable (Dual p) i y
lftMapCnt :: forall (h :: * -> * -> *) (i :: * -> *) x y (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Variant2 'Contravariant (Inv2 h) x y
-> Liftable p i x -> Liftable (Dual p) i y
lftMapCnt Variant2 'Contravariant (Inv2 h) x y
h = Struct (Sld i) y
-> Variant2 'Contravariant (Inv2 h) x y
-> Liftable p i x
-> Liftable (Dual p) i y
forall (h :: * -> * -> *) (i :: * -> *) y x (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Struct (Sld i) y
-> Variant2 'Contravariant (Inv2 h) x y
-> Liftable p i x
-> Liftable (Dual p) i y
lftMapCntStruct (Struct (ObjectClass h) y -> Struct (Sld i) y
forall x. Struct (ObjectClass h) x -> Struct (Sld i) x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Variant2 'Contravariant (Inv2 h) x y
-> Struct (ObjectClass (Variant2 'Contravariant (Inv2 h))) y
forall x y.
Variant2 'Contravariant (Inv2 h) x y
-> Struct (ObjectClass (Variant2 'Contravariant (Inv2 h))) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Contravariant (Inv2 h) x y
h)) Variant2 'Contravariant (Inv2 h) x y
h

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

-- Duality -


type instance Dual1 (Liftable p i) = Liftable (Dual p) i

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

-- lftMapS -


-- | mapping of 'Liftable'.

lftMapS :: (CategoryDisjunctive h, HomSlicedMultiplicative i h, p ~ Dual (Dual p))
  => Inv2 h x y -> SDualBi (Liftable p i) x -> SDualBi (Liftable p i) y
lftMapS :: forall (h :: * -> * -> *) (i :: * -> *) (p :: Perspective) x y.
(CategoryDisjunctive h, HomSlicedMultiplicative i h,
 p ~ Dual (Dual p)) =>
Inv2 h x y -> SDualBi (Liftable p i) x -> SDualBi (Liftable p i) y
lftMapS = (Variant2 'Covariant (Inv2 h) x y
 -> Liftable p i x -> Liftable p i y)
-> (Variant2 'Covariant (Inv2 h) x y
    -> Dual1 (Liftable p i) x -> Dual1 (Liftable p i) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> Liftable p i x -> Dual1 (Liftable p i) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> Dual1 (Liftable p i) x -> Liftable p i y)
-> Inv2 h x y
-> SDualBi (Liftable p i) x
-> SDualBi (Liftable p i) y
forall (h :: * -> * -> *) x y (d :: * -> *).
Disjunctive2 h =>
(Variant2 'Covariant h x y -> d x -> d y)
-> (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> Dual1 d x -> d y)
-> h x y
-> SDualBi d x
-> SDualBi d y
vmapBi Variant2 'Covariant (Inv2 h) x y
-> Liftable p i x -> Liftable p i y
forall (h :: * -> * -> *) (i :: * -> *) x y (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Variant2 'Covariant (Inv2 h) x y
-> Liftable p i x -> Liftable p i y
lftMapCov Variant2 'Covariant (Inv2 h) x y
-> Dual1 (Liftable p i) x -> Dual1 (Liftable p i) y
Variant2 'Covariant (Inv2 h) x y
-> Liftable (Dual p) i x -> Liftable (Dual p) i y
forall (h :: * -> * -> *) (i :: * -> *) x y (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Variant2 'Covariant (Inv2 h) x y
-> Liftable p i x -> Liftable p i y
lftMapCov Variant2 'Contravariant (Inv2 h) x y
-> Liftable p i x -> Dual1 (Liftable p i) y
Variant2 'Contravariant (Inv2 h) x y
-> Liftable p i x -> Liftable (Dual p) i y
forall (h :: * -> * -> *) (i :: * -> *) x y (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Variant2 'Contravariant (Inv2 h) x y
-> Liftable p i x -> Liftable (Dual p) i y
lftMapCnt Variant2 'Contravariant (Inv2 h) x y
-> Dual1 (Liftable p i) x -> Liftable p i y
Variant2 'Contravariant (Inv2 h) x y
-> Liftable (Dual p) i x -> Liftable (Dual (Dual p)) i y
forall (h :: * -> * -> *) (i :: * -> *) x y (p :: Perspective).
(CategoryDisjunctive h, HomSlicedMultiplicative i h) =>
Variant2 'Contravariant (Inv2 h) x y
-> Liftable p i x -> Liftable (Dual p) i y
lftMapCnt

instance (CategoryDisjunctive h, HomSlicedMultiplicative i h, p ~ Dual (Dual p))
  => ApplicativeG (SDualBi (Liftable p i)) (Inv2 h) (->) where
  amapG :: forall x y.
Inv2 h x y -> SDualBi (Liftable p i) x -> SDualBi (Liftable p i) y
amapG = Inv2 h x y -> SDualBi (Liftable p i) x -> SDualBi (Liftable p i) y
forall (h :: * -> * -> *) (i :: * -> *) (p :: Perspective) x y.
(CategoryDisjunctive h, HomSlicedMultiplicative i h,
 p ~ Dual (Dual p)) =>
Inv2 h x y -> SDualBi (Liftable p i) x -> SDualBi (Liftable p i) y
lftMapS

instance (CategoryDisjunctive h, HomSlicedMultiplicative i h, p ~ Dual (Dual p))
  => FunctorialG (SDualBi (Liftable p i)) (Inv2 h) (->)


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

-- Liftable - Valid -


relLiftableProjective :: Multiplicative x
  => i x -> XOrtOrientation x -> Liftable Projective i x -> Statement
relLiftableProjective :: forall x (i :: * -> *).
Multiplicative x =>
i x -> XOrtOrientation x -> Liftable 'Projective i x -> Statement
relLiftableProjective i x
i XOrtOrientation x
xo (LiftableProjective x
x Slice 'To i x -> Slice 'To i x
lft)
  = [Statement] -> Statement
And [ x -> Statement
forall a. Validable a => a -> Statement
valid x
x        
        , X (Slice 'To i x) -> (Slice 'To i x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Slice 'To i x)
xt (\Slice 'To i x
t
            -> [Statement] -> Statement
And [ Slice 'To i x -> Statement
forall a. Validable a => a -> Statement
valid Slice 'To i x
t
                   , let t' :: Slice 'To i x
t' = Slice 'To i x -> Slice 'To i x
lft Slice 'To i x
t in case x -> Point x
forall q. Oriented q => q -> Point q
start x
x Point x -> Point x -> Bool
forall a. Eq a => a -> a -> Bool
== x -> Point x
forall q. Oriented q => q -> Point q
start (Slice 'To i x -> x
forall (s :: Site) (i :: * -> *) x. Slice s i x -> x
slice Slice 'To i x
t) of
                       Bool
False -> String -> Label
Label String
"1.1" Label -> Statement -> Statement
:<=>: (Slice 'To i x -> Statement
forall a. Validable a => a -> Statement
valid Slice 'To i x
t' Statement -> Statement -> Statement
:=> AlgebraicException -> Statement
forall a e. Exception e => e -> a
throw AlgebraicException
implError)
                                  Statement -> (LiftableException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` (\LiftableException
e -> case LiftableException
e of LiftableException
NotLiftable -> Statement
SValid)
                                       
                       Bool
True  -> [Statement] -> Statement
And [ String -> Label
Label String
"1.2.1" Label -> Statement -> Statement
:<=>: Slice 'To i x -> Statement
forall a. Validable a => a -> Statement
valid Slice 'To i x
t'
                                    , String -> Label
Label String
"1.2.2" Label -> Statement -> Statement
:<=>: (x -> Point x
forall q. Oriented q => q -> Point q
start (Slice 'To i x -> x
forall (s :: Site) (i :: * -> *) x. Slice s i x -> x
slice Slice 'To i x
t') Point x -> Point x -> Bool
forall a. Eq a => a -> a -> Bool
== x -> Point x
forall q. Oriented q => q -> Point q
end x
x)
                                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x,String
"t"String -> String -> Parameter
:=Slice 'To i x -> String
forall a. Show a => a -> String
show Slice 'To i x
t,String
"t'"String -> String -> Parameter
:=Slice 'To i x -> String
forall a. Show a => a -> String
show Slice 'To i x
t']
                                    , String -> Label
Label String
"1.2.3" Label -> Statement -> Statement
:<=>: (Slice 'To i x -> x
forall (s :: Site) (i :: * -> *) x. Slice s i x -> x
slice Slice 'To i x
t x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== Slice 'To i x -> x
forall (s :: Site) (i :: * -> *) x. Slice s i x -> x
slice Slice 'To i x
t' x -> x -> x
forall c. Multiplicative c => c -> c -> c
* x
x)
                                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x,String
"t"String -> String -> Parameter
:=Slice 'To i x -> String
forall a. Show a => a -> String
show Slice 'To i x
t,String
"t'"String -> String -> Parameter
:=Slice 'To i x -> String
forall a. Show a => a -> String
show Slice 'To i x
t']
                                    ]

                   ]
                    )

        ]
    
  where implError :: AlgebraicException
implError = String -> AlgebraicException
ImplementationError String
"unliftable dos not throw a NotLiftable-exception"
        ip :: Point x
ip = i x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i x
i
  
        xt :: X (Slice 'To i x)
xt = (x -> Slice 'To i x) -> X x -> X (Slice 'To i x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (i x -> x -> Slice 'To i x
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i x
i)
           (X x -> X (Slice 'To i x)) -> X x -> X (Slice 'To i x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Q, X x)] -> X x
forall a. [(Q, X a)] -> X a
xOneOfXW [ (Q
9,XOrtOrientation x -> Orientation (Point x) -> X x
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation x
xo (x -> Point x
forall q. Oriented q => q -> Point q
start x
x Point x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:> Point x
ip))
                      , (Q
1,XOrtOrientation x -> X (Point x)
forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint XOrtOrientation x
xo X (Point x) -> (Point x -> X x) -> X x
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= XOrtOrientation x -> Orientation (Point x) -> X x
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation x
xo (Orientation (Point x) -> X x)
-> (Point x -> Orientation (Point x)) -> Point x -> 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
. (Point x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:>Point x
ip))
                      ]

-- | validity accroding to 'Liftable'.

relLiftable :: Multiplicative x => XOrtOrientation x -> Liftable p i x -> Statement
relLiftable :: forall x (p :: Perspective) (i :: * -> *).
Multiplicative x =>
XOrtOrientation x -> Liftable p i x -> Statement
relLiftable XOrtOrientation x
xo Liftable p i x
l = case Liftable p i x
l of
  LiftableProjective x
_ Slice 'To i x -> Slice 'To i x
_ -> i x -> XOrtOrientation x -> Liftable 'Projective i x -> Statement
forall x (i :: * -> *).
Multiplicative x =>
i x -> XOrtOrientation x -> Liftable 'Projective i x -> Statement
relLiftableProjective i x
forall x. i x
forall (s :: * -> *) x. Singleton1 s => s x
unit1 XOrtOrientation x
xo Liftable p i x
Liftable 'Projective i x
l
  LiftableInjective x
_ Slice 'From i x -> Slice 'From i x
_  -> XOrtOrientation (Op x)
-> Liftable 'Projective i (Op x) -> Statement
forall x (p :: Perspective) (i :: * -> *).
Multiplicative x =>
XOrtOrientation x -> Liftable p i x -> Statement
relLiftable (XOrtOrientation x -> Dual (XOrtOrientation x)
forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation x
xo) Dual1 (Liftable 'Injective i) (Op x)
Liftable 'Projective i (Op x)
l' where
    Contravariant2 Inv2 (HomDisjEmpty (Mlt, Sld i) Op) x (Op x)
i = Proxy i
-> Variant2
     'Contravariant (Inv2 (HomDisjEmpty (Mlt, Sld i) Op)) x (Op x)
forall (i :: * -> *) x (q :: (* -> *) -> *).
(Sliced i x, Multiplicative x) =>
q i -> Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x)
toDualOpMltSld' (Liftable p i x -> Proxy i
forall (p :: Perspective) (i :: * -> *) x.
Liftable p i x -> Proxy i
q Liftable p i x
l)
    SDualBi (Left1 Dual1 (Liftable 'Injective i) (Op x)
l') = Inv2 (HomDisjEmpty (Mlt, Sld i) Op) x (Op x)
-> SDualBi (Liftable 'Injective i) x
-> SDualBi (Liftable 'Injective i) (Op x)
forall x y.
Inv2 (HomDisjEmpty (Mlt, Sld i) Op) x y
-> SDualBi (Liftable 'Injective i) x
-> SDualBi (Liftable 'Injective i) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 (HomDisjEmpty (Mlt, Sld i) Op) x (Op x)
i (Either1 (Dual1 (Liftable p i)) (Liftable p i) x
-> SDualBi (Liftable p i) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Liftable p i x -> Either1 (Liftable 'Projective i) (Liftable p i) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Liftable p i x
l))

    q :: Liftable p i x -> Proxy i
    q :: forall (p :: Perspective) (i :: * -> *) x.
Liftable p i x -> Proxy i
q Liftable p i x
_ = Proxy i
forall {k} (t :: k). Proxy t
Proxy
    

instance (Multiplicative x, XStandardOrtOrientation x)
  => Validable (Liftable s i x) where
  valid :: Liftable s i x -> Statement
valid Liftable s i x
l = String -> Label
Label String
"Liftable" Label -> Statement -> Statement
:<=>: XOrtOrientation x -> Liftable s i x -> Statement
forall x (p :: Perspective) (i :: * -> *).
Multiplicative x =>
XOrtOrientation x -> Liftable p i x -> Statement
relLiftable XOrtOrientation x
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation Liftable s i x
l
                                      
--------------------------------------------------------------------------------

-- lftbBase -


-- | the underlying factor.

lftbBase :: Liftable s i x -> x
lftbBase :: forall (s :: Perspective) (i :: * -> *) x. Liftable s i x -> x
lftbBase (LiftableProjective x
x Slice 'To i x -> Slice 'To i x
_) = x
x
lftbBase (LiftableInjective x
x Slice 'From i x -> Slice 'From i x
_)  = x
x

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

-- lift -


-- | the lifting map.

lift :: Liftable p i x -> Slice (ToSite p) i x -> Slice (ToSite p) i x
lift :: forall (p :: Perspective) (i :: * -> *) x.
Liftable p i x -> Slice (ToSite p) i x -> Slice (ToSite p) i x
lift (LiftableProjective x
_ Slice 'To i x -> Slice 'To i x
l) = Slice (ToSite p) i x -> Slice (ToSite p) i x
Slice 'To i x -> Slice 'To i x
l
lift (LiftableInjective x
_ Slice 'From i x -> Slice 'From i x
l)  = Slice (ToSite p) i x -> Slice (ToSite p) i x
Slice 'From i x -> Slice 'From i x
l

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

-- LiftableCone -


-- | kernel respectively cokernel cones with a liftable factor.

--

-- __Property__ Let @c@ be in @'LiftableCone' __i s p d t n m x__@ for a

-- 'Distributive' structure @__x__@, then holds: @'lftcLiftable' c@ is 'valid'.

data LiftableCone i s p d t n m x where
  LiftableKernelCone
    :: KernelCone N1 x -> (Slice To i x -> Slice To i x)
    -> LiftableCone i Dst Projective Diagram (Parallel LeftToRight) N2 N1 x
  LiftableCokernelCone
    :: CokernelCone N1 x -> (Slice From i x -> Slice From i x)
    -> LiftableCone i Dst Injective Diagram (Parallel RightToLeft) N2 N1 x

instance Conic (LiftableCone i) where
  cone :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
LiftableCone i s p d t n m x -> Cone s p d t n m x
cone (LiftableKernelCone KernelCone N1 x
k Slice 'To i x -> Slice 'To i x
_)   = Cone s p d t n m x
KernelCone N1 x
k
  cone (LiftableCokernelCone CokernelCone N1 x
c Slice 'From i x -> Slice 'From i x
_) = Cone s p d t n m x
CokernelCone N1 x
c
  
--------------------------------------------------------------------------------

-- lftcLiftable -


-- | the associated 'Liftable'.

lftcLiftable :: Sliced i x => LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable :: forall (i :: * -> *) x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Sliced i x =>
LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable (LiftableKernelCone KernelCone N1 x
k Slice 'To i x -> Slice 'To i x
lft)   = x -> (Slice 'To i x -> Slice 'To i x) -> Liftable 'Projective i x
forall (i :: * -> *) x.
Sliced i x =>
x -> (Slice 'To i x -> Slice 'To i x) -> Liftable 'Projective i x
LiftableProjective (KernelCone N1 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Conic c =>
KernelConic c d n x -> x
kernelFactor KernelCone N1 x
k) Slice 'To i x -> Slice 'To i x
lft
lftcLiftable (LiftableCokernelCone CokernelCone N1 x
c Slice 'From i x -> Slice 'From i x
lft) = x
-> (Slice 'From i x -> Slice 'From i x) -> Liftable 'Injective i x
forall (i :: * -> *) x.
Sliced i x =>
x
-> (Slice 'From i x -> Slice 'From i x) -> Liftable 'Injective i x
LiftableInjective (CokernelCone N1 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Conic c =>
CokernelConic c d n x -> x
cokernelFactor CokernelCone N1 x
c) Slice 'From i x -> Slice 'From i x
lft

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

-- lftcMapCov -


lftcMapCovStruct :: (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h)
  => Struct (Sld i) x -> Variant2 Covariant (Inv2 h) x y
  -> LiftableCone i s p d t n m x -> LiftableCone i s p d t n m y
lftcMapCovStruct :: forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Struct (Sld i) x
-> Variant2 'Covariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s p d t n m y
lftcMapCovStruct Struct (Sld i) x
Struct (Covariant2 Inv2 h x y
i) c :: LiftableCone i s p d t n m x
c@(LiftableKernelCone KernelCone N1 x
k Slice 'To i x -> Slice 'To i x
_)
  = KernelCone N1 y
-> (Slice 'To i y -> Slice 'To i y)
-> LiftableCone
     i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 y
forall x (i :: * -> *).
KernelCone N1 x
-> (Slice 'To i x -> Slice 'To i x)
-> LiftableCone
     i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
LiftableKernelCone KernelCone N1 y
k' Slice 'To i y -> Slice 'To i y
lft' where
    SDualBi (Right1 KernelCone N1 y
k')                          = Inv2 h x y
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     x
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     y
forall x y.
Inv2 h x y
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     x
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 h x y
i (Either1
  (Dual1
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1))
  (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
  x
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (KernelCone N1 x
-> Either1
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 KernelCone N1 x
k))
    SDualBi (Right1 (LiftableProjective y
_ Slice 'To i y -> Slice 'To i y
lft')) = Inv2 h x y
-> SDualBi (Liftable 'Projective i) x
-> SDualBi (Liftable 'Projective i) y
forall x y.
Inv2 h x y
-> SDualBi (Liftable 'Projective i) x
-> SDualBi (Liftable 'Projective i) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 h x y
i (Either1 (Dual1 (Liftable 'Projective i)) (Liftable 'Projective i) x
-> SDualBi (Liftable 'Projective i) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Liftable p i x
-> Either1
     (Liftable (Dual 'Projective) i) (Liftable 'Projective i) x
Liftable 'Projective i x
-> Either1 (Liftable 'Injective i) (Liftable 'Projective i) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Liftable p i x
 -> Either1
      (Liftable (Dual 'Projective) i) (Liftable 'Projective i) x)
-> Liftable p i x
-> Either1
     (Liftable (Dual 'Projective) i) (Liftable 'Projective i) x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LiftableCone i s p d t n m x -> Liftable p i x
forall (i :: * -> *) x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Sliced i x =>
LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable LiftableCone i s p d t n m x
c))  
lftcMapCovStruct Struct (Sld i) x
Struct (Covariant2 Inv2 h x y
i) c :: LiftableCone i s p d t n m x
c@(LiftableCokernelCone CokernelCone N1 x
k Slice 'From i x -> Slice 'From i x
_)
  = CokernelCone N1 y
-> (Slice 'From i y -> Slice 'From i y)
-> LiftableCone
     i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1 y
forall x (i :: * -> *).
CokernelCone N1 x
-> (Slice 'From i x -> Slice 'From i x)
-> LiftableCone
     i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1 x
LiftableCokernelCone CokernelCone N1 y
k' Slice 'From i y -> Slice 'From i y
lft' where
    SDualBi (Right1 CokernelCone N1 y
k')                         = Inv2 h x y
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) y
forall x y.
Inv2 h x y
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 h x y
i (Either1
  (Dual1
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1))
  (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
  x
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (CokernelCone N1 x
-> Either1
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 CokernelCone N1 x
k))
    SDualBi (Right1 (LiftableInjective y
_ Slice 'From i y -> Slice 'From i y
lft')) = Inv2 h x y
-> SDualBi (Liftable 'Injective i) x
-> SDualBi (Liftable 'Injective i) y
forall x y.
Inv2 h x y
-> SDualBi (Liftable 'Injective i) x
-> SDualBi (Liftable 'Injective i) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 h x y
i (Either1 (Dual1 (Liftable 'Injective i)) (Liftable 'Injective i) x
-> SDualBi (Liftable 'Injective i) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Liftable p i x
-> Either1 (Liftable (Dual 'Injective) i) (Liftable 'Injective i) x
Liftable 'Injective i x
-> Either1 (Liftable 'Projective i) (Liftable 'Injective i) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Liftable p i x
 -> Either1
      (Liftable (Dual 'Injective) i) (Liftable 'Injective i) x)
-> Liftable p i x
-> Either1 (Liftable (Dual 'Injective) i) (Liftable 'Injective i) x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LiftableCone i s p d t n m x -> Liftable p i x
forall (i :: * -> *) x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Sliced i x =>
LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable LiftableCone i s p d t n m x
c))

-- | covariant mapping of 'LiftableCone'.

lftcMapCov :: (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h)
  => Variant2 Covariant (Inv2 h) x y
  -> LiftableCone i s p d t n m x -> LiftableCone i s p d t n m y
lftcMapCov :: forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Variant2 'Covariant (Inv2 h) x y
-> LiftableCone i s p d t n m x -> LiftableCone i s p d t n m y
lftcMapCov Variant2 'Covariant (Inv2 h) x y
h = Struct (Sld i) x
-> Variant2 'Covariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s p d t n m y
forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Struct (Sld i) x
-> Variant2 'Covariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s p d t n m y
lftcMapCovStruct (Struct (ObjectClass h) x -> Struct (Sld i) x
forall x. Struct (ObjectClass h) x -> Struct (Sld i) x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Variant2 'Covariant (Inv2 h) x y
-> Struct (ObjectClass (Variant2 'Covariant (Inv2 h))) x
forall x y.
Variant2 'Covariant (Inv2 h) x y
-> Struct (ObjectClass (Variant2 'Covariant (Inv2 h))) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Variant2 'Covariant (Inv2 h) x y
h)) Variant2 'Covariant (Inv2 h) x y
h

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

-- lftcMapCnt


lftcMapCntStruct :: (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h)
  => Struct (Sld i) x
  -> Variant2 Contravariant (Inv2 h) x y
  -> LiftableCone i s p d t n m x -> LiftableCone i s (Dual p) d (Dual t) n m y
lftcMapCntStruct :: forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Struct (Sld i) x
-> Variant2 'Contravariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s (Dual p) d (Dual t) n m y
lftcMapCntStruct Struct (Sld i) x
Struct (Contravariant2 Inv2 h x y
i) c :: LiftableCone i s p d t n m x
c@(LiftableKernelCone KernelCone N1 x
k Slice 'To i x -> Slice 'To i x
_)
  = CokernelCone N1 y
-> (Slice 'From i y -> Slice 'From i y)
-> LiftableCone
     i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1 y
forall x (i :: * -> *).
CokernelCone N1 x
-> (Slice 'From i x -> Slice 'From i x)
-> LiftableCone
     i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1 x
LiftableCokernelCone Dual1
  (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
  y
CokernelCone N1 y
k' Slice 'From i y -> Slice 'From i y
lft' where
    SDualBi (Left1 Dual1
  (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
  y
k')                         = Inv2 h x y
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     x
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     y
forall x y.
Inv2 h x y
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     x
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 h x y
i (Either1
  (Dual1
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1))
  (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
  x
-> SDualBi
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (KernelCone N1 x
-> Either1
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 KernelCone N1 x
k))
    SDualBi (Left1 (LiftableInjective y
_ Slice 'From i y -> Slice 'From i y
lft')) = Inv2 h x y
-> SDualBi (Liftable 'Projective i) x
-> SDualBi (Liftable 'Projective i) y
forall x y.
Inv2 h x y
-> SDualBi (Liftable 'Projective i) x
-> SDualBi (Liftable 'Projective i) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 h x y
i (Either1 (Dual1 (Liftable 'Projective i)) (Liftable 'Projective i) x
-> SDualBi (Liftable 'Projective i) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Liftable p i x
-> Either1
     (Dual1 (Liftable 'Projective i)) (Liftable 'Projective i) x
Liftable 'Projective i x
-> Either1 (Liftable 'Injective i) (Liftable 'Projective i) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Liftable p i x
 -> Either1
      (Dual1 (Liftable 'Projective i)) (Liftable 'Projective i) x)
-> Liftable p i x
-> Either1
     (Dual1 (Liftable 'Projective i)) (Liftable 'Projective i) x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LiftableCone i s p d t n m x -> Liftable p i x
forall (i :: * -> *) x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Sliced i x =>
LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable LiftableCone i s p d t n m x
c))
lftcMapCntStruct Struct (Sld i) x
Struct (Contravariant2 Inv2 h x y
i) c :: LiftableCone i s p d t n m x
c@(LiftableCokernelCone CokernelCone N1 x
k Slice 'From i x -> Slice 'From i x
_)
  = KernelCone N1 y
-> (Slice 'To i y -> Slice 'To i y)
-> LiftableCone
     i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 y
forall x (i :: * -> *).
KernelCone N1 x
-> (Slice 'To i x -> Slice 'To i x)
-> LiftableCone
     i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
LiftableKernelCone Dual1
  (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) y
KernelCone N1 y
k' Slice 'To i y -> Slice 'To i y
lft' where
    SDualBi (Left1 Dual1
  (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) y
k')                          = Inv2 h x y
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) y
forall x y.
Inv2 h x y
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 h x y
i (Either1
  (Dual1
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1))
  (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
  x
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (CokernelCone N1 x
-> Either1
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1)
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 CokernelCone N1 x
k))
    SDualBi (Left1 (LiftableProjective y
_ Slice 'To i y -> Slice 'To i y
lft')) = Inv2 h x y
-> SDualBi (Liftable 'Injective i) x
-> SDualBi (Liftable 'Injective i) y
forall x y.
Inv2 h x y
-> SDualBi (Liftable 'Injective i) x
-> SDualBi (Liftable 'Injective i) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 h x y
i (Either1 (Dual1 (Liftable 'Injective i)) (Liftable 'Injective i) x
-> SDualBi (Liftable 'Injective i) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Liftable p i x
-> Either1
     (Dual1 (Liftable 'Injective i)) (Liftable 'Injective i) x
Liftable 'Injective i x
-> Either1 (Liftable 'Projective i) (Liftable 'Injective i) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Liftable p i x
 -> Either1
      (Dual1 (Liftable 'Injective i)) (Liftable 'Injective i) x)
-> Liftable p i x
-> Either1
     (Dual1 (Liftable 'Injective i)) (Liftable 'Injective i) x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LiftableCone i s p d t n m x -> Liftable p i x
forall (i :: * -> *) x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Sliced i x =>
LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable LiftableCone i s p d t n m x
c))

-- | contravariant mapping of 'LiftableCone'.

lftcMapCnt :: (CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h)
  => Variant2 Contravariant (Inv2 h) x y
  -> LiftableCone i s p d t n m x -> LiftableCone i s (Dual p) d (Dual t) n m y
lftcMapCnt :: forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Variant2 'Contravariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s (Dual p) d (Dual t) n m y
lftcMapCnt Variant2 'Contravariant (Inv2 h) x y
h = Struct (Sld i) x
-> Variant2 'Contravariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s (Dual p) d (Dual t) n m y
forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Struct (Sld i) x
-> Variant2 'Contravariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s (Dual p) d (Dual t) n m y
lftcMapCntStruct (Struct (ObjectClass h) x -> Struct (Sld i) x
forall x. Struct (ObjectClass h) x -> Struct (Sld i) x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Variant2 'Contravariant (Inv2 h) x y
-> Struct (ObjectClass (Variant2 'Contravariant (Inv2 h))) x
forall x y.
Variant2 'Contravariant (Inv2 h) x y
-> Struct (ObjectClass (Variant2 'Contravariant (Inv2 h))) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Variant2 'Contravariant (Inv2 h) x y
h)) Variant2 'Contravariant (Inv2 h) x y
h

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

-- Duality -


type instance Dual1 (LiftableCone i s p d t n m) = LiftableCone i s (Dual p) d (Dual t) n m

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

-- lftcMapS -


-- | mapping of 'LiftableCone'.

lftcMapS ::
  ( CategoryDisjunctive h
  , HomSlicedDistributive i h
  , FunctorialOriented h
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  )
  => Inv2 h x y -> SDualBi (LiftableCone i s p d t n m) x -> SDualBi (LiftableCone i s p d t n m) y
lftcMapS :: forall (h :: * -> * -> *) (i :: * -> *) (p :: Perspective)
       (t :: DiagramType) x y s (d :: DiagramType -> N' -> N' -> * -> *)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t)) =>
Inv2 h x y
-> SDualBi (LiftableCone i s p d t n m) x
-> SDualBi (LiftableCone i s p d t n m) y
lftcMapS = (Variant2 'Covariant (Inv2 h) x y
 -> LiftableCone i s p d t n m x -> LiftableCone i s p d t n m y)
-> (Variant2 'Covariant (Inv2 h) x y
    -> Dual1 (LiftableCone i s p d t n m) x
    -> Dual1 (LiftableCone i s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> LiftableCone i s p d t n m x
    -> Dual1 (LiftableCone i s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> Dual1 (LiftableCone i s p d t n m) x
    -> LiftableCone i s p d t n m y)
-> Inv2 h x y
-> SDualBi (LiftableCone i s p d t n m) x
-> SDualBi (LiftableCone i s p d t n m) y
forall (h :: * -> * -> *) x y (d :: * -> *).
Disjunctive2 h =>
(Variant2 'Covariant h x y -> d x -> d y)
-> (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> Dual1 d x -> d y)
-> h x y
-> SDualBi d x
-> SDualBi d y
vmapBi Variant2 'Covariant (Inv2 h) x y
-> LiftableCone i s p d t n m x -> LiftableCone i s p d t n m y
forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Variant2 'Covariant (Inv2 h) x y
-> LiftableCone i s p d t n m x -> LiftableCone i s p d t n m y
lftcMapCov Variant2 'Covariant (Inv2 h) x y
-> Dual1 (LiftableCone i s p d t n m) x
-> Dual1 (LiftableCone i s p d t n m) y
Variant2 'Covariant (Inv2 h) x y
-> LiftableCone i s (Dual p) d (Dual t) n m x
-> LiftableCone i s (Dual p) d (Dual t) n m y
forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Variant2 'Covariant (Inv2 h) x y
-> LiftableCone i s p d t n m x -> LiftableCone i s p d t n m y
lftcMapCov Variant2 'Contravariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> Dual1 (LiftableCone i s p d t n m) y
Variant2 'Contravariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s (Dual p) d (Dual t) n m y
forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Variant2 'Contravariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s (Dual p) d (Dual t) n m y
lftcMapCnt Variant2 'Contravariant (Inv2 h) x y
-> Dual1 (LiftableCone i s p d t n m) x
-> LiftableCone i s p d t n m y
Variant2 'Contravariant (Inv2 h) x y
-> LiftableCone i s (Dual p) d (Dual t) n m x
-> LiftableCone i s (Dual (Dual p)) d (Dual (Dual t)) n m y
forall (h :: * -> * -> *) (i :: * -> *) x y s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h) =>
Variant2 'Contravariant (Inv2 h) x y
-> LiftableCone i s p d t n m x
-> LiftableCone i s (Dual p) d (Dual t) n m y
lftcMapCnt

instance 
  ( CategoryDisjunctive h
  , HomSlicedDistributive i h
  , FunctorialOriented h
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  )
  => ApplicativeG (SDualBi (LiftableCone i s p d t n m)) (Inv2 h) (->) where
  amapG :: forall x y.
Inv2 h x y
-> SDualBi (LiftableCone i s p d t n m) x
   -> SDualBi (LiftableCone i s p d t n m) y
amapG = Inv2 h x y
-> SDualBi (LiftableCone i s p d t n m) x
-> SDualBi (LiftableCone i s p d t n m) y
forall (h :: * -> * -> *) (i :: * -> *) (p :: Perspective)
       (t :: DiagramType) x y s (d :: DiagramType -> N' -> N' -> * -> *)
       (n :: N') (m :: N').
(CategoryDisjunctive h, HomSlicedDistributive i h,
 FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t)) =>
Inv2 h x y
-> SDualBi (LiftableCone i s p d t n m) x
-> SDualBi (LiftableCone i s p d t n m) y
lftcMapS

instance 
  ( CategoryDisjunctive h
  , HomSlicedDistributive i h
  , FunctorialOriented h
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (LiftableCone i s p d t n m)) (Inv2 h) (->)  

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

-- LiftableKernel -


-- | liftable kenrel according to a slice index @__i__@.

type LiftableKernel i = KernelG (LiftableCone i) Diagram N1


-- | liftable kernels according to a slice index @__i__@.

type LiftableKernels i = KernelsG (LiftableCone i) Diagram N1


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

-- LiftableCokernel -


-- | liftable cokernel according to a slice index @__i__@.

type LiftableCokernel i = CokernelG (LiftableCone i) Diagram N1

-- | liftable cokernels according to a slice index @__i__@.

type LiftableCokernels i = CokernelsG (LiftableCone i) Diagram N1

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

-- lftlKernel -


-- | the liftable property for 'LiftableKernel'.

lftlKernel :: Sliced i x => LiftableKernel i x -> Slice To i x -> Slice To i x
lftlKernel :: forall (i :: * -> *) x.
Sliced i x =>
LiftableKernel i x -> Slice 'To i x -> Slice 'To i x
lftlKernel = Liftable 'Projective i x
-> Slice (ToSite 'Projective) i x -> Slice (ToSite 'Projective) i x
Liftable 'Projective i x -> Slice 'To i x -> Slice 'To i x
forall (p :: Perspective) (i :: * -> *) x.
Liftable p i x -> Slice (ToSite p) i x -> Slice (ToSite p) i x
lift (Liftable 'Projective i x -> Slice 'To i x -> Slice 'To i x)
-> (LiftableKernel i x -> Liftable 'Projective i x)
-> LiftableKernel i x
-> Slice 'To i x
-> Slice 'To i 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
. LiftableCone
  i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
-> Liftable 'Projective i x
forall (i :: * -> *) x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Sliced i x =>
LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable (LiftableCone
   i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
 -> Liftable 'Projective i x)
-> (LiftableKernel i x
    -> LiftableCone
         i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x)
-> LiftableKernel i x
-> Liftable 'Projective i 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
. LiftableKernel i x
-> LiftableCone
     i Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone

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

-- lftlCokernel -


-- | the liftable property for 'LiftableCokernel'.

lftlCokernel :: Sliced i x => LiftableCokernel i x -> Slice From i x -> Slice From i x
lftlCokernel :: forall (i :: * -> *) x.
Sliced i x =>
LiftableCokernel i x -> Slice 'From i x -> Slice 'From i x
lftlCokernel = Liftable 'Injective i x
-> Slice (ToSite 'Injective) i x -> Slice (ToSite 'Injective) i x
Liftable 'Injective i x -> Slice 'From i x -> Slice 'From i x
forall (p :: Perspective) (i :: * -> *) x.
Liftable p i x -> Slice (ToSite p) i x -> Slice (ToSite p) i x
lift (Liftable 'Injective i x -> Slice 'From i x -> Slice 'From i x)
-> (LiftableCokernel i x -> Liftable 'Injective i x)
-> LiftableCokernel i x
-> Slice 'From i x
-> Slice 'From i 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
. LiftableCone
  i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1 x
-> Liftable 'Injective i x
forall (i :: * -> *) x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Sliced i x =>
LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable (LiftableCone
   i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1 x
 -> Liftable 'Injective i x)
-> (LiftableCokernel i x
    -> LiftableCone
         i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1 x)
-> LiftableCokernel i x
-> Liftable 'Injective i 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
. LiftableCokernel i x
-> LiftableCone
     i Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone

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

-- LiftableLimes - Predicate -


instance Oriented x => Show (LiftableCone i s p d t n m x) where
  show :: LiftableCone i s p d t n m x -> String
show (LiftableKernelCone KernelCone N1 x
k Slice 'To i x -> Slice 'To i x
_)   = [String] -> String
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join [String
"LiftableKernelCone (", KernelCone N1 x -> String
forall a. Show a => a -> String
show KernelCone N1 x
k, String
") lft"]
  show (LiftableCokernelCone CokernelCone N1 x
c Slice 'From i x -> Slice 'From i x
_) = [String] -> String
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join [String
"LiftableCokernelCone (", CokernelCone N1 x -> String
forall a. Show a => a -> String
show CokernelCone N1 x
c, String
") lft"]
  

instance ( Distributive x, Sliced i x
         , XStandardOrtOrientation x
         ) => Validable (LiftableCone i s p d t n m x) where
  valid :: LiftableCone i s p d t n m x -> Statement
valid l :: LiftableCone i s p d t n m x
l@(LiftableKernelCone KernelCone N1 x
k Slice 'To i x -> Slice 'To i x
_)   = String -> Label
Label String
"LiftableKernel" Label -> Statement -> Statement
:<=>: KernelCone N1 x -> Statement
forall a. Validable a => a -> Statement
valid KernelCone N1 x
k Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& Liftable p i x -> Statement
forall a. Validable a => a -> Statement
valid (LiftableCone i s p d t n m x -> Liftable p i x
forall (i :: * -> *) x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Sliced i x =>
LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable LiftableCone i s p d t n m x
l)
  valid l :: LiftableCone i s p d t n m x
l@(LiftableCokernelCone CokernelCone N1 x
c Slice 'From i x -> Slice 'From i x
_) = String -> Label
Label String
"LiftableCokernel" Label -> Statement -> Statement
:<=>: CokernelCone N1 x -> Statement
forall a. Validable a => a -> Statement
valid CokernelCone N1 x
c Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& Liftable p i x -> Statement
forall a. Validable a => a -> Statement
valid (LiftableCone i s p d t n m x -> Liftable p i x
forall (i :: * -> *) x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Sliced i x =>
LiftableCone i s p d t n m x -> Liftable p i x
lftcLiftable LiftableCone i s p d t n m x
l)

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

-- NatrualConic -


instance 
  ( CategoryDisjunctive h
  , HomSlicedDistributive i h
  , FunctorialOriented h
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  )
  => ApplicativeG (SDualBi (ConeG (LiftableCone i) s p d t n m)) (Inv2 h) (->) where
  amapG :: forall x y.
Inv2 h x y
-> SDualBi (ConeG (LiftableCone i) s p d t n m) x
   -> SDualBi (ConeG (LiftableCone i) s p d t n m) y
amapG Inv2 h x y
i = SDualBi (LiftableCone i s p d t n m) y
-> SDualBi (ConeG (LiftableCone i) s p d t n m) y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Dual1 (c s p d t n m) ~ c s (Dual p) d (Dual t) n m) =>
SDualBi (c s p d t n m) x -> SDualBi (ConeG c s p d t n m) x
sdbFromCncObj (SDualBi (LiftableCone i s p d t n m) y
 -> SDualBi (ConeG (LiftableCone i) s p d t n m) y)
-> (SDualBi (ConeG (LiftableCone i) s p d t n m) x
    -> SDualBi (LiftableCone i s p d t n m) y)
-> SDualBi (ConeG (LiftableCone i) s p d t n m) x
-> SDualBi (ConeG (LiftableCone i) s p d t n m) 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
. Inv2 h x y
-> SDualBi (LiftableCone i s p d t n m) x
-> SDualBi (LiftableCone i s p d t n m) y
forall x y.
Inv2 h x y
-> SDualBi (LiftableCone i s p d t n m) x
-> SDualBi (LiftableCone i s p 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 y
i (SDualBi (LiftableCone i s p d t n m) x
 -> SDualBi (LiftableCone i s p d t n m) y)
-> (SDualBi (ConeG (LiftableCone i) s p d t n m) x
    -> SDualBi (LiftableCone i s p d t n m) x)
-> SDualBi (ConeG (LiftableCone i) s p d t n m) x
-> SDualBi (LiftableCone i s p d t n m) 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
. SDualBi (ConeG (LiftableCone i) s p d t n m) x
-> SDualBi (LiftableCone i 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.
(Dual1 (c s p d t n m) ~ c s (Dual p) d (Dual t) n m) =>
SDualBi (ConeG c s p d t n m) x -> SDualBi (c s p d t n m) x
sdbToCncObj

instance
  ( CategoryDisjunctive h
  , HomSlicedDistributive i h
  , FunctorialOriented h
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (ConeG (LiftableCone i) s p d t n m)) (Inv2 h) (->)  

instance
  ( CategoryDisjunctive h
  , HomSlicedDistributive i h
  , FunctorialOriented h
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  , s ~ Dst
  )
  => NaturalTransformable (Inv2 h) (->)
       (SDualBi (ConeG (LiftableCone i) s p Diagram t n m)) (SDualBi (ConeG Cone s p Diagram t n m))  

instance
  ( CategoryDisjunctive h
  , HomSlicedDistributive i h
  , FunctorialOriented h
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  , s ~ Dst
  )
  => NaturalConic (Inv2 h) (LiftableCone i) s p Diagram t n m


{-
--------------------------------------------------------------------------------
-- LiftableStruct -

data LiftableStruct i s c where
  LiftableStruct :: (Distributive c, Sliced i c) => LiftableStruct i s c

instance OpReflexive (LiftableStruct i) Dst where
  opdStructOp LiftableStruct = LiftableStruct
  opdConeStruct LiftableStruct = ConeStructDst
  opdRefl LiftableStruct = isoToOpOpDst

instance OpDualisable (LiftableStruct i) (LiftableLimes i) Dst where
  opdToOp LiftableStruct (OpDuality rp rt)   = coLiftableLimes rp rt
  opdFromOp LiftableStruct (OpDuality rp rt) = coLiftableLimesInv rp rt

instance Typeable i => UniversalApplicative (IsoOp (Sld Dst i)) (LiftableLimes i) Dst where
  umap = lftlMap

-}