module Cat.Internal.Functor.Outer
  {o β„“} {C : Precategory o β„“}
  where

Outer FunctorsπŸ”—

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

We wish to relativize this to an arbitrary base category C\mathcal{C}, not just Sets\mathbf{Sets}. Specifically, if C\mathbb{C} is a category internal to C\mathcal{C}, we want to define β€œfunctor from Cβ†’C\mathbb{C} \to \mathcal{C}” β€” which we call an outer functor1. We will employ the fibration/family correspondence: a family of sets Bβ†’SetsB \to \mathbf{Sets} is the same as a function Eβ†’BE \to B β€” and we know how to relativise functions!

module _ (β„‚ : Internal-cat) where
  open Cat.Internal.Reasoning β„‚

  record Outer-functor : Type (o βŠ” β„“) where
    no-eta-equality

The first piece of data we require is some object P:CP : \mathcal{C} that will act like the disjoint union of the image of our functor. If the base category were Sets\mathbf{Sets}, this would be the type Ξ£(x:C)P(x)\Sigma_(x : \mathbb{C}) P(x). The next piece of data, P0P_0, corresponds to the first projection morphism: it assigns (generalised) objects of PP to objects of C\mathbb{C}.

    field
      ∫P : Ob
      Pβ‚€ : βˆ€ {Ξ“} β†’ Hom Ξ“ ∫P β†’ Hom Ξ“ Cβ‚€

The next data captures how C\mathbb{C}’s morphisms act on the fibres. Since the family-fibration correspondence takes dependency to sectioning, we require an assigment sending maps f:P0(x)β†’yf : P_0(x) \to y to maps P1(f):Ξ“β†’PP_1(f) : \Gamma \to P, which satisfy y=P0(P1(f))y = P_0(P_1(f)).

      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 C\mathbb{C}. The object PP is the total space, the map P0P_0 is the fibration itself, and P1P_1 captures the lifting into opcartesian maps.

We can obtain internal discrete fibrations by looking at outer functors from the internal opposite category of C\mathbb{C}.

Internal Hom FunctorsπŸ”—

The canonical example of an outer functor is the internal analog of the hom functor C(X,βˆ’)\mathcal{C}(X,-). We require the following data: C\mathcal{C} is finitely complete, C\mathbb{C} is a category internal to C\mathcal{C}, and x:C(⊀,C0)x : \mathcal{C}(\top, \mathbb{C}_0) is a global object of C\mathbb{C} β€” an object of C\mathbb{C} 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 C\mathbb{C} requires choosing an object P:CP : \mathcal{C} 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 xx. We can encode this internally with the following pullback:

The projection from the total space to C0C_0 takes a generalized element of CxC_x to its codomain. The lifting morphism P1P_1 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 Hom\mathbf{Hom}-functors, 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
      (pβ‚βˆ˜universal
      βˆ™ 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))
      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 Hom\mathbf{Hom} functor is defined by duality, which carries β€œpullback along $1\$1” to β€œpullback along $1\$1.”. 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 =
      unique
        (pβ‚βˆ˜universal
         βˆ™ 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)
        pβ‚‚βˆ˜universal
    outf .Pβ‚€-nat fβ‚“ Οƒ =
      sym (assoc _ _ _)
      βˆ™ ap (src ∘_) (sym (assoc _ _ _))
    outf .P₁-nat fβ‚“ g Οƒ =
      unique
        (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 C\mathcal{C} is a category, C\mathbb{C} is internal to C\mathcal{C}, and P,QP, Q are two outer functors on C\mathbb{C}, we can define the outer natural transformations Pβ†’QP \to Q: They are (mostly) given by transformations C(βˆ’,∫P)\mathcal{C}(-, \int P) to C(βˆ’,∫Q)\mathcal{C}(-, \int Q), together with a bit of naturality data.

module _ {β„‚ : Internal-cat} where
  open Internal-cat β„‚
  record _=>o_ (P Q : Outer-functor β„‚) : Type (o βŠ” β„“) where
    no-eta-equality
    field
      Ξ·o : βˆ€ {Ξ“} β†’ Hom Ξ“ (P .∫P) β†’ Hom Ξ“ (Q .∫P)

The first condition corresponds to indexing: Outer natural transformations map elements of ∫P\int P over xx to elements of ∫Q\int Q over xx.

      Ξ·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 Ξ·P1(f)=Q1(fΞ·)\eta P_1(f) = Q_1(f\eta).

      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 C\mathcal{C}.

      Ξ·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 X:CX : \mathcal{C}, which can be constructed if C\mathcal{C} has products. This is the internalized version of the chaotic bifibration.

The total space of this functor is the product XΓ—C0X \times \mathbb{C}_0, 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 x→yx \to y is a map in C\mathcal{C}, 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.β†©οΈŽ


References