16

There are several possible notions of proof relevance. Let us consider three similar situations: An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(a)$. An element of $\Sigma (x : A) . \|P(x)\|$, where $\|{-}\|$ is propositional truncation, is a pair $(a, q)$ where $a : A$ and $q$ is an equivalence class ...


13

I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know less on this topic than he does - but I was mentioned by name, as was my project. When I gave a talk about agda-categories, I explained one thing about it that ...


8

This is not an answer but a very long comment. I find the idea quite interesting. To keep things focused, I think it would be very good to have a clear idea of what it means for the encoding of cubical type theory to be correct, namely that it is sound and conservative. Soundness just means you can encode everything (for instance, that you did not forget to ...


3

But it does follow. The types $$A = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m)$$ and $$B = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$$ are both contractible. Indeed, they are both inhabited and because $\mathrm{Nat}$ is a set, its identity type is a proposition, hence so are $A$ and $B$, as they are ...


2

Addressing the question in the title: $\mathsf{\lambda n\,m.\,refl}$ is not a proof of commutativity by definition because addition is not a constant function by definition. Of course, the commutativity proof can be shown to be propositionally equal (by a "dependent" equality, or path-over-path) to the $\mathsf{refl}$-returning one, by Andrej's ...


Only top voted, non community-wiki answers of a minimum length are eligible