{-# LANGUAGE NoImplicitPrelude #-}

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


-- |

-- Module      : OAlg.Entity.Slice.Free

-- Description : slicing by free points.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- sliced structures with assigned /free/ 'Point's of some given /dimension/.

module OAlg.Entity.Slice.Free
  (

    -- * Free

    Free(..), free', freeN, castFree, isFree
  , SomeFree(..), sfrPoint, sfrMap

    -- * Sliced Free

  , SlicedFree(..), SldFr, HomOrientedSlicedFree
  , prpHomOrientedSlicedFree
  , SomeFreeSlice(..), slicedFree'
  
    -- * Diagram Free

  , DiagramFree(..),dgfDiagram
  , dgfMapS, dgfMapCov, dgfMapCnt
  
    -- * Some Free Slice Diagram

  , SomeFreeSliceDiagram(..)
  
    -- ** Duality

  , sfsdMapS, sfsdMapCov, sfsdMapCnt

    -- * Cone Liftable

  , ConeLiftable(..), cnLiftable, cnlMapS
    
    -- * Liftable Free

  , LiftableFree(..), liftFree
  , HomFree, lftFrMapSMlt, lftFrMapSDst
  , NaturalDiagrammaticFree

  , CokernelsLiftableSomeFree, CokernelLiftableSomeFree
  
    -- * Free Tip

  , ConicFreeTip(..)
  , KernelsSomeFreeFreeTip, KernelSomeFreeFreeTip
  , KernelSliceFromSomeFreeTip(..)

    -- * Duality

  , toDualOpFreeDst

  ) where

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

import OAlg.Prelude

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

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

import OAlg.Structure.Oriented
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive
import OAlg.Structure.Multiplicative
import OAlg.Structure.Distributive

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

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

import OAlg.Entity.Natural hiding ((++))
import OAlg.Entity.FinList hiding ((++))
import OAlg.Entity.Diagram
import OAlg.Entity.Slice.Definition
import OAlg.Entity.Slice.Sliced
import OAlg.Entity.Slice.Liftable

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

-- Free -


-- | index for free points within a 'Multiplicative' structure @__c__@.

--

-- >>> lengthN (Free attest :: Free N3 c)

-- 3

newtype Free k c = Free (Any k) deriving (Int -> Free k c -> ShowS
[Free k c] -> ShowS
Free k c -> String
(Int -> Free k c -> ShowS)
-> (Free k c -> String) -> ([Free k c] -> ShowS) -> Show (Free k c)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (k :: N') c. Int -> Free k c -> ShowS
forall (k :: N') c. [Free k c] -> ShowS
forall (k :: N') c. Free k c -> String
$cshowsPrec :: forall (k :: N') c. Int -> Free k c -> ShowS
showsPrec :: Int -> Free k c -> ShowS
$cshow :: forall (k :: N') c. Free k c -> String
show :: Free k c -> String
$cshowList :: forall (k :: N') c. [Free k c] -> ShowS
showList :: [Free k c] -> ShowS
Show,Free k c -> Free k c -> Bool
(Free k c -> Free k c -> Bool)
-> (Free k c -> Free k c -> Bool) -> Eq (Free k c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (k :: N') c. Free k c -> Free k c -> Bool
$c== :: forall (k :: N') c. Free k c -> Free k c -> Bool
== :: Free k c -> Free k c -> Bool
$c/= :: forall (k :: N') c. Free k c -> Free k c -> Bool
/= :: Free k c -> Free k c -> Bool
Eq,Free k c -> Statement
(Free k c -> Statement) -> Validable (Free k c)
forall a. (a -> Statement) -> Validable a
forall (k :: N') c. Free k c -> Statement
$cvalid :: forall (k :: N') c. Free k c -> Statement
valid :: Free k c -> Statement
Validable)

instance Attestable k => Singleton1 (Free k) where
  unit1 :: forall x. Free k x
unit1 = Any k -> Free k x
forall (k :: N') c. Any k -> Free k c
Free Any k
forall (n :: N'). Attestable n => W n
attest

instance Show1 (Free k)
instance Eq1 (Free k)
instance Validable1 (Free k)
-- instance Typeable k => Entity1 (Free k)


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

-- free' -


-- | @__k__@-'Free' of @__x__@, given by the proxy @__q x__@.

free' :: q x -> Any k -> Free k x
free' :: forall (q :: * -> *) x (k :: N'). q x -> Any k -> Free k x
free' q x
_ = Any k -> Free k x
forall (k :: N') c. Any k -> Free k c
Free

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

-- freeN -


-- | the underlying natural number.

freeN :: Free k c -> N
freeN :: forall (k :: N') c. Free k c -> N
freeN (Free Any k
k) = Any k -> N
forall x. LengthN x => x -> N
lengthN Any k
k

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

-- castFree -


-- | casting between 'Free' types.

castFree :: Free k x -> Free k y
castFree :: forall (k :: N') x y. Free k x -> Free k y
castFree (Free Any k
k) = Any k -> Free k y
forall (k :: N') c. Any k -> Free k c
Free Any k
k

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

-- isFree -


-- | check for being a free point, i.e. if it is equal to 'slicePoint'.

--

-- __Definition__ Let @n@ be in @'Free' __n__ __c__@ and @p@ in @'Point' __c__@ then

-- we call @p@ of __/order/__ @n@ if and only if @'slicePoint' i '==' p@.

isFree :: Sliced (Free k) c => Free k c -> Point c -> Bool
isFree :: forall (k :: N') c.
Sliced (Free k) c =>
Free k c -> Point c -> Bool
isFree Free k c
i Point c
p = Free k c -> Point c
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint Free k c
i Point c -> Point c -> Bool
forall a. Eq a => a -> a -> Bool
== Point c
p

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

-- SomeFree -


-- | some free attest.

data SomeFree c where
  SomeFree :: (Attestable k, Sliced (Free k) c) => Free k c -> SomeFree c

deriving instance Show (SomeFree c)

instance Eq (SomeFree c) where
  SomeFree (Free Any k
k) == :: SomeFree c -> SomeFree c -> Bool
== SomeFree (Free Any k
k') = case Any k
k Any k -> Any k -> Ordering
forall (n :: N') (m :: N'). W n -> W m -> Ordering
`cmpW` Any k
k' of
    Ordering
EQ -> Bool
True
    Ordering
_  -> Bool
False

instance Validable (SomeFree c) where
  valid :: SomeFree c -> Statement
valid (SomeFree Free k c
k) = String -> Label
Label String
"SomeFree" Label -> Statement -> Statement
:<=>: Free k c -> Statement
forall a. Validable a => a -> Statement
valid Free k c
k

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

-- sfrPoint -


-- | the given slice point.

sfrPoint :: SomeFree x -> Point x
sfrPoint :: forall x. SomeFree x -> Point x
sfrPoint (SomeFree Free k x
f) = Free k x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint Free k x
f

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

-- SliceFree -


-- | attest for @__k__@-free sliced structures.

class SlicedFree x where
  slicedFree :: Attestable k => Struct (Sld (Free k)) x

-- | attest for @__k__@-free sliced structures according to the given proxy type.

slicedFree' :: (SlicedFree x, Attestable k) => q x -> Any k -> Struct (Sld (Free k)) x
slicedFree' :: forall x (k :: N') (q :: * -> *).
(SlicedFree x, Attestable k) =>
q x -> Any k -> Struct (Sld (Free k)) x
slicedFree' q x
_ Any k
_ = Struct (Sld (Free k)) x
forall x (k :: N').
(SlicedFree x, Attestable k) =>
Struct (Sld (Free k)) x
forall (k :: N'). Attestable k => Struct (Sld (Free k)) x
slicedFree

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

-- tauSldFrTuple -


-- | decorating the @__s__@ structure with @__k__@ sliced free.

tauSldFrTuple :: (SlicedFree x, Attestable k) => Struct s x -> Struct (s,Sld (Free k)) x
tauSldFrTuple :: forall x (k :: N') s.
(SlicedFree x, Attestable k) =>
Struct s x -> Struct (s, Sld (Free k)) x
tauSldFrTuple Struct s x
s = Struct s x -> Struct (Sld (Free k)) x -> Struct (s, Sld (Free k)) x
forall s x t. Struct s x -> Struct t x -> Struct (s, t) x
tauTuple Struct s x
s Struct (Sld (Free k)) x
forall x (k :: N').
(SlicedFree x, Attestable k) =>
Struct (Sld (Free k)) x
forall (k :: N'). Attestable k => Struct (Sld (Free k)) x
slicedFree

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

-- tauSldFreeOp -


-- | propagating to 'Op'

tauSldFreeOp :: Struct (Sld (Free k)) x -> Struct (Sld (Free k)) (Op x)
tauSldFreeOp :: forall (k :: N') x.
Struct (Sld (Free k)) x -> Struct (Sld (Free k)) (Op x)
tauSldFreeOp Struct (Sld (Free k)) x
Struct = Struct (Sld (Free k)) (Op x)
forall s x. Structure s x => Struct s x
Struct 

instance SlicedFree x => SlicedFree (Op x) where slicedFree :: forall (k :: N'). Attestable k => Struct (Sld (Free k)) (Op x)
slicedFree = Struct (Sld (Free k)) x -> Struct (Sld (Free k)) (Op x)
forall (k :: N') x.
Struct (Sld (Free k)) x -> Struct (Sld (Free k)) (Op x)
tauSldFreeOp Struct (Sld (Free k)) x
forall x (k :: N').
(SlicedFree x, Attestable k) =>
Struct (Sld (Free k)) x
forall (k :: N'). Attestable k => Struct (Sld (Free k)) x
slicedFree

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

-- SldFr -


-- | 'SlicedFree' structures. 

data SldFr

type instance Structure SldFr x = SlicedFree x

instance Transformable s Ort    => Transformable (s,SldFr) Ort    where tau :: forall x. Struct (s, SldFr) x -> Struct Ort x
tau = Struct s x -> Struct Ort x
forall x. Struct s x -> Struct Ort x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Ort x)
-> (Struct (s, SldFr) x -> Struct s x)
-> Struct (s, SldFr) x
-> Struct Ort x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (s, SldFr) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance Transformable s Mlt    => Transformable (s,SldFr) Mlt    where tau :: forall x. Struct (s, SldFr) x -> Struct Mlt x
tau = Struct s x -> Struct Mlt x
forall x. Struct s x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Mlt x)
-> (Struct (s, SldFr) x -> Struct s x)
-> Struct (s, SldFr) x
-> Struct Mlt x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (s, SldFr) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance Transformable s Fbr    => Transformable (s,SldFr) Fbr    where tau :: forall x. Struct (s, SldFr) x -> Struct Fbr x
tau = Struct s x -> Struct Fbr x
forall x. Struct s x -> Struct Fbr x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Fbr x)
-> (Struct (s, SldFr) x -> Struct s x)
-> Struct (s, SldFr) x
-> Struct Fbr x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (s, SldFr) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance Transformable s Add    => Transformable (s,SldFr) Add    where tau :: forall x. Struct (s, SldFr) x -> Struct Add x
tau = Struct s x -> Struct Add x
forall x. Struct s x -> Struct Add x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Add x)
-> (Struct (s, SldFr) x -> Struct s x)
-> Struct (s, SldFr) x
-> Struct Add x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (s, SldFr) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance Transformable s FbrOrt => Transformable (s,SldFr) FbrOrt where tau :: forall x. Struct (s, SldFr) x -> Struct FbrOrt x
tau = Struct s x -> Struct FbrOrt x
forall x. Struct s x -> Struct FbrOrt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct FbrOrt x)
-> (Struct (s, SldFr) x -> Struct s x)
-> Struct (s, SldFr) x
-> Struct FbrOrt x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (s, SldFr) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance Transformable s Dst    => Transformable (s,SldFr) Dst    where tau :: forall x. Struct (s, SldFr) x -> Struct Dst x
tau = Struct s x -> Struct Dst x
forall x. Struct s x -> Struct Dst x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct Dst x)
-> (Struct (s, SldFr) x -> Struct s x)
-> Struct (s, SldFr) x
-> Struct Dst x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (s, SldFr) x -> Struct s x
forall s t x. Struct (s, t) x -> Struct s x
tauFst

instance TransformableOrt s    => TransformableOrt (s,SldFr)
instance TransformableMlt s    => TransformableMlt (s,SldFr)
instance TransformableFbr s    => TransformableFbr (s,SldFr)
instance TransformableAdd s    => TransformableAdd (s,SldFr)
instance TransformableFbrOrt s => TransformableFbrOrt (s,SldFr)
instance TransformableDst s    => TransformableDst (s,SldFr) 

instance TransformableObjectClass (Mlt,SldFr) (HomDisj Mlt Op (HomEmpty Mlt))
instance TransformableObjectClass (Dst,SldFr) (HomDisj Dst Op (HomEmpty Dst))

instance FunctorialOriented (Sub (Mlt,SldFr) (HomDisjEmpty Mlt Op))
instance FunctorialOriented (Sub (Dst,SldFr) (HomDisjEmpty Dst Op))

instance Attestable k => Transformable (s,SldFr) (Sld (Free k)) where
  tau :: forall x. Struct (s, SldFr) x -> Struct (Sld (Free k)) x
tau Struct (s, SldFr) x
s = case Struct (s, SldFr) x -> Struct SldFr x
forall s t x. Struct (s, t) x -> Struct t x
tauSnd Struct (s, SldFr) x
s of Struct SldFr x
Struct -> Struct (Sld (Free k)) x
forall x (k :: N').
(SlicedFree x, Attestable k) =>
Struct (Sld (Free k)) x
forall (k :: N'). Attestable k => Struct (Sld (Free k)) x
slicedFree
  
instance Attestable k => HomSlicedOriented (Free k) (Sub (Dst,SldFr) (HomDisjEmpty Dst Op))

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

-- lftFrSub -


-- | embedding of @'IsoO' __s__ 'Op'@.

lftFrSub :: q k
   -> Struct (s,Sld (Free k)) x -> Struct (s,Sld (Free k)) y
   -> Variant2 v (IsoO s Op) x y
   -> Variant2 v (Inv2 (Sub (s,Sld (Free k)) (HomDisjEmpty s Op))) x y
lftFrSub :: forall (q :: N' -> *) (k :: N') s x y (v :: Variant).
q k
-> Struct (s, Sld (Free k)) x
-> Struct (s, Sld (Free k)) y
-> Variant2 v (IsoO s Op) x y
-> Variant2
     v (Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op))) x y
lftFrSub q k
_ Struct (s, Sld (Free k)) x
sx Struct (s, Sld (Free k)) y
sy = (IsoO s Op x y
 -> Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op)) x y)
-> Variant2 v (IsoO s Op) x y
-> Variant2
     v (Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op))) x y
forall {k1} {k2} (f :: k1 -> k2 -> *) (x :: k1) (y :: k2)
       (g :: k1 -> k2 -> *) (v :: Variant).
(f x y -> g x y) -> Variant2 v f x y -> Variant2 v g x y
amapVariant2 (\(Inv2 HomDisjEmpty s Op x y
t HomDisjEmpty s Op y x
f) -> Sub (s, Sld (Free k)) (HomDisjEmpty s Op) x y
-> Sub (s, Sld (Free k)) (HomDisjEmpty s Op) y x
-> Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op)) x y
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 (Homomorphous (s, Sld (Free k)) x y
-> HomDisjEmpty s Op x y
-> Sub (s, Sld (Free k)) (HomDisjEmpty s Op) x y
forall s x y (h :: * -> * -> *).
Homomorphous s x y -> h x y -> Sub s h x y
sub' (Struct (s, Sld (Free k)) x
sxStruct (s, Sld (Free k)) x
-> Struct (s, Sld (Free k)) y -> Homomorphous (s, Sld (Free k)) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>:Struct (s, Sld (Free k)) y
sy) HomDisjEmpty s Op x y
t) (Homomorphous (s, Sld (Free k)) y x
-> HomDisjEmpty s Op y x
-> Sub (s, Sld (Free k)) (HomDisjEmpty s Op) y x
forall s x y (h :: * -> * -> *).
Homomorphous s x y -> h x y -> Sub s h x y
sub' (Struct (s, Sld (Free k)) y
syStruct (s, Sld (Free k)) y
-> Struct (s, Sld (Free k)) x -> Homomorphous (s, Sld (Free k)) y x
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>:Struct (s, Sld (Free k)) x
sx) HomDisjEmpty s Op y x
f))

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

-- DiagramFree -


-- | predicate for diagrams with free points.

data DiagramFree t n m a = DiagramFree (FinList n (SomeFree a)) (Diagram t n m a)
  deriving (Int -> DiagramFree t n m a -> ShowS
[DiagramFree t n m a] -> ShowS
DiagramFree t n m a -> String
(Int -> DiagramFree t n m a -> ShowS)
-> (DiagramFree t n m a -> String)
-> ([DiagramFree t n m a] -> ShowS)
-> Show (DiagramFree t n m a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
Int -> DiagramFree t n m a -> ShowS
forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
[DiagramFree t n m a] -> ShowS
forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
DiagramFree t n m a -> String
$cshowsPrec :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
Int -> DiagramFree t n m a -> ShowS
showsPrec :: Int -> DiagramFree t n m a -> ShowS
$cshow :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
DiagramFree t n m a -> String
show :: DiagramFree t n m a -> String
$cshowList :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
[DiagramFree t n m a] -> ShowS
showList :: [DiagramFree t n m a] -> ShowS
Show,DiagramFree t n m a -> DiagramFree t n m a -> Bool
(DiagramFree t n m a -> DiagramFree t n m a -> Bool)
-> (DiagramFree t n m a -> DiagramFree t n m a -> Bool)
-> Eq (DiagramFree t n m a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: DiagramType) (n :: N') (m :: N') a.
(EqPoint a, Eq a) =>
DiagramFree t n m a -> DiagramFree t n m a -> Bool
$c== :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(EqPoint a, Eq a) =>
DiagramFree t n m a -> DiagramFree t n m a -> Bool
== :: DiagramFree t n m a -> DiagramFree t n m a -> Bool
$c/= :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(EqPoint a, Eq a) =>
DiagramFree t n m a -> DiagramFree t n m a -> Bool
/= :: DiagramFree t n m a -> DiagramFree t n m a -> Bool
Eq)

instance Oriented a => Validable (DiagramFree t n m a) where
  valid :: DiagramFree t n m a -> Statement
valid (DiagramFree FinList n (SomeFree a)
sfs Diagram t n m a
d) = String -> Label
Label String
"DiagramFree"
    Label -> Statement -> Statement
:<=>: (FinList n (SomeFree a), Diagram t n m a) -> Statement
forall a. Validable a => a -> Statement
valid (FinList n (SomeFree a)
sfs,Diagram t n m a
d) Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& N -> FinList n (SomeFree a) -> FinList n (Point a) -> Statement
forall a (n :: N').
Oriented a =>
N -> FinList n (SomeFree a) -> FinList n (Point a) -> Statement
vld N
0 FinList n (SomeFree a)
sfs (Diagram t n m a -> FinList n (Point a)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m a
d) where
    vld :: Oriented a => N -> FinList n (SomeFree a) -> FinList n (Point a) -> Statement
    vld :: forall a (n :: N').
Oriented a =>
N -> FinList n (SomeFree a) -> FinList n (Point a) -> Statement
vld N
_ FinList n (SomeFree a)
Nil FinList n (Point a)
Nil = Statement
SValid
    vld N
i (SomeFree Free k a
k:|FinList n1 (SomeFree a)
sfs) (Point a
p:|FinList n1 (Point a)
ps)
      = [Statement] -> Statement
And [ (Free k a -> Point a
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint Free k a
k Point a -> Point a -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
i,String
"k"String -> String -> Parameter
:=Free k a -> String
forall a. Show a => a -> String
show Free k a
k,String
"p"String -> String -> Parameter
:=Point a -> String
forall a. Show a => a -> String
show Point a
p]
            , N -> FinList n1 (SomeFree a) -> FinList n1 (Point a) -> Statement
forall a (n :: N').
Oriented a =>
N -> FinList n (SomeFree a) -> FinList n (Point a) -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) FinList n1 (SomeFree a)
sfs FinList n1 (Point a)
FinList n1 (Point a)
ps
            ] 

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

-- dgfDiagram -


-- | the underlying diagram.

dgfDiagram :: DiagramFree t n m a -> Diagram t n m a
dgfDiagram :: forall (t :: DiagramType) (n :: N') (m :: N') a.
DiagramFree t n m a -> Diagram t n m a
dgfDiagram (DiagramFree FinList n (SomeFree a)
_ Diagram t n m a
d) = Diagram t n m a
d

instance Diagrammatic DiagramFree where diagram :: forall (t :: DiagramType) (n :: N') (m :: N') a.
DiagramFree t n m a -> Diagram t n m a
diagram = DiagramFree t n m x -> Diagram t n m x
forall (t :: DiagramType) (n :: N') (m :: N') a.
DiagramFree t n m a -> Diagram t n m a
dgfDiagram

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

-- HomOrientedSlicedFree -


-- | homomorphisms between 'SlicedFree' structures, i.e. homomorphisms between 'Oriented' structures

-- where 'pmap' preserves the @__k__@-parameterized slice points.

--

-- __Property__ Let @'HomOrientedSlicedFree' __h__@, then

-- for all @__x__@, @__y__@ and @h@ in @__h x y__@ holds:

--

-- (1) For all @__k__@ holds:

-- @'pmap' h ('slicePoint' '$' 'free'' qx k) '==' ('slicePoint' '$' 'free'' qy k)@ where

-- @k@ is in @'Free' __k__ __x__@ and @qx@ is any proxy in @__q x__@

-- and @qy@ is any proxy in @__q y__@. 

class (HomOrientedDisjunctive h, Transformable (ObjectClass h) SldFr) => HomOrientedSlicedFree h

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

-- prpHomOrientedSlicedFree -


relHomOrientedSlicedFreeStruct :: (HomOrientedSlicedFree h, Show2 h)
  => Struct Ort x -> Struct Ort y
  -> Struct SldFr x -> Struct SldFr y
  -> h x y -> Any k -> Statement
relHomOrientedSlicedFreeStruct :: forall (h :: * -> * -> *) x y (k :: N').
(HomOrientedSlicedFree h, Show2 h) =>
Struct Ort x
-> Struct Ort y
-> Struct SldFr x
-> Struct SldFr y
-> h x y
-> Any k
-> Statement
relHomOrientedSlicedFreeStruct sx :: Struct Ort x
sx@Struct Ort x
Struct sy :: Struct Ort y
sy@Struct Ort y
Struct Struct SldFr x
Struct Struct SldFr y
Struct h x y
h Any k
k = case Any k -> Ats k
forall (n :: N'). Any n -> Ats n
ats Any k
k of
  Ats k
Ats               -> case (Struct Ort x -> Any k -> Struct (Sld (Free k)) x
forall x (k :: N') (q :: * -> *).
(SlicedFree x, Attestable k) =>
q x -> Any k -> Struct (Sld (Free k)) x
slicedFree' Struct Ort x
sx Any k
k,Struct Ort y -> Any k -> Struct (Sld (Free k)) y
forall x (k :: N') (q :: * -> *).
(SlicedFree x, Attestable k) =>
q x -> Any k -> Struct (Sld (Free k)) x
slicedFree' Struct Ort y
sy Any k
k) of
    (Struct (Sld (Free k)) x
Struct,Struct (Sld (Free k)) y
Struct) -> (  h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h (Free k x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint (Free k x -> Point x) -> Free k x -> Point x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct Ort x -> Any k -> Free k x
forall (q :: * -> *) x (k :: N'). q x -> Any k -> Free k x
free' Struct Ort x
sx Any k
k)
                       Point y -> Point y -> Bool
forall a. Eq a => a -> a -> Bool
== (Free k y -> Point y
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint (Free k y -> Point y) -> Free k y -> Point y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct Ort y -> Any k -> Free k y
forall (q :: * -> *) x (k :: N'). q x -> Any k -> Free k x
free' Struct Ort y
sy Any k
k)
                       ) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [ String
"h"String -> String -> Parameter
:=h x y -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h x y
h
                                    , String
"k"String -> String -> Parameter
:=Any k -> String
forall a. Show a => a -> String
show Any k
k
                                    ]

relHomOrientedSlicedFree :: (HomOrientedSlicedFree h, Show2 h)
  => h x y -> Any k -> Statement
relHomOrientedSlicedFree :: forall (h :: * -> * -> *) x y (k :: N').
(HomOrientedSlicedFree h, Show2 h) =>
h x y -> Any k -> Statement
relHomOrientedSlicedFree h x y
h Any k
k
  = Struct Ort x
-> Struct Ort y
-> Struct SldFr x
-> Struct SldFr y
-> h x y
-> Any k
-> Statement
forall (h :: * -> * -> *) x y (k :: N').
(HomOrientedSlicedFree h, Show2 h) =>
Struct Ort x
-> Struct Ort y
-> Struct SldFr x
-> Struct SldFr y
-> h x y
-> Any k
-> Statement
relHomOrientedSlicedFreeStruct
      (Struct (ObjectClass h) x -> Struct Ort x
forall x. Struct (ObjectClass h) x -> Struct Ort x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) x -> Struct Ort x)
-> Struct (ObjectClass h) x -> Struct Ort x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h x y -> Struct (ObjectClass h) x
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 x y
h) (Struct (ObjectClass h) y -> Struct Ort y
forall x. Struct (ObjectClass h) x -> Struct Ort x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) y -> Struct Ort y)
-> Struct (ObjectClass h) y -> Struct Ort y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h x y -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h x y
h) (Struct (ObjectClass h) x -> Struct SldFr x
forall x. Struct (ObjectClass h) x -> Struct SldFr x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) x -> Struct SldFr x)
-> Struct (ObjectClass h) x -> Struct SldFr x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h x y -> Struct (ObjectClass h) x
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 x y
h) (Struct (ObjectClass h) y -> Struct SldFr y
forall x. Struct (ObjectClass h) x -> Struct SldFr x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) y -> Struct SldFr y)
-> Struct (ObjectClass h) y -> Struct SldFr y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h x y -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h x y
h) h x y
h Any k
k

-- | validity according to 'HomOrientedSlicedFree'.

prpHomOrientedSlicedFree :: (HomOrientedSlicedFree h, Show2 h)
  => h x y -> Any k -> Statement
prpHomOrientedSlicedFree :: forall (h :: * -> * -> *) x y (k :: N').
(HomOrientedSlicedFree h, Show2 h) =>
h x y -> Any k -> Statement
prpHomOrientedSlicedFree h x y
h Any k
k = String -> Label
Prp String
"HomOrientedSlicedFree" Label -> Statement -> Statement
:<=>: h x y -> Any k -> Statement
forall (h :: * -> * -> *) x y (k :: N').
(HomOrientedSlicedFree h, Show2 h) =>
h x y -> Any k -> Statement
relHomOrientedSlicedFree h x y
h Any k
k

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

-- sfrMap -


sfrMapStruct :: Struct SldFr y -> Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMapStruct :: forall y (v :: Variant) (h :: * -> * -> *) x.
Struct SldFr y -> Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMapStruct Struct SldFr y
Struct Variant2 v h x y
h (SomeFree (Free Any k
k)) = case Variant2 v h x y -> Any k -> Struct (Sld (Free k)) y
forall x (k :: N') (q :: * -> *).
(SlicedFree x, Attestable k) =>
q x -> Any k -> Struct (Sld (Free k)) x
slicedFree' Variant2 v h x y
h Any k
k of Struct (Sld (Free k)) y
Struct -> Free k y -> SomeFree y
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree (Any k -> Free k y
forall (k :: N') c. Any k -> Free k c
Free Any k
k)

-- | mapping of 'SomeFree'.

sfrMap :: HomOrientedSlicedFree h => Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMap :: forall (h :: * -> * -> *) (v :: Variant) x y.
HomOrientedSlicedFree h =>
Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMap h :: Variant2 v h x y
h@(Covariant2 h x y
hCov)     = Struct SldFr y -> Variant2 v h x y -> SomeFree x -> SomeFree y
forall y (v :: Variant) (h :: * -> * -> *) x.
Struct SldFr y -> Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMapStruct (Struct (ObjectClass h) y -> Struct SldFr y
forall x. Struct (ObjectClass h) x -> Struct SldFr x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) y -> Struct SldFr y)
-> Struct (ObjectClass h) y -> Struct SldFr y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h x y -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h x y
hCov) Variant2 v h x y
h
sfrMap h :: Variant2 v h x y
h@(Contravariant2 h x y
hCnt) = Struct SldFr y -> Variant2 v h x y -> SomeFree x -> SomeFree y
forall y (v :: Variant) (h :: * -> * -> *) x.
Struct SldFr y -> Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMapStruct (Struct (ObjectClass h) y -> Struct SldFr y
forall x. Struct (ObjectClass h) x -> Struct SldFr x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) y -> Struct SldFr y)
-> Struct (ObjectClass h) y -> Struct SldFr y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h x y -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h x y
hCnt) Variant2 v h x y
h

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

-- dgfMapCov -


-- | covariant mapping of 'DiagramFree'.

dgfMapCov :: HomOrientedSlicedFree h
  => Variant2 Covariant h x y -> DiagramFree t n m x -> DiagramFree t n m y
dgfMapCov :: forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Covariant h x y
-> DiagramFree t n m x -> DiagramFree t n m y
dgfMapCov Variant2 'Covariant h x y
h (DiagramFree FinList n (SomeFree x)
fs Diagram t n m x
d) = FinList n (SomeFree y) -> Diagram t n m y -> DiagramFree t n m y
forall (t :: DiagramType) (n :: N') (m :: N') a.
FinList n (SomeFree a) -> Diagram t n m a -> DiagramFree t n m a
DiagramFree FinList n (SomeFree y)
fs' Diagram t n m y
d' where
  fs' :: FinList n (SomeFree y)
fs' = (SomeFree x -> SomeFree y)
-> FinList n (SomeFree x) -> FinList n (SomeFree y)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Variant2 'Covariant h x y -> SomeFree x -> SomeFree y
forall (h :: * -> * -> *) (v :: Variant) x y.
HomOrientedSlicedFree h =>
Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMap Variant2 'Covariant h x y
h) FinList n (SomeFree x)
fs
  d' :: Diagram t n m y
d'  = Variant2 'Covariant h x y -> Diagram t n m x -> Diagram t n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedDisjunctive h =>
Variant2 'Covariant h x y -> Diagram t n m x -> Diagram t n m y
dgMapCov Variant2 'Covariant h x y
h Diagram t n m x
d

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

-- dgfMapCnt -


-- | contravariant mapping of 'DiagramFree'.

dgfMapCnt :: HomOrientedSlicedFree h
  => Variant2 Contravariant h x y -> DiagramFree t n m x -> DiagramFree (Dual t) n m y
dgfMapCnt :: forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Contravariant h x y
-> DiagramFree t n m x -> DiagramFree (Dual t) n m y
dgfMapCnt Variant2 'Contravariant h x y
h (DiagramFree FinList n (SomeFree x)
fs Diagram t n m x
d) = FinList n (SomeFree y)
-> Diagram (Dual t) n m y -> DiagramFree (Dual t) n m y
forall (t :: DiagramType) (n :: N') (m :: N') a.
FinList n (SomeFree a) -> Diagram t n m a -> DiagramFree t n m a
DiagramFree FinList n (SomeFree y)
fs' Dual1 (Diagram t n m) y
Diagram (Dual t) n m y
d' where
  fs' :: FinList n (SomeFree y)
fs' = (SomeFree x -> SomeFree y)
-> FinList n (SomeFree x) -> FinList n (SomeFree y)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Variant2 'Contravariant h x y -> SomeFree x -> SomeFree y
forall (h :: * -> * -> *) (v :: Variant) x y.
HomOrientedSlicedFree h =>
Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMap Variant2 'Contravariant h x y
h) FinList n (SomeFree x)
fs
  d' :: Dual1 (Diagram t n m) y
d'  = Variant2 'Contravariant h x y
-> Diagram t n m x -> Dual1 (Diagram t n m) y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedDisjunctive h =>
Variant2 'Contravariant h x y
-> Diagram t n m x -> Dual1 (Diagram t n m) y
dgMapCnt Variant2 'Contravariant h x y
h Diagram t n m x
d

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

-- DiagramFree - Dual -


type instance Dual1 (DiagramFree t n m) = DiagramFree (Dual t) n m

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

-- dgfMapS -


-- | mapping of 'DiagramFree'.

dgfMapS :: (HomOrientedSlicedFree h, t ~ Dual (Dual t))
  => h x y -> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y
dgfMapS :: forall (h :: * -> * -> *) (t :: DiagramType) x y (n :: N')
       (m :: N').
(HomOrientedSlicedFree h, t ~ Dual (Dual t)) =>
h x y
-> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y
dgfMapS = (Variant2 'Covariant h x y
 -> DiagramFree t n m x -> DiagramFree t n m y)
-> (Variant2 'Covariant h x y
    -> Dual1 (DiagramFree t n m) x -> Dual1 (DiagramFree t n m) y)
-> (Variant2 'Contravariant h x y
    -> DiagramFree t n m x -> Dual1 (DiagramFree t n m) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (DiagramFree t n m) x -> DiagramFree t n m y)
-> h x y
-> SDualBi (DiagramFree t n m) x
-> SDualBi (DiagramFree 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 h x y
-> DiagramFree t n m x -> DiagramFree t n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Covariant h x y
-> DiagramFree t n m x -> DiagramFree t n m y
dgfMapCov Variant2 'Covariant h x y
-> Dual1 (DiagramFree t n m) x -> Dual1 (DiagramFree t n m) y
Variant2 'Covariant h x y
-> DiagramFree (Dual t) n m x -> DiagramFree (Dual t) n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Covariant h x y
-> DiagramFree t n m x -> DiagramFree t n m y
dgfMapCov Variant2 'Contravariant h x y
-> DiagramFree t n m x -> Dual1 (DiagramFree t n m) y
Variant2 'Contravariant h x y
-> DiagramFree t n m x -> DiagramFree (Dual t) n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Contravariant h x y
-> DiagramFree t n m x -> DiagramFree (Dual t) n m y
dgfMapCnt Variant2 'Contravariant h x y
-> Dual1 (DiagramFree t n m) x -> DiagramFree t n m y
Variant2 'Contravariant h x y
-> DiagramFree (Dual t) n m x -> DiagramFree (Dual (Dual t)) n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Contravariant h x y
-> DiagramFree t n m x -> DiagramFree (Dual t) n m y
dgfMapCnt

instance (HomOrientedSlicedFree h, t ~ Dual (Dual t))
  => ApplicativeG (SDualBi (DiagramFree t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y
amapG = h x y
-> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y
forall (h :: * -> * -> *) (t :: DiagramType) x y (n :: N')
       (m :: N').
(HomOrientedSlicedFree h, t ~ Dual (Dual t)) =>
h x y
-> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y
dgfMapS

instance
  ( HomOrientedSlicedFree h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (DiagramFree t n m)) h (->)

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

-- DiagramFree - NaturalDiagrammatic -


instance
  ( HomOrientedSlicedFree h
  , t ~ Dual (Dual t)
  )
  =>  ApplicativeG (SDualBi (DiagramG DiagramFree t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (DiagramG DiagramFree t n m) x
   -> SDualBi (DiagramG DiagramFree t n m) y
amapG h x y
h = SDualBi (DiagramFree t n m) y
-> SDualBi (DiagramG DiagramFree t n m) y
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
(Dual1 (d t n m) ~ d (Dual t) n m) =>
SDualBi (d t n m) x -> SDualBi (DiagramG d t n m) x
sdbFromDgmObj (SDualBi (DiagramFree t n m) y
 -> SDualBi (DiagramG DiagramFree t n m) y)
-> (SDualBi (DiagramG DiagramFree t n m) x
    -> SDualBi (DiagramFree t n m) y)
-> SDualBi (DiagramG DiagramFree t n m) x
-> SDualBi (DiagramG DiagramFree 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
. h x y
-> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y
forall x y.
h x y
-> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h (SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y)
-> (SDualBi (DiagramG DiagramFree t n m) x
    -> SDualBi (DiagramFree t n m) x)
-> SDualBi (DiagramG DiagramFree t n m) x
-> SDualBi (DiagramFree 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 (DiagramG DiagramFree t n m) x
-> SDualBi (DiagramFree t n m) x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
(Dual1 (d t n m) ~ d (Dual t) n m) =>
SDualBi (DiagramG d t n m) x -> SDualBi (d t n m) x
sdbToDgmObj

instance
  ( HomOrientedSlicedFree h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  =>  FunctorialG (SDualBi (DiagramG DiagramFree t n m)) h (->)
  
instance
  ( HomOrientedSlicedFree h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => NaturalTransformable h (->)
       (SDualBi (DiagramG DiagramFree t n m)) (SDualBi (DiagramG Diagram t n m))
instance
  ( CategoryDisjunctive h
  , HomOrientedSlicedFree h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => NaturalDiagrammatic h DiagramFree t n m

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

-- SomeFreeSliceDiagram -


-- | some free slice diagram for kernels and cokernels diagrams.

data SomeFreeSliceDiagram t n m x where
  SomeFreeSliceKernel
    :: (Attestable k, Sliced (Free k) x)
    => Slice From (Free k) x
    -> SomeFreeSliceDiagram (Parallel LeftToRight) N2 N1 x
  SomeFreeSliceCokernel
    :: (Attestable k, Sliced (Free k) x)
    => Slice To (Free k) x
    -> SomeFreeSliceDiagram (Parallel RightToLeft) N2 N1 x

instance Diagrammatic SomeFreeSliceDiagram where
  diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x.
SomeFreeSliceDiagram t n m x -> Diagram t n m x
diagram (SomeFreeSliceKernel (SliceFrom Free k x
_ x
x)) = Point x
-> Point x
-> FinList m x
-> Diagram ('Parallel 'LeftToRight) ('S N1) m x
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR (x -> Point x
forall q. Oriented q => q -> Point q
start x
x) (x -> Point x
forall q. Oriented q => q -> Point q
end x
x) (x
xx -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil)
  diagram (SomeFreeSliceCokernel (SliceTo Free k x
_ x
x)) = Point x
-> Point x
-> FinList m x
-> Diagram ('Parallel 'RightToLeft) ('S N1) m x
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) m a
DiagramParallelRL (x -> Point x
forall q. Oriented q => q -> Point q
end x
x) (x -> Point x
forall q. Oriented q => q -> Point q
start x
x) (x
xx -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil)

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

-- sfsdMapCov -


sfsdMapCovStruct :: HomOrientedSlicedFree h
  => Struct SldFr y -> Variant2 Covariant h x y
  -> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram t n m y
sfsdMapCovStruct :: forall (h :: * -> * -> *) y x (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Struct SldFr y
-> Variant2 'Covariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram t n m y
sfsdMapCovStruct Struct SldFr y
Struct Variant2 'Covariant h x y
h (SomeFreeSliceKernel (SliceFrom (Free Any k
k) x
f))
  = case Variant2 'Covariant h x y -> Any k -> Struct (Sld (Free k)) y
forall x (k :: N') (q :: * -> *).
(SlicedFree x, Attestable k) =>
q x -> Any k -> Struct (Sld (Free k)) x
slicedFree' Variant2 'Covariant h x y
h Any k
k of Struct (Sld (Free k)) y
Struct -> Slice 'From (Free k) y
-> SomeFreeSliceDiagram ('Parallel 'LeftToRight) ('S N1) N1 y
forall (k :: N') x.
(Attestable k, Sliced (Free k) x) =>
Slice 'From (Free k) x
-> SomeFreeSliceDiagram ('Parallel 'LeftToRight) ('S N1) N1 x
SomeFreeSliceKernel (Free k y -> y -> Slice 'From (Free k) y
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom (Any k -> Free k y
forall (k :: N') c. Any k -> Free k c
Free Any k
k) (Variant2 'Covariant h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Variant2 'Covariant h x y
h x
f))
sfsdMapCovStruct Struct SldFr y
Struct Variant2 'Covariant h x y
h (SomeFreeSliceCokernel (SliceTo (Free Any k
k) x
f))
  = case Variant2 'Covariant h x y -> Any k -> Struct (Sld (Free k)) y
forall x (k :: N') (q :: * -> *).
(SlicedFree x, Attestable k) =>
q x -> Any k -> Struct (Sld (Free k)) x
slicedFree' Variant2 'Covariant h x y
h Any k
k of Struct (Sld (Free k)) y
Struct -> Slice 'To (Free k) y
-> SomeFreeSliceDiagram ('Parallel 'RightToLeft) ('S N1) N1 y
forall (k :: N') x.
(Attestable k, Sliced (Free k) x) =>
Slice 'To (Free k) x
-> SomeFreeSliceDiagram ('Parallel 'RightToLeft) ('S N1) N1 x
SomeFreeSliceCokernel (Free k y -> y -> Slice 'To (Free k) y
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo (Any k -> Free k y
forall (k :: N') c. Any k -> Free k c
Free Any k
k) (Variant2 'Covariant h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Variant2 'Covariant h x y
h x
f))

-- | covariant mapping of 'SomeFreeSliceDiagram'.

sfsdMapCov ::HomOrientedSlicedFree h
  => Variant2 Covariant h x y
  -> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram t n m y
sfsdMapCov :: forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Covariant h x y
-> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram t n m y
sfsdMapCov Variant2 'Covariant h x y
h = Struct SldFr y
-> Variant2 'Covariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram t n m y
forall (h :: * -> * -> *) y x (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Struct SldFr y
-> Variant2 'Covariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram t n m y
sfsdMapCovStruct (Struct (ObjectClass h) y -> Struct SldFr y
forall x. Struct (ObjectClass h) x -> Struct SldFr x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) y -> Struct SldFr y)
-> Struct (ObjectClass h) y -> Struct SldFr y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Variant2 'Covariant h x y
-> Struct (ObjectClass (Variant2 'Covariant h)) y
forall x y.
Variant2 'Covariant h x y
-> Struct (ObjectClass (Variant2 'Covariant h)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Covariant h x y
h) Variant2 'Covariant h x y
h
  
--------------------------------------------------------------------------------

-- sfsdMapCnt -


sfsdMapCntStruct :: HomOrientedSlicedFree h
  => Struct SldFr y -> Variant2 Contravariant h x y
  -> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram (Dual t) n m y
sfsdMapCntStruct :: forall (h :: * -> * -> *) y x (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Struct SldFr y
-> Variant2 'Contravariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram (Dual t) n m y
sfsdMapCntStruct Struct SldFr y
Struct Variant2 'Contravariant h x y
h (SomeFreeSliceKernel (SliceFrom (Free Any k
k) x
f))
  = case Variant2 'Contravariant h x y -> Any k -> Struct (Sld (Free k)) y
forall x (k :: N') (q :: * -> *).
(SlicedFree x, Attestable k) =>
q x -> Any k -> Struct (Sld (Free k)) x
slicedFree' Variant2 'Contravariant h x y
h Any k
k of Struct (Sld (Free k)) y
Struct -> Slice 'To (Free k) y
-> SomeFreeSliceDiagram ('Parallel 'RightToLeft) ('S N1) N1 y
forall (k :: N') x.
(Attestable k, Sliced (Free k) x) =>
Slice 'To (Free k) x
-> SomeFreeSliceDiagram ('Parallel 'RightToLeft) ('S N1) N1 x
SomeFreeSliceCokernel (Free k y -> y -> Slice 'To (Free k) y
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo (Any k -> Free k y
forall (k :: N') c. Any k -> Free k c
Free Any k
k) (Variant2 'Contravariant h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Variant2 'Contravariant h x y
h x
f))
sfsdMapCntStruct Struct SldFr y
Struct Variant2 'Contravariant h x y
h (SomeFreeSliceCokernel (SliceTo (Free Any k
k) x
f))
  = case Variant2 'Contravariant h x y -> Any k -> Struct (Sld (Free k)) y
forall x (k :: N') (q :: * -> *).
(SlicedFree x, Attestable k) =>
q x -> Any k -> Struct (Sld (Free k)) x
slicedFree' Variant2 'Contravariant h x y
h Any k
k of Struct (Sld (Free k)) y
Struct -> Slice 'From (Free k) y
-> SomeFreeSliceDiagram ('Parallel 'LeftToRight) ('S N1) N1 y
forall (k :: N') x.
(Attestable k, Sliced (Free k) x) =>
Slice 'From (Free k) x
-> SomeFreeSliceDiagram ('Parallel 'LeftToRight) ('S N1) N1 x
SomeFreeSliceKernel (Free k y -> y -> Slice 'From (Free k) y
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom (Any k -> Free k y
forall (k :: N') c. Any k -> Free k c
Free Any k
k) (Variant2 'Contravariant h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Variant2 'Contravariant h x y
h x
f))

-- | contravariant mapping of 'SomeFreeSliceDiagram'.

sfsdMapCnt ::HomOrientedSlicedFree h
  => Variant2 Contravariant h x y
  -> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram (Dual t) n m y
sfsdMapCnt :: forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Contravariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram (Dual t) n m y
sfsdMapCnt Variant2 'Contravariant h x y
h = Struct SldFr y
-> Variant2 'Contravariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram (Dual t) n m y
forall (h :: * -> * -> *) y x (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Struct SldFr y
-> Variant2 'Contravariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram (Dual t) n m y
sfsdMapCntStruct (Struct (ObjectClass h) y -> Struct SldFr y
forall x. Struct (ObjectClass h) x -> Struct SldFr x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) y -> Struct SldFr y)
-> Struct (ObjectClass h) y -> Struct SldFr y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Variant2 'Contravariant h x y
-> Struct (ObjectClass (Variant2 'Contravariant h)) y
forall x y.
Variant2 'Contravariant h x y
-> Struct (ObjectClass (Variant2 'Contravariant h)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Contravariant h x y
h) Variant2 'Contravariant h x y
h

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

-- Duality -


type instance Dual1 (SomeFreeSliceDiagram t n m) = SomeFreeSliceDiagram (Dual t) n m

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

-- sfsdMapS -


-- | mapping of 'SomeFreeSliceDiagram'.

sfsdMapS :: (HomOrientedSlicedFree h, t ~ Dual (Dual t))
  => h x y -> SDualBi (SomeFreeSliceDiagram t n m) x -> SDualBi (SomeFreeSliceDiagram t n m) y
sfsdMapS :: forall (h :: * -> * -> *) (t :: DiagramType) x y (n :: N')
       (m :: N').
(HomOrientedSlicedFree h, t ~ Dual (Dual t)) =>
h x y
-> SDualBi (SomeFreeSliceDiagram t n m) x
-> SDualBi (SomeFreeSliceDiagram t n m) y
sfsdMapS = (Variant2 'Covariant h x y
 -> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram t n m y)
-> (Variant2 'Covariant h x y
    -> Dual1 (SomeFreeSliceDiagram t n m) x
    -> Dual1 (SomeFreeSliceDiagram t n m) y)
-> (Variant2 'Contravariant h x y
    -> SomeFreeSliceDiagram t n m x
    -> Dual1 (SomeFreeSliceDiagram t n m) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (SomeFreeSliceDiagram t n m) x
    -> SomeFreeSliceDiagram t n m y)
-> h x y
-> SDualBi (SomeFreeSliceDiagram t n m) x
-> SDualBi (SomeFreeSliceDiagram 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 h x y
-> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram t n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Covariant h x y
-> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram t n m y
sfsdMapCov Variant2 'Covariant h x y
-> Dual1 (SomeFreeSliceDiagram t n m) x
-> Dual1 (SomeFreeSliceDiagram t n m) y
Variant2 'Covariant h x y
-> SomeFreeSliceDiagram (Dual t) n m x
-> SomeFreeSliceDiagram (Dual t) n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Covariant h x y
-> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram t n m y
sfsdMapCov Variant2 'Contravariant h x y
-> SomeFreeSliceDiagram t n m x
-> Dual1 (SomeFreeSliceDiagram t n m) y
Variant2 'Contravariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram (Dual t) n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Contravariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram (Dual t) n m y
sfsdMapCnt Variant2 'Contravariant h x y
-> Dual1 (SomeFreeSliceDiagram t n m) x
-> SomeFreeSliceDiagram t n m y
Variant2 'Contravariant h x y
-> SomeFreeSliceDiagram (Dual t) n m x
-> SomeFreeSliceDiagram (Dual (Dual t)) n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedSlicedFree h =>
Variant2 'Contravariant h x y
-> SomeFreeSliceDiagram t n m x
-> SomeFreeSliceDiagram (Dual t) n m y
sfsdMapCnt 

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

-- FunctorialG -


instance (HomOrientedSlicedFree h, t ~ Dual (Dual t))
  => ApplicativeG (SDualBi (SomeFreeSliceDiagram t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (SomeFreeSliceDiagram t n m) x
   -> SDualBi (SomeFreeSliceDiagram t n m) y
amapG = h x y
-> SDualBi (SomeFreeSliceDiagram t n m) x
-> SDualBi (SomeFreeSliceDiagram t n m) y
forall (h :: * -> * -> *) (t :: DiagramType) x y (n :: N')
       (m :: N').
(HomOrientedSlicedFree h, t ~ Dual (Dual t)) =>
h x y
-> SDualBi (SomeFreeSliceDiagram t n m) x
-> SDualBi (SomeFreeSliceDiagram t n m) y
sfsdMapS

instance (HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t))
  => FunctorialG (SDualBi (SomeFreeSliceDiagram t n m)) h (->)

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

-- LiftableFree -


-- | liftable according to a free slice.

data LiftableFree p x where
  LiftableFree :: (forall k . Any k -> Liftable p (Free k) x) -> LiftableFree p x

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

-- liftFree -


-- | lifting a free slice.

liftFree :: LiftableFree p x -> Any k -> Liftable p (Free k) x
liftFree :: forall (p :: Perspective) x (k :: N').
LiftableFree p x -> Any k -> Liftable p (Free k) x
liftFree (LiftableFree forall (k :: N'). Any k -> Liftable p (Free k) x
l) = Any k -> Liftable p (Free k) x
forall (k :: N'). Any k -> Liftable p (Free k) x
l

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

-- lftFrMapIsoOpCov -


lftFrMapIsoOpCovStruct ::
  ( TransformableType s
  , TransformableOp s
  , TransformableMlt s
  , Transformable (s,Sld (Free k)) s
  , SlicedFree x
  , SlicedFree y
  )
  => Struct s x -> Struct s y
  -> Variant2 Covariant (IsoO s Op) x y -> LiftableFree p x -> Any k -> Liftable p (Free k) y
lftFrMapIsoOpCovStruct :: forall s (k :: N') x y (p :: Perspective).
(TransformableType s, TransformableOp s, TransformableMlt s,
 Transformable (s, Sld (Free k)) s, SlicedFree x, SlicedFree y) =>
Struct s x
-> Struct s y
-> Variant2 'Covariant (IsoO s Op) x y
-> LiftableFree p x
-> Any k
-> Liftable p (Free k) y
lftFrMapIsoOpCovStruct Struct s x
sx Struct s y
sy Variant2 'Covariant (IsoO s Op) x y
i LiftableFree p x
lf Any k
k = case Any k -> Ats k
forall (n :: N'). Any n -> Ats n
ats Any k
k of
  Ats k
Ats -> Variant2
  'Covariant (Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op))) x y
-> Liftable p (Free k) x -> Liftable p (Free k) 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 (Any k
-> Struct (s, Sld (Free k)) x
-> Struct (s, Sld (Free k)) y
-> Variant2 'Covariant (IsoO s Op) x y
-> Variant2
     'Covariant (Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op))) x y
forall (q :: N' -> *) (k :: N') s x y (v :: Variant).
q k
-> Struct (s, Sld (Free k)) x
-> Struct (s, Sld (Free k)) y
-> Variant2 v (IsoO s Op) x y
-> Variant2
     v (Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op))) x y
lftFrSub Any k
k Struct (s, Sld (Free k)) x
sfx Struct (s, Sld (Free k)) y
sfy Variant2 'Covariant (IsoO s Op) x y
i) (LiftableFree p x -> Any k -> Liftable p (Free k) x
forall (p :: Perspective) x (k :: N').
LiftableFree p x -> Any k -> Liftable p (Free k) x
liftFree LiftableFree p x
lf Any k
k) where
            sfx :: Struct (s, Sld (Free k)) x
sfx = Struct s x -> Struct (s, Sld (Free k)) x
forall x (k :: N') s.
(SlicedFree x, Attestable k) =>
Struct s x -> Struct (s, Sld (Free k)) x
tauSldFrTuple Struct s x
sx
            sfy :: Struct (s, Sld (Free k)) y
sfy = Struct s y -> Struct (s, Sld (Free k)) y
forall x (k :: N') s.
(SlicedFree x, Attestable k) =>
Struct s x -> Struct (s, Sld (Free k)) x
tauSldFrTuple Struct s y
sy

lftFrMapIsoOpMltCov ::
  ( s ~ Mlt
  , SlicedFree x
  , SlicedFree y
  )
  => Variant2 Covariant (IsoO s Op) x y -> LiftableFree p x -> LiftableFree p y
lftFrMapIsoOpMltCov :: forall s x y (p :: Perspective).
(s ~ Mlt, SlicedFree x, SlicedFree y) =>
Variant2 'Covariant (IsoO s Op) x y
-> LiftableFree p x -> LiftableFree p y
lftFrMapIsoOpMltCov Variant2 'Covariant (IsoO s Op) x y
i LiftableFree p x
lf = (forall (k :: N'). Any k -> Liftable p (Free k) y)
-> LiftableFree p y
forall (p :: Perspective) x.
(forall (k :: N'). Any k -> Liftable p (Free k) x)
-> LiftableFree p x
LiftableFree (Struct s x
-> Struct s y
-> Variant2 'Covariant (IsoO s Op) x y
-> LiftableFree p x
-> Any k
-> Liftable p (Free k) y
forall s (k :: N') x y (p :: Perspective).
(TransformableType s, TransformableOp s, TransformableMlt s,
 Transformable (s, Sld (Free k)) s, SlicedFree x, SlicedFree y) =>
Struct s x
-> Struct s y
-> Variant2 'Covariant (IsoO s Op) x y
-> LiftableFree p x
-> Any k
-> Liftable p (Free k) y
lftFrMapIsoOpCovStruct (Variant2 'Covariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Covariant (IsoO s Op))) x
forall x y.
Variant2 'Covariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Covariant (IsoO s Op))) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Variant2 'Covariant (IsoO s Op) x y
i) (Variant2 'Covariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Covariant (IsoO s Op))) y
forall x y.
Variant2 'Covariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Covariant (IsoO s Op))) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Covariant (IsoO s Op) x y
i) Variant2 'Covariant (IsoO s Op) x y
i LiftableFree p x
lf)

lftFrMapIsoOpDstCov ::
  ( s ~ Dst
  , SlicedFree x
  , SlicedFree y
  )
  => Variant2 Covariant (IsoO s Op) x y -> LiftableFree p x -> LiftableFree p y
lftFrMapIsoOpDstCov :: forall s x y (p :: Perspective).
(s ~ Dst, SlicedFree x, SlicedFree y) =>
Variant2 'Covariant (IsoO s Op) x y
-> LiftableFree p x -> LiftableFree p y
lftFrMapIsoOpDstCov Variant2 'Covariant (IsoO s Op) x y
i LiftableFree p x
lf = (forall (k :: N'). Any k -> Liftable p (Free k) y)
-> LiftableFree p y
forall (p :: Perspective) x.
(forall (k :: N'). Any k -> Liftable p (Free k) x)
-> LiftableFree p x
LiftableFree (Struct s x
-> Struct s y
-> Variant2 'Covariant (IsoO s Op) x y
-> LiftableFree p x
-> Any k
-> Liftable p (Free k) y
forall s (k :: N') x y (p :: Perspective).
(TransformableType s, TransformableOp s, TransformableMlt s,
 Transformable (s, Sld (Free k)) s, SlicedFree x, SlicedFree y) =>
Struct s x
-> Struct s y
-> Variant2 'Covariant (IsoO s Op) x y
-> LiftableFree p x
-> Any k
-> Liftable p (Free k) y
lftFrMapIsoOpCovStruct (Variant2 'Covariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Covariant (IsoO s Op))) x
forall x y.
Variant2 'Covariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Covariant (IsoO s Op))) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Variant2 'Covariant (IsoO s Op) x y
i) (Variant2 'Covariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Covariant (IsoO s Op))) y
forall x y.
Variant2 'Covariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Covariant (IsoO s Op))) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Covariant (IsoO s Op) x y
i) Variant2 'Covariant (IsoO s Op) x y
i LiftableFree p x
lf)

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

-- lftFrMapIsoOpCnt -


lftFrMapIsoOpCntStruct ::
  ( TransformableType s
  , TransformableOp s
  , TransformableMlt s
  , Transformable (s,Sld (Free k)) s
  , SlicedFree x
  , SlicedFree y
  )
  => Struct s x -> Struct s y
  -> Variant2 Contravariant (IsoO s Op) x y -> LiftableFree p x
  -> Any k -> Liftable (Dual p) (Free k) y
lftFrMapIsoOpCntStruct :: forall s (k :: N') x y (p :: Perspective).
(TransformableType s, TransformableOp s, TransformableMlt s,
 Transformable (s, Sld (Free k)) s, SlicedFree x, SlicedFree y) =>
Struct s x
-> Struct s y
-> Variant2 'Contravariant (IsoO s Op) x y
-> LiftableFree p x
-> Any k
-> Liftable (Dual p) (Free k) y
lftFrMapIsoOpCntStruct Struct s x
sx Struct s y
sy Variant2 'Contravariant (IsoO s Op) x y
i LiftableFree p x
lf Any k
k = case Any k -> Ats k
forall (n :: N'). Any n -> Ats n
ats Any k
k of
  Ats k
Ats -> Variant2
  'Contravariant
  (Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op)))
  x
  y
-> Liftable p (Free k) x -> Liftable (Dual p) (Free k) 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 (Any k
-> Struct (s, Sld (Free k)) x
-> Struct (s, Sld (Free k)) y
-> Variant2 'Contravariant (IsoO s Op) x y
-> Variant2
     'Contravariant
     (Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op)))
     x
     y
forall (q :: N' -> *) (k :: N') s x y (v :: Variant).
q k
-> Struct (s, Sld (Free k)) x
-> Struct (s, Sld (Free k)) y
-> Variant2 v (IsoO s Op) x y
-> Variant2
     v (Inv2 (Sub (s, Sld (Free k)) (HomDisjEmpty s Op))) x y
lftFrSub Any k
k Struct (s, Sld (Free k)) x
sfx Struct (s, Sld (Free k)) y
sfy Variant2 'Contravariant (IsoO s Op) x y
i) (LiftableFree p x -> Any k -> Liftable p (Free k) x
forall (p :: Perspective) x (k :: N').
LiftableFree p x -> Any k -> Liftable p (Free k) x
liftFree LiftableFree p x
lf Any k
k) where
           sfx :: Struct (s, Sld (Free k)) x
sfx = Struct s x -> Struct (s, Sld (Free k)) x
forall x (k :: N') s.
(SlicedFree x, Attestable k) =>
Struct s x -> Struct (s, Sld (Free k)) x
tauSldFrTuple Struct s x
sx
           sfy :: Struct (s, Sld (Free k)) y
sfy = Struct s y -> Struct (s, Sld (Free k)) y
forall x (k :: N') s.
(SlicedFree x, Attestable k) =>
Struct s x -> Struct (s, Sld (Free k)) x
tauSldFrTuple Struct s y
sy

lftFrMapIsoOpMltCnt ::
  ( s ~ Mlt
  , SlicedFree x
  , SlicedFree y
  )
  => Variant2 Contravariant (IsoO s Op) x y -> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapIsoOpMltCnt :: forall s x y (p :: Perspective).
(s ~ Mlt, SlicedFree x, SlicedFree y) =>
Variant2 'Contravariant (IsoO s Op) x y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapIsoOpMltCnt Variant2 'Contravariant (IsoO s Op) x y
i LiftableFree p x
lf = (forall (k :: N'). Any k -> Liftable (Dual p) (Free k) y)
-> LiftableFree (Dual p) y
forall (p :: Perspective) x.
(forall (k :: N'). Any k -> Liftable p (Free k) x)
-> LiftableFree p x
LiftableFree (Struct s x
-> Struct s y
-> Variant2 'Contravariant (IsoO s Op) x y
-> LiftableFree p x
-> W k
-> Liftable (Dual p) (Free k) y
forall s (k :: N') x y (p :: Perspective).
(TransformableType s, TransformableOp s, TransformableMlt s,
 Transformable (s, Sld (Free k)) s, SlicedFree x, SlicedFree y) =>
Struct s x
-> Struct s y
-> Variant2 'Contravariant (IsoO s Op) x y
-> LiftableFree p x
-> Any k
-> Liftable (Dual p) (Free k) y
lftFrMapIsoOpCntStruct (Variant2 'Contravariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Contravariant (IsoO s Op))) x
forall x y.
Variant2 'Contravariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Contravariant (IsoO s Op))) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Variant2 'Contravariant (IsoO s Op) x y
i) (Variant2 'Contravariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Contravariant (IsoO s Op))) y
forall x y.
Variant2 'Contravariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Contravariant (IsoO s Op))) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Contravariant (IsoO s Op) x y
i) Variant2 'Contravariant (IsoO s Op) x y
i LiftableFree p x
lf)

lftFrMapIsoOpDstCnt ::
  ( s ~ Dst
  , SlicedFree x
  , SlicedFree y
  )
  => Variant2 Contravariant (IsoO s Op) x y -> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapIsoOpDstCnt :: forall s x y (p :: Perspective).
(s ~ Dst, SlicedFree x, SlicedFree y) =>
Variant2 'Contravariant (IsoO s Op) x y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapIsoOpDstCnt Variant2 'Contravariant (IsoO s Op) x y
i LiftableFree p x
lf = (forall (k :: N'). Any k -> Liftable (Dual p) (Free k) y)
-> LiftableFree (Dual p) y
forall (p :: Perspective) x.
(forall (k :: N'). Any k -> Liftable p (Free k) x)
-> LiftableFree p x
LiftableFree (Struct s x
-> Struct s y
-> Variant2 'Contravariant (IsoO s Op) x y
-> LiftableFree p x
-> W k
-> Liftable (Dual p) (Free k) y
forall s (k :: N') x y (p :: Perspective).
(TransformableType s, TransformableOp s, TransformableMlt s,
 Transformable (s, Sld (Free k)) s, SlicedFree x, SlicedFree y) =>
Struct s x
-> Struct s y
-> Variant2 'Contravariant (IsoO s Op) x y
-> LiftableFree p x
-> Any k
-> Liftable (Dual p) (Free k) y
lftFrMapIsoOpCntStruct (Variant2 'Contravariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Contravariant (IsoO s Op))) x
forall x y.
Variant2 'Contravariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Contravariant (IsoO s Op))) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Variant2 'Contravariant (IsoO s Op) x y
i) (Variant2 'Contravariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Contravariant (IsoO s Op))) y
forall x y.
Variant2 'Contravariant (IsoO s Op) x y
-> Struct (ObjectClass (Variant2 'Contravariant (IsoO s Op))) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Contravariant (IsoO s Op) x y
i) Variant2 'Contravariant (IsoO s Op) x y
i LiftableFree p x
lf)

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

-- HomFree -


-- | homomorphism between free sliced structures.

type HomFree s = Sub (s,SldFr) (HomDisjEmpty s Op)

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

instance
  ( TransformableOrt s
  , TransformableType s
  , TransformableOp s
  ) => HomOrientedSlicedFree (HomFree s)

instance HomOrientedSlicedFree (Inv2 (HomFree Mlt))
instance HomOrientedSlicedFree (Inv2 (HomFree Dst))

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

-- lftFrMapCov -


-- | covariant mapping of 'LiftableFree'.

lftFrMapMltCov :: Variant2 Covariant (Inv2 (HomFree Mlt)) x y -> LiftableFree p x -> LiftableFree p y
lftFrMapMltCov :: forall x y (p :: Perspective).
Variant2
  'Covariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree p x -> LiftableFree p y
lftFrMapMltCov (Covariant2 Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
i) = case (Struct (Mlt, SldFr) x -> Struct SldFr x
forall s t x. Struct (s, t) x -> Struct t x
tauSnd (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt)))))
     x
forall x y.
Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt)))))
     x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
i),Struct (Mlt, SldFr) y -> Struct SldFr y
forall s t x. Struct (s, t) x -> Struct t x
tauSnd (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt)))))
     y
forall x y.
Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt)))))
     y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
i)) of
  (Struct SldFr x
Struct,Struct SldFr y
Struct) -> Variant2 'Covariant (IsoO Mlt Op) x y
-> LiftableFree p x -> LiftableFree p y
forall s x y (p :: Perspective).
(s ~ Mlt, SlicedFree x, SlicedFree y) =>
Variant2 'Covariant (IsoO s Op) x y
-> LiftableFree p x -> LiftableFree p y
lftFrMapIsoOpMltCov (IsoO Mlt Op x y -> Variant2 'Covariant (IsoO Mlt Op) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> IsoO Mlt Op x y
forall s (h :: * -> * -> *) x y. Inv2 (Sub s h) x y -> Inv2 h x y
inv2Forget Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
i))

-- | covariant mapping of 'LiftableFree'.

lftFrMapDstCov :: Variant2 Covariant (Inv2 (HomFree Dst)) x y -> LiftableFree p x -> LiftableFree p y
lftFrMapDstCov :: forall x y (p :: Perspective).
Variant2
  'Covariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree p x -> LiftableFree p y
lftFrMapDstCov (Covariant2 Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
i) = case (Struct (Dst, SldFr) x -> Struct SldFr x
forall s t x. Struct (s, t) x -> Struct t x
tauSnd (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst)))))
     x
forall x y.
Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst)))))
     x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
i),Struct (Dst, SldFr) y -> Struct SldFr y
forall s t x. Struct (s, t) x -> Struct t x
tauSnd (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst)))))
     y
forall x y.
Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst)))))
     y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
i)) of
  (Struct SldFr x
Struct,Struct SldFr y
Struct) -> Variant2 'Covariant (IsoO Dst Op) x y
-> LiftableFree p x -> LiftableFree p y
forall s x y (p :: Perspective).
(s ~ Dst, SlicedFree x, SlicedFree y) =>
Variant2 'Covariant (IsoO s Op) x y
-> LiftableFree p x -> LiftableFree p y
lftFrMapIsoOpDstCov (IsoO Dst Op x y -> Variant2 'Covariant (IsoO Dst Op) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> IsoO Dst Op x y
forall s (h :: * -> * -> *) x y. Inv2 (Sub s h) x y -> Inv2 h x y
inv2Forget Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
i))

-- | contravariant mapping of 'LiftableFree'.

lftFrMapMltCnt :: Variant2 Contravariant (Inv2 (HomFree Mlt)) x y
  -> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapMltCnt :: forall x y (p :: Perspective).
Variant2
  'Contravariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapMltCnt (Contravariant2 Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
i) = case (Struct (Mlt, SldFr) x -> Struct SldFr x
forall s t x. Struct (s, t) x -> Struct t x
tauSnd (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt)))))
     x
forall x y.
Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt)))))
     x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
i),Struct (Mlt, SldFr) y -> Struct SldFr y
forall s t x. Struct (s, t) x -> Struct t x
tauSnd (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt)))))
     y
forall x y.
Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt)))))
     y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
i)) of
  (Struct SldFr x
Struct,Struct SldFr y
Struct) -> Variant2 'Contravariant (IsoO Mlt Op) x y
-> LiftableFree p x -> LiftableFree (Dual p) y
forall s x y (p :: Perspective).
(s ~ Mlt, SlicedFree x, SlicedFree y) =>
Variant2 'Contravariant (IsoO s Op) x y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapIsoOpMltCnt (IsoO Mlt Op x y -> Variant2 'Contravariant (IsoO Mlt Op) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> IsoO Mlt Op x y
forall s (h :: * -> * -> *) x y. Inv2 (Sub s h) x y -> Inv2 h x y
inv2Forget Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
i))

-- | contravariant mapping of 'LiftableFree'.

lftFrMapDstCnt :: Variant2 Contravariant (Inv2 (HomFree Dst)) x y
  -> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapDstCnt :: forall x y (p :: Perspective).
Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapDstCnt (Contravariant2 Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
i) = case (Struct (Dst, SldFr) x -> Struct SldFr x
forall s t x. Struct (s, t) x -> Struct t x
tauSnd (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst)))))
     x
forall x y.
Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst)))))
     x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
i),Struct (Dst, SldFr) y -> Struct SldFr y
forall s t x. Struct (s, t) x -> Struct t x
tauSnd (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst)))))
     y
forall x y.
Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> Struct
     (ObjectClass
        (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst)))))
     y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
i)) of
  (Struct SldFr x
Struct,Struct SldFr y
Struct) -> Variant2 'Contravariant (IsoO Dst Op) x y
-> LiftableFree p x -> LiftableFree (Dual p) y
forall s x y (p :: Perspective).
(s ~ Dst, SlicedFree x, SlicedFree y) =>
Variant2 'Contravariant (IsoO s Op) x y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapIsoOpDstCnt (IsoO Dst Op x y -> Variant2 'Contravariant (IsoO Dst Op) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> IsoO Dst Op x y
forall s (h :: * -> * -> *) x y. Inv2 (Sub s h) x y -> Inv2 h x y
inv2Forget Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
i))

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

-- Duality - LiftableFree -


type instance Dual1 (LiftableFree p) = LiftableFree (Dual p)

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

-- lftFrMapS -


-- | mapping of 'LiftableFree'.

lftFrMapSMlt :: p ~ Dual (Dual p)
  => Inv2 (HomFree Mlt) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
lftFrMapSMlt :: forall (p :: Perspective) x y.
(p ~ Dual (Dual p)) =>
Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
lftFrMapSMlt = (Variant2
   'Covariant
   (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
   x
   y
 -> LiftableFree p x -> LiftableFree p y)
-> (Variant2
      'Covariant
      (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
      x
      y
    -> Dual1 (LiftableFree p) x -> Dual1 (LiftableFree p) y)
-> (Variant2
      'Contravariant
      (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
      x
      y
    -> LiftableFree p x -> Dual1 (LiftableFree p) y)
-> (Variant2
      'Contravariant
      (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
      x
      y
    -> Dual1 (LiftableFree p) x -> LiftableFree p y)
-> Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> SDualBi (LiftableFree p) x
-> SDualBi (LiftableFree p) 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 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree p x -> LiftableFree p y
forall x y (p :: Perspective).
Variant2
  'Covariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree p x -> LiftableFree p y
lftFrMapMltCov Variant2
  'Covariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> Dual1 (LiftableFree p) x -> Dual1 (LiftableFree p) y
Variant2
  'Covariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree (Dual p) x -> LiftableFree (Dual p) y
forall x y (p :: Perspective).
Variant2
  'Covariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree p x -> LiftableFree p y
lftFrMapMltCov Variant2
  'Contravariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree p x -> Dual1 (LiftableFree p) y
Variant2
  'Contravariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree p x -> LiftableFree (Dual p) y
forall x y (p :: Perspective).
Variant2
  'Contravariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapMltCnt Variant2
  'Contravariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> Dual1 (LiftableFree p) x -> LiftableFree p y
Variant2
  'Contravariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree (Dual p) x -> LiftableFree (Dual (Dual p)) y
forall x y (p :: Perspective).
Variant2
  'Contravariant
  (Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))))
  x
  y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapMltCnt

-- | mapping of 'LiftableFree'.

lftFrMapSDst :: p ~ Dual (Dual p)
  => Inv2 (HomFree Dst) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
lftFrMapSDst :: forall (p :: Perspective) x y.
(p ~ Dual (Dual p)) =>
Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
lftFrMapSDst = (Variant2
   'Covariant
   (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
   x
   y
 -> LiftableFree p x -> LiftableFree p y)
-> (Variant2
      'Covariant
      (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
      x
      y
    -> Dual1 (LiftableFree p) x -> Dual1 (LiftableFree p) y)
-> (Variant2
      'Contravariant
      (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
      x
      y
    -> LiftableFree p x -> Dual1 (LiftableFree p) y)
-> (Variant2
      'Contravariant
      (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
      x
      y
    -> Dual1 (LiftableFree p) x -> LiftableFree p y)
-> Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> SDualBi (LiftableFree p) x
-> SDualBi (LiftableFree p) 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 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree p x -> LiftableFree p y
forall x y (p :: Perspective).
Variant2
  'Covariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree p x -> LiftableFree p y
lftFrMapDstCov Variant2
  'Covariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> Dual1 (LiftableFree p) x -> Dual1 (LiftableFree p) y
Variant2
  'Covariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree (Dual p) x -> LiftableFree (Dual p) y
forall x y (p :: Perspective).
Variant2
  'Covariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree p x -> LiftableFree p y
lftFrMapDstCov Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree p x -> Dual1 (LiftableFree p) y
Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree p x -> LiftableFree (Dual p) y
forall x y (p :: Perspective).
Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapDstCnt Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> Dual1 (LiftableFree p) x -> LiftableFree p y
Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree (Dual p) x -> LiftableFree (Dual (Dual p)) y
forall x y (p :: Perspective).
Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  y
-> LiftableFree p x -> LiftableFree (Dual p) y
lftFrMapDstCnt

instance p ~ Dual (Dual p) => ApplicativeG (SDualBi (LiftableFree p)) (Inv2 (HomFree Mlt)) (->) where
  amapG :: forall x y.
Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
amapG = Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
forall (p :: Perspective) x y.
(p ~ Dual (Dual p)) =>
Inv2 (Sub (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt))) x y
-> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
lftFrMapSMlt

instance p ~ Dual (Dual p) => FunctorialG (SDualBi (LiftableFree p)) (Inv2 (HomFree Mlt)) (->)

instance p ~ Dual (Dual p) => ApplicativeG (SDualBi (LiftableFree p)) (Inv2 (HomFree Dst)) (->) where
  amapG :: forall x y.
Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
amapG = Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
forall (p :: Perspective) x y.
(p ~ Dual (Dual p)) =>
Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
lftFrMapSDst

instance p ~ Dual (Dual p) => FunctorialG (SDualBi (LiftableFree p)) (Inv2 (HomFree Dst)) (->)

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

-- ConeLiftable -


-- | predicate for a liftable conic object.

--

-- __Property__ Let @cl@ be in @'ConeLiftable' __s p d t n m x__@, then holds:

--

-- (1) If @cl@ matches @'ConeKernelLiftable' c ('LiftableFree' l)@, then

-- for any @k@ in @'Any' __k__@ holds:

-- @'lftbBase' (l k)' '==' 'kernelFactor' c@.

--

-- (2) If @cl@ matches @'ConeCokernelLiftable' c ('LiftableFree' l)@, then

-- for any @k@ in @'Any' __k__@ holds:

-- @'lftbBase' (l k)' '==' 'cokernelFactor' c@.

data ConeLiftable s p d t n m x where
  ConeKernelLiftable
    :: KernelConic Cone d N1 x
    -> LiftableFree Projective x
    -> ConeLiftable Dst Projective d (Parallel LeftToRight) N2 N1 x
  ConeCokernelLiftable
    :: CokernelConic Cone d N1 x
    -> LiftableFree Injective x
    -> ConeLiftable Dst Injective d (Parallel RightToLeft) N2 N1 x

instance Conic ConeLiftable where
  cone :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
ConeLiftable s p d t n m x -> Cone s p d t n m x
cone (ConeKernelLiftable KernelConic Cone d N1 x
c LiftableFree 'Projective x
_)   = Cone s p d t n m x
KernelConic Cone d N1 x
c
  cone (ConeCokernelLiftable CokernelConic Cone d N1 x
c LiftableFree 'Injective x
_) = Cone s p d t n m x
CokernelConic Cone d N1 x
c


instance Show (d t n m x) => Show (ConeLiftable s p d t n m x) where
  show :: ConeLiftable s p d t n m x -> String
show (ConeKernelLiftable KernelConic Cone d N1 x
k LiftableFree 'Projective x
_) = String
"ConeKernelLiftable (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ KernelConic Cone d N1 x -> String
forall a. Show a => a -> String
show KernelConic Cone d N1 x
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") lftb"
  show (ConeCokernelLiftable CokernelConic Cone d N1 x
k LiftableFree 'Injective x
_) = String
"ConeCokernelLiftable (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CokernelConic Cone d N1 x -> String
forall a. Show a => a -> String
show CokernelConic Cone d N1 x
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") lftb"
  
--------------------------------------------------------------------------------

-- cnLiftable -


-- | the underlying liftable.

cnLiftable :: ConeLiftable s p d t n m x -> LiftableFree p x
cnLiftable :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
ConeLiftable s p d t n m x -> LiftableFree p x
cnLiftable (ConeKernelLiftable KernelConic Cone d N1 x
_ LiftableFree 'Projective x
lft)   = LiftableFree p x
LiftableFree 'Projective x
lft
cnLiftable (ConeCokernelLiftable CokernelConic Cone d N1 x
_ LiftableFree 'Injective x
lft) = LiftableFree p x
LiftableFree 'Injective x
lft

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

-- cnlMapCov -


-- | covariant mapping of 'ConeLiftable'.

cnlMapCov ::
  ( NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel LeftToRight) N2 N1
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel RightToLeft) N2 N1
  )
  => Variant2 Covariant (Inv2 (HomFree s)) x y
  -> ConeLiftable s p d t n m x -> ConeLiftable s p d t n m y
cnlMapCov :: forall s (d :: DiagramType -> N' -> N' -> * -> *) x y
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) ('S N1) N1,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) ('S N1) N1) =>
Variant2 'Covariant (Inv2 (HomFree s)) x y
-> ConeLiftable s p d t n m x -> ConeLiftable s p d t n m y
cnlMapCov (Covariant2 Inv2 (HomFree s) x y
i) (ConeKernelLiftable KernelConic Cone d N1 x
k LiftableFree 'Projective x
l) = KernelConic Cone d N1 y
-> LiftableFree 'Projective y
-> ConeLiftable
     Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1 y
forall (d :: DiagramType -> N' -> N' -> * -> *) x.
KernelConic Cone d N1 x
-> LiftableFree 'Projective x
-> ConeLiftable
     Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1 x
ConeKernelLiftable KernelConic Cone d N1 y
k' LiftableFree 'Projective y
l' where
  SDualBi (Right1 KernelConic Cone d N1 y
k') = Inv2 (HomFree s) x y
-> SDualBi
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) y
forall x y.
Inv2 (HomFree s) x y
-> SDualBi
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Projective d ('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 (HomFree s) x y
i (Either1
  (Dual1
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1))
  (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1)
  x
-> SDualBi
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (KernelConic Cone d N1 x
-> Either1
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 KernelConic Cone d N1 x
k))
  SDualBi (Right1 LiftableFree 'Projective y
l') = Inv2 (HomFree s) x y
-> SDualBi (LiftableFree 'Projective) x
-> SDualBi (LiftableFree 'Projective) y
forall x y.
Inv2 (HomFree s) x y
-> SDualBi (LiftableFree 'Projective) x
-> SDualBi (LiftableFree 'Projective) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 (HomFree s) x y
i (Either1
  (Dual1 (LiftableFree 'Projective)) (LiftableFree 'Projective) x
-> SDualBi (LiftableFree 'Projective) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LiftableFree 'Projective x
-> Either1 (LiftableFree 'Injective) (LiftableFree 'Projective) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LiftableFree 'Projective x
l))
cnlMapCov (Covariant2 Inv2 (HomFree s) x y
i) (ConeCokernelLiftable CokernelConic Cone d N1 x
k LiftableFree 'Injective x
l) = CokernelConic Cone d N1 y
-> LiftableFree 'Injective y
-> ConeLiftable
     Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1 y
forall (d :: DiagramType -> N' -> N' -> * -> *) x.
CokernelConic Cone d N1 x
-> LiftableFree 'Injective x
-> ConeLiftable
     Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1 x
ConeCokernelLiftable CokernelConic Cone d N1 y
k' LiftableFree 'Injective y
l' where
  SDualBi (Right1 CokernelConic Cone d N1 y
k') = Inv2 (HomFree s) x y
-> SDualBi
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) y
forall x y.
Inv2 (HomFree s) x y
-> SDualBi
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Injective d ('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 (HomFree s) x y
i (Either1
  (Dual1 (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1))
  (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
  x
-> SDualBi
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (CokernelConic Cone d N1 x
-> Either1
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1)
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 CokernelConic Cone d N1 x
k))
  SDualBi (Right1 LiftableFree 'Injective y
l') = Inv2 (HomFree s) x y
-> SDualBi (LiftableFree 'Injective) x
-> SDualBi (LiftableFree 'Injective) y
forall x y.
Inv2 (HomFree s) x y
-> SDualBi (LiftableFree 'Injective) x
-> SDualBi (LiftableFree 'Injective) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 (HomFree s) x y
i (Either1
  (Dual1 (LiftableFree 'Injective)) (LiftableFree 'Injective) x
-> SDualBi (LiftableFree 'Injective) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LiftableFree 'Injective x
-> Either1 (LiftableFree 'Projective) (LiftableFree 'Injective) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LiftableFree 'Injective x
l))

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

-- cnlMapCnt -


-- | contravariant mapping of 'ConeLiftable'.

cnlMapCnt ::
  ( NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel LeftToRight) N2 N1
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel RightToLeft) N2 N1
  )
  => Variant2 Contravariant (Inv2 (HomFree s)) x y
  -> ConeLiftable s p d t n m x -> ConeLiftable s (Dual p) d (Dual t) n m y
cnlMapCnt :: forall s (d :: DiagramType -> N' -> N' -> * -> *) x y
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) ('S N1) N1,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) ('S N1) N1) =>
Variant2 'Contravariant (Inv2 (HomFree s)) x y
-> ConeLiftable s p d t n m x
-> ConeLiftable s (Dual p) d (Dual t) n m y
cnlMapCnt (Contravariant2 Inv2 (HomFree s) x y
i) (ConeKernelLiftable KernelConic Cone d N1 x
k LiftableFree 'Projective x
l) = CokernelConic Cone d N1 y
-> LiftableFree 'Injective y
-> ConeLiftable
     Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1 y
forall (d :: DiagramType -> N' -> N' -> * -> *) x.
CokernelConic Cone d N1 x
-> LiftableFree 'Injective x
-> ConeLiftable
     Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1 x
ConeCokernelLiftable Dual1
  (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) y
CokernelConic Cone d N1 y
k' Dual1 (LiftableFree 'Projective) y
LiftableFree 'Injective y
l' where
  SDualBi (Left1 Dual1
  (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) y
k') = Inv2 (HomFree s) x y
-> SDualBi
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) y
forall x y.
Inv2 (HomFree s) x y
-> SDualBi
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Projective d ('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 (HomFree s) x y
i (Either1
  (Dual1
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1))
  (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1)
  x
-> SDualBi
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (KernelConic Cone d N1 x
-> Either1
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 KernelConic Cone d N1 x
k))
  SDualBi (Left1 Dual1 (LiftableFree 'Projective) y
l') = Inv2 (HomFree s) x y
-> SDualBi (LiftableFree 'Projective) x
-> SDualBi (LiftableFree 'Projective) y
forall x y.
Inv2 (HomFree s) x y
-> SDualBi (LiftableFree 'Projective) x
-> SDualBi (LiftableFree 'Projective) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 (HomFree s) x y
i (Either1
  (Dual1 (LiftableFree 'Projective)) (LiftableFree 'Projective) x
-> SDualBi (LiftableFree 'Projective) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LiftableFree 'Projective x
-> Either1 (LiftableFree 'Injective) (LiftableFree 'Projective) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LiftableFree 'Projective x
l))
cnlMapCnt (Contravariant2 Inv2 (HomFree s) x y
i) (ConeCokernelLiftable CokernelConic Cone d N1 x
k LiftableFree 'Injective x
l) = KernelConic Cone d N1 y
-> LiftableFree 'Projective y
-> ConeLiftable
     Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1 y
forall (d :: DiagramType -> N' -> N' -> * -> *) x.
KernelConic Cone d N1 x
-> LiftableFree 'Projective x
-> ConeLiftable
     Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1 x
ConeKernelLiftable Dual1 (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) y
KernelConic Cone d N1 y
k' Dual1 (LiftableFree 'Injective) y
LiftableFree 'Projective y
l' where
  SDualBi (Left1 Dual1 (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) y
k') = Inv2 (HomFree s) x y
-> SDualBi
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) y
forall x y.
Inv2 (HomFree s) x y
-> SDualBi
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) x
-> SDualBi
     (Cone Dst 'Injective d ('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 (HomFree s) x y
i (Either1
  (Dual1 (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1))
  (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
  x
-> SDualBi
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (CokernelConic Cone d N1 x
-> Either1
     (Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1)
     (Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 CokernelConic Cone d N1 x
k))
  SDualBi (Left1 Dual1 (LiftableFree 'Injective) y
l') = Inv2 (HomFree s) x y
-> SDualBi (LiftableFree 'Injective) x
-> SDualBi (LiftableFree 'Injective) y
forall x y.
Inv2 (HomFree s) x y
-> SDualBi (LiftableFree 'Injective) x
-> SDualBi (LiftableFree 'Injective) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 (HomFree s) x y
i (Either1
  (Dual1 (LiftableFree 'Injective)) (LiftableFree 'Injective) x
-> SDualBi (LiftableFree 'Injective) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LiftableFree 'Injective x
-> Either1 (LiftableFree 'Projective) (LiftableFree 'Injective) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LiftableFree 'Injective x
l))

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

-- ConeLiftable - Dual -


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

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

-- cnlMapS -


-- | mapping of 'ConeLiftable'.

cnlMapS ::
  ( NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel LeftToRight) N2 N1
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel RightToLeft) N2 N1
  , p ~ Dual (Dual p)
  , t ~ Dual (Dual t)
  )
  => Inv2 (HomFree s) x y
  -> SDualBi (ConeLiftable s p d t n m) x -> SDualBi (ConeLiftable s p d t n m) y
cnlMapS :: forall s (d :: DiagramType -> N' -> N' -> * -> *)
       (p :: Perspective) (t :: DiagramType) x y (n :: N') (m :: N').
(NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) ('S N1) N1,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) ('S N1) N1,
 p ~ Dual (Dual p), t ~ Dual (Dual t)) =>
Inv2 (HomFree s) x y
-> SDualBi (ConeLiftable s p d t n m) x
-> SDualBi (ConeLiftable s p d t n m) y
cnlMapS = (Variant2 'Covariant (Inv2 (HomFree s)) x y
 -> ConeLiftable s p d t n m x -> ConeLiftable s p d t n m y)
-> (Variant2 'Covariant (Inv2 (HomFree s)) x y
    -> Dual1 (ConeLiftable s p d t n m) x
    -> Dual1 (ConeLiftable s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 (HomFree s)) x y
    -> ConeLiftable s p d t n m x
    -> Dual1 (ConeLiftable s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 (HomFree s)) x y
    -> Dual1 (ConeLiftable s p d t n m) x
    -> ConeLiftable s p d t n m y)
-> Inv2 (HomFree s) x y
-> SDualBi (ConeLiftable s p d t n m) x
-> SDualBi (ConeLiftable 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 (HomFree s)) x y
-> ConeLiftable s p d t n m x -> ConeLiftable s p d t n m y
forall s (d :: DiagramType -> N' -> N' -> * -> *) x y
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) ('S N1) N1,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) ('S N1) N1) =>
Variant2 'Covariant (Inv2 (HomFree s)) x y
-> ConeLiftable s p d t n m x -> ConeLiftable s p d t n m y
cnlMapCov Variant2 'Covariant (Inv2 (HomFree s)) x y
-> Dual1 (ConeLiftable s p d t n m) x
-> Dual1 (ConeLiftable s p d t n m) y
Variant2 'Covariant (Inv2 (HomFree s)) x y
-> ConeLiftable s (Dual p) d (Dual t) n m x
-> ConeLiftable s (Dual p) d (Dual t) n m y
forall s (d :: DiagramType -> N' -> N' -> * -> *) x y
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) ('S N1) N1,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) ('S N1) N1) =>
Variant2 'Covariant (Inv2 (HomFree s)) x y
-> ConeLiftable s p d t n m x -> ConeLiftable s p d t n m y
cnlMapCov Variant2 'Contravariant (Inv2 (HomFree s)) x y
-> ConeLiftable s p d t n m x -> Dual1 (ConeLiftable s p d t n m) y
Variant2 'Contravariant (Inv2 (HomFree s)) x y
-> ConeLiftable s p d t n m x
-> ConeLiftable s (Dual p) d (Dual t) n m y
forall s (d :: DiagramType -> N' -> N' -> * -> *) x y
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) ('S N1) N1,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) ('S N1) N1) =>
Variant2 'Contravariant (Inv2 (HomFree s)) x y
-> ConeLiftable s p d t n m x
-> ConeLiftable s (Dual p) d (Dual t) n m y
cnlMapCnt Variant2 'Contravariant (Inv2 (HomFree s)) x y
-> Dual1 (ConeLiftable s p d t n m) x -> ConeLiftable s p d t n m y
Variant2 'Contravariant (Inv2 (HomFree s)) x y
-> ConeLiftable s (Dual p) d (Dual t) n m x
-> ConeLiftable s (Dual (Dual p)) d (Dual (Dual t)) n m y
forall s (d :: DiagramType -> N' -> N' -> * -> *) x y
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) ('S N1) N1,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) ('S N1) N1) =>
Variant2 'Contravariant (Inv2 (HomFree s)) x y
-> ConeLiftable s p d t n m x
-> ConeLiftable s (Dual p) d (Dual t) n m y
cnlMapCnt

instance
  ( NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel LeftToRight) N2 N1
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel RightToLeft) N2 N1
  , p ~ Dual (Dual p)
  , t ~ Dual (Dual t)
  )
  => ApplicativeG (SDualBi (ConeLiftable s p d t n m)) (Inv2 (HomFree s)) (->) where
  amapG :: forall x y.
Inv2 (HomFree s) x y
-> SDualBi (ConeLiftable s p d t n m) x
   -> SDualBi (ConeLiftable s p d t n m) y
amapG = Inv2 (HomFree s) x y
-> SDualBi (ConeLiftable s p d t n m) x
-> SDualBi (ConeLiftable s p d t n m) y
forall s (d :: DiagramType -> N' -> N' -> * -> *)
       (p :: Perspective) (t :: DiagramType) x y (n :: N') (m :: N').
(NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) ('S N1) N1,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) ('S N1) N1,
 p ~ Dual (Dual p), t ~ Dual (Dual t)) =>
Inv2 (HomFree s) x y
-> SDualBi (ConeLiftable s p d t n m) x
-> SDualBi (ConeLiftable s p d t n m) y
cnlMapS

instance
  ( NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel LeftToRight) N2 N1
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel RightToLeft) N2 N1
  , p ~ Dual (Dual p)
  , t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (ConeLiftable s p d t n m)) (Inv2 (HomFree s)) (->)

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

-- CokernelLiftableSomeFree -


-- | liftable cokernels for some free slice diagram

type CokernelLiftableSomeFree  = CokernelG ConeLiftable SomeFreeSliceDiagram N1

-- | liftable cokernels for some free slice diagram

type CokernelsLiftableSomeFree = CokernelsG ConeLiftable SomeFreeSliceDiagram N1

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

-- toDualOpFree -


-- | to dual operator.

toDualOpFreeDst :: (Distributive x, SlicedFree x)
  => Variant2 Contravariant (Inv2 (HomFree Dst)) x (Op x)
toDualOpFreeDst :: forall x.
(Distributive x, SlicedFree x) =>
Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  (Op x)
toDualOpFreeDst = Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x (Op x)
-> Variant2
     'Contravariant
     (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
     x
     (Op x)
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (HomFree Dst x (Op x)
-> HomFree Dst (Op x) x
-> Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x (Op x)
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 (HomDisjEmpty Dst Op x (Op x) -> HomFree Dst x (Op x)
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub HomDisjEmpty Dst Op x (Op x)
t) (HomDisjEmpty Dst Op (Op x) x -> HomFree Dst (Op x) x
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub HomDisjEmpty Dst Op (Op x) x
f)) where
  Contravariant2 (Inv2 HomDisjEmpty Dst Op x (Op x)
t HomDisjEmpty Dst Op (Op x) x
f) = Variant2 'Contravariant (IsoO Dst Op) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst

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

-- prpConeLiftable -


relConeKernelLiftable ::
  ( Diagrammatic d
  , Show (d (Parallel LeftToRight) n m x)
  , Validable (d (Parallel LeftToRight) n m x)
  , Distributive x
  , XStandardOrtOrientation x
  )
  => N -> ConeLiftable s Projective d (Parallel LeftToRight) n m x -> Statement
relConeKernelLiftable :: forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (m :: N')
       x s.
(Diagrammatic d, Show (d ('Parallel 'LeftToRight) n m x),
 Validable (d ('Parallel 'LeftToRight) n m x), Distributive x,
 XStandardOrtOrientation x) =>
N
-> ConeLiftable s 'Projective d ('Parallel 'LeftToRight) n m x
-> Statement
relConeKernelLiftable N
kMax (ConeKernelLiftable KernelConic Cone d N1 x
c (LiftableFree forall (k :: N'). Any k -> Liftable 'Projective (Free k) x
l)) =
  [Statement] -> Statement
And [ KernelConic Cone d N1 x -> Statement
forall a. Validable a => a -> Statement
valid KernelConic Cone d N1 x
c
      , X N -> (N -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (N -> N -> X N
xNB N
0 N
kMax)
          (\N
k -> case N -> SomeNatural
someNatural N
k of
              SomeNatural W n
k' -> [Statement] -> Statement
And [ Liftable 'Projective (Free n) x -> Statement
forall a. Validable a => a -> Statement
valid (W n -> Liftable 'Projective (Free n) x
forall (k :: N'). Any k -> Liftable 'Projective (Free k) x
l W n
k')
                                    , (Liftable 'Projective (Free n) x -> x
forall (s :: Perspective) (i :: * -> *) x. Liftable s i x -> x
lftbBase (W n -> Liftable 'Projective (Free n) x
forall (k :: N'). Any k -> Liftable 'Projective (Free k) x
l W n
k') x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== KernelConic Cone d 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 KernelConic Cone d N1 x
c)
                                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [ String
"k"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
k
                                                   , String
"c"String -> String -> Parameter
:=KernelConic Cone d N1 x -> String
forall a. Show a => a -> String
show KernelConic Cone d N1 x
c
                                                   ]
                                    ]
          )
      ]

-- | validity according to 'ConeLiftable'.

relConeLiftable ::
  ( Show (d (Parallel LeftToRight) n m x), Show (d (Parallel LeftToRight) n m (Op x))
  , Validable (d (Parallel LeftToRight) n m x), Validable (d (Parallel LeftToRight) n m (Op x))
  , Distributive x
  , SlicedFree x
  , XStandardOrtOrientation x
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel LeftToRight) n m
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel RightToLeft) n m
  , n ~ N2, m ~ N1
  )
  => N -> ConeLiftable s p d t n m x -> Statement
relConeLiftable :: forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (m :: N')
       x s (p :: Perspective) (t :: DiagramType).
(Show (d ('Parallel 'LeftToRight) n m x),
 Show (d ('Parallel 'LeftToRight) n m (Op x)),
 Validable (d ('Parallel 'LeftToRight) n m x),
 Validable (d ('Parallel 'LeftToRight) n m (Op x)), Distributive x,
 SlicedFree x, XStandardOrtOrientation x,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) n m,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) n m,
 n ~ 'S N1, m ~ N1) =>
N -> ConeLiftable s p d t n m x -> Statement
relConeLiftable N
kMax c :: ConeLiftable s p d t n m x
c@(ConeKernelLiftable KernelConic Cone d N1 x
_ LiftableFree 'Projective x
_)   = N
-> ConeLiftable s 'Projective d ('Parallel 'LeftToRight) n m x
-> Statement
forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (m :: N')
       x s.
(Diagrammatic d, Show (d ('Parallel 'LeftToRight) n m x),
 Validable (d ('Parallel 'LeftToRight) n m x), Distributive x,
 XStandardOrtOrientation x) =>
N
-> ConeLiftable s 'Projective d ('Parallel 'LeftToRight) n m x
-> Statement
relConeKernelLiftable N
kMax ConeLiftable s p d t n m x
ConeLiftable s 'Projective d ('Parallel 'LeftToRight) n m x
c
relConeLiftable N
kMax c :: ConeLiftable s p d t n m x
c@(ConeCokernelLiftable CokernelConic Cone d N1 x
_ LiftableFree 'Injective x
_) = N
-> ConeLiftable
     Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1 (Op x)
-> Statement
forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (m :: N')
       x s.
(Diagrammatic d, Show (d ('Parallel 'LeftToRight) n m x),
 Validable (d ('Parallel 'LeftToRight) n m x), Distributive x,
 XStandardOrtOrientation x) =>
N
-> ConeLiftable s 'Projective d ('Parallel 'LeftToRight) n m x
-> Statement
relConeKernelLiftable N
kMax Dual1
  (ConeLiftable Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
  (Op x)
ConeLiftable
  Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1 (Op x)
c' where
  Contravariant2 Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x (Op x)
i   = Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  (Op x)
forall x.
(Distributive x, SlicedFree x) =>
Variant2
  'Contravariant
  (Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))))
  x
  (Op x)
toDualOpFreeDst 
  SDualBi (Left1 Dual1
  (ConeLiftable Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
  (Op x)
c') = Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x (Op x)
-> SDualBi
     (ConeLiftable Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
     x
-> SDualBi
     (ConeLiftable Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
     (Op x)
forall x y.
Inv2 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x y
-> SDualBi
     (ConeLiftable Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) N1)
     x
-> SDualBi
     (ConeLiftable Dst 'Injective d ('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 (Sub (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst))) x (Op x)
i (Either1
  (Dual1 (ConeLiftable s p d t n m)) (ConeLiftable s p d t n m) x
-> SDualBi (ConeLiftable s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeLiftable s p d t n m x
-> Either1
     (ConeLiftable
        Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) N1)
     (ConeLiftable s p d t n m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 ConeLiftable s p d t n m x
c))


-- | validity according to 'ConeLiftable'.

prpConeLiftable ::
  ( Show (d (Parallel LeftToRight) n m x), Show (d (Parallel LeftToRight) n m (Op x))
  , Validable (d (Parallel LeftToRight) n m x), Validable (d (Parallel LeftToRight) n m (Op x))
  , Distributive x
  , SlicedFree x
  , XStandardOrtOrientation x
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel LeftToRight) n m
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel RightToLeft) n m
  , n ~ N2, m ~ N1
  )
  => N -> ConeLiftable s p d t n m x -> Statement
prpConeLiftable :: forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (m :: N')
       x s (p :: Perspective) (t :: DiagramType).
(Show (d ('Parallel 'LeftToRight) n m x),
 Show (d ('Parallel 'LeftToRight) n m (Op x)),
 Validable (d ('Parallel 'LeftToRight) n m x),
 Validable (d ('Parallel 'LeftToRight) n m (Op x)), Distributive x,
 SlicedFree x, XStandardOrtOrientation x,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) n m,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) n m,
 n ~ 'S N1, m ~ N1) =>
N -> ConeLiftable s p d t n m x -> Statement
prpConeLiftable N
kMax ConeLiftable s p d t n m x
c = String -> Label
Prp String
"ConeLiftable" Label -> Statement -> Statement
:<=>: N -> ConeLiftable s p d t n m x -> Statement
forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (m :: N')
       x s (p :: Perspective) (t :: DiagramType).
(Show (d ('Parallel 'LeftToRight) n m x),
 Show (d ('Parallel 'LeftToRight) n m (Op x)),
 Validable (d ('Parallel 'LeftToRight) n m x),
 Validable (d ('Parallel 'LeftToRight) n m (Op x)), Distributive x,
 SlicedFree x, XStandardOrtOrientation x,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) n m,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) n m,
 n ~ 'S N1, m ~ N1) =>
N -> ConeLiftable s p d t n m x -> Statement
relConeLiftable N
kMax ConeLiftable s p d t n m x
c

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

-- NaturalDiagrammaticFree -


-- | helper class to avoid undecidable instances.

class
  ( NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel LeftToRight) n m
  , NaturalDiagrammatic (Inv2 (HomFree s)) d (Parallel RightToLeft) n m

  )
  => NaturalDiagrammaticFree s d n m

instance NaturalDiagrammaticFree Dst DiagramFree n m
instance NaturalDiagrammaticFree Dst Diagram n m

instance
  ( Show (d (Parallel LeftToRight) n m x), Show (d (Parallel LeftToRight) n m (Op x))
  , Validable (d (Parallel LeftToRight) n m x), Validable (d (Parallel LeftToRight) n m (Op x))
  , Distributive x
  , SlicedFree x
  , XStandardOrtOrientation x
  , NaturalDiagrammaticFree s d n m
  , n ~ N2, m ~ N1
  )
  => Validable (ConeLiftable s p d t n m x) where
  valid :: ConeLiftable s p d t n m x -> Statement
valid = N -> ConeLiftable s p d t n m x -> Statement
forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (m :: N')
       x s (p :: Perspective) (t :: DiagramType).
(Show (d ('Parallel 'LeftToRight) n m x),
 Show (d ('Parallel 'LeftToRight) n m (Op x)),
 Validable (d ('Parallel 'LeftToRight) n m x),
 Validable (d ('Parallel 'LeftToRight) n m (Op x)), Distributive x,
 SlicedFree x, XStandardOrtOrientation x,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) n m,
 NaturalDiagrammatic
   (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) n m,
 n ~ 'S N1, m ~ N1) =>
N -> ConeLiftable s p d t n m x -> Statement
prpConeLiftable N
12


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

-- ConicFreeTip -


-- | predicate for a 'Conic' object with a free 'tip'.

--

-- __Property__ Let @c@ be in @'ConicFreeTip' __c s p d t n m x__@, then holds:

--

-- (1) @'slicePoint' k '==' 'tip' ('cone' c)@.

data ConicFreeTip c s
       (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> Type -> Type)
       (t :: DiagramType)
       (n :: N') (m :: N') x where
  ConicFreeTip :: (Attestable k, Sliced (Free k) x)
    => Free k x -> c s p d t n m x
    -> ConicFreeTip c s p d t n m x

instance Conic c => Conic (ConicFreeTip c) where
  cone :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
ConicFreeTip c s p d t n m x -> Cone s p d t n m x
cone (ConicFreeTip Free k x
_ c s p d t n m x
c) = c s p d t n m x -> Cone s p 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 p d t n m x
c

deriving instance Show (c s p d t n m x) => Show (ConicFreeTip c s p d t n m x)

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

-- KernelSomeFreeFreeTip -


-- | kernel with a free 'tip'.

type KernelSomeFreeFreeTip  = KernelG (ConicFreeTip Cone) SomeFreeSliceDiagram N1

-- | kernels with a free 'tip'.

type KernelsSomeFreeFreeTip = KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1

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

-- prpConicFreeTip -


relConicFreeTip ::
  ( Conic c
  , Show (c s p d t n m x)
  , Validable (c s p d t n m x)
  )
  => ConicFreeTip c s p d t n m x -> Statement
relConicFreeTip :: 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, Show (c s p d t n m x), Validable (c s p d t n m x)) =>
ConicFreeTip c s p d t n m x -> Statement
relConicFreeTip (ConicFreeTip Free k x
k c s p d t n m x
c)
  = [Statement] -> Statement
And [ Free k x -> Statement
forall a. Validable a => a -> Statement
valid Free k x
k
        , c s p d t n m x -> Statement
forall a. Validable a => a -> Statement
valid c s p d t n m x
c
        , (Free k x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint Free k x
k Point x -> Point x -> Bool
forall a. Eq a => a -> a -> Bool
== Cone s p d t n m x -> Point x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip (c s p d t n m x -> Cone s p 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 p d t n m x
c))
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [ String
"k"String -> String -> Parameter
:= Free k x -> String
forall a. Show a => a -> String
show Free k x
k
                       , String
"c"String -> String -> Parameter
:= c s p d t n m x -> String
forall a. Show a => a -> String
show c s p d t n m x
c
                       ]
        ]

-- | validity according to 'ConicFreeTip'.

prpConicFreeTip ::
  ( Conic c
  , Show (c s p d t n m x)
  , Validable (c s p d t n m x)
  )
  => ConicFreeTip c s p d t n m x -> Statement
prpConicFreeTip :: 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, Show (c s p d t n m x), Validable (c s p d t n m x)) =>
ConicFreeTip c s p d t n m x -> Statement
prpConicFreeTip ConicFreeTip c s p d t n m x
c = String -> Label
Prp String
"ConicFreeTip" Label -> Statement -> Statement
:<=>: ConicFreeTip c s p d t n m x -> Statement
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, Show (c s p d t n m x), Validable (c s p d t n m x)) =>
ConicFreeTip c s p d t n m x -> Statement
relConicFreeTip ConicFreeTip c s p d t n m x
c

instance
  ( Conic c
  , Show (c s p d t n m x)
  , Validable (c s p d t n m x)
  )
  => Validable (ConicFreeTip c s p d t n m x) where
  valid :: ConicFreeTip c s p d t n m x -> Statement
valid = ConicFreeTip c s p d t n m x -> Statement
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, Show (c s p d t n m x), Validable (c s p d t n m x)) =>
ConicFreeTip c s p d t n m x -> Statement
prpConicFreeTip


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

-- SomeFreeSlice -


-- | some free point within a 'Multiplicative' structure @__c__@.

data SomeFreeSlice s c where
  SomeFreeSlice :: (Attestable k, Sliced (Free k) c)
    => Slice s (Free k) c -> SomeFreeSlice s c
    
deriving instance Show c => Show (SomeFreeSlice s c)

instance Validable (SomeFreeSlice s c) where
  valid :: SomeFreeSlice s c -> Statement
valid (SomeFreeSlice Slice s (Free k) c
s) = String -> Label
Label String
"SomeFreeSlice" Label -> Statement -> Statement
:<=>: Slice s (Free k) c -> Statement
forall a. Validable a => a -> Statement
valid Slice s (Free k) c
s

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

-- KernelSliceFromSomeFreeTip -


-- | predicate for a kernel with a start point of its diagram given by the slice index and

-- a free universal tip.

--

-- __Property__ Let @'KernelSliceFromSomeFreeTip' k' i ker@ be in

-- @'KernelSliceFromSomeFreeTip' __n__ __c__@, then holds:

--

-- (1) @'slicePoint' i '==' s@ where @'DiagramParallelLR' s _ _ = 'diagram' ker@.

--

-- (2) @'slicePoint' k' '==' 'tip' ('universalCone' ker)@.

data KernelSliceFromSomeFreeTip n i c where
  KernelSliceFromSomeFreeTip :: (Attestable k', Sliced (Free k') c)
    => Free k' c -> i c -> Kernel n c -> KernelSliceFromSomeFreeTip n i c

instance (Oriented c, Sliced i c) => Show (KernelSliceFromSomeFreeTip n i c) where
  show :: KernelSliceFromSomeFreeTip n i c -> String
show (KernelSliceFromSomeFreeTip Free k' c
k i c
i Kernel n c
ker)
    = String
"KernelSliceFromSomeFreeTip[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Free k' c -> String
forall x. Free k' x -> String
forall (p :: * -> *) x. Show1 p => p x -> String
show1 Free k' c
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ i c -> String
forall x. i x -> String
forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] ("
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kernel n c -> String
forall a. Show a => a -> String
show Kernel n c
ker String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")" 

instance
  ( Distributive c, Sliced i c
  , XStandardEligibleConeKernel n c
  , XStandardEligibleConeFactorKernel n c
  , Typeable n
  )
  => Validable (KernelSliceFromSomeFreeTip n i c) where
  valid :: KernelSliceFromSomeFreeTip n i c -> Statement
valid (KernelSliceFromSomeFreeTip Free k' c
k' i c
i Kernel n c
ker) = String -> Label
Label String
"KernelSliceFromSomeFreeTip" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ Free k' c -> Statement
forall x. Free k' x -> Statement
forall (p :: * -> *) x. Validable1 p => p x -> Statement
valid1 Free k' c
k'
        , Kernel n c -> Statement
forall a. Validable a => a -> Statement
valid Kernel n c
ker
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: let DiagramParallelLR Point c
s Point c
_ FinList n c
_
                                = Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
-> Diagram ('Parallel 'LeftToRight) ('S N1) n c
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 Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
 -> Diagram ('Parallel 'LeftToRight) ('S N1) n c)
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
-> Diagram ('Parallel 'LeftToRight) ('S N1) n c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Cone 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 (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
 -> Cone
      Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c)
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Kernel n c
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
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 Kernel n c
ker
                           in
            (i c -> Point c
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i Point c -> Point c -> Bool
forall a. Eq a => a -> a -> Bool
== Point c
s) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=i c -> String
forall x. i x -> String
forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i,String
"s"String -> String -> Parameter
:= Point c -> String
forall a. Show a => a -> String
show Point c
s]
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (Free k' c -> Point c
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint Free k' c
k' Point c -> Point c -> Bool
forall a. Eq a => a -> a -> Bool
== Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
-> Point c
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip (Kernel n c
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) n c
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 Kernel n c
ker))
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"k'"String -> String -> Parameter
:=Free k' c -> String
forall x. Free k' x -> String
forall (p :: * -> *) x. Show1 p => p x -> String
show1 Free k' c
k',String
"ker"String -> String -> Parameter
:=Kernel n c -> String
forall a. Show a => a -> String
show Kernel n c
ker]
        ]