{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, 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, PullbacksG
  , Pullback, PullbackG
  , PullbackCone, PullbackConic
  , PullbackDiagram, PullbackDiagrammatic

    -- ** Construction

  , pullbacks, pullbacks0, pullbacks1, plbPrdEql2

    -- *** Orientation

  , pullbacksOrnt

    -- * Pushouts

  , Pushouts, PushoutsG
  , Pushout, PushoutG
  , PushoutCone, PushoutConic
  , PushoutDiagram, PushoutDiagrammatic

    -- ** Construction

  , pushouts, pushouts', pshSumCoeql2

    -- *** Orientation

  , pushoutsOrnt

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

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

-- Pullbacks -


-- | 'Diagrammatic' object for a pullback.

type PullbackDiagrammatic d (n :: N') = d (Star To) (n+1) n :: Type -> Type

-- | 'Diagram' for a pullback.

type PullbackDiagram n = PullbackDiagrammatic Diagram n

-- | 'Conic' object for a pullback.

type PullbackConic c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N')
  = c Mlt Projective d (Star To) (n+1) n :: Type -> Type

-- | 'Cone' for a pullback.

type PullbackCone n = PullbackConic Cone Diagram n

-- | generic pullback as 'LimesG'.

type PullbackG c d n = LimesG c Mlt Projective d (Star To) (n+1) n

-- | pullback as 'PullbackG'.

type Pullback n = PullbackG Cone Diagram n

-- | generic pullbacks for 'Multiplicative' structures.

type PullbacksG c d n = LimitsG c Mlt Projective d (Star To) (n+1) n

-- | pullbacks for 'Multiplicative' structures.

type Pullbacks n = PullbacksG Cone Diagram n

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

-- plbMinimumDiagram0 -


-- | the underlying minimum diagram.

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


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

-- plbMinimumCone0 -


-- | the underlying minimum cone.

plbMinimumCone0 :: PullbackCone n x -> MinimumCone To N0 x
plbMinimumCone0 :: forall (n :: N') x. PullbackCone n x -> MinimumCone 'To N0 x
plbMinimumCone0 (ConeProjective Diagram ('Star 'To) (n + 1) n x
d Point x
t (x
c0:|FinList n1 x
_))
  = Diagram ('Chain 'To) ('S N0) N0 x
-> Point x
-> FinList ('S N0) x
-> Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) 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 ('Star 'To) (n + 1) n x -> MinimumDiagram 'To N0 x
forall (n :: N') x. PullbackDiagram n x -> MinimumDiagram 'To N0 x
plbMinimumDiagram0 Diagram ('Star 'To) (n + 1) n x
d) Point x
t (x
c0x -> 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)

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

-- pullbacks0 -


-- | pullbacks for zero arrows as 'Minima'.

pullbacks0 :: Multiplicative x => Pullbacks N0 x
pullbacks0 :: forall x. Multiplicative x => Pullbacks N0 x
pullbacks0 = (Diagram ('Star 'To) ('S N0) N0 x
 -> LimesG Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) N0 x)
-> LimitsG Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) 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 (Minima 'To N0 x -> PullbackDiagram N0 x -> Pullback N0 x
forall x.
Multiplicative x =>
Minima 'To N0 x -> PullbackDiagram N0 x -> Pullback N0 x
plb Minima 'To N0 x
forall x (n :: N'). Multiplicative x => Minima 'To n x
minimaTo) where
  plb :: Multiplicative x => Minima To N0 x -> PullbackDiagram N0 x -> Pullback N0 x
  plb :: forall x.
Multiplicative x =>
Minima 'To N0 x -> PullbackDiagram N0 x -> Pullback N0 x
plb Minima 'To N0 x
min PullbackDiagram N0 x
d = Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) N0 x
-> (Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) N0 x -> x)
-> LimesG Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) 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 ('Star 'To) ('S N0) N0 x
l Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) N0 x -> x
u where
    LimesProjective Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) N0 x
lMin Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) N0 x -> x
uMin = LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) N0 x
-> Diagram ('Chain 'To) ('S N0) N0 x
-> LimesG Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) 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 Minima 'To N0 x
LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) N0 x
min (PullbackDiagram N0 x -> MinimumDiagram 'To N0 x
forall (n :: N') x. PullbackDiagram n x -> MinimumDiagram 'To N0 x
plbMinimumDiagram0 PullbackDiagram N0 x
d)
    l :: Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) N0 x
