* HoTT library
@ 2016-10-25 19:23 Bas Spitters
0 siblings, 0 replies; only message in thread
From: Bas Spitters @ 2016-10-25 19:23 UTC (permalink / raw)
To: homotopytypetheory
We wrote up our formalization work:
The HoTT Library: A formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman,
Matthieu Sozeau, Bas Spitters
https://arxiv.org/abs/1610.04591
We report on the development of the HoTT library, a formalization
of homotopy type theory in the Coq proof assistant. It formalizes most
of basic homotopy type theory, including univalence, higher inductive
types, and significant amounts of synthetic homotopy theory, as well
as category theory and modalities. The library has been used as a
basis for several independent developments. We discuss the decisions
that led to the design of the library, and we comment on the
interaction of homotopy type theory with recently introduced features
of Coq, such as universe polymorphism and private inductive types.
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2016-10-25 19:23 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2016-10-25 19:23 HoTT library Bas Spitters
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).