Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Fin

Documentation

data NAT Source Comments #

Constructors

Z
S NAT

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

Constructors

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

Instances

Instances details

CategoryOf (FIN n) Source Comments #

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

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

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 Comments #

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

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

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

(+++) :: 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 Comments #

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

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 Comments #

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

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

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

(+++) :: 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 Comments #

HasBinaryCoproducts (FIN 'Z) Source Comments #

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 Comments #

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

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

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

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

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

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 Comments #

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

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

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

(***) :: 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 Comments #

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

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 Comments #

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

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

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

(***) :: 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 Comments #

HasBinaryProducts (FIN 'Z) Source Comments #

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 Comments #

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

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

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

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

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

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 Comments #

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

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 Comments #

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

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 Comments #

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

Instance details

Defined in Proarrow.Category.Instance.Fin

Methods

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

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

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

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 Comments #

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

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

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 Comments #

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

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fin

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

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fin

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

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fin

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

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Fin

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

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

Instance details

Defined in Proarrow.Category.Instance.Fin

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

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

Instance details

Defined in Proarrow.Category.Instance.Fin

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

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

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 Comments #

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 Comments #

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 Comments #

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 Comments #

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 Comments #

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 Comments #

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 Comments #

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 Comments #

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 Comments #

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 Comments #

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

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

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

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

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 Comments #

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 Comments #
Instance details Defined in Proarrow.Category.Instance.Fin Methods id :: forall (a :: FIN n). Ob a => LTE a a Source Comments # (.) :: forall (b :: FIN n) (c :: FIN n) (a :: FIN n). LTE b c -> LTE a b -> LTE a c Source Comments #
ThinProfunctor (LTE :: FIN n -> FIN n -> Type) Source Comments #
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 Comments # withArr :: forall (a :: FIN n) (b :: FIN n) r. LTE a b -> (HasArrow (LTE :: FIN n -> FIN n -> Type) a b => r) -> r Source Comments #
Profunctor (LTE :: FIN n -> FIN n -> Type) Source Comments #
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 Comments # (\\) :: forall (a :: FIN n) (b :: FIN n) r. ((Ob a, Ob b) => r) -> LTE a b -> r Source Comments #
type HasArrow (LTE :: FIN n -> FIN n -> Type) (a :: FIN n) (b :: FIN n) Source Comments #
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 Comments #

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

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

Methods

singFin :: SFin a Source Comments #

Instances

Instances details

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

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

Methods

lte :: a ~> b Source Comments #

Instances

Instances details

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