Skip to main content
23 votes
Accepted

What are the complex induction patterns supported by Agda?

I try to write about what's supported in Agda and the semantics that we have (or don't have) for it. Disclaimers: I'm not an expert on the relevant parts of the Agda source code, I mostly write here ...
András Kovács's user avatar
22 votes

What are the differences between MLTT and CIC?

I do not think I would align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it ...
Neel Krishnaswami's user avatar
18 votes

What are the differences between MLTT and CIC?

The short answer is: $\mathbf{MLTT}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, $\mathbf{0}$, $\mathbf{1}$, $\mathbf{2}$, $\mathbf{W}$, and $\mathbf{CiC}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, ...
Namdak Tönpa's user avatar
18 votes
Accepted

How to run Agda?

Given that you arrived here "having no idea" how to run it, the easiest might be: Install Visual Studio Code Install banacorn.agda-mode package in Visual ...
Andrej Bauer's user avatar
  • 9,593
17 votes
Accepted

Constructive proof of strong normalization for simply typed lambda calculus

As Dan Doel says in the comments, the reason Kőnig's lemma is used is that Girard's definition of strong normalization is constructively too weak. It's defined as the non-existence of infinite ...
András Kovács's user avatar
15 votes
Accepted

In Agda, why is universe polymorphism explicit?

First of all, you may simplify your code with the keyword: ...
ice1000's user avatar
  • 6,276
14 votes
Accepted

Why did Agda give up cumulative universes?

One reason (not particularly specific to Agda) might be that eta reduction is not compatible with cumulativity. With cumulativity (that is $Set_0 \leq Set_1$), and given \begin{align*} f &:= \...
Couchy's user avatar
  • 2,271
13 votes

In what intensional type theories can absurdity be made definitionally proof irrelevant?

If you are happy to have your False live in a separate sort, then you can do this with strict propositions in Coq (and any other system that have those, which I ...
Meven Lennon-Bertrand's user avatar
12 votes

What are the differences between MLTT and CIC?

The technical answers are correct, but they completely overlook the philosophical differences between the two formalisms. Martin-Löf type theory closely reflects Arendt Heyting's explanations of the ...
Lawrence Paulson's user avatar
11 votes

What are the differences between MLTT and CIC?

Apart from judgmental equality, MLTT and CIC also differ in the following: The existence of an impredicative universe. CIC has Prop, and that's what makes it a part of the lambda cube. This universe ...
ice1000's user avatar
  • 6,276
11 votes

What are the upsides and downsides of typed vs untyped conversion?

From the perspective of implementation of conversion checking, it really depends on the specific setting. For vanilla intuitionistic type theories without more exotic features (like cubical TT, ...
András Kovács's user avatar
10 votes
Accepted

What subtyping rules does Agda support?

The current subtyping rules that Agda uses are for sized types (when --sized-types is enabled) and cumulativity (when ...
Jesper's user avatar
  • 506
10 votes
Accepted

Termination and confluence -- which goes first?

As you have noticed there is no "natural" way to prove confluence and termination: to prove confluence from local confluence you need termination, but proving termination often depends on ...
Jesper's user avatar
  • 506
9 votes
Accepted

Is it possible to define `fib` coinductive stream w/o sized types?

I recommend the state machine definition that we'd use for looping over Fibonacci numbers: ...
András Kovács's user avatar
9 votes
Accepted

Decidability for an infinite sequence of decidable propositions

This is equivalent to solving the Halting Problem (perhaps relativized to an oracle), so this is a very strong assumption. Fix a Turing machine M, suppose P n is ...
François G. Dorais's user avatar
8 votes

In what intensional type theories can absurdity be made definitionally proof irrelevant?

I think the paper you're looking for is Definitional Proof Irrelevance Without K (I seem to remember that there was some sort of snag in Agda, but I can't for the life of me remember what it was.) ...
Joey Eremondi's user avatar
8 votes
Accepted

Why is `--irrelevant-projections` unsafe in Agda?

--irrelevant-projections can be used to prove the irrelevance axiom mentioned in the Agda manual: ...
James Martin's user avatar
  • 1,035
8 votes
Accepted

What's the benefit of having pi and sigma types with an invariant parameter?

There are subtleties here, when type annotations are present, depending in quite a brittle way on where they must be placed. (I'm half-remembering conversations about this with Zhaohui Luo.) Suppose ...
pigworker's user avatar
  • 771
8 votes
Accepted

Curly Braces and Lambdas in Agda

The key thing about "pattern" lambda is that it's a fake: each such thing elaborates as the local invocation of a new (i.e., generative) top-level helper function. The type declaration for ...
pigworker's user avatar
  • 771
8 votes

How do real-world proof assistants bind variables and check equality?

Variables λΠ uses the Bindlib library, and so do several other systems, see the paper Abstract Representation of Binders in OCaml using the Bindlib Library and package documentation. I have recently ...
7 votes

In Agda, why is universe polymorphism explicit?

In Agda, universe levels are not only explicit but they are also first class. This means that you can store them in data structures and compute with them. This allows you to write generic programs in ...
gallais's user avatar
  • 1,256
7 votes
Accepted

Does Agda have breaking changes?

It has tons of breaking changes. For example, if they've found an inconsistency, they'll try to restrict some features, so code surely breaks. For instance, they used to have a special treatment for ...
ice1000's user avatar
  • 6,276
7 votes
Accepted

Data constructors and universe constraints

foo₁ gives a type error because the type of constructors* should live in the same type as that of the inductive type. That is, Foo₁ is declared to live in Set₀, while the constructor's type Set₀ → Foo₁...
ionchy's user avatar
  • 1,026
7 votes

Constructive proof of strong normalization for simply typed lambda calculus

For a modern take on the proof, you can have a look at POPLmark Reloaded. The paper's appendix explains in great details what the (sometimes technical) proofs are. The paper comes with various ...
gallais's user avatar
  • 1,256
7 votes
Accepted

Case splitting with quotient types in Cubical Agda

It means that your implementation of the squash case, let's call it u (where u may refer to i...
ice1000's user avatar
  • 6,276
7 votes
Accepted

Why can termination checker affect strict Prop in Agda?

After some research I have found a counterexample by Jesper Cockx: ...
ice1000's user avatar
  • 6,276
7 votes
Accepted

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

Sure: you can use the fact that _<_ is irreflexive to derive a contradiction from the assumption that both f x < f y and <...
gallais's user avatar
  • 1,256
7 votes
Accepted

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

I will answer the headline question and ignore UTT (I believe thinking of Agda as UTT causes more confusion than it solves). There are very many differences between the theories Agda and Coq implement,...
James Wood's user avatar
  • 1,053
7 votes

Binding variables to terms involving later variables

Great question Mike! Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently,...
James McKinna's user avatar
7 votes

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

[Supplemental: I rewrote the answer so that any shred of vagueness is gone, as it was evoking religuous zeal, and I would prefer to stick to math. Everything is explained in terms of a widely accepted ...
Andrej Bauer's user avatar
  • 9,593

Only top scored, non community-wiki answers of a minimum length are eligible