module Cat.Internal.Base {o β} (C : Precategory o β) where
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 is a category with [pullbacks], fix a pair of objects be a pair of objects, and parallel maps .
The idea is that and are meant to be the βobject of objectsβ and βobject of morphismsβ, respectively, while the maps and maps assign each morphism to its domain and codomain. A diagram is a category internal to if it has an identity-assigning morphism a composition morphism , 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 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 . 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 , rather than directly in , 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 , we restrict ourselves to working with representable presheaves β which is equivalent to by the Yoneda lemma.
From a type theoretic point of view, this is akin to defining structure relative to an arbitrary context , 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 be a category, and be a diagram as before. We will define internal morphisms between generalised objects to be morphisms 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 , where it reads as the following typing rule:
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β adjusti : β {Ξ 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 on internal morphisms. Zooming out to look at , substitutions are morphisms , 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 .
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 β‘iβ¨β©-syntax : β {Ξ} {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β² _β‘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 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β² syntax β‘iβ¨β©-syntax f rβ² r = f β‘iβ¨ r β© rβ² infixr 30 _βi_ infix 1 begini_ infixr 2 β‘iβ¨β©-syntax _β‘iΛβ¨_β©_
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 , at all! How in the world can this be the same as the textbook definition?
The pullbacks in enter the stage when we want to move our internal category structure, which is relative to arbitrary contexts , 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 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 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 , an internal functor 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
To be clear, we did not draw the identity constraints because they are trivial. Rather, speaking euphemistically, they are highly nontrivial.β©οΈ