Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 18:30 - 18:45 at CPP - Logic, Set Theory, and Category Theory Chair(s): Yannick Forster

The generality and pervasiness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain the ones we picked. In particular, we find that alternative definitions or alternative proofs from those found in standard textbooks can be advantageous, as well as “fit” Agda’s type theory more smoothly. Some definitions regarded as equivalent in standard textbooks turn out to make different “universe level” assumptions, with some being more polymorphic than others. We also pay close attention to engineering issues so that the library integrates well with Agda’s own standard library, as well as being compatible with as many of supported type theories in Agda as possible.

Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 18:45: Logic, Set Theory, and Category TheoryCPP at CPP
Chair(s): Yannick ForsterSaarland University

Streamed session: https://youtu.be/U_ZT9hfDAUQ

18:00 - 18:15
Talk
An Anti-Locally-Nameless Approach to Formalizing Quantifiers
CPP
Olivier LaurentCNRS & ENS Lyon
Pre-print Media Attached
18:15 - 18:30
Talk
The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
CPP
Dominik KirstSaarland University, Felix RechSaarland University
Pre-print Media Attached
18:30 - 18:45
Talk
Formalizing Category Theory in Agda
CPP
Jason Z.S. HuMcGill University, Jacques CaretteMcMaster University
Pre-print Media Attached