[Agda] no longer type checks

[Martin Escardo]

Right. But why are the in's not "injective" (Agda's error message) 
whereas false/true are?

What is the criterion used by Agda? And why do the in's look injective 
in plain definition by cases below?

I suppose you wanted refl not to be injective with without-K, but isn't 
the current criterion too strong?

Best,
Martin

On 14/12/12 00:14, Justus Matthiesen wrote:
>> Anyway, is there a simple workaround?
>
> The following should do the job:
>
>    bool-distinct : true ≡ false → ⊥
>    bool-distinct ()
>
>    is-in₀ : {X Y : Set} → X + Y → Bool
>    is-in₀ (in₀ _) = true
>    is-in₀ (in₁ _) = false
>
>    lemma : {X Y : Set} {x : X} {y : Y} → in₀ x ≡ in₁ y → ⊥
>    lemma e = bool-distinct (cong is-in₀ e)
>
>
> Justus
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe