Author Archives: Martin Escardo
Can the type of truth values be given the structure of a group?
When attempting to prove a theorem, not discussed in this post, I tried to give a certain set the structure of a group. After failing repeatedly, my proof attempts led me to consider a miniature version of the problem: can … Continue reading
The Cantor-Schröder-Bernstein Theorem for ∞-groupoids
The classical Cantor-Schröder-Bernstein Theorem (CSB) of set theory, formulated by Cantor and first proved by Bernstein, states that for any pair of sets, if there is an injection of each one into the other, then the two sets are in … Continue reading
Introduction to Univalent Foundations of Mathematics with Agda
I am going to teach HoTT/UF with Agda at the Midlands Graduate School in April, and I produced lecture notes that I thought may be of wider use and so I am advertising them here. The source files I used … Continue reading
A self-contained, brief and complete formulation of Voevodsky’s univalence axiom
I have often seen competent mathematicians and logicians, outside our circle, making technically erroneous comments about the univalence axiom, in conversations, in talks, and even in public material, in journals or the web. For some time I was a bit … Continue reading
Homotopy Type Theory 