Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Ordinal

Description

The finite ordinal n as a thin category: the kind ORDINAL n has objects OZ, OS OZ, ... (n of them), with an arrow a ~> b when and only when a <= b (LTE). This is the linear order on n elements. Small enough that (co)equalizers can be computed by explicit case analysis.

Synopsis

data ORDINAL (n :: Nat) where
- OZ :: forall (n1 :: Nat). ORDINAL ('S n1)
- OS :: forall (n1 :: Nat). ORDINAL ('S n1) -> ORDINAL ('S ('S n1))
type ORDINAL0 = ORDINAL 'Z
type ORDINAL1 = ORDINAL ('S 'Z)
type ORDINAL2 = ORDINAL ('S ('S 'Z))
type ORDINAL3 = ORDINAL ('S ('S ('S 'Z)))
data LTE (a :: ORDINAL n) (b :: ORDINAL n) where
- ZEQ :: forall {n1 :: Nat}. LTE ('OZ :: ORDINAL ('S n1)) ('OZ :: ORDINAL ('S n1))
- ZLT :: forall {n1 :: Nat} (b1 :: ORDINAL ('S n1)). LTE ('OZ :: ORDINAL ('S n1)) b1 -> LTE ('OZ :: ORDINAL ('S ('S n1))) ('OS b1)
- SLT :: forall {n1 :: Nat} (a1 :: ORDINAL ('S n1)) (b1 :: ORDINAL ('S n1)). LTE a1 b1 -> LTE ('OS a1) ('OS b1)
absurdL :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob a => a ~> b
absurdR :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob b => a ~> b
data SOrdinal (a :: ORDINAL n) where
- SOZ :: forall {n1 :: Nat}. SOrdinal ('OZ :: ORDINAL ('S n1))
- SOS :: forall {n1 :: Nat} (a1 :: ORDINAL ('S n1)). IsOrdinal a1 => SOrdinal ('OS a1)
class IsOrdinal (a :: ORDINAL n) where
- singOrdinal :: SOrdinal a
type family OrdIndex (a :: ORDINAL n) :: Nat where ...
type family OrdAt (n :: Nat) (i :: Nat) :: Maybe (ORDINAL n) where ...
type family OrdObjects (n :: Nat) :: [ORDINAL n] where ...
ordSize :: forall (n :: Nat) r. SNatI n => (n ~ 'Z => r) -> (n ~ 'S 'Z => r) -> (forall (m :: Nat). (n ~ 'S ('S m), SNatI m) => r) -> r
withOrdObjects :: forall (n :: Nat) (i :: Nat) r. SNatI n => SNat i -> (Lookup (OrdObjects n) i ~ OrdAt n i => IndexedList (OrdObjects n) -> r) -> r
ordAtOb :: forall (n :: Nat) (i :: Nat). SNatI n => SNat i -> AtOb (ORDINAL n) (OrdAt n i)
type family OrdLeq (a :: ORDINAL n) (b :: ORDINAL n) :: BOOL where ...
type MonoidalOrdinal (n :: Nat) = (HasProducts (ORDINAL n), Ob (TerminalObject :: ORDINAL n))

Documentation

data ORDINAL (n :: Nat) where Source Github #

Constructors

OZ :: forall (n1 :: Nat). ORDINAL ('S n1)
OS :: forall (n1 :: Nat). ORDINAL ('S n1) -> ORDINAL ('S ('S n1))

Instances

Instances details

SNatI n => Enumerable (ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

withIndex :: forall (a :: ORDINAL n) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: ORDINAL n) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (ORDINAL n) (At (ORDINAL n) i) Source Github #

SNatI n => Finite (ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type Objects (ORDINAL n)
Instance details Defined in Proarrow.Category.Instance.Ordinal type Objects (ORDINAL n) = OrdObjects n

Methods

finite :: IndexedList (Objects (ORDINAL n)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (ORDINAL n)) i ~ At (ORDINAL n) i => r) -> r Source Github #

Indexed (ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

MonoidalOrdinal n => Monoidal (ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.Ordinal type Unit = TerminalObject :: ORDINAL n

Methods

withOb2 :: forall (a :: ORDINAL n) (b :: ORDINAL n) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: ORDINAL n). Ob a => ((Unit :: ORDINAL n) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: ORDINAL n). Ob a => a ~> ((Unit :: ORDINAL n) ** a) Source Github #

rightUnitor :: forall (a :: ORDINAL n). Ob a => (a ** (Unit :: ORDINAL n)) ~> a Source Github #

rightUnitorInv :: forall (a :: ORDINAL n). Ob a => a ~> (a ** (Unit :: ORDINAL n)) Source Github #

associator :: forall (a :: ORDINAL n) (b :: ORDINAL n) (c :: ORDINAL n). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: ORDINAL n) (b :: ORDINAL n) (c :: ORDINAL n). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

MonoidalOrdinal n => SymMonoidal (ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

swap :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

MonoidalOrdinal n => CopyDiscard (ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

copy :: forall (a :: ORDINAL n). Ob a => a ~> (a ** a) Source Github #

discard :: forall (a :: ORDINAL n). Ob a => a ~> (Unit :: ORDINAL n) Source Github #

(Distributive (ORDINAL ('S n)), MonoidalOrdinal ('S n)) => Distributive (ORDINAL ('S ('S n))) Source Github #

A chain is a distributive lattice: the meet is the minimum and the join the maximum. By recursion on the objects, as the products and coproducts are. A bottom on either side makes both sides the same object, and otherwise both sides are a successor.

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

distL :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))) (c :: ORDINAL ('S ('S n))). (Ob a, Ob b, Ob c) => (a ** (b || c)) ~> ((a ** b) || (a ** c)) Source Github #

distR :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))) (c :: ORDINAL ('S ('S n))). (Ob a, Ob b, Ob c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)) Source Github #

absorbL :: forall (a :: ORDINAL ('S ('S n))). Ob a => (a ** (InitialObject :: ORDINAL ('S ('S n)))) ~> (InitialObject :: ORDINAL ('S ('S n))) Source Github #

