<div dir="ltr"><div class="gmail_quote">On Sat, Apr 25, 2015 at 10:52 PM N. Raghavendra <<a href="mailto:raghu@hri.res.in">raghu@hri.res.in</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">At 2015-04-25T18:53:05Z, Kirill Elagin wrote:<br>
<br>
> Also note, that in Agda’s stdlib from `a ≡ b` it follows that `a` is<br>
> `b`, as Agda knows that there is no other than `refl` way to<br>
> construct a proof of `a ≡ b`.<br>
<br>
Is this related to axiom K and uniqueness of identity proofs?<br></blockquote><div><br></div><div>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.<br><br></div><div>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.<br></div><div>Here is an [implementation of this theory](<a href="https://hackage.haskell.org/package/hoq">https://hackage.haskell.org/package/hoq</a>).<br> <br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> You said you are going to do HoTT, so you should be aware that this is<br>
> not true in HoTT (since there are types that are not 0-types).<br>
<br>
Is this why all HoTT-Agda files contain the {-# OPTIONS --without-K #-}<br>
pragma?<br></blockquote><div><br></div><div>Right.<br><br></div><div>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.<br><br></div><div>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.<br></div></div></div>