module Cat.Internal.Functor.Outer
  {o ℓ} {C : Precategory o ℓ}

Outer functors🔗

The category is not strict, so it is not internal to any category of sets, even setting aside size issues. However, still plays an important role in (strict) category theory, by passing to the copresheaf categories

We wish to relativize this to an arbitrary base category not just Specifically, if is a category internal to we want to define “functor from ” — which we call an outer functor1. We will employ the fibration/family correspondence: a family of sets is the same as a function — and we know how to relativise functions!

module _ (ℂ : Internal-cat) where
  open Cat.Internal.Reasoning ℂ

  record Outer-functor : Type (o ⊔ ℓ) where

The first piece of data we require is some object that will act like the disjoint union of the image of our functor. If the base category were this would be the type The next piece of data, corresponds to the first projection morphism: it assigns (generalised) objects of to objects of

      ∫P : Ob
      P₀ : ∀ {Γ} → Hom Γ ∫P → Hom Γ C₀

The next data captures how morphisms act on the fibres. Since the family-fibration correspondence takes dependency to sectioning, we require an assigment sending maps to maps which satisfy

      P₁ : ∀ {Γ} (px : Hom Γ ∫P) {y : Hom Γ C₀} → Homi (P₀ px) y → Hom Γ ∫P
      P₁-tgt : ∀ {Γ} (px : Hom Γ ∫P) {y : Hom Γ C₀}
             → (f : Homi (P₀ px) y) → y ≡ P₀ (P₁ px f)

Next, we have the functoriality conditions, which are straightforward (modulo indexing).

      P-id : ∀ {Γ} (px : Hom Γ ∫P) → P₁ px (idi (P₀ px)) ≡ px
      P-∘ : ∀ {Γ} (px : Hom Γ ∫P) {y z : Hom Γ C₀} (f : Homi y z) (g : Homi (P₀ px) y)
          → P₁ px (f ∘i g) ≡ P₁ (P₁ px g) (adjusti (P₁-tgt px g) refl f)

Finally, the naturality conditions that allow us to work using generalized objects.

      P₀-nat : ∀ {Γ Δ} → (px : Hom Δ ∫P) → (σ : Hom Γ Δ) → P₀ px ∘ σ ≡ P₀ (px ∘ σ)
      P₁-nat : ∀ {Γ Δ} (px : Hom Δ ∫P) {y : Hom Δ C₀} (f : Homi (P₀ px) y) (σ : Hom Γ Δ)
        → P₁ px f ∘ σ ≡ P₁ (px ∘ σ) (adjusti (P₀-nat px σ) refl (f [ σ ]))

open Outer-functor

Another perspective on outer functors is that they are the internal discrete opfibrations over The object is the total category, the map is the fibration itself, and captures the lifting into opcartesian maps.

We can obtain internal discrete fibrations by looking at outer functors from the internal opposite category of

Internal Hom functors🔗

The canonical example of an outer functor is the internal analog of the hom functor We require the following data: is finitely complete, is a category internal to and is a global object of — an object of in the empty context.

module _ (pb : has-pullbacks C) (term : Terminal C) (ℂ : Internal-cat) where
  open Cat.Internal.Reasoning ℂ
  open Pullbacks C pb
  open Terminal term

  Internal-hom-from : (x : Hom top C₀) → Outer-functor ℂ
  Internal-hom-from x = outf where

Recall that defining an outer functor on requires choosing an object to play the role of total space. For the outer functor corresponding to a Hom-functor, this ought to be the object of morphisms with domain We can encode this internally with the following pullback:

The projection from the total space to takes a generalized element of to its codomain. The lifting morphism follows from the universal property of the pullback.

    open Pullback (pb src x) renaming (apex to Cₓ)

    outf : Outer-functor ℂ
    outf .∫P = Cₓ
    outf .P₀ fₓ = tgt ∘ p₁ ∘ fₓ
    outf .P₁ fₓ {y = y} g = universal coh
      module hom-from-action where abstract
        coh : src ∘ (g ∘i homi (p₁ ∘ fₓ)) .ihom ≡ x ∘ !
        coh =
          src ∘ (g ∘i homi (p₁ ∘ fₓ)) .ihom ≡⟨ (g ∘i homi (p₁ ∘ fₓ)) .has-src ⟩≡
          src ∘ p₁ ∘ fₓ ≡⟨ pulll square ⟩≡
          (x ∘ p₂) ∘ fₓ ≡⟨ pullr (sym (!-unique _)) ⟩≡
          x ∘ ! ∎
