<div dir="ltr">Martin,<br><br><div><div class="gmail_extra">Thank you for testing it on your Agda files, it's great to hear that it's working for you.<br></div><div class="gmail_extra"><br><div class="gmail_quote">
On Wed, Apr 2, 2014 at 12:29 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><br></div>(Wouldn't it be better if the patch simply made without-K work in your<br>
way, rather than require to change all files from without-K to<br>
new-without-K?)<br></blockquote><div><br></div><div>Yes, but I kept the old version available for now for testing purposes and to allow easy comparison between the two versions. <br> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
I wonder what your automatic translation of my function in the above<br>
file to eliminators is. The reason I am asking is that what I prove<br>
above using pattern matching requires the use of a universe in MLTT.<br>
Does your automatic translation generate such a use of the universe?<span><font color="#888888"><br></font></span></blockquote><div><br></div><div>The translation to eliminators uses the generic "no confusion" property of constructors from "A few constructions on constructors" by Conor et al. (2006). This property is defined by a two-level construction, so it needs (at least) the first universe Set. For the _+_ type, the construction looks like this:<br>
<br><div style="margin-left:40px">+-NoConfusion : {X₀ X₁ : Set} → X₀ + X₁ → X₀ + X₁ → Set<br>+-NoConfusion (in₀ x) (in₀ y) = x ≡ y<br>+-NoConfusion (in₀ x) (in₁ y) = ∅<br>+-NoConfusion (in₁ x) (in₀ y) = ∅<br>+-NoConfusion (in₁ x) (in₁ y) = x ≡ y<br>
<br>+-noConfusion : {X₀ X₁ : Set} (x y : X₀ + X₁) → x ≡ y → +-NoConfusion x y<br>+-noConfusion (in₀ x) .(in₀ x) refl = refl<br>+-noConfusion (in₁ x) .(in₁ x) refl = refl<br></div><br></div><div>Both can easily written using the eliminators for _+_ and _≡_, see the paper for details. Now the definition of sum-disjoint from +-noConfusion is easy:<br>
<br><div style="margin-left:40px">sum-disjoint : {X Y : Set} {x : X} {y : Y} → in₀ x ≡ in₁ y → ∅<br>sum-disjoint {x = x} {y = y} = +-noConfusion (in₀ x) (in₁ y)<br></div><br></div><div>The actual translation looks much more complicated because it has to deal with possible multiple case splits and recursive calls, but the result is essentially the same.<br>
<br><br></div><div>Jesper<br>
</div><div><br></div></div><br></div></div></div>