Questions tagged [agda]

For questions regarding Agda: the programming language / proof assistant.

Filter by
Sorted by
Tagged with
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 ...
user avatar
  • 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, ...
user avatar
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 ...
user avatar
  • 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: ...
user avatar
  • 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, ...
user avatar
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 <...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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: ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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. ...
user avatar
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 <...
user avatar
  • 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 ...
user avatar
  • 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
user avatar
  • 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 ...
user avatar
  • 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?
user avatar