The functoriality constraint is analogous to that for the ordinary though here it is obscured by all the pullbacks. The naturality constraints similarly follow from uniqueness of maps into a limit.
    outf .P₁-tgt fₓ {y = y} g = tgt-coh where abstract
      tgt-coh : y ≡ tgt ∘ p₁ ∘ universal (hom-from-action.coh fₓ g)
      tgt-coh =
        y                                 ≡˘⟨ (g ∘i homi (p₁ ∘ fₓ)) .has-tgt ⟩≡˘
        tgt ∘ (g ∘i homi (p₁ ∘ fₓ)) .ihom ≡˘⟨ ap (tgt ∘_) p₁∘universal ⟩≡˘
        tgt ∘ p₁ ∘ universal _            ∎
    outf .P-id fₓ =
      sym $ unique (sym (ap ihom (idli _))) (sym (!-unique _))
    outf .P-∘ fₓ g h = unique
      ∙ ap ihom (sym $ associ _ _ _)
      ∙ ∘i-ihom
          (sym (ap (src ∘_) p₁∘universal ∙ (h ∘i homi (p₁ ∘ fₓ)) .has-src))
          (sym (ap (tgt ∘_) p₁∘universal ∙ (h ∘i homi (p₁ ∘ fₓ)) .has-tgt))
          refl refl (sym p₁∘universal))
    outf .P₀-nat fₓ σ = sym (assoc _ _ _) ∙ ap (tgt ∘_) (sym (assoc _ _ _))
    outf .P₁-nat fₓ g σ = unique
      (pulll p₁∘universal
        ∙ ap ihom (∘i-nat g (homi (p₁ ∘ fₓ)) σ)
        ∙ ∘i-ihom
            (sym (assoc _ _ _) ∙ ap (src ∘_) (sym (assoc _ _ _)))
            (sym (assoc _ _ _) ∙ ap (tgt ∘_) (sym (assoc _ _ _)))
            refl refl (sym (assoc _ _ _)))
      (sym (!-unique _))

The contravariant internal functor is defined by duality, which carries “pullback along ” to “pullback along ”. This outer functor plays the role of the Yoneda embedding.

  Internal-hom-into : (x : Hom top C₀) → Outer-functor (ℂ ^opi)
  Internal-hom-into x = outf where
    open Pullback (pb tgt x) renaming (apex to Cₓ)
We omit this construction due to its similarity with the covariant construction, performed above.
    outf : Outer-functor (ℂ ^opi)
    outf .∫P = Cₓ
    outf .P₀ fₓ = src ∘ p₁ ∘ fₓ
    outf .P₁ fₓ g = universal coh
      module hom-into-action where abstract
        coh : tgt ∘ (homi (p₁ ∘ fₓ) ∘i op-ihom g) .ihom ≡ x ∘ !
        coh =
          tgt ∘ (homi (p₁ ∘ fₓ) ∘i op-ihom g) .ihom ≡⟨ (homi (p₁ ∘ fₓ) ∘i op-ihom g) .has-tgt ⟩≡
          tgt ∘ p₁ ∘ fₓ ≡⟨ pulll square ⟩≡
          (x ∘ p₂) ∘ fₓ ≡⟨ pullr (sym (!-unique _)) ⟩≡
          x ∘ ! ∎
    outf .P₁-tgt fₓ {y} g = src-coh where abstract
      src-coh : y ≡ src ∘ p₁ ∘ universal (hom-into-action.coh fₓ g)
      src-coh =
        sym (ap (src ∘_) p₁∘universal
        ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom g) .has-src)
    outf .P-id fₓ =
      sym $ unique (sym (ap ihom (idri _))) (sym (!-unique _))
    outf .P-∘ fₓ g h =
         ∙ ap ihom (associ _ _ _)
         ∙ ∘i-ihom refl
             (sym (ap (src ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-src))
             (sym (ap (tgt ∘_) p₁∘universal ∙ (homi (p₁ ∘ fₓ) ∘i op-ihom h) .has-tgt))
             (sym p₁∘universal) refl)
    outf .P₀-nat fₓ σ =
      sym (assoc _ _ _)
      ∙ ap (src ∘_) (sym (assoc _ _ _))
    outf .P₁-nat fₓ g σ =
        (pulll p₁∘universal
        ∙ ap ihom (∘i-nat _ _ _)
        ∙ ∘i-ihom refl
             (sym (assoc _ _ _) ∙ ap (src ∘_) (sym (assoc _ _ _)))
             (sym (assoc _ _ _) ∙ ap (tgt ∘_) (sym (assoc _ _ _)))
             (sym (assoc _ _ _)) refl)
        (sym (!-unique _))

