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

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
    no-eta-equality

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

    field
      ∫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
      (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 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 =
      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 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
    no-eta-equality
    field
      Ξ·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.β†©οΈŽ


References