Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
49
questions
2
votes
1
answer
42
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
10
votes
1
answer
428
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 ...
- 3,230
7
votes
0
answers
137
views
What was the first proof assistant with eta equality for records?
The Agda language supports eta equality for (non-(co)inductive) record types:
...
- 421
6
votes
1
answer
160
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 (...
- 5,424
22
votes
0
answers
443
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 ...
- 2,832
1
vote
1
answer
90
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
6
votes
1
answer
122
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(...
- 237
5
votes
0
answers
105
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):
...
- 497
5
votes
1
answer
160
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 ...
- 5,424
5
votes
1
answer
140
views
How to convince Agda that definition is terminating in the presence of unapplied recursion?
In the following, termination check fails for Df:
...
1
vote
0
answers
159
views
Descriptions of heterogenous datatypes
When attempting to describe the datatype as appearing in my previous question, using indexed descriptions in style of The Gentle Art of Levitation to describe this datatype (using Agda for examples):
<...
- 497
7
votes
2
answers
235
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 ...
- 497
1
vote
1
answer
148
views
Does Agda's --injective-type-constructors flag have canonicity?
Since 2010/01/07, when the Anti-classicality of Agda was proved by Chung-Kil Hur, Agda's --injective-type-constructors is separated from the main branch of Agda (...
- 109
3
votes
1
answer
79
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 ...
- 237
5
votes
1
answer
146
views
Application of `SSet` in Agda
Is there any presentable work that makes essential use of SSet in Agda? I kind of get the theory, but I'm not sure about the practical value of this. The ...
- 3,261
3
votes
1
answer
86
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 ...
- 305
5
votes
1
answer
149
views
Strictly-monotone "max" operation for constructive Brouwer-trees?
The Setting
I'm trying to use Agda's well-founded ordering to prove that something is terminating using Brouwer Trees i.e.
...
- 653
3
votes
1
answer
93
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:
...
- 305
5
votes
2
answers
157
views
Agda: Cannot Instantiate Metavariable
I'm running into a certain error while trying to code something up in cubical Agda, but I can't understand the error. Here is my code:
...
- 305
9
votes
2
answers
222
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:
...
- 305
4
votes
2
answers
155
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 ...
- 906
8
votes
2
answers
485
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, ...
9
votes
2
answers
412
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,051
6
votes
1
answer
198
views
Proof of symmetry of universe-polymorphic Leibniz equality in Agda
Consider the following definition of universe-polymorphic Leibniz equality:
...
- 5,424
4
votes
1
answer
117
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, ...
9
votes
1
answer
238
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 <...
- 653
9
votes
2
answers
240
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 ...
- 5,424
5
votes
1
answer
290
views
What subtyping rules does Agda support?
Andrea Vezzosi said Cubical Agda made cubical subtyping coercion-based (inS and outS) because it's a bad idea to introduce more ...
- 5,424
10
votes
3
answers
939
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
6
votes
1
answer
221
views
Parameterized Datatypes in a Universe à la Tarski?
I'm wondering, is there a way to make a Universe à la Tarski that models all of the types in an open type theory, where there can be user defined parameterized inductive types?
For context, I'm trying ...
- 653
7
votes
1
answer
101
views
Decidability for an infinite sequence of decidable propositions
I've been trying to prove this in Agda:
lemma : (P : ℕ → Set)
→ ((n : ℕ) → Dec (P n))
→ Dec (Σ[ n ∈ ℕ ] ¬ (P n))
In words: We have an infinite sequence of ...
- 345
8
votes
1
answer
126
views
Are `P x` and `▸ ((next P) ⊛ (next x))` equivalent in Guarded Cubical Agda?
In Guarded Cubical Agda there's ▹_ : Set i → Set i and ▸_ : ▹ Set i → Set i.
If I've got ...
- 653
8
votes
1
answer
209
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 ...
- 983
6
votes
2
answers
90
views
Can I use if_then_else on indexed paths in HITs?
I want to define a function out of an indexed higher inductive type, and am running into some problems.
Here is a somewhat contrived minimal example of what I'm doing:
...
- 160
6
votes
2
answers
104
views
Data constructors and universe constraints
In the code below:
data Foo₁ : Set where
foo₁ : Set → Foo₁
data Foo₂ (A : Set) : Set where
foo₂ : Foo₂ A
type₂ : {A : Set} → Foo₂ A
type₂ = foo₂
for the ...
- 345
3
votes
2
answers
142
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
21
votes
2
answers
304
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 ...
- 751
7
votes
1
answer
174
views
When should I use `no-eta-equality` in Agda records?
In a recent development, I used the no-eta-equality attribute on a record. The motivation in that case was ad hoc: I noticed that I'd get better metavariable ...
- 601
15
votes
2
answers
294
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 ...
- 384
6
votes
0
answers
217
views
Can Agda proofs be trusted and do they conform to a specific, well-defined type theory?
When using Agda proofs, how can you know whether to trust it? Also, do they conform to a specific, well-defined type theory?
Credit
- 1,258
8
votes
1
answer
118
views
Is it possible to define `fib` coinductive stream w/o sized types?
In Agda with --guardedness, we can define productive definitions using copatterns like the following
...
- 5,424
4
votes
1
answer
104
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 ...
- 5,424
24
votes
4
answers
770
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 ...
- 3,230
13
votes
2
answers
292
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. ...
- 331
11
votes
1
answer
318
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 <...
- 5,424
7
votes
1
answer
100
views
How to state and prove the associativity of append of sized vectors with homogeneous equality?
Append (denoted ++) for sized vectors is obviously associative, i.e. a ++ (b ++ c) = (a ++ b) ++ c for ...
- 5,424
4
votes
1
answer
65
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,796
6
votes
1
answer
146
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,796
6
votes
2
answers
449
views
How to run Agda?
I want to run Agda, but I do not know how to run functions. I need to run "Hello, World!"; how can I do this?
- 235