Experimental library of univalent formalization of mathematics

Abstract

This paper contains a discussion of a library of formalized mathematics for the proof assistant Coq which the author worked on in 2011-13.

References in corpus (1)

• A preliminary univalent formalization of the p-adic numbers

Cited by in corpus (2)

• The HoTT Library: A formalization of homotopy type theory in Coq
• Weakly globular Tamsamani N-categories and their rigidification