open import 1Lab.Reflection.Record open import 1Lab.Equiv.Fibrewise open import 1Lab.HLevel.Retracts open import 1Lab.HLevel.Universe open import 1Lab.Univalence open import 1Lab.Rewrite open import 1Lab.HLevel open import 1Lab.Equiv open import 1Lab.Path open import 1Lab.Type hiding (id ; _β_) module Cat.Base where
Precategoriesπ
In univalent mathematics, it makes sense to distinguish two stages in the construction of categories: A precategory is the object that directly corresponds to the definition of precategory as it is traditionally formalised, whereas a category (or univalent category) has an extra condition: Isomorphic objects must be identified.
record Precategory (o h : Level) : Type (lsuc (o β h)) where noetaequality
A precategory is a βproofrelevant preorderβ. In a preordered set $(A, \le)$, the inhabitants of a set $A$ are related by a proposition $a \le b$, which is
 reflexive: $a \le a$
 transitive: $a \le b \land b \le c \to a \le c$
In a precategory, the condition that $a \le b$ be a proposition is relaxed: A precategory has a type of objects and, between each $x, y$, a set $\id{Hom}(x, y)$ of relations (or maps). The name Hom is historical and it betrays the original context in which categories where employed: algebra(ic topology), where the maps in question are homomorphisms.
field Ob : Type o Hom : Ob β Ob β Type h
Whereas reading a classical definition into a type theory where equality is a proposition, the word set may be read to mean inhabitant of a universe. But in HoTT, if we want categories to be wellbehaved, we do actually mean set: A type of hlevel 2.
field Homset : (x y : Ob) β isset (Hom x y)
If you are already familiar with the definition of precategory there are two things to note here:
First is that our formalization has a family of Homsets rather than a single Homset and source/target maps. This formulation is not unique to precategory theory done internally to type theory, but it is the most reasonable way to formulate things in this context.
Second is that the word βsetβ in the definition of Homset has nothing to do with βsizeβ. Indeed, the βsetβ/βnot a setβ (alternatively βsmallβ/βlargeβ) distinction makes no sense in type theory (some may argue it makes no sense in general).
Instead, the Precategory record is parametrised by two
levels: o
, and h
. The type of objects has to
fit in the universe Type o
, and the family of Homsets is
Type h
valued. As an example, the thin precategory
corresponding to the natural numbers with their usual ordering would
live in Precategory lzero lzero
.
This means, for instance, that there is no single βcategory of setsβ  there is a family of categories of sets, parametrised by the level in which its objects live.
field id : β {x} β Hom x x _β_ : β {x y z} β Hom y z β Hom x y β Hom x z infixr 40 _β_
The βproofrelevantβ version of the reflexivity and transitivity laws
are, respectively, the identity morphisms
and composition of morphisms. Unlike in
the proofirrelevant case, in which an inhabitant of
$x \le y$
merely witnesses that two things are related, these operations
matter, and thus must satisfy laws:
field idr : β {x y} (f : Hom x y) β f β id β‘ f idl : β {x y} (f : Hom x y) β id β f β‘ f
The two identity laws say that the identity morphisms serve as neutral elements for the composition operation, both on the left and on the right. The βtwoβ associativity laws (below) say that both ways of writing parentheses around a composition of three morphisms is equal: $(f \circ g) \circ h = f \circ (g \circ h)$.
assoc : β {w x y z} (f : Hom y z) (g : Hom x y) (h : Hom w x) β f β (g β h) β‘ (f β g) β h
Oppositesπ
A common theme throughout precategory theory is that of
duality: The dual of a categorical concept is same concept,
with βall the arrows invertedβ. To make this formal, we introduce the
idea of opposite categories: The opposite of
$C$,
written
$C\op$,
has the same objects
, but with
$\id{Hom}_{C\op}(x, y) = \id{Hom}_{C}(y, x)$.
infixl 60 _^op _^op : β {oβ hβ} β Precategory oβ hβ β Precategory oβ hβ (C ^op) .Precategory.Ob = Precategory.Ob C (C ^op) .Precategory.Hom x y = Precategory.Hom C y x (C ^op) .Precategory.Homset x y = Precategory.Homset C y x (C ^op) .Precategory.id = Precategory.id C (C ^op) .Precategory._β_ f g = Precategory._β_ C g f
Composition in the opposite precategory $C\op$ is βbackwardsβ with respect to $C$: $f \circ_{op} g = g \circ f$. This inversion, applied twice, ends up equal to what we started with by the nature of computation  An equality that arises like this, automatically from what Agda computes, is called definitional.
(C ^op) .Precategory.idl x = C .Precategory.idr x (C ^op) .Precategory.idr x = C .Precategory.idl x
The left and right identity laws are swapped for the construction of the opposite precategory: For idr one has to show $f \circ_{op} \id{id} = f$, which computes into having to show that $\id{id} \circ_op{f} = f$. The case for idl is symmetric.
(C ^op) .Precategory.assoc f g h i = Precategory.assoc C h g f (~ i)
For associativity, consider the case of assoc for the
opposite precategory
$C\op$.
What we have to show is  by the type of assocβ

