module index where

1lab🔗

A formalised, cross-linked reference resource for cubical methods in Homotopy Type Theory. Unlike the HoTT book, 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.

  • 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 Iosevka as its monospace typeface. Iosevka 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 rubber-pipe 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.Path          -- Path types
open import 1Lab.Path.Groupoid -- Groupoid structure of types

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.Sets     -- K, Rijke's theorem, Hedberg's theorem
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.Univalence.SIP.Record -- Derive is-univalent for record types

open import 1Lab.Type.Dec   -- Decidable types, discrete types
open import 1Lab.Type.Pi    -- Properties of dependent products
open import 1Lab.Type.Sigma -- Properties of dependent coproducts

open import 1Lab.HIT.S1         -- The circle as a cell complex
open import 1Lab.HIT.Sphere     -- Spheres of arbitrary dimension
open import 1Lab.HIT.Torus      -- Torus as a cell complex and as a product space
open import 1Lab.HIT.Sinfty     -- The infinity-dimensional sphere
open import 1Lab.HIT.Suspension -- The suspension operation
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.

open import Data.Nat  -- The natural numbers
open import Data.Int  -- The integers
open import Data.Sum  -- Coproduct types
open import Data.Bool -- The booleans
open import Data.List -- Finite lists
open import Data.Power           -- Power sets
open import Data.Power.Lattice   -- Power sets form a lattice
open import Data.Set.Coequaliser -- Set coequalisers

Category Theory🔗

In addition to providing a framework for the synthetic study of higher groupoids, HoTT also provides a natural place to develop constructive, predicative 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

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.Coequaliser            -- Coequalisers
open import Cat.Diagram.Colimit.Base           -- Conical colimits
open import Cat.Diagram.Coproduct.Indexed      -- Indexed coproducts
open import Cat.Diagram.Coequaliser.RegularEpi -- Regular epimorphisms

open import Cat.Diagram.Duals -- Dualisation of co/limits
open import Cat.Diagram.Image -- Image factorisations
open import Cat.Diagram.Idempotent -- Idempotent morphisms

-- Limits
open import Cat.Diagram.Product                -- Binary products
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.Zero -- Zero objects

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.Hom -- Hom functor, Yoneda embedding, Coyoneda lemma
open import Cat.Functor.Base -- Compendium of functor properties
open import Cat.Functor.Pullback -- Base change, dependent sum, Σf ⊣ f*
open import Cat.Functor.Bifunctor -- Functors out of product categories
open import Cat.Functor.Equivalence -- Equivalences of (pre)categories
open import Cat.Functor.Conservative -- Functors which reflect isomorphisms
open import Cat.Functor.FullSubcategory -- Full subcategories
open import Cat.Functor.Equivalence.Complete -- Completeness respects equivalence

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.Monad -- Monad from an adjunction
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

About Kan extensions:

open import Cat.Functor.Kan -- Kan extensions
open import Cat.Functor.Kan.Nerve -- The nerve/realisation adjunction (Lan along よ)

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.Instances.Algebra
  -- Eilenberg-Moore categories preserve univalence

Category instances🔗

Here’s where we actually build some categories and prove that they have desirable properties.

-- Comma categories:
open import Cat.Instances.Comma
open import Cat.Instances.Comma.Univalent

open import Cat.Instances.Delooping -- Delooping a monoid to give a category
open import Cat.Instances.Discrete -- Discrete categories
open import Cat.Instances.Elements -- Category of elements of a presheaf

-- Functor categories:
open import Cat.Instances.Functor
open import Cat.Instances.Functor.Limits -- Co/limits in functor categories
open import Cat.Instances.Functor.Duality -- 2-cell duality in Cat

-- Completion of a category under splitting idempotents
open import Cat.Instances.Karoubi

open import Cat.Instances.Lift -- Lifting a category to higher universes
open import Cat.Instances.Product -- Product categories

-- 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

-- 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

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

-- Strict categories
open import Cat.Instances.StrictCat
open import Cat.Instances.StrictCat.Cohesive
  -- ^ Strict category structure is a sort of "spatial" structure on a category

Thin categories🔗

Strict thin categories are a presentation of pre-ordered sets, i.e. sets equipped with a transitive and reflexive relation — so we call them “prosets”. When this relation is antisymmetric, we additionally have a univalent thin strict category — so we call these “posets”.

open import Cat.Thin            -- Basics of thin categories
open import Cat.Thin.Limits     -- Limits in thin categories
open import Cat.Thin.Completion -- Free poset on a proset

Displayed categories🔗

We also have a work-in-progress formalisation of Foundations of Relative Category Theory, in which the core idea is thinking of “categories over categories”.

open import Cat.Displayed.Base             -- Displayed categories
open import Cat.Displayed.Total            -- Total category of a displayed category
open import Cat.Displayed.Cartesian        -- Cartesian lifts, cartesian fibrations
open import Cat.Displayed.Instances.Family -- Family fibration
open import Cat.Displayed.Instances.Slice  -- Canonical self-indexing

Topos theory🔗

Grothendieck topos theory developed constructively and predicatively.

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

Algebra🔗

In the Algebra namespace, the theory of universal algebra is developed from a univalent perspective. Specifically, every definition of an algebraic structure comes with an associated proof that it is univalent — concretely, identification of groups is group isomorphism (for instance).

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.Group                      -- Groups as monoids with inverses
open import Algebra.Group.Free                 -- Free groups
open import Algebra.Group.Cayley               -- Cayley's theorem
open import Algebra.Group.Cat.Base             -- Category of groups
open import Algebra.Group.Cat.FinitelyComplete -- Finite limits in Groups
open import Algebra.Group.Homotopy             -- Homotopy groups
open import Algebra.Group.Subgroup             -- Subgroups, images and kernels

open import Algebra.Group.Ab -- Abelian groups, and the category Ab
open import Algebra.Group.Ab.Free -- The free abelian group on a group