module index where

# 1lab🔗

A formalised, cross-linked reference resource for cubical methods in
Homotopy Type Theory. Unlike the (Univalent
Foundations Program 2013), the 1lab is not a “linear”
resource: Concepts are presented as a directed graph, with links
indicating *dependencies*. For instance, the statement of the
univalence principle depends on universes, identifications and equivalences. In addition to the
hyperlinked “web of concepts” provided by the Agda code, there is a
short introduction to homotopy type theory: **Start here**.

_ : ∀ {ℓ} {A B : Type ℓ} → is-equiv (path→equiv {A = A} {B}) _ = univalence

The purpose of the “web of concepts” approach is to let each reader
approach the 1lab at their own pace: If you already know what all of the
code above means, you can click on `univalence`

to be taken directly
to the construction of the equivalence — but if you *don’t*, you
can click on other definitions like `is-equiv`

and `path→equiv`

, and in turn explore
the dependencies of *those* concepts, and so on.

The 1lab is a community project: we use GitHub for source control and
talk on Discord. Our purpose
is to make cubical methods in homotopy type theory accessible to, and
inclusive of, everyone who is interested, regardless of cultural
background, age, ability, ethnicity, gender identity, or expression.
Correspondingly, interactions in those forums are governed by the Contributor
Covenant Code of Conduct. **We believe HoTT is for everyone,
and are committed to fostering a kind, inclusive
environment.**

Mathematics is, fundamentally, a social activity. Correspondingly, we have a page dedicated to letting authors introduce and talk a bit themselves and their other work:

open import Authors

Similarly, we maintain this list of related resources which serve as an introduction to HoTT in general:

The “canonical” reference is the HoTT Book, written by a variety of mathematicians at the IAS Special Year for Univalent Mathematics, held between 2012-2013 and organised by Steve Awodey, Thierry Coquand, and the late Vladimir Voevodsky.

The Book is often referred to on this site - with those words - so if you don’t know which book “The Book” is, it’s the HoTT book! It’s split into two parts: Type Theory, which introduces the concepts of Homotopy Type Theory with no previous knowledge of type theory assumed; and Mathematics, which develops some mathematics (homotopy theory, category theory, set theory, and real analysis) in this theory.

While the 1Lab is not strictly meant to be a companion to, or a formalisation of, the HoTT book. But since there is significant overlap, one of our pages is simply a list of references to the HoTT book and their correspondent on the 1Lab: HoTT

Prof. Martín Escardó, at Birmingham, has done a great service to the community by

*also*formalising a great deal of univalent mathematics in Literate Agda, in his Introduction to Univalent Foundations of Mathematics with Agda.Prof. Escardó’s notes, unlike the 1lab, are done in base Agda, with univalence assumed explicitly in the theorems that need it. This is a principled decision when the goal is introducing univalent mathematics, but it is not practical when the goal is to

*practice*univalent mathematics in Agda.Even still, that document is

*much better*than this site will*ever*be as an introduction to the subject! While many of the pages of the 1lab have introductory*flavour*, it is not meant as an introduction to the subject of univalent mathematics.

Prof. Favonia has kindly uploaded the outline, videos and lecture notes for their 2020 course on higher-dimensional type theory, which also serves as an introduction to cubical methods in homotopy type theory, aimed at graduate students. You can find the course page here, the videos here on their YouTube, and the notes here (though heed the warning in the README).

Another comprehensive, formalised Agda resource is the agda-unimath project, though unlike us (and like prof. Escardó’s lecture notes) they make use of

*axiomatic*HoTT: Univalence is a postulate, and thus does not have computational content.Regardless, they have formalised a great deal of “ordinary” mathematics in the univalent context: elementary number theory, group theory and combinatorics being the most prominent projects.

## Technology🔗

The 1Lab uses Julia Mono as its monospace typeface. Julia Mono is licensed under the SIL Open Font License, v1.1, a copy of which can be found here. As the sans-serif typeface, we use the Inria Sans webfont, and as a serif typeface, EB Garamond. These fonts are both open-source, though rather than rehosting them, we use them from Google Fonts.

Mathematics is rendered using KaTeX, and as so, the 1Lab redistributes KaTeX’s fonts and stylesheets, even though the rendering is done entirely at build-time. KaTeX is licensed under the MIT License, a copy of which can be found here.

