Is it possible to prove the existence of the category of categories (with functors as morphisms) in Agda without functional extensionality?

Question

I am modelling categories and functors like this (the imports are from the standard library):

module Categories where

open import Level
open import Relation.Binary.PropositionalEquality

record Category a b  : Set (suc (a ⊔ b)) where
  field
    Obj : Set a
    _⇒_ : Obj → Obj → Set b
    _∘_ : {A B C : Obj} → B ⇒ C → A ⇒ B → A ⇒ C
    id : {A : Obj} → A ⇒ A

    left-id : ∀ {A B : Obj} (f : A ⇒ B) → id ∘ f ≡ f
    right-id : ∀ {A B : Obj} (f : A ⇒ B) → f ∘ id ≡ f
    assoc : ∀ {A B C D : Obj} (f : C ⇒ D) (g : B ⇒ C) (h : A ⇒ B) → (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)

infix 10 _[_⇒_] _[_∘_]
_[_⇒_] : ∀ {a b} (C : Category a b) (X : Category.Obj C) (Y : Category.Obj C) → Set b
_[_⇒_] = Category._⇒_

_[_∘_] : ∀ {a b} (C : Category a b) → ∀ {X Y Z} (f : C [ Y ⇒ Z ]) (g : C [ X ⇒ Y ]) → C [ X ⇒ Z ]
_[_∘_] = Category._∘_

record Functor {a b c d} (C : Category a b) (D : Category c d) : Set (a ⊔ b ⊔ c ⊔ d) where
  private module C = Category C
  private module D = Category D

  field
    F : C.Obj → D.Obj
    fmap′ : ∀ (A B : C.Obj) → C [ A ⇒ B ] → D [ F A ⇒ F B ]

    fmap-id′ : ∀ (A : C.Obj) → fmap′ A _ C.id ≡ D.id
    fmap-∘′ : ∀ (X Y Z : C.Obj) (f : C [ Y ⇒ Z ]) (g : C [ X ⇒ Y ]) → fmap′ _ _ (C [ f ∘ g ]) ≡ D [ fmap′ _ _ f ∘ fmap′ _ _ g ]

  fmap : ∀ {A B : C.Obj} → C [ A ⇒ B ] → D [ F A ⇒ F B ]
  fmap {A}{B} = fmap′ A B

  fmap-id : ∀ {A : C.Obj} → fmap′ A A C.id ≡ D.id
  fmap-id {A} = fmap-id′ A

  fmap-∘ : ∀ {X Y Z : C.Obj} (f : C [ Y ⇒ Z ]) (g : C [ X ⇒ Y ]) → fmap′ _ _ (C [ f ∘ g ]) ≡ D [ fmap′ _ _ f ∘ fmap′ _ _ g ]
  fmap-∘ {X}{Y}{Z} = fmap-∘′ X Y Z

And I am trying to prove the existence of the category of categories by instantiating it like this (where the levels a and b are parameters of the module for tidiness):

category : Category (suc (a ⊔ b)) (a ⊔ b)
category = record
  { Obj = Category a b
  ; _⇒_ = Functor
  ; _∘_ = Compose
  ; id = Identity
  ; left-id = {!!}
  ; right-id = {!!}
  ; assoc = {!!}
  }

Compose and Identity are defined as you'd expect, where, importantly, fmap-id for the composition of functors F and G is proved like this:

  fmap-id : ∀ (A : C.Obj) → fmap A _ C.id ≡ E.id
  fmap-id _ =
    begin
      F.fmap (G.fmap C.id)
    ≡⟨ cong F.fmap G.fmap-id ⟩
      F.fmap D.id
    ≡⟨ F.fmap-id ⟩
      E.id
    ∎

Now, I am stuck trying to prove left-id for this category. This is what I have so far:

FunctorCongruence : ∀ {C D : Category a b} → Functor C D → Functor C D → Set ((a ⊔ b))
FunctorCongruence F G = F.F ≅ G.F → F.fmap′ ≅ G.fmap′ → F.fmap-id′ ≅ G.fmap-id′ → F.fmap-∘′ ≅ G.fmap-∘′ → F ≅ G
  where
    module F = Functor F
    module G = Functor G

functor-cong : ∀ {C D : Category a b}{F : Functor C D}{G : Functor C D} → FunctorCongruence F G
functor-cong refl refl refl refl = refl

