open import Cat.Diagram.Pullback
open import Cat.Prelude

import Cat.Reasoning

module Cat.Internal.Base {o β} (C : Precategory o β) where

open Cat.Reasoning C


# Internal Categoriesπ

We often think of categories as places where we can do mathematics. This is done by translating definitions into the internal language of some suitably structured class of categories, and then working within that internal language to prove theorems.

This is all fine and good, but there is an obvious question: what happens if we internalize the definition of a category? Such categories are (unsurprisingly) called internal categories, and are quite well-studied. The traditional definition goes as follows: Suppose $\mathcal{C}$ is a category with [pullbacks], fix a pair of objects $\mathbb{C}_0, \mathbb{C}_1$ be a pair of objects, and parallel maps $\1, \1 : \mathbb{C}_1 \to \mathbb{C}_0$.

The idea is that $\mathbb{C}_0$ and $\mathbb{C}_1$ are meant to be the βobject of objectsβ and βobject of morphismsβ, respectively, while the maps $\1$ and $\1$ maps assign each morphism to its domain and codomain. A diagram $(\mathbb{C}_0, \mathbb{C}_1, \1, \1)$ is a category internal to $\mathcal{C}$ if it has an identity-assigning morphism $i : \mathbb{C}_0 \to \mathbb{C}_1$ a composition morphism $c : \mathbb{C}_1 \times_{C_0} \mathbb{C}_1 \to \mathbb{C}_1$, where the pullback β given by the square below β is the object of composable pairs.

These must also satisfy left/right identity and associativity. The associativity condition is given by the square below, and we trust that the reader will understand why will not attempt to draw the identity constraints.

Encoding this diagram in a proof assistant is a nightmare. Even constructing the maps into $C_1 \times_{C_0} C_1$ we must speak about is a pile of painful proof obligations, and these scale atrociously when talking about iterated pullbacks.1

To solve the problem, we look to a simpler case: internal monoids in $\mathcal{C}$. These are straightforward to define in diagramatic language, but can also be defined in terms of representability! The core idea is that we can define internal structure in the category of presheaves on $\mathcal{C}$, rather than directly in $\mathcal{C}$, letting us us use the structure of the meta-language to our advantage. To ensure that the structure defined in presheaves can be internalized to $\mathcal{C}$, we restrict ourselves to working with representable presheaves β which is equivalent to $\mathcal{C}$ by the Yoneda lemma.

From a type theoretic point of view, this is akin to defining structure relative to an arbitrary context $\Gamma$, rather than in the smallest context possible. This relativisation introduces a new proof obligation: stability under substitution. We have to ensure that we have defined the same structure in every context, which translates to a naturality condition.

## Representing internal morphismsπ

Let $\mathcal{C}$ be a category, and $(\mathbb{C}_0, \mathbb{C}_1, \operatorname{src}, \operatorname{tgt})$ be a diagram as before. We will define internal morphisms between generalised objects $x, y : \Gamma \to \mathbb{C}_0$ to be morphisms $f : \Gamma \to C_1$ making the following diagram commute.

record Internal-hom
{Cβ Cβ Ξ : Ob}
(src tgt : Hom Cβ Cβ) (x y : Hom Ξ Cβ)
: Type β where
no-eta-equality
field
ihom : Hom Ξ Cβ
has-src : src β ihom β‘ x
has-tgt : tgt β ihom β‘ y

open Internal-hom


This definition may seem somewhat odd, but we again stress that we are working in the internal language of $\mathcal{C}$, where it reads as the following typing rule:

$\frac{ \Gamma \vdash x : C_0\quad \Gamma \vdash y : C_0\quad \Gamma \vdash f : C_1\quad \operatorname{src}f \equiv x\quad \operatorname{tgt}f \equiv y\quad }{ \Gamma \vdash f : \mathbf{Hom}\ x\ y }$

Internal-hom-pathp
: β {Cβ Cβ Ξ} {src tgt : Hom Cβ Cβ} {x xβ² y yβ² : Hom Ξ Cβ}
β {f : Internal-hom src tgt x y} {g : Internal-hom src tgt xβ² yβ²}
β (p : x β‘ xβ²) (q : y β‘ yβ²)
β f .ihom β‘ g .ihom
β PathP (Ξ» i β Internal-hom src tgt (p i) (q i)) f g
Internal-hom-pathp p q r i .ihom = r i
Internal-hom-pathp {src = src} {f = f} {g = g} p q r i .has-src =
is-propβpathp (Ξ» i β Hom-set _ _ (src β r i) (p i)) (f .has-src) (g .has-src) i
Internal-hom-pathp {tgt = tgt} {f = f} {g = g} p q r i .has-tgt =
is-propβpathp (Ξ» i β Hom-set _ _ (tgt β r i) (q i)) (f .has-tgt) (g .has-tgt) i

