The Formal Theory of Monads, Univalently

2025-02-19

Niels van der Weide

We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of … We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal to a bicategory, and prove that it is univalent. We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects. Finally, we relate monads and adjunctions in arbitrary bicategories. Our work is formalized in Coq using the UniMath library.

View PDF Chat

Towards a Formal Theory of Graded Monads

2016-01-01

Soichiro Fujii , Shin-ya Katsumata , Paul-André Melliès

Univalent Monoidal Categories

2022-01-01

Kobe Wullaert , Ralph Matthes , Benedikt Ahrens

Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. … Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study them in a univalent setting. Specifically, we show that the bicategory of univalent monoidal categories is univalent. Furthermore, we construct a Rezk completion for monoidal categories: we show how any monoidal category is weakly equivalent to a univalent monoidal category, universally. We have fully formalized these results in UniMath, a library of univalent mathematics in the Coq proof assistant.

View PDF Chat

Univalent Monoidal Categories

2023-07-28

Kobe Wullaert , Ralph Matthes , Benedikt Ahrens

Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. … Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study them in a univalent setting. Specifically, we show that the bicategory of univalent monoidal categories is univalent. Furthermore, we construct a Rezk completion for monoidal categories: we show how any monoidal category is weakly equivalent to a univalent monoidal category, universally. We have fully formalized these results in UniMath, a library of univalent mathematics in the Coq proof assistant.

View PDF Chat

The formal theory of monads II

2002-11-01

Stephen Lack , Ross Street

The graphical theory of monads

2025-01-01

Ralf Hinze , Dan Marsden

Abstract The formal theory of monads shows that much of the theory of monads can be developed in the abstract at the level of 2-categories. This means that results about … Abstract The formal theory of monads shows that much of the theory of monads can be developed in the abstract at the level of 2-categories. This means that results about monads can be established once and for all and simply instantiated in settings such as enriched category theory. Unfortunately, these results can be hard to reason about as they involve more abstract machinery. In this paper, we present the formal theory of monads in terms of string diagrams — a graphical language for 2-categorical calculations. Using this perspective, we show that many aspects of the theory of monads, such as the Eilenberg–Moore and Kleisli resolutions of monads, liftings, and distributive laws, can be understood in terms of systematic graphical calculational reasoning. This paper will serve as an introduction both to the formal theory of monads and to the use of string diagrams, in particular, their application to calculations in monad theory.

The internal languages of univalent categories

2024-11-10

Niels van der Weide

Internal language theorems are fundamental in categorical logic, since they express an equivalence between syntax and semantics. One of such theorems was proven by Clairambault and Dybjer, who corrected the … Internal language theorems are fundamental in categorical logic, since they express an equivalence between syntax and semantics. One of such theorems was proven by Clairambault and Dybjer, who corrected the result originally by Seely. More specifically, they constructed a biequivalence between the bicategory of locally Cartesian closed categories and the bicategory of democratic categories with families with extensional identity types, $\sum$-types, and $\prod$-types. This theorem expresses that the internal language of locally Cartesian closed is extensional Martin-L\"of type theory with dependent sums and products. In this paper, we study the theorem by Clairambault and Dybjer for univalent categories, and we extend it to various classes of toposes, among which are $\prod$-pretoposes and elementary toposes. The results in this paper have been formalized using the proof assistant Coq and the UniMath library.

View PDF Chat

Eilenberg–Moore Monoids and Backtracking Monad Transformers

2016-04-01

Maciej Piróg

We develop an algebraic underpinning of backtracking monad transformers in the general setting of monoidal categories. As our main technical device, we introduce Eilenberg--Moore monoids, which combine monoids with algebras … We develop an algebraic underpinning of backtracking monad transformers in the general setting of monoidal categories. As our main technical device, we introduce Eilenberg--Moore monoids, which combine monoids with algebras for strong monads. We show that Eilenberg--Moore monoids coincide with algebras for the list monad transformer ('done right') known from Haskell libraries. From this, we obtain a number of results, including the facts that the list monad transformer is indeed a monad, a transformer, and an instance of the MonadPlus class. Finally, we construct an Eilenberg--Moore monoid of endomorphisms, which, via the codensity monad construction, yields a continuation-based implementation a la Hinze.

View PDF Chat

Bicategories in univalent foundations

2021-11-01

Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 more

We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples … We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

View PDF Chat

Strong functors and monoidal monads

1972-12-01

Anders Kock

Induction, Coinduction, and Fixed Points in Order Theory, Set Theory, (PL) Type Theory, Logic, and Category Theory: A Concise Survey (and Tutorial)

2018-12-25

Moez A. AbdelGawad

In this survey article (which hitherto is an ongoing work-in-progress) we present the formulation of the induction and coinduction principles using the language and conventions of each of order theory, … In this survey article (which hitherto is an ongoing work-in-progress) we present the formulation of the induction and coinduction principles using the language and conventions of each of order theory, set theory, programming languages' type theory, first-order logic, and category theory, for the purpose of examining some of the similarities and, more significantly, the dissimilarities between these various mathematical disciplines, and hence shed some light on the precise relation between these disciplines. Towards that end, in this article we discuss plenty of related concepts, such as fixed points, pre-fixed points, post-fixed points, inductive sets and types, coinductive sets and types, algebras and coalgebras. We conclude the survey by hinting at the possibility of a more abstract and unified treatment that uses concepts from category theory such as monads and comonads.

Monads Need Not Be Endofunctors

2010-01-01

Thorsten Altenkirch , James Chapman , Tarmo Uustalu