$f \circ_{op} (g \circ_{op} h) = (f \circ_{op} g) \circ_{op} h$.
This computes into
$(h \circ g) \circ f = h \circ (g \circ f)$
 which is exactly what sym (assoc C h g f)
shows!
C^op^opβ‘C : β {o β} {C : Precategory o β} β C ^op ^op β‘ C C^op^opβ‘C {C = C} i = precat i where open Precategory precat : C ^op ^op β‘ C precat i .Ob = C .Ob precat i .Hom = C .Hom precat i .Homset = C .Homset precat i .id = C .id precat i ._β_ = C ._β_ precat i .idr = C .idr precat i .idl = C .idl precat i .assoc = C .assoc
The precategory of Setsπ
Given a universe level, we can consider the collection of all sets of that level. This assembles into a precategory quite nicely, since functions preserve hlevels.
module _ where open Precategory Sets : (o : _) β Precategory (lsuc o) o Sets o .Ob = Set o Sets o .Hom A B = β£ A β£ β β£ B β£ Sets o .Homset _ B f g p q i j a = B .istr (f a) (g a) (happly p a) (happly q a) i j Sets o .id x = x Sets o ._β_ f g x = f (g x) Sets o .idl f = refl Sets o .idr f = refl Sets o .assoc f g h = refl
Functorsπ
Since a category is an algebraic structure, there is a natural definition of homomorphism of categories defined in the same fashion as, for instance, a homomorphism of groups. Since this kind of morphism is ubiquitous, it gets a shorter name: Functor.
Alternatively, functors can be characterised as the βproofrelevant versionβ of a monotone map: A monotone map is a map $F : C \to D$ which preserves the ordering relation, $x \le y \to F(x) \le F(y)$. Categorifying, βpreserves the ordering relationβ becomes a function between Homsets.
field Fβ : C.Ob β D.Ob Fβ : β {x y} β C.Hom x y β D.Hom (Fβ x) (Fβ y)
A Functor $F : C \to D$ consists of a function between the object sets  $F_0 : \id{Ob}(C) \to \id{Ob}(D)$, and a function between Homsets  which takes $f : x \to y \in C$ to $F_1(f) : F_0(x) \to F_0(y) \in D$.
field Fid : β {x} β Fβ (C.id {x}) β‘ D.id Fβ : β {x y z} (f : C.Hom y z) (g : C.Hom x y) β Fβ (f C.β g) β‘ Fβ f D.β Fβ g
Furthermore, the morphism mapping $F_1$ must be homomorphic: Identity morphisms are taken to identity morphisms (Fid) and compositions are taken to compositions (Fβ).
Functors also have duals: The opposite of $F : C \to D$ is $F\op : C\op \to D\op$.
op : Functor (C ^op) (D ^op) Fβ op = Fβ Fβ op = Fβ Fid op = Fid Fβ op f g = Fβ g f
Compositionπ
_Fβ_ : β {oβ hβ oβ hβ oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} {E : Precategory oβ hβ} β Functor D E β Functor C D β Functor C E _Fβ_ {C = C} {D} {E} F G = comps
Functors, being made up of functions, can themselves be composed. The object mapping of $(F \circ G)$ is given by $F_0 \circ G_0$, and similarly for the morphism mapping. Alternatively, composition of functors is a categorification of the fact that monotone maps compose.
Fβ : C.Ob β E.Ob Fβ x = F.Fβ (G.Fβ x) Fβ : {x y : C.Ob} β C.Hom x y β E.Hom (Fβ x) (Fβ y) Fβ f = F.Fβ (G.Fβ f)
To verify that the result is functorial, equational reasoning is employed, using the witnesses that $F$ and $G$ are functorial.
abstract Fid : {x : C.Ob} β Fβ (C.id {x}) β‘ E.id {Fβ x} Fid {x} = F.Fβ (G.Fβ C.id) β‘β¨ ap F.Fβ G.Fid β©β‘ F.Fβ D.id β‘β¨ F.Fid β©β‘ E.id β Fβ : {x y z : C.Ob} (f : C.Hom y z) (g : C.Hom x y) β Fβ (f C.β g) β‘ (Fβ f E.β Fβ g) Fβ f g = F.Fβ (G.Fβ (f C.β g)) β‘β¨ ap F.Fβ (G.Fβ f g) β©β‘ F.Fβ (G.Fβ f D.β G.Fβ g) β‘β¨ F.Fβ _ _ β©β‘ Fβ f E.β Fβ g β comps : Functor _ _ comps .Functor.Fβ = Fβ comps .Functor.Fβ = Fβ comps .Functor.Fid = Fid comps .Functor.Fβ = Fβ
The identity functor can be defined using the identity funct_ion_ for both its object and morphism mappings. That functors have an identity and compose would seem to imply that categories form a category: However, since there is no upper bound on the hlevel of Ob, we can not form a βcategory of categoriesβ. If we do impose a bound, however, we can obtain a category of strict categories, those which have a set of objects.
Id : β {oβ hβ} {C : Precategory oβ hβ} β Functor C C Functor.Fβ Id x = x Functor.Fβ Id f = f Functor.Fid Id = refl Functor.Fβ Id f g = refl
Natural Transformationsπ
Another common theme in category theory is that roughly every concept can be considered the objects of a category. This is the case for functors, as well! The functors between $C$ and $D$ assemble into a category, notated $[C, D]$  the functor category between $C$ and $D$.
record _=>_ {oβ hβ oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} (F G : Functor C D) : Type (oβ β hβ β hβ) where noetaequality constructor NT
The morphisms between functors are called natural transformations. A natural transformation $F \To G$ can be thought of as a way of turning $F(x)$s into $G(x)$s that doesnβt involve any βarbitrary choicesβ.
private module F = Functor F module G = Functor G module D = Precategory D module C = Precategory C field Ξ· : (x : _) β D.Hom (F.β x) (G.β x)
The transformation itself is given by Ξ·, the family of components, where the component at $x$ is a map $F(x) \to G(x)$. The βwithout arbitrary choicesβ part is encoded in the field isnatural, which encodes commutativity of the square below:
isnatural : (x y : _) (f : C.Hom x y) β Ξ· y D.β F.β f β‘ G.β f D.β Ξ· x
Natural transformations also dualize. The opposite of $\eta : F \To G$ is $\eta\op : G\op \To F\op$.
op : Functor.op G => Functor.op F op = record { Ξ· = Ξ· ; isnatural = Ξ» x y f β sym (isnatural _ _ f) }
Since the type of natural transformations is defined as a record, we can not a priori reason about its hlevel in a convenient way. However, using Agdaβs metaprogramming facilities (both reflection and instance search), we can automatically derive an equivalence between the type of natural transformations and a certain $\Sigma$ type; This type can then be shown to be a set using the standard hlevel machinery.
private unquoteDecl eqv = declarerecordiso eqv (quote _=>_) Natisset : isset (F => G) Natisset = ishlevelβ 2 (IsoβEquiv eqv eβ»ΒΉ) (hlevel 2) where open C.HLevelinstance open D.HLevelinstance
Another fundamental lemma is that equality of natural transformations depends only on equality of the family of morphisms, since being natural is a proposition:
Natpathp : {F' G' : Functor C D} β (p : F β‘ F') (q : G β‘ G') β {a : F => G} {b : F' => G'} β (β x β PathP _ (a .Ξ· x) (b .Ξ· x)) β PathP (Ξ» i β p i => q i) a b Natpathp p q path i .Ξ· x = path x i Natpathp p q {a} {b} path i .isnatural x y f = ispropβpathp (Ξ» i β D.Homset _ _ (path y i D.β Functor.Fβ (p i) f) (Functor.Fβ (q i) f D.β path x i)) (a .isnatural x y f) (b .isnatural x y f) i Natpath : {a b : F => G} β ((x : _) β a .Ξ· x β‘ b .Ξ· x) β a β‘ b Natpath = Natpathp refl refl