Questions tagged [agda]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0
votes
2answers
70 views

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

Suppose I have the following proof: ...
1
vote
0answers
50 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
48 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
89 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
127 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
92 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 ...
2
votes
0answers
84 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
219 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
99 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
196 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
228 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
232 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 ...