l = Diagram ('Star 'To) ('S N0) N0 x
-> Point x
-> FinList ('S N0) x
-> Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) 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 PullbackDiagram N0 x
Diagram ('Star 'To) ('S N0) N0 x
d (Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) 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 ('Chain 'To) ('S N0) N0 x
lMin) (Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) N0 x
-> FinList ('S N0) 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 'To) ('S N0) N0 x
lMin)  
    u :: Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) N0 x -> x
u = Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) N0 x -> x
uMin (Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) N0 x -> x)
-> (Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) N0 x
    -> Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) N0 x)
-> Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) 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
. PullbackCone N0 x -> MinimumCone 'To N0 x
Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) N0 x
-> Cone Mlt 'Projective Diagram ('Chain 'To) ('S N0) N0 x
forall (n :: N') x. PullbackCone n x -> MinimumCone 'To N0 x
plbMinimumCone0

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

-- plbMinimumDiagram1 -


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

plbMinimumDiagram1 :: PullbackDiagram (n+1) x -> MinimumDiagram To N1 x
plbMinimumDiagram1 :: forall (n :: N') x.
PullbackDiagram (n + 1) x -> MinimumDiagram 'To ('S N0) x
plbMinimumDiagram1 (DiagramSink Point x
e (x
a0:|FinList n1 x
_)) = Point x
-> FinList ('S N0) x -> Diagram ('Chain 'To) ('S N0 + 1) ('S N0) x
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo Point x
e (x
a0x -> 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)

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

-- plbMinimumCone1 -


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

plbMinimumCone1 :: PullbackCone (n+1) x -> MinimumCone To N1 x
plbMinimumCone1 :: forall (n :: N') x.
PullbackCone (n + 1) x -> MinimumCone 'To ('S N0) x
plbMinimumCone1 (ConeProjective Diagram ('Star 'To) ((n + 1) + 1) (n + 1) x
d Point x
t (x
c0:|x
c1:|FinList n1 x
_))
  = Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
-> Point x
-> FinList ('S ('S N0)) x
-> Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S 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 ('Star 'To) ((n + 1) + 1) (n + 1) x
-> MinimumDiagram 'To ('S N0) x
forall (n :: N') x.
PullbackDiagram (n + 1) x -> MinimumDiagram 'To ('S N0) x
plbMinimumDiagram1 Diagram ('Star 'To) ((n + 1) + 1) (n + 1) x
d) Point x
t (x
c0x -> FinList ('S N0) x -> FinList ('S N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
c1x -> 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)

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

-- pullbacks1 -


-- | pullbacks of one arrow, i.e. 'Minima'.

pullbacks1 :: Multiplicative x => Pullbacks N1 x
pullbacks1 :: forall x. Multiplicative x => Pullbacks ('S N0) x
pullbacks1 = (Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
 -> LimesG
      Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S N0) x)
-> LimitsG
     Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S 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 (Minima 'To ('S N0) x
-> PullbackDiagram ('S N0) x -> Pullback ('S N0) x
forall x.
Multiplicative x =>
Minima 'To ('S N0) x
-> PullbackDiagram ('S N0) x -> Pullback ('S N0) x
plb Minima 'To ('S N0) x
forall x (n :: N'). Multiplicative x => Minima 'To n x
minimaTo) where
  plb :: Multiplicative x => Minima To N1 x -> PullbackDiagram N1 x -> Pullback N1 x
  plb :: forall x.
Multiplicative x =>
Minima 'To ('S N0) x
-> PullbackDiagram ('S N0) x -> Pullback ('S N0) x
plb Minima 'To ('S N0) x
min PullbackDiagram ('S N0) x
d = Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
-> (Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
    -> x)
-> LimesG
     Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S 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 ('Star 'To) ('S ('S N0)) ('S N0) x
l Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
-> x
u where
    LimesProjective Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
lMin Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
-> x
uMin = LimitsG
  Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
-> Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
-> LimesG
     Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S 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 Minima 'To ('S N0) x
LimitsG
  Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
