[Agda] Sharing between records

[Nicolas Pouillard]

On Fri, 11 Mar 2011 18:36:03 -0800 (PST), Brandon Moore <brandon_m_moore at yahoo.com> wrote:
> 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?

I would take a different path by having less dependent fields (like having cat
as first field) and having more parameters. Moreover nothing prevents you from
building the dependent record afterwards. This is actually the style used in
the standard library.

If I omit these dependent versions alltogether it roughly gives:

= {-# 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 HaveTerminal (cat : Category) : Set₁ where
=   open Category cat
=   field
=     ⊥ : O
=     ! : (A : O) → A ↝ ⊥
=     !-uniq : {A : O} → (h : A ↝ ⊥) → h ≈H ! A
  
* record HavePairs (cat : Category) : Set₁ where
=   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 (cat : Category) : Set₁ where
*   field
*     pair : HavePairs cat
*     term : HaveTerminal cat
*   open HavePairs pair
*   open HaveTerminal term
*   open Category cat
=   ⊥l : {A : O} → ⊥ × A ↝ A
*   ⊥l = π₂

Best regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr