# Regular Calculi I: Graphical Regular Logic

@inproceedings{Clingman2021RegularCI, title={Regular Calculi I: Graphical Regular Logic}, author={T. Clingman and Brendan Fong and David I. Spivak}, year={2021} }

What is ergonomic syntax for relations? In this first paper in a series of two, to answer the question we define regular calculi: a suitably structured functor from a category representing the syntax of regular logic to the category of posets, that takes each object to the poset of relations on that type. We introduce two major classes of examples, regular calculi corresponding to regular theories, and regular calculi corresponding to regular categories. For working in regular calculi, we… Expand

#### References

SHOWING 1-10 OF 33 REFERENCES

String Diagrams for Regular Logic (Extended Abstract)

- Computer Science, Mathematics
- ACT
- 2019

The syntax and proof rules of regular logic are understood in terms of the free regular category FRg(T) on a set T to show that every natural category has an associated regular calculus, and conversely from every regular calculus one can construct a regular category. Expand

Regular and relational categories: Revisiting 'Cartesian bicategories I'

- Mathematics
- 2019

Regular logic is the fragment of first order logic generated by $=$, $\top$, $\wedge$, and $\exists$. A key feature of this logic is that it is the minimal fragment required to express composition of… Expand

A categorical interpretation of C.S. Peirce's propositional logic Alpha

- Mathematics
- 2000

Abstract C.S. Peirce's graphical system Alpha for propositional logic is given a geometric representation in terms of isotopy classes of planar diagrams, and surgery rules on these diagrams called… Expand

Quotient Completion for the Foundation of Constructive Mathematics

- Mathematics, Computer Science
- Logica Universalis
- 2013

Some tools developed in categorical logic are applied to give an abstract description of constructions used to formalize constructive mathematics in foundations based on intensional type theory, including the exact completion on a category with weak finite limits as an instance. Expand

On Doctrines and Cartesian Bicategories

- Computer Science, Mathematics
- CALCO
- 2021

It is proved that the relationship between cartesian bicategories and a specialisation of Lawvere’s hyperdoctrines, namely elementary existential doctrines, are related by an adjunction, which can be strengthened to an equivalence by imposing further constraints on doctrines. Expand

Adjointness in Foundations

- Computer Science
- 1969

This article sums up a stage of the development of the relationship between category theory and proof theory and shows how already in 1967 category theory had made explicit a number of conceptual advances that were entering into the everyday practice of mathematics. Expand

Regular Categories and Regular Logic

- Computer Science
- 1998

These notes were supposed to give more detailed information about the relationship between regular categories and regular logic than is contained in Jaap van Oosten's script on category theory (BRICS… Expand

Graphical Conjunctive Queries

- Computer Science, Mathematics
- CSL
- 2018

This work introduces the diagrammatic language Graphical Conjunctive Queries (GCQ) and shows that it has the same expressivity as CCQ and derives a model-theoretic completeness theorem of free cartesian bicategories (on a relational signature) for the category of sets and relations. Expand

Monoidal Grothendieck Construction

- Mathematics
- 2018

We lift the standard equivalence between fibrations and indexed categories to an equivalence between monoidal fibrations and monoidal indexed categories, namely weak monoidal pseudofunctors to the… Expand

Hypergraph Categories

- Mathematics, Computer Science
- Journal of Pure and Applied Algebra
- 2019

A coherence theorem for hypergraph categories is proved, which says that every hyper graph category is equivalent to an objectwise-free hypergraph category, and it is proved that the category of objectwise -free hyper graph categories is equivalentTo that end, the goal of this paper is to remove the scare-quotes and make the previous statement precise. Expand