{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# 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, Equalizer, EqualizerCone, EqualizerDiagram

    -- ** Construction
  , equalizers, equalizers0, equalizers1, equalizers2

    -- *** Orientation
  , equalizersOrnt

    -- * Coequalizers
  , Coequalizers, Coequalizer, CoequalizerCone, CoequalizerDiagram

    -- ** Construction
  , coequalizers, coequalizers'

    -- *** Orientation
  , coequalizersOrnt

    -- * Duality
  , coeqlLimitsDuality

  )
  where

import Data.Typeable

import OAlg.Prelude

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

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

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

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

--------------------------------------------------------------------------------
-- Equalizers -

-- | 'Diagram' for a equalizer. 
type EqualizerDiagram n = Diagram (Parallel LeftToRight) N2 n

-- | 'Cone' for a equalizer.
type EqualizerCone n = Cone Mlt Projective (Parallel LeftToRight) N2 n

-- | equalizer as 'Limes'.
type Equalizer n = Limes Mlt Projective (Parallel LeftToRight) N2 n

-- | equalizers for a 'Multiplicative' structures.
type Equalizers n = Limits Mlt Projective (Parallel LeftToRight) N2 n


--------------------------------------------------------------------------------
-- eqlProductDiagram -

-- | the underlying product diagram.
eqlProductDiagram :: EqualizerDiagram n a -> ProductDiagram N2 a
eqlProductDiagram :: forall (n :: N') a. EqualizerDiagram n a -> ProductDiagram N2 a
eqlProductDiagram (DiagramParallelLR Point a
p Point a
q FinList n a
_) = forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete (Point a
pforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|Point a
qforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)

--------------------------------------------------------------------------------
-- eqlProductCone -

-- | the underlying product cone.
eqlProductCone :: EqualizerCone n a -> ProductCone N2 a
eqlProductCone :: forall (n :: N') a. EqualizerCone n a -> ProductCone N2 a
eqlProductCone (ConeProjective Diagram ('Parallel 'LeftToRight) N2 n a
d Point a
t FinList N2 a
cs) = 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 (forall (n :: N') a. EqualizerDiagram n a -> ProductDiagram N2 a
eqlProductDiagram Diagram ('Parallel 'LeftToRight) N2 n a
d) Point a
t FinList N2 a
cs

--------------------------------------------------------------------------------
-- equalizers0 -

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

--------------------------------------------------------------------------------
-- eqlHeadDiagram -

-- | the underlying minimum diagram given by the first arrow.
eqlHeadDiagram :: EqualizerDiagram (n+1) a -> MinimumDiagram From N1 a
eqlHeadDiagram :: forall (n :: N') a.
EqualizerDiagram (n + 1) a -> MinimumDiagram 'From N1 a
eqlHeadDiagram (DiagramParallelLR Point a
p Point a
_ (a
a:|FinList n a
_)) = forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'From) (m + 1) m a
DiagramChainFrom Point a
p (a
aforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)

--------------------------------------------------------------------------------
-- eqlHeadCone -

-- | the underlying minimum cone given by the first arrow.
eqlHeadCone :: EqualizerCone (n+1) a -> MinimumCone From N1 a
eqlHeadCone :: forall (n :: N') a.
EqualizerCone (n + 1) a -> MinimumCone 'From N1 a
eqlHeadCone (ConeProjective Diagram ('Parallel 'LeftToRight) N2 (n + 1) a
d Point a
t FinList N2 a
cs) = 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 (forall (n :: N') a.
EqualizerDiagram (n + 1) a -> MinimumDiagram 'From N1 a
eqlHeadDiagram Diagram ('Parallel 'LeftToRight) N2 (n + 1) a
d) Point a
t FinList N2 a
cs

--------------------------------------------------------------------------------
-- equlizers1 -

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

--------------------------------------------------------------------------------
-- equlizers2 -

-- | promoting equalizers.
--
-- ![image equalizer](c:/Users/zeric/haskell/oalg/src/OAlg/Limes/equalizer.jpg)
equalizers2 :: Multiplicative a => Equalizers N2 a -> Equalizers (n+2) a
equalizers2 :: forall a (n :: N').
Multiplicative a =>
Equalizers N2 a -> Equalizers (n + 2) a
equalizers2 Equalizers N2 a
eql2 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a (n :: N') (n' :: N').
(Multiplicative a, n ~ (n' + 2)) =>
Equalizers N2 a -> EqualizerDiagram n a -> Equalizer n a
eql Equalizers N2 a
eql2) where
  eql :: (Multiplicative a, n ~ (n'+2))
      => Equalizers N2 a -> EqualizerDiagram n a -> Equalizer n a
  eql :: forall a (n :: N') (n' :: N').
(Multiplicative a, n ~ (n' + 2)) =>
Equalizers N2 a -> EqualizerDiagram n a -> Equalizer n a
eql Equalizers N2 a
eql2 d :: EqualizerDiagram n a
d@(DiagramParallelLR Point a
_ Point a
_ (a
_:|a
_:|FinList n a
Nil))        = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Equalizers N2 a
eql2 EqualizerDiagram n a
d
  eql Equalizers N2 a
eql2 d :: EqualizerDiagram n a
d@(DiagramParallelLR Point a
p Point a
q (a
a0:|aN :: FinList n a
aN@(a
_:|a
_:|FinList n a
_))) = 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 ('Parallel 'LeftToRight) N2 n a
l Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 n a -> a
u where
    dN :: Diagram ('Parallel 'LeftToRight) N2 n a
dN = forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) N2 m a
DiagramParallelLR Point a
p Point a
q FinList n a
aN
    LimesProjective (ConeProjective Diagram ('Parallel 'LeftToRight) N2 n a
_ Point a
h (a
h0:|a
h1:|FinList n a
Nil)) Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 n a -> a
Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S ('S n)) a -> a
uN = forall a (n :: N') (n' :: N').
(Multiplicative a, n ~ (n' + 2)) =>
Equalizers N2 a -> EqualizerDiagram n a -> Equalizer n a
eql Equalizers N2 a
eql2 Diagram ('Parallel 'LeftToRight) N2 n a
dN

    d2 :: Diagram ('Parallel 'LeftToRight) N2 N2 a
d2 = forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) N2 m a
DiagramParallelLR Point a
h Point a
q (a
a0forall c. Multiplicative c => c -> c -> c
*a
h0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|a
h1forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)
    LimesProjective (ConeProjective Diagram ('Parallel 'LeftToRight) N2 N2 a
_ Point a
k (a
k0:|a
k1:|FinList n a
Nil)) Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 N2 a -> a
u2 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Equalizers N2 a
eql2 Diagram ('Parallel 'LeftToRight) N2 N2 a
d2
    
    l :: Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 n a
l = 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 EqualizerDiagram n a
d Point a
k (a
h0forall c. Multiplicative c => c -> c -> c
*a
k0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|a
k1forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)
    u :: Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 n a -> a
u (ConeProjective EqualizerDiagram n a
_ Point a
x (a
x0:|a
x1:|FinList n a
Nil)) = a
uk where
      uk :: a
uk = Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 N2 a -> a
u2 (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 ('Parallel 'LeftToRight) N2 N2 a
d2 Point a
x (a
uhforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|a
x1forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil))
      uh :: a
uh = Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S ('S n)) a -> a
uN (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 ('Parallel 'LeftToRight) N2 n a
dN Point a
x (a
x0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|a
x1forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil))

--------------------------------------------------------------------------------
-- equlizers -

-- | equalizers of @n@ arrows given by products of two points and equalizers of two arrows.
equalizers :: Multiplicative a => Products N2 a -> Equalizers N2 a -> Equalizers n a
equalizers :: forall a (n :: N').
Multiplicative a =>
Products N2 a -> Equalizers N2 a -> Equalizers n a
equalizers Products N2 a
prd2 Equalizers N2 a
eql2 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a (n :: N').
Multiplicative a =>
Products N2 a
-> Equalizers N2 a -> EqualizerDiagram n a -> Equalizer n a
eql Products N2 a
prd2 Equalizers N2 a
eql2) where
  eql :: Multiplicative a
      => Products N2 a -> Equalizers N2 a -> EqualizerDiagram n a -> Equalizer n a
  eql :: forall a (n :: N').
Multiplicative a =>
Products N2 a
-> Equalizers N2 a -> EqualizerDiagram n a -> Equalizer n a
eql Products N2 a
prd2 Equalizers N2 a
eql2 EqualizerDiagram n a
d = case forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows EqualizerDiagram n a
d of
    FinList n a
Nil      -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes (forall a. Multiplicative a => Products N2 a -> Equalizers N0 a
equalizers0 Products N2 a
prd2) EqualizerDiagram n a
d
    a
_:|FinList n a
Nil   -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes forall a. Multiplicative a => Equalizers N1 a
equalizers1 EqualizerDiagram n a
d
    a
_:|a
_:|FinList n a
_  -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes (forall a (n :: N').
Multiplicative a =>
Equalizers N2 a -> Equalizers (n + 2) a
equalizers2 Equalizers N2 a
eql2) EqualizerDiagram n a
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 = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsToPrjOrnt

--------------------------------------------------------------------------------
-- Coequalizers -

-- | 'Diagram' for a coequalizer.
type CoequalizerDiagram n = Diagram (Parallel RightToLeft) N2 n

-- | 'Cone' for a coequalizer.
type CoequalizerCone n = Cone Mlt Injective (Parallel RightToLeft) N2 n

-- | coequalizer as 'Limes.
type Coequalizer n = Limes Mlt Injective (Parallel RightToLeft) N2 n

-- | coequalizers for a 'Multiplicative' structure.
type Coequalizers n       = Limits Mlt Injective (Parallel RightToLeft) N2 n

--------------------------------------------------------------------------------
-- Coequalizer - Duality -

-- | duality between coequalizers and equalizers.
coeqlLimitsDuality :: Multiplicative a
  => LimitsDuality Mlt (Coequalizers n) (Equalizers n) a
coeqlLimitsDuality :: forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Coequalizers n) (Equalizers n) a
coeqlLimitsDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limits s p t n m a)
-> (g (Op a) :~: Dual (Limits s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimitsDuality s f g a
LimitsDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- coequalizers -

-- | coequalizers of @n@ arrows given by sums of two points and coequalizers of two arrows.
coequalizers :: Multiplicative a => Sums N2 a -> Coequalizers N2 a -> Coequalizers n a
coequalizers :: forall a (n :: N').
Multiplicative a =>
Sums N2 a -> Coequalizers N2 a -> Coequalizers n a
coequalizers Sums N2 a
sum2 Coequalizers N2 a
coeql2 = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Coequalizers n) (Equalizers n) a
coeqlLimitsDuality forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (n :: N').
Multiplicative a =>
Products N2 a -> Equalizers N2 a -> Equalizers n a
equalizers Products N2 (Op a)
prd2 Equalizers N2 (Op a)
eql2 where
  prd2 :: Products N2 (Op a)
prd2 = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> f a -> g (Op a)
lmsToOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Sums n) (Products n) a
sumLimitsDuality Sums N2 a
sum2
  eql2 :: Equalizers N2 (Op a)
eql2 = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> f a -> g (Op a)
lmsToOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Coequalizers n) (Equalizers n) a
coeqlLimitsDuality Coequalizers N2 a
coeql2

-- | 'coequalizers' given by a proxy for @n@.
coequalizers' :: Multiplicative a
  => p n -> Sums N2 a -> Coequalizers N2 a -> Coequalizers n a
coequalizers' :: forall a (p :: N' -> *) (n :: N').
Multiplicative a =>
p n -> Sums N2 a -> Coequalizers N2 a -> Coequalizers n a
coequalizers' p n
_ = forall a (n :: N').
Multiplicative a =>
Sums N2 a -> Coequalizers N2 a -> Coequalizers n a
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 = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsFromInjOrnt