Hot answers tagged

19 votes
Accepted

Proof relevance vs. proof irrelevance

There are several possible notions of proof relevance. Let us consider three similar situations: An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(...
  • 26.8k
14 votes

Proof relevance vs. proof irrelevance

I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know ...
9 votes
Accepted

Is Church-pentation implementable in Agda?

According to the paper you linked, I think the answer to the question you want to ask is, "no." Pentation is not definable in a stratified version of system F. The paper says that their system can ...
  • 670
8 votes
Accepted

Is there a formalization of normalization of impredicative system F?

Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes. Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S :...
8 votes
Accepted

Small kernel (i.e. proof-verifier) for Agda?

It is true that Agda currently has a much shakier foundation than say Coq or Lean. It does have an internal term syntax that could be seen as a core language (https://github.com/agda/agda/blob/master/...
  • 356
6 votes
Accepted

Extensional type theory and function extensionality

Yes, equality reflection and $\eta$-rule for functions together imply function extensionality. Recall that equality reflection is the rule $$\frac{\vdash p : \mathsf{Id}_A(a,b)}{\vdash a \equiv b : A}...
  • 26.8k
4 votes

How can you build a coinductive memoization table for recursive functions over binary trees?

It's easy enough to get the recursion pattern to work with sized types. Hopefully the sharing is preserved through compilation![1] ...
  • 141
4 votes
Accepted

Is there a way to define dependent types without explicit substitutions internally within agda?

The thing is, the definition is "too" dependent. In order to define the type of substitution or renaming, you need to something like ...
  • 251
4 votes
Accepted

Example use cases for induction-recursion

Here is one article that discussed induction-recursion. Here's their code: ...
  • 923
3 votes
Accepted

Can a term on normal form prove an illogical assertion?

I'll turn my comments into an answer: In general, if you do not have any axioms or "stuck" terms, you cannot have a normal proof of $\mathrm{False}\simeq\forall X:*,X$ in a system like the CoC (or ...
  • 13.3k
2 votes

Pi-type over a list in dependent type theory

You asked several questions. You asked about a type indexed by a list, so you can do this. ...
  • 923
2 votes
Accepted

Formalization of dependent record types/kinds in MLTT or variant thereof?

I do not know how much of the paper it covers but we do have a module based on it in the standard library: https://agda.github.io/agda-stdlib/Data.Record.html
  • 636
1 vote

How to use Prop from UTT in Agda

Now Agda supports Prop: https://agda.readthedocs.io/en/v2.6.1.3/language/prop.html However, Agda's Prop is predicative and ...
  • 923

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