New answers tagged type-theory
2
Agda is definitely the better choice if you're doing Homotopy Type Theory.
Idris has several features that are specifically incompatible with HoTT. Specifically, you can use dependent pattern matching to prove Uniqueness of Identity Proofs (UIP), which, when combined with Univalence, allows you to prove False. There's also a type-case feature which you can ...
2
Interpreting your problem as finding a computable $f$ such that $f\big(\langle M\rangle\big)=\langle M'\rangle$ with the property that $M'$ enumerates all programs equivalent to $M$, i.e. all $M''$ with $L(M'')=L(M)$, the answer is no (such $f$ does not exist).
One way to show this is to observe that such $f$ would place the language $\left\{\big(\langle M_1\...
1
You should think in Turing Machines.
If I understand correctly, what you ask is more or less "Given the code of a Turing Machine, is it possible to enumerate the codes of all Turing Machines with the same language?".
I think this is not possible, because it is undecidable to know whether two TM have the same languages (all the more so list all TM ...
4
If by "non-terminating real number" you mean to say that the digit expansion of the number is an infinite sequence, then that is not saying much, because every real number is "non-terminating" in this sense, even the real number 42, for its digit expansion is
$$41.999999999999999999999999999999....$$
In any case, nobody suggests that the ...
1
Normally, Agda does an analysis to determine that your indexed type is equivalent to a parameterized type. Essentially, since A occurs in the result type, knowing that l : List A tells you what type A is 'stored' in the value l. The value is known, which means that tricks that involve embedding a universe into a small type within said universe to cause a ...
2
The best way to explain it is
$$\mathsf{Bool} \to C \cong C \times C,$$
which is a special case of
$$(A + B) \to C \cong (A \to C) \times (B \to C).$$
Read the above as follows: as sum is equivalent to a pair of visitors.
(By the way, this is not the de Morgan law. It does not have a name, as far as I know. It's a general consequence of the definition of the ...
Top 50 recent answers are included
