{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Limes.PullbacksAndPushouts
-- Description : pullbacks and pushouts
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- pullbacks and pushouts, i.e. limits of @'Diagram' ('Star' __d__)@.
module OAlg.Limes.PullbacksAndPushouts
  (
    -- * Pullbacks
    Pullbacks, Pullback, PullbackCone, PullbackDiagram

    -- ** Construction
  , pullbacks, pullbacks0, pullbacks1, plbPrdEql2

    -- *** Orientation
  , pullbacksOrnt

    -- * Pushouts
  , Pushouts, Pushout, PushoutCone, PushoutDiagram

    -- ** Construction
  , pushouts, pushouts', pshSumCoeql2

    -- *** Orientation
  , pushoutsOrnt

    -- * Duality
  , pshLimitsDuality

  )
  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
import OAlg.Limes.EqualizersAndCoequalizers


--------------------------------------------------------------------------------
-- Pullbacks -

-- | 'Diagram' for a pullback.
type PullbackDiagram n = Diagram (Star To) (n+1) n

-- | 'Cone' for a pullback.
type PullbackCone n = Cone Mlt Projective (Star To) (n+1) n

-- | pullback as 'Limes'.
type Pullback n = Limes Mlt Projective (Star To) (n+1) n

-- | pullbacks for 'Multiplicative' structures.
type Pullbacks n = Limits Mlt Projective (Star To) (n+1) n


--------------------------------------------------------------------------------
-- plbMinimumDiagram0 -

-- | the underlying minimum diagram.
plbMinimumDiagram0 :: PullbackDiagram n a -> MinimumDiagram To N0 a
plbMinimumDiagram0 :: forall (n :: N') a. PullbackDiagram n a -> MinimumDiagram 'To N0 a
plbMinimumDiagram0 (DiagramSink Point a
e FinList n a
_) = forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo Point a
e forall a. FinList N0 a
Nil


--------------------------------------------------------------------------------
-- plbMinimumCone0 -

-- | the underlying minimum cone.
plbMinimumCone0 :: PullbackCone n a -> MinimumCone To N0 a
plbMinimumCone0 :: forall (n :: N') a. PullbackCone n a -> MinimumCone 'To N0 a
plbMinimumCone0 (ConeProjective Diagram ('Star 'To) (n + 1) n a
d Point a
t (a
c0:|FinList n a
_))
  = 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. PullbackDiagram n a -> MinimumDiagram 'To N0 a
plbMinimumDiagram0 Diagram ('Star 'To) (n + 1) n a
d) Point a
t (a
c0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)

--------------------------------------------------------------------------------
-- pullbacks0 -

-- | pullbacks for zero arrows as 'Minima'.
pullbacks0 :: Multiplicative a => Pullbacks N0 a
pullbacks0 :: forall a. Multiplicative a => Pullbacks N0 a
pullbacks0 = 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 =>
Minima 'To N0 a -> PullbackDiagram N0 a -> Pullback N0 a
plb forall a (n :: N'). Multiplicative a => Minima 'To n a
minimaTo) where
  plb :: Multiplicative a => Minima To N0 a -> PullbackDiagram N0 a -> Pullback N0 a
  plb :: forall a.
Multiplicative a =>
Minima 'To N0 a -> PullbackDiagram N0 a -> Pullback N0 a
plb Minima 'To N0 a
min PullbackDiagram 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 ('Star 'To) ('S N0) N0 a
l Cone Mlt 'Projective ('Star 'To) ('S N0) N0 a -> a
u where
    LimesProjective Cone Mlt 'Projective ('Chain 'To) ('S N0) N0 a
lMin Cone Mlt 'Projective ('Chain 'To) ('S N0) N0 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 Minima 'To N0 a
min (forall (n :: N') a. PullbackDiagram n a -> MinimumDiagram 'To N0 a
plbMinimumDiagram0 PullbackDiagram N0 a
d)
    l :: Cone Mlt 'Projective ('Star 'To) ('S N0) 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 PullbackDiagram 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 ('Chain 'To) ('S N0) N0 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 'To) ('S N0) N0 a
lMin)  
    u :: Cone Mlt 'Projective ('Star 'To) ('S N0) N0 a -> a
