Showing cs.LOShow all
2 papers · 1 filter
cs.LO2021
The Multiverse: Logical Modularity for Proof Assistants
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau +2
Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as first-class…
cs.LO2021
Types are Internal -Groupoids
Antoine Allioux, Eric Finster, Matthieu Sozeau
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode…