Chapters 1 and 2 use the rebuild2 formalization. Agda links for Chapter 3 remain temporarily unavailable.

The checked modules supporting these sections are accessible here.

Modules

Chapter 1: The language of synthetic category theory
1.1 The basic vocabulary

Terminal

SCT.VolumeI.Chapter01.Section01.Terminal

Terms

SCT.VolumeI.Chapter01.Section01.Terms

Vocabulary

SCT.VolumeI.Chapter01.Section01.Vocabulary

1.2 Coherences

Coherence

SCT.VolumeI.Chapter01.Section02.Coherence

Naturality

SCT.VolumeI.Chapter01.Section02.Naturality

Products

SCT.VolumeI.Chapter01.Section02.Products

Whiskering

SCT.VolumeI.Chapter01.Section02.Whiskering

1.3 Equivalences of categories

Retracts

SCT.VolumeI.Chapter01.Section03.Retracts

Squares

SCT.VolumeI.Chapter01.Section03.Squares

Supporting

SCT.VolumeI.Chapter01.Section03.Supporting

Identifications

FunctorCoherence

SCT.VolumeI.Chapter01.Section03.Identifications.FunctorCoherence

Inverses

SCT.VolumeI.Chapter01.Section03.Identifications.Inverses

OverBase

SCT.VolumeI.Chapter01.Section03.Identifications.OverBase

Triangles

SCT.VolumeI.Chapter01.Section03.Identifications.Triangles

Products

Equivalences

SCT.VolumeI.Chapter01.Section03.Products.Equivalences

Pairing

SCT.VolumeI.Chapter01.Section03.Products.Pairing

1.4 Mapping animae

Coherence

SCT.VolumeI.Chapter01.Section04.Coherence

Core

SCT.VolumeI.Chapter01.Section04.Core

Currying

SCT.VolumeI.Chapter01.Section04.Currying

Points

SCT.VolumeI.Chapter01.Section04.Points

Uncurrying

SCT.VolumeI.Chapter01.Section04.Uncurrying

1.5 Initial categories and coproducts

Copairing

SCT.VolumeI.Chapter01.Section05.Copairing

Coproducts

SCT.VolumeI.Chapter01.Section05.Coproducts

Initial

SCT.VolumeI.Chapter01.Section05.Initial

1.6 Pullbacks of categories

Cones

SCT.VolumeI.Chapter01.Section06.Cones

Embeddings

SCT.VolumeI.Chapter01.Section06.Embeddings

Pullbacks

SCT.VolumeI.Chapter01.Section06.Pullbacks

1.7 Functor categories

CoreOfFun

SCT.VolumeI.Chapter01.Section07.CoreOfFun

Currying

SCT.VolumeI.Chapter01.Section07.Currying

Evaluation

SCT.VolumeI.Chapter01.Section07.Evaluation

1.8 Pushout squares

Cocones

SCT.VolumeI.Chapter01.Section08.Cocones

1.9 Categories over a base
Chapter 2: The internal structure of categories
2.1 Morphisms and diagrams

Morphisms

SCT.VolumeI.Chapter02.Section01.Morphisms

Triangles

SCT.VolumeI.Chapter02.Section01.Triangles

2.2 The Segal axiom

SegalAxiom

SCT.VolumeI.Chapter02.Section02.SegalAxiom

Square Calculus
2.3 The Rezk axiom

RezkAxiom

SCT.VolumeI.Chapter02.Section03.RezkAxiom

RezkFibers

SCT.VolumeI.Chapter02.Section03.RezkFibers

2.4 Groupoids

Groupoids

SCT.VolumeI.Chapter02.Section04.Groupoids

2.5 Recognizing animae
2.6 Exercises
All named declarations in checked SCT modules