Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
10
questions
26
votes
4
answers
1k
views
What are the differences between MLTT and CIC?
In the theory and design of proof assistants based upon dependent types, I feel like there’s a somewhat cultural divide between the "MLTT" world (with Agda as the main representative proof ...
- 5,510
13
votes
1
answer
429
views
Why did Agda give up cumulative universes?
In Ulf Norell's PhD thesis, which is considered the standard reference of the Agda 2 language, the universes are cumulative, say, Set i is not just an instance of <...
- 6,306
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 ...
8
votes
1
answer
282
views
Why is `--irrelevant-projections` unsafe in Agda?
In Agda, irrelevance is an annotation which marks a parameter, record field, or definition which "will only be typechecked but never evaluated", with the consequence that irrelevant ...
- 1,035
7
votes
2
answers
291
views
Proving strict positivity in Agda
In Agda we can prove termination of functions by using well-founded relations, is there a guideline for proving datatype declarations strictly positive, possibly via use of some container techniques ...
- 547
16
votes
2
answers
404
views
What are the upsides and downsides of typed vs untyped conversion?
What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"?
Background
Generally speaking, in dependent type ...
- 394
22
votes
2
answers
407
views
In what intensional type theories can absurdity be made definitionally proof irrelevant?
Various type theories have, over the years, explored extending the definitional equality with a variety of eta-laws and various forms of proof irrelevance.
Quite a lot of systems manage eta for ...
- 771
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,510
6
votes
1
answer
166
views
Does Agda have breaking changes?
Since Agda is software and sometimes software has breaking changes, e.g. Python 2 vs Python 3 (ref), does Agda have any significant breaking changes that one would need to be concerned about?
Also ...
- 2,846
4
votes
1
answer
71
views
When installing Agda does one have to be attentive to a version?
If I want to install Agda do I have to be attentive to versions, breaking changes, etc.?
A comment from an earlier question noted
Agda version for installed libraries
- 2,846