min (PullbackDiagram (N0 + 1) x -> MinimumDiagram 'To ('S N0) x
forall (n :: N') x.
PullbackDiagram (n + 1) x -> MinimumDiagram 'To ('S N0) x
plbMinimumDiagram1 PullbackDiagram (N0 + 1) x
PullbackDiagram ('S N0) x
d)
    
    l :: Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
l = Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
-> Point x
-> FinList ('S ('S N0)) x
-> Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S 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 PullbackDiagram ('S N0) x
Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
d (Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S 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 ('Chain 'To) ('S ('S N0)) ('S N0) x
lMin) (Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
-> FinList ('S ('S N0)) 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 'To) ('S ('S N0)) ('S N0) x
lMin)
    u :: Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
-> x
u = Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
-> x
uMin (Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
 -> x)
-> (Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
    -> Cone
         Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x)
-> Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S 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
. PullbackCone (N0 + 1) x -> MinimumCone 'To ('S N0) x
Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) ('S N0) x
-> Cone Mlt 'Projective Diagram ('Chain 'To) ('S ('S N0)) ('S N0) x
forall (n :: N') x.
PullbackCone (n + 1) x -> MinimumCone 'To ('S N0) x
plbMinimumCone1

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

-- pullbacks2 -


-- | promotion of pullbacks with at least two arrows.

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

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

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

-- pullbacks -


-- | promotion of pullbacks.

--

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

pullbacks :: Multiplicative x => Pullbacks N2 x -> Pullbacks n x
pullbacks :: forall x (n :: N').
Multiplicative x =>
Pullbacks ('S ('S N0)) x -> Pullbacks n x
pullbacks Pullbacks ('S ('S N0)) x
plb2 = (Diagram ('Star 'To) ('S n) n x
 -> LimesG Cone Mlt 'Projective Diagram ('Star 'To) ('S n) n x)
-> LimitsG Cone Mlt 'Projective Diagram ('Star 'To) ('S n) 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 (Pullbacks ('S ('S N0)) x -> PullbackDiagram n x -> Pullback n x
forall x (n :: N').
Multiplicative x =>
Pullbacks ('S ('S N0)) x -> PullbackDiagram n x -> Pullback n x
plb Pullbacks ('S ('S N0)) x
plb2) where
  plb :: Multiplicative x
      => Pullbacks N2 x -> PullbackDiagram n x -> Pullback n x
  plb :: forall x (n :: N').
Multiplicative x =>
Pullbacks ('S ('S N0)) x -> PullbackDiagram n x -> Pullback n x
plb Pullbacks ('S ('S N0)) x
plb2 PullbackDiagram n x
d = case Diagram ('Star 'To) ('S n) n x -> FinList n x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows PullbackDiagram n x
Diagram ('Star 'To) ('S n) n x
d of
    FinList n x
Nil     -> LimitsG Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) n x
-> Diagram ('Star 'To) ('S N0) n x
-> LimesG Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) 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 Pullbacks N0 x
LimitsG Cone Mlt 'Projective Diagram ('Star 'To) ('S N0) n x
forall x. Multiplicative x => Pullbacks N0 x
pullbacks0 PullbackDiagram n x
Diagram ('Star 'To) ('S N0) n x
d
    x
_:|FinList n1 x
Nil  -> LimitsG Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) n x
-> Diagram ('Star 'To) ('S ('S N0)) n x
-> LimesG Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) 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 Pullbacks ('S N0) x
LimitsG Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N0)) n x
forall x. Multiplicative x => Pullbacks ('S N0) x
pullbacks1 PullbackDiagram n x
Diagram ('Star 'To) ('S ('S N0)) n x
d
    x
_:|x
_:|FinList n1 x
_ -> LimitsG
  Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S ('S n1))) n x
-> Diagram ('Star 'To) ('S ('S ('S n1))) n x
-> LimesG
     Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S ('S n1))) 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 (Pullbacks ('S ('S N0)) x -> Pullbacks (n1 + 2) x
forall x (n :: N').
Multiplicative x =>
Pullbacks ('S ('S N0)) x -> Pullbacks (n + 2) x
pullbacks2 Pullbacks ('S ('S N0)) x
plb2) PullbackDiagram n x
Diagram ('Star 'To) ('S ('S ('S n1))) n x
d

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

-- plbPrdEql2 -




-- | pullbacks given by products and equalizers.

plbPrdEql2 :: Multiplicative x => Products N2 x -> Equalizers N2 x -> Pullbacks N2 x
plbPrdEql2 :: forall x.
Multiplicative x =>
Products ('S ('S N0)) x
-> Equalizers ('S ('S N0)) x -> Pullbacks ('S ('S N0)) x
plbPrdEql2 Products ('S ('S N0)) x
prd Equalizers ('S ('S N0)) x
eql = (Diagram ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) x
 -> LimesG
      Cone
      Mlt
      'Projective
      Diagram
      ('Star 'To)
      ('S ('S ('S N0)))
      ('S ('S N0))
      x)
