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

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 #

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 #

initiate' :: forall (a' :: Nat) (a :: Nat). (a' ~> 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 #

terminate' :: forall (a :: Nat) (a' :: Nat). (a ~> 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 #

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 #

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 :: k -> Nat -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

tabulate :: forall (b :: Nat) (a :: k). 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 :: k -> Nat -> Type) % 'Z Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

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

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

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (Replicate m :: k -> 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 (a + 'Z) ~ a => 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

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 #

CategoryOf (Simplex j k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Simplex type (~>) = BiSimplex :: Simplex j k -> Simplex j k -> Type

Promonad (BiSimplex :: Simplex j k -> Simplex j k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

id :: forall (a :: Simplex j k). Ob a => BiSimplex a a Source Comments #

(.) :: forall (b :: Simplex j k) (c :: Simplex j k) (a :: Simplex j k). BiSimplex b c -> BiSimplex a b -> BiSimplex a c Source Comments #

Profunctor (BiSimplex :: Simplex j k -> Simplex j k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

Methods

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

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

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type (~>) = BiSimplex :: Simplex j k -> Simplex j k -> Type

type Ob (a :: Simplex j k) Source Comments #

Instance details

Defined in Proarrow.Category.Instance.Simplex

type Ob (a :: Simplex j k) = IsSimplex a

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 => { unForget :: 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)

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 :: k -> Nat -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods index :: forall (a :: k) (b :: Nat). Replicate m a b -> a ~> (Replicate m % b) Source Comments # tabulate :: forall (b :: Nat) (a :: k). 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 :: k -> Nat -> Type) % 'Z Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type (Replicate m :: k -> Nat -> Type) % 'Z = Unit :: k
type (Replicate m :: k -> Nat -> Type) % ('S b :: Nat) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type (Replicate m :: k -> Nat -> Type) % ('S b :: Nat) = m ** (Replicate m % b)

class IsSimplex (s :: Simplex j k) where Source Comments #

Methods

bisimplex :: BiSimplex s s Source Comments #

Instances

Instances details

IsSimplex 'ZZ Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods bisimplex :: BiSimplex 'ZZ 'ZZ Source Comments #
IsSimplex s => IsSimplex ('Y s :: Simplex j ('S y)) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods bisimplex :: BiSimplex ('Y s) ('Y s) Source Comments #
IsSimplex s => IsSimplex ('X s :: Simplex ('S x) ('S y)) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods bisimplex :: BiSimplex ('X s) ('X s) Source Comments #

type family LT (j :: Nat) (k :: Nat) (f :: Simplex j k) (g :: Simplex j k) where ... Source Comments #

Equations

LT 'Z 'Z 'ZZ 'ZZ = ()
LT j ('S k) ('Y f :: Simplex j ('S k)) ('Y g :: Simplex j ('S k)) = LT j k f g
LT ('S j) ('S k) ('X f :: Simplex ('S j) ('S k)) ('X g :: Simplex ('S j) ('S k)) = LT j ('S k) f g

type (<=) (f :: Simplex j k) (g :: Simplex j k) = LT j k f g Source Comments #

data BiSimplex (f :: Simplex j k) (g :: Simplex j k) where Source Comments #

Constructors

ZZZ :: BiSimplex 'ZZ 'ZZ
YYY :: forall {j :: Nat} {k1 :: Nat} (f1 :: Simplex j k1) (g1 :: Simplex j k1). BiSimplex f1 g1 -> BiSimplex ('Y f1) ('Y g1)
XXX :: forall {j1 :: Nat} {y :: Nat} (f1 :: Simplex j1 ('S y)) (g1 :: Simplex j1 ('S y)). BiSimplex f1 g1 -> BiSimplex ('X f1) ('X g1)

Instances

Instances details

Promonad (BiSimplex :: Simplex j k -> Simplex j k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods id :: forall (a :: Simplex j k). Ob a => BiSimplex a a Source Comments # (.) :: forall (b :: Simplex j k) (c :: Simplex j k) (a :: Simplex j k). BiSimplex b c -> BiSimplex a b -> BiSimplex a c Source Comments #
Profunctor (BiSimplex :: Simplex j k -> Simplex j k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex Methods dimap :: forall (c :: Simplex j k) (a :: Simplex j k) (b :: Simplex j k) (d :: Simplex j k). (c ~> a) -> (b ~> d) -> BiSimplex a b -> BiSimplex c d Source Comments # (\\) :: forall (a :: Simplex j k) (b :: Simplex j k) r. ((Ob a, Ob b) => r) -> BiSimplex a b -> r Source Comments #

type family SimplexI :: Simplex i i Source Comments #

Instances

Instances details

type SimplexI Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type SimplexI = 'ZZ
type SimplexI Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type SimplexI = 'X ('Y (SimplexI :: Simplex n n))

type family SimplexO (f :: Simplex i j) (g :: Simplex j k) :: Simplex i k Source Comments #

Instances

Instances details

type SimplexO (f :: Simplex i 'Z) 'ZZ Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type SimplexO (f :: Simplex i 'Z) 'ZZ = f
type SimplexO (f :: Simplex x j) ('Y g :: Simplex j ('S y)) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type SimplexO (f :: Simplex x j) ('Y g :: Simplex j ('S y)) = 'Y (SimplexO f g)
type SimplexO ('Y f :: Simplex i ('S j)) ('X g :: Simplex ('S j) ('S y)) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type SimplexO ('Y f :: Simplex i ('S j)) ('X g :: Simplex ('S j) ('S y)) = SimplexO f g
type SimplexO ('X f :: Simplex ('S x1) ('S x2)) ('X g :: Simplex ('S x2) ('S y)) Source Comments #
Instance details Defined in Proarrow.Category.Instance.Simplex type SimplexO ('X f :: Simplex ('S x1) ('S x2)) ('X g :: Simplex ('S x2) ('S y)) = 'X (SimplexO f ('X g))