My repositories:
Formalization of Quaternionic Calculus in HOL Light
Formalisation of Metric Spaces in HOL Light
Other projects and repositories of code that I contributed to:
UniMath: Univalent mathematics on top of the Coq proof assistant
The HOL Light theorem prover
Universal Algebra in UniMath
My public profiles on social coding sites
My GitHub profile
My Bitbucket profile