New answers tagged homotopy-type-theory
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 ...
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 ...
Top 50 recent answers are included
