ℕ→ℕ-undecidable is not provable in Agda. If we postulate the law of excluded middle (LEM), it follows that equality on every set is decidable, contradicting ℕ→ℕ-undecidable. Since Agda is consistent with LEM, it follows that ℕ→ℕ-undecidable is not provable in base Agda. This holds the same for cubical and vanilla Agda.
The following explanation lacks mathematicial precision but should explain what is going on.
A GADT is a special case of a recursive type. A recursive type $T$ is a solution of a type equation of the form
$$T = \Phi(T).$$
(If this is not clear, please ask.)
Sometimes $\Phi$ depends on a parameter $p : P$ of some given type $P$, so we have a parameterized ...
First, let's desugar the withs.
wa''-aux : ∀ m n -> n + m ≡ m + n -> wa (m + n) ≡ wa (n + m)
wa''-aux m n refl = ? -- cannot unify n + m with m + n
wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m)
wa'' m n = wa''-aux m n (comm n m)
wa''-aux : ∀ m n w -> w ≡ m + n -> wa (m + n) ≡ wa w
wa''-aux m n .(m + n) refl ...
The definition is not correct. It states that a machine is polynomial time (the field poly in poly-time-machine) when its running time is below the exponential function $n \mapsto 2^n$ (the definition is-poly). This would allow, for example, a running time $n \mapsto 1.5^n$, which isn not poly-time according to the accepted definition.
Yes and no.
The obvious difference is that indexed types are able to vary in the result type of each constructor. So you can do:
data T : ℕ → Set where
t : T 5
You can do this with a parameterized type by taking an argument:
data T (n : ℕ) : Set where
t : n ≡ 5 → T n
But ≡ is itself an indexed type, so you need something indexed at the bottom (≡ can ...
Axiom K is related to "Uniqueness of Identity Proofs", which says is that any two proofs of equality are themselves equal to each other (i.e. are both Refl). Agda doesn't include K as an axiom, but it (and UIP) can be proved as a theorem using Agda's dependent pattern matching.
Axiom K is inconsistent with homotopy type theory, where the univalence axiom ...
The only way to prove ∥ X ∥ is to prove X (unless you admit some other axiom).
So, assuming P is a proposition, there is no way to prove ∥ ((A) ⊎ (¬ A)) ∥ if you cannot prove ((A) ⊎ (¬ A)).
It is not a correct intuition that undecidable propositions are either true or false, just we do not know about it.
A formal system S with an undecidable proposition P ...
Many total languages, including Agda and Coq, allow you to define coinductive data types. These model infinite objects, like infinite lists.
Obviously, a function producing an infinite list cannot terminate. However, it must, in a total language, be productive. This means that any finite prefix of the produced infinite list can be computed in finite time. ...