nLab Herman Geuvers

Selected writings

Selected writings

On mathematical structures formulated in dependent type theory, specifically in Coq:

On constructive analysis with exact real numbers via type theory:

On fixed-point combinators and looping combinators in type theory:

On higher inductive types in homotopy type theory:

On finite sets in homotopy type theory/univalent foundations of mathematics:

category: people

Last revised on February 15, 2023 at 08:16:16. See the history of this page for a list of all contributions to it.