# Tag Info

## Hot answers tagged agda

Accepted

• 31.8k
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
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

### 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
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
Accepted

### Example use cases for induction-recursion

Here is one article that discussed induction-recursion. Here's their code: ...
• 923
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

### 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
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