{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : An 'OrdinalCategory' is a 'TotalOrder' category where the total order is an order induced by ordinal numbers. 
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

An 'OrdinalCategory' is a 'TotalOrder' category where the total order is an order induced by ordinal numbers. 

Concretely the type parameter must implement the Enum typeclass.

For example, the 'TotalOrder' category induced by (R,<=) is not an 'OrdinalCategory' whereas (N,<=) is.

It induces a non trivial generating set of arrows thanks to the 'succ' function.
-}

module Math.Categories.OrdinalCategory
(
    OrdinalCategory(..),
    module Math.Categories.TotalOrder
    
)
where
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.CompleteCategory
    import              Math.CocompleteCategory
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.TotalOrder
    import              Math.FiniteCategories.Parallel
    import              Math.IO.PrettyPrint
    
    import qualified    Data.WeakSet          as Set
    import              Data.WeakSet.Safe
    import qualified    Data.WeakMap          as Map
    import              Data.WeakMap.Safe
    import              Data.Simplifiable
    
    import              GHC.Generics
    
    -- | An 'OrdinalCategory' is a 'TotalOrder' where the type /a/ follows the Enum typeclass.

    newtype OrdinalCategory a = OrdinalCategory (TotalOrder a) deriving (OrdinalCategory a -> OrdinalCategory a -> Bool
(OrdinalCategory a -> OrdinalCategory a -> Bool)
-> (OrdinalCategory a -> OrdinalCategory a -> Bool)
-> Eq (OrdinalCategory a)
forall a. OrdinalCategory a -> OrdinalCategory a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. OrdinalCategory a -> OrdinalCategory a -> Bool
== :: OrdinalCategory a -> OrdinalCategory a -> Bool
$c/= :: forall a. OrdinalCategory a -> OrdinalCategory a -> Bool
/= :: OrdinalCategory a -> OrdinalCategory a -> Bool
Eq, Int -> OrdinalCategory a -> ShowS
[OrdinalCategory a] -> ShowS
OrdinalCategory a -> String
(Int -> OrdinalCategory a -> ShowS)
-> (OrdinalCategory a -> String)
-> ([OrdinalCategory a] -> ShowS)
-> Show (OrdinalCategory a)
forall a. Int -> OrdinalCategory a -> ShowS
forall a. [OrdinalCategory a] -> ShowS
forall a. OrdinalCategory a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Int -> OrdinalCategory a -> ShowS
showsPrec :: Int -> OrdinalCategory a -> ShowS
$cshow :: forall a. OrdinalCategory a -> String
show :: OrdinalCategory a -> String
$cshowList :: forall a. [OrdinalCategory a] -> ShowS
showList :: [OrdinalCategory a] -> ShowS
Show, (forall x. OrdinalCategory a -> Rep (OrdinalCategory a) x)
-> (forall x. Rep (OrdinalCategory a) x -> OrdinalCategory a)
-> Generic (OrdinalCategory a)
forall x. Rep (OrdinalCategory a) x -> OrdinalCategory a
forall x. OrdinalCategory a -> Rep (OrdinalCategory a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (OrdinalCategory a) x -> OrdinalCategory a
forall a x. OrdinalCategory a -> Rep (OrdinalCategory a) x
$cfrom :: forall a x. OrdinalCategory a -> Rep (OrdinalCategory a) x
from :: forall x. OrdinalCategory a -> Rep (OrdinalCategory a) x
$cto :: forall a x. Rep (OrdinalCategory a) x -> OrdinalCategory a
to :: forall x. Rep (OrdinalCategory a) x -> OrdinalCategory a
Generic, Int -> Int -> String -> OrdinalCategory a -> String
Int -> OrdinalCategory a -> String
(Int -> OrdinalCategory a -> String)
-> (Int -> Int -> String -> OrdinalCategory a -> String)
-> (Int -> OrdinalCategory a -> String)
-> PrettyPrint (OrdinalCategory a)
forall a. Int -> Int -> String -> OrdinalCategory a -> String
forall a. Int -> OrdinalCategory a -> String
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
$cpprint :: forall a. Int -> OrdinalCategory a -> String
pprint :: Int -> OrdinalCategory a -> String
$cpprintWithIndentations :: forall a. Int -> Int -> String -> OrdinalCategory a -> String
pprintWithIndentations :: Int -> Int -> String -> OrdinalCategory a -> String
$cpprintIndent :: forall a. Int -> OrdinalCategory a -> String
pprintIndent :: Int -> OrdinalCategory a -> String
PrettyPrint, OrdinalCategory a -> OrdinalCategory a
(OrdinalCategory a -> OrdinalCategory a)
-> Simplifiable (OrdinalCategory a)
forall a. OrdinalCategory a -> OrdinalCategory a
forall a. (a -> a) -> Simplifiable a
$csimplify :: forall a. OrdinalCategory a -> OrdinalCategory a
simplify :: OrdinalCategory a -> OrdinalCategory a
Simplifiable)
    
    instance (Enum a, Ord a) => Category (OrdinalCategory a) (IsSmallerThan a) a where
        ar :: Morphism (IsSmallerThan a) a =>
OrdinalCategory a -> a -> a -> Set (IsSmallerThan a)
ar OrdinalCategory a
_ a
x a
y
            | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y = [IsSmallerThan a] -> Set (IsSmallerThan a)
forall a. [a] -> Set a
set [a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
y]
            | Bool
otherwise = [IsSmallerThan a] -> Set (IsSmallerThan a)
forall a. [a] -> Set a
set []
            
        identity :: Morphism (IsSmallerThan a) a =>
OrdinalCategory a -> a -> IsSmallerThan a
identity OrdinalCategory a
_ a
x = a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
x
        
        -- | An 'OrdinalCategory' is generated by morphisms from a number to its successor.

        genAr :: Morphism (IsSmallerThan a) a =>
OrdinalCategory a -> a -> a -> Set (IsSmallerThan a)
genAr OrdinalCategory a
_ a
x a
y
            | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [IsSmallerThan a] -> Set (IsSmallerThan a)
forall a. [a] -> Set a
set [a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
x]
            | (a -> a
forall a. Enum a => a -> a
succ a
x) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [IsSmallerThan a] -> Set (IsSmallerThan a)
forall a. [a] -> Set a
set [a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
y]
            | Bool
otherwise = [IsSmallerThan a] -> Set (IsSmallerThan a)
forall a. [a] -> Set a
set []
  
        decompose :: Morphism (IsSmallerThan a) a =>
OrdinalCategory a -> IsSmallerThan a -> [IsSmallerThan a]
decompose OrdinalCategory a
_ (IsSmallerThan a
x a
y)
            | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
y]
            | Bool
otherwise = [IsSmallerThan a] -> [IsSmallerThan a]
forall a. [a] -> [a]
reverse ([IsSmallerThan a] -> [IsSmallerThan a])
-> [IsSmallerThan a] -> [IsSmallerThan a]
forall a b. (a -> b) -> a -> b
$ (\a
n -> a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
n (a -> a
forall a. Enum a => a -> a
succ a
n)) (a -> IsSmallerThan a) -> [a] -> [IsSmallerThan a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a
x..(a -> a
forall a. Enum a => a -> a
pred a
y)]
    
    instance (Enum a, Ord a, Eq oIndex) => HasProducts (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a oIndex where
        product :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
product Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag = a
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone a
apexProduct NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
nat
            where
                apexProduct :: a
apexProduct = Set a -> a
forall a. Ord a => Set a -> a
Set.minimum (Set a -> a) -> Set a -> a
forall a b. (a -> b) -> a -> b
$ Map oIndex a -> Set a
forall k a. Eq k => Map k a -> Set a
Map.values (Map oIndex a -> Set a) -> Map oIndex a -> Set a
forall a b. (a -> b) -> a -> b
$ Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Map oIndex a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag
                nat :: NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
nat = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (DiscreteCategory oIndex
-> OrdinalCategory a
-> a
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> DiscreteCategory oIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag) (TotalOrder a -> OrdinalCategory a
forall a. TotalOrder a -> OrdinalCategory a
OrdinalCategory TotalOrder a
forall a. TotalOrder a
TotalOrder) a
apexProduct) Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag (Map oIndex (IsSmallerThan a)
 -> NaturalTransformation
      (DiscreteCategory oIndex)
      (DiscreteMorphism oIndex)
      oIndex
      (OrdinalCategory a)
      (IsSmallerThan a)
      a)
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall a b. (a -> b) -> a -> b
$ Set (oIndex, IsSmallerThan a) -> Map oIndex (IsSmallerThan a)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
i,a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
apexProduct (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> oIndex -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i)) | oIndex
i <- DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob (DiscreteCategory oIndex -> Set oIndex)
-> DiscreteCategory oIndex -> Set oIndex
forall a b. (a -> b) -> a -> b
$ Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> DiscreteCategory oIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag]
                
    instance (Enum a, Ord a) => HasEqualizers (OrdinalCategory a) (IsSmallerThan a) a where
        equalize :: Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Cone
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
equalize Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag = a
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
-> Cone
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone a
apexEq NaturalTransformation
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
nat
            where
                apexEq :: a
