[Agda] no-eta-equality

[Nils Anders Danielsson]

On 2016-09-26 15:01, Andrea Vezzosi wrote:
> You can have or not have a constructor, though I would strongly
> suggest that you add one otherwise some proofs might be impossible,
> e.g. the proof that "fst x , snd x" and "x" are prop. equal would go
> by pattern matching on x.

open import Agda.Builtin.Equality

record Σ (A : Set) (B : A → Set) : Set where
   field
     proj₁ : A
     proj₂ : B proj₁

open Σ

η : ∀ {A B} (p : Σ A B) → p ≡ record { proj₁ = proj₁ p; proj₂ = proj₂ p }
η (record { proj₁ = proj₁; proj₂ = proj₂ }) = refl

-- 
/NAD