Internal-hom-path
: β {Cβ Cβ Ξ} {src tgt : Hom Cβ Cβ} {x y : Hom Ξ Cβ}
β {f g : Internal-hom src tgt x y}
β f .ihom β‘ g .ihom
β f β‘ g
Internal-hom-path p = Internal-hom-pathp refl refl p

private unquoteDecl eqv = declare-record-iso eqv (quote Internal-hom)

Internal-hom-set
: β {Ξ Cβ Cβ} {src tgt : Hom Cβ Cβ} {x y : Hom Ξ Cβ}
β is-set (Internal-hom src tgt x y)
Internal-hom-set = Isoβis-hlevel 2 eqv hlevel!

instance
H-Level-Internal-hom
: β {Ξ Cβ Cβ} {src tgt : Hom Cβ Cβ} {x y : Hom Ξ Cβ} {n}
β H-Level (Internal-hom src tgt x y) (2 + n)
H-Level-Internal-hom = basic-instance 2 Internal-hom-set

_ihomβ
: β {Cβ Cβ Ξ} {src tgt : Hom Cβ Cβ} {x y : Hom Ξ Cβ}
β {f g : Internal-hom src tgt x y}
β f β‘ g
β f .ihom β‘ g .ihom
_ihomβ = ap ihom

infix -1 _ihomβ

: β {Ξ Cβ Cβ} {src tgt : Hom Cβ Cβ} {x xβ² y yβ² : Hom Ξ Cβ}
β x β‘ xβ² β y β‘ yβ² β Internal-hom src tgt x y β Internal-hom src tgt xβ² yβ²
adjusti p q f .ihom = f .ihom
adjusti p q f .has-src = f .has-src β p
adjusti p q f .has-tgt = f .has-tgt β q


We also must define the action of substitutions $\Delta \to \Gamma$ on internal morphisms. Zooming out to look at $\mathcal{C}$, substitutions are morphisms $\mathcal{C}(\Gamma, \Delta)$, and act on internal morphisms by precomposition.

_[_] : β {Cβ Cβ Ξ Ξ} {src tgt : Hom Cβ Cβ} {x y : Hom Ξ Cβ}
β Internal-hom src tgt x y
β (Ο : Hom Ξ Ξ)
β Internal-hom src tgt (x β Ο) (y β Ο)
(f [ Ο ]) .ihom = f .ihom β Ο
(f [ Ο ]) .has-src = pulll (f .has-src)
(f [ Ο ]) .has-tgt = pulll (f .has-tgt)

infix 50 _[_]


That out of the way, we can define internal categories in terms of their internal morphisms.

record Internal-cat-on {Cβ Cβ} (src tgt : Hom Cβ Cβ) : Type (o β β) where
no-eta-equality
field
idi : β {Ξ} β (x : Hom Ξ Cβ) β Internal-hom src tgt x x
_βi_ : β {Ξ} {x y z : Hom Ξ Cβ}
β Internal-hom src tgt y z β Internal-hom src tgt x y
β Internal-hom src tgt x z

infixr 40 _βi_


Having rewritten the pullbacks from before β where the previous attempt at a definition ended β in terms of dependency in the meta-language, we can state the laws of an internal category completely analogously to their external counterparts!

  field
idli : β {Ξ} {x y : Hom Ξ Cβ} (f : Internal-hom src tgt x y)
β idi y βi f β‘ f
idri : β {Ξ} {x y : Hom Ξ Cβ} (f : Internal-hom src tgt x y)
β f βi idi x β‘ f
associ : β {Ξ} {w x y z : Hom Ξ Cβ}
β (f : Internal-hom src tgt y z)
β (g : Internal-hom src tgt x y)
β (h : Internal-hom src tgt w x)
β f βi g βi h β‘ (f βi g) βi h


However, we do need to add the stability conditions, ensuring that we have the same internal category structure, even when moving between contexts.

    idi-nat : β {Ξ Ξ} {x : Hom Ξ Cβ} (Ο : Hom Ξ Ξ)
