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

8

According to the paper you linked, I think the answer to the question you want to ask is, "no." Pentation is not definable in a stratified version of system F. The paper says that their system can define every super-elementary function, and all definable functions are super-elementary. The super-elementary functions are level $\mathcal{E}^4$ in the ...

7

Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes. Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.

6

It is true that Agda currently has a much shakier foundation than say Coq or Lean. It does have an internal term syntax that could be seen as a core language (https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs). It even has an independent typechecker for internal syntax (https://github.com/agda/agda/blob/master/src/full/Agda/...

4

It's easy enough to get the recursion pattern to work with sized types. Hopefully the sharing is preserved through compilation![1] module _ where open import Size open import Data.Nat data BT (i : Size) : Set where Leaf : BT i Branch : ∀ {j : Size< i} → BT j → BT j → BT i record Memo (A : Set) (i : Size) : Set where coinductive field leaf :...

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

3

I'll turn my comments into an answer: In general, if you do not have any axioms or "stuck" terms, you cannot have a normal proof of $\mathrm{False}\simeq\forall X:*,X$ in a system like the CoC (or extensions of it). The (classical) proof I outlined here applies, crucially using inversion in several places. I believe it's not hard to have a normal proof of \$\...

2

I do not know how much of the paper it covers but we do have a module based on it in the standard library: https://agda.github.io/agda-stdlib/Data.Record.html

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