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
...
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 ...
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 ...
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:
...
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
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 (...
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):
...
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
...
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 ...
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 ...
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 ...
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 ...