apexEq = Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> ParallelOb -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA
                nat :: NaturalTransformation
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
nat = Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
-> Map ParallelOb (IsSmallerThan a)
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (Parallel
-> OrdinalCategory a
-> a
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram Parallel
Parallel (TotalOrder a -> OrdinalCategory a
forall a. TotalOrder a -> OrdinalCategory a
OrdinalCategory TotalOrder a
forall a. TotalOrder a
TotalOrder) a
apexEq) Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag (AssociationList ParallelOb (IsSmallerThan a)
-> Map ParallelOb (IsSmallerThan a)
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelOb
ParallelA, a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
apexEq a
apexEq),(ParallelOb
ParallelB, a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> ParallelOb -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB) (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> ParallelOb -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB))])
                
    instance (Enum a, Ord a, Eq mIndex, Eq oIndex) => CompleteCategory (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a cIndex mIndex oIndex where
        limit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Cone
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
limit Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag = a
-> NaturalTransformation
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Cone
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cone c1 m1 o1 c2 m2 o2
unsafeCone a
apexLimit NaturalTransformation
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
nat
            where
                apexLimit :: a
apexLimit = Set a -> a
forall a. Ord a => Set a -> a
Set.minimum (Set a -> a) -> Set a -> a
forall a b. (a -> b) -> a -> b
$ Map oIndex a -> Set a
forall k a. Eq k => Map k a -> Set a
Map.values (Map oIndex a -> Set a) -> Map oIndex a -> Set a
forall a b. (a -> b) -> a -> b
$ Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Map oIndex a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag
                nat :: NaturalTransformation
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
nat = Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Diagram
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (cIndex
-> OrdinalCategory a
-> a
-> Diagram
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram (Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag) (TotalOrder a -> OrdinalCategory a
forall a. TotalOrder a -> OrdinalCategory a
OrdinalCategory TotalOrder a
forall a. TotalOrder a
TotalOrder) a
apexLimit) Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag (Map oIndex (IsSmallerThan a)
 -> NaturalTransformation
      cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a)
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
forall a b. (a -> b) -> a -> b
$ Set (oIndex, IsSmallerThan a) -> Map oIndex (IsSmallerThan a)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
i,a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
apexLimit (Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> oIndex -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i)) | oIndex
i <- cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob (cIndex -> Set oIndex) -> cIndex -> Set oIndex
forall a b. (a -> b) -> a -> b
$ Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag]
                
        projectBase :: Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Diagram
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
projectBase Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag = Diagram{src :: OrdinalCategory a
src = Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> OrdinalCategory a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag, tgt :: OrdinalCategory a
tgt = Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> OrdinalCategory a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag, omap :: Map a a
omap = (a -> a) -> Set a -> Map a a
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction a -> a
forall a. a -> a
id (Map oIndex a -> Set a
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Map oIndex a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag)), mmap :: Map (IsSmallerThan a) (IsSmallerThan a)
mmap = (IsSmallerThan a -> IsSmallerThan a)
-> Set (IsSmallerThan a) -> Map (IsSmallerThan a) (IsSmallerThan a)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction IsSmallerThan a -> IsSmallerThan a
forall a. a -> a
id (Map mIndex (IsSmallerThan a) -> Set (IsSmallerThan a)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Map mIndex (IsSmallerThan a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag))}
                
    instance (Enum a, Ord a, Eq oIndex) => HasCoproducts (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a oIndex where
        coproduct :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
coproduct Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag = a
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone a
nadirCoproduct NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
nat
            where
                nadirCoproduct :: a
nadirCoproduct = Set a -> a
forall a. Ord a => Set a -> a
Set.maximum (Set a -> a) -> Set a -> a
forall a b. (a -> b) -> a -> b
$ Map oIndex a -> Set a
forall k a. Eq k => Map k a -> Set a
Map.values (Map oIndex a -> Set a) -> Map oIndex a -> Set a
forall a b. (a -> b) -> a -> b
$ Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Map oIndex a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag
                nat :: NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
nat = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag (DiscreteCategory oIndex
-> OrdinalCategory a
-> a
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> DiscreteCategory oIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag) (TotalOrder a -> OrdinalCategory a
forall a. TotalOrder a -> OrdinalCategory a
OrdinalCategory TotalOrder a
forall a. TotalOrder a
TotalOrder) a
nadirCoproduct) (Map oIndex (IsSmallerThan a)
 -> NaturalTransformation
      (DiscreteCategory oIndex)
      (DiscreteMorphism oIndex)
      oIndex
      (OrdinalCategory a)
      (IsSmallerThan a)
      a)
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall a b. (a -> b) -> a -> b
$ Set (oIndex, IsSmallerThan a) -> Map oIndex (IsSmallerThan a)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
i,a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan (Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> oIndex -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i) a
nadirCoproduct) | oIndex
i <- DiscreteCategory oIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob (DiscreteCategory oIndex -> Set oIndex)
-> DiscreteCategory oIndex -> Set oIndex
forall a b. (a -> b) -> a -> b
$ Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> DiscreteCategory oIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
diag]
                
    instance (Enum a, Ord a) => HasCoequalizers (OrdinalCategory a) (IsSmallerThan a) a where
        coequalize :: Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Cocone
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
coequalize Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag = a
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
-> Cocone
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone a
nadirCoeq NaturalTransformation
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
nat
            where
                nadirCoeq :: a
