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.