u = Cone Mlt 'Projective ('Chain 'To) ('S N0) N0 a -> a
uMin forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (n :: N') a. PullbackCone n a -> MinimumCone 'To N0 a
plbMinimumCone0

--------------------------------------------------------------------------------
-- plbMinimumDiagram1 -

-- | the underlying minimum diagram given by the first arrow.
plbMinimumDiagram1 :: PullbackDiagram (n+1) a -> MinimumDiagram To N1 a
plbMinimumDiagram1 :: forall (n :: N') a.
PullbackDiagram (n + 1) a -> MinimumDiagram 'To ('S N0) a
plbMinimumDiagram1 (DiagramSink Point a
e (a
a0:|FinList n a
_)) = forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo Point a
e (a
a0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)

--------------------------------------------------------------------------------
-- plbMinimumCone1 -

-- | the underlying minimum cone given by the first arrow.
plbMinimumCone1 :: PullbackCone (n+1) a -> MinimumCone To N1 a
plbMinimumCone1 :: forall (n :: N') a.
PullbackCone (n + 1) a -> MinimumCone 'To ('S N0) a
plbMinimumCone1 (ConeProjective Diagram ('Star 'To) ((n + 1) + 1) (n + 1) a
d Point a
t (a
c0:|a
c1:|FinList n a
_))
  = 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.
PullbackDiagram (n + 1) a -> MinimumDiagram 'To ('S N0) a
plbMinimumDiagram1 Diagram ('Star 'To) ((n + 1) + 1) (n + 1) a
d) Point a
t (a
c0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|a
c1forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)

--------------------------------------------------------------------------------
-- pullbacks1 -

-- | pullbacks of one arrow, i.e. 'Minima'.
pullbacks1 :: Multiplicative a => Pullbacks N1 a
pullbacks1 :: forall a. Multiplicative a => Pullbacks ('S N0) a
pullbacks1 = 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 =>
Minima 'To ('S N0) a
-> PullbackDiagram ('S N0) a -> Pullback ('S N0) a
plb forall a (n :: N'). Multiplicative a => Minima 'To n a
minimaTo) where
  plb :: Multiplicative a => Minima To N1 a -> PullbackDiagram N1 a -> Pullback N1 a
  plb :: forall a.
Multiplicative a =>
Minima 'To ('S N0) a
-> PullbackDiagram ('S N0) a -> Pullback ('S N0) a
plb Minima 'To ('S N0) a
min PullbackDiagram ('S 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 ('Star 'To) ('S ('S N0)) ('S N0) a
l Cone Mlt 'Projective ('Star 'To) ('S ('S N0)) ('S N0) a -> a
u where
    LimesProjective Cone Mlt 'Projective ('Chain 'To) ('S ('S N0)) ('S N0) a
lMin Cone Mlt 'Projective ('Chain 'To) ('S ('S N0)) ('S N0) 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 Minima 'To ('S N0) a
min (forall (n :: N') a.
PullbackDiagram (n + 1) a -> MinimumDiagram 'To ('S N0) a
plbMinimumDiagram1 PullbackDiagram ('S N0) a
d)
    
    l :: Cone Mlt 'Projective ('Star 'To) ('S ('S N0)) ('S 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 PullbackDiagram ('S 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 ('Chain 'To) ('S ('S N0)) ('S N0) 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 'To) ('S ('S N0)) ('S N0) a
lMin)
    u :: Cone Mlt 'Projective ('Star 'To) ('S ('S N0)) ('S N0) a -> a
u = Cone Mlt 'Projective ('Chain 'To) ('S ('S N0)) ('S N0) a -> a
uMin forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (n :: N') a.
PullbackCone (n + 1) a -> MinimumCone 'To ('S N0) a
plbMinimumCone1

--------------------------------------------------------------------------------
-- pullbacks2 -

-- | promotion of pullbacks with at least two arrows.
pullbacks2 :: Multiplicative a => Pullbacks N2 a -> Pullbacks (n+2) a
pullbacks2 :: forall a (n :: N').
Multiplicative a =>
Pullbacks ('S ('S N0)) a -> Pullbacks (n + 2) a
pullbacks2 Pullbacks ('S ('S N0)) a
plb2 = 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 =>
Pullbacks ('S ('S N0)) a
-> PullbackDiagram (n + 2) a -> Pullback (n + 2) a
plb Pullbacks ('S ('S N0)) a
plb2) where
  plb :: Multiplicative a
      => Pullbacks N2 a -> PullbackDiagram (n+2) a -> Pullback (n+2) a
  plb :: forall a (n :: N').
Multiplicative a =>
Pullbacks ('S ('S N0)) a
-> PullbackDiagram (n + 2) a -> Pullback (n + 2) a
plb Pullbacks ('S ('S N0)) a
plb2 d :: PullbackDiagram (n + 2) a
d@(DiagramSink 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 Pullbacks ('S ('S N0)) a
plb2 PullbackDiagram (n + 2) a
d
  plb Pullbacks ('S ('S N0)) a
