Questions tagged [agda]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1
vote
0answers
46 views

Does Type:Type lead to inconsistency without general inductive types?

In e.g. Agda , it is possible to derive an element of the empty type by enabling the "type in type" option. Every proof I have seen (and come up with) involves making a special inductive type ...
3
votes
1answer
42 views

Which inductive schemes can encode the following Agda definition?

Which induction schemes (e.g. induction-recursion by Dybjer and Setzer, "Irish" induction-recursion by McBride or induction-induction by Forsberg and Setzer or perhaps some simpler ones) allow one to ...
1
vote
0answers
67 views

Predecessor function with recursive types

I am defining the type Nat of natural numbers a recursive sum type: $$ Nat = \mu X. Unit \oplus X$$ Now, I have defined zero ...
0
votes
1answer
125 views

Is this statement of P = NP in Agda correct?

Looking for a self-contained statement of P = NP in type theory, I stumbled upon this short Agda formalization (a cleaned up version is reproduced below). The statement here does seem to express the ...
1
vote
2answers
88 views

Propositional truncation of excluded middle

It is clear to me that it should be impossible to prove : exclMidl = isProp A → ((A) ⊎ (¬ A)) Because it would give deciding oracle for every Proposition. My ...
1
vote
0answers
72 views

Strict Positivity of Indexed Datatype in Agda

Agda is ruling out definitions like data Bad : Set where bad : (Bad → Bad) → Bad Because "Non strictly-positive declarations are rejected because one can write ...
6
votes
1answer
205 views

Proof that type does not have decidable equality in Agda

Can one create such function in Agda ? ℕ→ℕ-undecidable : ¬ ( (f g : ℕ → ℕ ) → Dec (f ≡ g)) ℕ→ℕ-undecidable = ? I am particularly interested in proof using ...
2
votes
1answer
93 views

Can one get Turing-completeness without nontermination?

As I'm reading the movfuscator paper by Stephen Dolan, I encounter this claim: In order to have Turing-completeness, we must allow for nontermination. This seems like a reasonable statement. But I'...
2
votes
1answer
181 views

Why this pattern matching fails in Agda?

Consider function wa'' (need natural number definition, either in stdlib or Agda.Builtin.Nat): ...
3
votes
2answers
203 views

In Agda's GADT, is “parameterized” and “indexed” different semantically?

I know they have difference in scoping: data a (n : Set) : Set where introA : a n data b : Set -> Set where introB : {n : Set} -> b n That's not ...
4
votes
1answer
219 views

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

TL;DR: Can I say, "K-rule in Agda enables people to match $ \forall a.a \equiv a $ with $ refl $"? In https://agda.readthedocs.io/en/v2.5.4.1/language/without-k.html#without-k, K-rule is introduced ...