index.md

Index

Formalizations and Examples

Formalizations that are listed as Haskell structures are a formalization of that structure in the category Set reflecting the way it is encoded in Haskell.

Formalization	Module
Haskell Functor	Haskell.Functor
Haskell Applicative	Haskell.Applicative
Haskell Monad	Haskell.Monad
Haskell Graded Applicative	Haskell.Parameterized.Graded.Applicative
Haskell Graded Monad	Haskell.Parameterized.Graded.Monad
Haskell Indexed Applicative	Haskell.Parameterized.Indexed.Applicative
Haskell Indexed Monad	Haskell.Parameterized.Indexed.Monad
Category	Theory.Category.Definition
Monoidal Category	Theory.Category.Monoidal
Functor	Theory.Functor.Definition
Monoidal Functor	Theory.Functor.Monoidal
Lax Monoidal Functor	Theory.Functor.Monoidal
Graded Lax Monoidal Functor	Theory.Haskell.Parameterized.Graded.LaxMonoidalFunctor
Indexed Lax Monoidal Functor	Theory.Haskell.Parameterized.Indexed.LaxMonoidalFunctor
Monad	Theory.Monad.Definition
Graded Monad	Theory.Haskell.Parameterized.Graded.Monad
Indexed Monad	Theory.Haskell.Parameterized.Indexed.Monad
Kleisli Triple	Theory.Monad.Kleisli
Relative Monad	Theory.Monad.Relative
Atkey's Parameterized Monad	Theory.Monad.Atkey
Natural Transformation	Theory.Natural.Transformation
Natural Isomorphism	Theory.Natural.Isomorphism
Strict 2-Category	Theory.TwoCategory.Definition
Bicategory	Theory.TwoCategory.Bicategory
Lax 2-Functor (on Strict 2-Categories)	Theory.TwoFunctor.Definition
Lax 2-Functor (constant 0-Cell mapping)	Theory.TwoFunctor.ConstZeroCell
Monoid	Theory.Monoid

Relationships

An isomorphism or implication between structures listed here just indicates that there are cases where these implications hold, but they are not necessarily generally true.

Legend:

• A ≅ B -- Proof that A isomorphic to B.
• A ⇒ B -- Proof that A implies an instance of B. Can be interpreted as A is a subset of B.

Index:

• Atkey's Parameterized Monad ⇒ Lax 2-Functor
• Atkey's Parameterized Monad ≅ Haskell Indexed Monad
• Functor ≅ Haskell Functor
• Functor ⇒ Lax 2-Functor
• Graded Lax Monoidal Functor ≅ Haskell Graded Applicative
• Graded Monad ≅ Haskell Graded Monad
• Graded Monad ≅ Lax 2-Functor
• Indexed Lax Monoidal Functor ≅ Haskell Indexed Applicative
• Indexed Lax Monoidal Functor ≅ Graded Lax Monoidal Functor
• Indexed Monad ≅ Haskell Indexed Monad
• Indexed Monad ≅ Lax 2-Functor
• Indexed Monad ≅ Graded Monad
• Lax Monoidal Functor ≅ Graded Lax Monoidal Functor
• Lax Monoidal Functor ≅ Indexed Lax Monoidal Functor
• Lax Monoidal Functor ≅ Graded Monad
• Lax Monoidal Functor ≅ Monad
• Lax Monoidal Functor ≅ Haskell Applicative
• Lax Monoidal Functor ≅ Haskell Graded Applicative
• Lax Monoidal Functor ≅ Haskell Graded Monad
• Lax Monoidal Functor ≅ Lax 2-Functor
• Monad ≅ Haskell Monad
• Monad ≅ Lax 2-Functor