[Agda] Avoiding implicit argument proliferation?

[Brandon Moore]

Here's some code, extracted from an attempt at formalizing early excercies
in "Categories for the Working Mathematician". The hidden arguments
continue to accumulate as higher structures are build. They can be inferred,
so working with these definitions in expressions is not too bad, but to state
any types it seems I need to quantify over (and manually provide) all these
implicit arguments.

On the other hand, if all the implicit arguments became fields of the records
instead, I don't know how to enforce equalities like requiring the middle 
category
to agree in the definition of functor category. It's easy enough to take another
argument along the lines of Functor.source f2 \== Functor.target f1, but I don't
know how to use such a thing to make fields compatible, except by rewriting
them one at a time in with-clauses. I had an earlier message about
the problem, and most replies suggested to use parameters instead.

metagraph : Set → Set₁
metagraph Objects = Objects → Objects → Set

record Category{Objects : Set}(Arrows : metagraph Objects) : Set where
  field
    identity : (o : Objects) → Arrows o o
    compose : ∀{a b c} → Arrows a b → Arrows b c → Arrows a c
    compose-assoc : ∀{a b c d}(f : Arrows a b)(g : Arrows b c)(h : Arrows c d) →
      compose (compose f g) h ≡ compose f (compose g h)
    unit-left : ∀{a b}(f : Arrows a b) → compose (identity a) f ≡ f
    unit-right : ∀{a b}(f : Arrows a b) → compose f (identity b) ≡ f

record Functor {O1 O2 A1 A2} (C1 : Category {O1} A1 ; C2 : Category {O2} A2) : 
Set where
  field
    omap : O1 → O2
    amap : ∀{a b} → A1 a b → A2 (omap a) (omap b)
    compat : ∀{a b c}(f : A1 a b)(g : A1 b c) →
      amap (Category.compose C1 f g) ≡ Category.compose C2 (amap f) (amap g)

composeF : ∀{O1 O2 O3}{A1 A2 A3}{C1 C2 C3} → Functor {O2} {O3} {A2} {A3} C2 C3 → 
Functor {O1 = O1} {A1 = A1} C1 C2 → Functor C1 C3
composeF {O1} {O2} {O3} {A1} {A2} {A3} {C1} {C2} {C3} f23 f12 = record { omap = 
omap23 ∘ omap12 ; amap = amap23 ∘ amap12 ;
  compat = λ f g → begin amap23 (amap12 (Category.compose C1 f g)) ≡⟨ cong 
amap23 (compat12 f g) ⟩
                                       amap23 (Category.compose C2 (amap12 f) 
(amap12 g)) ≡⟨ compat23 (amap12 f) (amap12 g) ⟩
                                       Category.compose C3 (amap23 (amap12 f)) 
(amap23 (amap12 g)) ∎ }
  where open Functor f23 renaming (omap to omap23;amap to amap23;compat to 
compat23)
        open Functor f12 renaming (omap to omap12;amap to amap12;compat to 
compat12)

Brandon