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
Related Tags
homotopy-type-theory × 18type-theory × 12
lambda-calculus × 3
ct.category-theory × 3
dependent-type × 3
proof-assistants × 3
reference-request × 2
lo.logic × 2
type-systems × 2
proof-theory × 2
inductive-type × 2
soft-question × 1
boolean-functions × 1
application-of-theory × 1
coq × 1
calculus-of-constructions × 1
modal-logic × 1
equivalence × 1
agda × 1