plb2 d :: PullbackDiagram (n + 2) a
d@(DiagramSink Point a
e (a
a1:|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
  ('Star 'To)
  ('S ('S ('S ('S n))))
  ('S ('S ('S n)))
  a
l Cone
  Mlt
  'Projective
  ('Star 'To)
  ('S ('S ('S ('S n))))
  ('S ('S ('S n)))
  a
-> a
u where
    dN :: Diagram ('Star 'To) (n + 1) n a
dN = forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink Point a
e FinList n a
aN
    LimesProjective (ConeProjective Diagram ('Star 'To) ((n + 2) + 1) (n + 2) a
_ Point a
_ (a
h1:|FinList n a
FinList ('S ('S n)) a
hN)) Cone Mlt 'Projective ('Star 'To) ((n + 2) + 1) (n + 2) a -> a
Cone Mlt 'Projective ('Star 'To) ('S ('S ('S n))) ('S ('S n)) a
-> a
uN = forall a (n :: N').
Multiplicative a =>
Pullbacks ('S ('S N0)) a
-> PullbackDiagram (n + 2) a -> Pullback (n + 2) a
plb Pullbacks ('S ('S N0)) a
plb2 Diagram ('Star 'To) (n + 1) n a
dN

    d2 :: Diagram ('Star 'To) ('S ('S N0) + 1) ('S ('S N0)) a
d2 = forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink Point a
e (a
a1forall 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 ('Star 'To) ((N0 + 2) + 1) (N0 + 2) a
_ Point a
k (a
k0:|a
k1:|a
k2:|FinList n a
Nil)) Cone Mlt 'Projective ('Star 'To) ((N0 + 2) + 1) (N0 + 2) a -> a
Cone Mlt 'Projective ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) a
-> a
u2 = forall a (n :: N').
Multiplicative a =>
Pullbacks ('S ('S N0)) a
-> PullbackDiagram (n + 2) a -> Pullback (n + 2) a
plb Pullbacks ('S ('S N0)) a
plb2 Diagram ('Star 'To) ('S ('S N0) + 1) ('S ('S N0)) a
d2
    
    l :: Cone
  Mlt
  'Projective
  ('Star 'To)
  ('S ('S ('S ('S n))))
  ('S ('S ('S 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 PullbackDiagram (n + 2) a
d Point a
k (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 (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall c. Multiplicative c => c -> c -> c
*a
k2) FinList ('S ('S n)) a
hN)
    u :: Cone
  Mlt
  'Projective
  ('Star 'To)
  ('S ('S ('S ('S n))))
  ('S ('S ('S n)))
  a
-> a
u (ConeProjective Diagram ('Star 'To) ('S ('S ('S ('S n)))) ('S ('S ('S n))) a
_ Point a
x (a
x0:|a
x1:|FinList n a
xN)) = Cone Mlt 'Projective ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) 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 ('Star 'To) ('S ('S N0) + 1) ('S ('S N0)) a
d2 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
:|a
uhforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)) where
      uh :: a
uh = Cone Mlt 'Projective ('Star 'To) ('S ('S ('S n))) ('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 ('Star 'To) (n + 1) n a
dN Point a
x (a
x0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|FinList n a
xN))

--------------------------------------------------------------------------------
-- pullbacks -

