New answers tagged

2

What Agda is showing you in the source code in both cases are the propositional proofs, i.e., elements of the identity type. In Agda the judgemental (definitional) equality is invisible to the user. Agda uses it in the background to verify that terms have required types. When it has to compare $a$ and $b$, it normalizes both of them (based on judgemental ...


5

Supposing we have $a$ and $b$ of type $A$ and $p : \mathrm{Id}_A(a,b)$, there simply is not any rule of type theory that would allow you to replace $b$ with $a$ arbitrarily. So one answer is "because type theory does not let you do that", and if you think that it can be done, please show me how. But I suppose that is a non-answer, what you really are asking ...


4

We don't always want extentionality In mathematics, a function is a relation between its inputs and its output. Two functions are equal if and only if they map the same outputs to the same inputs. But in computer science, we're often interested in descriptions of computations which we also call “functions”, where it matters how the outputs are calculated ...


2

what does it mean by becoming extensional in the first place? The axiom of extensionality relates to what it means for two functions to be equal. Specifically, extensionality says: $f = g \iff \forall x \ldotp f(x) = g(x)$ That is, functions are equal if they map equal inputs to equal outputs. By this definition, quicksort and mergesort are equal, even if ...


5

Recall that (a few paragraphs above) two objects are definitionally equal if after certain computation steps they evaluate to identical results. Assume throughout this post that $M$ and $N$ are definitionally equal. This means that there is a series of computation steps $M_0 \leftrightarrow M_1 \leftrightarrow \ldots \leftrightarrow M_n$ where I use $\...


Top 50 recent answers are included