Hot answers tagged

7

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 define every super-elementary function, and all definable functions are super-elementary. The super-elementary functions are level $\mathcal{E}^4$ in the ...


7

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 : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.


6

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/src/full/Agda/Syntax/Internal.hs). It even has an independent typechecker for internal syntax (https://github.com/agda/agda/blob/master/src/full/Agda/...


4

It's easy enough to get the recursion pattern to work with sized types. Hopefully the sharing is preserved through compilation![1] module _ where open import Size open import Data.Nat data BT (i : Size) : Set where Leaf : BT i Branch : ∀ {j : Size< i} → BT j → BT j → BT i record Memo (A : Set) (i : Size) : Set where coinductive field leaf :...


4

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}$$ Suppose $A$ is a type, $x : A \vdash B(x)$ is a type over $A$, and $f, g : \prod_{x : A} B(x)$. We claim that function extensionality $$\textstyle (\prod_{x:...


3

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 extensions of it). The (classical) proof I outlined here applies, crucially using inversion in several places. I believe it's not hard to have a normal proof of $\...


2

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


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