Univalent Double Categories

Authors

Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North

Type: Article

Publication Date: 2024-01-09

Citations: 0

DOI: https://doi.org/10.1145/3636501.3636955

Ask PDF

Abstract

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.

Locations

arXiv (Cornell University)
View PDF
Research Repository (Delft University of Technology)
View PDF
Radboud Repository (Radboud University)
View PDF

Ask a Question About This Paper

Summary

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

Chat View PDF

Insights From Univalent Foundations: A Case Study Using Double Categories

2024-02-07

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

Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating objects and morphisms, which capture their interactions. It has influenced areas of computer science such as automata theory, functional … Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating objects and morphisms, which capture their interactions. It has influenced areas of computer science such as automata theory, functional programming, and semantics. Certain objects naturally exhibit two classes of morphisms, leading to the concept of a double category, which has found applications in computing science (e.g., ornaments, profunctor optics, denotational semantics). The emergence of diverse categorical structures motivated a unified framework for category theory. However, unlike other mathematical objects, classification of categorical structures faces challenges due to various relevant equivalences. This poses significant challenges when pursuing the formalization of categories and restricts the applicability of powerful techniques, such as transport along equivalences. This work contends that univalent foundations offers a suitable framework for classifying different categorical structures based on desired notions of equivalences, and remedy the challenges when formalizing categories. The richer notion of equality in univalent foundations makes the equivalence of a categorical structure an inherent part of its structure. We concretely apply this analysis to double categorical structures. We characterize and formalize various definitions in Coq UniMath, including (pseudo) double categories and double bicategories, up to chosen equivalences. We also establish univalence principles, making chosen equivalences part of the double categorical structure, analyzing strict double setcategories (invariant under isomorphisms), pseudo double setcategories (invariant under isomorphisms), univalent pseudo double categories (invariant under vertical equivalences) and univalent double bicategories (invariant under gregarious equivalences).

Chat View PDF

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.

Chat View PDF

Univalent Higher Categories via Complete Semi-Segal Types

2018-01-07

