Functor

------------------------------------------------------------------------
-- Functors and natural transformations (for 1-categories)
------------------------------------------------------------------------

-- The code is based on the presentation in the HoTT book (but might
-- not follow it exactly).

{-# OPTIONS --cubical-compatible --safe #-}

open import Equality

module Functor
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

import Surjection

open import Bijection eq hiding (id; _∘_; inverse; step-↔; finally-↔)
open import Category eq
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq using (_≃_; module _≃_; ↔⇒≃)
open import Extensionality eq
open import Function-universe eq hiding (id; _∘_)
open import H-level eq
open import H-level.Closure eq
open import Logical-equivalence using (_⇔_; module _⇔_)
open import Prelude as P hiding (id; _^_)

------------------------------------------------------------------------
-- Functors

Functor : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
          Precategory ℓ₁ ℓ₂ → Precategory ℓ₃ ℓ₄ → Type _
Functor C D =
  -- Object map.
  ∃ λ (F₀ : Obj C → Obj D) →

  -- Morphism map.
  ∃ λ (F : ∀ {X Y} → Hom C X Y → Hom D (F₀ X) (F₀ Y)) →

  -- F should be homomorphic with respect to identity and composition.
  (∀ {X} → F (id C {X = X}) ≡ id D) ×
  (∀ {X Y Z} {f : Hom C X Y} {g : Hom C Y Z} →
     F (_∙_ C g f) ≡ _∙_ D (F g) (F f))

  where open Precategory

-- A wrapper.

infix 4 _⇨_

record _⇨_ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}
           (C : Precategory ℓ₁ ℓ₂) (D : Precategory ℓ₃ ℓ₄) :
           Type (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
  field
    functor : Functor C D

  open Precategory

  infixr 10 _⊚_ _⊙_

  -- Object map.

  _⊚_ : Obj C → Obj D
  _⊚_ = proj₁ functor

  -- Morphism map.

  _⊙_ : ∀ {X Y} → Hom C X Y → Hom D (_⊚_ X) (_⊚_ Y)
  _⊙_ = proj₁ (proj₂ functor)

  -- The morphism map is homomorphic with respect to identity.

  ⊙-id : ∀ {X} → _⊙_ (id C {X = X}) ≡ id D
  ⊙-id = proj₁ (proj₂ (proj₂ functor))

  -- The morphism map is homomorphic with respect to composition.

  ⊙-∙ : ∀ {X Y Z} {f : Hom C X Y} {g : Hom C Y Z} →
        _⊙_ (_∙_ C g f) ≡ _∙_ D (_⊙_ g) (_⊙_ f)
  ⊙-∙ = proj₂ (proj₂ (proj₂ functor))

open _⇨_ public

opaque

  -- The homomorphism properties are propositional (assuming
  -- extensionality).

  functor-properties-propositional :
    ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
    Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
    {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄}
    (F : C ⇨ D) → let open Precategory in

    Is-proposition ((∀ {X} → F ⊙ id C {X = X} ≡ id D) ×
                    (∀ {X Y Z} {f : Hom C X Y} {g : Hom C Y Z} →
                     F ⊙ (_∙_ C g f) ≡ _∙_ D (F ⊙ g) (F ⊙ f)))

  functor-properties-propositional {ℓ₁} {ℓ₂} ext {D} _ = ×-closure 1
    (implicit-Π-closure (lower-extensionality ℓ₂ (ℓ₁ ⊔ ℓ₂) ext) 1 λ _ →
     Precategory.Hom-is-set D)
    (implicit-Π-closure (lower-extensionality ℓ₂ lzero     ext) 1 λ _ →
     implicit-Π-closure (lower-extensionality ℓ₂ lzero     ext) 1 λ _ →
     implicit-Π-closure (lower-extensionality ℓ₂ ℓ₁        ext) 1 λ _ →
     implicit-Π-closure (lower-extensionality ℓ₁ ℓ₁        ext) 1 λ _ →
     implicit-Π-closure (lower-extensionality ℓ₁ (ℓ₁ ⊔ ℓ₂) ext) 1 λ _ →
     Precategory.Hom-is-set D)

opaque

  -- Functor equality is equivalent to equality of the corresponding
  -- maps, suitably transported (assuming extensionality).

  equality-characterisation⇨ :
    ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
    Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
    {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D} →
    let open Precategory in

    (F ≡ G)

      ≃

    ∃ λ (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
        _≡_ {A = ∀ {X Y} → Hom C X Y → Hom D (G ⊚ X) (G ⊚ Y)}
            (subst (λ F → ∀ {X Y} → Hom C X Y → Hom D (F X) (F Y))
                   ⊚F≡⊚G (_⊙_ F))
            (_⊙_ G)

  equality-characterisation⇨ ext {C} {D} {F} {G} =
    let P : (Obj C → Obj D) → Type _
        P = λ F₀ → ∀ {X Y} → Hom C X Y → Hom D (F₀ X) (F₀ Y)

        Q : ∃ P → Type _
        Q = λ { (F₀ , F) → (∀ {X} → F (id C {X = X}) ≡ id D) ×
                           (∀ {X Y Z} {f : Hom C X Y} {g : Hom C Y Z} →
                              F (_∙_ C g f) ≡ _∙_ D (F g) (F f)) }
    in

    (F ≡ G)                                                              ↝⟨ ↔⇒≃ record
                                                                              { surjection = record
                                                                                { logical-equivalence = record
                                                                                  { to   = cong functor
                                                                                  ; from = cong λ f → record { functor = f }
                                                                                  }
                                                                                ; right-inverse-of = λ _ → trans (cong-∘ _ _ _) (sym $ cong-id _)
                                                                                }
                                                                              ; left-inverse-of = λ _ → trans (cong-∘ _ _ _) (sym $ cong-id _)
                                                                              } ⟩
    (functor F ≡ functor G)                                              ↔⟨ inverse Σ-≡,≡↔≡ ⟩

    (∃ λ (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
         subst (λ F₀ → ∃ λ (F : P F₀) → Q (F₀ , F)) ⊚F≡⊚G
               (proj₂ $ functor F) ≡ proj₂ (functor G))                  ↝⟨ ∃-cong (λ ⊚F≡⊚G → ≡⇒↝ _ $ cong (λ x → x ≡ proj₂ (functor G)) $
                                                                              push-subst-pair P Q) ⟩
    (∃ λ (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
         _≡_ {A = ∃ λ (H : P (_⊚_ G)) → Q (_⊚_ G , H)}
         ( subst P ⊚F≡⊚G (_⊙_ F)
         , subst Q (Σ-≡,≡→≡ ⊚F≡⊚G (refl _)) (proj₂ $ proj₂ $ functor F)
         )
         (proj₂ (functor G)))                                            ↔⟨ ∃-cong (λ ⊚F≡⊚G → inverse $
                                                                              ignore-propositional-component
                                                                                (functor-properties-propositional ext G)) ⟩□
    (∃ λ (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
         (λ {_ _} → subst P ⊚F≡⊚G (_⊙_ F)) ≡ _⊙_ G)                      □

    where open Precategory

  -- Some simplification lemmas.

  proj₁-to-equality-characterisation⇨ :
    ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}
    (ext : Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄))
    {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D} →
    let open Precategory in
    (F≡G : F ≡ G) →

    proj₁ (_≃_.to (equality-characterisation⇨ ext {F = F} {G = G}) F≡G)
      ≡
    cong _⊚_ F≡G

  proj₁-to-equality-characterisation⇨ ext F≡G =
    proj₁ (_≃_.to (equality-characterisation⇨ ext) F≡G)  ≡⟨ proj₁-Σ-≡,≡←≡ _ ⟩
    cong proj₁ (cong functor F≡G)                        ≡⟨ cong-∘ _ _ _ ⟩∎
    cong _⊚_ F≡G                                         ∎

  cong-⊚-from-equality-characterisation⇨ :
    ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}
    (ext : Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄))
    {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D} →
    let open Precategory in
    (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
    (⊙F≡⊙G : _≡_ {A = ∀ {X Y} → Hom C X Y → Hom D (G ⊚ X) (G ⊚ Y)}
                 (subst (λ F → ∀ {X Y} → Hom C X Y → Hom D (F X) (F Y))
                        ⊚F≡⊚G (_⊙_ F))
                 (_⊙_ G)) →

    cong _⊚_ (_≃_.from (equality-characterisation⇨ ext {F = F} {G = G})
                       (⊚F≡⊚G , ⊙F≡⊙G))
      ≡
    ⊚F≡⊚G

  cong-⊚-from-equality-characterisation⇨ ext {F} {G} ⊚F≡⊚G ⊙F≡⊙G =
    cong _⊚_ (_≃_.from (equality-characterisation⇨ ext {F = F} {G = G})
                       (⊚F≡⊚G , ⊙F≡⊙G))                                  ≡⟨ cong-∘ _ _ _ ⟩

    cong proj₁ (Σ-≡,≡→≡ ⊚F≡⊚G _)                                         ≡⟨ proj₁-Σ-≡,≡→≡ _ _ ⟩∎

    ⊚F≡⊚G                                                                ∎

opaque

  -- Another equality characterisation lemma.

  equality-characterisation≡⇨ :
    ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
    Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
    {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D}
    {eq₁ eq₂ : F ≡ G} →
    (eq₁ ≡ eq₂) ≃ (cong _⊚_ eq₁ ≡ cong _⊚_ eq₂)
  equality-characterisation≡⇨ {ℓ₁} {ℓ₂} ext {D} {eq₁} {eq₂} =
    eq₁ ≡ eq₂                                              ↝⟨ inverse $ Eq.≃-≡ (equality-characterisation⇨ ext) ⟩

    _≃_.to (equality-characterisation⇨ ext) eq₁ ≡
    _≃_.to (equality-characterisation⇨ ext) eq₂            ↔⟨ inverse $ ignore-propositional-component
                                                                (implicit-Π-closure (lower-extensionality ℓ₂ lzero     ext) 2 λ _ →
                                                                 implicit-Π-closure (lower-extensionality ℓ₂ ℓ₁        ext) 2 λ _ →
                                                                 Π-closure          (lower-extensionality ℓ₁ (ℓ₁ ⊔ ℓ₂) ext) 2 λ _ →
                                                                 Precategory.Hom-is-set D) ⟩
    proj₁ (_≃_.to (equality-characterisation⇨ ext) eq₁) ≡
    proj₁ (_≃_.to (equality-characterisation⇨ ext) eq₂)    ↝⟨ ≡⇒↝ _ (cong₂ _≡_ (proj₁-to-equality-characterisation⇨ _ _)
                                                                               (proj₁-to-equality-characterisation⇨ _ _)) ⟩□
    cong _⊚_ eq₁ ≡ cong _⊚_ eq₂                            □

-- Identity functor.

id⇨ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂} → C ⇨ C
functor id⇨ = P.id , P.id , refl _ , refl _

-- Composition of functors.

infixr 10 _∙⇨_

_∙⇨_ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
         {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
         {ℓ₅ ℓ₆} {E : Precategory ℓ₅ ℓ₆} →
       D ⇨ E → C ⇨ D → C ⇨ E
functor (_∙⇨_ {C} {D} {E} G F) =
  (G ⊚_) ∘ (F ⊚_) ,
  (G ⊙_) ∘ (F ⊙_) ,
  (G ⊙ F ⊙ id C              ≡⟨ cong (G ⊙_) $ ⊙-id F ⟩
   G ⊙ id D                  ≡⟨ ⊙-id G ⟩∎
   id E                      ∎) ,
  (λ {_ _ _ f g} →
     G ⊙ F ⊙ _∙_ C g f              ≡⟨ cong (G ⊙_) $ ⊙-∙ F ⟩
     G ⊙ _∙_ D (F ⊙ g) (F ⊙ f)      ≡⟨ ⊙-∙ G ⟩∎
     _∙_ E (G ⊙ F ⊙ g) (G ⊙ F ⊙ f)  ∎)
  where
  open Precategory

-- id⇨ is a left identity (assuming extensionality).

id⇨∙⇨ :
  ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
  Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
  {F : C ⇨ D} → id⇨ ∙⇨ F ≡ F
id⇨∙⇨ ext {F} = _≃_.from (equality-characterisation⇨ ext)
  ( refl (F ⊚_)
  , (subst _ (refl (F ⊚_)) (λ {_ _} → F ⊙_)  ≡⟨ subst-refl _ _ ⟩∎
     (λ {_ _} → F ⊙_)                        ∎)
  )

-- id⇨ is a right identity (assuming extensionality).

∙⇨id⇨ :
  ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
  Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
  {F : C ⇨ D} → F ∙⇨ id⇨ ≡ F
∙⇨id⇨ ext {F} = _≃_.from (equality-characterisation⇨ ext)
  ( refl (F ⊚_)
  , (subst _ (refl (F ⊚_)) (λ {_ _} → F ⊙_)  ≡⟨ subst-refl _ _ ⟩∎
     (λ {_ _} → F ⊙_)                        ∎)
  )

-- _∙⇨_ is associative (assuming extensionality).

∙⇨-assoc :
  ∀ {ℓ₁ ℓ₂} {C₁ : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {C₂ : Precategory ℓ₃ ℓ₄}
    {ℓ₅ ℓ₆} {C₃ : Precategory ℓ₅ ℓ₆}
    {ℓ₇ ℓ₈} {C₄ : Precategory ℓ₇ ℓ₈} →
  Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₈) →
  (F : C₃ ⇨ C₄) (G : C₂ ⇨ C₃) {H : C₁ ⇨ C₂} →
  F ∙⇨ (G ∙⇨ H) ≡ (F ∙⇨ G) ∙⇨ H
∙⇨-assoc ext F G {H} = _≃_.from (equality-characterisation⇨ ext)
  ( refl _
  , (subst _ (refl _) (λ {_ _} → (F ∙⇨ G ∙⇨ H) ⊙_)  ≡⟨ subst-refl _ _ ⟩
     (λ {_ _} → (F ∙⇨ G ∙⇨ H) ⊙_)                   ∎)
  )

------------------------------------------------------------------------
-- Natural transformations

Natural-transformation :
  ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
  C ⇨ D → C ⇨ D → Type _
Natural-transformation {C} {D} F G =
  -- Morphisms.
  ∃ λ (γ : ∀ {X} → Hom D (F ⊚ X) (G ⊚ X)) →

  -- Naturality.
  ∀ {X Y} {f : Hom C X Y} → (G ⊙ f) ∙ γ ≡ γ ∙ (F ⊙ f)

  where
  open Precategory hiding (_∙_)
  open Precategory D using (_∙_)

-- A wrapper.

infix 4 _⇾_

record _⇾_ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
           {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
           (F G : C ⇨ D) : Type (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
  field
    natural-transformation : Natural-transformation F G

  open Precategory hiding (_∙_)
  open Precategory D using (_∙_)

  -- Morphisms.

  transformation : ∀ {X} → Hom D (F ⊚ X) (G ⊚ X)
  transformation = proj₁ natural-transformation

  -- Naturality.

  natural : ∀ {X Y} {f : Hom C X Y} →
            (G ⊙ f) ∙ transformation ≡ transformation ∙ (F ⊙ f)
  natural = proj₂ natural-transformation

opaque

  -- The naturality property is a proposition (assuming
  -- extensionality).

  naturality-propositional :
    ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
    Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
    {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄}
    (F G : C ⇨ D) →
    let open Precategory hiding (_∙_); open Precategory D using (_∙_) in
    {transformation : ∀ {X} → Hom D (F ⊚ X) (G ⊚ X)} →

    Is-proposition (∀ {X Y} {f : Hom C X Y} →
                    (G ⊙ f) ∙ transformation ≡
                    transformation ∙ (F ⊙ f))

  naturality-propositional {ℓ₁} {ℓ₂} ext {D} _ _ =
    implicit-Π-closure (lower-extensionality ℓ₂ lzero     ext) 1 λ _ →
    implicit-Π-closure (lower-extensionality ℓ₂ ℓ₁        ext) 1 λ _ →
    implicit-Π-closure (lower-extensionality ℓ₁ (ℓ₁ ⊔ ℓ₂) ext) 1 λ _ →
    Precategory.Hom-is-set D

  -- Natural transformation equality is equivalent to pointwise
  -- equality of the corresponding "transformations" (assuming
  -- extensionality).

  equality-characterisation⇾ :
    ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
    Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
    {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄}
    {F G : C ⇨ D} {γ δ : F ⇾ G} →

    (γ ≡ δ)
      ≃
    (∀ {X} → _⇾_.transformation γ {X = X} ≡
             _⇾_.transformation δ {X = X})

  equality-characterisation⇾ {ℓ₁} {ℓ₂} ext {F} {G} {γ} {δ} =
    γ ≡ δ                                                          ↝⟨ inverse $ Eq.≃-≡ $ ↔⇒≃ record
                                                                        { surjection = record
                                                                          { logical-equivalence = record
                                                                            { to   = _⇾_.natural-transformation
                                                                            ; from = λ γ → record { natural-transformation = γ }
                                                                            }
                                                                          ; right-inverse-of = refl
                                                                          }
                                                                        ; left-inverse-of = refl
                                                                        } ⟩
    _⇾_.natural-transformation γ ≡ _⇾_.natural-transformation δ    ↔⟨ inverse $ ignore-propositional-component
                                                                                  (naturality-propositional ext F G) ⟩
    (λ {X} → _⇾_.transformation γ {X = X}) ≡ _⇾_.transformation δ  ↝⟨ inverse $ Eq.≃-≡ (Eq.↔⇒≃ implicit-Π↔Π) ⟩

    (λ X → _⇾_.transformation γ {X = X}) ≡
    (λ X → _⇾_.transformation δ {X = X})                           ↝⟨ inverse $ Eq.extensionality-isomorphism
                                                                                  (lower-extensionality ℓ₂ (ℓ₁ ⊔ ℓ₂) ext) ⟩
    (∀ X → _⇾_.transformation γ {X = X} ≡
           _⇾_.transformation δ {X = X})                           ↔⟨ inverse implicit-Π↔Π ⟩□

    (∀ {X} → _⇾_.transformation γ {X = X} ≡
             _⇾_.transformation δ {X = X})                         □

  -- Natural transformations form sets (assuming extensionality).

  ⇾-set :
    ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
    Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
    {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D} →
    Is-set (F ⇾ G)
  ⇾-set {ℓ₁} {ℓ₂} ext {D} {F} {G} =
    let surj = record
          { logical-equivalence = record
            { to   = λ γ → record { natural-transformation = γ }
            ; from = _⇾_.natural-transformation
            }
          ; right-inverse-of = refl
          } in

    respects-surjection surj 2 $
      Σ-closure 2
        (implicit-Π-closure
           (lower-extensionality ℓ₂ (ℓ₁ ⊔ ℓ₂) ext) 2 λ _ →
         Precategory.Hom-is-set D)
        (λ _ → mono₁ 1 $ naturality-propositional ext F G)

-- Identity natural transformation.

id⇾ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
        {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
      (F : C ⇨ D) → F ⇾ F
id⇾ {C} {D} F =
  record { natural-transformation = id , nat }
  where
  open Precategory D

  opaque

    nat : ∀ {X Y} {f : Precategory.Hom C X Y} →
          (F ⊙ f) ∙ id ≡ id ∙ (F ⊙ f)
    nat {f} =
      (F ⊙ f) ∙ id  ≡⟨ right-identity ⟩
      F ⊙ f         ≡⟨ sym $ left-identity ⟩∎
      id ∙ (F ⊙ f)  ∎

-- Composition of natural transformations.

infixr 10 _∙⇾_

_∙⇾_ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
         {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
         {F G H : C ⇨ D} →
       G ⇾ H → F ⇾ G → F ⇾ H
_∙⇾_ {C} {D} {F} {G} {H} γ δ =
  record { natural-transformation = ε , nat }
  where
  open Precategory D
  open _⇾_

  ε : ∀ {X} → Hom (F ⊚ X) (H ⊚ X)
  ε = transformation γ ∙ transformation δ

  opaque

    nat : ∀ {X Y} {f : Precategory.Hom C X Y} →
          (H ⊙ f) ∙ ε ≡ ε ∙ (F ⊙ f)
    nat {f} =
      (H ⊙ f) ∙ (transformation γ ∙ transformation δ)  ≡⟨ assoc ⟩
      ((H ⊙ f) ∙ transformation γ) ∙ transformation δ  ≡⟨ cong (λ f → f ∙ _) $ natural γ ⟩
      (transformation γ ∙ (G ⊙ f)) ∙ transformation δ  ≡⟨ sym assoc ⟩
      transformation γ ∙ ((G ⊙ f) ∙ transformation δ)  ≡⟨ cong (_∙_ _) $ natural δ ⟩
      transformation γ ∙ (transformation δ ∙ (F ⊙ f))  ≡⟨ assoc ⟩∎
      (transformation γ ∙ transformation δ) ∙ (F ⊙ f)  ∎

-- Composition of functors and natural transformations.

infixr 10 _⇾∙⇨_ _⇨∙⇾_

_⇾∙⇨_ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
          {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
          {ℓ₅ ℓ₆} {E : Precategory ℓ₅ ℓ₆}
          {G H : D ⇨ E} →
        G ⇾ H → (F : C ⇨ D) → (G ∙⇨ F) ⇾ (H ∙⇨ F)
_⇾_.natural-transformation (γ ⇾∙⇨ _) = transformation , natural
  where
  open _⇾_ γ

_⇨∙⇾_ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
          {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
          {ℓ₅ ℓ₆} {E : Precategory ℓ₅ ℓ₆}
          {G H : C ⇨ D} →
        (F : D ⇨ E) → G ⇾ H → (F ∙⇨ G) ⇾ (F ∙⇨ H)
_⇾_.natural-transformation (_⇨∙⇾_ {C} {D} {E} {G} {H} F γ) = ε , nat
  where
  open Precategory
  open _⇾_ γ

  ε : ∀ {X} → Hom E (F ⊚ G ⊚ X) (F ⊚ H ⊚ X)
  ε = F ⊙ transformation

  opaque

    nat : ∀ {X Y} {f : Hom C X Y} →
          _∙_ E (F ⊙ H ⊙ f) ε ≡ _∙_ E ε (F ⊙ G ⊙ f)
    nat {f} =
      _∙_ E (F ⊙ H ⊙ f) (F ⊙ transformation)  ≡⟨ sym $ ⊙-∙ F ⟩
      F ⊙ _∙_ D (H ⊙ f) transformation        ≡⟨ cong (F ⊙_) natural ⟩
      F ⊙ _∙_ D transformation (G ⊙ f)        ≡⟨ ⊙-∙ F ⟩∎
      _∙_ E (F ⊙ transformation) (F ⊙ G ⊙ f)  ∎

------------------------------------------------------------------------
-- Functor precategories

-- Functor precategories are defined using extensionality.

infix 10 _^_

_^_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
      Precategory ℓ₁ ℓ₂ → Precategory ℓ₃ ℓ₄ →
      Extensionality (ℓ₃ ⊔ ℓ₄) (ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) →
      Precategory _ _
(D ^ C) ext = record
  { precategory =
        (C ⇨ D)
      , (λ F G → (F ⇾ G) , ⇾-set ext)
      , id⇾ _
      , _∙⇾_
      , _≃_.from (equality-characterisation⇾ ext) left-identity
      , _≃_.from (equality-characterisation⇾ ext) right-identity
      , _≃_.from (equality-characterisation⇾ ext) assoc
  }
  where
  open Precategory D

opaque

  -- The natural transformation γ is an isomorphism in (D ^ C) ext iff
  -- _⇾_.transformation γ {X = X} is an isomorphism in D for every X.

  natural-isomorphism-lemma :
    ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}
    (ext : Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄)) →
    {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄}
    {F G : C ⇨ D} {γ : F ⇾ G} → let open Precategory in

    Is-isomorphism ((D ^ C) ext) γ ⇔
    (∀ {X} → Is-isomorphism D (_⇾_.transformation γ {X = X}))

  natural-isomorphism-lemma ext {D} {F} {G} {γ} = record
    { to = λ { (δ , γδ , δγ) →
        transformation δ ,
        (transformation γ ∙ transformation δ  ≡⟨⟩
         transformation (γ ∙⇾ δ)              ≡⟨ cong (λ ε → transformation ε) γδ ⟩
         transformation (id⇾ G)               ≡⟨⟩
         id                                   ∎) ,
        (transformation δ ∙ transformation γ  ≡⟨⟩
         transformation (δ ∙⇾ γ)              ≡⟨ cong (λ ε → transformation ε) δγ ⟩
         transformation (id⇾ F)               ≡⟨⟩
         id                                   ∎) }
    ; from = λ iso →
        record { natural-transformation =
          proj₁ iso ,
          (λ {_ _ f} →
               (F ⊙ f) ∙ proj₁ iso                                     ≡⟨ sym left-identity ⟩
               id ∙ (F ⊙ f) ∙ proj₁ iso                                ≡⟨ cong (λ g → g ∙ (F ⊙ f) ∙ proj₁ iso) $ sym $ proj₂ (proj₂ iso) ⟩
               (proj₁ iso ∙ transformation γ) ∙ (F ⊙ f) ∙ proj₁ iso    ≡⟨ sym assoc ⟩
               proj₁ iso ∙ (transformation γ ∙ (F ⊙ f) ∙ proj₁ iso)    ≡⟨ cong (_ ∙_) assoc ⟩
               proj₁ iso ∙ ((transformation γ ∙ (F ⊙ f)) ∙ proj₁ iso)  ≡⟨ cong (λ g → _ ∙ (g ∙ _)) $ sym $ natural γ ⟩
               proj₁ iso ∙ (((G ⊙ f) ∙ transformation γ) ∙ proj₁ iso)  ≡⟨ cong (_ ∙_) $ sym assoc ⟩
               proj₁ iso ∙ (G ⊙ f) ∙ (transformation γ ∙ proj₁ iso)    ≡⟨ cong ((_ ∙_) ∘ ((G ⊙ f) ∙_)) $ proj₁ (proj₂ iso) ⟩
               proj₁ iso ∙ (G ⊙ f) ∙ id                                ≡⟨ assoc ⟩
               (proj₁ iso ∙ (G ⊙ f)) ∙ id                              ≡⟨ right-identity ⟩∎
               proj₁ iso ∙ (G ⊙ f)                                     ∎) } ,
        _≃_.from (equality-characterisation⇾ ext) (proj₁ (proj₂ iso)) ,
        _≃_.from (equality-characterisation⇾ ext) (proj₂ (proj₂ iso))
    }
    where
    open Precategory D
    open _⇾_

opaque

  -- If D is a category, then (D ^ C) ext is also a category.

  infix 10 _↑_

  _↑_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
        Category ℓ₁ ℓ₂ → Precategory ℓ₃ ℓ₄ →
        Extensionality (ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) →
        Category (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
  _↑_ {ℓ₁} {ℓ₂} {ℓ₃} {ℓ₄} D C ext = record { category =
    D^C ,

    (λ {F G} → _≃_.is-equivalence $ ↔⇒≃ $ record
       { surjection = record
         { logical-equivalence = record
           { to   = Precategory.≡→≅ D^C
           ; from = λ { (F⇾G , F⇾G-iso) →

               let γ : ∀ X → F ⊚ X ≅ G ⊚ X
                   γ _ = _⇾_.transformation F⇾G ,
                         _⇔_.to (natural-isomorphism-lemma ext₁) F⇾G-iso

                   ⊚F≡⊚G : _⊚_ F ≡ _⊚_ G
                   ⊚F≡⊚G = apply-ext ext₂ λ X →
                     F ⊚ X  ≡⟨ ≅→≡ (γ X) ⟩∎
                     G ⊚ X  ∎

                   cong-⊚F≡⊚G : ∀ {X} → cong (λ H → H X) ⊚F≡⊚G ≡ ≅→≡ (γ X)
                   cong-⊚F≡⊚G = cong-ext ext₂

                   ⊙F≡⊙G : _≡_ {A = ∀ {X Y} → HomC X Y → Hom (G ⊚ X) (G ⊚ Y)}
                               (subst (λ F → ∀ {X Y} → HomC X Y → Hom (F X) (F Y))
                                      ⊚F≡⊚G
                                      (_⊙_ F))
                               (_⊙_ G)
                   ⊙F≡⊙G =
                     implicit-extensionality (lower-extensionality ℓ₄ ℓ₁        ext) λ X →
                     implicit-extensionality (lower-extensionality ℓ₄ (ℓ₁ ⊔ ℓ₃) ext) λ Y →
                     apply-ext (lower-extensionality ℓ₃ (ℓ₁ ⊔ ℓ₃ ⊔ ℓ₄) ext) λ f →

                     subst (λ F → ∀ {X Y} → HomC X Y → Hom (F X) (F Y))
                           ⊚F≡⊚G (_⊙_ F) f                               ≡⟨ cong (λ H → H f) $ sym $
                                                                                 push-subst-implicit-application ⊚F≡⊚G
                                                                                   (λ F X → ∀ {Y} → HomC X Y → Hom (F X) (F Y)) ⟩
                     subst (λ F → ∀ {Y} → HomC X Y → Hom (F X) (F Y))
                           ⊚F≡⊚G (_⊙_ F) f                               ≡⟨ cong (λ H → H f) $ sym $
                                                                                 push-subst-implicit-application ⊚F≡⊚G
                                                                                   (λ F Y → HomC X Y → Hom (F X) (F Y)) ⟩
                     subst (λ F → HomC X Y → Hom (F X) (F Y))
                           ⊚F≡⊚G (_⊙_ F) f                               ≡⟨ sym $ push-subst-application ⊚F≡⊚G
                                                                                    (λ F _ → Hom (F X) (F Y)) ⟩
                     subst (λ F → Hom (F X) (F Y)) ⊚F≡⊚G (F ⊙ f)         ≡⟨ subst-∘ (uncurry Hom) (λ H → (H X , H Y)) ⊚F≡⊚G ⟩

                     subst (uncurry Hom)
                           (cong (λ H → (H X , H Y)) ⊚F≡⊚G) (F ⊙ f)      ≡⟨ cong (λ p → subst (uncurry Hom) p (F ⊙ f)) $ sym $
                                                                                 cong₂-cong-cong {eq = ⊚F≡⊚G} (λ H → H X) (λ H → H Y) _,_ ⟩
                     subst (uncurry Hom)
                           (cong₂ _,_ (cong (λ H → H X) ⊚F≡⊚G)
                                      (cong (λ H → H Y) ⊚F≡⊚G)) (F ⊙ f)  ≡⟨ cong₂ (λ p q → subst (uncurry Hom) (cong₂ _,_ p q) (F ⊙ f))
                                                                                  cong-⊚F≡⊚G cong-⊚F≡⊚G ⟩
                     subst (uncurry Hom)
                           (cong₂ _,_ (≅→≡ (γ X)) (≅→≡ (γ Y))) (F ⊙ f)   ≡⟨ Hom-, (≅→≡ (γ X)) (≅→≡ (γ Y)) ⟩

                     ≡→≅ (≅→≡ (γ Y)) ¹ ∙ (F ⊙ f) ∙ ≡→≅ (≅→≡ (γ X)) ⁻¹    ≡⟨ cong₂ (λ p q → p ¹ ∙ (F ⊙ f) ∙ q ⁻¹)
                                                                                  (_≃_.right-inverse-of ≡≃≅ _)
                                                                                  (_≃_.right-inverse-of ≡≃≅ _) ⟩
                     γ Y ¹ ∙ (F ⊙ f) ∙ γ X ⁻¹                            ≡⟨ assoc ⟩

                     (γ Y ¹ ∙ (F ⊙ f)) ∙ γ X ⁻¹                          ≡⟨ cong (_∙ γ X ⁻¹) $ sym $ _⇾_.natural F⇾G ⟩

                     ((G ⊙ f) ∙ γ X ¹) ∙ γ X ⁻¹                          ≡⟨ sym assoc ⟩

                     (G ⊙ f) ∙ γ X ¹ ∙ γ X ⁻¹                            ≡⟨ cong (_ ∙_) $ γ X ¹⁻¹ ⟩

                     (G ⊙ f) ∙ id                                        ≡⟨ right-identity ⟩∎

                     G ⊙ f                                               ∎

               in _≃_.from (equality-characterisation⇨ ext₁)
                           (⊚F≡⊚G , ⊙F≡⊙G) }
           }
         ; right-inverse-of = λ { (F⇾G , F⇾G-iso) →
             _≃_.from (Precategory.≡≃≡¹ D^C) $
             _≃_.from (equality-characterisation⇾ ext₁) λ {X} →
               _⇾_.transformation (proj₁ (Precategory.≡→≅ D^C _))         ≡⟨⟩

               _⇾_.transformation
                 (proj₁ (elim (λ {F G} _ → Precategory._≅_ D^C F G)
                              (λ _ → Precategory.id≅ D^C) _))             ≡⟨ elim
                                                                               (λ {F G} F≡G →
                                                                                  _⇾_.transformation (proj₁ (Precategory.≡→≅ D^C F≡G)) ≡
                                                                                  elim (λ {F G} _ → Hom (F X) (G X)) (λ _ → id) (cong _⊚_ F≡G))
                                                                               (λ F →
                   _⇾_.transformation
                     (proj₁ (elim (λ {F G} _ → Precategory._≅_ D^C F G)
                                  (λ _ → Precategory.id≅ D^C) (refl F)))          ≡⟨ cong (λ f → _⇾_.transformation (proj₁ f) {X = X}) $
                                                                                     elim-refl (λ {X Y} _ → Precategory._≅_ D^C X Y) _ ⟩
                   _⇾_.transformation {F = F}
                     (proj₁ (Precategory.id≅ D^C))                                ≡⟨⟩

                   id                                                             ≡⟨ sym $ elim-refl (λ {F G} _ → Hom (F X) (G X)) _ ⟩

                   elim (λ {F G} _ → Hom (F X) (G X))
                        (λ _ → id) (refl (_⊚_ F))                                 ≡⟨ cong (elim (λ {F G} _ → Hom (F X) (G X)) _) $
                                                                                     sym $ cong-refl _⊚_ ⟩∎
                   elim (λ {F G} _ → Hom (F X) (G X))
                        (λ _ → id) (cong _⊚_ (refl F))                            ∎)
                                                                               _ ⟩
               elim (λ {F G} _ → Hom (F X) (G X))
                    (λ _ → id) (cong _⊚_ _)                               ≡⟨ cong (elim (λ {F G} _ → Hom (F X) (G X)) (λ _ → id)) $
                                                                             cong-⊚-from-equality-characterisation⇨ _ _ _ ⟩
               elim (λ {F G} _ → Hom (F X) (G X)) (λ _ → id)
                    (apply-ext ext₂ λ Y →
                     ≅→≡ (_⇾_.transformation F⇾G {X = Y} , _))            ≡⟨ elim-ext ext₂ ⟩

               elim (λ {X Y} _ → Hom X Y) (λ _ → id)
                    (≅→≡ (_⇾_.transformation F⇾G {X = X} , _))            ≡⟨ elim
                                                                               (λ {X Y} X≡Y →
                                                                                  elim (λ {X Y} _ → Hom X Y) (λ _ → id) X≡Y ≡
                                                                                  proj₁ (≡→≅ X≡Y))
                                                                               (λ X →
                   elim (λ {X Y} _ → Hom X Y) (λ _ → id) (refl X)                 ≡⟨ elim-refl (λ {X Y} _ → Hom X Y) _ ⟩
                   id                                                             ≡⟨⟩
                   proj₁ id≅                                                      ≡⟨ cong proj₁ (sym ≡→≅-refl) ⟩∎
                   proj₁ (≡→≅ (refl X))                                           ∎ )
                                                                               _ ⟩

               proj₁ (≡→≅ (≅→≡ (_⇾_.transformation F⇾G {X = X} , _)))     ≡⟨ cong proj₁ (_≃_.right-inverse-of ≡≃≅ _) ⟩∎

               _⇾_.transformation F⇾G {X = X}                             ∎ }
           }
       ; left-inverse-of = λ F≡G →
           _≃_.from (equality-characterisation≡⇨ ext₁) (
              cong _⊚_ _                                           ≡⟨ cong-⊚-from-equality-characterisation⇨ _ _ _ ⟩

              (apply-ext ext₂ λ X →
               ≅→≡ ( _⇾_.transformation
                       (proj₁ $ Precategory.≡→≅ D^C F≡G) {X = X}
                   , _
                   ))                                              ≡⟨ elim
                                                                        (λ {F G} F≡G → (f : (X : _) → _) →
                                                                           (apply-ext ext₂ λ X →
                                                                            ≅→≡ (_⇾_.transformation (proj₁ $ Precategory.≡→≅ D^C F≡G) , f X)) ≡
                                                                           cong _⊚_ F≡G)
                                                                        (λ F _ →
                  (apply-ext ext₂ λ _ →
                   ≅→≡ ( _⇾_.transformation
                           (proj₁ $ Precategory.≡→≅ D^C (refl F))
                       , _
                       ))                                                  ≡⟨ (cong (apply-ext ext₂) $ apply-ext ext₂ λ X → cong ≅→≡ $
                                                                               Σ-≡,≡→≡
                                                                                 (cong (λ f → _⇾_.transformation (proj₁ f) {X = X}) $
                                                                                  Precategory.≡→≅-refl D^C)
                                                                                 (refl _)) ⟩
                  (apply-ext ext₂ λ _ →
                   ≅→≡ ( _⇾_.transformation {F = F}
                           (proj₁ $ Precategory.id≅ D^C)
                       , _
                       ))                                                  ≡⟨⟩

                  apply-ext ext₂ (λ _ → ≅→≡ (id , _))                      ≡⟨ (cong (apply-ext ext₂) $ apply-ext ext₂ λ _ →
                                                                               cong ≅→≡ $ _≃_.from ≡≃≡¹ $ refl _) ⟩

                  apply-ext ext₂ (λ _ → ≅→≡ id≅)                           ≡⟨ (cong (apply-ext ext₂) $ apply-ext ext₂ λ _ →
                                                                               ≅→≡-refl) ⟩

                  apply-ext ext₂ (λ X → refl (F ⊚ X))                      ≡⟨ ext-refl ext₂ ⟩

                  refl (_⊚_ F)                                             ≡⟨ sym $ cong-refl _ ⟩∎

                  cong _⊚_ (refl F)                                        ∎)

                                                                        F≡G _ ⟩∎
              cong _⊚_ F≡G                                         ∎)
       }) }
    where
    open Category D
    open Precategory C using () renaming (Hom to HomC)

    ext₁ : Extensionality (ℓ₃ ⊔ ℓ₄) (ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
    ext₁ = lower-extensionality lzero ℓ₁ ext

    ext₂ : Extensionality ℓ₃ ℓ₁
    ext₂ = lower-extensionality ℓ₄ (ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) ext

    D^C : Precategory (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
    D^C = (precategory ^ C) ext₁