[Agda] Sharing between records

[Brandon Moore]

When using records to model structures, there seems to be no way to
express sharing similarly to an ML-with clause.

I would like to have an alternative to piling up parameters as structures grow.

Is there any natural way to define the last combined record in the
code below, and give the mixed type signature?

{-# OPTIONS --universe-polymorphism #-}
module ccc2 where
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Level

record Category : Set₁ where
  field
    Objs : Setoid zero zero
  O = Setoid.Carrier Objs
  _≈_ = Setoid._≈_ Objs
  field
    hom : O → O → Setoid zero zero
  _↝_ : O → O → Set
  _↝_ A B = Setoid.Carrier (hom A B)
  _≈H_ : {A B : O} → A ↝ B → A ↝ B → Set
  _≈H_ {A} {B} = Setoid._≈_ (hom A B)
  field
    id : (A : O) → A ↝ A
    _⟫_ : ∀{A B} → A ↝ B → ∀{C} → B ↝ C → A ↝ C
    idl : ∀{A B}{h : A ↝ B} → (id A ⟫ h) ≈H h
    idr : ∀{A B}{h : A ↝ B} → (h ⟫ id B) ≈H h
  infix 4 _≈_
  infix 4 _≈H_
  infixr 6 _⟫_
  infixr 5 _↝_

record Terminal : Set₁ where
  field
    cat : Category
  open Category cat
  field
    ⊥ : O
    ! : (A : O) → A ↝ ⊥
    !-uniq : {A : O} → (h : A ↝ ⊥) → h ≈H ! A

record Pairs : Set₁ where
  field
    cat : Category
  open Category cat
  field
    _×_ : O → O → O
    π₁ : ∀{A B} → (A × B) ↝ A
    π₂ : ∀{A B} → (A × B) ↝ B
    ⟨_,_⟩ : ∀{A B C} → (A ↝ B) → (A ↝ C) → A ↝ (B × C)
    ⟨_,_⟩₁ : ∀{A B C}(f : A ↝ B)(g : A ↝ C) → ⟨ f , g ⟩ ⟫ π₁ ≈H f
    ⟨_,_⟩₂ : ∀{A B C}(f : A ↝ B)(g : A ↝ C) → ⟨ f , g ⟩ ⟫ π₂ ≈H g
    ⟨_,_⟩-uniq : ∀{A B C}(f : A ↝ B)(g : A ↝ C){h : A ↝ (B × C)} →
      h ⟫ π₁ ≈H f → h ⟫ π₂ ≈H g → h ≈H ⟨ f , g ⟩
  _×H_ : ∀{A B}(f : A ↝ B) → ∀{C D}(g : C ↝ D) → A × C ↝ B × D
  f ×H g = ⟨ π₁ ⟫ f , π₂ ⟫ g ⟩
  infixr 6 _×_

record FiniteProducts : Set₁ where
  field
    pair : Pairs
    term : Terminal
    catSame : Pairs.cat pair ≡ Terminal.cat term
  open Pairs pair
  open Terminal term
  open Category (Pairs.cat pair)
  ⊥l : {A : O} → ⊥ × A ↝ A
  ⊥l = ?