Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Instance.Simplex

Documentation

data Nat Source Comments #

Constructors

Z
S Nat

Instances

Instances details

Monoidal Nat Source Comments #

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

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

leftUnitor :: forall (a :: Nat). Obj a -> ((Unit :: Nat) ** a) ~> a Source Comments #

leftUnitorInv :: forall (a :: Nat). Obj a -> a ~> ((Unit :: Nat) ** a) Source Comments #

rightUnitor :: forall (a :: Nat). Obj a -> (a ** (Unit :: Nat)) ~> a Source Comments #

rightUnitorInv :: forall (a :: Nat). Obj a -> a ~> (a ** (Unit :: Nat)) Source Comments #

associator :: forall (a :: Nat) (b :: Nat) (c :: Nat). Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) Source Comments #

associatorInv :: forall (a :: Nat) (b :: Nat) (c :: Nat). Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) Source Comments #

CategoryOf Nat Source Comments #

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). Obj 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). Obj 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 #

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 #

Profunctor Forget Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

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

Representable 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

index :: forall a (b :: Nat). Forget a b -> a ~> (Forget % b) Source Comments #

tabulate :: forall (b :: Nat) a. Ob b => (a ~> (Forget % b)) -> Forget a b Source Comments #

repMap :: forall (a :: Nat) (b :: Nat). (a ~> b) -> (Forget % a) ~> (Forget % b) Source Comments #

Monoid m => Profunctor (Replicate m :: j -> Nat -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

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

Monoid m => Representable (Replicate m :: j -> Nat -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

index :: forall (a :: j) (b :: Nat). Replicate m a b -> a ~> (Replicate m % b) Source Comments #

tabulate :: forall (b :: Nat) (a :: j). Ob b => (a ~> (Replicate m % b)) -> Replicate m a b Source Comments #

repMap :: 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 :: j -> Nat -> Type) % 'Z Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (Replicate m :: j -> Nat -> Type) % 'Z = Unit :: j

type (Replicate m :: j -> Nat -> Type) % ('S b :: Nat) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (Replicate m :: j -> Nat -> Type) % ('S b :: Nat) = m ** (Replicate m % b)

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

Constructors

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

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

singNat' :: forall (a :: Nat). Obj a -> SNat a Source Comments #

singObj :: forall (a :: Nat). SNat a -> Obj a Source Comments #

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

Constructors

Z :: 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 #
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 #

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 Forget a (b :: Nat) where Source Comments #

Constructors

Forget
Fields :: forall (b :: Nat) a. Ob b => { getForget :: a -> Fin b } -> Forget a b

Instances

Instances details

Profunctor Forget Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

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

Representable 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

index :: forall a (b :: Nat). Forget a b -> a ~> (Forget % b) Source Comments #

tabulate :: forall (b :: Nat) a. Ob b => (a ~> (Forget % b)) -> Forget a b Source Comments #

repMap :: 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)

rightUnitor' :: forall (b :: Nat). SNat b -> Simplex (b + 'Z) b Source Comments #

rightUnitorInv' :: forall (b :: Nat). SNat b -> Simplex b (b + 'Z) Source Comments #

associator' :: forall (a :: Nat) (b :: Nat) (c :: Nat). SNat a -> SNat b -> Obj c -> Simplex ((a + b) + c) (a + (b + c)) Source Comments #

associatorInv' :: forall (a :: Nat) (b :: Nat) (c :: Nat). SNat a -> SNat b -> Obj c -> Simplex (a + (b + c)) ((a + b) + c) Source Comments #

data Replicate (m :: k) (a :: k) (b :: Nat) where Source Comments #

Constructors

Replicate :: forall {k} (b :: Nat) (a :: k) (m :: k). Ob b => (a ~> (Replicate m % b)) -> Replicate m a b

Instances

Instances details

Monoid m => Profunctor (Replicate m :: j -> Nat -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods dimap :: forall (c :: j) (a :: j) (b :: Nat) (d :: Nat). (c ~> a) -> (b ~> d) -> Replicate m a b -> Replicate m c d Source Comments # (\\) :: forall (a :: j) (b :: Nat) r. ((Ob a, Ob b) => r) -> Replicate m a b -> r Source Comments #
Monoid m => Representable (Replicate m :: j -> Nat -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods index :: forall (a :: j) (b :: Nat). Replicate m a b -> a ~> (Replicate m % b) Source Comments # tabulate :: forall (b :: Nat) (a :: j). Ob b => (a ~> (Replicate m % b)) -> Replicate m a b Source Comments # repMap :: forall (a :: Nat) (b :: Nat). (a ~> b) -> (Replicate m % a) ~> (Replicate m % b) Source Comments #
type (Replicate m :: j -> Nat -> Type) % 'Z Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type (Replicate m :: j -> Nat -> Type) % 'Z = Unit :: j
type (Replicate m :: j -> Nat -> Type) % ('S b :: Nat) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type (Replicate m :: j -> Nat -> Type) % ('S b :: Nat) = m ** (Replicate m % b)