Hot answers tagged

21 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(...
Andrej Bauer's user avatar
  • 28.7k
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 ...
Jacques Carette's user avatar
10 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 ...
Dan Doel's user avatar
  • 931
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 :...
Neel Krishnaswami's user avatar
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/...
Jesper's user avatar
  • 356
6 votes
Accepted

Example use cases for induction-recursion

Here is one article that discussed induction-recursion. Here's their code: ...
ice1000's user avatar
  • 965
6 votes
Accepted

Formalization of matching logic (logic behind K Framework)

There is a number of formalizations of matching logic in various proof assistants. I am a co-author of the first one in the following list; thus I have more insight into that one. I am not aware of ...
Jan Tušil's user avatar
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}...
Andrej Bauer's user avatar
  • 28.7k
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] ...
Saizan's user avatar
  • 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 ...
Trebor's user avatar
  • 335
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 ...
cody's user avatar
  • 13.8k
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
gallais's user avatar
  • 635
2 votes

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 ...
ice1000's user avatar
  • 965
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. ...
ice1000's user avatar
  • 965
1 vote

Formalization of matching logic (logic behind K Framework)

I'm currently at the end of my PhD thesis about the interoperability of semantics. That's the reason I'm studying the translation from the semantical framework K into the logical framework Dedukti. ...
Amélie Ledein's user avatar

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