Proving Univalence for Generic Higher Structures and Specific Monoids on Sets
R. Santana Trejo (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Kobe Wullaert – Mentor (TU Delft - Programming Languages)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
More Info
expand_more
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.
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.