Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Simplex

Documentation

data Nat Source Comments #

Constructors

Z
S Nat

Instances

Instances details

Monoidal Nat Source Comments #

Addition as monoidal tensor.

Instance details

Defined in Proarrow.Category.Instance.Simplex

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.Simplex type Unit = 'Z
type (a :: Nat) ** (b :: Nat)
Instance details Defined in Proarrow.Category.Instance.Simplex type (a :: Nat) ** (b :: Nat) = a + b

Methods

withOb2 :: forall (a :: Nat) (b :: Nat) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Comments #

leftUnitor :: forall (a :: Nat). Ob a => ((Unit :: Nat) ** a) ~> a Source Comments #

leftUnitorInv :: forall (a :: Nat). Ob a => a ~> ((Unit :: Nat) ** a) Source Comments #

rightUnitor :: forall (a :: Nat). Ob a => (a ** (Unit :: Nat)) ~> a Source Comments #

rightUnitorInv :: forall (a :: Nat). Ob a => a ~> (a ** (Unit :: Nat)) Source Comments #

associator :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Comments #

associatorInv :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Comments #

CategoryOf Nat Source Comments #

The (augmented) simplex category is the category of finite ordinals and order preserving maps.

Instance details

Defined in Proarrow.Category.Instance.Simplex

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Simplex type (~>) = Simplex
type Ob (a :: Nat)
Instance details Defined in Proarrow.Category.Instance.Simplex type Ob (a :: Nat) = IsNat a

HasInitialObject Nat Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Simplex type InitialObject = 'Z

Methods

initiate :: forall (a :: Nat). Ob a => (InitialObject :: Nat) ~> a Source Comments #

HasTerminalObject Nat Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Simplex type TerminalObject = 'S 'Z

Methods

terminate :: forall (a :: Nat). Ob a => a ~> (TerminalObject :: Nat) Source Comments #

Promonad Simplex Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

id :: forall (a :: Nat). Ob a => Simplex a a Source Comments #

(.) :: forall (b :: Nat) (c :: Nat) (a :: Nat). Simplex b c -> Simplex a b -> Simplex a c Source Comments #

Monoid 'Z Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

mempty :: (Unit :: Nat) ~> 'Z Source Comments #

mappend :: ('Z ** 'Z) ~> 'Z Source Comments #

MonoidalProfunctor Simplex Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

par0 :: Simplex (Unit :: Nat) (Unit :: Nat) Source Comments #

par :: forall (x1 :: Nat) (x2 :: Nat) (y1 :: Nat) (y2 :: Nat). Simplex x1 x2 -> Simplex y1 y2 -> Simplex (x1 ** y1) (x2 ** y2) Source Comments #

Profunctor Simplex Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

dimap :: forall (c :: Nat) (a :: Nat) (b :: Nat) (d :: Nat). (c ~> a) -> (b ~> d) -> Simplex a b -> Simplex c d Source Comments #

(\\) :: forall (a :: Nat) (b :: Nat) r. ((Ob a, Ob b) => r) -> Simplex a b -> r Source Comments #

FunctorForRep Forget Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Associated Types

type Forget @ (n :: Nat)
Instance details Defined in Proarrow.Category.Instance.Simplex type Forget @ (n :: Nat) = Fin n

Methods

fmap :: forall (a :: Nat) (b :: Nat). (a ~> b) -> (Forget @ a) ~> (Forget @ b) Source Comments #

