### Skapa referens, olika format (klipp och klistra)

**Harvard**

Iversen, F. (2018) *Univalent Categories A formalization of category theory in Cubical Agda*. Göteborg : Chalmers University of Technology

** BibTeX **

@mastersthesis{

Iversen2018,

author={Iversen, Frederik Hanghøj},

title={Univalent Categories A formalization of category theory in Cubical Agda},

abstract={The usual notion of propositional equality in intensional type-theory is restrictive. For instance it
does not admit functional extensionality nor univalence. 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, which permits a constructive proof of univalence. The programming
language Agda has been extended with capabilities for working in such a cubical setting. This
thesis 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.},

publisher={Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola},

place={Göteborg},

year={2018},

note={49},

}

** RefWorks **

RT Generic

SR Electronic

ID 256404

A1 Iversen, Frederik Hanghøj

T1 Univalent Categories A formalization of category theory in Cubical Agda

YR 2018

AB The usual notion of propositional equality in intensional type-theory is restrictive. For instance it
does not admit functional extensionality nor univalence. 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, which permits a constructive proof of univalence. The programming
language Agda has been extended with capabilities for working in such a cubical setting. This
thesis 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.

PB Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola,

LA eng

LK http://publications.lib.chalmers.se/records/fulltext/256404/256404.pdf

OL 30