Questions tagged [agda]

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

Filter by
Sorted by
Tagged with
3 votes
2 answers
187 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: ...
tinlyx's user avatar
  • 2,034
3 votes
2 answers
232 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 ...
tinlyx's user avatar
  • 2,034
2 votes
1 answer
44 views

Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?

I am trying to prove the transitivity of <. But I got stuck as the proof found by Auto (...
tinlyx's user avatar
  • 2,034
3 votes
1 answer
364 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): ...
tinlyx's user avatar
  • 2,034
4 votes
2 answers
190 views

Binding variables to terms involving later variables

Consider the following pseudocode in a hypothetical proof assistant: def f (n : ℕ) : P n := match n with | zero -> ?0 | suc k -> ?1 end ...
Mike Shulman's user avatar
  • 3,040
6 votes
1 answer
261 views

What are the principal differences between Agda's core type theory and Coq's?

Agda is said to be based on Luo's unifying theory of dependent types while Coq is based on the Calculus of Inductive Constructions. Both of these as I understand it extend the impredicative ...
Patrick Nicodemus's user avatar
2 votes
2 answers
134 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 ...
Ember Edison's user avatar
6 votes
1 answer
532 views

Examples of theories where tactic language is required for simple proofs

I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
uhbif19's user avatar
  • 167
7 votes
0 answers
93 views

How to improve/understand typechecking performance in Agda?

I've recently been trying to do some basic formalization of category theory in Agda. As part of this I need to prove a bunch of basic properties around products/monoidal categories. A bunch of these ...
Eric Dobson's user avatar
4 votes
2 answers
311 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 ...
Joey Eremondi's user avatar
2 votes
2 answers
118 views

Inspecting proof terms in Agda

In Coq, if I am unsure how a definition foo is defined, I can use the command Print foo. to inspect what ...
Meven Lennon-Bertrand's user avatar
3 votes
1 answer
124 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 ...
Evaristo's user avatar
  • 133
1 vote
1 answer
181 views

When we can use refl?

I am confused with the context related to identity type in HoTT In particular, for a family $C : (a =_A a) \to U$ dependent on a loop, we cannot apply path induction and consider only the case for $C(...
maplgebra's user avatar
  • 181
3 votes
2 answers
775 views

How to prove f x < f y → x ≢ y

...
maplgebra's user avatar
  • 181
0 votes
2 answers
88 views

Proof of state updating

My code is ...
maplgebra's user avatar
  • 181
6 votes
2 answers
222 views

Is there a formalism of "coinductive" data types with negative occurrences?

Consider the following program in Haskell: ...
Sebastian Graf's user avatar
2 votes
1 answer
100 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, ...
Pandemonium's user avatar
15 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 ...
Meven Lennon-Bertrand's user avatar
7 votes
0 answers
190 views

What was the first proof assistant with eta equality for records?

The Agda language supports eta equality for (non-(co)inductive) record types: ...
Jesper's user avatar
  • 486
8 votes
1 answer
221 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 (...
ice1000's user avatar
  • 6,144
21 votes
0 answers
550 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 ...
Mike Shulman's user avatar
  • 3,040
1 vote
1 answer
127 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 ...
Caleb Kisby's user avatar
8 votes
1 answer
299 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(...
aradarbel10's user avatar
5 votes
0 answers
160 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): ...
Ilk's user avatar
  • 547
5 votes
1 answer
191 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 ...
ice1000's user avatar
  • 6,144
5 votes
1 answer
212 views

How to convince Agda that definition is terminating in the presence of unapplied recursion?

In the following, termination check fails for Df: ...
TerminationCheckFailed's user avatar
1 vote
0 answers
176 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): <...
Ilk's user avatar
  • 547
7 votes
2 answers
279 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 ...
Ilk's user avatar
  • 547
1 vote
1 answer
241 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 (...
Ember Edison's user avatar
3 votes
1 answer
124 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 ...
aradarbel10's user avatar
5 votes
1 answer
181 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 ...
Trebor's user avatar
  • 3,867
3 votes
1 answer
97 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 ...
IsAdisplayName's user avatar
5 votes
1 answer
172 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. ...
Joey Eremondi's user avatar
4 votes
1 answer
106 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: ...
IsAdisplayName's user avatar
5 votes
2 answers
228 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: ...
IsAdisplayName's user avatar
9 votes
2 answers
247 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: ...
IsAdisplayName's user avatar
4 votes
2 answers
177 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 ...
ionchy's user avatar
  • 1,026
8 votes
2 answers
646 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, ...
Olek Gierczak's user avatar
9 votes
2 answers
450 views

Defining coercion for proof irrelevant equality

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try ...
Couchy's user avatar
  • 2,211
6 votes
1 answer
215 views

Proof of symmetry of universe-polymorphic Leibniz equality in Agda

Consider the following definition of universe-polymorphic Leibniz equality: ...
ice1000's user avatar
  • 6,144
4 votes
1 answer
148 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, ...
Astra Kolomatskaia's user avatar
9 votes
1 answer
329 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 <...
Joey Eremondi's user avatar
9 votes
2 answers
310 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 ...
ice1000's user avatar
  • 6,144
5 votes
1 answer
373 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 ...
ice1000's user avatar
  • 6,144
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 ...
Itai Zukerman's user avatar
6 votes
1 answer
248 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 ...
Joey Eremondi's user avatar
7 votes
1 answer
146 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 ...
Itai Zukerman's user avatar
8 votes
1 answer
153 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 ...
Joey Eremondi's user avatar
8 votes
1 answer
269 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 ...
James Martin's user avatar
  • 1,015
6 votes
2 answers
101 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: ...
Åsmund Kløvstad's user avatar