Our favicon is Noto Emoji’s ice cube (cubical type theory - get it?), codepoint U+1F9CA. This is the only image from Noto we redistribute. Noto fonts are licensed under the Apache 2.0 License, a copy of which can be found here.

Commutative diagrams appearing in body text are created using quiver, and rendered to SVG using a combination of LaTeX and pdftocairo, part of the Poppler project. No part of these projects is redistributed.

And, of course, the formalisation would not be possible without Agda.

# Type theory🔗

Most of the modules in the 1Lab assume a baseline knowledge of type
theory. For this, **read the
introduction here**.

The first things to be explained are the foundational constructions
in (cubical) type theory - things like types themselves, universes, paths, equivalences, glueing and the univalence “axiom”. These are
developed under the `1Lab`

namespace. Start here:

-- All of these module names are links you can click! open import 1Lab.Type -- Universes open import 1Lab.Type.Pointed -- Pointed types open import 1Lab.Path -- Path types open import 1Lab.Path.Groupoid -- Groupoid structure of types open import 1Lab.Path.Reasoning -- Combinators for reasoning with path composition open import 1Lab.Path.IdentitySystem -- Families R for which R(x,y) ≃ (x ≡ y) open import 1Lab.Path.IdentitySystem.Strict -- Identity systems on sets open import 1Lab.Equiv -- “Contractible fibres” equivalences open import 1Lab.Equiv.Biinv -- Biinvertible maps open import 1Lab.Equiv.FromPath -- Transport is an equivalence, cubically open import 1Lab.Equiv.Embedding -- Embeddings open import 1Lab.Equiv.Fibrewise -- Fibrewise equivalences open import 1Lab.Equiv.HalfAdjoint -- Half-adjoint equivalences open import 1Lab.HLevel -- h-levels open import 1Lab.HLevel.Retracts -- Closure of h-levels under retractions/isos open import 1Lab.HLevel.Universe -- The type of n-types is a (n+1)-type open import 1Lab.Univalence -- Equivalence is equivalent to identification open import 1Lab.Univalence.SIP -- Univalence + preservation of structure open import 1Lab.Univalence.SIP.Auto -- Derive is-univalent for families of types open import 1Lab.Type.Pi -- Properties of dependent products open import 1Lab.Type.Sigma -- Properties of dependent coproducts open import 1Lab.HIT.Truncation -- Propositional truncation open import 1Lab.Counterexamples.IsIso -- Counterexample: is-iso is not a prop open import 1Lab.Counterexamples.Russell -- Counterexample: Russell's paradox open import 1Lab.Counterexamples.Sigma -- Counterexample: Sigma is not prop

## Data types🔗

The `Data`

namespace contains definitions of oft-used data
types, which are fundamental to the rest of the development but not
“basic type theory”. These modules contain (or re-export) the types
themselves, useful operations on them, characterisation of their path
spaces, etc.

The natural numbers have a lot of associated theory (number theory),
so there are a lot of child modules of `Data.Nat`

:

open import Data.Nat -- The natural numbers open import Data.Nat.Solver -- Commutative semiring solver for equations in Nat open import Data.Nat.DivMod -- Euclidean division open import Data.Nat.Divisible -- Divisibility open import Data.Nat.Divisible.GCD -- The greatest common divisor, Euclid's algorithm open import Data.Nat.Order -- Properties of ≤ open import Data.Nat.Properties -- Arithmetic properties

We also have a theory of finite sets:

open import Data.Fin open import Data.Fin.Base -- The standard finite sets open import Data.Fin.Finite -- Finiteness open import Data.Fin.Closure -- Closure properties of finiteness open import Data.Fin.Properties -- Properties of finite sets

Of similar importance is the type of integers:

open import Data.Int -- The integers (as a higher inductive type!) open import Data.Int.Inductive -- Inductively-defined integers open import Data.Int.Order -- ≤ on the integers open import Data.Int.Universal -- A universal property of the integers

General constructions on sets:

open import Data.Set.Truncation -- Set truncations open import Data.Set.Surjection -- Surjections of sets open import Data.Set.Coequaliser -- Set coequalisers

Well-founded relations, well-founded trees and well-founded induction:

open import Data.Wellfounded.W -- Trees open import Data.Wellfounded.Base -- Relations open import Data.Wellfounded.Properties -- Properties of well-founded relations

