proarrow

Safe Haskell	None
Language	GHC2024

Proarrow.Category.Topos

Synopsis

class (HasProducts k, Ob (Omega :: k)) => HasSubobjectClassifier k where
- type Omega :: k
- true :: (TerminalObject :: k) ~> (Omega :: k)
- classifyGraph :: forall (a :: k) (b :: k). (a ~> b) -> (a && b) ~> (Omega :: k)
isEq :: forall {k} (a :: k). (HasSubobjectClassifier k, Ob a) => (a && a) ~> (Omega :: k)
classifyImage :: forall {k} (a :: k) (b :: k). (HasSubobjectClassifier k, HasPushouts k) => (a ~> b) -> b ~> (Omega :: k)
classifyKernelPair :: forall {k} (a :: k) (b :: k). HasSubobjectClassifier k => (a ~> b) -> (a && a) ~> (Omega :: k)
class CategoryOf k => HasEpiMonoFactorization k where
- factorize :: forall (a :: k) (b :: k). (a ~> b) -> (Hom k :.: Hom k) a b
defaultFactorize :: forall k (a :: k) (b :: k). (HasPushouts k, HasEqualizers k) => (a ~> b) -> (Hom k :.: Hom k) a b
defaultFactorizeDual :: forall k (a :: k) (b :: k). (HasPullbacks k, HasCoequalizers k) => (a ~> b) -> (Hom k :.: Hom k) a b
type HasFiniteLimits k = (HasProducts k, HasPullbacks k, HasEqualizers k)
type HasFiniteColimits k = (HasCoproducts k, HasPushouts k, HasCoequalizers k)
class (HasFiniteLimits k, HasFiniteColimits k, CCC k, HasSubobjectClassifier k, HasEpiMonoFactorization k) => ElementaryTopos k
false :: ElementaryTopos k => (TerminalObject :: k) ~> (Omega :: k)
and :: ElementaryTopos k => ((Omega :: k) && (Omega :: k)) ~> (Omega :: k)
or :: ElementaryTopos k => ((Omega :: k) && (Omega :: k)) ~> (Omega :: k)
implies :: ElementaryTopos k => ((Omega :: k) && (Omega :: k)) ~> (Omega :: k)

Documentation

class (HasProducts k, Ob (Omega :: k)) => HasSubobjectClassifier k where Source Github #

Minimal complete definition

Associated Types

type Omega :: k Source Github #

Methods

true :: (TerminalObject :: k) ~> (Omega :: k) Source Github #

default true :: (HasProducts k, HasPushouts k) => (TerminalObject :: k) ~> (Omega :: k) Source Github #

classifyGraph :: forall (a :: k) (b :: k). (a ~> b) -> (a && b) ~> (Omega :: k) Source Github #

Classify the graph (id *** f :: a ~> a && b) of a morphism f. This is a minimal primitive that works for any morphism.

Instances

Instances details

HasSubobjectClassifier FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type Omega
Instance details Defined in Proarrow.Category.Instance.FinSet type Omega = 'FS Nat2

Methods

true :: (TerminalObject :: FINSET) ~> (Omega :: FINSET) Source Github #

classifyGraph :: forall (a :: FINSET) (b :: FINSET). (a ~> b) -> (a && b) ~> (Omega :: FINSET) Source Github #

isEq :: forall {k} (a :: k). (HasSubobjectClassifier k, Ob a) => (a && a) ~> (Omega :: k) Source Github #

classifyImage :: forall {k} (a :: k) (b :: k). (HasSubobjectClassifier k, HasPushouts k) => (a ~> b) -> b ~> (Omega :: k) Source Github #

classify f classifies the image of f. If f is mono, then this returns its characteristic map.

classifyKernelPair :: forall {k} (a :: k) (b :: k). HasSubobjectClassifier k => (a ~> b) -> (a && a) ~> (Omega :: k) Source Github #

class CategoryOf k => HasEpiMonoFactorization k where Source Github #

Methods

factorize :: forall (a :: k) (b :: k). (a ~> b) -> (Hom k :.: Hom k) a b Source Github #

Instances

Instances details

HasEpiMonoFactorization FINSET Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods factorize :: forall (a :: FINSET) (b :: FINSET). (a ~> b) -> (Hom FINSET :.: Hom FINSET) a b Source Github #

defaultFactorize :: forall k (a :: k) (b :: k). (HasPushouts k, HasEqualizers k) => (a ~> b) -> (Hom k :.: Hom k) a b Source Github #

defaultFactorizeDual :: forall k (a :: k) (b :: k). (HasPullbacks k, HasCoequalizers k) => (a ~> b) -> (Hom k :.: Hom k) a b Source Github #

type HasFiniteLimits k = (HasProducts k, HasPullbacks k, HasEqualizers k) Source Github #

type HasFiniteColimits k = (HasCoproducts k, HasPushouts k, HasCoequalizers k) Source Github #

class (HasFiniteLimits k, HasFiniteColimits k, CCC k, HasSubobjectClassifier k, HasEpiMonoFactorization k) => ElementaryTopos k Source Github #

Instances

Instances details

ElementaryTopos FINSET Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet

false :: ElementaryTopos k => (TerminalObject :: k) ~> (Omega :: k) Source Github #

and :: ElementaryTopos k => ((Omega :: k) && (Omega :: k)) ~> (Omega :: k) Source Github #

or :: ElementaryTopos k => ((Omega :: k) && (Omega :: k)) ~> (Omega :: k) Source Github #

implies :: ElementaryTopos k => ((Omega :: k) && (Omega :: k)) ~> (Omega :: k) Source Github #