Hot answers tagged

10 votes
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 ...
user avatar
8 votes

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 ...
user avatar
  • 28.4k
6 votes
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. ...
user avatar
5 votes

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 ...
user avatar
  • 28.4k
4 votes
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 ...
user avatar
  • 2,135
4 votes
Accepted

Why this pattern matching fails in Agda?

First, let's desugar the withs. First definition: ...
user avatar
  • 156
4 votes
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 ...
user avatar
3 votes
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 ...
user avatar
  • 2,135
3 votes

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. ...
user avatar
3 votes

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 ...
user avatar
  • 28.4k
3 votes
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. ...
user avatar
  • 2,135
3 votes
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: ...
user avatar
  • 2,135
3 votes

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 ...
user avatar
  • 29.2k
3 votes
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 ...
user avatar
  • 236
3 votes
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 ...
user avatar
  • 29.2k
2 votes

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

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