{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}
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
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
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
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))}