nadirCoeq = Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> ParallelOb -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelB
                nat :: NaturalTransformation
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
nat = Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
-> Map ParallelOb (IsSmallerThan a)
-> NaturalTransformation
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag (Parallel
-> OrdinalCategory a
-> a
-> Diagram
     Parallel
     ParallelAr
     ParallelOb
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram Parallel
Parallel (TotalOrder a -> OrdinalCategory a
forall a. TotalOrder a -> OrdinalCategory a
OrdinalCategory TotalOrder a
forall a. TotalOrder a
TotalOrder) a
nadirCoeq) (AssociationList ParallelOb (IsSmallerThan a)
-> Map ParallelOb (IsSmallerThan a)
forall k v. AssociationList k v -> Map k v
weakMap [(ParallelOb
ParallelA, a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> ParallelOb -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA) (Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
parallelDiag Diagram
  Parallel
  ParallelAr
  ParallelOb
  (OrdinalCategory a)
  (IsSmallerThan a)
  a
-> ParallelOb -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ ParallelOb
ParallelA)),(ParallelOb
ParallelB, a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
nadirCoeq a
nadirCoeq)])
                
    instance (Enum a, Ord a, Eq mIndex, Eq oIndex) => CocompleteCategory (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a cIndex mIndex oIndex where
        colimit :: (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
 Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Cocone
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
colimit Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag = a
-> NaturalTransformation
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Cocone
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
forall o2 c1 m1 o1 c2 m2.
o2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
-> Cocone c1 m1 o1 c2 m2 o2
unsafeCocone a
nadirColimit NaturalTransformation
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
nat
            where
                nadirColimit :: a
nadirColimit = Set a -> a
forall a. Ord a => Set a -> a
Set.maximum (Set a -> a) -> Set a -> a
forall a b. (a -> b) -> a -> b
$ Map oIndex a -> Set a
forall k a. Eq k => Map k a -> Set a
Map.values (Map oIndex a -> Set a) -> Map oIndex a -> Set a
forall a b. (a -> b) -> a -> b
$ Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Map oIndex a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag
                nat :: NaturalTransformation
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
nat = Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Diagram
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag (cIndex
-> OrdinalCategory a
-> a
-> Diagram
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram (Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag) (TotalOrder a -> OrdinalCategory a
forall a. TotalOrder a -> OrdinalCategory a
OrdinalCategory TotalOrder a
forall a. TotalOrder a
TotalOrder) a
nadirColimit) (Map oIndex (IsSmallerThan a)
 -> NaturalTransformation
      cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a)
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
forall a b. (a -> b) -> a -> b
$ Set (oIndex, IsSmallerThan a) -> Map oIndex (IsSmallerThan a)
forall k v. Set (k, v) -> Map k v
Map.weakMapFromSet [(oIndex
i,a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan (Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> oIndex -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ oIndex
i) a
nadirColimit) | oIndex
i <- cIndex -> Set oIndex
forall c m o. FiniteCategory c m o => c -> Set o
ob (cIndex -> Set oIndex) -> cIndex -> Set oIndex
forall a b. (a -> b) -> a -> b
$ Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> cIndex
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag]
                
        coprojectBase :: Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Diagram
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
     (OrdinalCategory a)
     (IsSmallerThan a)
     a
coprojectBase Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag = Diagram{src :: OrdinalCategory a
src = Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> OrdinalCategory a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag, tgt :: OrdinalCategory a
tgt = Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> OrdinalCategory a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag, omap :: Map a a
omap = (a -> a) -> Set a -> Map a a
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction a -> a
forall a. a -> a
id (Map oIndex a -> Set a
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Map oIndex a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag)), mmap :: Map (IsSmallerThan a) (IsSmallerThan a)
mmap = (IsSmallerThan a -> IsSmallerThan a)
-> Set (IsSmallerThan a) -> Map (IsSmallerThan a) (IsSmallerThan a)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction IsSmallerThan a -> IsSmallerThan a
forall a. a -> a
id (Map mIndex (IsSmallerThan a) -> Set (IsSmallerThan a)
forall k a. Eq k => Map k a -> Set a
Map.values (Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
-> Map mIndex (IsSmallerThan a)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap Diagram
  cIndex mIndex oIndex (OrdinalCategory a) (IsSmallerThan a) a
diag))}