β idi x [ Ο ] β‘ idi (x β Ο)
βi-nat : β {Ξ Ξ} {x y z : Hom Ξ Cβ}
β (f : Internal-hom src tgt y z) (g : Internal-hom src tgt x y)
β (Ο : Hom Ξ Ξ) β (f βi g) [ Ο ] β‘ (f [ Ο ] βi g [ Ο ])


We also provide a bundled definition, letting us talk about arbitrary categories internal to $\mathcal{C}$.

record Internal-cat : Type (o β β) where
field
Cβ Cβ : Ob
src tgt : Hom Cβ Cβ
has-internal-cat : Internal-cat-on src tgt

open Internal-cat-on has-internal-cat public

Homi : β {Ξ} (x y : Hom Ξ Cβ) β Type β
Homi x y = Internal-hom src tgt x y

  homi : β {Ξ} (f : Hom Ξ Cβ) β Homi (src β f) (tgt β f)
homi f .ihom = f
homi f .has-src = refl
homi f .has-tgt = refl

homi-nat : β {Ξ Ξ} (f : Hom Ξ Cβ) β (Ο : Hom Ξ Ξ)
β homi f [ Ο ] β‘ adjusti (assoc _ _ _) (assoc _ _ _) (homi (f β Ο))
homi-nat f Ο = Internal-hom-path refl

-- Some of the naturality conditions required for later definitions will
-- require the use of PathP{.agda}, which messes up our equational
-- reasoning machinery. To work around this, we define some custom
-- equational reasoning combinators for working with internal homs.

casti : β {Ξ} {x x' y y' : Hom Ξ Cβ} {f : Homi x y} {g : Homi x' y'}
β {p p' : x β‘ x'} {q q' : y β‘ y'}
β PathP (Ξ» i β Homi (p i) (q i)) f g
β PathP (Ξ» i β Homi (p' i) (q' i)) f g
casti {Ξ = Ξ} {x} {x'} {y} {y'} {f} {g} {p} {p'} {q} {q'} r =
transport (Ξ» i β
PathP
(Ξ» j β Homi (Hom-set Ξ Cβ x x' p p' i j) ( Hom-set Ξ Cβ y y' q q' i j))
f g) r

begini_ : β {Ξ} {x x' y y' : Hom Ξ Cβ} {f : Homi x y} {g : Homi x' y'}
β {p p' : x β‘ x'} {q q' : y β‘ y'}
β PathP (Ξ» i β Homi (p i) (q i)) f g
β PathP (Ξ» i β Homi (p' i) (q' i)) f g
begini_ = casti

_βi_
: β {Ξ} {x xβ² xβ³ y yβ² yβ³ : Hom Ξ Cβ}
β {f : Homi x y} {g : Homi xβ² yβ²} {h : Homi xβ³ yβ³}
β {p : x β‘ xβ²} {q : y β‘ yβ²} {pβ² : xβ² β‘ xβ³} {qβ² : yβ² β‘ yβ³}
β PathP (Ξ» i β Homi (p i) (q i)) f g
β PathP (Ξ» i β Homi (pβ² i) (qβ² i)) g h
β PathP (Ξ» i β Homi ((p β pβ²) i) ((q β qβ²) i)) f h
_βi_ {x = x} {xβ²} {xβ³} {y} {yβ²} {yβ³} {f} {g} {h} {p} {q} {pβ²} {qβ²} r rβ² i =
comp (Ξ» j β Homi (β-filler p pβ² j i) (β-filler q qβ² j i)) (β i) Ξ» where
j (i = i0) β f
j (i = i1) β rβ² j
j (j = i0) β r i

: β {Ξ} {x xβ² xβ³ y yβ² yβ³ : Hom Ξ Cβ}
β (f : Homi x y) {g : Homi xβ² yβ²} {h : Homi xβ³ yβ³}
β {p : x β‘ xβ²} {q : y β‘ yβ²} {pβ² : xβ² β‘ xβ³} {qβ² : yβ² β‘ yβ³}
β PathP (Ξ» i β Homi (pβ² i) (qβ² i)) g h
β PathP (Ξ» i β Homi (p i) (q i)) f g
β PathP (Ξ» i β Homi ((p β pβ²) i) ((q β qβ²) i)) f h
β‘iβ¨β©-syntax f rβ² r = r βi rβ²

