Chapter 1 code: rebuild2 edition, checked 14 October 2026. Included modules and omissions.
Read the Agda code alongside the book.Click dotted-underlined prose to read its Agda code alongside the book. Browse all code.
1.1 The basic vocabulary
We start by introducing the basic vocabulary of synthetic category theory.
Axiom A.1 (Primitives). The following are the primitives of synthetic category theory:
- (1)
-
There are categories, which we denote by symbols like \(C\), \(D\), and \(E\). Among categories, there are animae.
Agda Categories
CATAssumption, type checked
CAT : Context → Set c
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section01.Vocabulary whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Animae among categories
isAnAssumption, type checked
isAn : CAT Γ → Set a
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section01.Vocabulary where module _ {Γ : Context} whereANDefinition, checked
record AN : Set (c ⊔ a) where field category : CAT Γ witness : isAn category
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section01.Vocabulary where module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
- (2)
-
For categories \(C\) and \(D\), there is a primitive notion of a functor \(f\colon C\to D\). Every category has an identity functor \(\id _C\colon C\to C\). Given \(f\colon C\to D\) and \(g\colon D\to E\), there is a composite functor \(g\circ f\colon C\to E\), sometimes also denoted \(gf\).
Agda Functors
MAPAssumption, type checked
MAP : CAT Γ → CAT Γ → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section01.Vocabulary where module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Identity functors
idAssumption, type checked
id : (C : CAT Γ) → MAP C C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section01.Vocabulary where module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Composition of functors
_∘_Assumption, type checked
_∘_ : {C D E : CAT Γ} → MAP D E → MAP C D → MAP C E
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section01.Vocabulary where module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
- (3)
-
There exists an anima \(*\), called the terminal category.
Agda The terminal category
OneAssumption, type checked
One : CAT Γ
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section01.Vocabulary where module _ {Γ : Context} whereone-isAnAssumption, type checked
one-isAn : isAn One
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section01.Vocabulary where module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Categories and functors play the foundational role in synthetic category theory that sets and functions play in naive set theory. The role of the animae among the categories is to encode the idea of a homotopy-coherent collection: where objects in classical mathematics assemble into sets, in synthetic category theory they assemble into animae. A category additionally allows objects to be related by morphisms that need not be invertible.
For now, animae form a primitive distinguished class of categories. We regard every category equivalent to an anima as an anima. Once we have introduced morphisms and their invertibility, we can define groupoids as those categories in which every morphism is invertible. In the next chapter, we will impose the axiom that the animae are precisely the groupoids.
Definition 1.1.1 (Terms). A functor \(f\colon C\to D\) may be displayed in term notation as \[ x:C\vdash f(x):D. \] The functor and the expression \(f(x)\) are two notations for the same datum. We call \(x:C\) its context. More generally, we may write \(C\vdash t:D\) when the name of the variable is left implicit.
Agda Terms are functors
Term
Definition, checked
Term : CAT Γ → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terms where
module InContext {Γ : Context} (X : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Expressions display functors
Term
Definition, checked
Term : CAT Γ → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terms where
module InContext {Γ : Context} (X : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Throughout the chapter, we will indicate how the various rules we introduce may be written in their corresponding term notation. Conversely, any term expression obtained by combining these rules corresponds to a well-defined functor. The notation is inspired by type-theoretic approaches to synthetic category theory, such as [RS17; GWB24].
For example, composition of functors is displayed by substitution: for a second functor \(g\colon D\to E\), the term notation for the composite \(g\circ f\) is the expression \(x :C \vdash g(f(x)):E\). The term notation for the identity functor on \(C\) is \(x : C \vdash x : C\). We also refer to the latter as the universal term of \(C\).
Agda Substitution
_∘_
Assumption, type checked
_∘_ : {C D E : CAT Γ} → MAP D E → MAP C D → MAP C E
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Substitution by a functor
_∘_
Assumption, type checked
_∘_ : {C D E : CAT Γ} → MAP D E → MAP C D → MAP C E
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The universal term
id
Assumption, type checked
id : (C : CAT Γ) → MAP C C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Definition 1.1.2 (Objects). Given a term \(x:C\) in context \(\Gamma \), we say that \(x\) is an object (in context \(\Gamma )\) if \(\Gamma \) is an anima. If we speak about an object of \(C\), we mean an object in an arbitrary anima context.
An absolute object is a functor \(x\colon * \to C\), i.e. an object in context \(*\).
Agda Absolute objects
Obj-abs
Definition, checked
Obj-abs : CAT Γ → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
As already mentioned in the introduction of this book, one major difference between classical mathematics and homotopy theory is the idea that equality is structure. In classical mathematics, equality is a yes-no-question: two elements of a set are either equal or not. In homotopy theory, we change our perspective and allow there to be potentially several different identifications. The collection of identifications thus needs to assemble into an anima.
We thus introduce a primitive anima of identifications between every pair of functors. All our definitions and constructions should always respect identifications; we choose to implement this via explicit rules rather than via some deeper foundational principle as is for example done in homotopy type theory.
Axiom A.2 (Identifications). Given parallel functors \(f,g\colon C\to D\), there is an anima \((f= g)\), called the anima of identifications of \(f\) and \(g\). An identification \(\alpha : f = g\) is an absolute object of this anima.
Agda The isomorphism anima
_＝_
Assumption, type checked
_＝_ : {C D : CAT Γ} → MAP C D → MAP C D → CAT Γ
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} where＝-isAn
Assumption, type checked
＝-isAn : {C D : CAT Γ} (f g : MAP C D) → isAn (f ＝ g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Identifications
_=₁_
Definition, checked
_=₁_ : {C D : CAT Γ} → MAP C D → MAP C D → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
For \(h\colon D\to E\) and \(k\colon B\to C\), there are functors \[ h\star -\colon (f= g)\to (hf= hg), \qquad -\star k\colon (f= g)\to (fk= gk), \] called postwhiskering and prewhiskering, respectively.
Agda Postwhiskering
postWhisker
Assumption, type checked
postWhisker : {C D E : CAT Γ} {f g : MAP C D} (u : MAP D E) → MAP (f ＝ g) ((u ∘ f) ＝ (u ∘ g))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} where_◁_
Definition, checked
_◁_ : {P C D E : CAT Γ} {f g : MAP C D} → (u : MAP D E) → MAP P (f ＝ g) → MAP P ((u ∘ f) ＝ (u ∘ g))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module Operations where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Prewhiskering
preWhisker
Assumption, type checked
preWhisker : {B C D : CAT Γ} {f g : MAP C D} (k : MAP B C) → MAP (f ＝ g) ((f ∘ k) ＝ (g ∘ k))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} where_▷_
Definition, checked
_▷_ : {P B C D : CAT Γ} {f g : MAP C D} → MAP P (f ＝ g) → (k : MAP B C) → MAP P ((f ∘ k) ＝ (g ∘ k))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module Operations where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Notation 1.1.3. We also denote identifications \(\alpha : f = g\) in term notation as1 \[ x : C \vdash \alpha (x) : f(x) = g(x). \]
Agda Isomorphisms of whole expressions
_=₁_
Definition, checked
_=₁_ : {C D : CAT Γ} → MAP C D → MAP C D → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Footnote 1
1There is a slight clash between this notation and that of Definition 1.1.1: this does not mean a functor \(C \to f(x) = g(x)\), which does not even make sense.
Given an anima \(A\) and two absolute objects \(a,b:A\), we obtain an anima \(a = b\) of identifications between them. In particular, given two identifications \(\alpha ,\beta : f = g\), we may form the anima \(\alpha = \beta \). This construction may be iterated.
Agda Identifications of identifications
_=₂_
Definition, checked
_=₂_ : {C D : CAT Γ} {f g : MAP C D} → f =₁ g → f =₁ g → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Definition 1.1.4. A commutative square of functors, often displayed by means of a diagram
Agda Commutative squares
FunctorSquare
Definition, checked
record FunctorSquare (C D C′ D′ : CAT Γ) : Set m where constructor functor-square-data field top : MAP C D left : MAP C C′ right : MAP D D′ bottom : MAP C′ D′ cell : (right ∘ top) =₁ (bottom ∘ left)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Squares where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
consists of four functors \(f\), \(g\), \(h\) and \(f'\) with sources and targets as displayed in the diagram, together with a specified identification \(\alpha \colon h \circ f = f' \circ g\).
We will often refer to the data of just the four functors \(f\), \(g\), \(h\) and \(f'\) as a square, and say that the square commutes whenever an identification \(\alpha \colon h \circ f = f' \circ g\) can be provided.
A commutative triangle of functors, displayed by means of a diagram
Agda Commutative triangles
FunctorOverBase
Definition, checked
record FunctorOverBase {S : CAT Γ} (X Y : CategoryOverBase S) : Set m where constructor functor-over field functor : MAP (CategoryOverBase.category X) (CategoryOverBase.category Y) cell : (CategoryOverBase.map Y ∘ functor) =₁ CategoryOverBase.map X
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.RelativeFunctors where
module _ {Γ : Context} whereAbout this correspondence
The triangle is represented by a functor over a base: its underlying functor and specified commuting identification are bundled in this record. Triangles of identification families use the separate TriangleDiagram record.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
consists of three functors \(f\), \(g\) and \(h\) with sources and targets as displayed in the diagram, together with a specified identification \(\alpha \colon h = g \circ f\).
We will similarly display more general diagrams of functors by drawing directed planar graphs with vertices labeled by categories and edges labeled by functors. We consider diagrams whose faces are bounded by two directed paths with the same source and target, and fix a parenthesization for each composite. We say the diagram commutes if every face comes equipped with an identification between these two composites.
Definition 1.1.5 (Equivalence of categories). A functor \(f\colon C \to D\) is said to be an equivalence if there exists another functor \(g\colon D \to C\) equipped with identifications \(\id _{C} = gf\) and \(\id _{D} = fg\). We refer to \(g\) as the inverse of \(f\). Equivalences will often be introduced by writing \(f\colon C \iso D\). We may write \(C \simeq D\) to indicate that \(C\) and \(D\) are equivalent via an unnamed equivalence.
Agda Equivalence data
IsEquiv
Definition, checked
record IsEquiv {C D : CAT Γ} (f : MAP C D) : Set m where field inverse : MAP D C left-inverse-law : (id C) =₁ (inverse ∘ f) right-inverse-law : (id D) =₁ (f ∘ inverse)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda A chosen inverse
inverse
Definition, checked
inverse : MAP D C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} where
record IsEquiv {C D : CAT Γ} (f : MAP C D) : Set m whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda An unnamed equivalence
Equiv
Definition, checked
record Equiv (C D : CAT Γ) : Set m where field functor : MAP C D isEquiv : IsEquiv functor
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The next two axioms belong to the universal constructions of group B. We introduce them here because they are needed to formulate the coherence axioms of group A. We begin with the universal property of the terminal category.
Axiom B.1 (Terminal category). For every category \(T\), there is a functor \(p_T\colon T\to *\). For any functors \(f,g\colon T\to *\), the functor \[ p_{(f= g)}\colon (f= g)\longrightarrow * \] is an equivalence.
Agda The terminal functor
terminate
Assumption, type checked
terminate : (C : CAT Γ) → MAP C One
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terminal where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Terminal universality
terminal-identifications-isEquiv
Assumption, type checked
terminal-identifications-isEquiv : {T : CAT Γ} (f g : MAP T One) → IsEquiv (terminate (f ＝ g))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terminal where
module _ {Γ : Context} whereterminal-identifications-contractible
Derivation, checked
terminal-identifications-contractible : {X : CAT Γ} (f g : MAP X One) → IsContractible (f ＝ g)
Proof / implementation
terminal-identifications-contractible = terminal-identifications-isEquiv
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terminal where
module Contractibility where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
In particular, any two functors to \(*\) are identified.
Agda Uniqueness of terminal maps
terminal-identification
Derivation, checked
terminal-identification : {P : CAT Γ} (f g : MAP P One) → f =₁ g
Proof / implementation
terminal-identification f g = IsEquiv.inverse (terminal-identifications-isEquiv f g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terminal where
module Constructions where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Definition 1.1.6 (Contractible category). A category \(C\) is called contractible if the functor \(p_{C}\colon C \to *\) is an equivalence.
Agda Contractible categories
IsContractible
Definition, checked
IsContractible : CAT Γ → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terminal where
module Constructions where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Definition 1.1.7 (Constant functor). Let \(C\) and \(D\) be categories and let \(x\) be an absolute object of \(D\). We define the constant functor \(\const _x\colon C \to D\) as the composite \(x \circ p_C\colon C \to D\): \[ \const _x: C \xrightarrow {p_C} * \xrightarrow {x} D. \]
Agda Constant functors
const
Definition, checked
const : {P C : CAT Γ} → Obj-abs C → MAP P C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terminal where
module Constructions where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Remark 1.1.8. Observe that a category \(C\) is contractible if and only if there exists an absolute object \(x\colon * \to C\) equipped with an identification \(\id _C = \const _x\). Such an identification \(H\colon \id _C = \const _x\) is called a contraction of \(C\) onto \(x\).
Agda Characterizing contractibility
contractible-to-contraction
Derivation, checked
contractible-to-contraction : {C : CAT Γ} → IsContractible C → Contraction C
Proof / implementation
contractible-to-contraction e = record { center = IsEquiv.inverse e ; contraction = IsEquiv.left-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terminal where
module Contractibility where
module _ {Γ : Context} wherecontraction-to-contractible
Derivation, checked
contraction-to-contractible : {C : CAT Γ} → Contraction C → IsContractible C
Proof / implementation
contraction-to-contractible {C} H = record { inverse = Contraction.center H ; left-inverse-law = Contraction.contraction H ; right-inverse-law = terminal-identification (id One) (terminate C ∘ Contraction.center H) }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terminal where
module Contractibility where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Contractions
Contraction
Definition, checked
record Contraction (C : CAT Γ) : Set m where field center : Obj-abs C contraction : (id C) =₁ (const center)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Terminal where
module Contractibility where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
We will postpone most category constructors until later in the chapter, but we need one crucial one right now already in order to state various coherence relations.
Axiom B.2 (Product of categories). The product of categories \(C\) and \(D\) is a category \(C\times D\) equipped with projection functors \(\pr _1\colon C\times D\to C\) and \(\pr _2\colon C\times D\to D\).
Agda Binary products
_×_
Assumption, type checked
_×_ : CAT Γ → CAT Γ → CAT Γ
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The two projections
pr₁
Assumption, type checked
pr₁ : {C D : CAT Γ} → MAP (C × D) C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} wherepr₂
Assumption, type checked
pr₂ : {C D : CAT Γ} → MAP (C × D) D
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Given \(f\colon T\to C\) and \(g\colon T\to D\), there is a functor \((f,g)\colon T\to C\times D\) equipped with identifications \(\beta ^1_{f,g}:\pr _1(f,g)=f\) and \(\beta ^2_{f,g}:\pr _2(f,g)=g\). For any two functors \(h,k\colon T\to C\times D\), the functor \[ (\pr _1\star -,\pr _2\star -)\colon (h= k)\longrightarrow (\pr _1 h=\pr _1 k)\times (\pr _2 h=\pr _2 k) \] is an equivalence. If \(C\) and \(D\) are animae, then \(C\times D\) is an anima.
Agda Pairing functors
pair
Assumption, type checked
pair : {P C D : CAT Γ} → MAP P C → MAP P D → MAP P (C × D)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Projection comparisons
pair-β₁
Assumption, type checked
pair-β₁ : {P C D : CAT Γ} (f : MAP P C) (g : MAP P D) → (pr₁ ∘ pair f g) =₁ f
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} wherepair-β₂
Assumption, type checked
pair-β₂ : {P C D : CAT Γ} (f : MAP P C) (g : MAP P D) → (pr₂ ∘ pair f g) =₁ g
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Universality on isomorphism animae
product-coordinates
Definition, checked
product-coordinates : {C D : CAT Γ} (f g : Term (C × D)) → MAP (Equal f g) ((Equal (pr₁ ∘ f) (pr₁ ∘ g)) × (Equal (pr₂ ∘ f) (pr₂ ∘ g)))
Proof / implementation
product-coordinates f g = pair (postWhisker pr₁) (postWhisker pr₂)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Products where
module Coordinates where
module _ {Γ : Context} where
module _ {T : CAT Γ} whereproduct-coordinates-isEquiv
Assumption, type checked
product-coordinates-isEquiv : {T C D : CAT Γ} (f g : MAP T (C × D)) → IsEquiv (product-coordinates f g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Products where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Products of animae
product-isAn
Assumption, type checked
product-isAn : {C D : CAT Γ} → isAn C → isAn D → isAn (C × D)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
We refer to the functor \((f,g)\) as the pair construction. In term notation, it is written \[ x:T \vdash (f(x),g(x)): C \times D, \] with identifications \(\pr _1(f(x),g(x))= f(x)\) and \(\pr _2(f(x),g(x))= g(x)\). For arbitrary expressions \(h(x),k(x):C\times D\), two identifications \(\alpha (x):\pr _1 h(x)=\pr _1 k(x)\) and \(\beta (x):\pr _2 h(x)=\pr _2 k(x)\) give an identification \((\alpha (x),\beta (x)):h(x)= k(x)\) by applying an inverse of the displayed equivalence. Its two projections are identified with \(\alpha \) and \(\beta \).
Agda Pairing terms
pair
Assumption, type checked
pair : {P C D : CAT Γ} → MAP P C → MAP P D → MAP P (C × D)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Lifting the two comparisons
pair⁼
Derivation, checked
pair⁼ : {x x′ : Term C} {y y′ : Term D} → x ＝ x′ → y ＝ y′ → pair x y ＝ pair x′ y′
Proof / implementation
pair⁼ {x = x} {x′} {y} {y′} α β = ProductIdentification.identification (const ((pair-β₁ x′ y′) ⁻¹) ∙ (α ∙ const (pair-β₁ x y))) (const ((pair-β₂ x′ y′) ⁻¹) ∙ (β ∙ const (pair-β₂ x y)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Products where
module Calculus where
module _ {Γ : Context} where
module _ {A X C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Projections of a lifted comparison
pair⁼-β₁
Derivation, checked
pair⁼-β₁ : {x x′ : Term C} {y y′ : Term D} (α : x ＝ x′) (β : y ＝ y′) → (pr₁ ◁ pair⁼ α β) =₁ (const ((pair-β₁ x′ y′) ⁻¹) ∙ (α ∙ const (pair-β₁ x y)))
Proof / implementation
pair⁼-β₁ {x = x} {x′} {y} {y′} α β = ProductIdentification.β₁ (const ((pair-β₁ x′ y′) ⁻¹) ∙ (α ∙ const (pair-β₁ x y))) (const ((pair-β₂ x′ y′) ⁻¹) ∙ (β ∙ const (pair-β₂ x y)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Products where
module Calculus where
module _ {Γ : Context} where
module _ {A X C D : CAT Γ} wherepair⁼-β₂
Derivation, checked
pair⁼-β₂ : {x x′ : Term C} {y y′ : Term D} (α : x ＝ x′) (β : y ＝ y′) → (pr₂ ◁ pair⁼ α β) =₁ (const ((pair-β₂ x′ y′) ⁻¹) ∙ (β ∙ const (pair-β₂ x y)))
Proof / implementation
pair⁼-β₂ {x = x} {x′} {y} {y′} α β = ProductIdentification.β₂ (const ((pair-β₁ x′ y′) ⁻¹) ∙ (α ∙ const (pair-β₁ x y))) (const ((pair-β₂ x′ y′) ⁻¹) ∙ (β ∙ const (pair-β₂ x y)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Products where
module Calculus where
module _ {Γ : Context} where
module _ {A X C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Remark 1.1.9. Given categories \(C\) and \(D\), we define a span from \(C\) to \(D\) to be a triple \((T,f,g)\) consisting of a category \(T\) together with functors \(f\colon T \to C\) and \(g\colon T \to D\). Axiom B.2 may be rephrased as saying that the triple \((C \times D, \pr _1, \pr _2)\) is the terminal span from \(C\) to \(D\): every span \(C \leftarrow T \to D\) admits a factorization through \(C \times D\), and an identification of two functors \(T \to C \times D\) amounts to identifications between their respective components.
Agda Spans
Span
Definition, checked
record Span (C D : CAT Γ) : Set (c ⊔ m) where field apex : CAT Γ left : MAP apex C right : MAP apex D
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Products where
module _ {Γ : Context} whereSpanMap
Definition, checked
record SpanMap {C D : CAT Γ} (U Z : Span C D) : Set m where field functor : MAP (Span.apex U) (Span.apex Z) left-triangle : (Span.left Z ∘ functor) =₁ (Span.left U) right-triangle : (Span.right Z ∘ functor) =₁ (Span.right U)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Products where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The product span
productSpan
Derivation, checked
productSpan : (C D : CAT Γ) → Span C D
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Products where
module ProductSpans where
module _ {Γ : Context} wheretoProductSpan
Derivation, checked
toProductSpan : {C D : CAT Γ} (U : Span C D) → SpanMap U (productSpan C D)
Proof / implementation
toProductSpan U = record { functor = pair (Span.left U) (Span.right U) ; left-triangle = pair-β₁ (Span.left U) (Span.right U) ; right-triangle = pair-β₂ (Span.left U) (Span.right U) }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Products where
module ProductSpans where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Comparison of maps of spans
pair₌-unique
Derivation, checked
pair₌-unique : {C D : CAT Γ} {z z′ : Term (C × D)} {x x′ : Term C} {y y′ : Term D} {b₁ : ((pr₁ ∘ z) ＝ x)} {b₁′ : ((pr₁ ∘ z′) ＝ x′)} {b₂ : ((pr₂ ∘ z) ＝ y)} {b₂′ : ((pr₂ ∘ z′) ＝ y′)} {α : x ＝ x′} {β : y ＝ y′} {ε ε′ : z ＝ z′} → SquareCell₌ (pr₁ ◁ ε) α b₁ b₁′ → SquareCell₌ (pr₂ ◁ ε) β b₂ b₂′ → SquareCell₌ (pr₁ ◁ ε′) α b₁ b₁′ → SquareCell₌ (pr₂ ◁ ε′) β b₂ b₂′ → ε =₁ ε′
Proof / implementation
pair₌-unique {b₁′ = b₁′} {b₂′ = b₂′} first second first′ second′ = pair₌-extensionality (cancel-left b₁′ (first′ ⁻¹ ∙ first)) (cancel-left b₂′ (second′ ⁻¹ ∙ second))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Convention 1.1.10. A term of the form \(z : C \times D \vdash t : E\) may also be written as \[ x:C, y:D \vdash t(x,y) : E \] whenever the term \(t\) only depends on the variable \(z\) through the two projections \(\pr _1(z)\) and \(\pr _2(z)\). The expression \(t(x,y)\) is then obtained from \(t\) by replacing \(\pr _1(z)\) by \(x\) and \(\pr _2(z)\) by \(y\). For more than two variables we use a fixed parenthesization of their product.
Agda Product parameter notation
pr₁
Assumption, type checked
pr₁ : {C D : CAT Γ} → MAP (C × D) C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} wherepr₂
Assumption, type checked
pr₂ : {C D : CAT Γ} → MAP (C × D) D
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section01.Vocabulary where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.