left-id : ∀ {C D : Category a b} (F : Functor C D) → Compose Identity F ≡ F
left-id {C} F = ≅-to-≡ (functor-cong F-≅ fmap-≅ fmap-id-≅ fmap-∘-≅)
  where
    Cmp = Compose Identity F
    module F = Functor F
    module Cmp = Functor Cmp
    module C = Category C

    open HetEq.≅-Reasoning

    F-≅ : Cmp.F ≅ F.F
    F-≅ = refl

    fmap-≅ : Cmp.fmap′ ≅ F.fmap′
    fmap-≅ = refl

    lem : (λ A → trans (cong (λ x → x) (F.fmap-id′ A)) refl) ≅ F.fmap-id′
    lem =
      begin
        (λ A → trans (cong (λ x → x) (F.fmap-id′ A)) refl)
      ≅⟨ ? ⟩
        (λ A → cong (λ x → x) (F.fmap-id′ A))
      ≅⟨ ? ⟩
        (λ A → F.fmap-id′ A)
      ≅⟨ refl ⟩
        F.fmap-id′
      ∎

    fmap-id-≅ : Cmp.fmap-id′ ≅ F.fmap-id′
    fmap-id-≅ = lem

    fmap-∘-≅ : Cmp.fmap-∘′ ≅ F.fmap-∘′
    fmap-∘-≅ = ?

But I'm concerned that proving the equality (λ A → trans (cong (λ x → x) (F.fmap-id′ A)) refl) ≅ F.fmap-id′ seems to require functional extensionality of heterogeneous equality, because the LHS is hidden behind the λ A. If I am correct about that, is there perhaps a different way of defining fmap-id that will avoid this situation? Or does any proof of the existence of this category within Agda's type theory depend on functional extensionality?

Answer 1

Just make A ⇒ B a setoid rather than a Set. This is how it's done in the standard categories library. In my small development I did the same, but replaced

record Category α β γ : Set (suc (α ⊔ β ⊔ γ)) where
  field
    Obj    : Set α
    _⇒_    : Obj -> Obj -> Set β
    setoid : ∀ {A B} -> Setoid (A ⇒ B) γ
    ...

with

record Category α β γ : Set (suc (α ⊔ β ⊔ γ)) where
  field
    Obj    : Set α
    _⇒_    : Obj -> Obj -> Set β       
    setoid : ISetoid₂ _⇒_ γ
    ...

where

record IsIEquivalence {ι α β} {I : Set ι} (A : I -> Set α) (_≈_ : ∀ {i} -> A i -> A i -> Set β)
                      : Set (ι ⊔ α ⊔ β) where
  field
    refl  : ∀ {i} {x     : A i} -> x ≈ x
    sym   : ∀ {i} {x y   : A i} -> x ≈ y -> y ≈ x
    trans : ∀ {i} {x y z : A i} -> x ≈ y -> y ≈ z -> x ≈ z

record ISetoid {ι α} {I : Set ι} (A : I -> Set α) β : Set (ι ⊔ α ⊔ suc β) where
  infix 4 _≈_

  field
    _≈_            : ∀ {i} -> A i -> A i -> Set β
    isIEquivalence : IsIEquivalence A _≈_

ISetoid₂ : ∀ {ι₁ ι₂ α} {I₁ : Set ι₁} {I₂ : I₁ -> Set ι₂} (A : ∀ i₁ -> I₂ i₁ -> Set α) β
         -> Set (ι₁ ⊔ ι₂ ⊔ α ⊔ suc β)
ISetoid₂ A = ISetoid (uncurry A)

Not very big difference, but looks slightly nicer to me. Here is my variant of setoid over a Functor. And the Cat category.

---

I'll elaborate a bit. Functors are equal if they map equal objects to equal objects and equal morphisms to equal morphisms. But the latter implies the former, since if two moprhisms are equal then their domains and codomains are equal as well, so we get equality of objects from equality of identity morphisms:

F₁ (id A) ≈ G₁ (id A)
id (F₀ A) ≈ id (G₀ A)
F₀ A      ≡ G₀ A

In the standard categories library and in mine functors are equal if they map definitionally equal morphisms to equal morphisms (I wonder why):

F ≈ G = ∀ f -> F₁ f ≈ G₁ f

The problem here is that to say f ≈ g we need f and g to be morphisms between the same objects. But

f : A ⇒ B
F₁ f : F₀ A ⇒ F₀ B
G₁ f : G₀ A ⇒ G₀ B

F₁ f and G₁ f are of different types. The solution is to construct heterogeneous equality over the existing homogeneous

data _∼_ {A B} (f : A ⇒ B) : ∀ {X Y} → (X ⇒ Y) → Set (ℓ ⊔ e) where
  ≡⇒∼ : {g : A ⇒ B} → .(f ≡ g) → f ∼ g

We can deal with this more systematically and make the heterogeneous setoid from any indexed setoid:

data _≋_ {i} (x : A i) : ∀ {j} -> A j -> Set β where
  hetero : {y : A i} -> x ≈ y -> x ≋ y

(One nice thing is that using this transformation we can make Agda's heterogeneous equality from propositional equality.)