## 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.

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.

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.

Original language | English |
---|---|

Title of host publication | CPP 2024 |

Subtitle of host publication | Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs |

Publisher | Association for Computing Machinery (ACM) |

Pages | 246-259 |

Number of pages | 14 |

ISBN (Electronic) | 9798400704888 |

DOIs | |

Publication status | Published - 9 Jan 2024 |

Event | CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs - London, United Kingdom Duration: 15 Jan 2024 → 16 Jan 2024 |

### Conference

Conference | CPP '24 |
---|---|

Abbreviated title | CPP 2024 |

Country/Territory | United Kingdom |

City | London |

Period | 15/01/24 → 16/01/24 |

## Keywords

- formalization of mathematics
- category theory
- double categories
- univalent foundations