# Tag Info

10

ℕ→ℕ-undecidable is not provable in Agda. If we postulate the law of excluded middle (LEM), it follows that equality on every set is decidable, contradicting ℕ→ℕ-undecidable. Since Agda is consistent with LEM, it follows that ℕ→ℕ-undecidable is not provable in base Agda. This holds the same for cubical and vanilla Agda.

7

The following explanation lacks mathematicial precision but should explain what is going on. A GADT is a special case of a recursive type. A recursive type $T$ is a solution of a type equation of the form $$T = \Phi(T).$$ (If this is not clear, please ask.) Sometimes $\Phi$ depends on a parameter $p : P$ of some given type $P$, so we have a parameterized ...

5

The definition is not correct. It states that a machine is polynomial time (the field poly in poly-time-machine) when its running time is below the exponential function $n \mapsto 2^n$ (the definition is-poly). This would allow, for example, a running time $n \mapsto 1.5^n$, which isn not poly-time according to the accepted definition.

4

Yes and no. The obvious difference is that indexed types are able to vary in the result type of each constructor. So you can do: data T : ℕ → Set where t : T 5 You can do this with a parameterized type by taking an argument: data T (n : ℕ) : Set where t : n ≡ 5 → T n But ≡ is itself an indexed type, so you need something indexed at the bottom (≡ can ...

4

First, let's desugar the withs. First definition: wa''-aux : ∀ m n -> n + m ≡ m + n -> wa (m + n) ≡ wa (n + m) wa''-aux m n refl = ? -- cannot unify n + m with m + n wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m) wa'' m n = wa''-aux m n (comm n m) Second definition: wa''-aux : ∀ m n w -> w ≡ m + n -> wa (m + n) ≡ wa w wa''-aux m n .(m + n) refl ...

4

No scheme that I know of directly encodes that type. Sometimes it's called a "nested" inductive definition. The complication here is that Maybe and List are type constructors which are external to the signature, and we have to formalize strict positivity for external type operators in general, if we want to allow such definitions. In other words, the ...

3

For examples like this, they can often by easily written interactively just looking for the only thing possible to do at each stage. So for instance, you start with: wp e = ? and the only option is to apply e, at which point Agda will tell you you need to provide $((A → B) → A) → A$, so you introduce a lambda: wp e = e (λ k -> ?) Now you need to give an ...

3

Agda is definitely the better choice if you're doing Homotopy Type Theory. Idris has several features that are specifically incompatible with HoTT. Specifically, you can use dependent pattern matching to prove Uniqueness of Identity Proofs (UIP), which, when combined with Univalence, allows you to prove False. There's also a type-case feature which you can ...

3

Agda has an interpretation in classical set theory, as well as in realizability models. Any proof carried out in Agda is valid in any of these models. It can therefore be interpreted in classical set theory to give a proof of uncountability of $2^\mathbb{N}$, but it can also be interpreted in the effective topos to give a proof of computable uncountability ...

3

There is no assumption in your proof that the functions involved are computable, so it would be quite stingy to interpret the proof that way merely because Agda allows you to compute with its terms. Rather, yes how it should be interpreted depends on the model, and constructive (in the sense of just removing axioms) proofs like the one you've given enable an ...

3

The only way to prove ∥ X ∥ is to prove X (unless you admit some other axiom). So, assuming P is a proposition, there is no way to prove ∥ ((A) ⊎ (¬ A)) ∥ if you cannot prove ((A) ⊎ (¬ A)). It is not a correct intuition that undecidable propositions are either true or false, just we do not know about it. A formal system S with an undecidable proposition P ...

3

Axiom K is related to "Uniqueness of Identity Proofs", which says is that any two proofs of equality are themselves equal to each other (i.e. are both Refl). Agda doesn't include K as an axiom, but it (and UIP) can be proved as a theorem using Agda's dependent pattern matching. Axiom K is inconsistent with homotopy type theory, where the univalence axiom ...

2

Many total languages, including Agda and Coq, allow you to define coinductive data types. These model infinite objects, like infinite lists. Obviously, a function producing an infinite list cannot terminate. However, it must, in a total language, be productive. This means that any finite prefix of the produced infinite list can be computed in finite time. ...

2

As mentioned by Andrej, this is an instance of transporting along an equivalence of families and display maps. In this specific case, we have an equivalence of graphs and relations. open import Function open import Data.Product open import Relation.Binary.PropositionalEquality open import Level renaming (zero to lzero; suc to lsuc) -- type of relations on a ...

1

Normally, Agda does an analysis to determine that your indexed type is equivalent to a parameterized type. Essentially, since A occurs in the result type, knowing that l : List A tells you what type A is 'stored' in the value l. The value is known, which means that tricks that involve embedding a universe into a small type within said universe to cause a ...

1

Another thing you should know is that those truncations don't hide anything. For instance, it is relatively simple to prove the lemma: $$\mathsf{isProp}\ A → \mathsf{isProp}\ (A \uplus ¬ A)$$ which means that we can extract the evidence from $\| A \uplus ¬A \|$. I think the same is true of the $A \equiv \mathsf{Unit}$ version, because all types involved ...

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