Isomorphism is equality
A Coq formalisation of the proofs Isomorphism is equality by Coquand and Danielsson
T. Greeve (TU Delft - Electrical Engineering, Mathematics and Computer Science)
B.P. Ahrens – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
K.F. Wullaert – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
N. Yorke-Smith – Graduation committee member (TU Delft - Electrical Engineering, Mathematics and Computer Science)
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
This paper will give a formalisation of proofs, given in the paper "isomorphism is equality", in the proof assistant language Coq. The formalisations will be added to UniMath library. A library containing machine readable proofs in the mathematical field of Homotopy Type theory, a relatively new field which combines Homotopy Theory and Martin-Löf Type Theory. The proofs that have been formalised are the equality pair lemma and the proof that isomorphism is equivalent to equality. We have also constructed a concrete universe on which we defined a notion of isomorphism, as per the same paper.