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.8 Pushout squares
Using mapping animae, we may dualize the definition of a pullback square of categories:
Definition 1.8.1 (Pushout square). A commutative square of categories
Agda Pushout squares
IsPushout
Definition, checked
IsPushout : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} → Square l r → Set (c ⊔ m)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section08.PushoutSquares 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 square with its commutativity identification
Square
Definition, checked
record Square {A B A′ B′ : CAT Γ} (f : MAP A B) (f′ : MAP A′ B′) : Set m where constructor square field source-map : MAP A A′ target-map : MAP B B′ cell : (f′ ∘ source-map) =₁ (target-map ∘ 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.Section03.Squares where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
is called a pushout square (or cocartesian) if, for every category \(E\), the induced square
Agda The pushout condition
IsPushout
Definition, checked
IsPushout : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} → Square l r → Set (c ⊔ m)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section08.PushoutSquares 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 induced square of mapping animae
mappingOut
Definition, checked
mappingOut : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} (s : Square l r) (E : CAT Γ) → Cone (mapPre {D = E} (Square.source-map s)) (mapPre l) (Map D E)
Proof / implementation
mappingOut {l = l} {r} s E = record { left = mapPre r ; right = mapPre (Square.target-map s) ; match = (mapPre-comp l (Square.target-map s)) ⁻¹ ∙ (mapPre⁼ (Square.cell s) ∙ mapPre-comp (Square.source-map s) r) }
Enclosing interface 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.Section08.PushoutSquares 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 Every mapping-out square is a pullback
IsPushout
Definition, checked
IsPushout : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} → Square l r → Set (c ⊔ m)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section08.PushoutSquares where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Remark 1.8.2. We do not assume in the present metatheory that arbitrary pushouts of categories exist. We do not need this as a metatheoretic axiom, although such pushouts exist in all intended models of our theory. We will eventually prove that the synthetic category \(\Cat \) of small synthetic categories admits small colimits, which in particular provides pushouts of small categories.
Proposition 1.8.3. A commutative square of categories
Agda The functor-category criterion for pushouts
pushout→functor-criterion
Derivation, checked
pushout→functor-criterion : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} (s : Square l r) → IsPushout s → FunctorCriterion s
Proof / implementation
pushout→functor-criterion s hyp E = FunctorCriterionForward.comparison-isPullback s hyp E -- No anima hypothesis on P, and both directions use the same functorOut. -- Direct imports additionally: ProductConstructions.swap/swap-swap, -- Currying.reflect, native ordinary/transposed evaluation/recovery modules.
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion where
module _ {Γ : Context} wherefunctor-criterion→pushout
Derivation, checked
functor-criterion→pushout : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} (s : Square l r) → FunctorCriterion s → IsPushout s
Proof / implementation
functor-criterion→pushout s hyp E = FunctorCriterionConverse.comparison-isPullback s hyp E -- Full forward criterion, intended after OrdinaryPushout and concrete adapters.
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion where
module _ {Γ : Context} whereAbout this correspondence
Both implications use the same specified functor-category cone, constructed from evaluation of the actual product square. Agreement with the historical compositor-based matching is not 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 pushout square if and only if, for every category \(E\), the induced square
Agda The induced square of functor categories
functorOut
Definition, checked
functorOut : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} (s : Square l r) (E : CAT Γ) → Cone (funPre {D = E} (Square.source-map s)) (funPre l) (Fun D E)
Proof / implementation
functorOut s E = DirectCurriedFunctorSquare.value s E
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion 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 Pullback condition on the functor-category squares
FunctorCriterion
Definition, checked
FunctorCriterion : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} → Square l r → Set (c ⊔ m)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion 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. For any category \(T\), the commutative square
is equivalent to the commutative square
Agda Uncurrying the tested functor-category square
identification
Derivation, checked
identification : CoconeIdentification₁ source target
Proof / implementation
identification = Calculation.comparison
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion where
module _ {Γ : Context} where
module NativeParameterizedSquareEvaluation {P A B C D E : CAT Γ} {l : MAP A C} {r : MAP B D}
(s : Square l r) (h : MAP P (Fun D E)) whereAbout this correspondence
The current proof uses native evaluation of the actual product square with its complete specified matching. This is a related square-comparison result, not a literal implementation of the older uncurrying or transposition step. Agreement with the historical compositor-based matching is not 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.
which in turn is equivalent to the square
Agda Moving the parameter into the target functor category
identification
Derivation, checked
identification : CoconeIdentification₁ source target
Proof / implementation
identification = Calculation.comparison
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion where
module _ {Γ : Context} where
module NativeParameterizedSquareEvaluation {P A B C D E : CAT Γ} {l : MAP A C} {r : MAP B D}
(s : Square l r) (h : MAP P (Fun D E)) whereAbout this correspondence
The current proof uses native evaluation of the actual product square with its complete specified matching. This is a related square-comparison result, not a literal implementation of the older uncurrying or transposition step. Agreement with the historical compositor-based matching is not 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.
The latter is a pullback square for all \(T\) and \(E\) if and only if it is so for all \(E\) in the special case where \(T=*\) since there is a canonical equivalence \(E\iso \Fun (*,E)\). On the other hand, the first square is a pullback square for all \(T\) if and only if
Agda The canonical equivalence with functors from the point
funOneEvaluation-isEquiv
Derivation, checked
funOneEvaluation-isEquiv : (D : CAT Γ) → IsEquiv (funOneEvaluation D)
Proof / implementation
funOneEvaluation-isEquiv D = record { inverse = funOneInverse D ; left-inverse-law = (funOneInverse-evaluation D) ⁻¹ ; right-inverse-law = (funOneEvaluation-inverse 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.Section07.FunctorProperties 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. This proves the proposition. □
Agda The two implications of the criterion
pushout→functor-criterion
Derivation, checked
pushout→functor-criterion : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} (s : Square l r) → IsPushout s → FunctorCriterion s
Proof / implementation
pushout→functor-criterion s hyp E = FunctorCriterionForward.comparison-isPullback s hyp E -- No anima hypothesis on P, and both directions use the same functorOut. -- Direct imports additionally: ProductConstructions.swap/swap-swap, -- Currying.reflect, native ordinary/transposed evaluation/recovery modules.
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion where
module _ {Γ : Context} wherefunctor-criterion→pushout
Derivation, checked
functor-criterion→pushout : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D} (s : Square l r) → FunctorCriterion s → IsPushout s
Proof / implementation
functor-criterion→pushout s hyp E = FunctorCriterionConverse.comparison-isPullback s hyp E -- Full forward criterion, intended after OrdinaryPushout and concrete adapters.
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion 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.
Lemma 1.8.4 (Pasting lemma for pushout squares). Consider a commutative diagram
Agda Pasting and cancellation of pushout squares
paste-isPushout
Derivation, checked
paste-isPushout : IsPushout R → IsPushout (comp-square R L)
Proof / implementation
paste-isPushout e E = At.preserve E (e 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.Section08.PushoutPasting where
module _ {Γ : Context} {A1 A2 A3 B1 B2 B3 : CAT Γ}
{f1 : MAP A1 B1} {f2 : MAP A2 B2} {f3 : MAP A3 B3}
(L : Square f1 f2) (R : Square f2 f3) where
module DirectPushoutPasting (left-isPushout : IsPushout L) whereunpaste-isPushout
Derivation, checked
unpaste-isPushout : IsPushout (comp-square R L) → IsPushout R
Proof / implementation
unpaste-isPushout e E = At.reflect E (e 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.Section08.PushoutPasting where
module _ {Γ : Context} {A1 A2 A3 B1 B2 B3 : CAT Γ}
{f1 : MAP A1 B1} {f2 : MAP A2 B2} {f3 : MAP A3 B3}
(L : Square f1 f2) (R : Square f2 f3) where
module DirectPushoutPasting (left-isPushout : IsPushout L) 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 the left-hand square is a pushout square, then the right-hand square is a pushout square if and only if the outer rectangle is a pushout square.
Agda The specified outer rectangle
comp-square
Definition, checked
comp-square : {A B A′ B′ A″ B″ : CAT Γ} {f : MAP A B} {f′ : MAP A′ B′} {f″ : MAP A″ B″} → Square f′ f″ → Square f f′ → Square f f″
Proof / implementation
comp-square {f = f} {f′} {f″} Q P = square (source-map Q ∘ source-map P) (target-map Q ∘ target-map P) ((comp-assoc f (target-map P) (target-map Q)) ⁻¹ ∙ ((target-map Q ◁ cell P) ∙ (comp-assoc (source-map P) f′ (target-map Q) ∙ ((cell Q ▷ source-map P) ∙ (comp-assoc (source-map P) (source-map Q) f″) ⁻¹)))) where open 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.Section03.Squares where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. This follows immediately by applying Lemma 1.6.11 to the commutative diagrams
for each \(E\). □
Supplementary notes
- Mapping out of pasted squares AI-generated