Monoid m => FunctorForRep (Replicate m :: Nat +-> k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

fmap :: forall (a :: Nat) (b :: Nat). (a ~> b) -> (Replicate m @ a) ~> (Replicate m @ b) Source Comments #

Monoid ('S 'Z) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

mempty :: (Unit :: Nat) ~> 'S 'Z Source Comments #

mappend :: ('S 'Z ** 'S 'Z) ~> 'S 'Z Source Comments #

type Unit Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type Unit = 'Z

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (~>) = Simplex

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type InitialObject = 'Z

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type TerminalObject = 'S 'Z

type Ob (a :: Nat) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type Ob (a :: Nat) = IsNat a

type (a :: Nat) ** (b :: Nat) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (a :: Nat) ** (b :: Nat) = a + b

type Forget @ (n :: Nat) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type Forget @ (n :: Nat) = Fin n

type (Replicate m :: Nat +-> k) @ 'Z Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (Replicate m :: Nat +-> k) @ 'Z = Unit :: k

type (Replicate m :: Nat +-> k) @ ('S b :: Nat) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (Replicate m :: Nat +-> k) @ ('S b :: Nat) = m ** (Replicate m @ b)

data SNat (a :: Nat) where Source Comments #

Constructors

SZ :: SNat 'Z
SS :: forall (n :: Nat). IsNat n => SNat ('S n)

Instances

Instances details

Show (SNat n) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods showsPrec :: Int -> SNat n -> ShowS Comments # show :: SNat n -> String Comments # showList :: [SNat n] -> ShowS Comments #

class ((a + 'Z) ~ a, (a + 'S b) ~ 'S (a + b), ((a + b) + c) ~ (a + (b + c))) => Rules (a :: Nat) (b :: Nat) (c :: Nat) Source Comments #

Instances

Instances details

((a + 'Z) ~ a, (a + 'S b) ~ 'S (a + b), ((a + b) + c) ~ (a + (b + c))) => Rules a b c Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex

class (forall (b :: Nat) (c :: Nat). Rules a b c) => IsNat (a :: Nat) where Source Comments #

Methods

singNat :: SNat a Source Comments #

Instances

Instances details

IsNat 'Z Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods singNat :: SNat 'Z Source Comments #
IsNat a => IsNat ('S a) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods singNat :: SNat ('S a) Source Comments #

data Simplex (a :: Nat) (b :: Nat) where Source Comments #

Constructors

ZZ :: Simplex 'Z 'Z
Y :: forall (a :: Nat) (y :: Nat). Simplex a y -> Simplex a ('S y)
X :: forall (x :: Nat) (y :: Nat). Simplex x ('S y) -> Simplex ('S x) ('S y)

Instances

Instances details

Promonad Simplex Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods id :: forall (a :: Nat). Ob a => Simplex a a Source Comments # (.) :: forall (b :: Nat) (c :: Nat) (a :: Nat). Simplex b c -> Simplex a b -> Simplex a c Source Comments #
MonoidalProfunctor Simplex Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods par0 :: Simplex (Unit :: Nat) (Unit :: Nat) Source Comments # par :: forall (x1 :: Nat) (x2 :: Nat) (y1 :: Nat) (y2 :: Nat). Simplex x1 x2 -> Simplex y1 y2 -> Simplex (x1 y1) (x2 y2) Source Comments #
Profunctor Simplex Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods dimap :: forall (c :: Nat) (a :: Nat) (b :: Nat) (d :: Nat). (c ~> a) -> (b ~> d) -> Simplex a b -> Simplex c d Source Comments # (\\) :: forall (a :: Nat) (b :: Nat) r. ((Ob a, Ob b) => r) -> Simplex a b -> r Source Comments #
Show (Simplex a b) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods showsPrec :: Int -> Simplex a b -> ShowS Comments # show :: Simplex a b -> String Comments # showList :: [Simplex a b] -> ShowS Comments #
Eq (Simplex a b) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods (==) :: Simplex a b -> Simplex a b -> Bool Comments # (/=) :: Simplex a b -> Simplex a b -> Bool Comments #

suc :: forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex ('S a) ('S b) Source Comments #

data Fin (a :: Nat) where Source Comments #

Constructors

Fz :: forall (n :: Nat). Fin ('S n)
Fs :: forall (n :: Nat). Fin n -> Fin ('S n)

data family Forget :: Nat +-> Type Source Comments #

Instances

Instances details

FunctorForRep Forget Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Associated Types

type Forget @ (n :: Nat)
Instance details Defined in Proarrow.Category.Instance.Simplex type Forget @ (n :: Nat) = Fin n

Methods

fmap :: forall (a :: Nat) (b :: Nat). (a ~> b) -> (Forget @ a) ~> (Forget @ b) Source Comments #

type Forget @ (n :: Nat) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type Forget @ (n :: Nat) = Fin n

type family (a :: Nat) + (b :: Nat) :: Nat where ... Source Comments #

Equations

'Z + b = b
('S a) + b = 'S (a + b)

data family Replicate :: k -> Nat +-> k Source Comments #

Instances

Instances details

Monoid m => FunctorForRep (Replicate m :: Nat +-> k) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods fmap :: forall (a :: Nat) (b :: Nat). (a ~> b) -> (Replicate m @ a) ~> (Replicate m @ b) Source Comments #
type (Replicate m :: Nat +-> k) @ 'Z Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type (Replicate m :: Nat +-> k) @ 'Z = Unit :: k
type (Replicate m :: Nat +-> k) @ ('S b :: Nat) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type (Replicate m :: Nat +-> k) @ ('S b :: Nat) = m ** (Replicate m @ b)