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.

To address the challenge of the time-consuming nature of proofreading proofs, computer proof assistants—such as the Coq proof assistant—have been developed. The Univalent Mathematics project aims to formalise mathematics using the Coq proof assistant from a univalent perspective, which is based on homotopy type theory.

The Symmetry book is a textbook about symmetries in mathematics written from a univalent viewpoint. This paper focuses on formalising the proofs in chapter 3 of the Symmetry book using the UniMath Coq library. Currently, the book is partly formalised in the Agda UniMath library. In this paper, we aim to formalise the chapter using the UniMath Coq library to verify its correctness. We have successfully formalised all the theorems in sections 3.1 to 3.3, along some other minor proofs.

This paper focuses on implementing and verifying the proofs presented in ``Finite Sets in Homotopy Type Theory" within the UniMath library. The UniMath library currently lacks support for higher inductive types, which are crucial for reasoning about finite sets in Homotopy Type Theory. This paper addresses that issue and introduces higher inductive types to UniMath. This is used to develop a computer-checked implementation of the proofs within "Finite Sets in Homotopy Type Theory." This implementation enables future research on finite sets in HoTT by providing accessible and reliable proofs.

This paper defines finite sets as Kuratowski-finite. This is in contrast with the most common notion of finiteness, e.g. Bishop-finite and enumerated types. I argue that Kuratowski-finiteness is the most general finite for which the usual operations of finite types and sub-objects can be operated upon.

This report explores the differences in implementations of homotopy type theory using different definitions of finite sets. The expressive ability of homotopy theory is explored when using the newly established definition and implementation of Kuratowski finite sets. This implementation is then compared to that when using the previously established definition and implementation of Bishop finite sets in homotopy type theory. The implementation of finite sets in homotopy type theory is a topic of extensive research. Recent advances have come up with an implementation of Kuratowski-finite sets which promises to be more general and flexible than previously established implementations of finite sets via Bishop-finite sets and enumerated types. This paper will explore examples of types that satisfy Kuratowki-finite notions of finite sets, but not Bishop-finite notions. Through these examples, it will be proven that Kuratowski-finite notions are strictly more flexible than Bishop-finite notions. It will then be proven that by using Kuratowski-notions, the familiar computations involving sets can be used in the same way as with Bishop-finite sets; there is no loss in computational facilities