{-# LANGUAGE NoImplicitPrelude #-}

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

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

import Data.Typeable

import OAlg.Prelude

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

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

import OAlg.Hom

import OAlg.Adjunction.Definition

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


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

-- 
lmPrjMapStruct :: Hom Mlt h
  => Struct Mlt d
  -> Adjunction h d c
  -> Limes Mlt Projective t n m d -> Limes Mlt Projective t n m c
lmPrjMapStruct :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Mlt h =>
Struct Mlt d
-> Adjunction h d c
-> Limes Mlt 'Projective t n m d
-> Limes Mlt 'Projective t n m c
lmPrjMapStruct Struct Mlt d
Struct adj :: Adjunction h d c
adj@(Adjunction h c d
l h d c
r Point c -> c
_ Point d -> d
_) (LimesProjective Cone Mlt 'Projective t n m d
dLim Cone Mlt 'Projective t n m d -> d
dUniv)
  = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective t n m c
cLim Cone Mlt 'Projective t n m c -> c
cUniv where

  dDgm :: Diagram t n m d
dDgm = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone Mlt 'Projective t n m d
dLim
  
  cLim :: Cone Mlt 'Projective t n m c
cLim = forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
Hom s h =>
h a b -> Cone s p t n m a -> Cone s p t n m b
cnMap h d c
r Cone Mlt 'Projective t n m d
dLim
  
  cUniv :: Cone Mlt 'Projective t n m c -> c
cUniv (ConeProjective Diagram t n m c
_ Point c
cTip FinList n c
fs) = forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point c -> d -> c
adjr Adjunction h d c
adj Point c
cTip (Cone Mlt 'Projective t n m d -> d
dUniv Cone Mlt 'Projective t n m d
dCone) where
    -- from ConeProjective _ cTip fs is eligible and ajd is valid follows
    -- that dCone is eligible!
    dCone :: Cone Mlt 'Projective t n m d
dCone = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram t n m d
dDgm (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h c d
l Point c
cTip) FinList n d
fs'
    fs' :: FinList n d
fs' = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point d -> c -> d
adjl Adjunction h d c
adj)) (forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m d
dDgm forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` FinList n c
fs)


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


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

lmInjMapHom :: Hom Mlt h
  => Homomorphous Mlt d c
  -> Dual (Dual t) :~: t
  -> Adjunction h d c -> Limes Mlt Injective t n m c -> Limes Mlt Injective t n m d
lmInjMapHom :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Mlt h =>
Homomorphous Mlt d c
-> (Dual (Dual t) :~: t)
-> Adjunction h d c
-> Limes Mlt 'Injective t n m c
-> Limes Mlt 'Injective t n m d
lmInjMapHom (Struct Mlt d
Struct:>:Struct Mlt c
Struct) Dual (Dual t) :~: t
rt adj :: Adjunction h d c
adj@(Adjunction h c d
_ h d c
_ Point c -> c
_ Point d -> d
_) Limes Mlt 'Injective t n m c
lim
  = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Limes s p t n m a)
-> Limes s p t n m a
coLimesInv forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl Dual (Dual t) :~: t
rt
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Mlt h =>
Adjunction h d c
-> Limes Mlt 'Projective t n m d -> Limes Mlt 'Projective t n m c
lmPrjMap (forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Dual (Adjunction h d c)
coAdjunction Adjunction h d c
adj) (forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Limes s p t n m a
-> Dual (Limes s p t n m a)
coLimes forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl Dual (Dual t) :~: t
rt Limes Mlt 'Injective t n m c
lim)


-- | mapping a injective limes under an adjunction.
lmInjMap :: Hom Mlt h
  => Adjunction h d c -> Limes Mlt Injective t n m c -> Limes Mlt Injective t n m d
lmInjMap :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Mlt h =>
Adjunction h d c
-> Limes Mlt 'Injective t n m c -> Limes Mlt 'Injective t n m d
lmInjMap Adjunction h d c
adj Limes Mlt 'Injective t n m c
lim = forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Mlt h =>
Homomorphous Mlt d c
-> (Dual (Dual t) :~: t)
-> Adjunction h d c
-> Limes Mlt 'Injective t n m c
-> Limes Mlt 'Injective t n m d
lmInjMapHom (forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Homomorphous Mlt d c
adjHomMlt Adjunction h d c
adj) (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Dual (Dual t) :~: t
lmDiagramTypeRefl Limes Mlt 'Injective t n m c
lim) Adjunction h d c
adj Limes Mlt 'Injective t n m c
lim

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

lmPrjMapDstStruct :: Hom Dst h => Struct Dst d -> Adjunction h d c
  -> Limes Dst Projective t n m d -> Limes Dst Projective t n m c
lmPrjMapDstStruct :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Dst h =>
Struct Dst d
-> Adjunction h d c
-> Limes Dst 'Projective t n m d
-> Limes Dst 'Projective t n m c
lmPrjMapDstStruct Struct Dst d
Struct adj :: Adjunction h d c
adj@(Adjunction h c d
_ h d c
r Point c -> c
_ Point d -> d
_)
  (LimesProjective dLim :: Cone Dst 'Projective t n m d
dLim@(ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m d
_ d
_) Cone Dst 'Projective t n m d -> d
dUniv) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Dst 'Projective t n m c
cLim Cone Dst 'Projective t n m c -> c
cUniv where

  dDgm :: Diagram t n m d
dDgm = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone Dst 'Projective t n m d
dLim

  cLim :: Cone Dst 'Projective t n m c
cLim = forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
Hom s h =>
h a b -> Cone s p t n m a -> Cone s p t n m b
cnMap h d c
r Cone Dst 'Projective t n m d
dLim

  cUniv :: Cone Dst 'Projective t n m c -> c
cUniv (ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m c
_ c
x) = forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point c -> d -> c
adjr Adjunction h d c
adj (forall q. Oriented q => q -> Point q
start c
x) (Cone Dst 'Projective t n m d -> d
dUniv Cone Dst 'Projective ('Parallel 'LeftToRight) ('S N1) m d
dCone) where
    dCone :: Cone Dst 'Projective ('Parallel 'LeftToRight) ('S N1) m d
dCone = forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel Diagram t n m d
dDgm (forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Point d -> c -> d
adjl Adjunction h d c
adj (forall (n :: N') a. FinList (n + 1) a -> a
head forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m d
dDgm) c
x)

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

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

lmInjMapDstHom :: Hom Dst h
  => Homomorphous Dst d c
  -> Dual (Dual t) :~: t
  -> Adjunction h d c -> Limes Dst Injective t n m c -> Limes Dst Injective t n m d
lmInjMapDstHom :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Dst h =>
Homomorphous Dst d c
-> (Dual (Dual t) :~: t)
-> Adjunction h d c
-> Limes Dst 'Injective t n m c
-> Limes Dst 'Injective t n m d
lmInjMapDstHom (Struct Dst d
Struct:>:Struct Dst c
Struct) Dual (Dual t) :~: t
rt adj :: Adjunction h d c
adj@(Adjunction h c d
_ h d c
_ Point c -> c
_ Point d -> d
_) Limes Dst 'Injective t n m c
lim
  = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Limes s p t n m a)
-> Limes s p t n m a
coLimesInv forall a. Distributive a => ConeStruct Dst a
ConeStructDst forall {k} (a :: k). a :~: a
Refl Dual (Dual t) :~: t
rt
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Dst h =>
Adjunction h d c
-> Limes Dst 'Projective t n m d -> Limes Dst 'Projective t n m c
lmPrjMapDst (forall (h :: * -> * -> *) d c.
Hom Mlt h =>
Adjunction h d c -> Dual (Adjunction h d c)
coAdjunction Adjunction h d c
adj) (forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Limes s p t n m a
-> Dual (Limes s p t n m a)
coLimes forall a. Distributive a => ConeStruct Dst a
ConeStructDst forall {k} (a :: k). a :~: a
Refl Dual (Dual t) :~: t
rt Limes Dst 'Injective t n m c
lim)

-- | mapping a injective limes under an adjunction.
lmInjMapDst :: Hom Dst h
  => Adjunction h d c -> Limes Dst Injective t n m c -> Limes Dst Injective t n m d
lmInjMapDst :: forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Dst h =>
Adjunction h d c
-> Limes Dst 'Injective t n m c -> Limes Dst 'Injective t n m d
lmInjMapDst adj :: Adjunction h d c
adj@(Adjunction h c d
_ h d c
r Point c -> c
_ Point d -> d
_) Limes Dst 'Injective t n m c
lim
  = forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Dst h =>
Homomorphous Dst d c
-> (Dual (Dual t) :~: t)
-> Adjunction h d c
-> Limes Dst 'Injective t n m c
-> Limes Dst 'Injective t n m d
lmInjMapDstHom (forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h d c
r)) (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Dual (Dual t) :~: t
lmDiagramTypeRefl Limes Dst 'Injective t n m c
lim) Adjunction h d c
adj Limes Dst 'Injective t n m c
lim