Categories

Anna Williams, 17 October 2025

Formalisation of some 1-category theory with univalent foundations.
Included are definitions of wild categories, precategories,
(univalent) categories, functors and natural transformations.


{-# OPTIONS --safe --without-K #-}

module Categories.index where


We follow the naming conventions of the HoTT Book [1] and [2]. The properties of
the different types of category are given in the table below.

                ┌──────┬──────┬────────────┐
                │ obj  │ hom  │ univalence │
┌───────────────┼──────┼──────┼────────────┤
│ wild-category │ type │ type │ no         │
├───────────────┼──────┼──────┼────────────┤
│ pre-category  │ type │ set  │ no         │
├───────────────┼──────┼──────┼────────────┤
│ category      │ type │ set  │ yes        │
└───────────────┴──────┴──────┴────────────┘

[1] The Univalent Foundations Program (2013), Homotopy Type Theory: Univalent
Foundations of Mathematics. Institute for Advanced Study:
https://homotopytypetheory.org/book.

[2] Capriotti, Paolo and Nicolai Kraus (2017). Univalent Higher Categories via
Complete Semi-Segal Type. https://arxiv.org/abs/1707.03693.


import Categories.Wild
import Categories.Pre
import Categories.Univalent

import Categories.Functor
import Categories.Functor-Composition
import Categories.NaturalTransformation
import Categories.Adjoint

import Categories.Notation.index
import Categories.Examples.index


The above defines notation for working with categories, we use this so that
we can write the following and have the category fields be public.

`open WildCategoryNotation C`
`open PrecategoryNotation C`
`open CategoryNotation C`
`open FunctorNotation F renaming (functor-map to F')`
`open NaturalTNotation N`

We use this notation throughout the definitions, so for more concrete examples
please look there.

Displayed Categories.


import Categories.Displayed.index


A listing relating to the masters project of Anna Williams


import Categories.AW-MSciProject