Safe Haskell	Safe-Inferred
Language	Haskell2010

Hask.Category.Polynomial

Contents

Synopsis

Product Category

data Product p q a b Source

Constructors

Product (p (Fst a) (Fst b)) (q (Snd a) (Snd b))

Instances

(Category k p, Category k1 q, ProductOb k k1 p q a) => Functor ((,) k k) * (Product k k p q a)
(Category k p, Category k1 q) => Functor ((,) k k) ((,) k k -> *) (Product k k p q)
(Category k p, Category k1 q) => Category' ((,) k k) (Product k k p q)
type Dom ((,) k k1) * (Product k k1 p q a) = Product k k1 (Dom2 k * k p) (Dom2 k1 * k1 q)
type Cod ((,) k k1) * (Product k k1 p q a) = (->)
type Dom ((,) k k1) ((,) k k1 -> ) (Product k k1 p q) = Op ((,) k k1) (Product k k1 (Opd k (k -> ) p) (Opd k1 (k1 -> *) q))
type Cod ((,) k k1) ((,) k k1 -> ) (Product k k1 p q) = Nat ((,) k k1) (Product k k1 (Dom2 k * k p) (Dom2 k1 * k1 q)) (->)
type Ob ((,) k k1) (Product k k1 p q) = ProductOb k k1 p q

class (Ob p (Fst a), Ob q (Snd a)) => ProductOb p q a Source

Instances

(Ob i p (Fst i j a), Ob j q (Snd j i a)) => ProductOb i j p q a

type family Fst p :: i Source

Instances

type Fst k1 k ((,) k1 k a b) = a

type family Snd q :: j Source

Instances

type Snd k1 k ((,) k k1 a b) = b

Coproduct Category

data Coproduct c d a b where Source

Constructors

Inl :: c x y -> Coproduct c d (Left x) (Left y)
Inr :: d x y -> Coproduct c d (Right x) (Right y)

Instances

(Category k p, Category k1 q) => Functor (Either k k) * (Coproduct k k p q a)
(Category k p, Category k1 q) => Functor (Either k k) (Either k k -> *) (Coproduct k k p q)
(Category k p, Category k1 q) => Category' (Either k k) (Coproduct k k p q)
type Dom (Either k k1) * (Coproduct k k1 p q a) = Coproduct k k1 p q
type Cod (Either k k1) * (Coproduct k k1 p q a) = (->)
type Dom (Either k k1) (Either k k1 -> *) (Coproduct k k1 p q) = Op (Either k k1) (Coproduct k k1 p q)
type Cod (Either k k1) (Either k k1 -> ) (Coproduct k k1 p q) = Nat (Either k k1) (Coproduct k k1 p q) (->)
type Ob (Either k k1) (Coproduct k k1 p q) = CoproductOb k k1 p q

class CoproductOb p q a where Source

Methods

side :: Endo (Coproduct p q) a -> (forall x. (a ~ Left x, Ob p x) => r) -> (forall y. (a ~ Right y, Ob q y) => r) -> r Source

Instances

(Category j q, Ob j q y) => CoproductOb i j p q (Right i j y)
(Category i p, Ob i p x) => CoproductOb i j p q (Left i j x)

Constructors

Instances

Functor k * (Unit k k a)
FullyFaithful k * (Unit k k a)
Category' k (Unit k k)
Functor k (k -> *) (Unit k k)
FullyFaithful k (k -> *) (Unit k k)
type Dom k1 * (Unit k k1 a) = Unit k1 k1
type Cod k1 * (Unit k k1 a) = (->)
type Ob k (Unit k k) = Vacuous k (Unit k k)
type Dom k (k1 -> *) (Unit k k1) = Op k (Unit k k)
type Cod k (k1 -> ) (Unit k k1) = Nat k1 (Unit k1 k1) (->)

data Void :: *

A logically uninhabited data type.

Instances

Eq Void
Data Void
Ord Void
Read Void	Reading a `Void` value is always a parse error, considering `Void` as a data type with no constructors.
Show Void
Ix Void
Generic Void
Exception Void
Hashable Void
Semigroup Void
Typeable * Void
Comonoid' * Either Void
Cosemigroup * Either Void
Monoid' * Either Void
Semigroup * Either Void
Semigroup * (,) Void
type Rep Void = D1 D1Void (C1 C1_0Void (S1 NoSelector (Rec0 Void)))

Since Void values logically don't exist, this witnesses the logical reasoning tool of "ex falso quodlibet".