<div dir="ltr">No, they live in the same type: in the first clause, they both live in X₀, and in the last clause they both live in X₁. They do have different types in the two middle clauses, but there they are not equated.<br>

</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Apr 2, 2014 at 2:24 PM, Martin Escardo <span dir="ltr">&lt;<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class=""><br>
<br>
On 02/04/14 13:15, Jesper Cockx wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
The translation to eliminators uses the generic &quot;no confusion&quot; property<br>
of constructors from &quot;A few constructions on constructors&quot; by Conor et<br>
al. (2006). This property is defined by a two-level construction, so it<br>
needs (at least) the first universe Set. For the _+_ type, the<br>
construction looks like this:<br>
<br>
+-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>
</blockquote>
<br></div>
But x and y live in different types. Are you sure you mean x ≡ y?<div class=""><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
+-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>
<br>
Both can easily written using the eliminators for _+_ and _≡_, see the<br>
paper for details. Now the definition of sum-disjoint from +-noConfusion<br>
is easy:<br>
<br>
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>
<br>
The actual translation looks much more complicated because it has to<br>
deal with possible multiple case splits and recursive calls, but the<br>
result is essentially the same.<br>
</blockquote>
<br></div>
Ok, I understand, modulo the x ≡ y issue.<span class="HOEnZb"><font color="#888888"><br>
<br>
Martin<br>
<br>
</font></span></blockquote></div><br></div>