View PDF Chat

Bicategories in Univalent Foundations

2019-03-04

Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 more

We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples … We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories, we develop the notion of `displayed bicategories', an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-category is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

Monads need not be endofunctors

2015-03-06

Thosten Altenkirch , James Chapman , Tarmo Uustalu

We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We … We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We show that the Kleisli and Eilenberg-Moore constructions carry over to relative monads and are related to relative adjunctions. Under reasonable assumptions, relative monads are monoids in the functor category concerned and extend to monads, giving rise to a coreflection between relative monads and monads. Arrows are also an instance of relative monads.

View PDF Chat

Monads and their Eilenberg-Moore algebras in functional analysis

1973-01-01

Zbigniew Semadeni

Induction, Coinduction, and Fixed Points: A Concise Survey (and Tutorial)

2018-12-25

Moez A. AbdelGawad

In this survey article (which hitherto is an ongoing work-in-progress) we present the formulation of the induction and coinduction principles using the language and conventions of each of order theory, … In this survey article (which hitherto is an ongoing work-in-progress) we present the formulation of the induction and coinduction principles using the language and conventions of each of order theory, set theory, programming languages' type theory, first-order logic, and category theory, for the purpose of examining some of the similarities and, more significantly, the dissimilarities between these various mathematical disciplines, and hence shed some light on the precise relation between these disciplines. Towards that end, in this article we discuss plenty of related concepts, such as fixed points, pre-fixed points, post-fixed points, inductive sets and types, coinductive sets and types, algebras and coalgebras. We conclude the survey by hinting at the possibility of a more abstract and unified treatment that uses concepts from category theory such as monads and comonads.

Univalent Double Categories

2023-01-01

Niels van der Weide , Nima Rasekh , Benedikt Ahrens +1 more

Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of … Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for example in functional programming. Double categories are a natural generalization of categories which incorporate the data of two separate classes of morphisms, allowing a more nuanced representation of relationships and interactions between objects. Similar to category theory, double categories have been successfully applied to various situations in mathematics and computer science, in which objects naturally exhibit two types of morphisms. Examples include categories themselves, but also lenses, petri nets, and spans. While categories have already been formalized in a variety of proof assistants, double categories have received far less attention. In this paper we remedy this situation by presenting a formalization of double categories via the proof assistant Coq, relying on the Coq UniMath library. As part of this work we present two equivalent formalizations of the definition of a double category, an unfolded explicit definition and a second definition which exhibits excellent formal properties via 2-sided displayed categories. As an application of the formal approach we establish a notion of univalent double category along with a univalence principle: equivalences of univalent double categories coincide with their identities

View PDF Chat

Induction, Coinduction, and Fixed Points: A Concise Survey

2018-12-25

Moez A. AbdelGawad

In this survey article (which hitherto is an ongoing work-in-progress) we present the formulation of the induction and coinduction principles using the language and conventions of each of order theory, … In this survey article (which hitherto is an ongoing work-in-progress) we present the formulation of the induction and coinduction principles using the language and conventions of each of order theory, set theory, programming languages' type theory, first-order logic, and category theory, for the purpose of examining some of the similarities and, more significantly, the dissimilarities between these various mathematical disciplines, and hence shed some light on the precise relation between these disciplines. Towards that end, in this article we discuss plenty of related concepts, such as fixed points, pre-fixed points, post-fixed points, inductive sets and types, coinductive sets and types, algebras and coalgebras. We conclude the survey by hinting at the possibility of a more abstract and unified treatment that uses concepts from category theory such as monads and comonads.

Implementing a category-theoretic framework for typed abstract syntax

2022-01-11

Benedikt Ahrens , Ralph Matthes , Anders Mörtberg

In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof … In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant. In the present work, we describe what was necessary to generalize that work to account for simply-typed languages. First, some definitions had to be generalized to account for the natural appearance of non-endofunctors in the simply-typed case. As it turns out, in many cases our mechanized results carried over to the generalized definitions without any code change. Second, an existing mechanized library on $\omega$-cocontinuous functors had to be extended by constructions and theorems necessary for constructing multi-sorted syntax. Third, the theoretical framework for the semantical signatures had to be generalized from a monoidal to a bicategorical setting, again to account for non-endofunctors arising in the typed case. This uses actions of endofunctors on functors with given source, and the corresponding notion of strong functors between actions, all formalized in UniMath using a recently developed library of bicategory theory. We explain what needed to be done to plug all of these ingredients together, modularly. The main result of our work is a general construction that, when fed with a signature for a simply-typed language, returns an implementation of that language together with suitable boilerplate code, in particular, a certified monadic substitution operation.

View PDF Chat

From Signatures to Monads in UniMath

2018-07-11

Benedikt Ahrens , Ralph Matthes , Anders Mörtberg

The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent … The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it—in particular, general inductive types are not part of the system. In this work, we partially remedy the lack of inductive types by constructing some set-level datatypes and their associated induction principles from other type constructors. This involves a formalization of a category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the datatypes obtained. We also connect this construction to a previous formalization of substitution for languages with variable binding. Altogether, we construct a framework that allows us to concisely specify, via a simple notion of binding signature, a language with variable binding. From such a specification we obtain the datatype of terms of that language, equipped with a certified monadic substitution operation and a suitable recursion scheme. Using this we formalize the untyped lambda calculus and the raw syntax of Martin-Löf type theory.

View PDF Chat

The Formal Theory of Monads, Univalently

Authors

Abstract

Locations

Ask a Question About This Paper

Summary