And general data types:

open import Data.Sum -- Coproduct types open import Data.Dec -- Decisions and decidable types open import Data.Bool -- The booleans open import Data.List -- Finite lists open import Data.Maybe -- The Maybe type

We also consider “data types” to encompass properties of properties, or, more generally, predicates:

open import Data.Power -- Power sets open import Data.Power.Complemented -- Complemented or decidable subobjects

# Category theory🔗

In addition to providing a framework for the synthetic study of higher groupoids, HoTT also provides a natural place to develop constructive category theory, while still being compatible with classicality principles like the axiom of choice and/or the law of excluded middle. Here, we do not assume any classicality principles.

## Basics🔗

The main modules in the `Cat`

namespace provide the
foundation for the rest of the development, defining basic constructions
like precategories themselves, functors, natural transformations,
etc.

open import Cat.Base -- Precategories, functors, natural transformations open import Cat.Solver -- Automatic solver for associativity problems open import Cat.Morphism -- Important classes of morphisms open import Cat.Reasoning -- Categorical reasoning combinators open import Cat.Groupoid -- Groupoids

### Diagrams🔗

For convenience, we define a plethora of “concrete” universal diagrams, unpacking their definitions as limits or colimits. These are simpler to work with since they provide the relevant data with fewer layers of indirection.

open import Cat.Diagram.Congruence -- Internal equivalence relations -- Colimits: open import Cat.Diagram.Initial -- Initial objects open import Cat.Diagram.Pushout -- Pushouts open import Cat.Diagram.Coproduct -- Binary coproducts open import Cat.Diagram.Coproduct.Copower -- Copowers open import Cat.Diagram.Coequaliser -- Coequalisers open import Cat.Diagram.Colimit.Base -- Conical colimits open import Cat.Diagram.Colimit.Finite -- Finite colimits open import Cat.Diagram.Coproduct.Indexed -- Indexed coproducts open import Cat.Diagram.Coequaliser.RegularEpi -- Regular epimorphisms -- Coends: open import Cat.Diagram.Coend -- Coends open import Cat.Diagram.Coend.Sets -- Concrete computation of coends in sets open import Cat.Diagram.Coend.Formula -- A formula for computing coends open import Cat.Diagram.Duals -- Dualisation of co/limits open import Cat.Diagram.Image -- Image factorisations open import Cat.Diagram.Sieve -- Subobjects of a Hom-functor open import Cat.Diagram.Idempotent -- Idempotent morphisms -- Limits open import Cat.Diagram.Product -- Binary products open import Cat.Diagram.Product.Finite -- n-Ary products open import Cat.Diagram.Product.Solver -- Automatic solving of equations in a Cartesian monoidal category open import Cat.Diagram.Pullback -- Fibred products open import Cat.Diagram.Terminal -- Terminal objects open import Cat.Diagram.Equaliser -- Equalisers open import Cat.Diagram.Limit.Base -- Conical limits open import Cat.Diagram.Limit.Finite open import Cat.Diagram.Limit.Product open import Cat.Diagram.Limit.Pullback open import Cat.Diagram.Limit.Equaliser open import Cat.Diagram.Product.Indexed open import Cat.Diagram.Equaliser.Kernel -- Kernels open import Cat.Diagram.Pullback.Properties -- Properties of fibred products open import Cat.Diagram.Equaliser.RegularMono -- Regular monomorphisms open import Cat.Diagram.Monad -- Monads open import Cat.Diagram.Monad.Limits -- Limits in Eilenberg-Moore categories open import Cat.Diagram.Monad.Codensity -- Codensity monads open import Cat.Diagram.Zero -- Zero objects

### Interesting morphisms🔗

There are a number of properties, constructions and classes of
morphisms we can construct in *any* category.

open import Cat.Morphism.StrongEpi -- Strong epimorphisms open import Cat.Morphism.Orthogonal -- Orthogonality open import Cat.Morphism.Factorisation -- Factorisation systems open import Cat.Morphism.Duality -- Duality of morphism classes

## Functors🔗

This namespace has definitions of properties functors can have, utility modules for working with functors, the definition of full subcategories, and adjoint functors.

