No-eta-equality records as positive labeled products

Foo.agda

module Foo where

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

record NamedPair (A B : Set) : Set where
  pattern -- not allowed to pattern match on NamedPair otherwise
  no-eta-equality
  field
    fst : A
    snd : B

variable
  A B C : Set
  a : A
  b : B
  p : NamedPair A B


lett : ∀ {A B C : Set}
  → (A → B → C)
  → NamedPair A B → C
lett f record { fst = fst ; snd = snd } = f fst snd

lettβ : ∀ {f : A → B → C}
  → lett f (record { fst = a ; snd = b }) ≡ f a b
lettβ = refl

Named-pair-weak-η :
  ∀ (p : NamedPair A B) → 
  p ≡ record { fst = p .NamedPair.fst ; snd = p .NamedPair.snd }
-- Named-pair-weak-η p = {!refl!} -- doesn't type check
Named-pair-weak-η record { fst = fst ; snd = snd } = refl

postulate
  funExt : ∀ {f g : A → B}
    → (∀ a → f a ≡ g a) → f ≡ g

lettη : ∀ {g : NamedPair A B → C}
  → g ≡ lett λ a b → g (record { fst = a ; snd = b })
-- lettη = refl  -- doesn't type check
lettη = funExt (λ { record { fst = fst ; snd = snd } → refl } )