Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
70
questions
1
vote
1
answer
376
views
Why does Agda use Set instead of Type?
In the 'Hello world' example in Agda — Agda 2.6.5 documentation, it straightforwardly uses Set as follows:
‘Hello world’ in Agda — Agda 2.6.5 documentation
...
- 161
3
votes
0
answers
113
views
Lower bounds in type theory proof assistant with ordinals and universes without axioms
I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024?
My ...
- 279
11
votes
5
answers
2k
views
How do real-world proof assistants bind variables and check equality?
There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc.
There are also ...
6
votes
2
answers
436
views
Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?
I myself have fallen prey to this misconception, i.e., that being dependently typed as in Agda, Coq, etc., implies not being Turing complete, which can be (whether now or previously) found at quite a ...
6
votes
1
answer
102
views
What are the typechecking differences between records and iterated sigma types in Agda?
If we have univalence at hand, the records and iterated sigma versions of some type will be equal. Still, there may be some important typechecking-related differences.
For example, it seems that one ...
- 161
3
votes
2
answers
235
views
Has extensionality ever caused any problems in a mathematical proof?
I read the following about extensionality in PLFA,
Agda does not presume extensionality, but we can postulate that it
holds:
...
- 2,220
3
votes
2
answers
259
views
How to convert Agda's with statement to a helper function?
I read here that
Every use of with is equivalent to defining a helper function
But I couldn't get it working with trying to re-implement a with-clause (which itself came from re-implementing the ...
- 2,220
2
votes
1
answer
54
views
Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?
I am trying to prove the transitivity of <. But I got stuck as the proof found by Auto (...
- 2,220
3
votes
1
answer
395
views
How to provide proof for termination in Agda?
I am trying to write an integer division function from scratch in agda2 (as of 2.6.3):
...
- 2,220
4
votes
2
answers
214
views
Binding variables to terms involving later variables
Consider the following pseudocode in a hypothetical proof assistant:
def f (n : ℕ) : P n
:= match n with
| zero -> ?0
| suc k -> ?1
end
...
- 3,200
6
votes
1
answer
430
views
What are the principal differences between Agda's core type theory and Coq's?
Agda is said to be based on Luo's unifying theory of dependent types while Coq is based on the Calculus of Inductive Constructions. Both of these as I understand it extend the impredicative ...
3
votes
2
answers
156
views
Can Hyperreal exist a axiom-free implementation in HoTT?
The main current implementations of hyperreal numbers are model-theoretic and set-theoretic approaches. Most of these implementations are strongly non-constructive, and many require a very deep ...
- 279
7
votes
1
answer
557
views
Examples of theories where tactic language is required for simple proofs
I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
- 177
7
votes
0
answers
106
views
How to improve/understand typechecking performance in Agda?
I've recently been trying to do some basic formalization of category theory in Agda. As part of this I need to prove a bunch of basic properties around products/monoidal categories. A bunch of these ...
- 171
4
votes
2
answers
321
views
Reasoning about CwFs in a proof assistant
I've been chatting with folks on Mastodon about this but the perspective there is markedly Agda-focused, so I thought I'd ask here for some broader opinions.
What tools/libraries are there for ...
- 971
2
votes
2
answers
144
views
Inspecting proof terms in Agda
In Coq, if I am unsure how a definition foo is defined, I can use the command Print foo. to inspect what ...
- 5,530
3
votes
1
answer
135
views
Cumulativity unsafe in Agda 2.6.3
I've been reading and understand the design choices behind Agda not having a cumulative universe hierarchy by default. However, while tinkering with the language, I've noticed that, at least for Agda ...
- 133
1
vote
1
answer
202
views
When we can use refl?
I am confused with the context related to identity type in HoTT
In particular, for a family $C : (a =_A a) \to U$ dependent on a loop, we cannot apply path induction and consider only the case for $C(...
- 181
3
votes
2
answers
777
views
0
votes
2
answers
88
views
6
votes
2
answers
236
views
Is there a formalism of "coinductive" data types with negative occurrences?
Consider the following program in Haskell:
...
2
votes
1
answer
126
views
How to write if_then_else function that accepts a type argument explicitly?
While this function example works by declaring type A implicitly between brackets,
...
- 123
18
votes
1
answer
1k
views
What are the complex induction patterns supported by Agda?
A question was recently asked on the Coq-club mailing list on Coq rejecting a nastily nested inductive type. We encountered a similar difficulty while trying to port code from Agda to Coq: Agda ...
- 5,530
7
votes
0
answers
195
views
What was the first proof assistant with eta equality for records?
The Agda language supports eta equality for (non-(co)inductive) record types:
...
- 506
8
votes
1
answer
241
views
Termination and confluence -- which goes first?
I'm implementing a version of cubical type theory where the well-definedness of pattern matching functions is implied by:
the well-typedness of the clauses (type check)
the coverage of the patterns (...
- 6,316
23
votes
0
answers
571
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 3,200
1
vote
1
answer
135
views
Agda - Help with importing Haskell function via FFI
I'm trying out Agda's Foreign Function Interface with a simple correctness proof of quicksort (which I have defined in Haskell), but I'm having trouble importing the Haskell function. I've been ...
- 13
9
votes
1
answer
362
views
What are the differences and similarities between records, coinductive records, and codatatypes?
Record types are a common feature in most paradigms.
Agda also allows defining records with the coinductive keyword.
Lastly there are the seemingly more exotic co(...
- 319
5
votes
0
answers
168
views
What are the conditions for Agda to detect that induction-recursion has a least fixed point?
This is a 3rd in a series of questions, spurred by my attempts to encode an argument by Danielsson [1] [2] regarding existence of syntactically non-strictly positive datatype.
The idea (rephrased):
...
- 547
6
votes
1
answer
200
views
Why can termination checker affect strict Prop in Agda?
In https://dl.acm.org/doi/10.1145/3290316 section 4 (which I believe is a standard reference), the authors claimed that Voevodsky's propositional resizing rule justifies the consistency of an ...
- 6,316