Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Fin

Description

The finite ordinal n as a thin category: the kind FIN n has objects FZ, FS FZ, ... (n of them), with an arrow a ~> b exactly when a <= b (LTE) -- the linear order on n elements. Small enough that (co)equalizers can be computed by explicit case analysis.

Documentation

data NAT Source Github #

Constructors

Z
S NAT

data FIN (n :: NAT) where Source Github #

Constructors

FZ :: forall (n1 :: NAT). FIN ('S n1)
FS :: forall (n1 :: NAT). FIN ('S n1) -> FIN ('S ('S n1))

Instances

Instances details

HasEpiMonoFactorization (FIN n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

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

HasBinaryCoproducts (FIN ('S n)) => HasBinaryCoproducts (FIN ('S ('S n))) Source Github #

Maximum

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

withObCoprod :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: FIN ('S ('S n))) (a :: FIN ('S ('S n))) (y :: FIN ('S ('S n))). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))) (x :: FIN ('S ('S n))) (y :: FIN ('S ('S n))). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

HasBinaryCoproducts (FIN ('S 'Z)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Associated Types

type ('FZ :: FIN ('S 'Z)) \|\| ('FZ :: FIN ('S 'Z))
Instance details Defined in Proarrow.Category.Instance.Fin type ('FZ :: FIN ('S 'Z)) \|\| ('FZ :: FIN ('S 'Z)) = 'FZ :: FIN ('S 'Z)

Methods

withObCoprod :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: FIN ('S 'Z)) (a :: FIN ('S 'Z)) (y :: FIN ('S 'Z)). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)) (x :: FIN ('S 'Z)) (y :: FIN ('S 'Z)). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

