Chapter 1 code: rebuild2 edition, checked 14 October 2026. Included modules and omissions.
Read the Agda code alongside the book.Click dotted-underlined prose to read its Agda code alongside the book. Browse all code.
1.6 Pullbacks of categories
We will now axiomatize the pullback of two functors \(f\colon C \to E\) and \(g\colon D \to E\) of categories. This will be similar to the axiom for the product \(C \times D\), but it is more involved due to the fact that we need to record compatibilities with the structure maps to \(E\).
Definition 1.6.1. Consider two functors \(f\colon C \to E\) and \(g\colon D \to E\). Given a category \(T\), we define a cone diagram on \(T\) to be a triple \(c = (t_C,t_D,\tau )\) consisting of functors \(t_C\colon T \to C\) and \(t_D\colon T \to D\) together with an identification \(\tau \colon f \circ t_C = g \circ t_D\). In other words, a cone diagram consists of a commutative square of the form
Agda A cone diagram
Cone
Definition, checked
record Cone {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) (T : CAT Γ) : Set m where field left : MAP T C right : MAP T D match : (f ∘ left) =₁ (g ∘ 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.Chapter01.Section06.Cones where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The two legs of a cone
left
Definition, checked
left : MAP T C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Cones where
module _ {Γ : Context} where
record Cone {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) (T : CAT Γ) : Set m whereright
Definition, checked
right : MAP T D
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Cones where
module _ {Γ : Context} where
record Cone {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) (T : CAT Γ) : Set m whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The matching isomorphism
match
Definition, checked
match : (f ∘ left) =₁ (g ∘ 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.Chapter01.Section06.Cones where
module _ {Γ : Context} where
record Cone {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) (T : CAT Γ) : Set m whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
We call \(T\) the cone point of the diagram. Given another cone diagram \(c' = (t'_C,t'_D,\tau ')\), an identification of cone diagrams \(c = c'\) is a triple \(\Phi \colon (\varphi _C,\varphi _D,H)\), where \(\varphi _C\colon t_C = t'_C\) and \(\varphi _D\colon t_D = t'_D\) are identifications, and \(H\) is an identification \[ \tau '\circ (f\star \varphi _C)=(g\star \varphi _D)\circ \tau . \] In particular, a comparison of cones needs to be compatible with the identifications forming the commutative square. In turn, if \(\Psi \colon (\psi _C,\psi _D,G)\) is another identification of cone diagrams \(c = c'\), we say that \(\Phi \) and \(\Psi \) are identified if there are identifications \(\varphi _C = \psi _C\) and \(\varphi _D = \psi _D\) under which \(H\) becomes identified with \(G\).
Agda An isomorphism of cone diagrams
ConeIdentification
Definition, checked
record ConeIdentification (X : CAT Γ) {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} (s t : Cone f g T) : Set m where open Terms.Equalities X using (_＝_) field left : Cone.left s ＝ Cone.left t right : Cone.right s ＝ Cone.right t compatible : SquareCell₌ (f ◁ left) (g ◁ right) (const (Cone.match s)) (const (Cone.match 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.Chapter01.Section06.Cones where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The two leg comparisons
left
Definition, checked
left : Cone.left s ＝ Cone.left 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.Chapter01.Section06.Cones where
module _ {Γ : Context} where
record ConeIdentification (X : CAT Γ) {C D E T : CAT Γ}
{f : MAP C E} {g : MAP D E} (s t : Cone f g T) : Set m whereright
Definition, checked
right : Cone.right s ＝ Cone.right 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.Chapter01.Section06.Cones where
module _ {Γ : Context} where
record ConeIdentification (X : CAT Γ) {C D E T : CAT Γ}
{f : MAP C E} {g : MAP D E} (s t : Cone f g T) : Set m whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Compatibility with the matching
compatible
Definition, checked
compatible : SquareCell₌ (f ◁ left) (g ◁ right) (const (Cone.match s)) (const (Cone.match 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.Chapter01.Section06.Cones where
module _ {Γ : Context} where
record ConeIdentification (X : CAT Γ) {C D E T : CAT Γ}
{f : MAP C E} {g : MAP D E} (s t : Cone f g T) : Set m whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Identifying cone comparisons
ConeIdentificationEquality
Definition, checked
record ConeIdentificationEquality {X C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} {s t : Cone f g T} (Φ Ψ : ConeIdentification X s t) : Set m where field left : ConeIdentification.left Φ =₁ ConeIdentification.left Ψ right : ConeIdentification.right Φ =₁ ConeIdentification.right Ψ left-boundary : (const (Cone.match t) ∙ (f ◁ ConeIdentification.left Φ)) =₁ (const (Cone.match t) ∙ (f ◁ ConeIdentification.left Ψ)) left-boundary = comp₌-cong (id₌ (const (Cone.match t))) (postWhisker f ◁ left) right-boundary : ((g ◁ ConeIdentification.right Φ) ∙ const (Cone.match s)) =₁ ((g ◁ ConeIdentification.right Ψ) ∙ const (Cone.match s)) right-boundary = comp₌-cong (postWhisker g ◁ right) (id₌ (const (Cone.match s))) field compatible : (ConeIdentification.compatible Ψ ∙ left-boundary) =₂ (right-boundary ∙ ConeIdentification.compatible Φ)
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.Section06.Cones where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Given a functor \(s\colon S \to T\) and a cone diagram \(c = (t_C,t_D,\tau )\) on \(T\) we obtain another cone diagram \(s^*(c) := (t_C \circ s, t_D \circ s, \tau \ast \id _s)\) on \(S\). Similarly, every identification \(s_1 = s_2\) of functors \(S \to T\) induces an identification \(s^*_1(c) = s^*_2(c)\) of cone diagrams.
Agda Restricting a cone
cone-restrict
Definition, checked
cone-restrict : {C D E S T : CAT Γ} {f : MAP C E} {g : MAP D E} → MAP S T → Cone f g T → Cone f g S
Proof / implementation
cone-restrict {f = f} {g} r s = record { left = Cone.left s ∘ r ; right = Cone.right s ∘ r ; match = comp-assoc r (Cone.right s) g ∙ ((Cone.match s ▷ r) ∙ (comp-assoc r (Cone.left s) f) ⁻¹) }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Cones where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda A identification induces a cone comparison
cone-action
Derivation, checked
cone-action : {C D E S T : CAT Γ} {f : MAP C E} {g : MAP D E} (s : Cone f g T) {h k : MAP S T} → h ＝ k → ConeIdentification X (cone-restrict h s) (cone-restrict k s)
Proof / implementation
cone-action s {h} {k} δ = ConeAction.Boundary.decode s h k (cone-restrict δ (ConeAction.identification-cone s h k))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.ConeIdentifications where
module _ {Γ : Context} where
module _ {X : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Axiom B.6 (Pullback of categories). For functors \(f\colon C\to E\) and \(g\colon D\to E\), there is a category \(C\times _E D\), called their pullback or fiber product, with projections \(\pr _1\colon C\times _E D\to C\) and \(\pr _2\colon C\times _E D\to D\), and an identification \(\tau _{\univ }\colon f\pr _1= g\pr _2\). Given \(a\colon T\to C\), \(b\colon T\to D\) and \(\tau \colon fa= gb\), there is a functor \((a,b)_\tau \colon T\to C\times _E D\) equipped with projection comparisons \(c\colon \pr _1(a,b)_\tau = a\) and \(d\colon \pr _2(a,b)_\tau = b\) and an identification \[ \tau \circ (f\star c)= (g\star d)\circ (\tau _{\univ }\star (a,b)_\tau ). \] If \(C,D,E\) are animae, then \(C\times _E D\) is an anima.
Agda The chosen pullback category
Pullback
Assumption, type checked
Pullback : {C D E : CAT Γ} → MAP C E → MAP D E → 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.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The pullback projections
pullback₁
Definition, checked
pullback₁ : {C D E : CAT Γ} {f : MAP C E} {g : MAP D E} → MAP (Pullback f g) C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Pullbacks where
module _ {Γ : Context} wherepullback₂
Definition, checked
pullback₂ : {C D E : CAT Γ} {f : MAP C E} {g : MAP D E} → MAP (Pullback f g) D
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The universal matching
pullback-match
Definition, checked
pullback-match : {C D E : CAT Γ} {f : MAP C E} {g : MAP D E} → (f ∘ pullback₁) =₁ (g ∘ pullback₂)
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.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Factoring a cone through the pullback
pullback-factor
Assumption, type checked
pullback-factor : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} → Cone f g T → MAP T (Pullback f g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The projection comparisons
pullback-factor-β₁
Derivation, checked
pullback-factor-β₁ : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} (s : Cone f g T) → (pullback₁ ∘ pullback-factor s) =₁ Cone.left s
Proof / implementation
pullback-factor-β₁ s = ConeIdentification₁.left (pullback-factor-β s)
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.Section06.Pullbacks where
module _ {Γ : Context} wherepullback-factor-β₂
Derivation, checked
pullback-factor-β₂ : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} (s : Cone f g T) → (pullback₂ ∘ pullback-factor s) =₁ Cone.right s
Proof / implementation
pullback-factor-β₂ s = ConeIdentification₁.right (pullback-factor-β s)
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.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Compatibility of the factorization
pullback-factor-β
Assumption, type checked
pullback-factor-β : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} (s : Cone f g T) → ConeIdentification₁ (cone-restrict (pullback-factor s) (pullback-cone f g)) s
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.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Pullbacks of animae
pullback-isAn
Assumption, type checked
pullback-isAn : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) → isAn C → isAn D → isAn E → isAn (Pullback f g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
For any \(h,k\colon T\to C\times _E D\), the projection-induced functor \[ (h= k)\longrightarrow (\pr _1 h=\pr _1 k) \times _{(f\pr _1 h= g\pr _2 k)} (\pr _2 h=\pr _2 k) \] is an equivalence; here the two functors defining the pullback on the right are \[ \alpha \longmapsto (\tau _{\univ }\star k)\circ (f\star \alpha ), \qquad \beta \longmapsto (g\star \beta )\circ (\tau _{\univ }\star h). \] Interchange with \(\tau _{\univ }\) identifies their composites with the two projections from \((h= k)\) and thereby defines the displayed functor.
Agda The projection-induced functor on isomorphism animae
restriction
Definition, checked
restriction : MAP (h ＝ k) Target
Proof / implementation
restriction = pullback-factor identification-cone
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.Section06.Pullbacks where
module _ {Γ : Context} where
module PullbackIdentifications {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
(h k : MAP T (Pullback f g)) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The uniqueness equivalence
pullback-identifications-isEquiv
Assumption, type checked
pullback-identifications-isEquiv : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} (h k : MAP T (Pullback f g)) → IsEquiv (PullbackIdentifications.restriction h k)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Interchange supplies the comparison matching
identification-cone
Definition, checked
identification-cone : Cone Boundary.left-map Boundary.right-map (h ＝ k)
Proof / implementation
identification-cone = Action.identification-cone
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.Section06.Pullbacks where
module _ {Γ : Context} where
module PullbackIdentifications {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
(h k : MAP T (Pullback f g)) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The final clause uses the pullback construction, now applied to three animae of identifications. In term notation the factorization is written \[ x:T\vdash (a(x),b(x))_{\tau (x)}:C\times _E D. \] The subscript may be omitted when it is clear from context, or left implicit to simplify notation. An identification between two such expressions is written \((\alpha (x),\beta (x))_{\eta (x)}\), where \(\eta \) is the identification between the two composites in the middle anima of identifications of the axiom.
Agda The two boundary maps
identification-cone
Definition, checked
identification-cone : Cone Boundary.left-map Boundary.right-map (h ＝ k)
Proof / implementation
identification-cone = Action.identification-cone
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.Section06.Pullbacks where
module _ {Γ : Context} where
module PullbackIdentifications {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
(h k : MAP T (Pullback f g)) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Pullback tuples in term notation
pullback-factor
Assumption, type checked
pullback-factor : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} → Cone f g T → MAP T (Pullback f g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The matching remains part of a tuple
match
Definition, checked
match : (f ∘ left) =₁ (g ∘ 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.Chapter01.Section06.Cones where
module _ {Γ : Context} where
record Cone {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) (T : CAT Γ) : Set m whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Identifications between pullback tuples
identification
Derivation, checked
identification : h ＝ k
Proof / implementation
identification = Fact.factor chosen
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.Section06.PullbackSquares where
module _ {Γ : Context} where
module PullbackRecovery {C D E T X : CAT Γ} {f : MAP C E} {g : MAP D E}
(h k : MAP T (Pullback f g))
(Φ : ConeIdentification X
(cone-restrict h (pullback-cone f g))
(cone-restrict k (pullback-cone f g))) whereleft-image
Derivation, checked
left-image : ConeIdentification.left (cone-action (pullback-cone f g) identification) =₁ ConeIdentification.left Φ
Proof / implementation
left-image = ConeIdentificationEquality.left recovery-law
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.Section06.PullbackSquares where
module _ {Γ : Context} where
module PullbackRecovery {C D E T X : CAT Γ} {f : MAP C E} {g : MAP D E}
(h k : MAP T (Pullback f g))
(Φ : ConeIdentification X
(cone-restrict h (pullback-cone f g))
(cone-restrict k (pullback-cone f g))) whereright-image
Derivation, checked
right-image : ConeIdentification.right (cone-action (pullback-cone f g) identification) =₁ ConeIdentification.right Φ
Proof / implementation
right-image = ConeIdentificationEquality.right recovery-law
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.Section06.PullbackSquares where
module _ {Γ : Context} where
module PullbackRecovery {C D E T X : CAT Γ} {f : MAP C E} {g : MAP D E}
(h k : MAP T (Pullback f g))
(Φ : ConeIdentification X
(cone-restrict h (pullback-cone f g))
(cone-restrict k (pullback-cone f g))) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The resulting map may be displayed as follows:
Definition 1.6.2 (Pullback square). A commutative square
Agda A pullback square
IsPullback
Definition, checked
IsPullback : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E} → Cone f g S → Set m
Proof / implementation
IsPullback s = IsEquiv (pullback-factor s)
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.Section06.PullbackSquares where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
with matching identification \(\sigma \colon fp= gq\) is a pullback square, or is cartesian, if its induced functor \((p,q)_\sigma \colon P\to C\times _E D\) is an equivalence. We indicate this by putting the symbol \(\lrcorner \) in the square.
A pullback square has the same universal property as the chosen pullback: every cone factors through it with an identification of cone diagrams, and its animae of identifications are given by the displayed pullbacks of animae of identifications. Indeed, transfer the two clauses of the axiom through the equivalence \(P\to C\times _E D\), using Lemma 1.3.10. Conversely, these clauses construct inverse functors between \(P\) and the chosen pullback.
Agda Factorization through any pullback square
factor
Derivation, checked
factor : {T : CAT Γ} → Cone f g T → MAP T S
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.Section06.PullbackSquares where
module _ {Γ : Context} where
module UniversalCone {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g S) (e : IsPullback s) whereβ
Derivation, checked
β : {T : CAT Γ} (t : Cone f g T) → ConeIdentification₁ (cone-restrict (factor t) s) t
Proof / implementation
β t = cone-compose (pullback-factor-β t) (cone-compose (cone-action-One (pullback-cone f g) (factor-triangle t)) (cone-compose (cone-restrict-assoc (factor t) comparison (pullback-cone f g)) (cone-inverse (cone-identification-restrict-One (factor t) (pullback-factor-β s)))))
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.Section06.PullbackSquares where
module _ {Γ : Context} where
module UniversalCone {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g S) (e : IsPullback s) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Transferring cone comparisons to any pullback
identification
Derivation, checked
identification : h =₁ k
Proof / implementation
identification = Fact.factor chosen
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.Section06.UniversalConeIdentifications where
module _ {Γ : Context} where
module UniversalConeIdentification {C D E T S : CAT Γ} {f : MAP C E} {g : MAP D E}
(t : Cone f g T) (e : IsPullback t) (h k : MAP S T)
(Φ : ConeIdentification₁ (cone-restrict h t) (cone-restrict k t)) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Recognizing a pullback from lifting and comparisons
isPullback-from-factor-and-reflection
Derivation, checked
isPullback-from-factor-and-reflection : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E} (s : Cone f g S) (inverse : MAP (Pullback f g) S) (beta : ConeIdentification₁ (cone-restrict inverse s) (pullback-cone f g)) (reflect : (h k : MAP S S) → ConeIdentification₁ (cone-restrict h s) (cone-restrict k s) → h =₁ k) → IsPullback s
Proof / implementation
isPullback-from-factor-and-reflection {f = f} {g} s inverse beta reflect = record { inverse = inverse ; left-inverse-law = reflect (id _) (inverse ∘ comparison) (cone-compose (cone-restrict-assoc comparison inverse s) (cone-compose (cone-inverse (cone-identification-restrict-One comparison beta)) (cone-compose (cone-inverse (pullback-factor-β s)) (cone-restrict-id s)))) ; right-inverse-law = pullback-reflect (id _) (comparison ∘ inverse) (cone-compose (cone-restrict-assoc inverse comparison chosen-cone) (cone-compose (cone-inverse (cone-identification-restrict-One inverse (pullback-factor-β s))) (cone-compose (cone-inverse beta) (cone-restrict-id chosen-cone)))) } where chosen-cone = pullback-cone f g comparison = pullback-factor s
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.Section06.PullbackSquares where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Note that any functor between two pullbacks of the same cospan that respects the projections and the specified identifications making the squares is an equivalence. Indeed, the induced functors to the chosen pullback are equivalences and form a commutative triangle with this functor, so the claim follows by two-out-of-three.
Agda Comparison between pullback cones
comparison
Definition, checked
comparison : MAP S (Pullback f g)
Proof / implementation
comparison = pullback-factor s
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.Section06.PullbackSquares where
module _ {Γ : Context} where
module UniversalCone {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g S) (e : IsPullback s) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proposition 1.6.3. A commutative square of categories is a pullback square if and only if applying \(\Map (T,-)\) gives a pullback square for every category \(T\).
Agda Mapping animae preserve and detect pullbacks
map-preserves-pullback
Derivation, checked
map-preserves-pullback : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E} (T : CAT Γ) (s : Cone f g S) → IsPullback s → IsPullback (mapped-cone T s)
Proof / implementation
map-preserves-pullback {f = f} {g} T s es = equiv-transport ((mapped-cone-factorization T s) ⁻¹) (equiv-compose (mapPost (pullback-factor s)) (pullback-factor (mapped-cone T (pullback-cone f g))) (mapPost-isEquiv (pullback-factor s) es) (MappingPullback.square-isPullback T f g))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} wheremap-detects-pullback
Derivation, checked
map-detects-pullback : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E} (s : Cone f g S) → ((T : CAT Γ) → IsPullback (mapped-cone T s)) → IsPullback s
Proof / implementation
map-detects-pullback {f = f} {g} s tests = post-tests-all (pullback-factor s) (λ T → equiv-cancel-left (mapPost (pullback-factor s)) (pullback-factor (mapped-cone T (pullback-cone f g))) (MappingPullback.square-isPullback T f g) (equiv-transport (mapped-cone-factorization T s) (tests 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.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. We first show that applying \(\Map (T,-)\) to the chosen pullback \(C\times _E D\) results in a pullback square. Postcomposition with the two projections and whiskering with \(\tau _{\univ }\) gives a comparison functor \[ \Map (T,C\times _E D)\longrightarrow \Map (T,C)\times _{\Map (T,E)}\Map (T,D). \] For an inverse, let \(P\) be the anima on the right. Uncurrying the projections to \(\Map (T,C)\) and \(\Map (T,D)\) gives maps from \(P \times T\) to \(C\) and \(D\). Moreover, the identification in the commutative square for \(C \times _E D\) results in an identification of two functors \(P \times T \to E\). The pullback axiom thus supplies a functor from \(P \times T\) to \(C\times _E D\), with the projection comparisons and their compatibility with the squares. Currying gives a candidate inverse functor \(P \to \Map (T,C \times _D E)\).
Agda The mapping-anima comparison
forward
Definition, checked
forward : MAP S R
Proof / implementation
forward = pullback-factor 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.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} where
module MappingPullback {C D E : CAT Γ} (T : CAT Γ) (f : MAP C E) (g : MAP D E) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Uncurrying the universal cone
uncurried
Definition, checked
uncurried : Cone f g (X × 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.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} where
module MappingPullback {C D E : CAT Γ} (T : CAT Γ) (f : MAP C E) (g : MAP D E) where
module FactorCone {X : CAT Γ} (xAn : isAn X) (s : Cone F G X) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Currying the inverse candidate
factor
Definition, checked
factor : MAP X S
Proof / implementation
factor = mapCurry xAn uncurried-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.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} where
module MappingPullback {C D E : CAT Γ} (T : CAT Γ) (f : MAP C E) (g : MAP D E) where
module FactorCone {X : CAT Γ} (xAn : isAn X) (s : Cone F G X) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
To compare the composite on the right to the identity, we first do so on its two projections, where it follows by currying the identifications we just constructed. To show that the resulting two commutative squares are identified, we may again do so after uncurrying, where it follows from unwinding definitions.
Agda The first inverse comparison
factor-law
Derivation, checked
factor-law : ConeIdentification₁ (cone-restrict factor square) s
Proof / implementation
factor-law = ReflectedCone.identification {f = f} {g = g} xAn (cone-restrict factor square) s (cone-compose (pullback-factor-β uncurried) (cone-compose (cone-action-One original (mapCurry-β xAn uncurried-factor)) (MappedCone.evaluate T original 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.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} where
module MappingPullback {C D E : CAT Γ} (T : CAT Γ) (f : MAP C E) (g : MAP D E) where
module FactorCone {X : CAT Γ} (xAn : isAn X) (s : Cone F G X) whereAbout this correspondence
The current proof uses factorization with its full cone comparison and reflection of identifications. This replaces the older presentation by two separately named inverse comparisons.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
For the composite on the left, we need to show its uncurrying agrees with the evaluation map. This can in turn be tested after both projections and comparing the commutativity identifications.
Agda The other inverse comparison
reflect
Derivation, checked
reflect : {X : CAT Γ} → isAn X → (h k : MAP X S) → ConeIdentification₁ (cone-restrict h square) (cone-restrict k square) → h =₁ k
Proof / implementation
reflect xAn h k Φ = uncurry-reflect xAn h k (pullback-reflect {f = f} {g = g} (uncurry h) (uncurry k) (cone-compose (MappedCone.evaluate T original k) (cone-compose (uncurry-cone-identification {f = f} {g = g} Φ) (cone-inverse (MappedCone.evaluate T original h)))))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} where
module MappingPullback {C D E : CAT Γ} (T : CAT Γ) (f : MAP C E) (g : MAP D E) wheresquare-isPullback
Derivation, checked
square-isPullback : IsPullback square
Proof / implementation
square-isPullback = isPullback-from-factor-and-reflection square inverse Inverse.factor-law (reflect (map-isAn T (Pullback f g)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} where
module MappingPullback {C D E : CAT Γ} (T : CAT Γ) (f : MAP C E) (g : MAP D E) whereAbout this correspondence
The current proof uses factorization with its full cone comparison and reflection of identifications. This replaces the older presentation by two separately named inverse comparisons.
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 Mapping animae preserve an arbitrary pullback square
map-preserves-pullback
Derivation, checked
map-preserves-pullback : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E} (T : CAT Γ) (s : Cone f g S) → IsPullback s → IsPullback (mapped-cone T s)
Proof / implementation
map-preserves-pullback {f = f} {g} T s es = equiv-transport ((mapped-cone-factorization T s) ⁻¹) (equiv-compose (mapPost (pullback-factor s)) (pullback-factor (mapped-cone T (pullback-cone f g))) (mapPost-isEquiv (pullback-factor s) es) (MappingPullback.square-isPullback T f g))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} whereAbout this correspondence
These are the corresponding current results or underlying constructions. Some helpers used by the previous proof were consolidated or replaced; no line-by-line agreement of the two implementations is asserted.
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.
Lemma 1.6.4. For functors \(C \to E\) and \(D \to E\), the functor \((\pr _{C}^{\simeq }, \pr _{D}^{\simeq })\colon (C \times _{E} D)^{\simeq } \to C^{\simeq } \times _{E^{\simeq }} D^{\simeq }\) is an equivalence.
Agda Cores preserve pullbacks
map-preserves-pullback
Derivation, checked
map-preserves-pullback : {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E} (T : CAT Γ) (s : Cone f g S) → IsPullback s → IsPullback (mapped-cone T s)
Proof / implementation
map-preserves-pullback {f = f} {g} T s es = equiv-transport ((mapped-cone-factorization T s) ⁻¹) (equiv-compose (mapPost (pullback-factor s)) (pullback-factor (mapped-cone T (pullback-cone f g))) (mapPost-isEquiv (pullback-factor s) es) (MappingPullback.square-isPullback T f g))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.MappingPullbacks where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. This is a special case of Proposition 1.6.3. □
Exercise 1.6.5 (Exercise 1.9.4 (outside selection)). Show that the fiber product is commutative, associative and unital: for functors \(C\to \Gamma \), \(D \to \Gamma \) and \(B \to \Gamma \), there are preferred equivalences \[ C \times _{\Gamma } D \iso D \times _{\Gamma } C, \qquad B \times _{\Gamma } (C \times _{\Gamma } D) \iso (B \times _{\Gamma } C) \times _{\Gamma } D, \qquad C \times _{\Gamma } \Gamma \iso C. \]
Agda Commutativity, associativity and units of pullbacks
pullback-swap-isEquiv
Derivation, checked
pullback-swap-isEquiv : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) → IsEquiv (pullback-swap f g)
Proof / implementation
pullback-swap-isEquiv f g = SwappedCone.isPullback (pullback-cone f g) (pullback-cone-isPullback f g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.PullbackConstructions where
module _ {Γ : Context} wherepullback-unitˡ
Derivation, checked
pullback-unitˡ : {C E : CAT Γ} (f : MAP C E) → IsEquiv (pullback₁ {f = f} {g = id E})
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.PullbackConstructions where
module _ {Γ : Context} wherepullback-unitʳ
Derivation, checked
pullback-unitʳ : {C E : CAT Γ} (f : MAP C E) → IsEquiv (pullback₂ {f = id E} {g = f})
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.PullbackConstructions where
module _ {Γ : Context} whereassociator-isEquiv
Derivation, checked
associator-isEquiv : IsEquiv associator
Proof / implementation
associator-isEquiv = equiv-compose (middle ∘ first) last (equiv-compose first middle (equiv-compose (pullback-swap f (g ∘ pCD)) First.insert (pullback-swap-isEquiv f (g ∘ pCD)) First.insert-isEquiv) (equiv-compose (pullback-swap pCD pCB) Second.flatten (pullback-swap-isEquiv pCD pCB) Second.flatten-isEquiv)) (equiv-compose (pullback-map swap-cospan) Change.forward Swap.pullback-map-isEquiv Change.forward-isEquiv)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.PullbackAssociativity where
module _ {Γ : Context} where
module Associativity {B C D E : CAT Γ} (f : MAP B E) (g : MAP C E) (h : MAP D E) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Exercise 1.6.6 (Exercise 1.9.5 (outside selection)). Consider categories \(C\) and \(D\), and let \(p_C\colon C \to *\) and \(p_D\colon D \to *\) be their functors to the terminal category. Show that the functor \((\pr _1,\pr _2)\colon C \times _* D \to C \times D\) is an equivalence.
Agda Pullback over the terminal category
to-product
Derivation, checked
to-product : MAP (Pullback f g) (C × D)
Proof / implementation
to-product = pair pullback₁ pullback₂
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.Section06.PullbackConstructions where
module _ {Γ : Context} where
module TerminalBase {C D : CAT Γ} (f : MAP C One) (g : MAP D One) whereto-product-isEquiv
Derivation, checked
to-product-isEquiv : IsEquiv to-product
Proof / implementation
to-product-isEquiv = record { inverse = from-product ; left-inverse-law = from-to ⁻¹ ; right-inverse-law = to-from ⁻¹ }
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.Section06.PullbackConstructions where
module _ {Γ : Context} where
module TerminalBase {C D : CAT Γ} (f : MAP C One) (g : MAP D One) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Construction 1.6.7. The construction of pullbacks of categories is functorial: given a commutative diagram
Agda Functoriality of pullbacks
pullback-map
Derivation, checked
pullback-map : {C D E C′ D′ E′ : CAT Γ} {f : MAP C E} {g : MAP D E} {f′ : MAP C′ E′} {g′ : MAP D′ E′} → CospanMap f g f′ g′ → MAP (Pullback f g) (Pullback f′ g′)
Proof / implementation
pullback-map {f = f} {g} F = pullback-factor (CospanMap.map-cone F (pullback-cone f g))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.PullbackFunctoriality where
module _ {Γ : Context} wherepullback-map-β
Derivation, checked
pullback-map-β : {C D E C′ D′ E′ : CAT Γ} {f : MAP C E} {g : MAP D E} {f′ : MAP C′ E′} {g′ : MAP D′ E′} (F : CospanMap f g f′ g′) → ConeIdentification₁ (cone-restrict (pullback-map F) (pullback-cone f′ g′)) (CospanMap.map-cone F (pullback-cone f g))
Proof / implementation
pullback-map-β {f = f} {g} F = pullback-factor-β (CospanMap.map-cone F (pullback-cone f g))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.PullbackFunctoriality where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
there is an induced functor \[ \varphi \times _{\chi } \psi := (\varphi \circ \pr _1, \psi \circ \pr _2)\colon C \times _{\Gamma } D \to C' \times _{\Gamma '} D'. \]
Exercise 1.6.8. In the above situation, show that if each of the functors \(\varphi \), \(\psi \) and \(\chi \) is an equivalence, then so is \(\varphi \times _{\chi } \psi \).
Agda Pullbacks of equivalences
pullback-map-isEquiv
Derivation, checked
pullback-map-isEquiv : IsEquiv (pullback-map F)
Proof / implementation
pullback-map-isEquiv = CospanCartesian.pullback-map-isEquiv F eu (isPullback-from-left-isEquiv ew (cospan-right-cone F) ev)
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.Section06.PullbackFunctoriality where
module _ {Γ : Context} where
module CospanEquivalence {C D E C′ D′ E′ : CAT Γ}
{f : MAP C E} {g : MAP D E} {f′ : MAP C′ E′} {g′ : MAP D′ E′}
(F : CospanMap f g f′ g′) (eu : IsEquiv (CospanMap.left F))
(ev : IsEquiv (CospanMap.right F)) (ew : IsEquiv (CospanMap.base F)) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Corollary 1.6.9. Equivalences are closed under pullback: if \(g\colon D \to E\) is an equivalence and \(f\colon C \to E\) is an arbitrary functor, then also \(C \times _{E} D \to C\) is an equivalence.
Agda Equivalences are closed under pullback
pullback₁-isEquiv
Derivation, checked
pullback₁-isEquiv : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) → IsEquiv g → IsEquiv (pullback₁ {f = f} {g = g})
Proof / implementation
pullback₁-isEquiv = BaseChangeEquivalence.projection-isEquiv
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.PullbackConstructions where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. This is a special case of Exercise 1.6.8 by taking \(C' = C\), \(\Gamma = \Gamma ' = E\), \(D' = E\), \(\varphi = \id _{C}\), \(\chi = \id _{E}\) and \(\psi = g\): this exhibits the projection \(C \times _{E} D \to C\) as the composite of the equivalence \(\varphi \times _{\chi } \psi \colon C \times _{E} D \to C \times _{E} E\) with the unitality equivalence \(C \times _{E} E \iso C\) from Exercise 1.6.5. □
1.6.1 Fibers of functors
Pullbacks of categories lead to the notion of a fiber of a functor:
Definition 1.6.10 (Fiber). Let \(f\colon C \to D\) be a functor and let \(x\colon *\to D\) be an absolute object. We define the fiber of \(f\) over \(x\) as the pullback
Agda The fiber over an absolute object
Pullback
Assumption, type checked
Pullback : {C D E : CAT Γ} → MAP C E → MAP D E → 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.Section06.Pullbacks where
module _ {Γ : Context} wherepullback₁
Definition, checked
pullback₁ : {C D E : CAT Γ} {f : MAP C E} {g : MAP D E} → MAP (Pullback f g) C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Pullbacks where
module _ {Γ : Context} wherepullback-match
Definition, checked
pullback-match : {C D E : CAT Γ} {f : MAP C E} {g : MAP D E} → (f ∘ pullback₁) =₁ (g ∘ pullback₂)
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.Section06.Pullbacks where
module _ {Γ : Context} whereAbout this correspondence
The fiber is the specialization of Pullback to a functor and a point from One; rebuild2 does not introduce a separate Fiber abbreviation.
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.
One particular case is the fiber of a map \(b\colon * \to C\) over some object \(a\colon * \to C\). The absolute terms of this fiber can be identified with identifications \(\alpha \colon a = b\). We impose as an axiom that the same holds in families:
Axiom B.7 (Representability of identifications). For every category \(C\) and absolute objects \(a,b \in C\), there is an identification \[ \varepsilon :\const _a=\const _b \] of functors \((a=b) \to C\) such that the square
Agda Representability of identifications
identification
Assumption, type checked
identification : {E : CAT Γ} (a b : Obj-abs E) → (const {P = a ＝ b} a) =₁ const b
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.Section06.Representability where
module _ {Γ : Context} whereidentification-isPullback
Assumption, type checked
identification-isPullback : {E : CAT Γ} (a b : Obj-abs E) → IsPullback (identification-square a b (identification a b))
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.Section06.Representability where
module _ {Γ : Context} whereidentification-evaluate-β
Assumption, type checked
identification-evaluate-β : {E : CAT Γ} (a b : Obj-abs E) (α : a =₁ b) → identification-evaluate a b (identification a b) α =₂ α
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.Section06.Representability where
module _ {Γ : Context} whereAbout this correspondence
The primitive assumption uses the manuscript fiber square. The later RepresentabilityDiagonal module derives the diagonal formulation; that result is not an additional axiom.
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.
For a functor \(u\colon T\to (a=b)\), the corresponding identification between the constant functors \(T\to C\) is obtained by prewhiskering \(\varepsilon \) with \(u\), using the terminal-category comparisons to identify its source and target.
1.6.2 Properties of pullback squares
Lemma 1.6.11 (Pasting lemma for pullback squares). Consider a commutative diagram
Agda Pasting and cancellation of pullback squares
paste-isPullback
Derivation, checked
paste-isPullback : {S : CAT Γ} (s : Cone f (Cone.left t) S) → IsPullback s → IsPullback (Paste.paste s)
Proof / implementation
paste-isPullback s es = equiv-transport (factor-law s ⁻¹) (equiv-compose (pullback-factor s) Nest.flatten es Nest.flatten-isEquiv)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.PastingLemma where
module _ {Γ : Context} where
module Pasting {A B X Z Q : CAT Γ} (f : MAP A B) (g : MAP B Z) (h : MAP X Z)
(t : Cone g h Q) (e : IsPullback t) whereunpaste-isPullback
Derivation, checked
unpaste-isPullback : {S : CAT Γ} (s : Cone f (Cone.left t) S) → IsPullback (Paste.paste s) → IsPullback s
Proof / implementation
unpaste-isPullback s ep = equiv-cancel-left (pullback-factor s) Nest.flatten Nest.flatten-isEquiv (equiv-transport (factor-law s) ep)
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.Section06.PastingLemma where
module _ {Γ : Context} where
module Pasting {A B X Z Q : CAT Γ} (f : MAP A B) (g : MAP B Z) (h : MAP X Z)
(t : Cone g h Q) (e : IsPullback t) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
- (1)
-
There is a preferred equivalence \(D_1 \times _{D_3} C_3 \iso D_1 \times _{D_2} (D_2 \times _{D_3} C_3)\).
- (2)
-
If the right-hand square is a pullback square, then the left-hand square is a pullback square if and only if the outer rectangle is a pullback square.
Proof
Proof. For part (1), we define the functor as \((\pr _1, (h_1 \circ \pr _1, \pr _2))\). We claim that an inverse is given by the functor \[ (\pr _1, \pr _2 \circ \pr _2)\colon D_1 \times _{D_2} (D_2 \times _{D_3} C_3) \to D_1 \times _{D_3} C_3. \] To show that the two composites are identified with the respective identities, it suffices to construct these identifications after projecting to the two components and verifying that these identifications agree after composing with the functors to \(D_3\). But after unwinding the definitions, this holds tautologically by the very construction of the two functors in both directions.
Agda The nested-pullback insertion
insert
Definition, checked
insert : MAP Outer NestedVertex
Proof / implementation
insert = pullback-factor insertion-cone
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.Section06.NestedPullbacks where
module _ {Γ : Context} where
module Nested {A B X Z Q : CAT Γ} (f : MAP A B) (g : MAP B Z) (h : MAP X Z)
(t : Cone g h Q) (e : IsPullback t) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The nested-pullback projection
flatten
Definition, checked
flatten : MAP NestedVertex Outer
Proof / implementation
flatten = pullback-factor flat-cone
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.Section06.NestedPullbacks where
module _ {Γ : Context} where
module Nested {A B X Z Q : CAT Γ} (f : MAP A B) (g : MAP B Z) (h : MAP X Z)
(t : Cone g h Q) (e : IsPullback t) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The two inverse comparisons
insert-flatten
Derivation, checked
insert-flatten : (insert ∘ flatten) =₁ id NestedVertex
Proof / implementation
insert-flatten = pullback-reflect _ _ (cone-compose (cone-inverse (cone-restrict-id nested-cone)) (cone-compose insertion-cone-comparison (cone-compose (cone-identification-restrict-One flatten insert-β) (cone-inverse (cone-restrict-assoc flatten insert nested-cone)))))
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.Section06.NestedPullbacks where
module _ {Γ : Context} where
module Nested {A B X Z Q : CAT Γ} (f : MAP A B) (g : MAP B Z) (h : MAP X Z)
(t : Cone g h Q) (e : IsPullback t) whereflatten-insert
Derivation, checked
flatten-insert : (flatten ∘ insert) =₁ id Outer
Proof / implementation
flatten-insert = pullback-reflect _ _ (cone-compose (cone-inverse (cone-restrict-id outer-cone)) (cone-compose pasted-insertion-comparison (cone-compose (Paste.paste-identification insert-β) (cone-compose (Paste.paste-restrict insert nested-cone) (cone-compose (cone-identification-restrict-One insert flatten-β) (cone-inverse (cone-restrict-assoc insert flatten outer-cone)))))))
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.Section06.NestedPullbacks where
module _ {Γ : Context} where
module Nested {A B X Z Q : CAT Γ} (f : MAP A B) (g : MAP B Z) (h : MAP X Z)
(t : Cone g h Q) (e : IsPullback t) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Part (2) is an immediate consequence of the 2-out-of-3 property from Lemma 1.3.6 applied to the following commutative square:
where the right vertical map is an equivalence by applying Exercise 1.6.8 to the equivalence \(C_2 \iso D_2 \times _{D_3} C_3\). □
Lemma 1.6.12. Consider a commutative square
Agda A square with an equivalence on one edge
isPullback-from-left-isEquiv
Derivation, checked
isPullback-from-left-isEquiv : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} → IsEquiv g → (s : Cone f g T) → IsEquiv (Cone.left s) → IsPullback s
Proof / implementation
isPullback-from-left-isEquiv {f = f} {g} eg s es = equiv-cancel-left (pullback-factor s) pullback₁ (pullback₁-isEquiv f g eg) (equiv-transport ((pullback-factor-β₁ s) ⁻¹) es)
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.Section06.PullbackConstructions where
module _ {Γ : Context} whereleft-isEquiv-from-isPullback
Derivation, checked
left-isEquiv-from-isPullback : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} → IsEquiv g → (s : Cone f g T) → IsPullback s → IsEquiv (Cone.left s)
Proof / implementation
left-isEquiv-from-isPullback {f = f} {g} eg s es = equiv-transport (pullback-factor-β₁ s) (equiv-compose (pullback-factor s) pullback₁ es (pullback₁-isEquiv f g eg))
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.Section06.PullbackConstructions where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
and assume that \(h\) is an equivalence. Then \(g\) is an equivalence if and only if the square is a pullback square.
Proof
Proof. Since \(h\) is an equivalence, also the projection map \(\pr _2\colon D \times _{F} E \to E\) is an equivalence by Corollary 1.6.9. Since the composite of the map \((f,g) \colon C \to D \times _{F} E\) with \(\pr _2\) is identified with \(g\), the claim follows from the 2-out-of-3 property of equivalences, Lemma 1.3.6. □
Lemma 1.6.13. Consider functors \(f\colon C \to E\) and \(g\colon D \to E\). Then the commutative square
Agda Pullbacks as pullbacks of the diagonal
preserve
Derivation, checked
preserve : IsPullback s → IsPullback value
Proof / implementation
preserve es = equiv-transport (factor-law ⁻¹) (equiv-compose (pullback-factor s) forward es forward-isEquiv)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.DiagonalPullbacks where
module _ {Γ : Context} where
module DiagonalPullback {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) where
module Square {T : CAT Γ} (s : Cone f g T) wherereflect
Derivation, checked
reflect : IsPullback value → IsPullback s
Proof / implementation
reflect es = equiv-cancel-left (pullback-factor s) forward forward-isEquiv (equiv-transport factor-law es)
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.Section06.DiagonalPullbacks where
module _ {Γ : Context} where
module DiagonalPullback {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) where
module Square {T : CAT Γ} (s : Cone f g T) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
is a pullback square.
Proof
Proof. This follows immediately from the pasting lemma for pullback squares, Lemma 1.6.11, applied to the following commutative diagram:
1.6.3 Universality of coproducts
The strictness of the initial category immediately implies its universality:
Lemma 1.6.14. For every functor \(g\colon D \to E\), the commutative square
Agda The canonical square on the initial category
empty-cone
Derivation, checked
empty-cone : {D E : CAT Γ} (g : MAP D E) → Cone (initiate E) g Zero
Proof / implementation
empty-cone g = record { left = id Zero ; right = initiate _ ; match = initial-unique _ _ }
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.Section06.DisjointCoproducts where
module _ {Γ : Context} whereempty-isPullback
Derivation, checked
empty-isPullback : {D E : CAT Γ} (g : MAP D E) → IsPullback (empty-cone g)
Proof / implementation
empty-isPullback {E = E} g = equiv-cancel-left (pullback-factor (empty-cone g)) projection (into-zero-isEquiv projection) (into-zero-isEquiv (projection ∘ pullback-factor (empty-cone g))) where projection : MAP (Pullback (initiate E) g) Zero projection = pullback₁
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.Section06.DisjointCoproducts where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
is a pullback square.
Proof
Proof. We need to show that the induced map \(\emptyset \to \emptyset \times _E D\) is an equivalence. But this follows directly from Axiom B.4’ by applying 2-out-of-3 to the maps \(\emptyset \to \emptyset \times _E D \xrightarrow {\pr _1} \emptyset \). □
We now postulate a analogous universality property on coproducts of categories:
Axiom B.5’ (Universality of coproducts). Consider categories \(\Gamma _0\) and \(\Gamma _1\), define \(\Gamma := \Gamma _0 \sqcup \Gamma _1\), and let \(i_0\colon \Gamma _0 \to \Gamma \) and \(i_1\colon \Gamma _1 \to \Gamma \) denote the two inclusions.
- (1)
-
For functors \(f\colon C \to \Gamma _0\) and \(g\colon D \to \Gamma _1\), the commutative squares
Agda The two inclusion squares are pullbacks
coproductSquare₁Definition, checked
coproductSquare₁ : {C D P Q : CAT Γ} (f : MAP C P) (g : MAP D Q) → Cone (in₁ {C = P} {D = Q}) (coproductMap f g) C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section06.UniversalCoproducts where module _ {Γ : Context} wherecoproductSquare₂Definition, checked
coproductSquare₂ : {C D P Q : CAT Γ} (f : MAP C P) (g : MAP D Q) → Cone (in₂ {C = P} {D = Q}) (coproductMap f g) D
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section06.UniversalCoproducts where module _ {Γ : Context} whereinclusion₁-isPullbackAssumption, type checked
inclusion₁-isPullback : {C D P Q : CAT Γ} (f : MAP C P) (g : MAP D Q) → IsPullback (coproductSquare₁ f g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section06.UniversalCoproducts where module _ {Γ : Context} whereinclusion₂-isPullbackAssumption, type checked
inclusion₂-isPullback : {C D P Q : CAT Γ} (f : MAP C P) (g : MAP D Q) → IsPullback (coproductSquare₂ f g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section06.UniversalCoproducts where module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
are pullback squares.
- (2)
-
For a functor \(h\colon E \to \Gamma \), the functor \[ \lra {\pr _1,\pr _1} \colon (E \times _{\Gamma } \Gamma _0) \sqcup (E \times _{\Gamma } \Gamma _1) \to E \] is an equivalence.
Agda Reassembly from the two pullbacks
reassembleDefinition, checked
reassemble : {E P Q : CAT Γ} (h : MAP E (P ⊔ Q)) → MAP (Pullback h in₁ ⊔ Pullback h in₂) E
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section06.UniversalCoproducts where module _ {Γ : Context} wherereassemble-isEquivAssumption, type checked
reassemble-isEquiv : {E P Q : CAT Γ} (h : MAP E (P ⊔ Q)) → IsEquiv (reassemble h)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section06.UniversalCoproducts where module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Corollary 1.6.15 (Disjointness of coproducts). Coproducts are disjoint: for categories \(C\) and \(D\), the commutative square
Agda Disjointness of coproducts
disjoint-isPullback
Derivation, checked
disjoint-isPullback : (C D : CAT Γ) → IsPullback (disjoint-cone C D)
Proof / implementation
disjoint-isPullback = Disjointness.isPullback
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.Section06.DisjointCoproducts where
module _ {Γ : Context} whereAbout this correspondence
These are the corresponding current results or underlying constructions. Some helpers used by the previous proof were consolidated or replaced; no line-by-line agreement of the two implementations is asserted.
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. □
Lemma 1.6.16. For functors \(f\colon C \to \Gamma \), \(g\colon D \to \Gamma \) and \(\varphi \colon \Gamma ' \to \Gamma \), the commutative square
Agda Descent for coproducts
descent-isEquiv
Derivation, checked
descent-isEquiv : IsEquiv descent
Proof / implementation
descent-isEquiv = equiv-transport reassembly-law (equiv-compose (coproductMap identify₁ identify₂) (reassemble totalProjection) (coproductMap-isEquiv identify₁ identify₂ identify₁-isEquiv identify₂-isEquiv) (reassemble-isEquiv totalProjection))
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.Section06.CoproductDescent where
module _ {Γ : Context} where
module Descent {C D P Q : CAT Γ} (f : MAP C P) (g : MAP D P) (φ : MAP Q P) whereAbout this correspondence
The current Descent construction proves the reassembly equivalence directly, retaining its two pullback identifications. This replaces the older separate direct-square helper.
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.
Proof
Proof. We need to show that the induced functor \[ (C \times _{\Gamma } \Gamma ') \sqcup (D \times _{\Gamma } \Gamma ') \to (C \sqcup D) \times _\Gamma \Gamma ' \] is an equivalence. But this is a special case of Axiom B.5’ applied to the functor \(f = \pr _1\colon (C \sqcup D) \times _\Gamma \Gamma ' \to C \sqcup D\): by the pasting law of pullback squares there are equivalences \[ C \times _{C \sqcup D} (C \sqcup D) \times _\Gamma \Gamma ' \simeq C \times _\Gamma \Gamma ' \qquadtext { and } D \times _{C \sqcup D} (C \sqcup D) \times _\Gamma \Gamma ' \simeq D \times _\Gamma \Gamma '. \] This finishes the proof. □
Agda Identifying the two iterated pullbacks
identify₁-isEquiv
Derivation, checked
identify₁-isEquiv : IsEquiv identify₁
Proof / implementation
identify₁-isEquiv = equiv-compose (LeftNesting.insert ∘ LeftBoundary.forward) (pullback-swap in₁ totalProjection) (equiv-compose LeftBoundary.forward LeftNesting.insert LeftBoundary.forward-isEquiv LeftNesting.insert-isEquiv) (pullback-swap-isEquiv in₁ totalProjection)
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.Section06.CoproductDescent where
module _ {Γ : Context} where
module Descent {C D P Q : CAT Γ} (f : MAP C P) (g : MAP D P) (φ : MAP Q P) whereidentify₂-isEquiv
Derivation, checked
identify₂-isEquiv : IsEquiv identify₂
Proof / implementation
identify₂-isEquiv = equiv-compose (RightNesting.insert ∘ RightBoundary.forward) (pullback-swap in₂ totalProjection) (equiv-compose RightBoundary.forward RightNesting.insert RightBoundary.forward-isEquiv RightNesting.insert-isEquiv) (pullback-swap-isEquiv in₂ totalProjection)
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.Section06.CoproductDescent where
module _ {Γ : Context} where
module Descent {C D P Q : CAT Γ} (f : MAP C P) (g : MAP D P) (φ : MAP Q P) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The descent comparison is an equivalence
descent-isEquiv
Derivation, checked
descent-isEquiv : IsEquiv descent
Proof / implementation
descent-isEquiv = equiv-transport reassembly-law (equiv-compose (coproductMap identify₁ identify₂) (reassemble totalProjection) (coproductMap-isEquiv identify₁ identify₂ identify₁-isEquiv identify₂-isEquiv) (reassemble-isEquiv totalProjection))
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.Section06.CoproductDescent where
module _ {Γ : Context} where
module Descent {C D P Q : CAT Γ} (f : MAP C P) (g : MAP D P) (φ : MAP Q P) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Corollary 1.6.17 (Distributivity). For categories \(C\), \(D\) and \(E\), the functor \[ \lra {E \times i_C, E \times i_D} \colon E \times C \sqcup E \times D \to E \times (C \sqcup D) \] is an equivalence.
Agda Products distribute over coproducts
distribute
Definition, checked
distribute : MAP ((E × C) ⊔ (E × D)) (E × (C ⊔ D))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Distributivity where
module _ {Γ : Context} where
module Distributivity (E C D : CAT Γ) wheredistribute-isEquiv
Derivation, checked
distribute-isEquiv : IsEquiv distribute
Proof / implementation
distribute-isEquiv = equiv-transport descent-law (equiv-compose (Base.descent ∘ sourceChange) Total.to-swapped (equiv-compose sourceChange Base.descent (coproductMap-isEquiv Left.from-swapped Right.from-swapped Left.from-swapped-isEquiv Right.from-swapped-isEquiv) Base.descent-isEquiv) Total.to-swapped-isEquiv)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Distributivity where
module _ {Γ : Context} where
module Distributivity (E C D : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Agda Distributivity from descent over the terminal category
distribute-isEquiv
Derivation, checked
distribute-isEquiv : IsEquiv distribute
Proof / implementation
distribute-isEquiv = equiv-transport descent-law (equiv-compose (Base.descent ∘ sourceChange) Total.to-swapped (equiv-compose sourceChange Base.descent (coproductMap-isEquiv Left.from-swapped Right.from-swapped Left.from-swapped-isEquiv Right.from-swapped-isEquiv) Base.descent-isEquiv) Total.to-swapped-isEquiv)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Distributivity where
module _ {Γ : Context} where
module Distributivity (E C D : CAT Γ) whereAbout this correspondence
These are the corresponding current results or underlying constructions. Some helpers used by the previous proof were consolidated or replaced; no line-by-line agreement of the two implementations is asserted.
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.
Consequently, expressions with an additional parameter \(t:T\) may be defined by cases: combine the functors \(T\times C\to E\) and \(T\times D\to E\) by copairing, then precompose with the inverse of distributivity. Their restriction comparisons are the comparisons of the resulting expression on the two summands.
Agda Case distinction with an additional parameter
distribute-isEquiv
Derivation, checked
distribute-isEquiv : IsEquiv distribute
Proof / implementation
distribute-isEquiv = equiv-transport descent-law (equiv-compose (Base.descent ∘ sourceChange) Total.to-swapped (equiv-compose sourceChange Base.descent (coproductMap-isEquiv Left.from-swapped Right.from-swapped Left.from-swapped-isEquiv Right.from-swapped-isEquiv) Base.descent-isEquiv) Total.to-swapped-isEquiv)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Distributivity where
module _ {Γ : Context} where
module Distributivity (E C D : CAT Γ) wherecopair
Derivation, checked
copair : {C D E : CAT Γ} → MAP C E → MAP D E → MAP (C ⊔ D) E
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section05.Copairing where
module _ {Γ : Context} wherecopair-β₁
Derivation, checked
copair-β₁ : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) → (copair f g ∘ in₁) =₁ f
Proof / implementation
copair-β₁ f g = name-reflect (copair f g ∘ in₁) f (pair-β₁ (name f) (name g) ∙ ((pr₁ ◁ copairName-β f g) ∙ ((project-pair₁ (mapPre in₁) (mapPre in₂) (copairName f g)) ⁻¹ ∙ ((mapPre in₁ ◁ name-decode (copairName f g)) ∙ (mapPre-name in₁ (copair f g)) ⁻¹))))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section05.Copairing where
module _ {Γ : Context} wherecopair-β₂
Derivation, checked
copair-β₂ : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) → (copair f g ∘ in₂) =₁ g
Proof / implementation
copair-β₂ f g = name-reflect (copair f g ∘ in₂) g (pair-β₂ (name f) (name g) ∙ ((pr₂ ◁ copairName-β f g) ∙ ((project-pair₂ (mapPre in₁) (mapPre in₂) (copairName f g)) ⁻¹ ∙ ((mapPre in₂ ◁ name-decode (copairName f g)) ∙ (mapPre-name in₂ (copair f g)) ⁻¹))))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section05.Copairing where
module _ {Γ : Context} whereAbout this correspondence
The ingredients are the distributivity equivalence and copairing, with its two restriction comparisons. No separate named cases operator is introduced here.
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 case restriction comparisons
distribute-isEquiv
Derivation, checked
distribute-isEquiv : IsEquiv distribute
Proof / implementation
distribute-isEquiv = equiv-transport descent-law (equiv-compose (Base.descent ∘ sourceChange) Total.to-swapped (equiv-compose sourceChange Base.descent (coproductMap-isEquiv Left.from-swapped Right.from-swapped Left.from-swapped-isEquiv Right.from-swapped-isEquiv) Base.descent-isEquiv) Total.to-swapped-isEquiv)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Distributivity where
module _ {Γ : Context} where
module Distributivity (E C D : CAT Γ) wherecopair
Derivation, checked
copair : {C D E : CAT Γ} → MAP C E → MAP D E → MAP (C ⊔ D) E
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section05.Copairing where
module _ {Γ : Context} wherecopair-β₁
Derivation, checked
copair-β₁ : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) → (copair f g ∘ in₁) =₁ f
Proof / implementation
copair-β₁ f g = name-reflect (copair f g ∘ in₁) f (pair-β₁ (name f) (name g) ∙ ((pr₁ ◁ copairName-β f g) ∙ ((project-pair₁ (mapPre in₁) (mapPre in₂) (copairName f g)) ⁻¹ ∙ ((mapPre in₁ ◁ name-decode (copairName f g)) ∙ (mapPre-name in₁ (copair f g)) ⁻¹))))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section05.Copairing where
module _ {Γ : Context} wherecopair-β₂
Derivation, checked
copair-β₂ : {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) → (copair f g ∘ in₂) =₁ g
Proof / implementation
copair-β₂ f g = name-reflect (copair f g ∘ in₂) g (pair-β₂ (name f) (name g) ∙ ((pr₂ ◁ copairName-β f g) ∙ ((project-pair₂ (mapPre in₁) (mapPre in₂) (copairName f g)) ⁻¹ ∙ ((mapPre in₂ ◁ name-decode (copairName f g)) ∙ (mapPre-name in₂ (copair f g)) ⁻¹))))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section05.Copairing where
module _ {Γ : Context} whereAbout this correspondence
These are the copairing comparisons used after transporting along distributivity. This is a link to the ingredients, not a separately named parametrized-cases theorem.
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.
Lemma 1.6.18. The following two conditions are equivalent:
Agda Contractibility of the two-point coproduct
two-contractible-implies-all
Derivation, checked
two-contractible-implies-all : IsContractible (One ⊔ One) → (C : CAT Γ) → IsContractible C
Proof / implementation
two-contractible-implies-all two-contractible C = contractible-source to-zero (into-zero-isEquiv to-zero) zero-contractible where inclusion : MAP One (One ⊔ One) inclusion = in₁ inclusion-isEquiv : IsEquiv inclusion inclusion-isEquiv = equiv-cancel-left inclusion (terminate (One ⊔ One)) two-contractible (equiv-transport (terminal-identification (id One) _ ) (id-isEquiv One)) initial-terminal-isEquiv : IsEquiv (initiate One) initial-terminal-isEquiv = left-isEquiv-from-isPullback inclusion-isEquiv (disjoint-cone One One) (disjoint-isPullback One One) zero-contractible : IsContractible Zero zero-contractible = equiv-transport (terminal-identification (initiate One) (terminate Zero)) initial-terminal-isEquiv to-zero : MAP C Zero to-zero = IsEquiv.inverse initial-terminal-isEquiv ∘ terminate C
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.DisjointCoproducts where
module _ {Γ : Context} whereAbout this correspondence
These are the corresponding current results or underlying constructions. Some helpers used by the previous proof were consolidated or replaced; no line-by-line agreement of the two implementations is asserted.
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.
- (1)
-
The category \(* \sqcup *\) is contractible;
- (2)
-
Every category is contractible.
Proof
Proof. It is clear that (2) implies (1). Conversely, assume that \(* \sqcup *\) is contractible, i.e. that the map \(* \sqcup * \to *\) is an equivalence. Since this map admits a section given by the left inclusion \(l\colon * = * \sqcup \emptyset \hookrightarrow * \sqcup *\), it follows that \(l\) is an equivalence. In particular, its fiber over the right point must be contractible. Since this fiber is the empty category \(\emptyset \) by Corollary 1.6.15, we see that the map \(\emptyset \to *\) is an equivalence, and it follows from taking the product with any category \(C\) that also \(\emptyset \to C\) is an equivalence. By 2-out-of-3 this implies that \(C\) is contractible. □
1.6.4 Embeddings of categories
We introduce the notion of embeddings of categories and prove basic properties about them. We will eventually see that embeddings precisely correspond to subcategories, see Proposition 6.4.1 (outside selection).
Definition 1.6.19 (Embedding). A functor \(f\colon C \to D\) is called an embedding if the diagonal \(\Delta _f := (\id _{C},\id _{C})\colon C \to C \times _{D} C\) is an equivalence, or equivalently if the commutative diagram
Agda An embedding of categories
diagonal
Definition, checked
diagonal : {C D : CAT Γ} (f : MAP C D) → MAP C (Pullback f f)
Proof / implementation
diagonal f = pullback-factor (diagonal-cone f)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Embeddings where
module _ {Γ : Context} whereIsEmbedding
Definition, checked
IsEmbedding : {C D : CAT Γ} → MAP C D → Set m
Proof / implementation
IsEmbedding f = IsPullback (diagonal-cone f)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Embeddings where
module _ {Γ : Context} whereAbout this correspondence
These are the corresponding current results or underlying constructions. Some helpers used by the previous proof were consolidated or replaced; no line-by-line agreement of the two implementations is asserted.
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.
Proposition 1.6.20. A functor \(f\colon C \to D\) is an embedding if and only if for every category \(E\) the induced map \(f_*\colon \Map (E,C) \to \Map (E,D)\) is an embedding.
Agda Testing embeddings on mapping animae
map-preserves-embedding
Derivation, checked
map-preserves-embedding : {C D : CAT Γ} (T : CAT Γ) (f : MAP C D) → IsEmbedding f → IsEmbedding (mapPost {C = T} f)
Proof / implementation
map-preserves-embedding T f ef = embedding-from-projection-isEquiv (mapPost f) (equiv-cancel-right (pullback-factor (mapped-cone T (pullback-cone f f))) pullback₁ (MappingPullback.square-isPullback T f f) (equiv-transport ((pullback-factor-β₁ (mapped-cone T (pullback-cone f f))) ⁻¹) (mapPost-isEquiv pullback₁ (embedding-projection-isEquiv f ef))))
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.Section06.EmbeddingCharacterizations where
module _ {Γ : Context} wheremap-detects-embedding
Derivation, checked
map-detects-embedding : {C D : CAT Γ} (f : MAP C D) → ((T : CAT Γ) → IsEmbedding (mapPost {C = T} f)) → IsEmbedding f
Proof / implementation
map-detects-embedding f tests = embedding-from-projection-isEquiv f (post-tests-all pullback₁ (λ T → equiv-transport (pullback-factor-β₁ (mapped-cone T (pullback-cone f f))) (equiv-compose (pullback-factor (mapped-cone T (pullback-cone f f))) pullback₁ (MappingPullback.square-isPullback T f f) (embedding-projection-isEquiv (mapPost f) (tests 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.Chapter01.Section06.EmbeddingCharacterizations where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. This follows immediately from Proposition 1.6.3 by considering the commutative diagram
Corollary 1.6.21. Given an embedding \(f\colon C \to D\), the functor \(f^{\simeq } \colon C^{\simeq } \to D^{\simeq }\) is also an embedding.
Agda Cores preserve embeddings
map-preserves-embedding
Derivation, checked
map-preserves-embedding : {C D : CAT Γ} (T : CAT Γ) (f : MAP C D) → IsEmbedding f → IsEmbedding (mapPost {C = T} f)
Proof / implementation
map-preserves-embedding T f ef = embedding-from-projection-isEquiv (mapPost f) (equiv-cancel-right (pullback-factor (mapped-cone T (pullback-cone f f))) pullback₁ (MappingPullback.square-isPullback T f f) (equiv-transport ((pullback-factor-β₁ (mapped-cone T (pullback-cone f f))) ⁻¹) (mapPost-isEquiv pullback₁ (embedding-projection-isEquiv f ef))))
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.Section06.EmbeddingCharacterizations where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. In light of the definition of embeddings, this is immediate from Lemma 1.6.4. □
Lemma 1.6.22. A functor \(f\colon C \to D\) is an embedding if and only if the commutative square
Agda The alternative diagonal characterization
square
Definition, checked
square : Cone (productMap f f) (pair (id D) (id D)) C
Proof / implementation
square = cone-change-legs Square.value (pair (id C) (id C)) f (id₌ (pair (id C) (id C))) (comp-unitʳ f)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.EmbeddingCharacterizations where
module _ {Γ : Context} where
module DiagonalCharacterization {C D : CAT Γ} (f : MAP C D) wherefrom-embedding
Derivation, checked
from-embedding : IsEmbedding f → IsPullback square
Proof / implementation
from-embedding ef = isPullback-cone-identification cone-law (Square.preserve ef)
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.Section06.EmbeddingCharacterizations where
module _ {Γ : Context} where
module DiagonalCharacterization {C D : CAT Γ} (f : MAP C D) whereto-embedding
Derivation, checked
to-embedding : IsPullback square → IsEmbedding f
Proof / implementation
to-embedding es = Square.reflect (isPullback-cone-identification (cone-inverse cone-law) es)
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.Section06.EmbeddingCharacterizations where
module _ {Γ : Context} where
module DiagonalCharacterization {C D : CAT Γ} (f : MAP C D) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
is a pullback square.
Proof
Proof. By Lemma 1.6.13 the pullback of this diagram is \(C \times _D C\). Since the induced map \(C \to C \times _D C\) is precisely the diagonal \(\Delta _f\colon C \to C \times _D C\) of \(f\), the claim follows. □
Lemma 1.6.23. Consider a pullback square
Agda Embeddings are closed under base change
base-change-embedding
Derivation, checked
base-change-embedding : {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E} (s : Cone f g T) → IsPullback s → IsEmbedding g → IsEmbedding (Cone.left s)
Proof / implementation
base-change-embedding {f = f} {g} s es eg = embedding-cong (pullback-factor-β₁ s) (LeftCancellation.compose (pullback-factor s) pullback₁ (chosen-base-change-embedding f g eg) (equivalence-isEmbedding (pullback-factor s) es))
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.Section06.Embeddings where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
of categories. If \(v\) is an embedding, then also \(u\) is an embedding.
Proof
Proof. This is left as an exercise for the reader, see Exercise 1.9.10 (outside selection) □
Lemma 1.6.24. Let \(f\colon C \to D\) be an embedding which admits a section \(s\colon D \to C\). Then \(f\) is an equivalence.
Agda An embedding with a section is an equivalence
embedding-with-section
Derivation, checked
embedding-with-section : {C D : CAT Γ} (f : MAP C D) → IsEmbedding f → Section f → IsEquiv f
Proof / implementation
embedding-with-section f ef σ = record { inverse = Section.section σ ; left-inverse-law = embedding-reflect f ef _ _ (comp-assoc f (Section.section σ) f ∙ ((Section.section-law σ ▷ f) ∙ ((comp-unitˡ f) ⁻¹ ∙ comp-unitʳ f))) ; right-inverse-law = Section.section-law σ }
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.Section06.Embeddings where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. As \(fs = \id _D\), it remains to show that \(sf = \id _C\). Consider the following commutative diagram:
Agda Reflecting the remaining inverse comparison
embedding-reflect
Derivation, checked
embedding-reflect : (f : MAP C D) → IsEmbedding f → (x y : Term C) → (f ∘ x) =₁ (f ∘ y) → x =₁ y
Proof / implementation
embedding-reflect f ef x y α = pullback-factor-β₂ s ∙ ((embedding-projections-equal f ef ▷ pullback-factor s) ∙ (pullback-factor-β₁ s) ⁻¹) where s : Cone f f T s = record { left = x; right = y; match = α }
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.Section06.Embeddings where
module _ {Γ : Context} where
module _ {T C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Since the right square is a pullback square by assumption on \(f\), there exists a map \(h \colon C \to C\) making the diagram commute. It follows that \(sf = h = \id _C\), finishing the proof. □
We will now prove some more intricate properties about embeddings, which may be skipped on first reading and referred back to whenever needed.
Lemma 1.6.25. Let \(f\colon C \to D\) and \(g\colon D \to E\) be functors and assume that \(g\) is an embedding. Then the square
Agda The auxiliary square for an embedding
composition-cone
Derivation, checked
composition-cone : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → Cone (g ∘ f) g C
Proof / implementation
composition-cone {C} f g = record { left = id C ; right = f ; match = comp-unitʳ (g ∘ f) }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Embeddings where
module _ {Γ : Context} wherecomposition-cone-isPullback
Derivation, checked
composition-cone-isPullback : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEmbedding g → IsPullback (composition-cone f g)
Proof / implementation
composition-cone-isPullback f g eg = equiv-cancel-left (pullback-factor (composition-cone f g)) pullback₁ (nested-projection-isEquiv f g g (embedding-projection-isEquiv g eg)) (equiv-transport ((pullback-factor-β₁ (composition-cone f g)) ⁻¹) (id-isEquiv _))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section06.Embeddings where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
is a pullback square.
Proof
Proof. This is immediate from the pasting law of pullback squares applied to the following commutative diagram:
Indeed, the bottom square is a pullback square by assumption on \(g\), while the top square is clearly a pullback square. □
Lemma 1.6.26. Consider a commutative triangle
Agda Left cancellation of embeddings
compose
Derivation, checked
compose : IsEmbedding f → IsEmbedding (g ∘ f)
Proof / implementation
compose ef = embedding-from-projection-isEquiv (g ∘ f) (equiv-cancel-right N.flatten pullback₁ N.flatten-isEquiv (equiv-transport ((pullback-factor-β₁ N.flat-cone) ⁻¹) (embedding-projection-isEquiv f ef)))
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.Section06.Embeddings where
module _ {Γ : Context} where
module LeftCancellation {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) (eg : IsEmbedding g) wherecancel
Derivation, checked
cancel : IsEmbedding (g ∘ f) → IsEmbedding f
Proof / implementation
cancel egf = embedding-from-projection-isEquiv f (equiv-transport (pullback-factor-β₁ N.flat-cone) (equiv-compose N.flatten pullback₁ N.flatten-isEquiv (embedding-projection-isEquiv (g ∘ f) egf)))
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.Section06.Embeddings where
module _ {Γ : Context} where
module LeftCancellation {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) (eg : IsEmbedding g) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
of functors. If \(g\) is an embedding, then \(f\) is an embedding if and only if \(gf\) is an embedding.
Proof
Proof. Consider the following commutative diagram:
Since \(g\) is an embedding, the right square is a pullback square by Lemma 1.6.25. It follows from the pasting law of pullback squares, Lemma 1.6.11, that the left square is cartesian if and only if the outer rectangle is cartesian, proving the claim. □
Corollary 1.6.27. Consider a commutative diagram
Agda An embedding through a pullback
factor-isEmbedding
Derivation, checked
factor-isEmbedding : IsEmbedding (Cone.right s) → IsEmbedding (pullback-factor s)
Proof / implementation
factor-isEmbedding eu = LeftCancellation.cancel (pullback-factor s) pullback₂ projection (embedding-cong ((pullback-factor-β₂ s) ⁻¹) eu)
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.Section06.Embeddings where
module _ {Γ : Context} where
module RelativeEmbedding {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g T) (ef : IsEmbedding f) whereright-isEmbedding
Derivation, checked
right-isEmbedding : IsEmbedding (pullback-factor s) → IsEmbedding (Cone.right s)
Proof / implementation
right-isEmbedding eh = embedding-cong (pullback-factor-β₂ s) (LeftCancellation.compose (pullback-factor s) pullback₂ projection eh)
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.Section06.Embeddings where
module _ {Γ : Context} where
module RelativeEmbedding {C D E T : CAT Γ} {f : MAP C E} {g : MAP D E}
(s : Cone f g T) (ef : IsEmbedding f) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
of functors such that \(v\) is an embedding. Then \(u\) is an embedding if and only if the induced map \((f,u)\colon A \to B \times _D C\) is an embedding.
Proof
Lemma 1.6.28. Consider a commutative diagram
Agda Cancellation of pullback squares with embeddings
top-isPullback
Derivation, checked
top-isPullback : IsPullback top
Proof / implementation
top-isPullback = embedding-with-section top-factor top-factor-isEmbedding chosen-section
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.Section06.PullbackCancellation where
module _ {Γ : Context} where
module Cancellation {C D E D′ E′ C′ : CAT Γ}
(f : MAP C D) (g : MAP D E) (w : MAP E′ E)
(bottom : Cone g w D′) (top : Cone f (Cone.left bottom) C′)
(ev : IsEmbedding (Cone.left bottom)) (ew : IsEmbedding w)
(outer-isPullback : IsPullback (PasteCones.paste f g bottom top)) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
If \(v\) and \(w\) are embeddings and the composite square is a pullback square, then also the top square is a pullback square.
Proof
Proof. Consider the following commutative diagram:
Since \(w\) is an embedding, the map \(E' \times _E D \to D\) is an embedding by Lemma 1.6.23. Since \(v\colon D' \to D\) is also an embedding, it thus follows from Lemma 1.6.26 that the map \((g',v)\colon D' \to E' \times _E D\) is an embedding, and thus by Lemma 1.6.25 the top left square is a pullback square. Since the right bottom square and right outer rectangle are pullback squares, so is the top right square by the pasting law Lemma 1.6.11. Another instance of Lemma 1.6.11 shows that the outer rectangle is a pullback square, as desired. □
Supplementary notes
- Restricting and pasting cone diagrams AI-generated
- Fiber squares and diagonal squares AI-generated