# Tag Info

Accepted

### Proof that type does not have decidable equality in Agda

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

### In Agda's GADT, are "parameterized" and "indexed" different semantically?

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 ...
• 28.4k
Accepted

### Building non-classical logics in Agda & Coq

You can define many non-classical logics in Coq (and I assume Agda too), even if they are incompatible with the logic of your proof assistant, but you need to define the concept of inference yourself. ...
• 176

### Is this statement of P = NP in Agda correct?

The definition is not correct. It states that a machine is polynomial time (the field poly in poly-time-machine) when its ...
• 28.4k
Accepted

### In Agda's GADT, are "parameterized" and "indexed" different semantically?

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 ...
• 2,135
Accepted

### Why this pattern matching fails in Agda?

First, let's desugar the withs. First definition: ...
• 156
Accepted

### Which inductive schemes can encode the following Agda definition?

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

### Proving transitivity in an intuitionistic type theory without the K rule

$\newcommand{\J}{\mathsf{J}} \newcommand{\K}{\mathsf{K}} \newcommand{\refl}{\mathsf{refl}}$ Yes, this just uses axiom $\J$. $\K$ is only necessary for translating certain particular cases of pattern ...
• 2,135

### Relationship between inductive families and type-returning functions

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

### Interpreting a proof of $2^\mathbb{N}$ being uncountable

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 ...
• 28.4k
Accepted

### Interpreting a proof of $2^\mathbb{N}$ being uncountable

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. ...
• 2,135
Accepted

### Proving intuitionistic tautologies in Agda

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: ...
• 2,135

### Which would be better for programming using Homotopy type theory Agda or Idris

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 ...
• 29.2k
Accepted

### Propositional truncation of excluded middle

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 ...
• 236
Accepted

### What does it mean if we disable K-rule in Agda?

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 ...
• 29.2k

### Can one get Turing-completeness without nontermination?

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

### Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda

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 ...
• 2,135
1 vote

### Propositional truncation of excluded middle

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 ...
• 2,135

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