HasBinaryCoproducts (FIN 'Z) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Associated Types

type (a :: FIN 'Z) \|\| (b :: FIN 'Z)
Instance details Defined in Proarrow.Category.Instance.Fin type (a :: FIN 'Z) \|\| (b :: FIN 'Z) = a

Methods

withObCoprod :: forall (a :: FIN 'Z) (b :: FIN 'Z) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: FIN 'Z) (b :: FIN 'Z). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: FIN 'Z) (b :: FIN 'Z). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: FIN 'Z) (a :: FIN 'Z) (y :: FIN 'Z). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: FIN 'Z) (b :: FIN 'Z) (x :: FIN 'Z) (y :: FIN 'Z). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

HasCoequalizers (FIN n) Source Github #

Dual to the HasEqualizers instance above.

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

coequalize :: forall (a :: FIN n) (b :: FIN n) r. (a ~> b) -> (a ~> b) -> (forall (c :: FIN n). (b ~> c) -> r) -> r Source Github #

factorCoequalizer :: forall (c :: FIN n) (x :: FIN n) (c' :: FIN n). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #

HasInitialObject (FIN ('S n)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Fin type InitialObject = 'FZ :: FIN ('S n)

Methods

initiate :: forall (a :: FIN ('S n)). Ob a => (InitialObject :: FIN ('S n)) ~> a Source Github #

HasPushouts (FIN n) Source Github #

Dual to the HasPullbacks instance above: pushouts in a thin category are joins.

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

pushout :: forall (o :: FIN n) (a :: FIN n) (b :: FIN n) r. (o ~> a) -> (o ~> b) -> (forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r) -> r Source Github #

factorPushout :: forall (a :: FIN n) (b :: FIN n) (p :: FIN n) (q :: FIN n). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

CategoryOf (FIN n) Source Github #

The (thin) category of finite ordinals. An arrow from a to b means that a is less than or equal to b.

Instance details

Defined in Proarrow.Category.Instance.Fin

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Fin type (~>) = LTE :: FIN n -> FIN n -> Type

HasBinaryProducts (FIN ('S n)) => HasBinaryProducts (FIN ('S ('S n))) Source Github #

Minimum

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

withObProd :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: FIN ('S ('S n))) (x :: FIN ('S ('S n))) (y :: FIN ('S ('S n))). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: FIN ('S ('S n))) (b :: FIN ('S ('S n))) (x :: FIN ('S ('S n))) (y :: FIN ('S ('S n))). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasBinaryProducts (FIN ('S 'Z)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Associated Types

type ('FZ :: FIN ('S 'Z)) && ('FZ :: FIN ('S 'Z))
Instance details Defined in Proarrow.Category.Instance.Fin type ('FZ :: FIN ('S 'Z)) && ('FZ :: FIN ('S 'Z)) = 'FZ :: FIN ('S 'Z)

Methods

withObProd :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: FIN ('S 'Z)) (x :: FIN ('S 'Z)) (y :: FIN ('S 'Z)). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: FIN ('S 'Z)) (b :: FIN ('S 'Z)) (x :: FIN ('S 'Z)) (y :: FIN ('S 'Z)). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasBinaryProducts (FIN 'Z) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Associated Types

type (a :: FIN 'Z) && (b :: FIN 'Z)
Instance details Defined in Proarrow.Category.Instance.Fin type (a :: FIN 'Z) && (b :: FIN 'Z) = a

Methods

withObProd :: forall (a :: FIN 'Z) (b :: FIN 'Z) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: FIN 'Z) (b :: FIN 'Z). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: FIN 'Z) (b :: FIN 'Z). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: FIN 'Z) (x :: FIN 'Z) (y :: FIN 'Z). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: FIN 'Z) (b :: FIN 'Z) (x :: FIN 'Z) (y :: FIN 'Z). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasEqualizers (FIN n) Source Github #

LTE is thin, so equalizers are trivial; factorEqualizer incl h just needs h's domain to be <= incl's domain, which -- since both share the codomain x -- can only fail when incl's domain is FZ (nothing below it) but h's domain is a successor (necessarily above FZ).

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

equalize :: forall (a :: FIN n) (b :: FIN n) r. (a ~> b) -> (a ~> b) -> (forall (e :: FIN n). (e ~> a) -> r) -> r Source Github #

factorEqualizer :: forall (e :: FIN n) (x :: FIN n) (e' :: FIN n). (e ~> x) -> (e' ~> x) -> e' ~> e Source Github #

HasPullbacks (FIN n) Source Github #

Pullbacks in a thin category are just meets; computed directly (rather than via thinPullback, which would need HasProducts (FIN n) -- unavailable for an abstract n, since HasBinaryProducts and HasTerminalObject are only resolvable for a syntactically concrete n).

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

pullback :: forall (o :: FIN n) (a :: FIN n) (b :: FIN n) r. (a ~> o) -> (b ~> o) -> (forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r) -> r Source Github #

factorPullback :: forall (a :: FIN n) (b :: FIN n) (p :: FIN n) (q :: FIN n). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #

HasTerminalObject (FIN ('S n)) => HasTerminalObject (FIN ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Fin type TerminalObject = 'FS (TerminalObject :: FIN ('S n))

Methods

terminate :: forall (a :: FIN ('S ('S n))). Ob a => a ~> (TerminalObject :: FIN ('S ('S n))) Source Github #

HasTerminalObject (FIN ('S 'Z)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Fin type TerminalObject = 'FZ :: FIN ('S 'Z)

Methods

terminate :: forall (a :: FIN ('S 'Z)). Ob a => a ~> (TerminalObject :: FIN ('S 'Z)) Source Github #

Promonad (LTE :: FIN n -> FIN n -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

id :: forall (a :: FIN n). Ob a => LTE a a Source Github #

(.) :: forall (b :: FIN n) (c :: FIN n) (a :: FIN n). LTE b c -> LTE a b -> LTE a c Source Github #

ThinProfunctor (LTE :: FIN n -> FIN n -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

arr :: forall (a :: FIN n) (b :: FIN n). (Ob a, Ob b, HasArrow (LTE :: FIN n -> FIN n -> Type) a b) => LTE a b Source Github #

withArr :: forall (a :: FIN n) (b :: FIN n) r. LTE a b -> ((HasArrow (LTE :: FIN n -> FIN n -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

Profunctor (LTE :: FIN n -> FIN n -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

dimap :: forall (c :: FIN n) (a :: FIN n) (b :: FIN n) (d :: FIN n). (c ~> a) -> (b ~> d) -> LTE a b -> LTE c d Source Github #

lmap :: forall (c :: FIN n) (a :: FIN n) (b :: FIN n). (c ~> a) -> LTE a b -> LTE c b Source Github #

rmap :: forall (b :: FIN n) (d :: FIN n) (a :: FIN n). (b ~> d) -> LTE a b -> LTE a d Source Github #

(\\) :: forall (a :: FIN n) (b :: FIN n) r. ((Ob a, Ob b) => r) -> LTE a b -> r Source Github #

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type InitialObject = 'FZ :: FIN ('S n)

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type (~>) = LTE :: FIN n -> FIN n -> Type

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type TerminalObject = 'FS (TerminalObject :: FIN ('S n))

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type TerminalObject = 'FZ :: FIN ('S 'Z)

type Ob (a :: FIN n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type Ob (a :: FIN n) = IsFin a

type (a :: FIN 'Z) || (b :: FIN 'Z) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type (a :: FIN 'Z) || (b :: FIN 'Z) = a

type (a :: FIN 'Z) && (b :: FIN 'Z) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type (a :: FIN 'Z) && (b :: FIN 'Z) = a

type (a :: FIN ('S ('S n))) || ('FZ :: FIN ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type (a :: FIN ('S ('S n))) || ('FZ :: FIN ('S ('S n))) = a

type (a :: FIN ('S ('S n))) && ('FZ :: FIN ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type (a :: FIN ('S ('S n))) && ('FZ :: FIN ('S ('S n))) = 'FZ :: FIN ('S ('S n))

type ('FZ :: FIN ('S ('S n))) || (b :: FIN ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type ('FZ :: FIN ('S ('S n))) || (b :: FIN ('S ('S n))) = b

type ('FZ :: FIN ('S ('S n))) && (b :: FIN ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type ('FZ :: FIN ('S ('S n))) && (b :: FIN ('S ('S n))) = 'FZ :: FIN ('S ('S n))

type ('FZ :: FIN ('S 'Z)) || ('FZ :: FIN ('S 'Z)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type ('FZ :: FIN ('S 'Z)) || ('FZ :: FIN ('S 'Z)) = 'FZ :: FIN ('S 'Z)

type ('FZ :: FIN ('S 'Z)) && ('FZ :: FIN ('S 'Z)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type ('FZ :: FIN ('S 'Z)) && ('FZ :: FIN ('S 'Z)) = 'FZ :: FIN ('S 'Z)

type HasArrow (LTE :: FIN n -> FIN n -> Type) (a :: FIN n) (b :: FIN n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type HasArrow (LTE :: FIN n -> FIN n -> Type) (a :: FIN n) (b :: FIN n) = IsLTE a b

type ('FS a :: FIN ('S ('S n))) || ('FS b :: FIN ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type ('FS a :: FIN ('S ('S n))) || ('FS b :: FIN ('S ('S n))) = 'FS (a || b)

type ('FS a :: FIN ('S ('S n))) && ('FS b :: FIN ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Fin

type ('FS a :: FIN ('S ('S n))) && ('FS b :: FIN ('S ('S n))) = 'FS (a && b)

type FIN0 = FIN 'Z Source Github #

type FIN1 = FIN ('S 'Z) Source Github #

type FIN2 = FIN ('S ('S 'Z)) Source Github #

type FIN3 = FIN ('S ('S ('S 'Z))) Source Github #

data SFin (a :: FIN n) where Source Github #

Constructors

SZ :: forall {n1 :: NAT}. SFin ('FZ :: FIN ('S n1))
SS :: forall {n1 :: NAT} (a1 :: FIN ('S n1)). IsFin a1 => SFin ('FS a1)

data LTE (a :: FIN n) (b :: FIN n) where Source Github #

Constructors

ZEQ :: forall {n1 :: NAT}. LTE ('FZ :: FIN ('S n1)) ('FZ :: FIN ('S n1))
ZLT :: forall {n1 :: NAT} (b1 :: FIN ('S n1)). LTE ('FZ :: FIN ('S n1)) b1 -> LTE ('FZ :: FIN ('S ('S n1))) ('FS b1)
SLT :: forall {n1 :: NAT} (a1 :: FIN ('S n1)) (b1 :: FIN ('S n1)). LTE a1 b1 -> LTE ('FS a1) ('FS b1)

Instances

Instances details

Promonad (LTE :: FIN n -> FIN n -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin Methods id :: forall (a :: FIN n). Ob a => LTE a a Source Github # (.) :: forall (b :: FIN n) (c :: FIN n) (a :: FIN n). LTE b c -> LTE a b -> LTE a c Source Github #
ThinProfunctor (LTE :: FIN n -> FIN n -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin Methods arr :: forall (a :: FIN n) (b :: FIN n). (Ob a, Ob b, HasArrow (LTE :: FIN n -> FIN n -> Type) a b) => LTE a b Source Github # withArr :: forall (a :: FIN n) (b :: FIN n) r. LTE a b -> ((HasArrow (LTE :: FIN n -> FIN n -> Type) a b, Ob a, Ob b) => r) -> r Source Github #
Profunctor (LTE :: FIN n -> FIN n -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin Methods dimap :: forall (c :: FIN n) (a :: FIN n) (b :: FIN n) (d :: FIN n). (c ~> a) -> (b ~> d) -> LTE a b -> LTE c d Source Github # lmap :: forall (c :: FIN n) (a :: FIN n) (b :: FIN n). (c ~> a) -> LTE a b -> LTE c b Source Github # rmap :: forall (b :: FIN n) (d :: FIN n) (a :: FIN n). (b ~> d) -> LTE a b -> LTE a d Source Github # (\\) :: forall (a :: FIN n) (b :: FIN n) r. ((Ob a, Ob b) => r) -> LTE a b -> r Source Github #
type HasArrow (LTE :: FIN n -> FIN n -> Type) (a :: FIN n) (b :: FIN n) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin type HasArrow (LTE :: FIN n -> FIN n -> Type) (a :: FIN n) (b :: FIN n) = IsLTE a b

absurdL :: forall (a :: FIN 'Z) (b :: FIN 'Z). a ~> b Source Github #

absurdR :: forall (a :: FIN 'Z) (b :: FIN 'Z). a ~> b Source Github #

class IsFin (a :: FIN n) where Source Github #

Methods

singFin :: SFin a Source Github #

Instances

Instances details

IsFin (a :: FIN 'Z) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin Methods singFin :: SFin a Source Github #
IsFin ('FZ :: FIN ('S n)) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin Methods singFin :: SFin ('FZ :: FIN ('S n)) Source Github #
IsFin b => IsFin ('FS b :: FIN ('S ('S n))) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin Methods singFin :: SFin ('FS b) Source Github #

class IsLTE (a :: FIN n) (b :: FIN n) where Source Github #

Methods

lte :: a ~> b Source Github #

Instances

Instances details

IsLTE ('FZ :: FIN ('S n)) ('FZ :: FIN ('S n)) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin Methods lte :: ('FZ :: FIN ('S n)) ~> ('FZ :: FIN ('S n)) Source Github #
IsLTE ('FZ :: FIN ('S n)) b => IsLTE ('FZ :: FIN ('S ('S n))) ('FS b :: FIN ('S ('S n))) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin Methods lte :: ('FZ :: FIN ('S ('S n))) ~> 'FS b Source Github #
IsLTE a b => IsLTE ('FS a :: FIN ('S ('S n))) ('FS b :: FIN ('S ('S n))) Source Github #
Instance details Defined in Proarrow.Category.Instance.Fin Methods lte :: 'FS a ~> 'FS b Source Github #