Questions tagged [agda]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3 votes
1 answer
117 views

Building non-classical logics in Agda & Coq

Is it possible to construct different systems of logic in Coq or Agda? I ask because I'm interested in using a proof assistant to construct (and verify) theorems in things like many-valued logics, ...
user avatar
2 votes
0 answers
42 views

"Universe-shrinking" function in Agda

Agda does not allow datatypes in one universe to be indexed by, or non-trivially parametrized by a type in a larger universe (strangely, Coq does not appear to require this for propositional ...
user avatar
1 vote
1 answer
81 views

Proving intuitionistic tautologies in Agda

I am to use Agda to prove some intuitionistic tautologies. One of them is the so called Weak Peirce's Law $$ ((((A \rightarrow B) \rightarrow A) \rightarrow A) \rightarrow B) \rightarrow B $$ I ...
user avatar
1 vote
0 answers
43 views

Are Agda's inductive-inductive types safe?

An inductive-inductive definition is a kind of simultaneous inductive definition of a type $A : \mathcal U$ and a type $B : A \to \mathcal U$. I think Agda also lets you extend this idea in all of ...
user avatar
  • 111
2 votes
1 answer
168 views

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

I'm looking to model data inputs for an artificially intelligent system, which is affected by its internal parts and has feedback loops. I'd like to model it mathematically, using category theory or ...
user avatar
  • 21
2 votes
1 answer
62 views

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

An observation when defining List in agda with --without-K enabled: The following parameterized inductive definition is accepted:...
user avatar
  • 191
8 votes
1 answer
312 views

Relationship between inductive families and type-returning functions

Dependently typed languages such as Agda support inductive families, also called indexed datatypes, which allow type parameters to vary between constructors. This can be used to define a set of ...
user avatar
1 vote
2 answers
97 views

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

Suppose I have the following proof: ...
user avatar
2 votes
0 answers
89 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 ...
user avatar
4 votes
1 answer
80 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 ...
user avatar
1 vote
0 answers
132 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 ...
user avatar
0 votes
1 answer
155 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 ...
user avatar
2 votes
2 answers
123 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 ...
user avatar
  • 125
3 votes
0 answers
160 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 ...
user avatar
  • 125
7 votes
1 answer
343 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 ...
user avatar
  • 125
2 votes
1 answer
177 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'...
user avatar
  • 121
2 votes
1 answer
300 views

Why this pattern matching fails in Agda?

Consider function wa'' (need natural number definition, either in stdlib or Agda.Builtin.Nat): ...
user avatar
  • 888
7 votes
2 answers
465 views

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

I know they have different scoping: data a (n : Set) : Set where introA : a n data b : Set -> Set where introB : {n : Set} -> b n That's not what I'...
user avatar
  • 888
5 votes
1 answer
360 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 $ \mathit{refl} $"? In https://agda.readthedocs.io/en/v2.5.4.1/language/without-k.html#without-k, K-...
user avatar
  • 888