open import Cat.Diagram.Product.Solver
open import Cat.Internal.Opposite
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Prelude

import Cat.Internal.Reasoning
import Cat.Internal.Base
import Cat.Reasoning

module Cat.Internal.Functor.Outer
{o β} {C : Precategory o β}
where

open import Cat.Reasoning C
open import Cat.Internal.Base C
open Internal-hom


# Outer functorsπ

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

We wish to relativize this to an arbitrary base category $\mathcal{C}$, not just $\mathbf{Sets}$. Specifically, if $\mathbb{C}$ is a category internal to $\mathcal{C}$, we want to define βfunctor from $\mathbb{C} \to \mathcal{C}$β β which we call an outer functor1. We will employ the fibration/family correspondence: a family of sets $B \to \mathbf{Sets}$ is the same as a function $E \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 : \mathcal{C}$ that will act like the disjoint union of the image of our functor. If the base category were $\mathbf{Sets}$, this would be the type $\Sigma_(x : \mathbb{C}) P(x)$. The next piece of data, $P_0$, corresponds to the first projection morphism: it assigns (generalised) objects of $P$ to objects of $\mathbb{C}$.

    field
β«P : Ob
Pβ : β {Ξ} β Hom Ξ β«P β Hom Ξ Cβ


The next data captures how $\mathbb{C}$βs morphisms act on the fibres. Since the family-fibration correspondence takes dependency to sectioning, we require an assigment sending maps $f : P_0(x) \to y$ to maps $P_1(f) : \Gamma \to P$, which satisfy $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 $\mathbb{C}$. The object $P$ is the total category, the map $P_0$ is the fibration itself, and $P_1$ captures the lifting into opcartesian maps.

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

## Internal Hom functorsπ

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

The projection from the total space to $C_0$ takes a generalized element of $C_x$ to its codomain. The lifting morphism $P_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 $\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 $\mathbf{Hom}$ functor is defined by duality, which carries βpullback along $\operatorname{src}$β to βpullback along $\operatorname{tgt}$.β. 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 $\mathcal{C}$ is a category, $\mathbb{C}$ is internal to $\mathcal{C}$, and $P, Q$ are two outer functors on $\mathbb{C}$, we can define the outer natural transformations $P \to Q$: They are (mostly) given by transformations $\mathcal{C}(-, \int P)$ to $\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 $\int P$ over $x$ to elements of $\int Q$ over $x$.

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

      Ξ·o-nat : β {Ξ Ξ} (px : Hom Ξ (P .β«P)) (Ο : Hom Ξ Ξ) β Ξ·o px β Ο β‘ Ξ·o (px β Ο)

open _=>o_

  Outer-nat-path
: β {F G : Outer-functor β} {Ξ± Ξ² : F =>o G}
β (β {Ξ} (px : Hom Ξ (F .β«P)) β Ξ± .Ξ·o px β‘ Ξ² .Ξ·o px)
β Ξ± β‘ Ξ²
Outer-nat-path p i .Ξ·o px = p px i
Outer-nat-path {G = G} {Ξ± = Ξ±} {Ξ² = Ξ²} p i .Ξ·o-fib px =
is-propβpathp (Ξ» i β Hom-set _ _ (G .Pβ (p px i)) _)
(Ξ± .Ξ·o-fib px)
(Ξ² .Ξ·o-fib px) i
Outer-nat-path {F = F} {G = G} {Ξ± = Ξ±} {Ξ² = Ξ²} p i .is-naturalo px y f j =
is-setβsquarep (Ξ» i j β Hom-set _ _)
(p (F .Pβ px f))
(Ξ± .is-naturalo px y f)
(Ξ² .is-naturalo px y f)
(Ξ» i β G .Pβ (p px i)
(adjusti (sym (Outer-nat-path {Ξ± = Ξ±} {Ξ² = Ξ²} p i .Ξ·o-fib px)) refl f))
i j
Outer-nat-path {Ξ± = Ξ±} {Ξ² = Ξ²} p i .Ξ·o-nat px Ο =
is-propβpathp (Ξ» i β Hom-set _ _ (p px i β Ο) (p (px β Ο) i))
(Ξ± .Ξ·o-nat px Ο)
(Ξ² .Ξ·o-nat px Ο) i

private unquoteDecl nat-eqv = declare-record-iso nat-eqv (quote _=>o_)

Outer-nat-is-set
: β {F G : Outer-functor β} β is-set (F =>o G)
Outer-nat-is-set = Isoβis-hlevel 2 nat-eqv hlevel!

instance
H-Level-Outer-nat
: β {β : Internal-cat} {F G : Outer-functor β} {n}
β H-Level (F =>o G) (2 + n)
H-Level-Outer-nat = basic-instance 2 Outer-nat-is-set


## Some outer functorsπ

One important outer functor is the constant outer functor on an object $X : \mathcal{C}$, which can be constructed if $\mathcal{C}$ has products. This is the internalized version of the chaotic bifibration.

module _ (prods : has-products C) {β : Internal-cat} where
open Binary-products C prods
open Internal-cat β
open _=>o_


The total space of this functor is the product $X \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 \to y$ is a map in $\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. calls these functors internal base-valued functors, while in they are referred to as category actions.β©οΈ