Proving Univalence for Generic Higher Structures and Specific Monoids on Sets

Bachelor thesis (2022)

Authors

R. Santana Trejo Electrical Engineering, Mathematics and Computer Science

Contributors

K.F. Wullaert Programming Languages - EEMCS (mentor)
B.P. Ahrens Programming Languages - EEMCS (mentor)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2022 Raul Santana Trejo
More Info
expand_more

Published Date

19-06-2022

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

Type Theory enables mathematicians to perform proofs in a formal language that
computers can understand. This enables computer-assisted proofs and the computerization of all mathematical knowledge. Homotopy Type Theory (HoTT) views types as topological spaces, unlocking new ways to understand and expand Type Theory. One of the most interesting expansions of Type Theory thanks to HoTT has been the development of the Univalence Axiom which expands the definition of "equality between types". This paper analyses the work done in the paper "Isomorphims is Equality"and applies their proof of Univalence for higher structures to two specific monoids on sets. This is done in terminology that is understandable to Computer Scientists with the aim to further the collaboration between the two fields.