-> LimitsG
     Cone
     Mlt
     'Projective
     Diagram
     ('Star 'To)
     ('S ('S ('S N0)))
     ('S ('S 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 ('S ('S N0)) x
-> Equalizers ('S ('S N0)) x
-> PullbackDiagram ('S ('S N0)) x
-> Pullback ('S ('S N0)) x
forall x.
Multiplicative x =>
Products ('S ('S N0)) x
-> Equalizers ('S ('S N0)) x
-> PullbackDiagram ('S ('S N0)) x
-> Pullback ('S ('S N0)) x
plb Products ('S ('S N0)) x
prd Equalizers ('S ('S N0)) x
eql) where
  cnDiagram :: Cone s p Diagram t n m x -> Diagram t n m x
cnDiagram = Diagram t n m x -> Diagram t n m x
forall (t :: DiagramType) (n :: N') (m :: N') x.
Diagram t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram (Diagram t n m x -> Diagram t n m x)
-> (Cone s p Diagram t n m x -> Diagram t n m x)
-> Cone s p Diagram t n m x
-> Diagram t n m 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 s p Diagram t n m x -> Diagram t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> d t n m a
diagrammaticObject
  
  plb :: Multiplicative x
    => Products N2 x -> Equalizers N2 x -> PullbackDiagram N2 x -> Pullback N2 x
  plb :: forall x.
Multiplicative x =>
Products ('S ('S N0)) x
-> Equalizers ('S ('S N0)) x
-> PullbackDiagram ('S ('S N0)) x
-> Pullback ('S ('S N0)) x
plb Products ('S ('S N0)) x
prd Equalizers ('S ('S N0)) x
eql d :: PullbackDiagram ('S ('S N0)) x
d@(DiagramSink Point x
s as :: FinList ('S ('S N0)) x
as@(x
f:|x
g:|FinList n1 x
Nil)) = Cone
  Mlt
  'Projective
  Diagram
  ('Star 'To)
  ('S ('S ('S N0)))
  ('S ('S N0))
  x
-> (Cone
      Mlt
      'Projective
      Diagram
      ('Star 'To)
      ('S ('S ('S N0)))
      ('S ('S N0))
      x
    -> x)
-> LimesG
     Cone
     Mlt
     'Projective
     Diagram
     ('Star 'To)
     ('S ('S ('S N0)))
     ('S ('S 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
  ('Star 'To)
  ('S ('S ('S N0)))
  ('S ('S N0))
  x
l Cone
  Mlt
  'Projective
  Diagram
  ('Star 'To)
  ('S ('S ('S N0)))
  ('S ('S N0))
  x
-> x
u where
    LimesProjective Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) N0 x
p Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) N0 x -> x
uPrd = Products ('S ('S N0)) x
-> Diagram 'Discrete ('S ('S N0)) N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) 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 ('S ('S N0)) x
prd (FinList ('S ('S N0)) (Point x)
-> Diagram 'Discrete ('S ('S N0)) N0 x
forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete (FinList ('S ('S N0)) (Point x)
 -> Diagram 'Discrete ('S ('S N0)) N0 x)
-> FinList ('S ('S N0)) (Point x)
-> Diagram 'Discrete ('S ('S N0)) N0 x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (x -> Point x)
-> FinList ('S ('S N0)) x -> FinList ('S ('S N0)) (Point x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> Point x
forall q. Oriented q => q -> Point q
start FinList ('S ('S N0)) x
as)
    shp :: FinList ('S ('S N0)) x
shp@(x
pf:|x
pg:|FinList n1 x
Nil) = Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) N0 x
-> FinList ('S ('S N0)) 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 ('S ('S N0)) N0 x
p
    dp :: Diagram 'Discrete ('S ('S N0)) N0 x
dp = Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) N0 x
-> Diagram 'Discrete ('S ('S N0)) N0 x
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'} {x}.
Cone s p Diagram t n m x -> Diagram t n m x
cnDiagram Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) N0 x
p

    LimesProjective Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  x
e Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  x
-> x
uEql = Equalizers ('S ('S N0)) x
-> Diagram ('Parallel 'LeftToRight) ('S ('S N0)) ('S ('S N0)) x
-> LimesG
     Cone
     Mlt
     'Projective
     Diagram
     ('Parallel 'LeftToRight)
     ('S ('S N0))
     ('S ('S 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 Equalizers ('S ('S N0)) x
