Understanding function extensionality

cats.agda

-- {-# OPTIONS --cubical #-}
module cats where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)
-- open import Cubical.Core.Everything
-- open import Cubical.Foundations.Prelude


variable ℓ ℓ1 ℓ2 ℓ3 : Level
postulate
  extensionality : {A : Set ℓ1} {B : Set ℓ2} {f g : A → B}
    → ( (x : A) → f x ≡ g x) → f ≡ g

record Cat ℓ : Set (lsuc ℓ) where
  field
    Obj : Set ℓ
    Hom : Obj → Obj → Set ℓ
    ι : (x : Obj) → Hom x x
    o : {x y z : Obj} → Hom y z → Hom x y → Hom x z
    ι∘ : {x y : Obj} (f : Hom x y) → o (ι y) f ≡ f
    ∘ι : {x y : Obj} (f : Hom x y) → o f (ι x) ≡ f
    ∘assoc : {a b c d : Obj} (f : Hom a b) (g : Hom b c) (h : Hom c d)
      → o h (o g f) ≡ o (o h g) f
open Cat

record Functor (𝒞 : Cat ℓ1) (𝒟 : Cat ℓ2) : Set (ℓ1 ⊔ ℓ2) where
  field
    F₀ : Obj 𝒞 → Obj 𝒟
    F₁ : {x y : Obj 𝒞} → Hom 𝒞 x y → Hom 𝒟 (F₀ x) (F₀ y)
    Fι : (x : Obj 𝒞) → F₁ (ι 𝒞 x) ≡ ι 𝒟 (F₀ x)
    F∘ : {x y z : Obj 𝒞} (f : Hom 𝒞 y z) (g : Hom 𝒞 x y) → F₁ (o 𝒞 f g) ≡ o 𝒟 (F₁ f) (F₁ g)
  Fι₁ Fι₀ : (x : Obj 𝒞) → Hom 𝒟 (F₀ x) (F₀ x)
  Fι₁ x = F₁ (ι 𝒞 x)
  Fι₀ x = ι 𝒟 (F₀ x)
  ExtFι : (λ x → F₁ (ι 𝒞 x)) ≡ (λ x → ι 𝒟 (F₀ x))
  ExtFι = extensionality Fι
open Functor

-- Cannot instantiate the metavariable _138 to solution
-- Hom 𝒟 (F₀ x) (F₀ x) since it contains the variable x
-- which is not in scope of the metavariable
-- when checking that the inferred type of an application
--   _f_139 ≡ _g_140
-- matches the expected type
--   (λ x → F₁ (ι 𝒞 x)) ≡ (λ x → ι 𝒟 (F₀ x))