3 papers
cs.LO2024
On symmetries of spheres in univalent foundations
Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus +1
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form . The case of the circle has a slick answer: th…
cs.LO2016
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic
Robin Adams, Marc Bezem, Thierry Coquand
The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property o…
cs.LO2014
A Vernacular for Coherent Logic
Sana Stojanovic, Julien Narboux, Marc Bezem +1
We propose a simple, yet expressive proof representation from which proofs for different proof assistants can easily be generated. The representation uses only a few inference rule…