-- | promotion of pullbacks.
--
-- ![image pullback](c:/Users/zeric/haskell/oalg/src/OAlg/Limes/pullback.png)
pullbacks :: Multiplicative a => Pullbacks N2 a -> Pullbacks n a
pullbacks :: forall a (n :: N').
Multiplicative a =>
Pullbacks ('S ('S N0)) a -> Pullbacks n a
pullbacks Pullbacks ('S ('S N0)) a
plb2 = 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 =>
Pullbacks ('S ('S N0)) a -> PullbackDiagram n a -> Pullback n a
plb Pullbacks ('S ('S N0)) a
plb2) where
  plb :: Multiplicative a
      => Pullbacks N2 a -> PullbackDiagram n a -> Pullback n a
  plb :: forall a (n :: N').
Multiplicative a =>
Pullbacks ('S ('S N0)) a -> PullbackDiagram n a -> Pullback n a
plb Pullbacks ('S ('S N0)) a
plb2 PullbackDiagram n a
d = case forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows PullbackDiagram 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 => Pullbacks N0 a
pullbacks0 PullbackDiagram 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 => Pullbacks ('S N0) a
pullbacks1 PullbackDiagram 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 =>
Pullbacks ('S ('S N0)) a -> Pullbacks (n + 2) a
pullbacks2 Pullbacks ('S ('S N0)) a
plb2) PullbackDiagram n a
d

--------------------------------------------------------------------------------
-- plbPrdEql2 -

-- | pullbacks given by products and equalizers.
plbPrdEql2 :: Multiplicative a => Products N2 a -> Equalizers N2 a -> Pullbacks N2 a
plbPrdEql2 :: forall a.
Multiplicative a =>
Products ('S ('S N0)) a
-> Equalizers ('S ('S N0)) a -> Pullbacks ('S ('S N0)) a
plbPrdEql2 Products ('S ('S N0)) a
prd Equalizers ('S ('S N0)) a
eql = 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 ('S ('S N0)) a
-> Equalizers ('S ('S N0)) a
-> PullbackDiagram ('S ('S N0)) a
-> Pullback ('S ('S N0)) a
plb Products ('S ('S N0)) a
prd Equalizers ('S ('S N0)) a
eql) where
  plb :: Multiplicative a
    => Products N2 a -> Equalizers N2 a -> PullbackDiagram N2 a -> Pullback N2 a
  plb :: forall a.
Multiplicative a =>
Products ('S ('S N0)) a
-> Equalizers ('S ('S N0)) a
-> PullbackDiagram ('S ('S N0)) a
-> Pullback ('S ('S N0)) a
plb Products ('S ('S N0)) a
prd Equalizers ('S ('S N0)) a
eql d :: PullbackDiagram ('S ('S N0)) a
d@(DiagramSink Point a
s as :: FinList ('S ('S N0)) a
as@(a
f:|a
g:|FinList n a
Nil)) = 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 ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) a
l Cone Mlt 'Projective ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) a
-> a
u where
    LimesProjective Cone Mlt 'Projective 'Discrete ('S ('S N0)) N0 a
p Cone Mlt 'Projective 'Discrete ('S ('S N0)) N0 a -> a
uPrd = 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 ('S ('S N0)) a
prd (forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall q. Oriented q => q -> Point q
start FinList ('S ('S N0)) a
as)
    shp :: FinList ('S ('S N0)) a
shp@(a
pf:|a
pg:|FinList n a
Nil) = 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 ('S ('S N0)) N0 a
p
    dp :: Diagram 'Discrete ('S ('S N0)) N0 a
dp = 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 'Discrete ('S ('S N0)) N0 a
p

    LimesProjective Cone
  Mlt
  'Projective
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  a
e Cone
  Mlt
  'Projective
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  a
-> a
uEql = 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 ('S ('S N0)) a
eql (forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S ('S N0)) m a
DiagramParallelLR (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 ('S ('S N0)) N0 a
p) Point a
s (a
fforall c. Multiplicative c => c -> c -> c
*a
pfforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|a
gforall c. Multiplicative c => c -> c -> c
*a
pgforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil))
    a
e0:|a
e1:|FinList n a
Nil = 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
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  a
e
    de :: Diagram ('Parallel 'LeftToRight) ('S ('S N0)) ('S ('S N0)) a
de = 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
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  a
e
    
    l :: Cone Mlt 'Projective ('Star 'To) ('S ('S ('S N0))) ('S ('S 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 PullbackDiagram ('S ('S 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
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  a
e) (a
e1forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall c. Multiplicative c => c -> c -> c
*a
e0) FinList ('S ('S N0)) a
shp) 
    u :: Cone Mlt 'Projective ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) a
-> a
u (ConeProjective Diagram ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) a
_ Point a
x (a
x0:|FinList n a
xs)) = Cone
  Mlt
  'Projective
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  a
-> a
uEql (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) ('S ('S N0)) ('S ('S N0)) a
de Point a
x (a
upforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|a
x0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)) where
      up :: a
