Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
69
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
23
votes
0
answers
570
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
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
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
15
votes
2
answers
417
views
In Agda, why is universe polymorphism explicit?
I've noticed that the process of coding a definition in Agda that is universe polymorphic usually requires little thought in how the Level parameters are specified. ...
- 361
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 ...
10
votes
2
answers
1k
views
Constructive proof of strong normalization for simply typed lambda calculus
I'm reading Girard's Proofs and Types, and in section 4.4 he writes:
Lemma: t is strongly normalisable iff there is a number ...
- 345
9
votes
2
answers
325
views
What's the benefit of having pi and sigma types with an invariant parameter?
Ulf Norell wrote this in his PhD thesis (figure 1.6):
This contradicts my stereotype on pi & sigma types, where pi parameter should be contravariant and sigma parameter is covariant. Why is Agda ...
- 6,306
9
votes
2
answers
467
views
Defining coercion for proof irrelevant equality
Say I would like to define coercion for proof irrelevant equality between types. In Coq I try
...
- 2,290
9
votes
2
answers
252
views
How to access local definitions in Agda
I'm working in cubical agda. I am wondering how to access local definitions once outside of the local environment. For example, suppose I have the following code:
...
- 317
9
votes
1
answer
348
views
Case splitting with quotient types in Cubical Agda
I'm getting started with Cubcal Agda and I'm quite confused.
I've got a HIT A defined, with a path constructor eq returning <...
- 921
9
votes
1
answer
358
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
8
votes
2
answers
685
views
Curly Braces and Lambdas in Agda
The docs on lambdas in Agda provide two forms of lambda: a curly brace based version, and the where syntax. But while writing some programs, I stumbled across a third version: one pattern, no braces, ...
