{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.EqualizersAndCoequalizers

-- Description : equalizers and coequalizers

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- equalizers and coequalizers, i.e. limits of @'Diagram' ('Parallel' __d__)@.

module OAlg.Limes.EqualizersAndCoequalizers
  (
    -- * Equalizers

    Equalizers, EqualizersG
  , Equalizer, EqualizerG
  , EqualizerCone, EqualizerConic
  , EqualizerDiagram, EqualizerDiagrammatic

    -- ** Construction

  , equalizers, equalizers0, equalizers1, equalizers2

    -- *** Orientation

  , equalizersOrnt

    -- * Coequalizers

  , Coequalizers, CoequalizersG
  , Coequalizer, CoequalizerG
  , CoequalizerCone, CoequalizerConic
  , CoequalizerDiagram, CoequalizerDiagrammatic

    -- ** Construction

  , coequalizers, coequalizers'

    -- *** Orientation

  , coequalizersOrnt

  )
  where

import Data.Kind

import OAlg.Prelude

import OAlg.Category.SDuality

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

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

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

import OAlg.Hom.Multiplicative

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

import OAlg.Limes.MinimaAndMaxima
import OAlg.Limes.ProductsAndSums

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

-- Equalizers -


-- | 'Diagrammatic' object for a equalizer. 

type EqualizerDiagrammatic d (n :: N') = d (Parallel LeftToRight) N2 n :: Type -> Type

-- | 'Diagram' for a equalizer. 

type EqualizerDiagram n = EqualizerDiagrammatic Diagram n

-- | 'Conic' object for a equalizer.

type EqualizerConic c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N')
  = c Mlt Projective d (Parallel LeftToRight) N2 n :: Type -> Type

-- | 'Cone' for a equalizer.

type EqualizerCone n = EqualizerConic Cone Diagram n

-- | generic equalizer as 'LimesG'.

type EqualizerG c d n = LimesG c Mlt Projective d (Parallel LeftToRight) N2 n

-- | equalizer as 'Limes'.

type Equalizer n = EqualizerG Cone Diagram n

-- | generic equalizers for a 'Multiplicative' structures.

type EqualizersG c d n = LimitsG c Mlt Projective d (Parallel LeftToRight) N2 n

-- | equalizers for a 'Multiplicative' structures.

type Equalizers n = EqualizersG Cone Diagram n

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

-- eqlProductDiagram -


-- | the underlying product diagram.

eqlProductDiagram :: EqualizerDiagram n x -> ProductDiagram N2 x
eqlProductDiagram :: forall (n :: N') x. EqualizerDiagram n x -> ProductDiagram N2 x
eqlProductDiagram (DiagramParallelLR Point x
p Point x
q FinList n x
_) = FinList N2 (Point x) -> Diagram 'Discrete N2 'N0 x
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete (Point x
pPoint x -> FinList N1 (Point x) -> FinList (N1 + 1) (Point x)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|Point x
qPoint x -> FinList 'N0 (Point x) -> FinList ('N0 + 1) (Point x)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 (Point x)
forall a. FinList 'N0 a
Nil)

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

-- eqlProductCone -


-- | the underlying product cone.

eqlProductCone :: EqualizerCone n x -> ProductCone N2 x
eqlProductCone :: forall (n :: N') x. EqualizerCone n x -> ProductCone N2 x
eqlProductCone (ConeProjective Diagram ('Parallel 'LeftToRight) N2 n x
d Point x
t FinList N2 x
cs) = Diagram 'Discrete N2 'N0 x
-> Point x
-> FinList N2 x
-> Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective (Diagram ('Parallel 'LeftToRight) N2 n x
-> Diagram 'Discrete N2 'N0 x
forall (n :: N') x. EqualizerDiagram n x -> ProductDiagram N2 x
eqlProductDiagram Diagram ('Parallel 'LeftToRight) N2 n x
d) Point x
t FinList N2 x
cs

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

-- equalizers0 -


-- | the induced equalizers of zero parallel arrows.

equalizers0 :: Multiplicative x => Products N2 x -> Equalizers N0 x
equalizers0 :: forall x. Multiplicative x => Products N2 x -> Equalizers 'N0 x
equalizers0 Products N2 x
prd2 = (Diagram ('Parallel 'LeftToRight) N2 'N0 x
 -> LimesG
      Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x)
-> LimitsG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (Products N2 x
-> Diagram ('Parallel 'LeftToRight) N2 'N0 x
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
forall x.
Multiplicative x =>
Products N2 x -> EqualizerDiagram 'N0 x -> Equalizer 'N0 x
eql Products N2 x
prd2) where
  eql :: Multiplicative x
    => Products N2 x -> EqualizerDiagram N0 x -> Equalizer N0 x
  eql :: forall x.
Multiplicative x =>
Products N2 x -> EqualizerDiagram 'N0 x -> Equalizer 'N0 x
eql Products N2 x
prd2 EqualizerDiagram 'N0 x
d = Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
-> (Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
    -> x)
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
l Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x -> x
u where
    LimesProjective Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
lPrd2 Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x -> x
uPrd2 = Products N2 x
-> Diagram 'Discrete N2 'N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes Products N2 x
prd2 (EqualizerDiagram 'N0 x -> Diagram 'Discrete N2 'N0 x
forall (n :: N') x. EqualizerDiagram n x -> ProductDiagram N2 x
eqlProductDiagram EqualizerDiagram 'N0 x
d)
    l :: Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
l = EqualizerDiagram 'N0 x
-> Point x
-> FinList N2 x
-> Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective EqualizerDiagram 'N0 x
d (Cone Mlt 'Projective Diagram 'Discrete N2 'N0 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 Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
lPrd2) (Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x -> FinList N2 x
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> FinList n a
shell Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
lPrd2)
    u :: Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x -> x
u = Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x -> x
uPrd2 (Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x -> x)
-> (Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
    -> Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x)
-> Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
-> x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 'N0 x
-> Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
forall (n :: N') x. EqualizerCone n x -> ProductCone N2 x
eqlProductCone

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

-- eqlHeadDiagram -


-- | the underlying minimum diagram given by the first arrow.

eqlHeadDiagram :: EqualizerDiagram (n+1) x -> MinimumDiagram From N1 x
eqlHeadDiagram :: forall (n :: N') x.
EqualizerDiagram (n + 1) x -> MinimumDiagram 'From N1 x
eqlHeadDiagram (DiagramParallelLR Point x
p Point x
_ (x
a:|FinList n1 x
_)) = Point x -> FinList N1 x -> Diagram ('Chain 'From) (N1 + 1) N1 x
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'From) (m + 1) m a
DiagramChainFrom Point x
p (x
ax -> 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)

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

-- eqlHeadCone -


-- | the underlying minimum cone given by the first arrow.

eqlHeadCone :: EqualizerCone (n+1) x -> MinimumCone From N1 x
eqlHeadCone :: forall (n :: N') x.
EqualizerCone (n + 1) x -> MinimumCone 'From N1 x
eqlHeadCone (ConeProjective Diagram ('Parallel 'LeftToRight) N2 (n + 1) x
d Point x
t FinList N2 x
cs) = Diagram ('Chain 'From) N2 N1 x
-> Point x
-> FinList N2 x
-> Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective (Diagram ('Parallel 'LeftToRight) N2 (n + 1) x
-> MinimumDiagram 'From N1 x
forall (n :: N') x.
EqualizerDiagram (n + 1) x -> MinimumDiagram 'From N1 x
eqlHeadDiagram Diagram ('Parallel 'LeftToRight) N2 (n + 1) x
d) Point x
t FinList N2 x
cs

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

-- equlizers1 -


-- | equalizers of one parallel arrow, i.e. 'Minima'.

equalizers1 :: Multiplicative x => Equalizers N1 x
equalizers1 :: forall x. Multiplicative x => Equalizers N1 x
equalizers1 = (Diagram ('Parallel 'LeftToRight) N2 N1 x
 -> LimesG
      Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x)
-> LimitsG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG Diagram ('Parallel 'LeftToRight) N2 N1 x
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
forall x.
Multiplicative x =>
EqualizerDiagram N1 x -> Equalizer N1 x
eql where
  eql :: Multiplicative x => EqualizerDiagram N1 x -> Equalizer N1 x
  eql :: forall x.
Multiplicative x =>
EqualizerDiagram N1 x -> Equalizer N1 x
eql EqualizerDiagram N1 x
d = Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> (Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
    -> x)
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
l Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x -> x
u where
    LimesProjective Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x
lMin Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x -> x
uMin = LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x
-> Diagram ('Chain 'From) N2 N1 x
-> LimesG Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes Minima 'From N1 x
LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x
forall x (n :: N'). Multiplicative x => Minima 'From n x
minimaFrom (EqualizerDiagram ('N0 + 1) x -> MinimumDiagram 'From N1 x
forall (n :: N') x.
EqualizerDiagram (n + 1) x -> MinimumDiagram 'From N1 x
eqlHeadDiagram EqualizerDiagram ('N0 + 1) x
EqualizerDiagram N1 x
d)  
    l :: Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
l = EqualizerDiagram N1 x
-> Point x
-> FinList N2 x
-> Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective EqualizerDiagram N1 x
d (Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 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 Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x
lMin) (Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x -> FinList N2 x
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> FinList n a
shell Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x
lMin)
    u :: Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x -> x
u = Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x -> x
uMin (Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x -> x)
-> (Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
    -> Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x)
-> Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. EqualizerCone ('N0 + 1) x -> MinimumCone 'From N1 x
Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> Cone Mlt 'Projective Diagram ('Chain 'From) N2 N1 x
forall (n :: N') x.
EqualizerCone (n + 1) x -> MinimumCone 'From N1 x
eqlHeadCone

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

-- equlizers2 -


-- | promoting equalizers.

--

-- ![image equalizer](c:/Users/zeric/haskell/oalg/src/OAlg/Limes/equalizer.jpg)

equalizers2 :: Multiplicative x => Equalizers N2 x -> Equalizers (n+2) x
equalizers2 :: forall x (n :: N').
Multiplicative x =>
Equalizers N2 x -> Equalizers (n + 2) x
equalizers2 Equalizers N2 x
eql2 = (Diagram ('Parallel 'LeftToRight) N2 ('S ('S n)) x
 -> LimesG
      Cone
      Mlt
      'Projective
      Diagram
      ('Parallel 'LeftToRight)
      N2
      ('S ('S n))
      x)
-> LimitsG
     Cone
     Mlt
     'Projective
     Diagram
     ('Parallel 'LeftToRight)
     N2
     ('S ('S n))
     x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (Equalizers N2 x
-> Diagram ('Parallel 'LeftToRight) N2 ('S ('S n)) x
-> LimesG
     Cone
     Mlt
     'Projective
     Diagram
     ('Parallel 'LeftToRight)
     N2
     ('S ('S n))
     x
forall x (n :: N') (n' :: N').
(Multiplicative x, n ~ (n' + 2)) =>
Equalizers N2 x -> EqualizerDiagram n x -> Equalizer n x
eql Equalizers N2 x
eql2) where
  eql :: (Multiplicative x, n ~ (n'+2))
      => Equalizers N2 x -> EqualizerDiagram n x -> Equalizer n x
  eql :: forall x (n :: N') (n' :: N').
(Multiplicative x, n ~ (n' + 2)) =>
Equalizers N2 x -> EqualizerDiagram n x -> Equalizer n x
eql Equalizers N2 x
eql2 d :: EqualizerDiagram n x
d@(DiagramParallelLR Point x
_ Point x
_ (x
_:|x
_:|FinList n1 x
Nil))        = LimitsG
  Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> EqualizerDiagram n x
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG
  Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
Equalizers N2 x
eql2 EqualizerDiagram n x
d
  eql Equalizers N2 x
eql2 d :: EqualizerDiagram n x
d@(DiagramParallelLR Point x
p Point x
q (x
a0:|aN :: FinList n1 x
aN@(x
_:|x
_:|FinList n1 x
_))) = Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> (Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
    -> x)
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
l Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x -> x
u where
    dN :: Diagram ('Parallel 'LeftToRight) N2 n1 x
dN = Point x
-> Point x
-> FinList n1 x
-> Diagram ('Parallel 'LeftToRight) N2 n1 x
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) N2 m a
DiagramParallelLR Point x
p Point x
q FinList n1 x
aN
    LimesProjective (ConeProjective Diagram ('Parallel 'LeftToRight) N2 n1 x
_ Point x
h (x
h0:|x
h1:|FinList n1 x
Nil)) Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n1 x -> x
Cone
  Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S ('S n1)) x
-> x
uN = Equalizers N2 x
-> Diagram ('Parallel 'LeftToRight) N2 n1 x
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n1 x
forall x (n :: N') (n' :: N').
(Multiplicative x, n ~ (n' + 2)) =>
Equalizers N2 x -> EqualizerDiagram n x -> Equalizer n x
eql Equalizers N2 x
eql2 Diagram ('Parallel 'LeftToRight) N2 n1 x
dN

    d2 :: Diagram ('Parallel 'LeftToRight) N2 N2 x
d2 = Point x
-> Point x
-> FinList N2 x
-> Diagram ('Parallel 'LeftToRight) N2 N2 x
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) N2 m a
DiagramParallelLR Point x
h Point x
q (x
a0x -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
h0x -> FinList N1 x -> FinList (N1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
h1x -> 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)
    LimesProjective (ConeProjective Diagram ('Parallel 'LeftToRight) N2 N2 x
_ Point x
k (x
k0:|x
k1:|FinList n1 x
Nil)) Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N2 x -> x
u2 = Equalizers N2 x
-> Diagram ('Parallel 'LeftToRight) N2 N2 x
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N2 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes Equalizers N2 x
eql2 Diagram ('Parallel 'LeftToRight) N2 N2 x
d2
    
    l :: Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
l = EqualizerDiagram n x
-> Point x
-> FinList N2 x
-> Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective EqualizerDiagram n x
d Point x
k (x
h0x -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
k0x -> FinList N1 x -> FinList (N1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
k1x -> 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)
    u :: Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x -> x
u (ConeProjective EqualizerDiagram n x
_ Point x
x (x
x0:|x
x1:|FinList n1 x
Nil)) = x
uk where
      uk :: x
uk = Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N2 x -> x
u2 (Diagram ('Parallel 'LeftToRight) N2 N2 x
-> Point x
-> FinList N2 x
-> Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N2 x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective Diagram ('Parallel 'LeftToRight) N2 N2 x
d2 Point x
x (x
uhx -> FinList N1 x -> FinList (N1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
x1x -> 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))
      uh :: x
uh = Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n1 x -> x
Cone
  Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S ('S n1)) x
-> x
uN (Diagram ('Parallel 'LeftToRight) N2 n1 x
-> Point x
-> FinList N2 x
-> Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective Diagram ('Parallel 'LeftToRight) N2 n1 x
dN Point x
x (x
x0x -> FinList N1 x -> FinList (N1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
x1x -> 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))

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

-- equlizers -


-- | equalizers of @n@ arrows given by products of two points and equalizers of two arrows.

equalizers :: Multiplicative x => Products N2 x -> Equalizers N2 x -> Equalizers n x
equalizers :: forall x (n :: N').
Multiplicative x =>
Products N2 x -> Equalizers N2 x -> Equalizers n x
equalizers Products N2 x
prd2 Equalizers N2 x
eql2 = (Diagram ('Parallel 'LeftToRight) N2 n x
 -> LimesG
      Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x)
-> LimitsG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (Products N2 x
-> Equalizers N2 x
-> Diagram ('Parallel 'LeftToRight) N2 n x
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall x (n :: N').
Multiplicative x =>
Products N2 x
-> Equalizers N2 x -> EqualizerDiagram n x -> Equalizer n x
eql Products N2 x
prd2 Equalizers N2 x
eql2) where
  eql :: Multiplicative x
      => Products N2 x -> Equalizers N2 x -> EqualizerDiagram n x -> Equalizer n x
  eql :: forall x (n :: N').
Multiplicative x =>
Products N2 x
-> Equalizers N2 x -> EqualizerDiagram n x -> Equalizer n x
eql Products N2 x
prd2 Equalizers N2 x
eql2 EqualizerDiagram n x
d = case EqualizerDiagram n x -> FinList n x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows EqualizerDiagram n x
d of
    FinList n x
Nil      -> LimitsG
  Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> EqualizerDiagram n x -> Equalizer n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes (Products N2 x -> Equalizers 'N0 x
forall x. Multiplicative x => Products N2 x -> Equalizers 'N0 x
equalizers0 Products N2 x
prd2) EqualizerDiagram n x
d
    x
_:|FinList n1 x
Nil   -> LimitsG
  Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> EqualizerDiagram n x -> Equalizer n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG
  Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
Equalizers N1 x
forall x. Multiplicative x => Equalizers N1 x
equalizers1 EqualizerDiagram n x
d
    x
_:|x
_:|FinList n1 x
_  -> LimitsG
  Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> EqualizerDiagram n x -> Equalizer n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes (Equalizers N2 x -> Equalizers (n1 + 2) x
forall x (n :: N').
Multiplicative x =>
Equalizers N2 x -> Equalizers (n + 2) x
equalizers2 Equalizers N2 x
eql2) EqualizerDiagram n x
d 

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

-- equlizersOrnt -


-- | equalizers for 'Orientation' 

equalizersOrnt :: Entity p => p -> Equalizers n (Orientation p)
equalizersOrnt :: forall p (n :: N'). Entity p => p -> Equalizers n (Orientation p)
equalizersOrnt = p
-> Limits
     Mlt 'Projective ('Parallel 'LeftToRight) N2 n (Orientation p)
forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsMltPrjOrnt

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

-- Coequalizers -


-- | 'Diagrammatic' object for a coequalizer. 

type CoequalizerDiagrammatic d (n :: N') = d (Parallel RightToLeft) N2 n :: Type -> Type

-- | 'Diagram' for a coequalizer. 

type CoequalizerDiagram n = CoequalizerDiagrammatic Diagram n

-- | 'Conic' object for a coequalizer.

type CoequalizerConic c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N')
  = c Mlt Injective d (Parallel RightToLeft) N2 n :: Type -> Type

-- | 'Cone' for a coequalizer.

type CoequalizerCone n = CoequalizerConic Cone Diagram n

-- | generic coequalizer as 'LimesG'.

type CoequalizerG c d n = LimesG c Mlt Injective d (Parallel RightToLeft) N2 n

-- | coequalizer as 'Limes'.

type Coequalizer n = CoequalizerG Cone Diagram n

-- | generic coequalizers for a 'Multiplicative' structures.

type CoequalizersG c d n = LimitsG c Mlt Injective d (Parallel RightToLeft) N2 n

-- | coequalizers for a 'Multiplicative' structures.

type Coequalizers n = CoequalizersG Cone Diagram n

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

-- coequalizers -


-- | coequalizers of @n@ arrows given by sums of two points and coequalizers of two arrows.

coequalizers :: Multiplicative x => Sums N2 x -> Coequalizers N2 x -> Coequalizers n x
coequalizers :: forall x (n :: N').
Multiplicative x =>
Sums N2 x -> Coequalizers N2 x -> Coequalizers n x
coequalizers Sums N2 x
sum2 Coequalizers N2 x
coeql2 = LimitsG Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
coeqls where
  Contravariant2 IsoO Mlt Op x (Op x)
i = Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
forall x.
Multiplicative x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
toDualOpMlt

  SDualBi (Left1 Dual1 (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) (Op x)
prd2)    = IsoO Mlt Op x (Op x)
-> SDualBi (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) x
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Mlt Op x (Op x)
i (Either1
  (Dual1 (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0))
  (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0)
  x
-> SDualBi (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Sums N2 x
-> Either1
     (LimitsG Cone Mlt 'Projective Diagram 'Discrete N2 'N0)
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Sums N2 x
sum2))
  SDualBi (Left1 Dual1
  (LimitsG
     Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 N2)
  (Op x)
eql2)    = IsoO Mlt Op x (Op x)
-> SDualBi
     (LimitsG
        Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 N2)
     x
-> SDualBi
     (LimitsG
        Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 N2)
     (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Mlt Op x (Op x)
i (Either1
  (Dual1
     (LimitsG
        Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 N2))
  (LimitsG
     Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 N2)
  x
-> SDualBi
     (LimitsG
        Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 N2)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Coequalizers N2 x
-> Either1
     (LimitsG
        Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 N2)
     (LimitsG
        Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 N2)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Coequalizers N2 x
coeql2))
  eqls :: Equalizers n (Op x)
eqls                    = Products N2 (Op x) -> Equalizers N2 (Op x) -> Equalizers n (Op x)
forall x (n :: N').
Multiplicative x =>
Products N2 x -> Equalizers N2 x -> Equalizers n x
equalizers Dual1 (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) (Op x)
Products N2 (Op x)
prd2 Dual1
  (LimitsG
     Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 N2)
  (Op x)
Equalizers N2 (Op x)
eql2
  SDualBi (Right1 LimitsG Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
coeqls) = Inv2 (HomDisjEmpty Mlt Op) (Op x) x
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Mlt Op x (Op x) -> Inv2 (HomDisjEmpty Mlt Op) (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Mlt Op x (Op x)
i) (Either1
  (Dual1
     (LimitsG
        Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 n))
  (LimitsG Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
  (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Equalizers n (Op x)
-> Either1
     (LimitsG
        Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 n)
     (LimitsG Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Equalizers n (Op x)
eqls))

-- | 'coequalizers' given by a proxy for @n@.

coequalizers' :: Multiplicative x
  => p n -> Sums N2 x -> Coequalizers N2 x -> Coequalizers n x
coequalizers' :: forall x (p :: N' -> *) (n :: N').
Multiplicative x =>
p n -> Sums N2 x -> Coequalizers N2 x -> Coequalizers n x
coequalizers' p n
_ = Sums N2 x -> Coequalizers N2 x -> Coequalizers n x
forall x (n :: N').
Multiplicative x =>
Sums N2 x -> Coequalizers N2 x -> Coequalizers n x
coequalizers

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

-- coequalizersOrnt -


-- | coequalizers for 'Orientation'.

coequalizersOrnt :: Entity p => p -> Coequalizers n (Orientation p)
coequalizersOrnt :: forall p (n :: N'). Entity p => p -> Coequalizers n (Orientation p)
coequalizersOrnt = p
-> Limits
     Mlt 'Injective ('Parallel 'RightToLeft) N2 n (Orientation p)
forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsMltInjOrnt