TG
T. Greeve
1 records found
1
Authored
Isomorphism is equality
A Coq formalisation of the proofs Isomorphism is equality by Coquand and Danielsson
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,
...