It's very well known that formalization of mathematics, logic, programming languages and program verification done within the confines of type theory reveals severe limitations of the hierarchy of equality in it. The minstrels of academia routinely sing us the song of setoid hell and a rare hero fights its consequences with nothing but papers. The more definitionally equal terms we have the easier it gets. Not only we get to write less code, typechecking might even take a little bit less than ages if we use the proof-by-reflection approach. Who cares about proofs? The theory should just decisively squash them together and let us get our subset types without any hassle. But introducing definitionally equal proof terms naïvely is a road to nowhere: we either loose decidability of typechecking or become incompatible with other extensions, especially univalence.
The first act of the talk will introduce and explain the universes of the Coq proof assistant to set the scene for the second act. In the second act we'll get acquainted with a pretty recent experimental addition to the family of Coq's universes, low and behold, our major character -- SProp, a universe of strict propositions. I'll provide a number of examples to illustrate the applicability of SProp, its elimination principles over type, the difference between Sprop and Prop and how all the universes interact.
Speaker: Anton Trunov
1. "Definitional proof-irrelevance without K" - G. Gilbert, J. Cockx, M. Sozeau, N. Tabareau (2019), https://dl.acm.org/doi/10.1145/3290316
2. The Coq Reference Manual: https://coq.github.io/doc/master/refman/addendum/s...
The seminar will be held in google meet on Monday November 2 at 17:30 (google meet room: https://meet.google.com/myu-dhmz-gvu)