open import Cat.Functor.Base -- Compendium of functor properties open import Cat.Functor.Dense -- Dense functors open import Cat.Functor.Final -- Final functors open import Cat.Functor.Slice -- Extending functors to slice categories open import Cat.Functor.Pullback -- Base change, dependent sum, Σf ⊣ f* open import Cat.Functor.Amnestic -- Functors which reflect univalence open import Cat.Functor.Bifunctor -- Functors out of product categories open import Cat.Functor.Conservative -- Functors which reflect isomorphisms open import Cat.Functor.FullSubcategory -- Full subcategories open import Cat.Functor.WideSubcategory -- Wide subcategories open import Cat.Functor.Subcategory -- Subcategories, generally

Helpers for working with functions in equational reasoning:

open import Cat.Functor.Reasoning open import Cat.Functor.Reasoning.FullyFaithful

About equivalences of (pre)categories:

open import Cat.Functor.Equivalence -- Equivalences of (pre)categories open import Cat.Functor.Equivalence.Path -- Categories are identical by their equivalences open import Cat.Functor.Equivalence.Complete -- Equivalences preserve completeness

About adjoint functors, and their associated monads:

open import Cat.Diagram.Monad -- Definition of monads open import Cat.Functor.Adjoint -- Unit-counit adjunctions and universal arrows open import Cat.Functor.Adjoint.Hom -- Adjoints in terms of Hom-isomorphisms open import Cat.Functor.Adjoint.Representable -- Adjoints in terms of representables open import Cat.Functor.Adjoint.Monad -- Monad from an adjunction open import Cat.Functor.Adjoint.Unique -- Uniqueness of adjoints open import Cat.Functor.Adjoint.Monadic -- Monadic adjunctions open import Cat.Functor.Adjoint.Compose -- Adjunctions compose open import Cat.Functor.Adjoint.Continuous -- Right adjoints preserve limits open import Cat.Functor.Adjoint.Reflective -- Reflective subcategories open import Cat.Functor.Adjoint.Mate -- Mates of adjoints

Monadicity theorems:

open import Cat.Functor.Monadic.Beck -- Beck's coequalisers open import Cat.Functor.Monadic.Crude -- The crude monadicity theorem

About Kan extensions:

open import Cat.Functor.Kan.Base -- Kan extensions open import Cat.Functor.Kan.Duality -- Left and right extensions are dual open import Cat.Functor.Kan.Nerve -- The nerve/realisation adjunction open import Cat.Functor.Kan.Global -- Global Kan extensions open import Cat.Functor.Kan.Adjoint -- Adjoints are Kan extensions open import Cat.Functor.Kan.Pointwise -- Pointwise Kan extensions open import Cat.Functor.Kan.Unique -- Uniqueness of Kan extensions open import Cat.Functor.Kan.Representable -- Kan extensions as Hom isomorphisms

Properties of Hom-functors, and (direct) consequences of the Yoneda lemma:

open import Cat.Functor.Hom -- Hom functor, Yoneda embedding open import Cat.Functor.Hom.Cocompletion -- Universal property of PSh(C) open import Cat.Functor.Hom.Coyoneda -- The Coyoneda lemma open import Cat.Functor.Hom.Representable -- Representable functors open import Cat.Functor.Hom.Duality -- Duality of Hom functors open import Cat.Functor.Hom.Displayed -- Hom functors of displayed categories

## Univalent categories🔗

In HoTT/UF, the word “category” is reserved for the precategories (what the rest of the world refers to as just “category”) in which isomorphic objects are indistinguishable, i.e. the categories which satisfy a version of the univalence axiom. Sometimes we also refer to these as “univalent categories” to make the distinction clear.

open import Cat.Univalent -- Basic properties of categories open import Cat.Univalent.Rezk -- Free category on a precategory open import Cat.Univalent.Rezk.Universal -- Universal property of the Rezk completion open import Cat.Univalent.Instances.Algebra -- Eilenberg-Moore categories preserve univalence

## Strict categories🔗

In general, precategories do not have a set of objects. We call
categories that do **strict**.

open import Cat.Strict -- Categories with a set of objects. open import Cat.Skeletal -- Categories where isomorphisms are automorphisms. open import Cat.Gaunt -- Strict univalent categories.

Properties, constructions, and the category of strict categories:

