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

9

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

8

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.

8

In Agda this is done by tagging types as "irrelevant". It's a kind of quotenting. A function from an irrelevant to a (relevant) type must be constant (and Agda enforces this). You can read more about it on the Agda wiki Irrelevance page.

7

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

Andrej answer covers uses of extraction, but as far as expressiveness goes, I believe that having impredicative Prop leads to a system that is strictly stronger than Agda. In fact "Martin-Löf type theory with universes" is sometimes called "Luo's predicative UTT" One subtle issue is induction-recursion, which gives Agda significant power and seems to be ...

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

3

Here is one article that discussed induction-recursion. Here's their code: data Lang : Set ⟦_⟧ : Lang → Set data Lang where Zero One Two : Lang Pair Fun Tree : (A : Lang) (B : ⟦ A ⟧ → Lang) → Lang ⟦ Zero ⟧ = ⊥ ⟦ One ⟧ = ⊤ ⟦ Two ⟧ = Bool ⟦ Pair A B ⟧ = Σ ⟦ A ⟧ λ a → ⟦ B a ⟧ ⟦ Fun A B ⟧ = (a : ⟦ A ⟧) → ⟦ B a ⟧ ⟦ Tree A B ⟧ = W ⟦ A ⟧ ...

2

You asked several questions. You asked about a type indexed by a list, so you can do this. data DataType (A : Type) (F : A -> Type) : List A -> Type where empty : DataType A F [] _bla_ : forall {xs} {x} -> DataType A F xs -> F x -> DataType A F (x ∷ xs) Where F is a type family that is indexed by the elements of the list. Apart from that, ...

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

Now Agda supports Prop: https://agda.readthedocs.io/en/v2.6.1.3/language/prop.html However, Agda's Prop is predicative and definitionally irrelevant, so it's still not as strong as discussed in Cody's answer. To use it, one needs to supply --prop to Agda. This can be done by adding {-# OPTIONS --prop #-} at the top of an Agda file.

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