{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}

{-| Module  : FiniteCategories
Description : Typeclasses for 'Category' which are cartesian complete.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Typeclasses for 'Category' which are cartesian complete.

A 'TwoBase' specifies an internal domain and an internal codomain.

A 'Tripod' is the data necessary to specify an exponential object.

An exponential object is a terminal object in the category of candidate exponential objects.
-}

module Math.CartesianClosedCategory
(
    -- * 2-base

    TwoBase(..),
    -- * Tripod

    Tripod,
    -- ** Getters

    twoCone,
    evalMap,
    internalDomainLeg,
    internalCodomainLeg,
    powerObjectLeg,
    internalDomain,
    internalCodomain,
    powerObject,
    universeCategoryTripod,
    -- ** Smart constructors

    tripod,
    unsafeTripod,
    -- * Cartesian closed category

    CartesianClosedCategory(..),
    TwoProduct(..),
    Exponential(..),
    unexproject,
    Cartesian(..),
    -- * Exponential object

    -- ** Candidate exponential object

    isCandidateExponentialObject,
    CandidateExponentialObject(..),
    -- ** Candidate exponential object morphism

    CandidateExponentialObjectMorphism,
    -- *** Getters

    transpose,
    -- *** Smart constructors

    candidateExponentialObjectMorphism,
    unsafeCandidateExponentialObjectMorphism,
    -- ** Candidate exponential object category,

    CandidateExponentialObjectCategory(..),
    -- ** Exponential object function

    exponentialObjects,
)
where
    import              Data.WeakSet             (Set)
    import qualified    Data.WeakSet           as Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap             (Map)
    import qualified    Data.WeakMap           as Map
    import              Data.WeakMap.Safe
    import              Data.List               (intercalate)
    import              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.CompleteCategory
    import              Math.FiniteCategories.DiscreteTwo
    import              Math.FiniteCategories.ConeCategory
    import              Math.FiniteCategories.FunctorCategory
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    -- | A 'TwoBase' is the specification of an internal domain and an internal codomain.

    --

    -- The object 'A' selects the internal domain, the object 'B' selects the internal codomain.

    --

    -- Don't confuse the 2-base of an exponential object with the base of its 2-cone. The 2-base selects the internal domain and internal codomain of the exponential object. The base of the 2-cone selects the power object and the internal domain.

    type TwoBase c m o = Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o
    
    -- | A 'Tripod' is a 2-cone on the power object and the internal domain, and an evaluation map from the apex of the 2-cone to the internal codomain.

    --

    -- 'Tripod' is private, use smart constructor 'tripod' which checks the structure of the 'Tripod' or use 'unsafeTripod' if you know that the 'evalMap' has the apex of the 'twoCone' as a source.

    data Tripod c m o = Tripod {
        forall c m o.
Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone :: (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o), -- ^ In the base of the cone, the power object should be the image of 'A' and the internal domain should be the image of 'B'.

        forall c m o. Tripod c m o -> m
evalMap :: m -- ^ The evaluation map should go from the apex of the 2-cone to the internal codomain

        } deriving (Tripod c m o -> Tripod c m o -> Bool
(Tripod c m o -> Tripod c m o -> Bool)
-> (Tripod c m o -> Tripod c m o -> Bool) -> Eq (Tripod c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq o, Eq c, Eq m) =>
Tripod c m o -> Tripod c m o -> Bool
$c== :: forall c m o.
(Eq o, Eq c, Eq m) =>
Tripod c m o -> Tripod c m o -> Bool
== :: Tripod c m o -> Tripod c m o -> Bool
$c/= :: forall c m o.
(Eq o, Eq c, Eq m) =>
Tripod c m o -> Tripod c m o -> Bool
/= :: Tripod c m o -> Tripod c m o -> Bool
Eq, Int -> Tripod c m o -> ShowS
[Tripod c m o] -> ShowS
Tripod c m o -> String
(Int -> Tripod c m o -> ShowS)
-> (Tripod c m o -> String)
-> ([Tripod c m o] -> ShowS)
-> Show (Tripod c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o.
(Show o, Show c, Show m) =>
Int -> Tripod c m o -> ShowS
forall c m o. (Show o, Show c, Show m) => [Tripod c m o] -> ShowS
forall c m o. (Show o, Show c, Show m) => Tripod c m o -> String
$cshowsPrec :: forall c m o.
(Show o, Show c, Show m) =>
Int -> Tripod c m o -> ShowS
showsPrec :: Int -> Tripod c m o -> ShowS
$cshow :: forall c m o. (Show o, Show c, Show m) => Tripod c m o -> String
show :: Tripod c m o -> String
$cshowList :: forall c m o. (Show o, Show c, Show m) => [Tripod c m o] -> ShowS
showList :: [Tripod c m o] -> ShowS
Show, (forall x. Tripod c m o -> Rep (Tripod c m o) x)
-> (forall x. Rep (Tripod c m o) x -> Tripod c m o)
-> Generic (Tripod c m o)
forall x. Rep (Tripod c m o) x -> Tripod c m o
forall x. Tripod c m o -> Rep (Tripod c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x. Rep (Tripod c m o) x -> Tripod c m o
forall c m o x. Tripod c m o -> Rep (Tripod c m o) x
$cfrom :: forall c m o x. Tripod c m o -> Rep (Tripod c m o) x
from :: forall x. Tripod c m o -> Rep (Tripod c m o) x
$cto :: forall c m o x. Rep (Tripod c m o) x -> Tripod c m o
to :: forall x. Rep (Tripod c m o) x -> Tripod c m o
Generic, Tripod c m o -> Tripod c m o
(Tripod c m o -> Tripod c m o) -> Simplifiable (Tripod c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
(Simplifiable o, Simplifiable c, Simplifiable m) =>
Tripod c m o -> Tripod c m o
$csimplify :: forall c m o.
(Simplifiable o, Simplifiable c, Simplifiable m) =>
Tripod c m o -> Tripod c m o
simplify :: Tripod c m o -> Tripod c m o
Simplifiable, Int -> Int -> String -> Tripod c m o -> String
Int -> Tripod c m o -> String
(Int -> Tripod c m o -> String)
-> (Int -> Int -> String -> Tripod c m o -> String)
-> (Int -> Tripod c m o -> String)
-> PrettyPrint (Tripod c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> Int -> String -> Tripod c m o -> String
forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> Tripod c m o -> String
$cpprint :: forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> Tripod c m o -> String
pprint :: Int -> Tripod c m o -> String
$cpprintWithIndentations :: forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> Int -> String -> Tripod c m o -> String
pprintWithIndentations :: Int -> Int -> String -> Tripod c m o -> String
$cpprintIndent :: forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> Tripod c m o -> String
pprintIndent :: Int -> Tripod c m o -> String
PrettyPrint)
        
    -- | Smart constructor of 'Tripod', checks that the apex of the 'twoCone' is the source of the 'evalMap'.

    tripod :: (Morphism m o, Eq o) => Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o -> m -> Maybe (Tripod c m o)
    tripod :: forall m o c.
(Morphism m o, Eq o) =>
Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> m -> Maybe (Tripod c m o)
tripod Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
cone m
em
        | m -> o
forall m o. Morphism m o => m -> o
source m
em o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o -> o
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
cone = Maybe (Tripod c m o)
forall a. Maybe a
Nothing
        | Bool
otherwise = Tripod c m o -> Maybe (Tripod c m o)
forall a. a -> Maybe a
Just Tripod{twoCone :: Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone = Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
cone, evalMap :: m
evalMap = m
em}
        
    -- | Construct a 'Tripod' without checking the sructure of the 'Tripod', use with caution.

    unsafeTripod :: Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o -> m -> Tripod c m o
    unsafeTripod :: forall c m o.
Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> m -> Tripod c m o
unsafeTripod Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
cone m
em = Tripod{twoCone :: Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone = Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
cone, evalMap :: m
evalMap = m
em}    
    
    -- | Return the internal domain leg of a 'Tripod'.

    internalDomainLeg :: (Morphism m o) => Tripod c m o -> m
    internalDomainLeg :: forall m o c. Morphism m o => Tripod c m o -> m
internalDomainLeg Tripod c m o
t = (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> NaturalTransformation
     DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone (Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c m o.
Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone Tripod c m o
t)) NaturalTransformation DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> DiscreteTwoAr -> m
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ DiscreteTwoAr
B
    
    -- | Return the internal domain of a 'Tripod'.

    internalDomain :: (Morphism m o) => Tripod c m o -> o
    internalDomain :: forall m o c. Morphism m o => Tripod c m o -> o
internalDomain = m -> o
forall m o. Morphism m o => m -> o
target(m -> o) -> (Tripod c m o -> m) -> Tripod c m o -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Tripod c m o -> m
forall m o c. Morphism m o => Tripod c m o -> m
internalDomainLeg
    
    -- | Return the internal codomain leg of a 'Tripod'.

    internalCodomainLeg :: (Morphism m o) => Tripod c m o -> m
    internalCodomainLeg :: forall m o c. Morphism m o => Tripod c m o -> m
internalCodomainLeg Tripod c m o
t = Tripod c m o -> m
forall c m o. Tripod c m o -> m
evalMap Tripod c m o
t
    
    -- | Return the internal codomain of a 'Tripod'.

    internalCodomain :: (Morphism m o) => Tripod c m o -> o
    internalCodomain :: forall m o c. Morphism m o => Tripod c m o -> o
internalCodomain = m -> o
forall m o. Morphism m o => m -> o
target(m -> o) -> (Tripod c m o -> m) -> Tripod c m o -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Tripod c m o -> m
forall m o c. Morphism m o => Tripod c m o -> m
internalCodomainLeg
    
    -- | Return the power object leg of a 'Tripod'.

    powerObjectLeg :: (Morphism m o) => Tripod c m o -> m
    powerObjectLeg :: forall m o c. Morphism m o => Tripod c m o -> m
powerObjectLeg Tripod c m o
t = (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> NaturalTransformation
     DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone (Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c m o.
Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone Tripod c m o
t)) NaturalTransformation DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> DiscreteTwoAr -> m
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ DiscreteTwoAr
A
    
    -- | Return the power object of a 'Tripod'.

    powerObject :: (Morphism m o) => Tripod c m o -> o
    powerObject :: forall m o c. Morphism m o => Tripod c m o -> o
powerObject = m -> o
forall m o. Morphism m o => m -> o
target(m -> o) -> (Tripod c m o -> m) -> Tripod c m o -> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Tripod c m o -> m
forall m o c. Morphism m o => Tripod c m o -> m
powerObjectLeg
    
    -- | Return the category in which a 'Tripod' lives.

    universeCategoryTripod :: (Category c m o, Morphism m o, Eq c, Eq m, Eq o) => 
        Tripod c m o -> c
    universeCategoryTripod :: forall c m o.
(Category c m o, Morphism m o, Eq c, Eq m, Eq o) =>
Tripod c m o -> c
universeCategoryTripod = Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o -> c
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Cone c1 m1 o1 c2 m2 o2 -> c2
universeCategoryCone(Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o -> c)
-> (Tripod c m o
    -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
-> Tripod c m o
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c m o.
Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone
    
    -- | For a 'Category' parametrized over a type t, the power object of an exponential object of a 2-base will contain 'ExponentialElement' constructions (an exponential element is a mapping). A given mapping has as domain and codomain values 'Exprojection's.

    --

    -- For example, in 'FinSet', let's consider the 2-base selecting {1,2} and {3,4} as internal domain and codomain. The power object of the 2-base is {{1->3,2->3},{1->3,2->4},{1->4,2->3},{1->4,2->4}}, note that it is not an object of ('Finset' Int) but an object of ('FinSet' (Set (Map Int))). The 'Exponential' type allows to construct type ('FinSet' ('Exponential' Int)) in which we can consider the original objects with 'Exprojection' and the new mappings with 'ExponentialElement'. Here, instead of mappings, we can construct the type ('FinSet' (Set (Exponential Int))), a mapping is then ('ExponentialElement' (weakMap [(1,3),(2,3)])). We can construct exprojections in the same category, for example along 'A' which will map ('ExponentialElement' (weakMap [(1,3),(2,3)])) to (set ['Exprojection' 1, 'Exprojection' 2]).

    data Exponential t = Exprojection t -- ^A 'ExponentialElement' can be applied to an 'Exprojection' yielding another 'Exprojection'.  

                       | ExponentialElement (Map t t) -- ^ An 'ExponentialElement' is an element in an exponential object, it is a mapping between objects of type t.

        deriving (Exponential t -> Exponential t -> Bool
(Exponential t -> Exponential t -> Bool)
-> (Exponential t -> Exponential t -> Bool) -> Eq (Exponential t)
forall t. Eq t => Exponential t -> Exponential t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall t. Eq t => Exponential t -> Exponential t -> Bool
== :: Exponential t -> Exponential t -> Bool
$c/= :: forall t. Eq t => Exponential t -> Exponential t -> Bool
/= :: Exponential t -> Exponential t -> Bool
Eq, Int -> Exponential t -> ShowS
[Exponential t] -> ShowS
Exponential t -> String
(Int -> Exponential t -> ShowS)
-> (Exponential t -> String)
-> ([Exponential t] -> ShowS)
-> Show (Exponential t)
forall t. Show t => Int -> Exponential t -> ShowS
forall t. Show t => [Exponential t] -> ShowS
forall t. Show t => Exponential t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Exponential t -> ShowS
showsPrec :: Int -> Exponential t -> ShowS
$cshow :: forall t. Show t => Exponential t -> String
show :: Exponential t -> String
$cshowList :: forall t. Show t => [Exponential t] -> ShowS
showList :: [Exponential t] -> ShowS
Show, (forall x. Exponential t -> Rep (Exponential t) x)
-> (forall x. Rep (Exponential t) x -> Exponential t)
-> Generic (Exponential t)
forall x. Rep (Exponential t) x -> Exponential t
forall x. Exponential t -> Rep (Exponential t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (Exponential t) x -> Exponential t
forall t x. Exponential t -> Rep (Exponential t) x
$cfrom :: forall t x. Exponential t -> Rep (Exponential t) x
from :: forall x. Exponential t -> Rep (Exponential t) x
$cto :: forall t x. Rep (Exponential t) x -> Exponential t
to :: forall x. Rep (Exponential t) x -> Exponential t
Generic, Exponential t -> Exponential t
(Exponential t -> Exponential t) -> Simplifiable (Exponential t)
forall t. (Simplifiable t, Eq t) => Exponential t -> Exponential t
forall a. (a -> a) -> Simplifiable a
$csimplify :: forall t. (Simplifiable t, Eq t) => Exponential t -> Exponential t
simplify :: Exponential t -> Exponential t
Simplifiable, Int -> Int -> String -> Exponential t -> String
Int -> Exponential t -> String
(Int -> Exponential t -> String)
-> (Int -> Int -> String -> Exponential t -> String)
-> (Int -> Exponential t -> String)
-> PrettyPrint (Exponential t)
forall t.
(PrettyPrint t, Eq t) =>
Int -> Int -> String -> Exponential t -> String
forall t. (PrettyPrint t, Eq t) => Int -> Exponential t -> String
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
$cpprint :: forall t. (PrettyPrint t, Eq t) => Int -> Exponential t -> String
pprint :: Int -> Exponential t -> String
$cpprintWithIndentations :: forall t.
(PrettyPrint t, Eq t) =>
Int -> Int -> String -> Exponential t -> String
pprintWithIndentations :: Int -> Int -> String -> Exponential t -> String
$cpprintIndent :: forall t. (PrettyPrint t, Eq t) => Int -> Exponential t -> String
pprintIndent :: Int -> Exponential t -> String
PrettyPrint)
        
    -- | Remove the constructor 'Exprojection' from an original object t, throws an error if an 'ExponentialElement' is given.

    unexproject :: Exponential t -> t
    unexproject :: forall t. Exponential t -> t
unexproject (Exprojection t
t) = t
t
    unexproject (ExponentialElement Map t t
_) = String -> t
forall a. HasCallStack => String -> a
error String
"Unexproject an exponential element."
        
    -- | For a category to be cartesian closed, we need to construct 2-products.

    type TwoProduct t = Limit DiscreteTwoOb t
    
    -- | For a category to be cartesian closed, we need to construct 2-products of exponential objects with exprojected objects.

    type Cartesian t = TwoProduct (Exponential t)
    
    
    class CartesianClosedCategory c m o cLim mLim oLim cLimExp mLimExp oLimExp | 
        c -> m, m -> o, cLim -> mLim, mLim -> oLim, cLimExp -> mLimExp, mLimExp -> oLimExp, c m o -> cLimExp where
        
        internalHom :: (CompleteCategory c m o cLim mLim oLim DiscreteTwo DiscreteTwoAr DiscreteTwoOb) => TwoBase c m o -> Tripod cLimExp mLimExp oLimExp

    -- | Return wether a 'Tripod' is a candidate exponential object or not. A 'Tripod' is a candidate exponential object if its 'twoCone' is a limit. Tests if the 2-cone is a 2-product by computing the limits in the universe category with the function 'limits' : it is slow.

    isCandidateExponentialObject :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Tripod c m o -> Bool
    isCandidateExponentialObject :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
Tripod c m o -> Bool
isCandidateExponentialObject Tripod c m o
t = (Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c m o.
Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone Tripod c m o
t) Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> Set (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o) -> Bool
forall a. Eq a => a -> Set a -> Bool
`Set.elem` (Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> Set (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
limits(Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
 -> Set (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o))
-> (Tripod c m o
    -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
-> Tripod c m o
-> Set (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c1 m1 o1 m2 o2 c2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Morphism m2 o2) =>
Cone c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
baseCone(Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
 -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
-> (Tripod c m o
    -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
-> Tripod c m o
-> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c m o.
Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone (Tripod c m o
 -> Set (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o))
-> Tripod c m o
-> Set (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
forall a b. (a -> b) -> a -> b
$ Tripod c m o
t)
    
    -- | A 'CandidateExponentialObject' is a 'Tripod' such that its 'twoCone' is a limit.

    type CandidateExponentialObject c m o = Tripod c m o
    
    -- | A 'CandidateExponentialObjectMorphism' is a morphism between two 'CandidateExponentialObject's. It is private, use smart constructors 'candidateExponentialObjectMorphism' and 'unsafeCandidateExponentialObjectMorphism' to instantiate.

    data CandidateExponentialObjectMorphism c m o = CandidateExponentialObjectMorphism {
                                                        forall c m o.
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
sourceCandidateExponentialObject :: CandidateExponentialObject c m o,
                                                        forall c m o.
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
targetCandidateExponentialObject :: CandidateExponentialObject c m o,
                                                        forall c m o. CandidateExponentialObjectMorphism c m o -> m
transpose :: m
                                                    }
                                                    deriving (CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o -> Bool
(CandidateExponentialObjectMorphism c m o
 -> CandidateExponentialObjectMorphism c m o -> Bool)
-> (CandidateExponentialObjectMorphism c m o
    -> CandidateExponentialObjectMorphism c m o -> Bool)
-> Eq (CandidateExponentialObjectMorphism c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq o, Eq c, Eq m) =>
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o -> Bool
$c== :: forall c m o.
(Eq o, Eq c, Eq m) =>
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o -> Bool
== :: CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o -> Bool
$c/= :: forall c m o.
(Eq o, Eq c, Eq m) =>
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o -> Bool
/= :: CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o -> Bool
Eq, Int -> CandidateExponentialObjectMorphism c m o -> ShowS
[CandidateExponentialObjectMorphism c m o] -> ShowS
CandidateExponentialObjectMorphism c m o -> String
(Int -> CandidateExponentialObjectMorphism c m o -> ShowS)
-> (CandidateExponentialObjectMorphism c m o -> String)
-> ([CandidateExponentialObjectMorphism c m o] -> ShowS)
-> Show (CandidateExponentialObjectMorphism c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o.
(Show o, Show c, Show m) =>
Int -> CandidateExponentialObjectMorphism c m o -> ShowS
forall c m o.
(Show o, Show c, Show m) =>
[CandidateExponentialObjectMorphism c m o] -> ShowS
forall c m o.
(Show o, Show c, Show m) =>
CandidateExponentialObjectMorphism c m o -> String
$cshowsPrec :: forall c m o.
(Show o, Show c, Show m) =>
Int -> CandidateExponentialObjectMorphism c m o -> ShowS
showsPrec :: Int -> CandidateExponentialObjectMorphism c m o -> ShowS
$cshow :: forall c m o.
(Show o, Show c, Show m) =>
CandidateExponentialObjectMorphism c m o -> String
show :: CandidateExponentialObjectMorphism c m o -> String
$cshowList :: forall c m o.
(Show o, Show c, Show m) =>
[CandidateExponentialObjectMorphism c m o] -> ShowS
showList :: [CandidateExponentialObjectMorphism c m o] -> ShowS
Show, (forall x.
 CandidateExponentialObjectMorphism c m o
 -> Rep (CandidateExponentialObjectMorphism c m o) x)
-> (forall x.
    Rep (CandidateExponentialObjectMorphism c m o) x
    -> CandidateExponentialObjectMorphism c m o)
-> Generic (CandidateExponentialObjectMorphism c m o)
forall x.
Rep (CandidateExponentialObjectMorphism c m o) x
-> CandidateExponentialObjectMorphism c m o
forall x.
CandidateExponentialObjectMorphism c m o
-> Rep (CandidateExponentialObjectMorphism c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x.
Rep (CandidateExponentialObjectMorphism c m o) x
-> CandidateExponentialObjectMorphism c m o
forall c m o x.
CandidateExponentialObjectMorphism c m o
-> Rep (CandidateExponentialObjectMorphism c m o) x
$cfrom :: forall c m o x.
CandidateExponentialObjectMorphism c m o
-> Rep (CandidateExponentialObjectMorphism c m o) x
from :: forall x.
CandidateExponentialObjectMorphism c m o
-> Rep (CandidateExponentialObjectMorphism c m o) x
$cto :: forall c m o x.
Rep (CandidateExponentialObjectMorphism c m o) x
-> CandidateExponentialObjectMorphism c m o
to :: forall x.
Rep (CandidateExponentialObjectMorphism c m o) x
-> CandidateExponentialObjectMorphism c m o
Generic, CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o
(CandidateExponentialObjectMorphism c m o
 -> CandidateExponentialObjectMorphism c m o)
-> Simplifiable (CandidateExponentialObjectMorphism c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
(Simplifiable o, Simplifiable c, Simplifiable m) =>
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o
$csimplify :: forall c m o.
(Simplifiable o, Simplifiable c, Simplifiable m) =>
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o
simplify :: CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o
Simplifiable, Int
-> Int
-> String
-> CandidateExponentialObjectMorphism c m o
-> String
Int -> CandidateExponentialObjectMorphism c m o -> String
(Int -> CandidateExponentialObjectMorphism c m o -> String)
-> (Int
    -> Int
    -> String
    -> CandidateExponentialObjectMorphism c m o
    -> String)
-> (Int -> CandidateExponentialObjectMorphism c m o -> String)
-> PrettyPrint (CandidateExponentialObjectMorphism c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int
-> Int
-> String
-> CandidateExponentialObjectMorphism c m o
-> String
forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> CandidateExponentialObjectMorphism c m o -> String
$cpprint :: forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> CandidateExponentialObjectMorphism c m o -> String
pprint :: Int -> CandidateExponentialObjectMorphism c m o -> String
$cpprintWithIndentations :: forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int
-> Int
-> String
-> CandidateExponentialObjectMorphism c m o
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> CandidateExponentialObjectMorphism c m o
-> String
$cpprintIndent :: forall c m o.
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) =>
Int -> CandidateExponentialObjectMorphism c m o -> String
pprintIndent :: Int -> CandidateExponentialObjectMorphism c m o -> String
PrettyPrint)
    
    
    -- | Smart constructor for 'CandidateExponentialObjectMorphism'. Checks wether the transpose has valid domain and valid codomain.

    candidateExponentialObjectMorphism :: (Morphism m o, Eq m, Eq o) => CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> m -> Maybe (CandidateExponentialObjectMorphism c m o)
    candidateExponentialObjectMorphism :: forall m o c.
(Morphism m o, Eq m, Eq o) =>
CandidateExponentialObject c m o
-> CandidateExponentialObject c m o
-> m
-> Maybe (CandidateExponentialObjectMorphism c m o)
candidateExponentialObjectMorphism CandidateExponentialObject c m o
s CandidateExponentialObject c m o
t m
transp
        | m -> o
forall m o. Morphism m o => m -> o
source m
transp o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== m -> o
forall m o. Morphism m o => m -> o
target ((Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> NaturalTransformation
     DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
 -> NaturalTransformation
      DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
-> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> NaturalTransformation
     DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall a b. (a -> b) -> a -> b
$ CandidateExponentialObject c m o
-> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c m o.
Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone CandidateExponentialObject c m o
s) NaturalTransformation DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> DiscreteTwoAr -> m
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ DiscreteTwoAr
A) Bool -> Bool -> Bool
&& m -> o
forall m o. Morphism m o => m -> o
target m
transp o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== m -> o
forall m o. Morphism m o => m -> o
target ((Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> NaturalTransformation
     DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c1 m1 o1 c2 m2 o2.
Cone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCone (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
 -> NaturalTransformation
      DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
-> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> NaturalTransformation
     DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall a b. (a -> b) -> a -> b
$ CandidateExponentialObject c m o
-> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
forall c m o.
Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone CandidateExponentialObject c m o
t) NaturalTransformation DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
-> DiscreteTwoAr -> m
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ DiscreteTwoAr
A) = CandidateExponentialObjectMorphism c m o
-> Maybe (CandidateExponentialObjectMorphism c m o)
forall a. a -> Maybe a
Just CandidateExponentialObjectMorphism {sourceCandidateExponentialObject :: CandidateExponentialObject c m o
sourceCandidateExponentialObject = CandidateExponentialObject c m o
s, targetCandidateExponentialObject :: CandidateExponentialObject c m o
targetCandidateExponentialObject = CandidateExponentialObject c m o
t, transpose :: m
transpose = m
transp}
        | Bool
otherwise = Maybe (CandidateExponentialObjectMorphism c m o)
forall a. Maybe a
Nothing
        
    -- | Unsafe version of 'candidateExponentialObjectMorphism', use with caution as it does not check wether the transpose has valid domain and valid codomain.

    unsafeCandidateExponentialObjectMorphism :: CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> m -> CandidateExponentialObjectMorphism c m o
    unsafeCandidateExponentialObjectMorphism :: forall c m o.
CandidateExponentialObject c m o
-> CandidateExponentialObject c m o
-> m
-> CandidateExponentialObjectMorphism c m o
unsafeCandidateExponentialObjectMorphism CandidateExponentialObject c m o
s CandidateExponentialObject c m o
t m
transp = CandidateExponentialObjectMorphism {sourceCandidateExponentialObject :: CandidateExponentialObject c m o
sourceCandidateExponentialObject = CandidateExponentialObject c m o
s, targetCandidateExponentialObject :: CandidateExponentialObject c m o
targetCandidateExponentialObject = CandidateExponentialObject c m o
t, transpose :: m
transpose = m
transp}
    
    instance (Morphism m o) => Morphism (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o) where
        source :: CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
source = CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
forall c m o.
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
sourceCandidateExponentialObject
        target :: CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
target = CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
forall c m o.
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
targetCandidateExponentialObject
        CandidateExponentialObjectMorphism c m o
ceom2 @ :: CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObjectMorphism c m o
@ CandidateExponentialObjectMorphism c m o
ceom1 = CandidateExponentialObjectMorphism {sourceCandidateExponentialObject :: CandidateExponentialObject c m o
sourceCandidateExponentialObject = CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
forall c m o.
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
sourceCandidateExponentialObject CandidateExponentialObjectMorphism c m o
ceom1, targetCandidateExponentialObject :: CandidateExponentialObject c m o
targetCandidateExponentialObject = CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
forall c m o.
CandidateExponentialObjectMorphism c m o
-> CandidateExponentialObject c m o
targetCandidateExponentialObject CandidateExponentialObjectMorphism c m o
ceom2, transpose :: m
transpose = (CandidateExponentialObjectMorphism c m o -> m
forall c m o. CandidateExponentialObjectMorphism c m o -> m
transpose CandidateExponentialObjectMorphism c m o
ceom2) m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (CandidateExponentialObjectMorphism c m o -> m
forall c m o. CandidateExponentialObjectMorphism c m o -> m
transpose CandidateExponentialObjectMorphism c m o
ceom1)}
    
    data CandidateExponentialObjectCategory c m o = CandidateExponentialObjectCategory (TwoBase c m o)
        deriving (CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o -> Bool
(CandidateExponentialObjectCategory c m o
 -> CandidateExponentialObjectCategory c m o -> Bool)
-> (CandidateExponentialObjectCategory c m o
    -> CandidateExponentialObjectCategory c m o -> Bool)
-> Eq (CandidateExponentialObjectCategory c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq c, Eq m, Eq o) =>
CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o -> Bool
$c== :: forall c m o.
(Eq c, Eq m, Eq o) =>
CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o -> Bool
== :: CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o -> Bool
$c/= :: forall c m o.
(Eq c, Eq m, Eq o) =>
CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o -> Bool
/= :: CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o -> Bool
Eq, Int -> CandidateExponentialObjectCategory c m o -> ShowS
[CandidateExponentialObjectCategory c m o] -> ShowS
CandidateExponentialObjectCategory c m o -> String
(Int -> CandidateExponentialObjectCategory c m o -> ShowS)
-> (CandidateExponentialObjectCategory c m o -> String)
-> ([CandidateExponentialObjectCategory c m o] -> ShowS)
-> Show (CandidateExponentialObjectCategory c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o.
(Show c, Show o, Show m) =>
Int -> CandidateExponentialObjectCategory c m o -> ShowS
forall c m o.
(Show c, Show o, Show m) =>
[CandidateExponentialObjectCategory c m o] -> ShowS
forall c m o.
(Show c, Show o, Show m) =>
CandidateExponentialObjectCategory c m o -> String
$cshowsPrec :: forall c m o.
(Show c, Show o, Show m) =>
Int -> CandidateExponentialObjectCategory c m o -> ShowS
showsPrec :: Int -> CandidateExponentialObjectCategory c m o -> ShowS
$cshow :: forall c m o.
(Show c, Show o, Show m) =>
CandidateExponentialObjectCategory c m o -> String
show :: CandidateExponentialObjectCategory c m o -> String
$cshowList :: forall c m o.
(Show c, Show o, Show m) =>
[CandidateExponentialObjectCategory c m o] -> ShowS
showList :: [CandidateExponentialObjectCategory c m o] -> ShowS
Show, (forall x.
 CandidateExponentialObjectCategory c m o
 -> Rep (CandidateExponentialObjectCategory c m o) x)
-> (forall x.
    Rep (CandidateExponentialObjectCategory c m o) x
    -> CandidateExponentialObjectCategory c m o)
-> Generic (CandidateExponentialObjectCategory c m o)
forall x.
Rep (CandidateExponentialObjectCategory c m o) x
-> CandidateExponentialObjectCategory c m o
forall x.
CandidateExponentialObjectCategory c m o
-> Rep (CandidateExponentialObjectCategory c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x.
Rep (CandidateExponentialObjectCategory c m o) x
-> CandidateExponentialObjectCategory c m o
forall c m o x.
CandidateExponentialObjectCategory c m o
-> Rep (CandidateExponentialObjectCategory c m o) x
$cfrom :: forall c m o x.
CandidateExponentialObjectCategory c m o
-> Rep (CandidateExponentialObjectCategory c m o) x
from :: forall x.
CandidateExponentialObjectCategory c m o
-> Rep (CandidateExponentialObjectCategory c m o) x
$cto :: forall c m o x.
Rep (CandidateExponentialObjectCategory c m o) x
-> CandidateExponentialObjectCategory c m o
to :: forall x.
Rep (CandidateExponentialObjectCategory c m o) x
-> CandidateExponentialObjectCategory c m o
Generic, CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o
(CandidateExponentialObjectCategory c m o
 -> CandidateExponentialObjectCategory c m o)
-> Simplifiable (CandidateExponentialObjectCategory c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
(Simplifiable c, Simplifiable o, Simplifiable m) =>
CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o
$csimplify :: forall c m o.
(Simplifiable c, Simplifiable o, Simplifiable m) =>
CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o
simplify :: CandidateExponentialObjectCategory c m o
-> CandidateExponentialObjectCategory c m o
Simplifiable, Int
-> Int
-> String
-> CandidateExponentialObjectCategory c m o
-> String
Int -> CandidateExponentialObjectCategory c m o -> String
(Int -> CandidateExponentialObjectCategory c m o -> String)
-> (Int
    -> Int
    -> String
    -> CandidateExponentialObjectCategory c m o
    -> String)
-> (Int -> CandidateExponentialObjectCategory c m o -> String)
-> PrettyPrint (CandidateExponentialObjectCategory c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int
-> Int
-> String
-> CandidateExponentialObjectCategory c m o
-> String
forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> CandidateExponentialObjectCategory c m o -> String
$cpprint :: forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> CandidateExponentialObjectCategory c m o -> String
pprint :: Int -> CandidateExponentialObjectCategory c m o -> String
$cpprintWithIndentations :: forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int
-> Int
-> String
-> CandidateExponentialObjectCategory c m o
-> String
pprintWithIndentations :: Int
-> Int
-> String
-> CandidateExponentialObjectCategory c m o
-> String
$cpprintIndent :: forall c m o.
(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) =>
Int -> CandidateExponentialObjectCategory c m o -> String
pprintIndent :: Int -> CandidateExponentialObjectCategory c m o -> String
PrettyPrint)
        
    instance (Category c m o, Morphism m o, Eq c, Eq m ,Eq o) => Category (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o) where
        
        identity :: Morphism
  (CandidateExponentialObjectMorphism c m o)
  (CandidateExponentialObject c m o) =>
CandidateExponentialObjectCategory c m o
-> CandidateExponentialObject c m o
-> CandidateExponentialObjectMorphism c m o
identity (CandidateExponentialObjectCategory TwoBase c m o
base) CandidateExponentialObject c m o
tripod
            | Bool
differentInternalDomain = String -> CandidateExponentialObjectMorphism c m o
forall a. HasCallStack => String -> a
error String
"identity in a CandidateExponentialObjectCategory of a tripod with a different internal domain."
            | Bool
differentInternalCodomain = String -> CandidateExponentialObjectMorphism c m o
forall a. HasCallStack => String -> a
error String
"identity in a CandidateExponentialObjectCategory of a tripod with a different internal codomain."
            | Bool
differentUniverseCategory = String -> CandidateExponentialObjectMorphism c m o
forall a. HasCallStack => String -> a
error String
"identity in a CandidateExponentialObjectCategory of a tripod with a different universe category."
            | Bool
otherwise = CandidateExponentialObjectMorphism {sourceCandidateExponentialObject :: CandidateExponentialObject c m o
sourceCandidateExponentialObject = CandidateExponentialObject c m o
tripod, targetCandidateExponentialObject :: CandidateExponentialObject c m o
targetCandidateExponentialObject = CandidateExponentialObject c m o
tripod, transpose :: m
transpose = c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (CandidateExponentialObject c m o -> c
forall c m o.
(Category c m o, Morphism m o, Eq c, Eq m, Eq o) =>
Tripod c m o -> c
universeCategoryTripod CandidateExponentialObject c m o
tripod) (CandidateExponentialObject c m o -> o
forall m o c. Morphism m o => Tripod c m o -> o
powerObject CandidateExponentialObject c m o
tripod)}
            where
                differentInternalDomain :: Bool
differentInternalDomain = CandidateExponentialObject c m o -> o
forall m o c. Morphism m o => Tripod c m o -> o
internalDomain CandidateExponentialObject c m o
tripod o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= TwoBase c m o
base TwoBase c m o -> DiscreteTwoAr -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A
                differentInternalCodomain :: Bool
differentInternalCodomain = CandidateExponentialObject c m o -> o
forall m o c. Morphism m o => Tripod c m o -> o
internalCodomain CandidateExponentialObject c m o
tripod o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= TwoBase c m o
base TwoBase c m o -> DiscreteTwoAr -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
B
                differentUniverseCategory :: Bool
differentUniverseCategory = CandidateExponentialObject c m o -> c
forall c m o.
(Category c m o, Morphism m o, Eq c, Eq m, Eq o) =>
Tripod c m o -> c
universeCategoryTripod CandidateExponentialObject c m o
tripod c -> c -> Bool
forall a. Eq a => a -> a -> Bool
/= TwoBase c m o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt TwoBase c m o
base
            
        
        ar :: Morphism
  (CandidateExponentialObjectMorphism c m o)
  (CandidateExponentialObject c m o) =>
CandidateExponentialObjectCategory c m o
-> CandidateExponentialObject c m o
-> CandidateExponentialObject c m o
-> Set (CandidateExponentialObjectMorphism c m o)
ar (CandidateExponentialObjectCategory TwoBase c m o
base) CandidateExponentialObject c m o
tripod1 CandidateExponentialObject c m o
tripod2
            | Bool
differentInternalDomain1 = String -> Set (CandidateExponentialObjectMorphism c m o)
forall a. HasCallStack => String -> a
error String
"ar in a CandidateExponentialObjectCategory where the source has different internal domain."
            | Bool
differentInternalCodomain1 = String -> Set (CandidateExponentialObjectMorphism c m o)
forall a. HasCallStack => String -> a
error String
"ar in a CandidateExponentialObjectCategory where the source has different internal codomain."
            | Bool
differentUniverseCategory1 = String -> Set (CandidateExponentialObjectMorphism c m o)
forall a. HasCallStack => String -> a
error String
"ar in a CandidateExponentialObjectCategory where the source has different universe Category."
            | Bool
differentInternalDomain2 = String -> Set (CandidateExponentialObjectMorphism c m o)
forall a. HasCallStack => String -> a
error String
"ar in a CandidateExponentialObjectCategory where the target has different internal domain."
            | Bool
differentInternalCodomain2 = String -> Set (CandidateExponentialObjectMorphism c m o)
forall a. HasCallStack => String -> a
error String
"ar in a CandidateExponentialObjectCategory where the target has different internal codomain."
            | Bool
differentUniverseCategory2 = String -> Set (CandidateExponentialObjectMorphism c m o)
forall a. HasCallStack => String -> a
error String
"ar in a CandidateExponentialObjectCategory where the target has different universe Category."
            | Bool
otherwise = (\m
m -> CandidateExponentialObjectMorphism{sourceCandidateExponentialObject :: CandidateExponentialObject c m o
sourceCandidateExponentialObject = CandidateExponentialObject c m o
tripod1, targetCandidateExponentialObject :: CandidateExponentialObject c m o
targetCandidateExponentialObject = CandidateExponentialObject c m o
tripod2, transpose :: m
transpose = m
m}) (m -> CandidateExponentialObjectMorphism c m o)
-> Set m -> Set (CandidateExponentialObjectMorphism c m o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (CandidateExponentialObject c m o -> c
forall c m o.
(Category c m o, Morphism m o, Eq c, Eq m, Eq o) =>
Tripod c m o -> c
universeCategoryTripod CandidateExponentialObject c m o
tripod1) (CandidateExponentialObject c m o -> o
forall m o c. Morphism m o => Tripod c m o -> o
powerObject CandidateExponentialObject c m o
tripod1) (CandidateExponentialObject c m o -> o
forall m o c. Morphism m o => Tripod c m o -> o
powerObject CandidateExponentialObject c m o
tripod2)
            where
                differentInternalDomain1 :: Bool
differentInternalDomain1 = CandidateExponentialObject c m o -> o
forall m o c. Morphism m o => Tripod c m o -> o
internalDomain CandidateExponentialObject c m o
tripod1 o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= TwoBase c m o
base TwoBase c m o -> DiscreteTwoAr -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A
                differentInternalCodomain1 :: Bool
differentInternalCodomain1 = CandidateExponentialObject c m o -> o
forall m o c. Morphism m o => Tripod c m o -> o
internalCodomain CandidateExponentialObject c m o
tripod1 o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= TwoBase c m o
base TwoBase c m o -> DiscreteTwoAr -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
B
                differentUniverseCategory1 :: Bool
differentUniverseCategory1 = CandidateExponentialObject c m o -> c
forall c m o.
(Category c m o, Morphism m o, Eq c, Eq m, Eq o) =>
Tripod c m o -> c
universeCategoryTripod CandidateExponentialObject c m o
tripod1 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
/= TwoBase c m o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt TwoBase c m o
base
                differentInternalDomain2 :: Bool
differentInternalDomain2 = CandidateExponentialObject c m o -> o
forall m o c. Morphism m o => Tripod c m o -> o
internalDomain CandidateExponentialObject c m o
tripod2 o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= TwoBase c m o
base TwoBase c m o -> DiscreteTwoAr -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A
                differentInternalCodomain2 :: Bool
differentInternalCodomain2 = CandidateExponentialObject c m o -> o
forall m o c. Morphism m o => Tripod c m o -> o
internalCodomain CandidateExponentialObject c m o
tripod2 o -> o -> Bool
forall a. Eq a => a -> a -> Bool
/= TwoBase c m o
base TwoBase c m o -> DiscreteTwoAr -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
B
                differentUniverseCategory2 :: Bool
differentUniverseCategory2 = CandidateExponentialObject c m o -> c
forall c m o.
(Category c m o, Morphism m o, Eq c, Eq m, Eq o) =>
Tripod c m o -> c
universeCategoryTripod CandidateExponentialObject c m o
tripod2 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
/= TwoBase c m o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt TwoBase c m o
base
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m ,Eq o) => FiniteCategory (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o) where
        
        ob :: CandidateExponentialObjectCategory c m o
-> Set (CandidateExponentialObject c m o)
ob (CandidateExponentialObjectCategory TwoBase c m o
base) = [Tripod{twoCone :: Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone = Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
c, evalMap :: m
evalMap = m
m} | o
powerObj <- c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob (TwoBase c m o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt TwoBase c m o
base), Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
c <- TwoBase c m o
-> Set (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Set (Cone c1 m1 o1 c2 m2 o2)
limits (c -> o -> o -> TwoBase c m o
forall c m o.
(Category c m o, Morphism m o) =>
c
-> o -> o -> Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoDiagram (TwoBase c m o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt TwoBase c m o
base) o
powerObj (TwoBase c m o
base TwoBase c m o -> DiscreteTwoAr -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
A)), m
m <- c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (TwoBase c m o -> c
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt TwoBase c m o
base) (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o -> o
forall c1 m1 o1 c2 m2 o2. Cone c1 m1 o1 c2 m2 o2 -> o2
apex Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
c) (TwoBase c m o
base TwoBase c m o -> DiscreteTwoAr -> o
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ DiscreteTwoAr
B), CandidateExponentialObject c m o -> Bool
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
Tripod c m o -> Bool
isCandidateExponentialObject Tripod{twoCone :: Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
twoCone = Cone DiscreteTwo DiscreteTwoAr DiscreteTwoAr c m o
c, evalMap :: m
evalMap = m
m}]
        
    -- | Return the exponential objects of a given 2-base.

    exponentialObjects :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m ,Eq o) => TwoBase c m o -> Set (CandidateExponentialObject c m o)
    exponentialObjects :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) =>
TwoBase c m o -> Set (CandidateExponentialObject c m o)
exponentialObjects TwoBase c m o
base = CandidateExponentialObjectCategory c m o
-> Set (CandidateExponentialObject c m o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
terminalObjects (TwoBase c m o -> CandidateExponentialObjectCategory c m o
forall c m o.
TwoBase c m o -> CandidateExponentialObjectCategory c m o
CandidateExponentialObjectCategory TwoBase c m o
base)