eql (Point x
-> Point x
-> FinList ('S ('S N0)) x
-> Diagram ('Parallel 'LeftToRight) ('S ('S N0)) ('S ('S N0)) x
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S ('S N0)) m a
DiagramParallelLR (Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) 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 ('S ('S N0)) N0 x
p) Point x
s (x
fx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
pfx -> FinList ('S N0) x -> FinList ('S N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
gx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
pgx -> 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))
    x
e0:|x
e1:|FinList n1 x
Nil = Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  x
-> FinList ('S ('S N0)) 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
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  x
e
    de :: Diagram ('Parallel 'LeftToRight) ('S ('S N0)) ('S ('S N0)) x
de = Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  x
-> Diagram ('Parallel 'LeftToRight) ('S ('S N0)) ('S ('S N0)) x
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'} {x}.
Cone s p Diagram t n m x -> Diagram t n m x
cnDiagram Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  x
e
    
    l :: Cone
  Mlt
  'Projective
  Diagram
  ('Star 'To)
  ('S ('S ('S N0)))
  ('S ('S N0))
  x
l = Diagram ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) x
-> Point x
-> FinList ('S ('S ('S N0))) x
-> Cone
     Mlt
     'Projective
     Diagram
     ('Star 'To)
     ('S ('S ('S N0)))
     ('S ('S 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 PullbackDiagram ('S ('S N0)) x
Diagram ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) x
d (Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S 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
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  x
e) (x
e1x -> FinList ('S ('S N0)) x -> FinList ('S ('S N0) + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|(x -> x) -> FinList ('S ('S N0)) x -> FinList ('S ('S N0)) x
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (x -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
e0) FinList ('S ('S N0)) x
shp) 
    u :: Cone
  Mlt
  'Projective
  Diagram
  ('Star 'To)
  ('S ('S ('S N0)))
  ('S ('S N0))
  x
-> x
u (ConeProjective Diagram ('Star 'To) ('S ('S ('S N0))) ('S ('S N0)) x
_ Point x
x (x
x0:|FinList n1 x
xs)) = Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S ('S N0))
  ('S ('S N0))
  x
-> x
uEql (Diagram ('Parallel 'LeftToRight) ('S ('S N0)) ('S ('S N0)) x
-> Point x
-> FinList ('S ('S N0)) x
-> Cone
     Mlt
     'Projective
     Diagram
     ('Parallel 'LeftToRight)
     ('S ('S N0))
     ('S ('S 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) ('S ('S N0)) ('S ('S N0)) x
de Point x
x (x
upx -> FinList ('S N0) x -> FinList ('S N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
x0x -> 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)) where
      up :: x
up = Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) N0 x -> x
uPrd (Diagram 'Discrete ('S ('S N0)) N0 x
-> Point x
-> FinList ('S ('S N0)) x
-> Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) 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 'Discrete ('S ('S N0)) N0 x
dp Point x
x FinList n1 x
FinList ('S ('S N0)) x
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 = p
-> LimitsG
     Cone Mlt 'Projective Diagram ('Star 'To) (n + 1) n (Orientation p)
p -> Limits Mlt 'Projective ('Star 'To) ('S n) n (Orientation p)
forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsMltPrjOrnt


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

-- Pushouts -


-- | 'Diagrammatic' object for a pushout.