absorbR :: forall (a :: ORDINAL ('S ('S n))). Ob a => ((InitialObject :: ORDINAL ('S ('S n))) ** a) ~> (InitialObject :: ORDINAL ('S ('S n))) Source Github #

Distributive (ORDINAL ('S 'Z)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

distL :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)) (c :: ORDINAL ('S 'Z)). (Ob a, Ob b, Ob c) => (a ** (b || c)) ~> ((a ** b) || (a ** c)) Source Github #

distR :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)) (c :: ORDINAL ('S 'Z)). (Ob a, Ob b, Ob c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)) Source Github #

absorbL :: forall (a :: ORDINAL ('S 'Z)). Ob a => (a ** (InitialObject :: ORDINAL ('S 'Z))) ~> (InitialObject :: ORDINAL ('S 'Z)) Source Github #

absorbR :: forall (a :: ORDINAL ('S 'Z)). Ob a => ((InitialObject :: ORDINAL ('S 'Z)) ** a) ~> (InitialObject :: ORDINAL ('S 'Z)) Source Github #

HasEpiMonoFactorization (ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

Maximum

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type ('OZ :: ORDINAL ('S 'Z)) \|\| ('OZ :: ORDINAL ('S 'Z))
Instance details Defined in Proarrow.Category.Instance.Ordinal type ('OZ :: ORDINAL ('S 'Z)) \|\| ('OZ :: ORDINAL ('S 'Z)) = 'OZ :: ORDINAL ('S 'Z)

Methods

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

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

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

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

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

HasBinaryCoproducts (ORDINAL 'Z) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

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

Methods

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

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

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

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

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

HasCoequalizers (ORDINAL n) Source Github #

Dual to the HasEqualizers instance above.

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Ordinal type InitialObject = 'OZ :: ORDINAL ('S n)

Methods

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

HasPushouts (ORDINAL n) Source Github #

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

CategoryOf (ORDINAL 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.Ordinal

Associated Types

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

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

Minimum

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

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

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type ('OZ :: ORDINAL ('S 'Z)) && ('OZ :: ORDINAL ('S 'Z))
Instance details Defined in Proarrow.Category.Instance.Ordinal type ('OZ :: ORDINAL ('S 'Z)) && ('OZ :: ORDINAL ('S 'Z)) = 'OZ :: ORDINAL ('S 'Z)

Methods

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

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

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

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

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

HasBinaryProducts (ORDINAL 'Z) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

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

Methods

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

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

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

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

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

HasEqualizers (ORDINAL n) Source Github #

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

HasPullbacks (ORDINAL n) Source Github #

Pullbacks in a thin category are just meets. Computed directly, not via thinPullback, which would need HasProducts (ORDINAL n). That is unavailable for an abstract n, since HasBinaryProducts and HasTerminalObject are only resolvable for a syntactically concrete n.

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Ordinal type TerminalObject = 'OS (TerminalObject :: ORDINAL ('S n))

Methods

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

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Ordinal type TerminalObject = 'OZ :: ORDINAL ('S 'Z)

Methods

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

(MonoidalOrdinal n, Ob a) => CocommutativeComonoid (a :: ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

(MonoidalOrdinal n, Ob a) => Comonoid (a :: ORDINAL n) Source Github #

Every object is a comonoid by the diagonal and the map to the top. So the chain is CopyDiscard, and hence Cartesian.

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

counit :: a ~> (Unit :: ORDINAL n) Source Github #

comult :: a ~> (a ** a) Source Github #

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

Finitary (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github #

The ordinals are thin too, so the same three lines serve. So a chain can be used as a site: a cover there can have a leg that is itself covered, which no coverage on a two-object category can arrange.

Instance details

Defined in Proarrow.Category.Enriched.Finitary

Methods

size :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => Natural Source Github #

toIndex :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => LTE a b -> Natural Source Github #

fromIndex :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => Natural -> LTE a b Source Github #

elements :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => [LTE a b] Source Github #

DecidableProfunctor (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

decide :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => Decision (LTE :: ORDINAL n -> ORDINAL n -> Type) a b (Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) a b) Source Github #

toHolds :: forall (a :: ORDINAL n) (b :: ORDINAL n) r. LTE a b -> ((Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

MonoidalOrdinal n => MonoidalProfunctor (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

one :: LTE (Unit :: ORDINAL n) (Unit :: ORDINAL n) Source Github #

(**) :: forall (x1 :: ORDINAL n) (x2 :: ORDINAL n) (y1 :: ORDINAL n) (y2 :: ORDINAL n). LTE x1 x2 -> LTE y1 y2 -> LTE (x1 ** y1) (x2 ** y2) Source Github #

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

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

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

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

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

type Objects (ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type Objects (ORDINAL n) = OrdObjects n

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type Unit = TerminalObject :: ORDINAL n

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type InitialObject = 'OZ :: ORDINAL ('S n)

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

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

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type TerminalObject = 'OS (TerminalObject :: ORDINAL ('S n))

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type TerminalObject = 'OZ :: ORDINAL ('S 'Z)

type At (ORDINAL n) i Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type At (ORDINAL n) i = OrdAt n i

type Index (a :: ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type Index (a :: ORDINAL n) = OrdIndex a

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type Ob (a :: ORDINAL n) = IsOrdinal a

type (a :: ORDINAL n) ** (b :: ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type (a :: ORDINAL n) ** (b :: ORDINAL n) = a && b

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

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

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

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

type (a :: ORDINAL ('S ('S n))) || ('OZ :: ORDINAL ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type (a :: ORDINAL ('S ('S n))) || ('OZ :: ORDINAL ('S ('S n))) = a

type (a :: ORDINAL ('S ('S n))) && ('OZ :: ORDINAL ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type (a :: ORDINAL ('S ('S n))) && ('OZ :: ORDINAL ('S ('S n))) = 'OZ :: ORDINAL ('S ('S n))

type ('OZ :: ORDINAL ('S ('S n))) || (b :: ORDINAL ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type ('OZ :: ORDINAL ('S ('S n))) || (b :: ORDINAL ('S ('S n))) = b

type ('OZ :: ORDINAL ('S ('S n))) && (b :: ORDINAL ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type ('OZ :: ORDINAL ('S ('S n))) && (b :: ORDINAL ('S ('S n))) = 'OZ :: ORDINAL ('S ('S n))

type ('OZ :: ORDINAL ('S 'Z)) || ('OZ :: ORDINAL ('S 'Z)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type ('OZ :: ORDINAL ('S 'Z)) || ('OZ :: ORDINAL ('S 'Z)) = 'OZ :: ORDINAL ('S 'Z)

type ('OZ :: ORDINAL ('S 'Z)) && ('OZ :: ORDINAL ('S 'Z)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type ('OZ :: ORDINAL ('S 'Z)) && ('OZ :: ORDINAL ('S 'Z)) = 'OZ :: ORDINAL ('S 'Z)

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

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type HasArrow (LTE :: ORDINAL n -> ORDINAL n -> Type) (a :: ORDINAL n) (b :: ORDINAL n) = Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) a b ~ 'TRU

type Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) (a :: ORDINAL n) (b :: ORDINAL n) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) (a :: ORDINAL n) (b :: ORDINAL n) = OrdLeq a b

type ('OS a :: ORDINAL ('S ('S n))) || ('OS b :: ORDINAL ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type ('OS a :: ORDINAL ('S ('S n))) || ('OS b :: ORDINAL ('S ('S n))) = 'OS (a || b)

type ('OS a :: ORDINAL ('S ('S n))) && ('OS b :: ORDINAL ('S ('S n))) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Ordinal

type ('OS a :: ORDINAL ('S ('S n))) && ('OS b :: ORDINAL ('S ('S n))) = 'OS (a && b)

type ORDINAL0 = ORDINAL 'Z Source Github #

type ORDINAL1 = ORDINAL ('S 'Z) Source Github #

type ORDINAL2 = ORDINAL ('S ('S 'Z)) Source Github #

type ORDINAL3 = ORDINAL ('S ('S ('S 'Z))) Source Github #

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

Constructors

ZEQ :: forall {n1 :: Nat}. LTE ('OZ :: ORDINAL ('S n1)) ('OZ :: ORDINAL ('S n1))
ZLT :: forall {n1 :: Nat} (b1 :: ORDINAL ('S n1)). LTE ('OZ :: ORDINAL ('S n1)) b1 -> LTE ('OZ :: ORDINAL ('S ('S n1))) ('OS b1)
SLT :: forall {n1 :: Nat} (a1 :: ORDINAL ('S n1)) (b1 :: ORDINAL ('S n1)). LTE a1 b1 -> LTE ('OS a1) ('OS b1)

Instances

Instances details

Promonad (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Ordinal Methods id :: forall (a :: ORDINAL n). Ob a => LTE a a Source Github # (.) :: forall (b :: ORDINAL n) (c :: ORDINAL n) (a :: ORDINAL n). LTE b c -> LTE a b -> LTE a c Source Github #
Finitary (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github #	The ordinals are thin too, so the same three lines serve. So a chain can be used as a site: a cover there can have a leg that is itself covered, which no coverage on a two-object category can arrange.
Instance details Defined in Proarrow.Category.Enriched.Finitary Methods size :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => Natural Source Github # toIndex :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => LTE a b -> Natural Source Github # fromIndex :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => Natural -> LTE a b Source Github # elements :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => [LTE a b] Source Github #
DecidableProfunctor (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Ordinal Methods decide :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => Decision (LTE :: ORDINAL n -> ORDINAL n -> Type) a b (Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) a b) Source Github # toHolds :: forall (a :: ORDINAL n) (b :: ORDINAL n) r. LTE a b -> ((Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #
ThinProfunctor (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Ordinal Methods arr :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b, HasArrow (LTE :: ORDINAL n -> ORDINAL n -> Type) a b) => LTE a b Source Github # withArr :: forall (a :: ORDINAL n) (b :: ORDINAL n) r. LTE a b -> ((HasArrow (LTE :: ORDINAL n -> ORDINAL n -> Type) a b, Ob a, Ob b) => r) -> r Source Github #
MonoidalOrdinal n => MonoidalProfunctor (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Ordinal Methods one :: LTE (Unit :: ORDINAL n) (Unit :: ORDINAL n) Source Github # () :: forall (x1 :: ORDINAL n) (x2 :: ORDINAL n) (y1 :: ORDINAL n) (y2 :: ORDINAL n). LTE x1 x2 -> LTE y1 y2 -> LTE (x1 y1) (x2 ** y2) Source Github #
Profunctor (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Ordinal Methods dimap :: forall (c :: ORDINAL n) (a :: ORDINAL n) (b :: ORDINAL n) (d :: ORDINAL n). (c ~> a) -> (b ~> d) -> LTE a b -> LTE c d Source Github # lmap :: forall (c :: ORDINAL n) (a :: ORDINAL n) (b :: ORDINAL n). (c ~> a) -> LTE a b -> LTE c b Source Github # rmap :: forall (b :: ORDINAL n) (d :: ORDINAL n) (a :: ORDINAL n). (b ~> d) -> LTE a b -> LTE a d Source Github # (\\) :: forall (a :: ORDINAL n) (b :: ORDINAL n) r. ((Ob a, Ob b) => r) -> LTE a b -> r Source Github #
type HasArrow (LTE :: ORDINAL n -> ORDINAL n -> Type) (a :: ORDINAL n) (b :: ORDINAL n) Source Github #
Instance details Defined in Proarrow.Category.Instance.Ordinal type HasArrow (LTE :: ORDINAL n -> ORDINAL n -> Type) (a :: ORDINAL n) (b :: ORDINAL n) = Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) a b ~ 'TRU
type Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) (a :: ORDINAL n) (b :: ORDINAL n) Source Github #
Instance details Defined in Proarrow.Category.Instance.Ordinal type Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) (a :: ORDINAL n) (b :: ORDINAL n) = OrdLeq a b

absurdL :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob a => a ~> b Source Github #

ORDINAL Z is the empty ordinal, so an object of it is a contradiction: LTE a a has no constructor that can match at this kind, and the empty case discharges any goal.

absurdR :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob b => a ~> b Source Github #

data SOrdinal (a :: ORDINAL n) where Source Github #

Constructors

SOZ :: forall {n1 :: Nat}. SOrdinal ('OZ :: ORDINAL ('S n1))
SOS :: forall {n1 :: Nat} (a1 :: ORDINAL ('S n1)). IsOrdinal a1 => SOrdinal ('OS a1)

class IsOrdinal (a :: ORDINAL n) where Source Github #

Methods

singOrdinal :: SOrdinal a Source Github #

Instances

Instances details

IsOrdinal ('OZ :: ORDINAL ('S n)) Source Github #
Instance details Defined in Proarrow.Category.Instance.Ordinal Methods singOrdinal :: SOrdinal ('OZ :: ORDINAL ('S n)) Source Github #
IsOrdinal b => IsOrdinal ('OS b :: ORDINAL ('S ('S n))) Source Github #
Instance details Defined in Proarrow.Category.Instance.Ordinal Methods singOrdinal :: SOrdinal ('OS b) Source Github #

type family OrdIndex (a :: ORDINAL n) :: Nat where ... Source Github #

Each ordinal is numbered by itself: OZ is zero and OS the successor.

Equations

OrdIndex ('OZ :: ORDINAL ('S n)) = 'Z
OrdIndex ('OS a :: ORDINAL ('S ('S n))) = 'S (OrdIndex a)

type family OrdAt (n :: Nat) (i :: Nat) :: Maybe (ORDINAL n) where ... Source Github #

Equations

OrdAt 'Z i = 'Nothing :: Maybe (ORDINAL 'Z)
OrdAt ('S n) 'Z = 'Just ('OZ :: ORDINAL ('S n))
OrdAt ('S 'Z) ('S i) = 'Nothing :: Maybe (ORDINAL ('S 'Z))
OrdAt ('S ('S n)) ('S i) = FmapWrap ('OS :: ORDINAL ('S n) -> ORDINAL ('S ('S n))) (OrdAt ('S n) i)

type family OrdObjects (n :: Nat) :: [ORDINAL n] where ... Source Github #

The ordinals of ORDINAL n, in order.

Equations

OrdObjects 'Z = '[] :: [ORDINAL 'Z]
OrdObjects ('S 'Z) = '['OZ :: ORDINAL ('S 'Z)]
OrdObjects ('S ('S n)) = ('OZ :: ORDINAL ('S ('S n))) ': MapWrap ('OS :: ORDINAL ('S n) -> ORDINAL ('S ('S n))) (OrdObjects ('S n))

ordSize :: forall (n :: Nat) r. SNatI n => (n ~ 'Z => r) -> (n ~ 'S 'Z => r) -> (forall (m :: Nat). (n ~ 'S ('S m), SNatI m) => r) -> r Source Github #

An ordinal count is none, one, or more. It needs three cases, and not the two of Nat, because OS lands in ORDINAL (S (S n)), so ORDINAL (S Z) holds only OZ.

withOrdObjects :: forall (n :: Nat) (i :: Nat) r. SNatI n => SNat i -> (Lookup (OrdObjects n) i ~ OrdAt n i => IndexedList (OrdObjects n) -> r) -> r Source Github #

The ordinals of ORDINAL n together with the proof that the list tabulates OrdAt at one index. The two are produced by the same recursion, so each level builds the shorter list once and both the proof and the longer list use it.

ordAtOb :: forall (n :: Nat) (i :: Nat). SNatI n => SNat i -> AtOb (ORDINAL n) (OrdAt n i) Source Github #

The ordinal at an index, if there is one. Enumerable cannot go through the generic atOb, which is defined in terms of the withOb being given here, so the walk is done by recursion on the index instead of on the object list.

type family OrdLeq (a :: ORDINAL n) (b :: ORDINAL n) :: BOOL where ... Source Github #

a <= b on the ordinal, as a BOOL.

Equations

OrdLeq ('OZ :: ORDINAL ('S n)) (b :: ORDINAL ('S n)) = 'TRU
OrdLeq ('OS a :: ORDINAL ('S ('S n))) ('OZ :: ORDINAL ('S ('S n))) = 'FLS
OrdLeq ('OS a :: ORDINAL ('S ('S n))) ('OS b :: ORDINAL ('S ('S n))) = OrdLeq a b

type MonoidalOrdinal (n :: Nat) = (HasProducts (ORDINAL n), Ob (TerminalObject :: ORDINAL n)) Source Github #

The meet as tensor and the top as unit: the cartesian monoidal structure. Like the products it is made of, only for a syntactically concrete n. MonoidalOrdinal names the context.