This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
This package just contains the file GirardsParadox.v, which is a formalization of Girards Paradox, and which compiles in versions of Coq which allow “Type in Type”. It should not be seen as part of the UniMath project proper, but is just provided as a record that an inconsistency is formalizable in the present (at the time of this writing) version of UniMath, as will hopefully be impossible in future versions.