type PushoutDiagrammatic d (n :: N') = d (Star From) (n+1) n :: Type -> Type

-- | 'Diagram' for a pushout.

type PushoutDiagram n = PushoutDiagrammatic Diagram n

-- | 'Conic' object for a pushout.

type PushoutConic c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N')
  = c Mlt Injective d (Star From) (n+1) n :: Type -> Type

-- | 'Cone' for a pushout.

type PushoutCone n = PushoutConic Cone Diagram n

-- | generic pushout as 'LimesG'.

type PushoutG c d n = LimesG c Mlt Injective d (Star From) (n+1) n

-- | pushout as 'Limes'.

type Pushout n = PushoutG Cone Diagram n

-- | generic pushouts for 'Multiplicative' structures.

type PushoutsG c d n = LimitsG c Mlt Injective d (Star From) (n+1) n

-- | pushouts for 'Multiplicative' structures.

type Pushouts n = PushoutsG Cone Diagram n


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

-- pushouts -


-- | promotion of pushouts.

pushouts :: Multiplicative x => Pushouts N2 x -> Pushouts n x
pushouts :: forall x (n :: N').
Multiplicative x =>
Pushouts ('S ('S N0)) x -> Pushouts n x
pushouts Pushouts ('S ('S N0)) x
psh2 = LimitsG Cone Mlt 'Injective Diagram ('Star 'From) (n + 1) n x
LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n x
pshs 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
     ('Star 'From)
     ('S ('S ('S N0)))
     ('S ('S N0)))
  (Op x)
plb2)  = IsoO Mlt Op x (Op x)
-> SDualBi
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S N0)))
     x
-> SDualBi
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S 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
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S N0))))
  (LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Star 'From)
     ('S ('S ('S N0)))
     ('S ('S N0)))
  x
-> SDualBi
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S N0)))
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimitsG
  Cone
  Mlt
  'Injective
  Diagram
  ('Star 'From)
  ('S ('S ('S N0)))
  ('S ('S N0))
  x
-> Either1
     (Dual1
        (LimitsG
           Cone
           Mlt
           'Injective
           Diagram
           ('Star 'From)
           ('S ('S ('S N0)))
           ('S ('S N0))))
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S N0)))
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Pushouts ('S ('S N0)) x
LimitsG
  Cone
  Mlt
  'Injective
  Diagram
  ('Star 'From)
  ('S ('S ('S N0)))
  ('S ('S N0))
  x
psh2))
  plbs :: Pullbacks n (Op x)
plbs                  = Pullbacks ('S ('S N0)) (Op x) -> Pullbacks n (Op x)
forall x (n :: N').
Multiplicative x =>
Pullbacks ('S ('S N0)) x -> Pullbacks n x
pullbacks Dual1
  (LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Star 'From)
     ('S ('S ('S N0)))
     ('S ('S N0)))
  (Op x)
Pullbacks ('S ('S N0)) (Op x)
plb2
  SDualBi (Right1 LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n x
pshs) = Inv2 (HomDisjEmpty Mlt Op) (Op x) x
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n) (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) 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 ('Star 'From) ('S n) n))
  (LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n)
  (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Dual1
  (LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n) (Op x)
-> Either1
     (Dual1
        (LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n))
     (LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Dual1
  (LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n) (Op x)
Pullbacks n (Op x)
plbs))
  

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

pushouts' :: Multiplicative x => p n -> Pushouts N2 x -> Pushouts n x
pushouts' :: forall x (p :: N' -> *) (n :: N').
Multiplicative x =>
p n -> Pushouts ('S ('S N0)) x -> Pushouts n x
pushouts' p n
_ = Pushouts ('S ('S N0)) x -> Pushouts n x
forall x (n :: N').
Multiplicative x =>
Pushouts ('S ('S N0)) x -> Pushouts n x
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 = p
-> LimitsG
     Cone Mlt 'Injective Diagram ('Star 'From) (n + 1) n (Orientation p)
p -> Limits Mlt 'Injective ('Star 'From) ('S n) n (Orientation p)
forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsMltInjOrnt

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

-- pshSumCoeql2 -


-- | pushouts given by sums and coequalizers.

pshSumCoeql2 :: Multiplicative x => Sums N2 x -> Coequalizers N2 x -> Pushouts N2 x
pshSumCoeql2 :: forall x.
Multiplicative x =>
Sums ('S ('S N0)) x
-> Coequalizers ('S ('S N0)) x -> Pushouts ('S ('S N0)) x
pshSumCoeql2 Sums ('S ('S N0)) x
sum Coequalizers ('S ('S N0)) x
coeql = LimitsG
  Cone
  Mlt
  'Injective
  Diagram
  ('Star 'From)
  ('S ('S N0) + 1)
  ('S ('S N0))
  x
LimitsG
  Cone
  Mlt
  'Injective
  Diagram
  ('Star 'From)
  ('S ('S ('S N0)))
  ('S ('S N0))
  x
pshs 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 ('S ('S N0)) N0)
  (Op x)
prd)   = IsoO Mlt Op x (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S N0)) N0) x
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S N0)) 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 ('S ('S N0)) N0))
  (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S N0)) N0)
  x
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S N0)) N0) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Sums ('S ('S N0)) x
-> Either1
     (LimitsG Cone Mlt 'Projective Diagram 'Discrete ('S ('S N0)) N0)
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S N0)) N0)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Sums ('S ('S N0)) x
sum))
  SDualBi (Left1 Dual1
  (LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Parallel 'RightToLeft)
     ('S ('S N0))
     ('S ('S N0)))
  (Op x)
eql)   = IsoO Mlt Op x (Op x)
-> SDualBi
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Parallel 'RightToLeft)
        ('S ('S N0))
        ('S ('S N0)))
     x
-> SDualBi
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Parallel 'RightToLeft)
        ('S ('S N0))
        ('S ('S 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
        ('Parallel 'RightToLeft)
        ('S ('S N0))
        ('S ('S N0))))
  (LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Parallel 'RightToLeft)
     ('S ('S N0))
     ('S ('S N0)))
  x
-> SDualBi
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Parallel 'RightToLeft)
        ('S ('S N0))
        ('S ('S N0)))
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Coequalizers ('S ('S N0)) x
-> Either1
     (LimitsG
        Cone
        Mlt
        'Projective
        Diagram
        ('Parallel 'LeftToRight)
        ('S ('S N0))
        ('S ('S N0)))
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Parallel 'RightToLeft)
        ('S ('S N0))
        ('S ('S N0)))
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Coequalizers ('S ('S N0)) x
coeql))
  plbs :: Pullbacks ('S ('S N0)) (Op x)
plbs                  = Products ('S ('S N0)) (Op x)
-> Equalizers ('S ('S N0)) (Op x) -> Pullbacks ('S ('S N0)) (Op x)
forall x.
Multiplicative x =>
Products ('S ('S N0)) x
-> Equalizers ('S ('S N0)) x -> Pullbacks ('S ('S N0)) x
plbPrdEql2 Dual1
  (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S N0)) N0)
  (Op x)
Products ('S ('S N0)) (Op x)
prd Dual1
  (LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Parallel 'RightToLeft)
     ('S ('S N0))
     ('S ('S N0)))
  (Op x)
Equalizers ('S ('S N0)) (Op x)
eql
  SDualBi (Right1 LimitsG
  Cone
  Mlt
  'Injective
  Diagram
  ('Star 'From)
  ('S ('S ('S N0)))
  ('S ('S N0))
  x
pshs) = Inv2 (HomDisjEmpty Mlt Op) (Op x) x
-> SDualBi
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S N0)))
     (Op x)
-> SDualBi
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S N0)))
     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
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S N0))))
  (LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Star 'From)
     ('S ('S ('S N0)))
     ('S ('S N0)))
  (Op x)
-> SDualBi
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S N0)))
     (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Dual1
  (LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Star 'From)
     ('S ('S ('S N0)))
     ('S ('S N0)))
  (Op x)
-> Either1
     (Dual1
        (LimitsG
           Cone
           Mlt
           'Injective
           Diagram
           ('Star 'From)
           ('S ('S ('S N0)))
           ('S ('S N0))))
     (LimitsG
        Cone
        Mlt
        'Injective
        Diagram
        ('Star 'From)
        ('S ('S ('S N0)))
        ('S ('S N0)))
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Dual1
  (LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Star 'From)
     ('S ('S ('S N0)))
     ('S ('S N0)))
  (Op x)
Pullbacks ('S ('S N0)) (Op x)
plbs))