: β {Ξ} {x xβ² xβ³ y yβ² yβ³ : Hom Ξ Cβ}
β (f : Homi x y) {g : Homi xβ² yβ²} {h : Homi xβ³ yβ³}
β {p : xβ² β‘ x} {q : yβ² β‘ y} {pβ² : xβ² β‘ xβ³} {qβ² : yβ² β‘ yβ³}
β PathP (Ξ» i β Homi (p i) (q i)) g f
β PathP (Ξ» i β Homi (pβ² i) (qβ² i)) g h
β PathP (Ξ» i β Homi ((sym p β pβ²) i) ((sym q β qβ²) i)) f h
_β‘iΛβ¨_β©_ f r rβ²  = symP r βi rβ²

infixr 30 _βi_
infix 1 begini_


### Where did the pullbacks go?π

After seeing the definition above, the reader may be slightly concerned: we make no reference to pullbacks, or to limits in $\mathcal{C}$, at all! How in the world can this be the same as the textbook definition?

The pullbacks in $\mathcal{C}$ enter the stage when we want to move our internal category structure, which is relative to arbitrary contexts $\Gamma$, to the smallest possible context. To start, we note that internalizing the identity morphism can be done by looking instantiating idi at the identity morphism.

private module _ (pbs : has-pullbacks C) (β : Internal-cat) where
open Internal-cat β
open Pullbacks C pbs
open pullback

internal-id : Hom Cβ Cβ
internal-id = idi id .ihom


Now letβs see composition: enter, stage rights, the pullbacks. we define $\mathbb{C}_2$ to be the object of composable pairs β the first pullback square we gave, intersecting on compatible source and target. By translating the (internal) pullback square to (external) indexing, we have a pair of internal morphisms that can be composed.

  Cβ : Ob
Cβ = Pb src tgt

internal-comp : Hom Cβ Cβ
internal-comp = (f βi g) .ihom where
f : Homi (src β pβ src tgt) (tgt β pβ src tgt)
f .ihom = pβ src tgt
f .has-src = refl
f .has-tgt = refl

