Skip to content

Abstracts.2019.Cat.Cubical

Jump to bottom
Fabian edited this page Apr 29, 2020 · 2 revisions

Univalent Categories — A formalization of category theory in Cubical Agda

by Frederik Hanghøj Iversen

Abstract

The usual notion of propositional equality in intensional type-theory is restrictive. For instance it does not admit functional extensionality nor univalence.[2] This poses a severe limitation on both what is provable and the re-usability of proofs. Recent developments have, however, resulted in cubical type theory[3], which permits a constructive proof of univalence. The programming language Agda has been extended with capabilities for working in such a cubical setting.[4] This thesis[1] will explore the usefulness of this extension in the context of category theory. The thesis will motivate the need for univalence and explain why propositional equality in cubical Agda is more expressive than in standard Agda. Alternative approaches to Cubical Agda will be presented and their pros and cons will be explained. As an example of the application of univalence, two formulations of monads will be presented: Namely monads in the monoidal form and monads in the Kleisli form. Using univalence, it will be shown how these are equal. Finally the thesis will explain the challenges that a developer will face when working with cubical Agda and give some techniques to overcome these difficulties. It will suggest how further work can help alleviate some of these challenges.

References

  1. Frederik Hanghøj Iversen. 2018. Univalent Categories — A Formalization of Category Theory in Cubical Agda. Master Thesis, Repository.
  2. The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Book.
  3. Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. 2016. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. Paper.
  4. Andrea Vezzosi, Anders Mörtberg, Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Paper, Documentation, Library.
  5. Anders Mörtberg. 2019. Cubical Methods in Homotopy Type Theory and Univalent Foundations. Lecture Notes.
  6. Agda Github Community. 2019. A New Categories Library for Agda. Repository. This is a rewrite of Daniel Peebles' library, which is based on Stevan Andjelkovic's library (dead link).
  7. Steve Awodey. 2006, 2010. Category Theory. Book.
Clone this wiki locally