# Tag Info

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 ...

4

Yes, equality reflection and $\eta$-rule for functions together imply function extensionality. Recall that equality reflection is the rule $$\frac{\vdash p : \mathsf{Id}_A(a,b)}{\vdash a \equiv b : A}$$ Suppose $A$ is a type, $x : A \vdash B(x)$ is a type over $A$, and $f, g : \prod_{x : A} B(x)$. We claim that function extensionality \textstyle (\prod_{x:...

1

I'll try to explain this without mentioning "K" or "UIP". Here's a proof in Coq -- unfortunately, it uses JMeq_ind (it is supposed to be the eliminator/induction principle of JMeq) which is based on JMeq_eq: Require Import Coq.Logic.JMeq. Definition JMeq_eq2 : forall (A : Type) (x y : A), JMeq x y -> x = y. Proof. intros A x. ...

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