[Agda] Re: Builtins

[Kirill Elagin]

On Sat, Apr 25, 2015 at 10:52 PM N. Raghavendra <raghu at hri.res.in> wrote:

> At 2015-04-25T18:53:05Z, Kirill Elagin wrote:
>
> > Also note, that in Agda’s stdlib from `a ≡ b` it follows that `a` is
> > `b`, as Agda knows that there is no other than `refl` way to
> > construct a proof of `a ≡ b`.
>
> Is this related to axiom K and uniqueness of identity proofs?
>

Simply put, it is the ability to pattern-match on `refl` that gives you the
K axiom and the uniqueness of identity (which follows from K). When you
want to prove something about a path (let’s start using the HoTT
terminology) – e.g. that it equals `refl` – Agda tells you that it is
enough to consider the case when the path is `refl` itself – in which case
proving that it is equal to `refl` is trivial. So, the obvious thing to do
is to throw away pattern matching and stick to eliminators. Which is not
very convenient.

There is also another way around: introduce paths in a completely different
way. For example, one might add the interval type `I` to the theory and
define a path from `a` to `b` in `A` to be a function `p : I -> A` such
that `p 0` is `a` and `p 1` is `b`. This way the type of paths is a
_derived_ one, so it doesn’t have any constructors on its own, and as a
result you can’t pattern-match on it, so you don’t get the K axiom. The
theory you get is _slightly_ different from what you’ll find in the HoTT
book, but it is still great for doing HoTT.
Here is an [implementation of this theory](
https://hackage.haskell.org/package/hoq).


> > You said you are going to do HoTT, so you should be aware that this is
> > not true in HoTT (since there are types that are not 0-types).
>
> Is this why all HoTT-Agda files contain the {-# OPTIONS --without-K #-}
> pragma?
>

Right.

So, as I said, it’s pattern matching that lets you prove the K axiom.
(Warning: here I start talking about things I don’t really know much
about.) It seems that the pattern of pattern matching (huh!) used in known
proofs of K is somewhat special and as a result it can be detected. That’s
what the `--without-K` key does, it tells Agda to detect this special usage
of pattern matching and reject it. The proof of `J` at the same time
doesn’t follow this pattern, so Agda will still accept it.

The funny thing is that, as far as I know, it is not proven that there is
no other way to derive K, using, maybe, some other weird trick with pattern
matching. So the `--without-K` is not guaranteed to save you from K, but it
is believed to do so.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150425/21100779/attachment.html