Print Email Facebook Twitter Isomorphism is equality Title Isomorphism is equality: A Coq formalisation of the proofs Isomorphism is equality by Coquand and Danielsson Author Greeve, Tiago (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor Ahrens, B.P. (mentor) Wullaert, K.F. (mentor) Yorke-Smith, N. (graduation committee) Degree granting institution Delft University of Technology Programme Computer Science and Engineering Project CSE3000 Research Project Date 2023-06-28 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. Subject Homotopy Type TheoryIsomorphismCoqMartin-Löf Type Theory To reference this document use: http://resolver.tudelft.nl/uuid:09d15517-9c72-404b-b7ff-9bfef67519da Part of collection Student theses Document type bachelor thesis Rights © 2023 Tiago Greeve Files PDF CSE3000_research_paper_Ti ... Greeve.pdf 167.03 KB Close viewer /islandora/object/uuid:09d15517-9c72-404b-b7ff-9bfef67519da/datastream/OBJ/view