Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
70
questions
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
4
votes
2
answers
190
views
Turning off some sProp checks
In Definitional Proof Irrelevance Without K, inductives in sProp need to satisfy three conditions to allow large elimination:
(1) Every non-forced argument must be in sProp.
(2) The return types of ...
- 1,026
4
votes
1
answer
171
views
Why does Agda's `--without-K` option also affect the indices of inductive types, where they have to be of lower levels?
In my understanding, --without-K changes the index unification algorithm so that deletion rules are no longer used, as described in Jesper Cockx' "pattern ...
- 6,316
4
votes
1
answer
73
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
4
votes
1
answer
160
views
Literate Agda: How do I change the size of the displayed code?
I am making Beamer slides for a talk about an Agda formalisation of mine.
In order to make the code fit onto the slide, I need to scale the font size. One would think that this might not be so hard, ...
4
votes
1
answer
111
views
Agda Error after reload when successfully filling a goal
So I'm not sure what this error is and I'm not even sure how I would find out. I'm trying to code up a proof that refl is a right identity. I've gotten to this stage:
...
- 317
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
777
views
3
votes
1
answer
140
views
Can I specify `refl`'s parameter explicitly in Agda?
I'm working on some proofs in Agda that, for educational purposes, explicitly use the path induction principle (which I've defined myself) rather than pattern matching. In the theoretical mathematical ...
- 319
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
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
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
3
votes
1
answer
98
views
Using induction to define Indexed family of HITs in agda
I am looking to define a family of HITs parametrized by $\mathbb{N}$. I want $(-)$-glob : $\mathbb{N} \to Type$, so that $n$-glob is the n-dimensional glob. I know how to construct the n-$glob$ by ...
- 317
3
votes
2
answers
214
views
How do I make use of an irrelevant equality in a proof?
open import Agda.Primitive
import Relation.Binary.PropositionalEquality as Eq
open Eq public
open Eq.≡-Reasoning
Suppose I have a dependent pair whose second ...
- 151
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