Read the Agda code alongside the book.Click dotted-underlined prose to read its Agda code alongside the book. Browse all code.
2.6 Exercises
Exercise 2.6.1. Let \(C_0\) and \(C_1\) be categories and consider morphisms \(f_0\colon x_0 \to y_0\) and \(g_0\colon y_0 \to z_0\) in \(C_0\) and morphisms \(f_1\colon x_1 \to y_1\) and \(g_1\colon y_1 \to z_1\) in \(C_1\). Show that the composite \((g_0,g_1) \circ (f_0,f_1)\colon (x_0,x_1) \to (z_0,z_1)\) in \(C_0 \times C_1\) is given by \((g_0 \circ f_0, g_1 \circ f_1)\).
Agda Composition in a product
product-composition
Derivation, checked
product-composition : MorphismFamilyIdentification One chosen-product-composite paired-component-composite
Proof / implementation
product-composition = product-family-reflect {alpha = chosen-product-composite} {beta = paired-component-composite} first-projected-product-composition second-projected-product-composition
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.ProductMorphismFamilies where
module ProductComposition {Γ : Context} (C D : CAT Γ)
(product-segal : IsEquiv (short-edges (C × D)))
(left-segal : IsEquiv (short-edges C)) (right-segal : IsEquiv (short-edges D)) where
module _ {P : CAT Γ} {x₁ y₁ z₁ : MAP P C} {x₂ y₂ z₂ : MAP P D}
(beta₁ : MorphismFamily y₁ z₁) (alpha₁ : MorphismFamily x₁ y₁)
(beta₂ : MorphismFamily y₂ z₂) (alpha₂ : MorphismFamily x₂ y₂) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Exercise 2.6.2. Let \(f\colon x\to y\) be a morphism in a category \(C\). Prove that the following assertions are equivalent:
Agda The elementary Yoneda criterion
isomorphism-postcompose
Definition, checked
isomorphism-postcompose : IsIsomorphism → PostcompositionEquivalences
Proof / implementation
isomorphism-postcompose given = InvertibleHom.postcomposition-isEquiv C x y point (point-lift given)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section06.HomIsomorphisms where
module Criterion {Γ : Context} {C : CAT Γ} {x y : MAP One C} (f : Morphism x y) whereisomorphism-precompose
Definition, checked
isomorphism-precompose : IsIsomorphism → PrecompositionEquivalences
Proof / implementation
isomorphism-precompose given = InvertibleHom.precomposition-isEquiv C x y point (point-lift given)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section06.HomIsomorphisms where
module Criterion {Γ : Context} {C : CAT Γ} {x y : MAP One C} (f : Morphism x y) wherepostcompose-isomorphism
Definition, checked
postcompose-isomorphism : PostcompositionEquivalences → IsIsomorphism
Proof / implementation
postcompose-isomorphism tests = postcompose-detects-isomorphism (tests x) (tests y)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section06.HomIsomorphisms where
module Criterion {Γ : Context} {C : CAT Γ} {x y : MAP One C} (f : Morphism x y) whereprecompose-isomorphism
Definition, checked
precompose-isomorphism : PrecompositionEquivalences → IsIsomorphism
Proof / implementation
precompose-isomorphism tests = precompose-detects-isomorphism (tests x) (tests y)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section06.HomIsomorphisms where
module Criterion {Γ : Context} {C : CAT Γ} {x y : MAP One C} (f : Morphism x y) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
- \(f\) is an isomorphism;
- for any object \(c\) of \(C\), \(f\) induces an equivalence of the form \[ f\circ -\colon C(c,x)\iso C(c,y)\, ; \]
- for any object \(c\) of \(C\), \(f\) induces an equivalence of the form \[ -\circ f\colon C(y,c)\iso C(x,c)\, . \]
Supplementary notes
- Hom expressions and restriction AI-generated