-- Strict categories open import Cat.Instances.StrictCat open import Cat.Instances.StrictCat.Cohesive -- ^ Strict category structure is a sort of "spatial" structure on a -- set open import Cat.Instances.Free -- Free strict categories on a directed graph open import Cat.Instances.FinSet -- Skeleton of the category of finite sets open import Cat.Instances.Simplex -- Skeleton of the simplex category open import Cat.Instances.Discrete -- Discrete categories open import Cat.Instances.Delooping -- Delooping a monoid to give a category

## Category instances🔗

Category “instances” are constructions of, and proofs associated to, the construction of actual categories, rather than reasoning about categories in the abstract. We begin with some assorted constructions:

open import Cat.Instances.Elements -- Category of elements of a presheaf open import Cat.Instances.Karoubi -- Completion of a category under splitting of idempotents open import Cat.Instances.Twisted -- The twisted arrow category (used in computing co/ends) open import Cat.Instances.Lift -- Lifting a category to higher universes open import Cat.Instances.Product -- Product categories open import Cat.Instances.Core -- The core of a category.

The construction and properties of functor categories:

-- Functor categories: open import Cat.Functor.Base open import Cat.Functor.Compose -- Composition of functors is functorial (also whiskering natural -- transformations) open import Cat.Instances.Functor.Limits -- Co/limits in functor categories open import Cat.Instances.Functor.Duality -- 2-cell duality in CatThe internal versions of functor categories:

-- Internal functor categories: open import Cat.Instances.InternalFunctor open import Cat.Instances.InternalFunctor.Compose -- Composition of internal functors is functorial (also whiskering internal -- natural transformations) open import Cat.Instances.OuterFunctor -- The category of functors from an internal category to its base.

Properties of the category of sets:

-- The category of sets: open import Cat.Instances.Sets -- is univalent open import Cat.Instances.Sets.Complete -- is complete open import Cat.Instances.Sets.Cocomplete -- is cocomplete, with disjoint coproducts open import Cat.Instances.Sets.Congruences -- has effective congruences open import Cat.Instances.Sets.CartesianClosed -- and is locally cartesian closed

The category of polynomial functors:

open import Cat.Instances.Poly

A few concrete, tiny categories are classed as “diagram shapes”:

-- Diagram shapes: open import Cat.Instances.Shape.Join open import Cat.Instances.Shape.Cospan open import Cat.Instances.Shape.Interval open import Cat.Instances.Shape.Parallel open import Cat.Instances.Shape.Terminal open import Cat.Instances.Shape.Isomorphism -- The walking isomorphism

Slice categories and comma objects:

open import Cat.Instances.Comma -- Comma categories open import Cat.Instances.Slice -- Slice categories open import Cat.Instances.Slice.Presheaf -- PSh(C)/X ≅ PSh(∫ X) open import Cat.Instances.Comma.Univalent

## Cartesian closed categories🔗

A Cartesian
closed category, or CCC for short, is one that has
*internalisations* for all its
$\mathbf{Hom}$-sets:
exponential
objects. Put another way, a CCC interprets the simply-typed
lambda calculus. Also of interest are the *locally*
Cartesian closed categories, where we also have an interpretation
for *dependent product* types.

open import Cat.Diagram.Exponential open import Cat.CartesianClosed.Lambda open import Cat.CartesianClosed.Locally

## Allegories🔗

Allegories are abstractions of the nice properties that the category
of relations enjoys. They are, strictly speaking, *bicategories*,
but since they are locally posets, we have a definition of allegory free
of all the extra coherence that is necessary for specifying a
bicategory.

open import Cat.Allegory.Base -- The definition open import Cat.Allegory.Maps -- Functional relations in an allegory open import Cat.Allegory.Morphism -- Morphisms in allegories open import Cat.Allegory.Reasoning -- Reasoning combinators

## Restriction categories🔗

Restriction categories axiomatize categories of partial maps by adding n restriction operation $(-)\downarrow : \mathcal{C}(X,Y) \to \mathcal{C}(X,X)$ that takes a morphism $f$ to a subobject of the identity morphism that is defined precisely when $f$ is.

open import Cat.Restriction.Base -- The definition open import Cat.Restriction.Functor -- Functors between restriction categories open import Cat.Restriction.Reasoning -- Reasoning combinators and morphism classes open import Cat.Restriction.Total -- Categories of total maps

