title: Equality of records in Agda
body: <p>It seems that to prove that two items of a record type are equivalent, I need to write a helper that takes component wise proofs and applies them.
  An example:</p>
  
  <pre><code>postulate P : ℕ → Set
  
  record Silly : Set (ℓsuc ℓ₀) where
   constructor _#_#_
   field
    n : ℕ
    pn : P n
    f : Set → ℕ
  
  open Silly
  
  SillyEq : ∀ s t → n s ≡ n t → pn s ≅ pn t → f s ≡ f t → s ≡ t
  SillyEq (n # pn # f) (.n # .pn # .f) ≡-refl ≅-refl ≡-refl = ≡-refl
  </code></pre>
  
  <p>I feel like <code>SillyEq</code> should somehow be available to me, that I do not need to write it myself --or am I mistaken.</p>
  
  <p>Also, I could not prove <code>SillyEq</code> without declaring a constructor and then pattern matching on it.</p>
  
  <p>Thanks for your assistance!</p>