Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Simplex

Contents

Orphan instances

Synopsis

suc :: forall (a :: Nat) (b :: Nat). Simplex a b -> Simplex ('S a) ('S b)
type (+) (n :: Nat) (m :: Nat) = Plus n m
data family Forget :: Nat +-> Type
class (forall (b :: Nat) (c :: Nat). Rules a b c, SNatI a, Typeable a) => IsNat (a :: Nat) where
- singNat :: SNat a
data family Pick :: Type -> OPPOSITE Nat +-> Type
data family Replicate :: k -> Nat +-> k
class ((a + 'Z) ~ a, (a + 'S b) ~ 'S (a + b), ((a + b) + c) ~ (a + (b + c))) => Rules (a :: Nat) (b :: Nat) (c :: Nat)
data SNat (a :: Nat) where
- SZ :: SNat 'Z
- SS :: forall (n :: Nat). IsNat n => SNat ('S n)
data Simplex (a :: Nat) (b :: Nat) where
- 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)
data Nat
- = Z
- | S Nat

Documentation

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

type (+) (n :: Nat) (m :: Nat) = Plus n m Source Github #

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

Instances

Instances details

FunctorForRep Forget Source Github #

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

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

Instance details

Defined in Proarrow.Category.Instance.Simplex

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

class (forall (b :: Nat) (c :: Nat). Rules a b c, SNatI a, Typeable a) => IsNat (a :: Nat) where Source Github #

Methods

singNat :: SNat a Source Github #

Instances

Instances details

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

data family Pick :: Type -> OPPOSITE Nat +-> Type Source Github #

Instances

Instances details

FunctorForRep (Pick a :: OPPOSITE Nat +-> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods fmap :: forall (a0 :: OPPOSITE Nat) (b :: OPPOSITE Nat). (a0 ~> b) -> (Pick a @ a0) ~> (Pick a @ b) Source Github #
type (Pick a :: OPPOSITE Nat +-> Type) @ ('OP n :: OPPOSITE Nat) Source Github #
Instance details Defined in Proarrow.Category.Instance.Simplex type (Pick a :: OPPOSITE Nat +-> Type) @ ('OP n :: OPPOSITE Nat) = Vec n a

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

Instances

Instances details

Monoid m => FunctorForRep (Replicate m :: Nat +-> k) Source Github #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods fmap :: forall (a :: Nat) (b :: Nat). (a ~> b) -> (Replicate m @ a) ~> (Replicate m @ b) Source Github #
type (Replicate m :: Nat +-> k) @ 'Z Source Github #
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 Github #
Instance details Defined in Proarrow.Category.Instance.Simplex type (Replicate m :: Nat +-> k) @ ('S b :: Nat) = m ** (Replicate m @ b)

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

Instances

Instances details

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

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

Constructors

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

Instances

Instances details

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

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

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

data Nat Source Github #

Nat natural numbers.

Better than GHC's built-in Nat for some use cases.

Constructors

Z
S Nat

Instances

Instances details

Arbitrary Nat Source Github #

Instance details

Defined in Data.Nat

Methods

arbitrary :: Gen Nat Source Github #

shrink :: Nat -> [Nat] Source Github #

CoArbitrary Nat Source Github #

Instance details

Defined in Data.Nat

Methods

coarbitrary :: Nat -> Gen b -> Gen b Source Github #

Function Nat Source Github #

Instance details

Defined in Data.Nat

Methods

function :: (Nat -> b) -> Nat :-> b Source Github #

NFData Nat Source Github #

Instance details

Defined in Data.Nat

Methods

rnf :: Nat -> () Github #

Data Nat Source Github #

Instance details

Defined in Data.Nat

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nat -> c Nat Github #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Nat Github #

toConstr :: Nat -> Constr Github #

dataTypeOf :: Nat -> DataType Github #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Nat) Github #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat) Github #

gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat Github #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r Github #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r Github #

gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u] Github #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u Github #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Nat -> m Nat Github #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat Github #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat Github #

Enum Nat Source Github #

Instance details

Defined in Data.Nat

Methods

succ :: Nat -> Nat Github #

pred :: Nat -> Nat Github #

toEnum :: Int -> Nat Github #

fromEnum :: Nat -> Int Github #

enumFrom :: Nat -> [Nat] Github #

enumFromThen :: Nat -> Nat -> [Nat] Github #

enumFromTo :: Nat -> Nat -> [Nat] Github #

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] Github #

Num Nat Source Github #

Instance details

Defined in Data.Nat

Methods

(+) :: Nat -> Nat -> Nat Github #

(-) :: Nat -> Nat -> Nat Github #

(*) :: Nat -> Nat -> Nat Github #

negate :: Nat -> Nat Github #

abs :: Nat -> Nat Github #

signum :: Nat -> Nat Github #

fromInteger :: Integer -> Nat Github #

Integral Nat Source Github #

Instance details

Defined in Data.Nat

Methods

quot :: Nat -> Nat -> Nat Github #

rem :: Nat -> Nat -> Nat Github #

div :: Nat -> Nat -> Nat Github #

mod :: Nat -> Nat -> Nat Github #

quotRem :: Nat -> Nat -> (Nat, Nat) Github #

divMod :: Nat -> Nat -> (Nat, Nat) Github #

toInteger :: Nat -> Integer Github #

Real Nat Source Github #

Instance details

Defined in Data.Nat

Methods

toRational :: Nat -> Rational Github #

Show Nat Source Github #

Nat is printed as Natural.

To see explicit structure, use explicitShow or explicitShowsPrec

Instance details

Defined in Data.Nat

Methods

showsPrec :: Int -> Nat -> ShowS Github #

show :: Nat -> String Github #

showList :: [Nat] -> ShowS Github #

Eq Nat Source Github #

Instance details

Defined in Data.Nat

Methods

(==) :: Nat -> Nat -> Bool Github #

(/=) :: Nat -> Nat -> Bool Github #

Ord Nat Source Github #

Instance details

Defined in Data.Nat

Methods

compare :: Nat -> Nat -> Ordering Github #

(<) :: Nat -> Nat -> Bool Github #

(<=) :: Nat -> Nat -> Bool Github #

(>) :: Nat -> Nat -> Bool Github #

(>=) :: Nat -> Nat -> Bool Github #

max :: Nat -> Nat -> Nat Github #

min :: Nat -> Nat -> Nat Github #

Hashable Nat Source Github #

Instance details

Defined in Data.Nat

Methods

hashWithSalt :: Int -> Nat -> Int Source Github #

hash :: Nat -> Int Source Github #

Monoidal Nat Source Github #

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

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

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

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

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

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

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

CategoryOf Nat Source Github #

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

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

HasTerminalObject Nat Source Github #

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

Universe Nat Source Github #

>>> import qualified Data.Universe.Class as U
>>> take 10 (U.universe :: [Nat])
[0,1,2,3,4,5,6,7,8,9]

Since: fin-0.1.2

Instance details

Defined in Data.Nat

Methods

universe :: [Nat] Source Github #

Category LEProof Source Github #

The other variant (LEPRoof) isn't Category, because leRefl requires SNat evidence.

Instance details

Defined in Data.Type.Nat.LE.ReflStep

Methods

id :: forall (a :: Nat). LEProof a a Github #

(.) :: forall (b :: Nat) (c :: Nat) (a :: Nat). LEProof b c -> LEProof a b -> LEProof a c Github #

TestEquality SNat Source Github #

Instance details

Defined in Data.Type.Nat

Methods

testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) Github #

Promonad Simplex Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

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

Monoid 'Z Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

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

EqP Fin Source Github #

>>> eqp FZ FZ
True

>>> eqp FZ (FS FZ)
False

>>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
[True,False,False,False,False,False]
[False,True,False,False,False,False]
[False,False,True,False,False,False]
[False,False,False,True,False,False]

Since: fin-0.2.2

Instance details

Defined in Data.Fin

Methods

eqp :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Bool Source Github #

EqP SNat Source Github #

Since: fin-0.2.2

Instance details

Defined in Data.Type.Nat

Methods

eqp :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Bool Source Github #

GNFData SNat Source Github #

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

grnf :: forall (a :: Nat). SNat a -> () Source Github #

GCompare SNat Source Github #

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gcompare :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> GOrdering a b Source Github #

GEq SNat Source Github #

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

geq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) Source Github #

GShow Fin Source Github #

Since: fin-0.2.2

Instance details

Defined in Data.Fin

Methods

gshowsPrec :: forall (a :: Nat). Int -> Fin a -> ShowS Source Github #

GShow SNat Source Github #

Since: fin-0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gshowsPrec :: forall (a :: Nat). Int -> SNat a -> ShowS Source Github #

OrdP Fin Source Github #

>>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
[EQ,LT,LT,LT,LT,LT]
[GT,EQ,LT,LT,LT,LT]
[GT,GT,EQ,LT,LT,LT]
[GT,GT,GT,EQ,LT,LT]

Since: fin-0.2.2

Instance details

Defined in Data.Fin

Methods

comparep :: forall (a :: Nat) (b :: Nat). Fin a -> Fin b -> Ordering Source Github #

OrdP SNat Source Github #

Since: fin-0.2.2

Instance details

Defined in Data.Type.Nat

Methods

comparep :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Ordering Source Github #

MonoidalProfunctor Simplex Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

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

Profunctor Simplex Source Github #

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

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

FunctorForRep Forget Source Github #

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

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

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

Monoid ('S 'Z) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

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

FunctorForRep (Pick a :: OPPOSITE Nat +-> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

fmap :: forall (a0 :: OPPOSITE Nat) (b :: OPPOSITE Nat). (a0 ~> b) -> (Pick a @ a0) ~> (Pick a @ b) Source Github #

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type Unit = 'Z

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (~>) = Simplex

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type InitialObject = 'Z

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type TerminalObject = 'S 'Z

type Ob (a :: Nat) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type Ob (a :: Nat) = IsNat a

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

Instance details

Defined in Proarrow.Category.Instance.Simplex

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

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

Instance details

Defined in Proarrow.Category.Instance.Simplex

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

type UN 'FR ('FR n :: FINREL) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

type UN 'FR ('FR n :: FINREL) = n

type UN 'FS ('FS n :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type UN 'FS ('FS n :: FINSET) = n

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

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

Instance details

Defined in Proarrow.Category.Instance.Simplex

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

type UN ('M :: Nat -> MatK a) ('M n :: MatK a) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Mat

type UN ('M :: Nat -> MatK a) ('M n :: MatK a) = n

type (Pick a :: OPPOSITE Nat +-> Type) @ ('OP n :: OPPOSITE Nat) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (Pick a :: OPPOSITE Nat +-> Type) @ ('OP n :: OPPOSITE Nat) = Vec n a

Orphan instances

Monoidal Nat Source Github #

Addition as monoidal tensor.

Instance details

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

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

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

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

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

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

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

CategoryOf Nat Source Github #

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

Instance details

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

Instance details

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

HasTerminalObject Nat Source Github #

Instance details

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

Monoid 'Z Source Github #

Instance details

Methods

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

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

Monoid ('S 'Z) Source Github #

Instance details

Methods

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

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