open import 1Lab.Path.Cartesian

open import Cat.Prelude

import Cat.Reasoning

module Cat.Functor.Base where

Functor precategories🔗

Fix a pair of (completely arbitrary!) precategories and We’ll show how to make the type of functors into a precategory on its own right, with the natural transformations as the morphisms. First, given we construct the identity natural transformation by having every component be the identity:

private variable
  o o₁ o₂ ℓ ℓ₁ ℓ₂ : Level
  B C D E : Precategory o ℓ
  F G : Functor C D

private module Pc = Precategory
open Functor
open _=>_

module _ {C : Precategory o ℓ} {D : Precategory o₁ ℓ₁} where
  private
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D

  idnt : {F : Functor C D} → F => F
  idnt .η _              = D.id
  idnt .is-natural _ _ _ = D.id-comm-sym

Moreover, if we have a pair of composable-looking natural transformations and then we can indeed make their pointwise composite into a natural transformation:

  _∘nt_ : ∀ {F G H : Functor C D} → G => H → F => G → F => H
  (f ∘nt g) .η x = f .η x D.∘ g .η x
  _∘nt_ {F} {G} {H} f g .is-natural x y h =
    (f .η y D.∘ g .η y) D.∘ F .F₁ h ≡⟨ D.pullr (g .is-natural x y h) ⟩≡
    f .η y D.∘ G .F₁ h D.∘ g .η x   ≡⟨ D.extendl (f .is-natural x y h) ⟩≡
    H .F₁ h D.∘ f .η x D.∘ g .η x   ∎

  infixr 40 _∘nt_

Since we already know that identity of natural transformations is determined by identity of the underlying family of morphisms, and the identities and composition we’ve just defined are componentwise just identity and composition in then the category laws we have to prove are, once again, those of 

Cat[_,_]
  : Precategory o ℓ → Precategory o₁ ℓ₁
  → Precategory (o ⊔ ℓ ⊔ o₁ ⊔ ℓ₁) (o ⊔ ℓ ⊔ ℓ₁)
Cat[ C , D ] .Pc.Ob          = Functor C D
Cat[ C , D ] .Pc.Hom         = _=>_
Cat[ C , D ] .Pc.Hom-set F G = hlevel 2

Cat[ C , D ] .Pc.id  = idnt
Cat[ C , D ] .Pc._∘_ = _∘nt_

Cat[ C , D ] .Pc.idr f       = ext λ x → D .Pc.idr _
Cat[ C , D ] .Pc.idl f       = ext λ x → D .Pc.idl _
Cat[ C , D ] .Pc.assoc f g h = ext λ x → D .Pc.assoc _ _ _

We’ll also need the following foundational tool, characterising paths between functors. It says that, given a homotopy between the object-parts of functors and, over this, an identification between the actions of and on morphisms, we can construct a path

Paths between functors🔗

Functor-path
  : {F G : Functor C D}
  → (p0 : ∀ x → F .F₀ x ≡ G .F₀ x)
  → (p1 : ∀ {x y} (f : C .Pc.Hom x y)
        → PathP (λ i → D .Pc.Hom (p0 x i) (p0 y i)) (F .F₁ f) (G .F₁ f))
  → F ≡ G

Note that this lemma is a bit unusual: we’re characterising the identity type of the objects of a precategory, rather than, as is more common, the morphisms of a precategory. However, this characterisation will let us swiftly establish necessary conditions for univalence of functor categories.

Functor-pathp
  : {C : I → Precategory o ℓ} {D : I → Precategory o₁ ℓ₁}
    {F : Functor (C i0) (D i0)} {G : Functor (C i1) (D i1)}
  → (p0 : ∀ (p : ∀ i → C i .Pc.Ob) → PathP (λ i → D i .Pc.Ob) (F .F₀ (p i0)) (G .F₀ (p i1)))
  → (p1 : ∀ {x y : ∀ i → _}
        → (r : ∀ i → C i .Pc.Hom (x i) (y i))
        → PathP (λ i → D i .Pc.Hom (p0 x i) (p0 y i))
                (F .F₁ (r i0)) (G .F₁ (r i1)))
  → PathP (λ i → Functor (C i) (D i)) F G
Functor-pathp {C = C} {D} {F} {G} p0 p1 = fn where
  open Pc
  cob : I → Type _
  cob = λ i → C i .Ob

  exth
    : ∀ i j (x y : C i .Ob) (f : C i .Hom x y)
    → C i .Hom (coe cob i i x) (coe cob i i y)
  exth i j x y f =
    comp (λ j → C i .Hom (coei→i cob i x (~ j ∨ i)) (coei→i cob i y (~ j ∨ i)))
    ((~ i ∧ ~ j) ∨ (i ∧ j))
    λ where
      k (k = i0) → f
      k (i = i0) (j = i0) → f
      k (i = i1) (j = i1) → f

  actm
    : ∀ i (x y : C i .Ob) f
    → D i .Hom (p0 (λ j → coe cob i j x) i) (p0 (λ j → coe cob i j y) i)
  actm i x y f =
    p1 {λ j → coe cob i j x} {λ j → coe cob i j y}
      (λ j → coe (λ j → C j .Hom (coe cob i j x) (coe cob i j y)) i j (exth i j x y f))
      i

  fn : PathP (λ i → Functor (C i) (D i)) F G
  fn i .F₀ x =
    p0 (λ j → coe cob i j x)
      i
  fn i .F₁ {x} {y} f = actm i x y f
  fn i .F-id {x} =
    hcomp (∂ i) λ where
      j (i = i0) → D i .Hom-set (F .F₀ x) (F .F₀ x) (F .F₁ (C i .id)) (D i .id) base (F .F-id) j
      j (i = i1) → D i .Hom-set (G .F₀ x) (G .F₀ x) (G .F₁ (C i .id)) (D i .id) base (G .F-id) j
      j (j = i0) → base
    where
      base = coe0→i (λ i → (x : C i .Ob) → actm i x x (C i .id) ≡ D i .id) i
        (λ _ → F .F-id) x
  fn i .F-∘ {x} {y} {z} f g =
    hcomp (∂ i) λ where
      j (i = i0) → D i .Hom-set (F .F₀ x) (F .F₀ z) _ _ base (F .F-∘ f g) j
      j (i = i1) → D i .Hom-set (G .F₀ x) (G .F₀ z) _ _ base (G .F-∘ f g) j
      j (j = i0) → base
    where
      base = coe0→i (λ i → (x y z : C i .Ob) (f : C i .Hom y z) (g : C i .Hom x y)
                         → actm i x z (C i ._∘_ f g)
                         ≡ D i ._∘_ (actm i y z f) (actm i x y g)) i
        (λ _ _ _ → F .F-∘) x y z f g