open import Cat.Restriction.Instances.Allegory -- Restriction structures on partial maps of an allegory.

## Displayed categories🔗

A category displayed over $\mathcal{B}$ is a particular concrete presentation of the bicategorical slice $\mathfrak{Cat}/\mathcal{B}$; that is, it is a better way of presenting the data of a category $\mathcal{E}$ and a functor $\mathcal{E} \to \mathcal{B}$.

In addition to the *extensive* use of displayed
categories to model “pre-indexing” in the 1Lab, we also contain an
in-progress formalisation of Foundations of
Relative Category Theory.

open import Cat.Displayed.Base -- Displayed categories open import Cat.Displayed.Total -- Total category of a displayed category open import Cat.Displayed.Total.Free -- Free objects in a total category open import Cat.Displayed.Total.Op -- Total opposite categories open import Cat.Displayed.Fibre -- Fibre categories of a displayed category open import Cat.Displayed.Univalence -- Univalence for displayed categories open import Cat.Displayed.Univalence.Thin -- The structure identity principle open import Cat.Displayed.Reasoning -- Reasoning combinators for displayed categories open import Cat.Displayed.Morphism -- Important classes of morphisms in displayed categories open import Cat.Displayed.Morphism.Duality -- Duality of morphism classes in displayed categories open import Cat.Displayed.Instances.Elements -- The category of elements of a presheaf, instantiated as being -- displayed over the domain. open import Cat.Displayed.Instances.TotalProduct -- The total product of two displayed categories. open import Cat.Displayed.Composition -- Composition of displayed categories

We can also investigate how displayed categories relate to other displayed categories (over the same base, or over different bases), and their higher groupoid structure:

open import Cat.Displayed.Path open import Cat.Displayed.Functor open import Cat.Displayed.Adjoint

### Cartesian fibrations🔗

In the land of 1-categories, the notion of “indexed families of
objects” is accurately captured by slice categories. But when we’re
talking about the 2-category
$\mathfrak{Cat}$,
plain functors won’t do. In terms of displayed categories, we need to
talk about *Cartesian
fibrations* instead. These satisfy a property analogous to the
existence of pullbacks, and they are precisely those which correspond to
families
$\mathcal{B} \to \mathfrak{Cat}$.

open import Cat.Displayed.Cartesian -- Cartesian lifts, cartesian fibrations open import Cat.Displayed.Cartesian.Weak -- Weak cartesian morphisms open import Cat.Displayed.Cartesian.Street -- Street's fibrations open import Cat.Displayed.Cartesian.Discrete -- Discrete fibrations are presheaves open import Cat.Displayed.Cartesian.Right -- Fibrations in groupoids open import Cat.Displayed.Cartesian.Indexing -- Fibrations have pseudofunctorial reindexing.

Not to dwell on a vacuous concept, we also have constructions of Cartesian fibrations:

open import Cat.Displayed.Instances.Slice -- Canonical self-indexing open import Cat.Displayed.Instances.Subobjects -- Fibration of subobjects open import Cat.Displayed.Instances.Family -- Family fibration open import Cat.Displayed.Instances.DisplayedFamilies -- Families internal to a fibration. open import Cat.Displayed.Instances.Pullback -- Pullback of a displayed category by a functor open import Cat.Displayed.Instances.Scone -- We can consider *scones* over a category C with a terminal object as -- forming a displayed category over C. Moreover, it's a Cartesian -- fibration by construction. open import Cat.Displayed.Instances.Trivial -- Any category can be displayed over the terminal category. open import Cat.Displayed.Instances.Lifting -- Liftings of functors along a fibration open import Cat.Displayed.Instances.Diagrams -- The fibration of diagrams open import Cat.Displayed.Instances.Objects -- The fibration of objects. open import Cat.Displayed.Instances.Externalisation -- Internal categories as fibrations.

### Cocartesian fibrations🔗

open import Cat.Displayed.Cocartesian -- Cocartesian lifts, opfibrations open import Cat.Displayed.Cocartesian.Indexing -- Opfibrations have covariant opreindexing open import Cat.Displayed.Cocartesian.Weak -- Weak cocartesian morphisms

### Bifibrations🔗