up = Cone Mlt 'Projective 'Discrete ('S ('S N0)) N0 a -> a
uPrd (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 'Discrete ('S ('S N0)) N0 a
dp Point a
x FinList n a
xs)

--------------------------------------------------------------------------------
-- pullbacksOrnt -

-- | pullbacks for 'Orientation'.
pullbacksOrnt :: Entity p => p -> Pullbacks n (Orientation p)
pullbacksOrnt :: forall p (n :: N'). Entity p => p -> Pullbacks n (Orientation p)
pullbacksOrnt = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsToPrjOrnt

--------------------------------------------------------------------------------
-- Pushouts -

-- | 'Diagram' for a pushout.
type PushoutDiagram n = Diagram (Star From) (n+1) n

-- | 'Cone' for a pushout.
type PushoutCone n = Cone Mlt Injective (Star From) (n+1) n

-- | pushout as 'Limes'.
type Pushout n = Limes Mlt Injective (Star From) (n+1) n

-- | pushouts for a 'Multiplicative' structures.
type Pushouts n       = Limits Mlt Injective (Star From) (n+1) n

--------------------------------------------------------------------------------
-- Pusouts - Duality -

-- | duality between pushouts and pullbacks.
pshLimitsDuality :: Multiplicative a
  => LimitsDuality Mlt (Pushouts n) (Pullbacks n) a
pshLimitsDuality :: forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Pushouts n) (Pullbacks n) a
pshLimitsDuality = 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

--------------------------------------------------------------------------------
-- pushouts -

-- | promotion of pushouts.
pushouts :: Multiplicative a => Pushouts N2 a -> Pushouts n a
pushouts :: forall a (n :: N').
Multiplicative a =>
Pushouts ('S ('S N0)) a -> Pushouts n a
pushouts Pushouts ('S ('S N0)) a
psh2 = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Pushouts n) (Pullbacks n) a
pshLimitsDuality forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (n :: N').
Multiplicative a =>
Pullbacks ('S ('S N0)) a -> Pullbacks n a
pullbacks Limits
  Mlt 'Projective ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) (Op a)
plb2 where
  plb2 :: Limits
  Mlt 'Projective ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) (Op a)
plb2 = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> f a -> g (Op a)
lmsToOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Pushouts n) (Pullbacks n) a
pshLimitsDuality Pushouts ('S ('S N0)) a
psh2

-- | 'pushouts' given by a proxy for @n@.
pushouts' :: Multiplicative a => p n -> Pushouts N2 a -> Pushouts n a
pushouts' :: forall a (p :: N' -> *) (n :: N').
Multiplicative a =>
p n -> Pushouts ('S ('S N0)) a -> Pushouts n a
pushouts' p n
_ = forall a (n :: N').
Multiplicative a =>
Pushouts ('S ('S N0)) a -> Pushouts n a
pushouts

--------------------------------------------------------------------------------
-- pushoutsOrnt -

-- | pushouts for 'Orientation'.
pushoutsOrnt :: Entity p => p -> Pushouts n (Orientation p)
pushoutsOrnt :: forall p (n :: N'). Entity p => p -> Pushouts n (Orientation p)
pushoutsOrnt = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsFromInjOrnt

--------------------------------------------------------------------------------
-- pshSumCoeql2 -

-- | pushouts given by sums and coequalizers.
pshSumCoeql2 :: Multiplicative a => Sums N2 a -> Coequalizers N2 a -> Pushouts N2 a
pshSumCoeql2 :: forall a.
Multiplicative a =>
Sums ('S ('S N0)) a
-> Coequalizers ('S ('S N0)) a -> Pushouts ('S ('S N0)) a
pshSumCoeql2 Sums ('S ('S N0)) a
sum Coequalizers ('S ('S N0)) a
coeql = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Pushouts n) (Pullbacks n) a
pshLimitsDuality forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a.
Multiplicative a =>
Products ('S ('S N0)) a
-> Equalizers ('S ('S N0)) a -> Pullbacks ('S ('S N0)) a
plbPrdEql2 Products ('S ('S N0)) (Op a)
prd Equalizers ('S ('S N0)) (Op a)
eql where
  prd :: Products ('S ('S N0)) (Op a)
prd = 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 ('S ('S N0)) a
sum
  eql :: Equalizers ('S ('S N0)) (Op a)
eql = 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 ('S ('S N0)) a
coeql