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

{-| Module  : FiniteCategories
Description : Any total (or linear) order induces a preorder category where elements are objects, there is an arrow between two objects iff the relation is satisfied.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Any total (or linear) order induces a preorder category where elements are objects, there is an arrow between two objects iff the relation is satisfied.

(See Categories for the working mathematican. Saunders Mac Lane. p.11)
-}

module Math.Categories.TotalOrder
(
    IsSmallerThan(..),
    TotalOrder(..),
    
)
where
    import              Math.FiniteCategory
    import              Math.Category
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.CompleteCategory
    import              Math.CocompleteCategory
    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
    
    -- | 'IsSmallerThan' is the type of morphisms in a linear order, it reminds the fact that there is a morphism from a source to a target iff the source is smaller than the target.

    data IsSmallerThan a = IsSmallerThan a a deriving (IsSmallerThan a -> IsSmallerThan a -> Bool
(IsSmallerThan a -> IsSmallerThan a -> Bool)
-> (IsSmallerThan a -> IsSmallerThan a -> Bool)
-> Eq (IsSmallerThan a)
forall a. Eq a => IsSmallerThan a -> IsSmallerThan a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => IsSmallerThan a -> IsSmallerThan a -> Bool
== :: IsSmallerThan a -> IsSmallerThan a -> Bool
$c/= :: forall a. Eq a => IsSmallerThan a -> IsSmallerThan a -> Bool
/= :: IsSmallerThan a -> IsSmallerThan a -> Bool
Eq, Int -> IsSmallerThan a -> ShowS
[IsSmallerThan a] -> ShowS
IsSmallerThan a -> String
(Int -> IsSmallerThan a -> ShowS)
-> (IsSmallerThan a -> String)
-> ([IsSmallerThan a] -> ShowS)
-> Show (IsSmallerThan a)
forall a. Show a => Int -> IsSmallerThan a -> ShowS
forall a. Show a => [IsSmallerThan a] -> ShowS
forall a. Show a => IsSmallerThan a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> IsSmallerThan a -> ShowS
showsPrec :: Int -> IsSmallerThan a -> ShowS
$cshow :: forall a. Show a => IsSmallerThan a -> String
show :: IsSmallerThan a -> String
$cshowList :: forall a. Show a => [IsSmallerThan a] -> ShowS
showList :: [IsSmallerThan a] -> ShowS
Show, (forall x. IsSmallerThan a -> Rep (IsSmallerThan a) x)
-> (forall x. Rep (IsSmallerThan a) x -> IsSmallerThan a)
-> Generic (IsSmallerThan a)
forall x. Rep (IsSmallerThan a) x -> IsSmallerThan a
forall x. IsSmallerThan a -> Rep (IsSmallerThan a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (IsSmallerThan a) x -> IsSmallerThan a
forall a x. IsSmallerThan a -> Rep (IsSmallerThan a) x
$cfrom :: forall a x. IsSmallerThan a -> Rep (IsSmallerThan a) x
from :: forall x. IsSmallerThan a -> Rep (IsSmallerThan a) x
$cto :: forall a x. Rep (IsSmallerThan a) x -> IsSmallerThan a
to :: forall x. Rep (IsSmallerThan a) x -> IsSmallerThan a
Generic, IsSmallerThan a -> IsSmallerThan a
(IsSmallerThan a -> IsSmallerThan a)
-> Simplifiable (IsSmallerThan a)
forall a. Simplifiable a => IsSmallerThan a -> IsSmallerThan a
forall a. (a -> a) -> Simplifiable a
$csimplify :: forall a. Simplifiable a => IsSmallerThan a -> IsSmallerThan a
simplify :: IsSmallerThan a -> IsSmallerThan a
Simplifiable)
    
    instance (Eq a) => Morphism (IsSmallerThan a) a where
        (IsSmallerThan a
m1 a
t) @ :: IsSmallerThan a -> IsSmallerThan a -> IsSmallerThan a
@ (IsSmallerThan a
s a
m2) = a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
s a
t
        source :: IsSmallerThan a -> a
source (IsSmallerThan a
s a
_) = a
s
        target :: IsSmallerThan a -> a
target (IsSmallerThan a
_ a
t) = a
t
    
    -- | A 'TotalOrder' category is the category induced by a total order.

    --

    -- (See Categories for the working mathematican. Saunders Mac Lane. p.11)

    data TotalOrder a = TotalOrder deriving (TotalOrder a -> TotalOrder a -> Bool
(TotalOrder a -> TotalOrder a -> Bool)
-> (TotalOrder a -> TotalOrder a -> Bool) -> Eq (TotalOrder a)
forall a. TotalOrder a -> TotalOrder a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. TotalOrder a -> TotalOrder a -> Bool
== :: TotalOrder a -> TotalOrder a -> Bool
$c/= :: forall a. TotalOrder a -> TotalOrder a -> Bool
/= :: TotalOrder a -> TotalOrder a -> Bool
Eq, Int -> TotalOrder a -> ShowS
[TotalOrder a] -> ShowS
TotalOrder a -> String
(Int -> TotalOrder a -> ShowS)
-> (TotalOrder a -> String)
-> ([TotalOrder a] -> ShowS)
-> Show (TotalOrder a)
forall a. Int -> TotalOrder a -> ShowS
forall a. [TotalOrder a] -> ShowS
forall a. TotalOrder a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Int -> TotalOrder a -> ShowS
showsPrec :: Int -> TotalOrder a -> ShowS
$cshow :: forall a. TotalOrder a -> String
show :: TotalOrder a -> String
$cshowList :: forall a. [TotalOrder a] -> ShowS
showList :: [TotalOrder a] -> ShowS
Show, (forall x. TotalOrder a -> Rep (TotalOrder a) x)
-> (forall x. Rep (TotalOrder a) x -> TotalOrder a)
-> Generic (TotalOrder a)
forall x. Rep (TotalOrder a) x -> TotalOrder a
forall x. TotalOrder a -> Rep (TotalOrder a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (TotalOrder a) x -> TotalOrder a
forall a x. TotalOrder a -> Rep (TotalOrder a) x
$cfrom :: forall a x. TotalOrder a -> Rep (TotalOrder a) x
from :: forall x. TotalOrder a -> Rep (TotalOrder a) x
$cto :: forall a x. Rep (TotalOrder a) x -> TotalOrder a
to :: forall x. Rep (TotalOrder a) x -> TotalOrder a
Generic, Int -> Int -> String -> TotalOrder a -> String
Int -> TotalOrder a -> String
(Int -> TotalOrder a -> String)
-> (Int -> Int -> String -> TotalOrder a -> String)
-> (Int -> TotalOrder a -> String)
-> PrettyPrint (TotalOrder a)
forall a. Int -> Int -> String -> TotalOrder a -> String
forall a. Int -> TotalOrder a -> String
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
$cpprint :: forall a. Int -> TotalOrder a -> String
pprint :: Int -> TotalOrder a -> String
$cpprintWithIndentations :: forall a. Int -> Int -> String -> TotalOrder a -> String
pprintWithIndentations :: Int -> Int -> String -> TotalOrder a -> String
$cpprintIndent :: forall a. Int -> TotalOrder a -> String
pprintIndent :: Int -> TotalOrder a -> String
PrettyPrint, TotalOrder a -> TotalOrder a
(TotalOrder a -> TotalOrder a) -> Simplifiable (TotalOrder a)
forall a. TotalOrder a -> TotalOrder a
forall a. (a -> a) -> Simplifiable a
$csimplify :: forall a. TotalOrder a -> TotalOrder a
simplify :: TotalOrder a -> TotalOrder a
Simplifiable)
    
    instance (Eq a, Ord a) => Category (TotalOrder a) (IsSmallerThan a) a where
        identity :: Morphism (IsSmallerThan a) a =>
TotalOrder a -> a -> IsSmallerThan a
identity TotalOrder a
_ a
x = a -> a -> IsSmallerThan a
forall a. a -> a -> IsSmallerThan a
IsSmallerThan a
x a
x
        ar :: Morphism (IsSmallerThan a) a =>
TotalOrder a -> a -> a -> Set (IsSmallerThan a)
ar TotalOrder 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 []
    
    instance (PrettyPrint a) => PrettyPrint (IsSmallerThan a) where
        pprint :: Int -> IsSmallerThan a -> String
pprint Int
0 (IsSmallerThan a
x a
y) = Int -> a -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
0 a
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> a -> String
forall a. PrettyPrint a => Int -> a -> String
pprint Int
0 a
y
        pprint Int
v (IsSmallerThan a
x a
y) = Int -> a -> String
forall a. PrettyPrint a => Int -> a -> String
pprint (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) a
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> a -> String
forall a. PrettyPrint a => Int -> a -> String
pprint (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) a
y
        
        -- pprintWithIndentations 0 ov indent (IsSmallerThan x y) = indentation ov indent ++ pprint 0 x++" <= "++pprint 0 y ++ "\n"

        -- pprintWithIndentations cv ov indent (IsSmallerThan x y) = indentation (ov - cv) indent ++ pprint (cv-1) x++" <= "++pprint (cv-1) y ++ "\n"

        
    instance (Ord a, Eq oIndex) => HasProducts (TotalOrder a) (IsSmallerThan a) a (TotalOrder a) (IsSmallerThan a) a oIndex where
        product :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder a)
  (IsSmallerThan a)
  a
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder a)
     (IsSmallerThan a)
     a
product Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag = a
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder a)
     (IsSmallerThan a)
     a
-> Cone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder 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
  (TotalOrder 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
  (TotalOrder 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
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag
                nat :: NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder a)
  (IsSmallerThan a)
  a
nat = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder a)
  (IsSmallerThan a)
  a
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder a)
     (IsSmallerThan a)
     a
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder 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
-> TotalOrder a
-> a
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder 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
  (TotalOrder 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
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag) TotalOrder a
forall a. TotalOrder a
TotalOrder a
apexProduct) Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag (Map oIndex (IsSmallerThan a)
 -> NaturalTransformation
      (DiscreteCategory oIndex)
      (DiscreteMorphism oIndex)
      oIndex
      (TotalOrder a)
      (IsSmallerThan a)
      a)
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder 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
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder 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
  (TotalOrder 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
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag]
                
    instance (Ord a) => HasEqualizers (TotalOrder a) (IsSmallerThan a) a where
        equalize :: Diagram
  Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
-> Cone
     Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
equalize Diagram
  Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
parallelDiag = a
-> NaturalTransformation
     Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
-> Cone
     Parallel ParallelAr ParallelOb (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
nat
            where
                apexEq :: a
apexEq = Diagram
  Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
nat = Diagram
  Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
-> Diagram
     Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
-> Map ParallelOb (IsSmallerThan a)
-> NaturalTransformation
     Parallel ParallelAr ParallelOb (TotalOrder 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
-> TotalOrder a
-> a
-> Diagram
     Parallel ParallelAr ParallelOb (TotalOrder 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
forall a. TotalOrder a
TotalOrder a
apexEq) Diagram
  Parallel ParallelAr ParallelOb (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (TotalOrder 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 (Ord a, Eq mIndex, Eq oIndex) => CompleteCategory (TotalOrder a) (IsSmallerThan a) a (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
-> Cone cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
limit Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
diag = a
-> NaturalTransformation
     cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> Cone cIndex mIndex oIndex (TotalOrder 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
  cIndex mIndex oIndex (TotalOrder 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 cIndex mIndex oIndex (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag
                nat :: NaturalTransformation
  cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
nat = Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     cIndex mIndex oIndex (TotalOrder 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
-> TotalOrder a
-> a
-> Diagram cIndex mIndex oIndex (TotalOrder 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 (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag) TotalOrder a
forall a. TotalOrder a
TotalOrder a
apexProduct) Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
diag (Map oIndex (IsSmallerThan a)
 -> NaturalTransformation
      cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a)
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     cIndex mIndex oIndex (TotalOrder 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 cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
diag Diagram cIndex mIndex oIndex (TotalOrder 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 (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag]
                
        projectBase :: Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> Diagram
     (TotalOrder a)
     (IsSmallerThan a)
     a
     (TotalOrder a)
     (IsSmallerThan a)
     a
projectBase Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
diag = Diagram{src :: TotalOrder a
src = Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> TotalOrder a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
diag, tgt :: TotalOrder a
tgt = Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> TotalOrder a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram cIndex mIndex oIndex (TotalOrder 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 (TotalOrder 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 (TotalOrder 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 (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag))}
                
    instance (Ord a, Eq oIndex) => HasCoproducts (TotalOrder a) (IsSmallerThan a) a (TotalOrder a) (IsSmallerThan a) a oIndex where
        coproduct :: Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder a)
  (IsSmallerThan a)
  a
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder a)
     (IsSmallerThan a)
     a
coproduct Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag = a
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder a)
     (IsSmallerThan a)
     a
-> Cocone
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder 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
  (TotalOrder 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
  (TotalOrder 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
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag
                nat :: NaturalTransformation
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder a)
  (IsSmallerThan a)
  a
nat = Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder a)
  (IsSmallerThan a)
  a
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder a)
     (IsSmallerThan a)
     a
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder 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
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag (DiscreteCategory oIndex
-> TotalOrder a
-> a
-> Diagram
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder 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
  (TotalOrder 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
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag) TotalOrder a
forall a. TotalOrder a
TotalOrder a
nadirCoproduct) (Map oIndex (IsSmallerThan a)
 -> NaturalTransformation
      (DiscreteCategory oIndex)
      (DiscreteMorphism oIndex)
      oIndex
      (TotalOrder a)
      (IsSmallerThan a)
      a)
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     (DiscreteCategory oIndex)
     (DiscreteMorphism oIndex)
     oIndex
     (TotalOrder 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
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag Diagram
  (DiscreteCategory oIndex)
  (DiscreteMorphism oIndex)
  oIndex
  (TotalOrder 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
  (TotalOrder 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
  (TotalOrder a)
  (IsSmallerThan a)
  a
diag]
                
    instance (Ord a) => HasCoequalizers (TotalOrder a) (IsSmallerThan a) a where
        coequalize :: Diagram
  Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
-> Cocone
     Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
coequalize Diagram
  Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
parallelDiag = a
-> NaturalTransformation
     Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
-> Cocone
     Parallel ParallelAr ParallelOb (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
nat
            where
                nadirCoeq :: a
nadirCoeq = Diagram
  Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
nat = Diagram
  Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
-> Diagram
     Parallel ParallelAr ParallelOb (TotalOrder a) (IsSmallerThan a) a
-> Map ParallelOb (IsSmallerThan a)
-> NaturalTransformation
     Parallel ParallelAr ParallelOb (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
parallelDiag (Parallel
-> TotalOrder a
-> a
-> Diagram
     Parallel ParallelAr ParallelOb (TotalOrder 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
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 (TotalOrder a) (IsSmallerThan a) a
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
parallelDiag Diagram
  Parallel ParallelAr ParallelOb (TotalOrder 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 (Ord a, Eq mIndex, Eq oIndex) => CocompleteCategory (TotalOrder a) (IsSmallerThan a) a (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
-> Cocone cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
colimit Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
diag = a
-> NaturalTransformation
     cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> Cocone cIndex mIndex oIndex (TotalOrder 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 (TotalOrder 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 (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag
                nat :: NaturalTransformation
  cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
nat = Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     cIndex mIndex oIndex (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag (cIndex
-> TotalOrder a
-> a
-> Diagram cIndex mIndex oIndex (TotalOrder 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 (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag) TotalOrder a
forall a. TotalOrder a
TotalOrder a
nadirColimit) (Map oIndex (IsSmallerThan a)
 -> NaturalTransformation
      cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a)
-> Map oIndex (IsSmallerThan a)
-> NaturalTransformation
     cIndex mIndex oIndex (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag Diagram cIndex mIndex oIndex (TotalOrder 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 (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag]
                
        coprojectBase :: Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> Diagram
     (TotalOrder a)
     (IsSmallerThan a)
     a
     (TotalOrder a)
     (IsSmallerThan a)
     a
coprojectBase Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
diag = Diagram{src :: TotalOrder a
src = Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> TotalOrder a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
diag, tgt :: TotalOrder a
tgt = Diagram cIndex mIndex oIndex (TotalOrder a) (IsSmallerThan a) a
-> TotalOrder a
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram cIndex mIndex oIndex (TotalOrder 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 (TotalOrder 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 (TotalOrder 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 (TotalOrder 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 (TotalOrder a) (IsSmallerThan a) a
diag))}