open import Cat.Displayed.Bifibration -- Bifibrations, adjoints to base change open import Cat.Displayed.Instances.Chaotic -- The bifibration associated with the projection functor -- $\cB \times \cJ \to \cB$. open import Cat.Displayed.Instances.Identity -- The bifibration associated with the identity functor.

### Structures in fibrations🔗

open import Cat.Displayed.InternalSum -- The fibred equivalent of sigma types and existential quantifiers open import Cat.Displayed.GenericObject -- Generic objects in fibrations.

### Logical structure of fibrations🔗

Fibrations serve as an excellent foundation for exploring various logical and type-theoretic phenomena.

open import Cat.Displayed.Comprehension -- A categorical model of context extension. open import Cat.Displayed.Comprehension.Coproduct -- Coproducts in comprehension categories open import Cat.Displayed.Comprehension.Coproduct.Strong -- Coproducts with a stronger elimination principle open import Cat.Displayed.Comprehension.Coproduct.VeryStrong -- Coproducts with a very strong elimination principle

## Internal categories🔗

The theory of internal categories. Internal category theory generalizes strict category theory by replacing the ambient category $\mathbf{Sets}$ with an arbitrary category $\mathcal{C}$ with pullbacks.

open import Cat.Internal.Base -- Internal categories, internal functors, and internal natural -- transformations. open import Cat.Internal.Morphism -- Internal monos, epis, and isos. open import Cat.Internal.Reasoning -- Reasoning combinators for internal categories. open import Cat.Internal.Opposite -- The opposite of an internal category. open import Cat.Internal.Functor.Outer -- Internal functors from an internal category to its base. open import Cat.Internal.Sets -- Categories internal to sets are strict categories.

### Examples of internal categories🔗

open import Cat.Internal.Instances.Discrete -- Discrete internal categories. open import Cat.Internal.Instances.Congruence -- Internal equivalence relations are internal categories.

## Bicategories🔗

The theory of bicategories, as isolated objects. Note that a
comprehensive study of how bicategories interact with other bicategories
is a **tri**categorical problem!

open import Cat.Bi.Base -- Prebicategories, lax functors, pseudofunctors, lax transformations, -- pseudonatural transformations, modifications, and the bicategory of -- categories. open import Cat.Bi.Instances.Spans -- The prebicategory of spans in a precategory with pullbacks open import Cat.Bi.Instances.Discrete -- The locally discrete prebicategory associated to a precategory open import Cat.Bi.Instances.InternalCats -- The prebicategory of categories internal to a fixed base category.

### Diagrams in bicategories🔗

open import Cat.Bi.Diagram.Monad -- Monads in a bicategory open import Cat.Bi.Diagram.Monad.Spans -- Internal categories as monads in Span(C) open import Cat.Bi.Diagram.Adjunction -- Adjunction diagrams in a bicategory

## Monoidal categories🔗

In addition to general bicategories, we also have bicategories with one object.

open import Cat.Monoidal.Base open import Cat.Monoidal.Diagram.Monoid open import Cat.Monoidal.Instances.Cartesian open import Cat.Monoidal.Diagram.Monoid.Representable -- Internal monoids, representability, and the internal language of a category.

## Homological algebra🔗

The theory of abelian (and Ab-enriched) categories in general, and specific constructions of abelian categories.

open import Cat.Abelian.Base -- Definition of the tower of Ab-enriched categories open import Cat.Abelian.Endo -- Endomorphism rings open import Cat.Abelian.Images -- Image factorisations in abelian categories open import Cat.Abelian.Limits -- Finite biproducts in abelian categories open import Cat.Abelian.Functor -- Ab-enriched functors open import Cat.Abelian.Instances.Ab -- The category of abelian groups open import Cat.Abelian.Instances.Functor -- Ab-enriched functor categories

## Topos theory🔗

Grothendieck topos theory developed constructively.