g : Homi (src β pβ src tgt) (src β pβ src tgt)
g .ihom = pβ src tgt
g .has-src = refl
g .has-tgt = sym $square src tgt  ## Internal functorsπ We will now start our project of relativisng category theory to arbitrary bases. Suppose $\mathbb{C}, \mathbb{D}$ are internal categories: what are the maps between them? Reasoning diagramatically, they are the morphisms between object-objects and morphism-objects that preserve source, target, commute with identity, and commute with composition. record Internal-functor (β π» : Internal-cat) : Type (o β β) where no-eta-equality private module β = Internal-cat β module π» = Internal-cat π»  Now thinking outside $\mathcal{C}$, an internal functor $\mathbb{C} \to \mathbb{D}$ consists of a family of maps between internal objects, together with a dependent function between internal morphisms β exactly as in the external case! With that indexing, the functoriality constraints also look identical.  field Fiβ : β {Ξ} β Hom Ξ β.Cβ β Hom Ξ π».Cβ Fiβ : β {Ξ} {x y : Hom Ξ β.Cβ} β β.Homi x y β π».Homi (Fiβ x) (Fiβ y) Fi-id : β {Ξ} {x : Hom Ξ β.Cβ} β Fiβ (β.idi x) β‘ π».idi (Fiβ x) Fi-β : β {Ξ} {x y z : Hom Ξ β.Cβ} β (f : β.Homi y z) (g : β.Homi x y) β Fiβ (f β.βi g) β‘ Fiβ f π».βi Fiβ g  However, do not forget the naturality conditions. Since we now have a βdependent functionβ between internal morphism spaces, its substitution stability depends on stability for the mapping between objects.  Fiβ-nat : β {Ξ Ξ} (x : Hom Ξ β.Cβ) β (Ο : Hom Ξ Ξ) β Fiβ x β Ο β‘ Fiβ (x β Ο) Fiβ-nat : β {Ξ Ξ} {x y : Hom Ξ β.Cβ} β (f : β.Homi x y) β (Ο : Hom Ξ Ξ) β PathP (Ξ» i β π».Homi (Fiβ-nat x Ο i) (Fiβ-nat y Ο i)) (Fiβ f [ Ο ]) (Fiβ (f [ Ο ])) open Internal-functor  ### Internal functor compositionπ module _ {β π» πΌ : Internal-cat} where private module β = Internal-cat β module π» = Internal-cat π» module πΌ = Internal-cat πΌ  As a demonstration of the power of these definitions, we can define composition of internal functors, which β at the risk of sounding like a broken record β mirrors the external definition exactly.  _Fiβ_ : Internal-functor π» πΌ β Internal-functor β π» β Internal-functor β πΌ (F Fiβ G) .Fiβ x = F .Fiβ (G .Fiβ x) (F Fiβ G) .Fiβ f = F .Fiβ (G .Fiβ f) (F Fiβ G) .Fi-id = ap (F .Fiβ) (G .Fi-id) β F .Fi-id (F Fiβ G) .Fi-β f g = ap (F .Fiβ) (G .Fi-β f g) β F .Fi-β _ _ (F Fiβ G) .Fiβ-nat x Ο = F .Fiβ-nat (G .Fiβ x) Ο β ap (F .Fiβ) (G .Fiβ-nat x Ο) (F Fiβ G) .Fiβ-nat f Ο = F .Fiβ-nat (G .Fiβ f) Ο πΌ.βi (Ξ» i β F .Fiβ (G .Fiβ-nat f Ο i)) infixr 30 _Fiβ_  There is also an internal version of the identity functor. Idi : β {β : Internal-cat} β Internal-functor β β Idi .Fiβ x = x Idi .Fiβ f = f Idi .Fi-id = refl Idi .Fi-β _ _ = refl Idi .Fiβ-nat _ _ = refl Idi .Fiβ-nat _ _ = refl  ## Internal natural transformationsπ Internal natural transformations follow the same pattern: we replace objects with generalized objects, morphisms with internal morphisms, and attach a condition encoding stability under substitution. Here again we must state stability over another stability condition. record _=>i_ {β π» : Internal-cat} (F G : Internal-functor β π») : Type (o β β) where no-eta-equality private module β = Internal-cat β module π» = Internal-cat π»   field Ξ·i : β {Ξ} (x : Hom Ξ β.Cβ) β π».Homi (F .Fiβ x) (G .Fiβ x) is-naturali : β {Ξ} (x y : Hom Ξ β.Cβ) (f : β.Homi x y) β Ξ·i y π».βi F .Fiβ f β‘ G .Fiβ f π».βi Ξ·i x Ξ·i-nat : β {Ξ Ξ} (x : Hom Ξ β.Cβ) β (Ο : Hom Ξ Ξ) β PathP (Ξ» i β π».Homi (F .Fiβ-nat x Ο i) (G .Fiβ-nat x Ο i)) (Ξ·i x [ Ο ]) (Ξ·i (x β Ο)) infix 20 _=>i_ open _=>i_  module _ {β π» : Internal-cat} {F G : Internal-functor β π»} where private module β = Internal-cat β module π» = Internal-cat π» Internal-nat-path : {Ξ± Ξ² : F =>i G} β (β {Ξ} (x : Hom Ξ β.Cβ) β Ξ± .Ξ·i x β‘ Ξ² .Ξ·i x) β Ξ± β‘ Ξ² Internal-nat-path {Ξ±} {Ξ²} p i .Ξ·i x = p x i Internal-nat-path {Ξ±} {Ξ²} p i .is-naturali x y f = is-propβpathp (Ξ» i β Internal-hom-set (p y i π».βi F .Fiβ f) (G .Fiβ f π».βi p x i)) (Ξ± .is-naturali x y f) (Ξ² .is-naturali x y f) i Internal-nat-path {Ξ±} {Ξ²} p i .Ξ·i-nat x Ο = is-setβsquarep (Ξ» i j β Internal-hom-set) (Ξ» i β p x i [ Ο ]) (Ξ± .Ξ·i-nat x Ο) (Ξ² .Ξ·i-nat x Ο) (Ξ» i β p (x β Ο) i) i private unquoteDecl nat-eqv = declare-record-iso nat-eqv (quote _=>i_) Internal-nat-set : is-set (F =>i G) Internal-nat-set = Isoβis-hlevel 2 nat-eqv$
Ξ£-is-hlevel 2 hlevel! $Ξ» _ β Ξ£-is-hlevel 2 hlevel!$ Ξ» _ β
Ξ -is-hlevelβ² 2 Ξ» _ β Ξ -is-hlevelβ² 2 Ξ» _ β
Ξ -is-hlevel 2 Ξ» _ β Ξ -is-hlevel 2 Ξ» _ β
PathP-is-hlevel 2 Internal-hom-set

instance
H-Level-Internal-nat
: β {β π» : Internal-cat} {F G : Internal-functor β π»} {n}
β H-Level (F =>i G) (2 + n)
H-Level-Internal-nat = basic-instance 2 Internal-nat-set


1. To be clear, we did not draw the identity constraints because they are trivial. Rather, speaking euphemistically, they are highly nontrivial.β©οΈ