Paolo Capriotti , Nicolai Kraus

Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (Ahrens … Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (Ahrens et al. 2015) solves this by considering only truncated types, and it roughly corresponds to an ordinary category. The drawback is that univalent categories fail to capture many naturally occurring structures, such as type universes or the type of univalent categories themselves. This stems from the fact that the natural notion of a category in homotopy type theory is not that of an ordinary, but rather a higher category.

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.

Chat View PDF

Functional bivarieties in functor categories

1975-01-01

E. G. Shul’geifer

Introduction to Homotopy Type Theory

2022-01-01

Egbert Rijke

This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common … This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-L\"of's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.

Chat View PDF

Bicategories in Univalent Foundations

2019-06-01

Benedikt Ahrens , Dan Frumin , Marco Maggesi +1 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 those, we develop the notion of bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. To demonstrate the applicability of this notion, we prove several bicategories are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Our work is formalized in the UniMath library of univalent mathematics.

Introduction to Univalent Foundations of Mathematics with Agda.

2019-11-01

Martı́n Hötzel Escardó

We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-Lof type theory. Agda allows us to … We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-Lof type theory. Agda allows us to write mathematical definitions, constructions, theorems and proofs, for example in number theory, analysis, group theory, topology, category theory or programming language theory, checking them for logical and mathematical correctness. Agda is a constructive mathematical system by default, which amounts to saying that it can also be considered as a programming language for manipulating mathematical objects. But we can assume the axiom of choice or the principle of excluded middle for pieces of mathematics that require them, at the cost of losing the implicit programming-language character of the system. For a fully constructive development of univalent mathematics in Agda, we would need to use its new cubical flavour, and we hope these notes provide a base for researchers interested in learning cubical type theory and cubical Agda as the next step. Compared to most expositions of the subject, we work with explicit universe levels.

Chat View PDF

The Double Category of Paired Dialgebras on the Chu Category

2018-12-18

Aydin Manzouri

The scientific and practical needs of the twenty-first century lead humankind to convergence of the specialized and diverse branches of science and technology. This convergence reveals the need for new … The scientific and practical needs of the twenty-first century lead humankind to convergence of the specialized and diverse branches of science and technology. This convergence reveals the need for new mathematical theories capable of providing common languages and frameworks to be utilized by professionals from different fileds in solving interdisciplinary and challenging problems. The present thesis is done in the same direction. Here, we develop a new formalism with the central idea of unification of various mathematical branches. For this purpose, we utilize three major tools from today's mathematics, each of which possessing a unifying nature itself: category theory and especially the theory of cateogries, the theory of universal dialgebra, and the Chu construction. With the aid of these tools, we define and study a double category that subsumes a significant portion of the formalisms usual within the body of mathematics and theoretical computer science. We show that this double category possesses the properties of self-duality and vertical self-duality. Also, we perform a primary investigation about existence of binary horizontal products and coproducts in this category. Finally, we give some suggestions for future work.

Chat View PDF

Categories and Functors

2017-01-01

Alexey L. Gorodentsev

Categories of Functors

1992-08-27

R. F. C. Walters

A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content. A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.

Directed univalence in simplicial homotopy type theory

2024-07-12

Daniel Gratzer , Jonathan Weinberger , Ulrik Buchholtz

Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics … Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics -- where it allows for synthetic (higher) category theory -- and programming languages -- where it leads to a directed version of the structure identity principle. In this work, we construct the first types in simplicial type theory with non-trivial homomorphisms. We extend simplicial type theory with modalities and new reasoning principles to obtain triangulated type theory in order to construct the universe of discrete types $\mathcal{S}$. We prove that homomorphisms in this type correspond to ordinary functions of types i.e., that $\mathcal{S}$ is directed univalent. The construction of $\mathcal{S}$ is foundational for both of the aforementioned applications of simplicial type theory. We are able to define several crucial examples of categories and to recover important results from category theory. Using $\mathcal{S}$, we are also able to define various types whose usage is guaranteed to be functorial. These provide the first complete examples of the proposed directed structure identity principle.

Chat View PDF

The Double Category of Paired Dialgebras on the Chu Category

2018-01-01

Aydin Manzouri

The scientific and practical needs of the twenty-first century lead humankind to convergence of the specialized and diverse branches of science and technology. This convergence reveals the need for new … The scientific and practical needs of the twenty-first century lead humankind to convergence of the specialized and diverse branches of science and technology. This convergence reveals the need for new mathematical theories capable of providing common languages and frameworks to be utilized by professionals from different fileds in solving interdisciplinary and challenging problems. The present thesis is done in the same direction. Here, we develop a new formalism with the central idea of "unification of various mathematical branches". For this purpose, we utilize three major tools from today's mathematics, each of which possessing a unifying nature itself: category theory and especially the theory of "double cateogries", the theory of "universal dialgebra", and the "Chu construction". With the aid of these tools, we define and study a double category that subsumes a significant portion of the formalisms usual within the body of mathematics and theoretical computer science. We show that this double category possesses the properties of "horizontal self-duality" and "vertical self-duality". Also, we perform a primary investigation about existence of binary horizontal products and coproducts in this category. Finally, we give some suggestions for future work.

Chat View PDF

Functors

2022-09-22

Anil Madhavapeddy , Yaron Minsky

A summary is not available for this content so a preview has been provided. As you have access to this content, a full PDF is available via the ‘Save PDF’ … A summary is not available for this content so a preview has been provided. As you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Chat View PDF

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.

Chat View PDF

Univalent Monoidal Categories

2023-07-28

Kobe Wullaert , Ralph Matthes , Benedikt Ahrens

Chat View PDF

Introduction to Univalent Foundations of Mathematics with Agda

2019-01-01

Martı́n Hötzel Escardó

We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-L\"of type theory. Agda allows us to … We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-L\"of type theory. Agda allows us to write mathematical definitions, constructions, theorems and proofs, for example in number theory, analysis, group theory, topology, category theory or programming language theory, checking them for logical and mathematical correctness. Agda is a constructive mathematical system by default, which amounts to saying that it can also be considered as a programming language for manipulating mathematical objects. But we can assume the axiom of choice or the principle of excluded middle for pieces of mathematics that require them, at the cost of losing the implicit programming-language character of the system. For a fully constructive development of univalent mathematics in Agda, we would need to use its new cubical flavour, and we hope these notes provide a base for researchers interested in learning cubical type theory and cubical Agda as the next step. Compared to most expositions of the subject, we work with explicit universe levels.

Chat View PDF

Categorical structures for type theory in univalent foundations

2017-01-01

Benedikt Ahrens , Peter LeFanu Lumsdaine , Vladimir Voevodsky

In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps … In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.

Chat View PDF

A unified framework for generalized multicategories

2009-01-01

G. S. H. Cruttwell , Michael Shulman

Notions of generalized multicategory have been defined in numerous contexts throughout the literature, and include such diverse examples as symmetric multicategories, globular operads, Lawvere theories, and topological spaces. In each … Notions of generalized multicategory have been defined in numerous contexts throughout the literature, and include such diverse examples as symmetric multicategories, globular operads, Lawvere theories, and topological spaces. In each case, generalized multicategories are defined as the "lax algebras" or "Kleisli monoids" relative to a "monad" on a bicategory. However, the meanings of these words differ from author to author, as do the specific bicategories considered. We propose a unified framework: by working with monads on double categories and related structures (rather than bicategories), one can define generalized multicategories in a way that unifies all previous examples, while at the same time simplifying and clarifying much of the theory.

Chat View PDF

A Categorical Treatment of Ornaments

2013-06-01

Pierre-Évariste Dagand , Conor McBride

Ornaments aim at taming the multiplication of special-purpose data types in dependently typed programming languages. In type theory, purpose is logic. By presenting data types as the combination of a … Ornaments aim at taming the multiplication of special-purpose data types in dependently typed programming languages. In type theory, purpose is logic. By presenting data types as the combination of a structure and a logic, ornaments relate these special-purpose data types through their common structure. In the original presentation, the concept of ornament was introduced concretely for an example universe of inductive families in type theory, but it was clear that the notion was more general. This paper digs out the abstract notion of ornaments in the form of a categorical model. As a necessary first step, we abstract the universe of data types using the theory of polynomial functors. We are then able to characterise ornaments as cartesian morphisms between polynomial functors. We thus gain access to powerful mathematical tools that shall help us understand and develop ornaments. We shall also illustrate the adequacy of our model. Firstly, we rephrase the standard ornamental constructions into our framework. Thanks to its conciseness, we gain a deeper understanding of the structures at play. Secondly, we develop new ornamental constructions, by translating categorical structures into type theoretic artefacts.

Chat View PDF

The lean mathematical library

2020-01-20

The mathlib Community

This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently … This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led to its development.

Chat View PDF

Open Systems: A Double Categorical Perspective

2020-01-01

Kenny Courser

Fong developed `decorated cospans' to model various kinds of open systems: that is, systems with inputs and outputs. In this framework, open systems are seen as the morphisms of a … Fong developed `decorated cospans' to model various kinds of open systems: that is, systems with inputs and outputs. In this framework, open systems are seen as the morphisms of a category and can be composed as such, allowing larger open systems to be built up from smaller ones. Much work has already been done in this direction, but there is a problem: the notion of isomorphism between decorated cospans is often too restrictive. Here we introduce and compare two ways around this problem: structured cospans, and a new version of decorated cospans. Structured cospans are very simple: given a functor $L \colon \mathsf{A} \to \mathsf{X}$, a `structured cospan' is a diagram in $\mathsf{X}$ of the form $L(a) \rightarrow x \leftarrow L(b)$. If $\mathsf{A}$ and $\mathsf{X}$ have finite colimits and $L$ is a left adjoint, there is a symmetric monoidal category whose objects are those of $\mathsf{A}$ and whose morphisms are isomorphism classes of structured cospans. However, this category arises from a more fundamental structure: a symmetric monoidal double category. Under certain conditions this symmetric monoidal double category is equivalent to one built using our new version of decorated cospans. We apply these ideas to symmetric monoidal double categories of open electrical circuits, open Markov processes and open Petri nets.

Chat View PDF

Structured versus Decorated Cospans

2022-09-01

John C. Baez , Kenny Courser , Christina Vasilakopoulou

One goal of applied category theory is to understand open systems. We compare two ways of describing open systems as cospans equipped with extra data. First, given a functor $L … One goal of applied category theory is to understand open systems. We compare two ways of describing open systems as cospans equipped with extra data. First, given a functor $L \colon \mathsf{A} \to \mathsf{X}$, a "structured cospan" is a diagram in $\mathsf{X}$ of the form $L(a) \rightarrow x \leftarrow L(b)$. If $\mathsf{A}$ and $\mathsf{X}$ have finite colimits and $L$ preserves them, it is known that there is a symmetric monoidal double category whose objects are those of $\mathsf{A}$ and whose horizontal 1-cells are structured cospans. Second, given a pseudofunctor $F \colon \mathsf{A} \to \mathbf{Cat}$, a "decorated cospan" is a diagram in $\mathsf{A}$ of the form $a \rightarrow m \leftarrow b$ together with an object of $F(m)$. Generalizing the work of Fong, we show that if $\mathsf{A}$ has finite colimits and $F \colon (\mathsf{A},+) \to (\mathsf{Cat},\times)$ is symmetric lax monoidal, there is a symmetric monoidal double category whose objects are those of $\mathsf{A}$ and whose horizontal 1-cells are decorated cospans. We prove that under certain conditions, these two constructions become isomorphic when we take $\mathsf{X} = \int F$ to be the Grothendieck category of $F$. We illustrate these ideas with applications to electrical circuits, Petri nets, dynamical systems and epidemiological modeling.

Chat View PDF

Double Categories of Open Dynamical Systems (Extended Abstract)

2021-01-19

David Jaz Myers

A (closed) dynamical system is a notion of how things can be, together with a notion of how they may change given how they are. The idea and mathematics of … A (closed) dynamical system is a notion of how things can be, together with a notion of how they may change given how they are. The idea and mathematics of closed dynamical systems has proven incredibly useful in those sciences that can isolate their object of study from its environment. But many changing situations in the world cannot be meaningfully isolated from their environment - a cell will die if it is removed from everything beyond its walls. To study systems that interact with their environment, and to design such systems in a modular way, we need a robust theory of open dynamical systems. In this extended abstract, we put forward a general definition of open dynamical system. We define two general sorts of morphisms between these systems: covariant morphisms which include trajectories, steady states, and periodic orbits; and contravariant morphisms which allow for plugging variables of some systems into parameters of other systems. We define an indexed double category of open dynamical systems indexed by their interface and use a double Grothendieck construction to construct a double category of open dynamical systems. In our main theorem, we construct covariantly representable indexed double functors from the indexed double category of dynamical systems to an indexed double category of spans. This shows that all covariantly representable structures of dynamical systems - including trajectories, steady states, and periodic orbits - compose according to the laws of matrix arithmetic.

Chat View PDF

Bicategories in univalent foundations

2021-11-01

Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 more

Chat View PDF

Framed bicategories and monoidal fibrations

2007-01-01

Michael Shulman

In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or … In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the `morphisms between 0-cells', such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change `nonalgebraically', using categorical fibrations. The resulting `framed bicategories' assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones. We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a `monoidal fibration', meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.

Chat View PDF

Univalent Monoidal Categories

2023-07-28

Kobe Wullaert , Ralph Matthes , Benedikt Ahrens

Chat View PDF