open import Topoi.Base -- Topoi, properties of topoi, geometric morphisms open import Topoi.Reasoning -- Exactness properties of topoi (cont'd), reasoning open import Topoi.Classifying.Diaconescu -- ^ Presheaf topoi classify flat functors on their site

# Order theory🔗

Order theory is, to the category theorist, the study of 0-categories: Those for which we have a (-1)-groupoid of morphisms between any two objects, i.e., those for which rather than having $\mathbf{Hom}$-sets, we have a $x \le y$ relation.

open import Order.Base -- Definitions open import Order.Cat -- Posets generate categories open import Order.Reasoning -- Nice syntax for posets open import Order.Displayed -- Displayed posets

For readability, we have diagrams in orders separate from diagrams in their generated categories:

open import Order.Diagram.Glb open import Order.Diagram.Lub open import Order.Diagram.Fixpoint -- Least and Greatest fixpoints

Some order-theoretic structures are equivalently presented as algebraic structures: these are the lattices and related structures.

open import Order.Frame open import Order.Lattice open import Order.Semilattice open import Order.Semilattice.Free open import Order.Semilattice.Order

Examples of actual orders:

open import Order.Instances.Discrete -- Discrete posets open import Order.Instances.Props -- Ω open import Order.Instances.Lower -- Lower sets open import Order.Instances.Pointwise -- The pointwise ordering on A→B open import Order.Instances.Pointwise.Diagrams

## Domain theory🔗

Domain theory is the study of posets that are complete under various classes of least upper bounds. These posets are used to model notions of partiality, which makes them extremely useful in the search for semantics of various programming languages.

open import Order.DCPO -- Directed-complete partial orders open import Order.DCPO.Pointed -- Pointed directed-complete partial orders open import Order.DCPO.Free -- Free DCPOs and free pointed DCPOs

# Logic🔗

open import Logic.Propositional.Classical -- Classical logic, soundness, completeness open import Logic.Propositional.Classical.CNF -- Conjunctive normal forms open import Logic.Propositional.Classical.SAT -- DPLL SAT solver

# Algebra🔗

open import Algebra.Magma -- Binary operations open import Algebra.Magma.Unital -- Operations with two-sided units open import Algebra.Magma.Unital.EckmannHilton -- The Eckmann-Hilton argument open import Algebra.Semigroup -- Semigroups (associative magmas) open import Algebra.Monoid -- Monoids as unital semigroups open import Algebra.Monoid.Category -- The category of monoids

## Group theory🔗

open import Algebra.Group -- Groups as monoids with inverses open import Algebra.Group.NAry -- NAry sums on groups open import Algebra.Group.Free -- Free groups open import Algebra.Group.Action -- Group actions open import Algebra.Group.Cayley -- Cayley's theorem open import Algebra.Group.Cat.Base -- The category of groups open import Algebra.Group.Cat.Monadic -- ... is monadic over Sets open import Algebra.Group.Cat.FinitelyComplete -- Finite limits in Groups open import Algebra.Group.Subgroup -- Subgroups, images and kernels open import Algebra.Group.Concrete -- Concrete groups (pointed connected groupoids) open import Algebra.Group.Homotopy -- Homotopy groups open import Algebra.Group.Homotopy.BAut -- Delooping groupoids of automorphism groups open import Algebra.Group.Ab -- Abelian groups, and the category Ab open import Algebra.Group.Ab.Sum -- Direct sum abelian groups open import Algebra.Group.Ab.Free -- The free abelian group on a group

## Ring theory🔗

open import Algebra.Ring -- Rings open import Algebra.Ring.Ideal -- Ideals in commutative rings open import Algebra.Ring.Module -- Modules over a commutative ring open import Algebra.Ring.Quotient -- Quotient rings open import Algebra.Ring.Cat.Initial -- ℤ is the initial ring open import Algebra.Ring.Commutative -- Commutative rings open import Algebra.Ring.Module.Vec -- Finite direct sums of R as an R-module open import Algebra.Ring.Module.Free -- Free R-modules as a HIT open import Algebra.Ring.Module.Category -- The bifibration of Mod over Ring

# Homotopy theory🔗

Synthetic homotopy theory is the name given to studying $\infty$-groupoids in their own terms, i.e., the application of homotopy type theory to computing homotopy invariants of spaces.

open import Homotopy.Base -- Basic definitions open import Homotopy.Connectedness -- Connected types open import Homotopy.Space.Suspension -- Suspensions open import Homotopy.Space.Circle -- The circle open import Homotopy.Space.Sphere -- The n-spheres open import Homotopy.Space.Sinfty -- The ∞-sphere open import Homotopy.Space.Torus -- The torus

## References

- Univalent Foundations Program, The. 2013.
*Homotopy Type Theory: Univalent Foundations of Mathematics*. Institute for Advanced Study: https://homotopytypetheory.org/book.