[Agda] Incompatibilities affecting ``Fresh Look''

[Nils Anders Danielsson]

On 2010-12-14 04:29, kahl at cas.mcmaster.ca wrote:
> and had to notice that the new Data.Maybe.decSetoid doesn't preserve
> _≡_ anymore. Is the a ``right way'' to get this to work with the
> current library

I don't think so.

> Second Problem: In Data.Product.Extras, they have:
>
> \begin{code}
> proj₁-injective : ∀ {a b} {A : Set a} {B : A → Set b} {x y : Σ A B}
>                      (B-uniq : ∀ {z} (p₁ p₂ : B z) → p₁ ≡ p₂)
>                    → proj₁ x ≡ proj₁ y → x ≡ y
> proj₁-injective {x = (a , p₁)} {y = (.a , p₂)} B-uniq refl
>    = cong (λ p → (a , p)) (B-uniq p₁ p₂)
> \end{code}

[...]

> How can this be done?

proj₁-injective : ∀ {a b} {A : Set a} {B : A → Set b} {x y : Σ A B}
                     (B-uniq : ∀ {z} (p₁ p₂ : B z) → p₁ ≡ p₂)
                   → proj₁ x ≡ proj₁ y → x ≡ y
proj₁-injective {B = B} {x = (a₁ , b₁)} {y = (a₂ , b₂)}
                 B-uniq a₁≡a₂ = helper a₁≡a₂
   where
   helper : ∀ {a₁ a₂} {b₁ : B a₁} {b₂ : B a₂} →
            a₁ ≡ a₂ → _,_ {B = B} a₁ b₁ ≡ (a₂ , b₂)
   helper refl = cong ,_ (B-uniq _ _)

-- 
/NAD