Questions tagged [agda]
For questions regarding Agda: the programming language / proof assistant.
29
questions
4
votes
2
answers
133
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 ...
- 856
8
votes
2
answers
410
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
367
views
Defining coercion for proof irrelevant equality
Say I would like to define coercion for proof irrelevant equality between types. In Coq I try
...
- 1,662
6
votes
1
answer
166
views
Proof of symmetry of universe-polymorphic Leibniz equality in Agda
Consider the following definition of universe-polymorphic Leibniz equality:
...
- 4,136
4
votes
1
answer
90
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, ...
8
votes
1
answer
165
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 <...
- 475
9
votes
2
answers
185
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 ...
- 4,136
5
votes
1
answer
224
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 ...
- 4,136
9
votes
3
answers
766
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 ...
- 325
6
votes
1
answer
170
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 ...
- 475
7
votes
1
answer
87
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 ...
- 325
7
votes
1
answer
105
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 ...
- 475
6
votes
1
answer
122
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 ...
- 893
6
votes
2
answers
76
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:
...
- 128
5
votes
2
answers
90
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 ...
- 325
2
votes
2
answers
124
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 ...
- 141
20
votes
2
answers
240
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 ...
- 721
7
votes
1
answer
131
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 ...
- 497
13
votes
2
answers
166
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 ...
- 356
4
votes
0
answers
202
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,182
7
votes
1
answer
97
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
...
- 4,136
3
votes
1
answer
81
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 ...
- 4,136
24
votes
4
answers
531
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 ...
- 1,881
13
votes
2
answers
219
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. ...
- 303
12
votes
1
answer
246
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 <...
- 4,136
7
votes
1
answer
73
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 ...
- 4,136
4
votes
1
answer
62
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,676
7
votes
1
answer
126
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,676
6
votes
2
answers
207
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?
- 227