Outer natural transformations🔗

If is a category, is internal to and are two outer functors on we can define the outer natural transformations They are (mostly) given by transformations to together with a bit of naturality data.

module _ {ℂ : Internal-cat} where
  open Internal-cat ℂ
  record _=>o_ (P Q : Outer-functor ℂ) : Type (o ⊔ ℓ) where
      ηo : ∀ {Γ} → Hom Γ (P .∫P) → Hom Γ (Q .∫P)

The first condition corresponds to indexing: Outer natural transformations map elements of over to elements of over

      ηo-fib : ∀ {Γ} (px : Hom Γ (P .∫P)) → Q .P₀ (ηo px) ≡ P .P₀ px

Over this coherence, we can state the naturality condition. It should be familiar, since, modulo the aforementioned coherence, it says

      is-naturalo : ∀ {Γ : Ob} (px : Hom Γ (P .∫P)) (y : Hom Γ C₀)
        → (f : Homi (P .P₀ px) y)
        → ηo (P .P₁ px f) ≡ Q .P₁ (ηo px) (adjusti (sym (ηo-fib px)) refl f)

The final naturality condition is stability under substitution, allowing us to work in the internal language of

      ηo-nat : ∀ {Γ Δ} (px : Hom Δ (P .∫P)) (σ : Hom Γ Δ) → ηo px ∘ σ ≡ ηo (px ∘ σ)

  open _=>o_

Some outer functors🔗

One important outer functor is the constant outer functor on an object which can be constructed if has products. This is the internalized version of the chaotic bifibration.

The total space of this functor is the product and the projection map is simply the second projection.

  ConstO : (X : Ob) → Outer-functor ℂ
  ConstO X .∫P = X ⊗₀ C₀
  ConstO X .P₀ f = π₂ ∘ f

Lifting is given by the universal map into the product.

  ConstO X .P₁ px {y} f = ⟨ π₁ ∘ px , y ⟩
  ConstO X .P₁-tgt px {y = y} f = sym π₂∘⟨⟩

For once, the naturality constraints are not egregious: In fact, since they are all facts about products, they can all be solved automatically.

  ConstO X .P-id px = products! C prods
  ConstO X .P-∘ px f g = products! C prods
  ConstO X .P₀-nat px σ = sym (assoc _ _ _)
  ConstO X .P₁-nat px f σ = products! C prods

If is a map in then it defines an outer natural transformation between the associated constant outer functors. Here too we can apply automation to satisfy the coherence constraints.

  const-nato : ∀ {X Y : Ob} → Hom X Y → ConstO X =>o ConstO Y
  const-nato f .ηo g = ⟨ f ∘ π₁ ∘ g , π₂ ∘ g ⟩
  const-nato f .ηo-fib px          = products! C prods
  const-nato f .is-naturalo px y g = products! C prods
  const-nato f .ηo-nat px σ        = products! C prods

  1. The terminology here is somewhat inconsistent. (Borceux 1994) calls these functors internal base-valued functors, while in (Mac Lane and Moerdijk 1994) they are referred to as category actions.↩︎