Functor-path p0 p1 i .F₀ x = p0 x i
Functor-path p0 p1 i .F₁ f = p1 f i
Functor-path {C = C} {D = D} {F = F} {G = G} p0 p1 i .F-id =
  is-prop→pathp (λ j → D .Pc.Hom-set _ _ (p1 (C .Pc.id) j) (D .Pc.id))
    (F .F-id) (G .F-id) i
Functor-path {C = C} {D = D} {F = F} {G = G} p0 p1 i .F-∘ f g =
  is-prop→pathp (λ i → D .Pc.Hom-set _ _ (p1 (C .Pc._∘_ f g) i) (D .Pc._∘_ (p1 f i) (p1 g i)))
    (F .F-∘ f g) (G .F-∘ f g) i

Action on isomorphisms🔗

module F-iso {C : Precategory o ℓ} {D : Precategory o₁ ℓ₁} (F : Functor C D) where
  private module _ where
    module C = Cat.Reasoning C
    module D = Cat.Reasoning D
    open Cat.Reasoning using (_≅_ ; Inverses)
    open _≅_ public
    open Inverses public

We have also to make note of the following fact: absolutely all functors preserve isomorphisms, and, more generally, preserve invertibility.

  F-map-iso : ∀ {x y} → x C.≅ y → F · x D.≅ F · y
  F-map-iso x .to       = F .F₁ (x .to)
  F-map-iso x .from     = F .F₁ (x .from)
  F-map-iso x .inverses =
    record { invl = sym (F .F-∘ _ _) ∙ ap (F .F₁) (x .invl) ∙ F .F-id
           ; invr = sym (F .F-∘ _ _) ∙ ap (F .F₁) (x .invr) ∙ F .F-id
           }
    where module x = C._≅_ x

  F-map-invertible : ∀ {x y} {f : C.Hom x y} → C.is-invertible f → D.is-invertible (F .F₁ f)
  F-map-invertible inv =
    D.make-invertible (F .F₁ _)
      (sym (F .F-∘ _ _) ∙∙ ap (F .F₁) x.invl ∙∙ F .F-id)
      (sym (F .F-∘ _ _) ∙∙ ap (F .F₁) x.invr ∙∙ F .F-id)
    where module x = C.is-invertible inv

If the categories the functor maps between are univalent, there is a competing notion of preserving isomorphisms: the action on paths of the object-part of the functor. We first turn the isomorphism into a path (using univalence of the domain), run it through the functor, then turn the resulting path back into an isomorphism. Fortunately, functors are already coherent enough to ensure that these actions agree:

  F-map-path
    : (ccat : is-category C) (dcat : is-category D)
    → ∀ {x y} (i : x C.≅ y)
    → ap· F (Univalent.iso→path ccat i) ≡ Univalent.iso→path dcat (F-map-iso i)
  F-map-path ccat dcat {x} = Univalent.J-iso ccat P pr where
    P : (b : C.Ob) → C.Isomorphism x b → Type _
    P b im = ap· F (Univalent.iso→path ccat im)
           ≡ Univalent.iso→path dcat (F-map-iso im)

    pr : P x C.id-iso
    pr =
      ap· F (Univalent.iso→path ccat C.id-iso) ≡⟨ ap (ap· F) (Univalent.iso→path-id ccat) ⟩≡
      ap· F refl                               ≡˘⟨ Univalent.iso→path-id dcat ⟩≡˘
      dcat .to-path D.id-iso                   ≡⟨ ap (dcat .to-path) (ext (sym (F .F-id))) ⟩≡
      dcat .to-path (F-map-iso C.id-iso)       ∎

  ap-F₀-to-iso
    : ∀ {y z}
    → (p : y ≡ z) → path→iso (ap· F p) ≡ F-map-iso (path→iso p)
  ap-F₀-to-iso {y} =
    J (λ _ p → path→iso (ap· F p) ≡ F-map-iso (path→iso p))
      (D.≅-pathp (λ _ → F .F₀ y) (λ _ → F .F₀ y)
        (Regularity.fast! (sym (F .F-id))))

  ap-F₀-iso
    : ∀ (cc : is-category C) {y z : C.Ob}
    → (p : y C.≅ z) → path→iso (ap· F (cc .to-path p)) ≡ F-map-iso p
  ap-F₀-iso cc p = ap-F₀-to-iso (cc .to-path p)
                 ∙ ap F-map-iso (Univalent.iso→path→iso cc p)

open F-iso public

Presheaf precategories🔗

Of principal importance among the functor categories are those to the category these are the presheaf categories.

PSh : ∀ κ {o ℓ} → Precategory o ℓ → Precategory _ _
PSh κ C = Cat[ C ^op , Sets κ ]