Read the Agda code alongside the book.Click dotted-underlined prose to read its Agda code alongside the book. Browse all code.
2.1 Morphisms and diagrams
In the case of morphisms, we use the following test category.
Axiom C.1 (Walking morphism). There is a category \([1]\) equipped with objects \(0,1\colon * \to [1]\). Moreover, the functors \(0,1\colon * \to [1]^{\simeq }\) induce an equivalence \[ \lra {0,1}\colon * \sqcup * \iso [1]^{\simeq }. \]
Agda The walking morphism
[1]
Assumption, type checked
[1] : 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.Chapter02.Section01.WalkingMorphism where
module _ {Γ : Context} wherezero
Assumption, type checked
zero one : MAP One [1]
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.Chapter02.Section01.WalkingMorphism where
module _ {Γ : Context} whereone
Assumption, type checked
zero one : MAP One [1]
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.Chapter02.Section01.WalkingMorphism where
module _ {Γ : Context} whereintervalCore-isEquiv
Assumption, type checked
intervalCore-isEquiv : IsEquiv intervalCore
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.Chapter02.Section01.WalkingMorphism where
module _ {Γ : Context} whereAbout this correspondence
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 interval category
[1]
Assumption, type checked
[1] : 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.Chapter02.Section01.WalkingMorphism where
module _ {Γ : Context} whereAbout this correspondence
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 distinguished objects
zero
Assumption, type checked
zero one : MAP One [1]
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.Chapter02.Section01.WalkingMorphism where
module _ {Γ : Context} whereone
Assumption, type checked
zero one : MAP One [1]
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.Chapter02.Section01.WalkingMorphism where
module _ {Γ : Context} whereAbout this correspondence
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 specified interval core equivalence
intervalCore
Definition, checked
intervalCore : MAP (One ⊔ One) (Core [1])
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.Chapter02.Section01.WalkingMorphism where
module _ {Γ : Context} whereintervalCore-isEquiv
Assumption, type checked
intervalCore-isEquiv : IsEquiv intervalCore
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.Chapter02.Section01.WalkingMorphism where
module _ {Γ : Context} whereAbout this correspondence
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, \(*\sqcup *\) is an anima, since it is equivalent to the anima \([1]^\simeq \).
Agda The two-point category is an anima
two-point-isAn
Derivation, checked
two-point-isAn : isAn (One {Γ = Γ} ⊔ One)
Proof / implementation
two-point-isAn = equivalence-reflects-anima intervalCore intervalCore-isEquiv (core-isAn [1])
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.Chapter02.Section05.ArrowCoproducts where
module _ {Γ : Context} whereAbout this correspondence
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.
By substitution along \(p_\Gamma \colon \Gamma \to *\), the two displayed objects also give terms \[ \Gamma \vdash 0,1:[1] \] in every categorical context \(\Gamma \).
The category \([1]\) is called the walking morphism and should be thought of as the poset \(\{0 \leq 1\}\).
Let us introduce some standard terminology regarding functors out of \([1]\).
Definition 2.1.1 (Morphisms). A morphism in a category \(C\) is defined as a functor \(f\colon [1] \to C\), or equivalently as an object of the arrow category \(\Fun ([1],C)\).
Agda Morphisms and their endpoints
Mor
Definition, checked
Mor : 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 --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereMorphism
Definition, checked
record Morphism {C : CAT Γ} (x y : MAP One C) : Set m where field diagram : Mor C source-frame : source diagram =₁ x target-frame : target diagram =₁ y
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} wheresource
Definition, checked
source target : {C : CAT Γ} → Mor C → MAP One C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} wheretarget
Definition, checked
source target : {C : CAT Γ} → Mor C → MAP One C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereev₀
Definition, checked
ev₀ ev₁ : {C : CAT Γ} → MAP (Ar C) C
Proof / implementation
ev₀ = AtPoint.evaluation zero ev₁ = AtPoint.evaluation one
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereev₁
Definition, checked
ev₀ ev₁ : {C : CAT Γ} → MAP (Ar C) C
Proof / implementation
ev₀ = AtPoint.evaluation zero ev₁ = AtPoint.evaluation one
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 morphism is an interval diagram
Mor
Definition, checked
Mor : 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 --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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.
Every morphism \(f\colon [1] \to C\) has a source/domain \(f(0)\colon * \to C\) and a target/codomain \(f(1) \colon * \to C\), obtained by precomposition with \(0,1\colon * \to [1]\). If \(f\) is a morphism in \(C\), and \(x\) and \(y\) are objects of \(C\), we will often write \(f\colon x \to y\) to indicate that \(f\) comes equipped with identifications \(x = f(0)\) and \(y = f(1)\), which we will mostly leave implicit in the notation. In this case we say that \(f\) is a morphism from \(x\) to \(y\).
Agda Source of a morphism
source
Definition, checked
source target : {C : CAT Γ} → Mor C → MAP One C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 Target of a morphism
target
Definition, checked
source target : {C : CAT Γ} → Mor C → MAP One C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 morphism with fixed endpoints
Morphism
Definition, checked
record Morphism {C : CAT Γ} (x y : MAP One C) : Set m where field diagram : Mor C source-frame : source diagram =₁ x target-frame : target diagram =₁ y
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 write \(\ev _0,\ev _1\colon \Fun ([1],C) \to C\) for the source and target functors, given by evaluation at \(0\) and \(1\), cf. Construction 1.7.6.
Agda Source and target functors
ev₀
Definition, checked
ev₀ ev₁ : {C : CAT Γ} → MAP (Ar C) C
Proof / implementation
ev₀ = AtPoint.evaluation zero ev₁ = AtPoint.evaluation one
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereev₁
Definition, checked
ev₀ ev₁ : {C : CAT Γ} → MAP (Ar C) C
Proof / implementation
ev₀ = AtPoint.evaluation zero ev₁ = AtPoint.evaluation one
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 2.1.2 (Natural transformations). If \(C\) and \(D\) are categories, we define a natural transformation of functors \(C \to D\) to be a morphism in \(\Fun (C,D)\). By (un)currying, this may equivalently be encoded as a functor \([1] \times C \to D\).
Agda Natural transformations
NatTrans
Definition, checked
NatTrans : (C D : 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 --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} wheretransformation-diagram
Definition, checked
transformation-diagram : {C D : CAT Γ} → NatTrans C D → MAP ([1] × C) D
Proof / implementation
transformation-diagram = funUncurry
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} wherediagram-transformation
Definition, checked
diagram-transformation : {C D : CAT Γ} → MAP ([1] × C) D → NatTrans C D
Proof / implementation
diagram-transformation = funCurry
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} wheretransformation-β
Derivation, checked
transformation-β : {C D : CAT Γ} (H : MAP ([1] × C) D) → transformation-diagram (diagram-transformation H) =₁ H
Proof / implementation
transformation-β = funCurry-β
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} wheretransformation-η
Derivation, checked
transformation-η : {C D : CAT Γ} (α : NatTrans C D) → diagram-transformation (transformation-diagram α) =₁ α
Proof / implementation
transformation-η = funCurry-η
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 Natural transformations as morphisms
NatTrans
Definition, checked
NatTrans : (C D : 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 --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 uncurried transformation diagram
transformation-diagram
Definition, checked
transformation-diagram : {C D : CAT Γ} → NatTrans C D → MAP ([1] × C) D
Proof / implementation
transformation-diagram = funUncurry
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} wherediagram-transformation
Definition, checked
diagram-transformation : {C D : CAT Γ} → MAP ([1] × C) D → NatTrans C D
Proof / implementation
diagram-transformation = funCurry
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 2.1.3 (Arrow category/hom anima). For a category \(C\), we define its arrow category as \[ \Ar (C) \quad := \quad \Fun ([1],C). \] Given absolute objects \(x\) and \(y\) of \(C\), we define the hom anima \(C(x,y)\) via the following pullback square:
Agda Arrow categories and hom categories
Ar
Definition, checked
Ar : 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 --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereHom
Definition, checked
Hom : (C : CAT Γ) → MAP One C → MAP One C → 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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereendpointMap
Definition, checked
endpointMap : (C : CAT Γ) → MAP (Ar C) (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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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 arrow category
Ar
Definition, checked
Ar : 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 --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 hom pullback
Hom
Definition, checked
Hom : (C : CAT Γ) → MAP One C → MAP One C → 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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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.
At this point, the pullback defines a category. We call it the hom anima in anticipation of Corollary 5.3.5 (outside selection), where it will be shown to be an anima. Observe that the absolute objects of \(C(x,y)\) are triples \((f,\alpha ,\beta )\), where \(f\colon x' \to y'\) is a morphism in \(C\) and \(\alpha \colon x = x'\) and \(\beta \colon y = y'\) are identifications in \(C\). We will sometimes use the alternative notation \(\Hom _C(x,y)\) for \(C(x,y)\).
Convention 2.1.4 (Morphism expressions). For functors \(f,g\colon C\to D\), the notation \[ x:C\vdash \alpha (x):f(x)\to g(x) \] means a functor \(H:C\times [1]\to D\) together with identifications \(H(-,0)= f\) and \(H(-,1)= g\). Currying gives its equivalent description as a functor \(C\to \Ar (D)\) with the same endpoint comparisons. In the absolute case, we use \([1]\to D\) directly.
Agda Morphism expressions with endpoint comparisons
Morphism
Definition, checked
record Morphism {C : CAT Γ} (x y : MAP One C) : Set m where field diagram : Mor C source-frame : source diagram =₁ x target-frame : target diagram =₁ y
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereDiagramFamily
Definition, checked
record DiagramFamily {P C : CAT Γ} (f g : MAP P C) : Set m where field diagram : MAP (P × [1]) C source-frame : (diagram ∘ insert zero) =₁ f target-frame : (diagram ∘ insert one) =₁ g
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereencode
Definition, checked
encode : {P C : CAT Γ} {f g : MAP P C} → DiagramFamily f g → MorphismFamily f g
Proof / implementation
encode α = record { arrow = funCurry (DiagramFamily.diagram α) ; source-frame = DiagramFamily.source-frame α ∙ AtPoint.curry-image zero (DiagramFamily.diagram α) ; target-frame = DiagramFamily.target-frame α ∙ AtPoint.curry-image one (DiagramFamily.diagram α) }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} wheredecode
Definition, checked
decode : {P C : CAT Γ} {f g : MAP P C} → MorphismFamily f g → DiagramFamily f g
Proof / implementation
decode α = record { diagram = funUncurry (MorphismFamily.arrow α) ; source-frame = MorphismFamily.source-frame α ∙ (AtPoint.uncurry-image zero (MorphismFamily.arrow α)) ⁻¹ ; target-frame = MorphismFamily.target-frame α ∙ (AtPoint.uncurry-image one (MorphismFamily.arrow α)) ⁻¹ }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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.
An identification between two morphism expressions with the same displayed source and target is an identification of their interval diagrams together with compatibility with the two endpoint comparisons. For absolute morphisms between fixed objects \(a,b:D\), it is an identification in \(D(a,b)\). In context \(x:C\), with the same fixed endpoints, it is an identification between functors \(C\to D(a,b)\). For general \(f\) and \(g\) that vary with \(x\), it is simply a functor into \(D\) with the two endpoint compatibilities.
Agda Identifications between morphism expressions
MorphismFamilyIdentification
Definition, checked
record MorphismFamilyIdentification (X : CAT Γ) {P C : CAT Γ} {f g : MAP P C} (α β : MorphismFamily f g) : Set m where open Terms.Equalities X using (_＝_) field identification : MorphismFamily.arrow α ＝ MorphismFamily.arrow β source-compatible : (const (MorphismFamily.source-frame β) ∙ (ev₀ ◁ identification)) =₁ const (MorphismFamily.source-frame α) target-compatible : (const (MorphismFamily.target-frame β) ∙ (ev₁ ◁ identification)) =₁ const (MorphismFamily.target-frame α)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereDiagramFamilyIdentification
Definition, checked
record DiagramFamilyIdentification (X : CAT Γ) {P C : CAT Γ} {f g : MAP P C} (α β : DiagramFamily f g) : Set m where open Terms.Equalities X using (_＝_) field identification : DiagramFamily.diagram α ＝ DiagramFamily.diagram β source-compatible : (const (DiagramFamily.source-frame β) ∙ (identification ▷ insert zero)) =₁ const (DiagramFamily.source-frame α) target-compatible : (const (DiagramFamily.target-frame β) ∙ (identification ▷ insert one)) =₁ const (DiagramFamily.target-frame α)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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.
Construction 2.1.5 (From identifications to morphism expressions). A primitive identification \(\alpha \colon f= g\) determines a morphism expression from \(f(x)\) to \(g(x)\). Take the constant interval \[ C\times [1]\xrightarrow {\pr _1}C\xrightarrow {f}D, \] with its canonical source identification, and with target identification given by \(\alpha \).
Agda From primitive identifications to morphisms
identification-family
Derivation, checked
identification-family : {P C : CAT Γ} {f g : MAP P C} → f =₁ g → MorphismFamily f g
Proof / implementation
identification-family {f = f} p = record { arrow = MorphismFamily.arrow (identity-family f) ; source-frame = MorphismFamily.source-frame (identity-family f) ; target-frame = p ∙ MorphismFamily.target-frame (identity-family f) }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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.
Construction 2.1.6. Let \(f\colon C \to D\) be a functor and consider two absolute objects \(x\) and \(y\) of \(C\). Then the induced functor \(f_*\colon \Ar (C) \to \Ar (D)\) induces a functor \[ f\colon C(x,y) \to D(f(x),f(y)) \] on fibers.
Agda Functoriality of hom categories
map-hom
Definition, checked
map-hom : {C D : CAT Γ} (F : MAP C D) (x y : MAP One C) → MAP (Hom C x y) (Hom D (F ∘ x) (F ∘ 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.Chapter02.Section01.MorphismFunctor where
module _ {Γ : Context} whereAbout this correspondence
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.
Example 2.1.7 (Identity morphism). In a common categorical context \(\Gamma \), a term \(\Gamma \vdash x:C\) determines the identity morphism \(\Gamma \vdash \id _x\colon x\to x\), defined by currying the composite \[ \Gamma \times [1]\xrightarrow {\pr _1}\Gamma \xrightarrow {x}C. \] It comes with a specified identification from its uncurrying to this composite. For every functor \(f\colon C\to D\), there is a preferred identification \(\Gamma \vdash f(\id _x)=\id _{f(x)}\). In the absolute case \(\Gamma =*\), this recovers the usual identity morphism \(\id _x\in C(x,x)\).
Agda Identity morphisms
identity-family
Definition, checked
identity-family : {P C : CAT Γ} (f : MAP P C) → MorphismFamily f f
Proof / implementation
identity-family {P} {C} f = record { arrow = funCurry (f ∘ pr₁) ; source-frame = boundary zero ; target-frame = boundary one } where boundary : (a : MAP One [1]) → (AtPoint.evaluation a ∘ funCurry (f ∘ pr₁)) =₁ f boundary a = comp-unitʳ f ∙ ((f ◁ pair-β₁ (id P) (const a)) ∙ (comp-assoc (insert a) pr₁ f ∙ AtPoint.curry-image a (f ∘ pr₁)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereidentityArrow
Definition, checked
identityArrow : {C : CAT Γ} → MAP C (Ar C)
Proof / implementation
identityArrow {C} = constantArrow [1] C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section01.Morphisms where
module _ {Γ : Context} whereAbout this correspondence
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 Functors preserve identities
post-identity-family
Derivation, checked
post-identity-family : {Γ : Context} {P C D : CAT Γ} (F : MAP C D) (f : MAP P C) → MorphismFamilyIdentification One (map-morphism-family F (identity-family f)) (identity-family (F ∘ f))
Proof / implementation
post-identity-family = IdentityImage.value
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.Chapter02.Section01.IdentityFamilyPostcomposition whereAbout this correspondence
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 2.1.8 (Slice categories). Let \(C\) be a category and let \(x\) be an absolute object of \(C\). We define the slice categories \(C_{/x}\) and \(C_{x/}\) via the following two pullback diagrams:
Agda Slice and coslice categories
Slice
Definition, checked
Slice Coslice : (C : CAT Γ) → MAP One C → CAT Γ
Proof / implementation
Slice C x = EndpointFiber.category (id C) (const x) Coslice C x = EndpointFiber.category (const x) (id 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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereCoslice
Definition, checked
Slice Coslice : (C : CAT Γ) → MAP One C → CAT Γ
Proof / implementation
Slice C x = EndpointFiber.category (id C) (const x) Coslice C x = EndpointFiber.category (const x) (id 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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereslice-projection
Definition, checked
slice-projection : {C : CAT Γ} (x : MAP One C) → MAP (Slice C x) 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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} wherecoslice-projection
Definition, checked
coslice-projection : {C : CAT Γ} (x : MAP One C) → MAP (Coslice C x) 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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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 slice and coslice
Slice
Definition, checked
Slice Coslice : (C : CAT Γ) → MAP One C → CAT Γ
Proof / implementation
Slice C x = EndpointFiber.category (id C) (const x) Coslice C x = EndpointFiber.category (const x) (id 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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereCoslice
Definition, checked
Slice Coslice : (C : CAT Γ) → MAP One C → CAT Γ
Proof / implementation
Slice C x = EndpointFiber.category (id C) (const x) Coslice C x = EndpointFiber.category (const x) (id 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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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, an object of the category \(C_{/x}\) consists of a pair \((y,u)\) where \(y\) is an object of \(C\) and \(u\colon y \to x\) is a morphism in \(C\). Similarly the objects of \(C_{x/}\) are pairs \((y,v)\) where now \(v\) is a morphism in \(C\) of the form \(v\colon x \to y\).
Definition 2.1.9 (Initial/terminal object). An absolute object \(x\) in a category \(C\) is called terminal if the functor \(p_x\colon C_{/x} \to C\) is an equivalence. Dually, \(x\) is called initial if \(q_x\colon C_{x/} \to C\) is an equivalence.
Agda Initial and terminal objects
IsTerminal
Definition, checked
IsTerminal IsInitial : {C : CAT Γ} → MAP One C → Set m
Proof / implementation
IsTerminal x = IsEquiv (slice-projection x) IsInitial x = IsEquiv (coslice-projection x) -- Initial and terminal endpoints of the directed interval.
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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereIsInitial
Definition, checked
IsTerminal IsInitial : {C : CAT Γ} → MAP One C → Set m
Proof / implementation
IsTerminal x = IsEquiv (slice-projection x) IsInitial x = IsEquiv (coslice-projection x) -- Initial and terminal endpoints of the directed interval.
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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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 objects
IsTerminal
Definition, checked
IsTerminal IsInitial : {C : CAT Γ} → MAP One C → Set m
Proof / implementation
IsTerminal x = IsEquiv (slice-projection x) IsInitial x = IsEquiv (coslice-projection x) -- Initial and terminal endpoints of the directed interval.
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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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 Initial objects
IsInitial
Definition, checked
IsTerminal IsInitial : {C : CAT Γ} → MAP One C → Set m
Proof / implementation
IsTerminal x = IsEquiv (slice-projection x) IsInitial x = IsEquiv (coslice-projection x) -- Initial and terminal endpoints of the directed interval.
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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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 2.1.10. Observe that the fiber of \(p_x\) over an absolute object \(y\) is the hom anima \(C(y,x)\), using the pasting law for pullback squares. In particular, if \(x\) is terminal then \(C(y,x)\) is contractible for every \(y\). Dually, if \(x\) is initial then \(C(x,y)\) is contractible for all \(y\). The converse will be established later, once additional axioms have been introduced.
Agda The fiber of the slice projection
fiber-to-hom-isEquiv
Derivation, checked
fiber-to-hom-isEquiv : IsEquiv fiber-to-hom
Proof / implementation
fiber-to-hom-isEquiv = Fiber.fiber-to-target-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.Chapter02.Section01.SliceFibers where
module _ {Γ : Context} where
module EndpointFiberAt {B C : CAT Γ} (u v : MAP B C) (y : MAP One B)
(x₀ x₁ : MAP One C) (α : (u ∘ y) =₁ x₀) (β : (v ∘ y) =₁ x₁) whereAbout this correspondence
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 Hom into a terminal object
terminal-hom-contractible
Derivation, checked
terminal-hom-contractible : {C : CAT Γ} (x : MAP One C) → IsTerminal x → (y : MAP One C) → IsContractible (Hom C y x)
Proof / implementation
terminal-hom-contractible x e y = TerminalFiber.hom-contractible x y 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.Chapter02.Section01.SliceFibers where
module _ {Γ : Context} whereAbout this correspondence
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 Hom out of an initial object
initial-hom-contractible
Derivation, checked
initial-hom-contractible : {C : CAT Γ} (x : MAP One C) → IsInitial x → (y : MAP One C) → IsContractible (Hom C x y)
Proof / implementation
initial-hom-contractible x e y = InitialFiber.hom-contractible x y 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.Chapter02.Section01.SliceFibers where
module _ {Γ : Context} whereAbout this correspondence
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.
Axiom C.2. The absolute object \(0\colon *\to [1]\) is initial. The absolute object \(1\colon *\to [1]\) is terminal.
Agda The endpoints are initial and terminal
interval-zero-initial
Assumption, type checked
interval-zero-initial : IsInitial (zero {Γ = Γ})
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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereinterval-one-terminal
Assumption, type checked
interval-one-terminal : IsTerminal (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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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 initial endpoint
interval-zero-initial
Assumption, type checked
interval-zero-initial : IsInitial (zero {Γ = Γ})
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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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 terminal endpoint
interval-one-terminal
Assumption, type checked
interval-one-terminal : IsTerminal (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.Chapter02.Section01.HomAndSlices where
module _ {Γ : Context} whereAbout this correspondence
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.
Construction 2.1.11. As a consequence of Axiom C.2, we obtain the following two pullback squares:
Agda Minimum and maximum
min
Definition, checked
min max : MAP ([1] × [1]) ([1] {Γ = Γ})
Proof / implementation
min = funUncurry d₂ max = funUncurry 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheremax
Definition, checked
min max : MAP ([1] × [1]) ([1] {Γ = Γ})
Proof / implementation
min = funUncurry d₂ max = funUncurry 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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.
Using \(\Ar (C)=\Fun ([1],C)\), the two top horizontal maps in these diagrams correspond under currying/uncurrying to functors \[ \min \colon [1] \times [1] \to [1] \qquadtext { and } \max \colon [1] \times [1] \to [1]. \]
Lemma 2.1.12. The maps \(\max \) and \(\min \) satisfy the identifications \begin {align*} \max (x,0) &= x = \max (0,x), & \max (x,1) &= 1 = \max (1,x), \\ \min (x,0) &= 0 = \min (0,x), & \min (x,1) &= x = \min (1,x), \end {align*}
Agda Endpoint identities for minimum and maximum
min-right-zero
Derivation, checked
min-right-zero : (min ∘ insert zero) =₁ const (zero {Γ = Γ})
Proof / implementation
min-right-zero = s₀-d₂ ∙ (AtPoint.uncurry-image zero 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheremin-right-one
Derivation, checked
min-right-one : (min ∘ insert one) =₁ id ([1] {Γ = Γ})
Proof / implementation
min-right-one = s₁-d₂ ∙ (AtPoint.uncurry-image one 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheremax-right-zero
Derivation, checked
max-right-zero : (max ∘ insert zero) =₁ id ([1] {Γ = Γ})
Proof / implementation
max-right-zero = s₀-d₀ ∙ (AtPoint.uncurry-image zero 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheremax-right-one
Derivation, checked
max-right-one : (max ∘ insert one) =₁ const (one {Γ = Γ})
Proof / implementation
max-right-one = s₁-d₀ ∙ (AtPoint.uncurry-image one 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheremin-left-zero
Derivation, checked
min-left-zero : (min ∘ pair (const zero) (id [1])) =₁ const (zero {Γ = Γ})
Proof / implementation
min-left-zero = row-from-point d₂ zero (const zero) d₂-zero
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheremin-left-one
Derivation, checked
min-left-one : (min ∘ pair (const one) (id [1])) =₁ id ([1] {Γ = Γ})
Proof / implementation
min-left-one = row-from-point d₂ one (id [1]) d₂-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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheremax-left-zero
Derivation, checked
max-left-zero : (max ∘ pair (const zero) (id [1])) =₁ id ([1] {Γ = Γ})
Proof / implementation
max-left-zero = row-from-point d₀ zero (id [1]) d₀-zero
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheremax-left-one
Derivation, checked
max-left-one : (max ∘ pair (const one) (id [1])) =₁ const (one {Γ = Γ})
Proof / implementation
max-left-one = row-from-point d₀ one (const one) d₀-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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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 the sense that the following diagrams commute:
Proof
Proof. The identifications \(\min (x,0) = 0\), \(\min (x,1) = x\), \(\max (x,0) = x\) and \(\max (x,1) = 1\) are immediate from the two pullback squares stated before the lemma. For the other four relations we use that \(q_0^{-1}\colon [1] \iso [1]_{0/}\) sends \(0\) to \(\id _0\colon 0 \to 0\) and \(1\) to \(\can \colon 0 \to 1\), while \(p_1^{-1}\colon [1] \iso [1]_{/1}\) sends \(0\) to \(\can \colon 0 \to 1\) and \(1\) to \(\id _1\colon 1 \to 1\). □
2.1.1 Commutative triangles
Apart from the poset \([1] = \{0 \leq 1\}\), which classifies morphisms, there should also be a poset \([2] = \{\overline {0} \leq \overline {1} \leq \overline {2}\}\) classifying commutative triangles.
Definition 2.1.13 (Walking commutative triangle). We define the walking commutative triangle as \[ [2] \quad := \quad \Ar ([1]) \quad = \quad \Fun ([1],[1]). \] We define objects \(\overline {0}, \overline {1},\overline {2}: [2]\) by: \[ \overline {0} := \id _0, \qquad \overline {1} := \can , \qquad \overline {2} := \id _1, \] where \(\can \colon [1] \to [1]\) is the identity of \([1]\), regarded as a morphism \(\can \colon 0 \to 1\) in \([1]\).
Agda The walking commutative triangle
[2]
Definition, checked
[2] : 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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wherevertex₀
Definition, checked
vertex₀ vertex₁ vertex₂ : MAP One [2]
Proof / implementation
vertex₀ = funName (const zero) vertex₁ = funName (id [1]) vertex₂ = funName (const 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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wherevertex₁
Definition, checked
vertex₀ vertex₁ vertex₂ : MAP One [2]
Proof / implementation
vertex₀ = funName (const zero) vertex₁ = funName (id [1]) vertex₂ = funName (const 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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wherevertex₂
Definition, checked
vertex₀ vertex₁ vertex₂ : MAP One [2]
Proof / implementation
vertex₀ = funName (const zero) vertex₁ = funName (id [1]) vertex₂ = funName (const 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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereAbout this correspondence
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 walking triangle
[2]
Definition, checked
[2] : 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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereAbout this correspondence
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 three vertices
vertex₀
Definition, checked
vertex₀ vertex₁ vertex₂ : MAP One [2]
Proof / implementation
vertex₀ = funName (const zero) vertex₁ = funName (id [1]) vertex₂ = funName (const 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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wherevertex₁
Definition, checked
vertex₀ vertex₁ vertex₂ : MAP One [2]
Proof / implementation
vertex₀ = funName (const zero) vertex₁ = funName (id [1]) vertex₂ = funName (const 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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wherevertex₂
Definition, checked
vertex₀ vertex₁ vertex₂ : MAP One [2]
Proof / implementation
vertex₀ = funName (const zero) vertex₁ = funName (id [1]) vertex₂ = funName (const 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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereAbout this correspondence
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.
Construction 2.1.14. We construct three face maps \(d_i\colon [1] \to [2]\) for \(i =0,1,2\):
Agda Faces and degeneracies
d₀
Definition, checked
d₂ d₀ : MAP ([1] {Γ = Γ}) [2]
Proof / implementation
d₂ = MorphismFamily.arrow minimum d₀ = MorphismFamily.arrow maximum
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whered₁
Definition, checked
d₁ : MAP [1] [2]
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whered₂
Definition, checked
d₂ d₀ : MAP ([1] {Γ = Γ}) [2]
Proof / implementation
d₂ = MorphismFamily.arrow minimum d₀ = MorphismFamily.arrow maximum
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wheres₀
Definition, checked
s₀ s₁ : MAP [2] [1]
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wheres₁
Definition, checked
s₀ s₁ : MAP [2] [1]
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereAbout this correspondence
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 set \(d_0 := \overline {\max }\colon [1] \to \Fun ([1],[1])\);
- We set \(d_1 := p_{[1]}^*\colon [1] \to \Fun ([1],[1])\);
- We set \(d_2 := \overline {\min }\colon [1] \to \Fun ([1],[1])\).
Agda The zeroth face
d₀
Definition, checked
d₂ d₀ : MAP ([1] {Γ = Γ}) [2]
Proof / implementation
d₂ = MorphismFamily.arrow minimum d₀ = MorphismFamily.arrow maximum
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereAbout this correspondence
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 middle face
d₁
Definition, checked
d₁ : MAP [1] [2]
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereAbout this correspondence
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 second face
d₂
Definition, checked
d₂ d₀ : MAP ([1] {Γ = Γ}) [2]
Proof / implementation
d₂ = MorphismFamily.arrow minimum d₀ = MorphismFamily.arrow maximum
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereAbout this correspondence
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 also construct two degeneracy maps \(s_i\colon [2] \to [1]\) for \(i=0,1\):
- We set \(s_0 := \ev _0\colon \Fun ([1],[1]) \to [1]\);
- We set \(s_1 := \ev _1\colon \Fun ([1],[1]) \to [1]\).
Agda The zeroth degeneracy
s₀
Definition, checked
s₀ s₁ : MAP [2] [1]
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereAbout this correspondence
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 first degeneracy
s₁
Definition, checked
s₀ s₁ : MAP [2] [1]
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereAbout this correspondence
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 2.1.15. It will sometimes be useful to denote the terminal category by \([0]\), and to denote the maps \(0: * \to [1]\) and \(1: * \to [1]\) by \(d_1\colon [0] \to [1]\) and \(d_0\colon [0] \to [1]\), respectively. We will visualize the three categories \([0]\), \([1]\) and \([2]\) as follows:
Agda The terminal category as the zero simplex
One
Assumption, 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} whereAbout this correspondence
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 five face maps \(d_0,d_1\colon [0] \to [1]\) and \(d_0,d_1,d_2\colon [1] \to [2]\) and the relations between them may be displayed as follows:
The two degeneracy maps \(s_0,s_1\colon [2] \to [1]\) may be interpreted as the following ‘projections’:
Let us establish some of the relations implicit in this figure.
Lemma 2.1.16 (Simplicial identities). There are vertex identifications \[ \begin {aligned} d_2(0) &= \overline {0} = d_1(0),\qquad & d_2(1) &= \overline {1} = d_0(0),\qquad & d_0(1) &= \overline {2} = d_1(1), \\ s_0(\overline {0}) &= 0 = s_0(\overline {1}), \qquad & s_0(\overline {2}) = &1, \quad s_1(\overline {0}) = 0, \qquad & s_1(\overline {1}) &= 1 = s_1(\overline {2}). \end {aligned} \] There are identifications of morphisms \[ \begin {aligned} s_0d_0& = \id _{[1]},\quad & s_0d_1& = \id _{[1]},\quad & s_0d_2& = \const _0,\\ s_1d_0& = \const _1,\quad & s_1d_1& = \id _{[1]},\quad& s_1d_2& = \id _{[1]}. \end {aligned} \] These identifications may be chosen so that the morphism identifications are compatible with the vertex identifications.
Agda Simplicial identities and vertex compatibility
face-top
Derivation, checked
face-top : (d₀ ∘ (one {Γ = Γ})) =₁ (d₁ ∘ one)
Proof / implementation
face-top = TopVertex.value
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereface-middle
Derivation, checked
face-middle : (d₀ ∘ (zero {Γ = Γ})) =₁ (d₂ ∘ one)
Proof / implementation
face-middle = MiddleVertex.value
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} whereface-bottom
Derivation, checked
face-bottom : (d₁ ∘ (zero {Γ = Γ})) =₁ (d₂ ∘ zero)
Proof / implementation
face-bottom = BottomVertex.value
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wheres₀-d₀
Derivation, checked
s₀-d₀ : (s₀ ∘ d₀) =₁ id ([1] {Γ = Γ})
Proof / implementation
s₀-d₀ = MorphismFamily.source-frame maximum
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wheres₀-d₁
Derivation, checked
s₀-d₁ : (s₀ ∘ d₁) =₁ id ([1] {Γ = Γ})
Proof / implementation
s₀-d₁ = evAt-constant zero
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wheres₀-d₂
Derivation, checked
s₀-d₂ : (s₀ ∘ d₂) =₁ const (zero {Γ = Γ})
Proof / implementation
s₀-d₂ = MorphismFamily.source-frame minimum
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wheres₁-d₀
Derivation, checked
s₁-d₀ : (s₁ ∘ d₀) =₁ const (one {Γ = Γ})
Proof / implementation
s₁-d₀ = MorphismFamily.target-frame maximum
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wheres₁-d₁
Derivation, checked
s₁-d₁ : (s₁ ∘ d₁) =₁ id ([1] {Γ = Γ})
Proof / implementation
s₁-d₁ = evAt-constant 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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wheres₁-d₂
Derivation, checked
s₁-d₂ : (s₁ ∘ d₂) =₁ id ([1] {Γ = Γ})
Proof / implementation
s₁-d₂ = MorphismFamily.target-frame minimum
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} wheresource-compatible
Definition, checked
source-compatible : (MorphismFamily.source-frame after ∙ (ev₀ ◁ value)) =₂ MorphismFamily.source-frame before
Proof / implementation
source-compatible = unconstant-frame-compatible ev₀ _ _ value (MorphismFamilyIdentification.source-compatible comparison)
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} where
module MiddleVertex wheretarget-compatible
Definition, checked
target-compatible : (MorphismFamily.target-frame after ∙ (ev₁ ◁ value)) =₂ MorphismFamily.target-frame before
Proof / implementation
target-compatible = unconstant-frame-compatible ev₁ _ _ value (MorphismFamilyIdentification.target-compatible comparison)
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} where
module MiddleVertex wheresource-compatible
Definition, checked
source-compatible : (MorphismFamily.source-frame after ∙ (ev₀ ◁ value)) =₂ MorphismFamily.source-frame before
Proof / implementation
source-compatible = unconstant-frame-compatible ev₀ _ _ value (MorphismFamilyIdentification.source-compatible comparison)
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} where
module BottomVertex wheretarget-compatible
Definition, checked
target-compatible : (MorphismFamily.target-frame after ∙ (ev₁ ◁ value)) =₂ MorphismFamily.target-frame before
Proof / implementation
target-compatible = unconstant-frame-compatible ev₁ _ _ value (MorphismFamilyIdentification.target-compatible comparison)
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} where
module BottomVertex wheresource-compatible
Definition, checked
source-compatible : (MorphismFamily.source-frame after ∙ (ev₀ ◁ value)) =₂ MorphismFamily.source-frame before
Proof / implementation
source-compatible = unconstant-frame-compatible ev₀ _ _ value (MorphismFamilyIdentification.source-compatible comparison)
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} where
module TopVertex wheretarget-compatible
Definition, checked
target-compatible : (MorphismFamily.target-frame after ∙ (ev₁ ◁ value)) =₂ MorphismFamily.target-frame before
Proof / implementation
target-compatible = unconstant-frame-compatible ev₁ _ _ value (MorphismFamilyIdentification.target-compatible comparison)
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.Chapter02.Section01.WalkingTriangle where
module _ {Γ : Context} where
module TopVertex whereAbout this correspondence
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 last statement means that if we evaluate one of the six morphism identifications at one of the two vertices \(0\) and \(1\), the resulting identification agrees with the one obtained by combining the twelve vertex identifications. For example, in the case of evaluating \(s_0d_0 = \id _{[1]}\) at \(0\) it asserts that the following square of identifications commutes:
Proof
Proof. Recall that \(s_0\) and \(s_1\) are evaluation at the source and target. The defining pullback squares for \(d_2=\overline {\min }\) and \(d_0=\overline {\max }\) therefore give \[ s_0d_2 =\const _0,\qquad s_1d_2 =\id _{[1]},\qquad s_0d_0 = \id _{[1]},\qquad s_1d_0 = \const _1. \] The two remaining identifications follow from the definition of \(d_1\) as the constant-arrow functor.
The vertex identifications for \(s_0\) and \(s_1\) are the specified source and target identifications of \[ \overline 0=\id _0,\qquad \overline 1=\can ,\qquad \overline 2=\id _1. \] At the vertices, these constructions give identifications \[ \begin {aligned} d_2(0)& = \overline 0 = d_1(0),\\ d_2(1)& = \overline 1 = d_0(0),\\ d_0(1)& = \overline 2 = d_1(1). \end {aligned} \] We choose them with the source and target comparisons just specified. This is possible because the categories of morphisms \(0\to 0\), \(0\to 1\), and \(1\to 1\) in \([1]\) are contractible, by initiality of \(0\) and terminality of \(1\).
Each of these six vertex comparisons is chosen with its specified source and target identifications. Applying \(s_0\) or \(s_1\) therefore gives the corresponding commuting square of identifications, as required. □
Definition 2.1.17 (Commutative triangle). Given a category \(C\), we define a commutative triangle in \(C\) to be a functor \([2] \to C\). We define the category of commutative triangles in \(C\) as \[ \Triang (C) \quad := \quad \Fun ([2],C). \] The three functors \(d_0,d_1,d_2\colon [1] \to [2]\) induce three restriction functors \[ d^*_0, d^*_1, d^*_2\colon \Triang (C) \to \Ar (C). \]
Agda Commutative triangles
Triangle
Definition, checked
Triangle : 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereTriangles
Definition, checked
Triangles : 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereedge₀
Definition, checked
edge₀ edge₁ edge₂ : {C : CAT Γ} → MAP (Triangles C) (Ar 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereedge₁
Definition, checked
edge₀ edge₁ edge₂ : {C : CAT Γ} → MAP (Triangles C) (Ar 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereedge₂
Definition, checked
edge₀ edge₁ edge₂ : {C : CAT Γ} → MAP (Triangles C) (Ar 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereAbout this correspondence
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 triangle as a diagram
Triangle
Definition, checked
Triangle : 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereAbout this correspondence
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 frequently denote commutative triangles by
where \(f = d^*_2(\sigma )\), \(g = d^*_0(\sigma )\) and \(h = d^*_1(\sigma )\). We use the identifications of Lemma 2.1.16 whenever we restrict a triangle to its edges and vertices. Thus the three edges have specified common vertices, and the simplicial identities respect those identifications. For families of triangles, these comparisons are obtained by uncurrying and restricting the evaluation functor; compatibility follows by applying evaluation to the comparisons above. We will often leave commutative triangles unnamed, and only label their three edges. We may sometimes denote in the same manner triples of morphisms \((f,g,h)\) that do not (or not necessarily) come from a commutative triangle, which will then be mentioned explicitly.
Agda The three edges of a triangle
edge₂
Definition, checked
edge₀ edge₁ edge₂ : {C : CAT Γ} → MAP (Triangles C) (Ar 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereedge₀
Definition, checked
edge₀ edge₁ edge₂ : {C : CAT Γ} → MAP (Triangles C) (Ar 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereedge₁
Definition, checked
edge₀ edge₁ edge₂ : {C : CAT Γ} → MAP (Triangles C) (Ar 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereAbout this correspondence
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 2.1.18. Given morphisms \(f\colon x \to y\) and \(g\colon y \to z\) in \(C\), a composite of \(f\) and \(g\) is a morphism \(h\colon x \to z\) that comes equipped with a commutative triangle \(\sigma \) of the above form:
Agda The category of composites
Composites
Definition, checked
Composites : {P C : CAT Γ} → MAP P (Composable C) → 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereComposable
Definition, checked
Composable : 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereshort-edges
Definition, checked
short-edges : (C : CAT Γ) → MAP (Triangles C) (Composable C)
Proof / implementation
short-edges C = pullback-factor (triangle-cone 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereAbout this correspondence
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 composite with its witnessing triangle
TrianglePresentation
Definition, checked
TrianglePresentation : {P C : CAT Γ} {f g h : MAP P C} (alpha : MorphismFamily f g) (beta : MorphismFamily g h) (gamma : MorphismFamily f h) → Set m
Proof / implementation
TrianglePresentation {P} {C} alpha beta gamma = Data.Σ (MAP P (Triangles C)) λ triangle → Data.Σ ((edge₂ {C = C} ∘ triangle) =₁ MorphismFamily.arrow alpha) λ first → Data.Σ ((edge₀ {C = C} ∘ triangle) =₁ MorphismFamily.arrow beta) λ second → Data.Σ ((edge₁ {C = C} ∘ triangle) =₁ MorphismFamily.arrow gamma) λ long → Data.Σ (MiddleCorner alpha beta triangle first second) λ _ → Data.Σ (SourceCorner alpha gamma triangle long first) λ _ → TargetCorner beta gamma triangle long 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.Chapter02.Section02.FramedTrianglePresentations where
module _ {Γ : Context} whereAbout this correspondence
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 define the category of composites \(\Comp _{f,g}(C)\) as the following pullback:
Agda The category of composites
Composites
Definition, checked
Composites : {P C : CAT Γ} → MAP P (Composable C) → 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereAbout this correspondence
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 Restriction to a composable pair
short-edges
Definition, checked
short-edges : (C : CAT Γ) → MAP (Triangles C) (Composable C)
Proof / implementation
short-edges C = pullback-factor (triangle-cone 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} wheretriangle-cone
Definition, checked
triangle-cone : (C : CAT Γ) → Cone (ev₁ {C = C}) ev₀ (Triangles C)
Proof / implementation
triangle-cone C = record { left = edge₂; right = edge₀ ; match = (evAt-pre zero d₀) ⁻¹ ∙ (evAt-cong (face-middle ⁻¹) ∙ evAt-pre one 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.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereAbout this correspondence
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.
Example 2.1.19. The two functors \(s_0,s_1\colon [2] \to [1]\) induce functors \[ s_0^*,s_1^*\colon \Ar (C) \to \Triang (C), \] so that every morphism \(f\colon x \to y\) in \(C\) gives rise to two commutative diagrams \(s_0^*(f)\) and \(s_1^*(f)\) in \(C\). As a consequence of the simplicial identities from Lemma 2.1.16, these commutative triangles have the following form:
Agda Composites with an identity
source
Definition, checked
source : TrianglePresentation (identity-family (ev₀ {C = C})) U.universal-arrow U.universal-arrow
Proof / implementation
source = triangle-presentation S.Source.triangle U.Source.First.comparison U.Source.Second.comparison U.Source.Long.comparison V.Source.MiddleVertex.vertex-equation V.Source.SourceVertex.vertex-equation V.Source.TargetVertex.vertex-equation
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.Chapter02.Section02.MorphismCompositionUnits where
module UniversalUnitPresentations {Γ : Context} (C : CAT Γ) wheretarget
Definition, checked
target : TrianglePresentation U.universal-arrow (identity-family (ev₁ {C = C})) U.universal-arrow
Proof / implementation
target = triangle-presentation S.Target.triangle U.Target.First.comparison U.Target.Second.comparison U.Target.Long.comparison V.Target.MiddleVertex.vertex-equation V.Target.SourceVertex.vertex-equation V.Target.TargetVertex.vertex-equation
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.Chapter02.Section02.MorphismCompositionUnits where
module UniversalUnitPresentations {Γ : Context} (C : CAT Γ) whereAbout this correspondence
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, these triangles exhibit \(f\) as a composite of \(\id _x\) and \(f\), as well as a composite of \(f\) and \(\id _y\).
2.1.2 Commutative squares
Throughout, \(C\) denotes a category.
Definition 2.1.20 (Commutative square). We define a commutative square in \(C\) to be a functor \([1] \times [1] \to C\). We define the category of commutative squares in \(C\) as \[ \Sq (C) \quad := \quad \Fun ([1] \times [1],C). \] We will often display commutative squares as follows:
Agda Commutative squares
Squares
Definition, checked
Squares : 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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 square as a diagram
Squares
Definition, checked
Squares : 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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 ordinary category theory, a commutative square consists of morphisms \(f\), \(g\), \(h\) and \(k\) as above that satisfy the condition that \(h \circ f = k \circ g\). We will now formulate a synthetic analogue of this.
Definition 2.1.21. We define two functors \(j_0,j_1\colon [2] \to [1] \times [1]\) as \[ j_0 := (s_0,s_1) \qquadtext { and } j_1 := (s_1,s_0). \] These two commutative triangles in \([1] \times [1]\) may be visualized as follows:
Agda The two triangles in a square
j₀
Definition, checked
j₀ j₁ : MAP ([2] {Γ = Γ}) ([1] × [1])
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherej₁
Definition, checked
j₀ j₁ : MAP ([2] {Γ = Γ}) ([1] × [1])
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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 triangle inclusions
j₀
Definition, checked
j₀ j₁ : MAP ([2] {Γ = Γ}) ([1] × [1])
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherej₁
Definition, checked
j₀ j₁ : MAP ([2] {Γ = Γ}) ([1] × [1])
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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 simplicial relations \(s_0 \circ d_1 = \id _{[1]} = s_1 \circ d_1\) provide an identification making the following square commute:
Agda The specified common diagonal
gluing-square
Definition, checked
gluing-square : Square (d₁ {Γ = Γ}) j₀
Proof / implementation
gluing-square = record { source-map = d₁; target-map = j₁ ; cell = j₁-diagonal ⁻¹ ∙ j₀-diagonal }
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherej₀-diagonal
Derivation, checked
j₀-diagonal : (j₀ ∘ (d₁ {Γ = Γ})) =₁ diagonal
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherej₁-diagonal
Derivation, checked
j₁-diagonal : (j₁ ∘ (d₁ {Γ = Γ})) =₁ diagonal
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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.
Axiom D (Commutative square axiom). The commutative square (2.1) is a pushout square: For every category \(C\), the commutative square
Agda The commutative square axiom
square-isPushout
Assumption, type checked
square-isPushout : IsPushout gluing-square
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheresquare-functor-pullback
Derivation, checked
square-functor-pullback : (C : CAT Γ) → IsPullback (square-cone C)
Proof / implementation
square-functor-pullback = pushout→functor-criterion gluing-square square-isPushout
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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.
is a pullback square.
Construction 2.1.22. In a common categorical context \(\Gamma \), consider terms \(\Gamma \vdash \sigma ,\tau :\Triang (C)\) equipped with an identification \(\Gamma \vdash \varphi \colon d_1^*(\sigma )= d_1^*(\tau )\). By Axiom D, these determine a term \[ \Gamma \vdash \square (\sigma ,\tau ,\varphi ):\Sq (C) \] with specified identifications \(\sigma = j_0^*(\square (\sigma ,\tau ,\varphi ))\) and \(\tau = j_1^*(\square (\sigma ,\tau ,\varphi ))\). In the absolute case it is the commutative square
Agda Gluing two triangles
glue
Definition, checked
glue : Cocone (d₁ {Γ = Γ}) d₁ C → MAP ([1] × [1]) C
Proof / implementation
glue = Chosen.value
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} where
module Absolute (C : CAT Γ) whereglue-β
Derivation, checked
glue-β : (t : Cocone (d₁ {Γ = Γ}) d₁ C) → CoconeIdentification₁ (cocone-postcompose (glue t) (square-cocone gluing-square)) t
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} where
module Absolute (C : CAT Γ) whereglue
Definition, checked
glue : {P : CAT Γ} → Cone (funPre {D = C} d₁) (funPre d₁) P → MAP P (Squares C)
Proof / implementation
glue = Universal.factor
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} where
module Families (C : CAT Γ) whereglue-β
Derivation, checked
glue-β : {P : CAT Γ} (t : Cone (funPre {D = C} d₁) (funPre d₁) P) → ConeIdentification₁ (cone-restrict (glue t) (square-cone C)) t
Proof / implementation
glue-β = Universal.β
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} where
module Families (C : CAT Γ) whereglue-left
Derivation, checked
glue-left : {C : CAT Γ} (t : Cocone (d₁ {Γ = Γ}) d₁ C) → (Absolute.glue C t ∘ pair (const zero) (id [1])) =₁ (Cocone.left t ∘ d₂)
Proof / implementation
glue-left {C} t = (CoconeIdentification₁.left (Absolute.glue-β C t) ▷ d₂) ∙ ((comp-assoc d₂ j₀ (Absolute.glue C t)) ⁻¹ ∙ (Absolute.glue C t ◁ j₀-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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereglue-right
Derivation, checked
glue-right : {C : CAT Γ} (t : Cocone (d₁ {Γ = Γ}) d₁ C) → (Absolute.glue C t ∘ pair (const one) (id [1])) =₁ (Cocone.right t ∘ d₀)
Proof / implementation
glue-right {C} t = (CoconeIdentification₁.right (Absolute.glue-β C t) ▷ d₀) ∙ ((comp-assoc d₀ j₁ (Absolute.glue C t)) ⁻¹ ∙ (Absolute.glue C t ◁ j₁-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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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 Leaving the gluing comparison implicit
glue
Definition, checked
glue : Cocone (d₁ {Γ = Γ}) d₁ C → MAP ([1] × [1]) C
Proof / implementation
glue = Chosen.value
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} where
module Absolute (C : CAT Γ) whereglue-β
Derivation, checked
glue-β : (t : Cocone (d₁ {Γ = Γ}) d₁ C) → CoconeIdentification₁ (cocone-postcompose (glue t) (square-cocone gluing-square)) t
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} where
module Absolute (C : CAT Γ) whereAbout this correspondence
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.
Construction 2.1.23. We construct functors \(p_0,p_2\colon [1] \times [1] \to [2]\), pictorially represented by the following diagrams:
Agda The two square retractions
p₀
Definition, checked
p₀ p₂ : MAP ([1] × [1]) ([2] {Γ = Γ})
Proof / implementation
p₀ = Absolute.glue [2] lower-cocone p₂ = Absolute.glue [2] upper-cocone
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherep₂
Definition, checked
p₀ p₂ : MAP ([1] × [1]) ([2] {Γ = Γ})
Proof / implementation
p₀ = Absolute.glue [2] lower-cocone p₂ = Absolute.glue [2] upper-cocone
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherelower-cocone
Definition, checked
lower-cocone upper-cocone : Cocone (d₁ {Γ = Γ}) d₁ [2]
Proof / implementation
lower-cocone = record { left = id [2]; right = d₁ ∘ s₀; match = collapse-matching s₀ s₀-d₁ } upper-cocone = record { left = d₁ ∘ s₁; right = id [2]; match = (collapse-matching s₁ s₁-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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereupper-cocone
Definition, checked
lower-cocone upper-cocone : Cocone (d₁ {Γ = Γ}) d₁ [2]
Proof / implementation
lower-cocone = record { left = id [2]; right = d₁ ∘ s₀; match = collapse-matching s₀ s₀-d₁ } upper-cocone = record { left = d₁ ∘ s₁; right = id [2]; match = (collapse-matching s₁ s₁-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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherep₀-j₀
Derivation, checked
p₀-j₀ : (p₀ ∘ j₀) =₁ id [2]
Proof / implementation
p₀-j₀ = CoconeIdentification₁.left p₀-β
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherep₀-j₁
Derivation, checked
p₀-j₁ : (p₀ ∘ j₁) =₁ d₁ ∘ s₀
Proof / implementation
p₀-j₁ = CoconeIdentification₁.right p₀-β
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherep₂-j₀
Derivation, checked
p₂-j₀ : (p₂ ∘ j₀) =₁ d₁ ∘ s₁
Proof / implementation
p₂-j₀ = CoconeIdentification₁.left p₂-β
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherep₂-j₁
Derivation, checked
p₂-j₁ : (p₂ ∘ j₁) =₁ id [2]
Proof / implementation
p₂-j₁ = CoconeIdentification₁.right p₂-β
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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.
More precisely, \(p_0 := \square (\id _{[2]}, d_1s_0)\) is the commutative square determined by the two commutative triangles \(\sigma = \id _{[2]}\) and \(\tau = d_1 \circ s_0\), with identification \[ d_1^*(\sigma ) = \id _{[2]} \circ d_1 = d_1 = d_1 \circ \id _{[1]} = d_1 \circ s_0 \circ d_1 = d_1^*(\tau ). \] Similarly, \(p_2 := \square (d_1s_1, \id _{[2]})\) is the square determined by \(\sigma = d_1 \circ s_1\) and \(\tau = \id _{[2]}\), with analogous identification between \(d_1^*(\sigma )\) and \(d_1^*(\tau )\).
Agda The lower square retraction
p₀
Definition, checked
p₀ p₂ : MAP ([1] × [1]) ([2] {Γ = Γ})
Proof / implementation
p₀ = Absolute.glue [2] lower-cocone p₂ = Absolute.glue [2] upper-cocone
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherelower-cocone
Definition, checked
lower-cocone upper-cocone : Cocone (d₁ {Γ = Γ}) d₁ [2]
Proof / implementation
lower-cocone = record { left = id [2]; right = d₁ ∘ s₀; match = collapse-matching s₀ s₀-d₁ } upper-cocone = record { left = d₁ ∘ s₁; right = id [2]; match = (collapse-matching s₁ s₁-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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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 upper square retraction
p₂
Definition, checked
p₀ p₂ : MAP ([1] × [1]) ([2] {Γ = Γ})
Proof / implementation
p₀ = Absolute.glue [2] lower-cocone p₂ = Absolute.glue [2] upper-cocone
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereupper-cocone
Definition, checked
lower-cocone upper-cocone : Cocone (d₁ {Γ = Γ}) d₁ [2]
Proof / implementation
lower-cocone = record { left = id [2]; right = d₁ ∘ s₀; match = collapse-matching s₀ s₀-d₁ } upper-cocone = record { left = d₁ ∘ s₁; right = id [2]; match = (collapse-matching s₁ s₁-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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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.
By construction these two maps satisfy the following two relations: \[ p_0 \circ j_0 = \id _{[2]}, \qquad p_0 \circ j_1 = d_1 \circ s_0, \qquad p_2 \circ j_0 = d_1 \circ s_1, \qquad p_2 \circ j_1 = \id _{[2]}. \]
Lemma 2.1.24. We have the relations \[ \square (s_0,s_1) = \pr _1 \qquadtext { and } \square (s_1,s_0) = \pr _2 \] of functors \([1] \times [1] \to [1]\).
Agda Projections as glued squares
square-first-projection
Derivation, checked
square-first-projection : Absolute.glue [1] first-projection-cocone =₁ pr₁
Proof / implementation
square-first-projection = pair-β₂ pr₂ pr₁ ∙ ((exchanged ▷ swap) ∙ ((comp-assoc swap swap H) ⁻¹ ∙ ((H ◁ (swap-swap [1] [1]) ⁻¹) ∙ (comp-unitʳ H) ⁻¹))) where H : MAP ([1] × [1]) ([1] {Γ = Γ}) H = Absolute.glue [1] first-projection-cocone exchanged : (H ∘ swap) =₁ pr₂ exchanged = recognize-second-projection _ (s₀-d₂ ∙ (glue-left first-projection-cocone ∙ exchanged-row H zero)) (s₁-d₀ ∙ (glue-right first-projection-cocone ∙ exchanged-row H 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheresquare-second-projection
Derivation, checked
square-second-projection : Absolute.glue [1] second-projection-cocone =₁ pr₂
Proof / implementation
square-second-projection = recognize-second-projection _ (s₀-d₂ ∙ glue-bottom second-projection-cocone) (s₁-d₀ ∙ glue-top second-projection-cocone)
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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.
Proof
Proof. It suffices to observe that these two projection maps have the correct restrictions to the triangles \(j_0\) and \(j_1\). □
Lemma 2.1.25. We have \[ \max = \square (s_1,s_1) \qquadtext { and } \min = \square (s_0,s_0). \]
Agda Minimum and maximum as glued squares
square-minimum
Derivation, checked
square-minimum : Absolute.glue [1] minimum-cocone =₁ min
Proof / implementation
square-minimum = recognize-min _ (s₀-d₂ ∙ glue-bottom minimum-cocone) (s₀-d₀ ∙ glue-top minimum-cocone)
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheresquare-maximum
Derivation, checked
square-maximum : Absolute.glue [1] maximum-cocone =₁ max
Proof / implementation
square-maximum = recognize-max _ (s₁-d₂ ∙ glue-bottom maximum-cocone) (s₁-d₀ ∙ glue-top maximum-cocone)
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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.
Proof
Proof. It suffices to check that \(\max \) and \(\min \) restrict correctly along \(j_0\) and \(j_1\), and this follows directly by unwinding the definitions of \(\square (s_1,s_1)\) and \(\square (s_0,s_0)\) from Construction 2.1.22. □
Lemma 2.1.26. We have relations \begin {align*} j_0p_0(x,y) = (\min (x,y),y), &\qquad j_1p_0(x,y) = (y,\min (x,y)), \\ j_0p_2(x,y) = (y,\max (x,y)), &\qquad j_1p_2(x,y) = (\max (x,y),y). \end {align*}
Agda Coordinates of the square retractions
j₀-p₀
Derivation, checked
j₀-p₀ : (j₀ ∘ p₀) =₁ pair min 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherej₁-p₀
Derivation, checked
j₁-p₀ : (j₁ ∘ p₀) =₁ pair pr₂ min
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherej₀-p₂
Derivation, checked
j₀-p₂ : (j₀ ∘ p₂) =₁ pair pr₂ max
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wherej₁-p₂
Derivation, checked
j₁-p₂ : (j₁ ∘ p₂) =₁ pair max 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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheres₀-p₀
Derivation, checked
s₀-p₀ : (s₀ ∘ p₀) =₁ min
Proof / implementation
s₀-p₀ = recognize-min _ (s₀-d₂ ∙ ((collapse-coordinate s₀ s₀-d₁ s₀ ▷ d₂) ∙ coordinate-bottom s₀ lower-cocone)) (s₀-d₀ ∙ ((comp-unitʳ s₀ ▷ d₀) ∙ coordinate-top s₀ lower-cocone))
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheres₁-p₀
Derivation, checked
s₁-p₀ : (s₁ ∘ p₀) =₁ (pr₂ {C = [1] {Γ = Γ}} {D = [1]})
Proof / implementation
s₁-p₀ = recognize-second-projection _ (s₀-d₂ ∙ ((collapse-coordinate s₁ s₁-d₁ s₀ ▷ d₂) ∙ coordinate-bottom s₁ lower-cocone)) (s₁-d₀ ∙ ((comp-unitʳ s₁ ▷ d₀) ∙ coordinate-top s₁ lower-cocone))
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheres₀-p₂
Derivation, checked
s₀-p₂ : (s₀ ∘ p₂) =₁ (pr₂ {C = [1] {Γ = Γ}} {D = [1]})
Proof / implementation
s₀-p₂ = recognize-second-projection _ (s₀-d₂ ∙ ((comp-unitʳ s₀ ▷ d₂) ∙ coordinate-bottom s₀ upper-cocone)) (s₁-d₀ ∙ ((collapse-coordinate s₀ s₀-d₁ s₁ ▷ d₀) ∙ coordinate-top s₀ upper-cocone))
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} wheres₁-p₂
Derivation, checked
s₁-p₂ : (s₁ ∘ p₂) =₁ max
Proof / implementation
s₁-p₂ = recognize-max _ (s₁-d₂ ∙ ((comp-unitʳ s₁ ▷ d₂) ∙ coordinate-bottom s₁ upper-cocone)) (s₁-d₀ ∙ ((collapse-coordinate s₁ s₁-d₁ s₁ ▷ d₀) ∙ coordinate-top s₁ upper-cocone))
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.Chapter02.Section01.SquareGluing where
module _ {Γ : Context} whereAbout this correspondence
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.
Proof
Proof. Since \(p_0 := \square (\id _{[2]}, d_1s_0)\) and \(p_2 := \square (d_1s_1, \id _{[2]})\), we have \begin {align*} s_0p_0 &= \square (s_0, s_0d_1s_0) = \min , & s_1p_0 &= \square (s_1, s_1d_1s_0) = \square (s_1,s_0) = \pr _2 \\ s_0p_2 &= \square (s_0d_1s_1, s_0) = \square (s_1,s_0) = \pr _2, & s_1p_2&= \square (s_1d_1s_1, s_1) = \max , \end {align*}
where we used Lemma 2.1.24. Using \(j_0 = (s_0,s_1)\) and \(j_1 = (s_1,s_0)\) we get the desired four relations. □
Lemma 2.1.27. The map \(\lra {0,1,2}\colon * \sqcup * \sqcup * \to [2]^{\simeq }\) is an equivalence.
Agda The core of the walking triangle
triangleCore-isEquiv
Derivation, checked
triangleCore-isEquiv : IsEquiv (triangleCore)
Proof / implementation
triangleCore-isEquiv = record { inverse = triangleCore-inverse ; left-inverse-law = triangleCore-inverse-left ⁻¹ ; right-inverse-law = triangleCore-inverse-right ⁻¹ }
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.Chapter02.Section01.TriangleCore where
module _ {Γ : Context} whereAbout this correspondence
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.
Proof
Proof. Recall the functors \(j_0=(s_0,s_1)\colon [2]\to [1]\times [1]\) and \(p_0\colon [1]\times [1]\to [2]\) from Definition 2.1.21 and Construction 2.1.23. They satisfy \(p_0j_0=\id _{[2]}\). Choose an inverse to the preferred equivalence \[ \kappa :=(\pr _1^{\simeq },\pr _2^{\simeq })\colon ([1]\times [1])^{\simeq }\iso ([1]^{\simeq })^2 \] from Lemma 1.4.17, and put \(\bar j_0:=\kappa \circ j_0^{\simeq }\) and \(\bar p_0:=p_0^{\simeq }\circ \kappa ^{-1}\). Let \[ a\colon *\sqcup *\sqcup *\longrightarrow (*\sqcup *)^2 \] send \(0,1,2\) to \((0,0),(0,1),(1,1)\), respectively, and let \[ b\colon (*\sqcup *)^2\longrightarrow *\sqcup *\sqcup * \] send \((0,0),(0,1),(1,0),(1,1)\) to \(0,1,0,2\), respectively. Then \(b\circ a=\id \). The defining identifications for groupoid-core functoriality and the displayed descriptions of \(j_0\) and \(p_0\) show that the following squares commute:
The comparison for composition of groupoid-core functors, together with \(p_0j_0=\id _{[2]}\), gives \(\bar p_0\bar j_0=\id \). Thus this exhibits the map \[ \lra {0,1,2}\colon *\sqcup *\sqcup *\longrightarrow [2]^{\simeq } \] as a retract of \[ \lra {0,1}^2\colon (*\sqcup *)^2\longrightarrow ([1]^{\simeq })^2. \] The latter map is an equivalence because it is the product of the equivalence in Axiom C.1 with itself. The claim follows from closure of equivalences under retracts (Lemma 1.3.9). □
Lemma 2.1.28. For categories \(C\) and \(D\), the maps \(C^{\simeq } \to (C \sqcup D)^{\simeq }\) and \(D^{\simeq } \to (C \sqcup D)^{\simeq }\) induce an equivalence \(C^{\simeq } \sqcup D^{\simeq } \iso (C \sqcup D)^{\simeq }\).
Agda Cores preserve coproducts
coreCopair-isEquiv
Derivation, checked
coreCopair-isEquiv : (C D : CAT Γ) → IsEquiv (coreCopair C D)
Proof / implementation
coreCopair-isEquiv C D = CoproductCover.copair-isEquiv (mapPost {C = One} in₁) (mapPost {C = One} in₂) (mapPost {C = One} (coproductMap (terminate C) (terminate D))) (mapped-cone One (coproductSquare₁ (terminate C) (terminate D))) (mapped-cone One (coproductSquare₂ (terminate C) (terminate D))) (map-preserves-pullback One _ (inclusion₁-isPullback (terminate C) (terminate D))) (map-preserves-pullback One _ (inclusion₂-isPullback (terminate C) (terminate D))) two-point-copair-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.Chapter02.Section01.CoreCoproducts where
module _ {Γ : Context} whereAbout this correspondence
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.
Proof
Proof. Let \(i_0\colon * \to * \sqcup *\) and \(i_1\colon * \to * \sqcup *\) denote the inclusions of the first and second point, respectively. By combining Lemma 1.6.4 and Axiom B.5’, there are pullback squares
It remains to show that the two maps \(i_0^{\simeq }\) and \(i_1^{\simeq }\) induce an equivalence \[ q\colon (*)^{\simeq } \sqcup (*)^{\simeq } \longrightarrow (* \sqcup *)^{\simeq }. \] The defining identifications for groupoid-core functoriality give a commutative square
The left vertical functor is an equivalence by Proposition 1.4.15, and the right vertical functor is an equivalence by Proposition 1.4.15, since \(*\sqcup *\) is an anima. Hence \(q\) is an equivalence by 2-out-of-3. The two pullback squares above, descent for coproducts, and base change along \(q\) now identify \(C^{\simeq }\sqcup D^{\simeq }\) with \((C\sqcup D)^{\simeq }\). □
Remark 2.1.29. By Proposition 1.7.16 and Lemma 2.1.27, there are preferred equivalences \[ \Map ([1],[1]) \simeq \Fun ([1],[1])^{\simeq } \simeq [2]^{\simeq } \simeq * \sqcup * \sqcup *. \] We may think of these three points as picking out the three morphisms \(\id _0\colon 0 \to 0\), \(\id _1\colon 1 \to 1\) and \(\can \colon 0 \to 1\) of \([1]\). In particular, we see that \([1]\) only has three morphisms.
Agda The three interval endomorphisms
intervalEndomorphisms-isEquiv
Derivation, checked
intervalEndomorphisms-isEquiv : IsEquiv {Γ = Γ} intervalEndomorphisms
Proof / implementation
intervalEndomorphisms-isEquiv = equiv-transport intervalEndomorphisms-image (equiv-compose triangleCore (coreFunUncurrying [1] [1]) triangleCore-isEquiv (coreFunUncurrying-isEquiv [1] [1]))
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.Chapter02.Section01.TriangleCore where
module _ {Γ : Context} whereAbout this correspondence
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.
Supplementary notes
- Arrows with specified endpoints AI-generated