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.3 Equivalences of categories
We now develop some basic properties of the equivalences introduced in Definition 1.1.5.
Proposition 1.3.1. Let \(f\colon C\to D\) be a functor. For \(f\) to be an equivalence, it suffices that the following properties hold for every category \(T\):
Agda Equivalences as naive bijections
factor-and-reflection-isEquiv
Derivation, checked
factor-and-reflection-isEquiv : {C D : CAT Γ} (f : MAP C D) → ((T : CAT Γ) → ReflectsIdentifications f T) → ({T : CAT Γ} (d : MAP T D) → Factorization f d) → IsEquiv f
Proof / implementation
factor-and-reflection-isEquiv {C} {D} f reflect factors = record { inverse = g ; left-inverse-law = (reflect C (g ∘ f) (id C) image) ⁻¹ ; right-inverse-law = β ⁻¹ } where chosen : Factorization f (id D) chosen = factors (id D) g : MAP D C g = factor chosen β : (f ∘ g) =₁ id D β = triangle chosen image : (f ∘ (g ∘ f)) =₁ (f ∘ id C) image = (comp-unitʳ f) ⁻¹ ∙ (comp-unitˡ f ∙ ((β ▷ f) ∙ (comp-assoc f g f) ⁻¹))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Factorizations 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.
- (1)
-
For \(a,b\colon T\to C\), any identification \(fa= fb\) gives an identification \(a= b\).
Agda Equivalences as naive bijections step 1
factor-and-reflection-isEquivDerivation, checked
factor-and-reflection-isEquiv : {C D : CAT Γ} (f : MAP C D) → ((T : CAT Γ) → ReflectsIdentifications f T) → ({T : CAT Γ} (d : MAP T D) → Factorization f d) → IsEquiv f
Proof / implementation
factor-and-reflection-isEquiv {C} {D} f reflect factors = record { inverse = g ; left-inverse-law = (reflect C (g ∘ f) (id C) image) ⁻¹ ; right-inverse-law = β ⁻¹ } where chosen : Factorization f (id D) chosen = factors (id D) g : MAP D C g = factor chosen β : (f ∘ g) =₁ id D β = triangle chosen image : (f ∘ (g ∘ f)) =₁ (f ∘ id C) image = (comp-unitʳ f) ⁻¹ ∙ (comp-unitˡ f ∙ ((β ▷ f) ∙ (comp-assoc f g f) ⁻¹))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section03.Factorizations 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.
- (2)
-
For any \(d\colon T\to D\), there is a functor \(c\colon T\to C\) equipped with an identification \(fc= d\).
Agda Equivalences as naive bijections step 2
factor-and-reflection-isEquivDerivation, checked
factor-and-reflection-isEquiv : {C D : CAT Γ} (f : MAP C D) → ((T : CAT Γ) → ReflectsIdentifications f T) → ({T : CAT Γ} (d : MAP T D) → Factorization f d) → IsEquiv f
Proof / implementation
factor-and-reflection-isEquiv {C} {D} f reflect factors = record { inverse = g ; left-inverse-law = (reflect C (g ∘ f) (id C) image) ⁻¹ ; right-inverse-law = β ⁻¹ } where chosen : Factorization f (id D) chosen = factors (id D) g : MAP D C g = factor chosen β : (f ∘ g) =₁ id D β = triangle chosen image : (f ∘ (g ∘ f)) =₁ (f ∘ id C) image = (comp-unitʳ f) ⁻¹ ∙ (comp-unitˡ f ∙ ((β ▷ f) ∙ (comp-assoc f g f) ⁻¹))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section03.Factorizations 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.
Proof
Proof. Apply the second property to \(\id _D\) to obtain \(g\colon D\to C\) and \(fg=\id _D\). The associator, this identification, and the unitors identify \(f(gf)\) with \(f\id _C\). The first property, with \(T=C\), gives \(gf=\id _C\). □
Agda Equivalences as naive bijections step 3
factor-and-reflection-isEquiv
Derivation, checked
factor-and-reflection-isEquiv : {C D : CAT Γ} (f : MAP C D) → ((T : CAT Γ) → ReflectsIdentifications f T) → ({T : CAT Γ} (d : MAP T D) → Factorization f d) → IsEquiv f
Proof / implementation
factor-and-reflection-isEquiv {C} {D} f reflect factors = record { inverse = g ; left-inverse-law = (reflect C (g ∘ f) (id C) image) ⁻¹ ; right-inverse-law = β ⁻¹ } where chosen : Factorization f (id D) chosen = factors (id D) g : MAP D C g = factor chosen β : (f ∘ g) =₁ id D β = triangle chosen image : (f ∘ (g ∘ f)) =₁ (f ∘ id C) image = (comp-unitʳ f) ⁻¹ ∙ (comp-unitˡ f ∙ ((β ▷ f) ∙ (comp-assoc f g f) ⁻¹))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Factorizations 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.
Agda Equivalences as naive bijections step 4
factor-and-reflection-isEquiv
Derivation, checked
factor-and-reflection-isEquiv : {C D : CAT Γ} (f : MAP C D) → ((T : CAT Γ) → ReflectsIdentifications f T) → ({T : CAT Γ} (d : MAP T D) → Factorization f d) → IsEquiv f
Proof / implementation
factor-and-reflection-isEquiv {C} {D} f reflect factors = record { inverse = g ; left-inverse-law = (reflect C (g ∘ f) (id C) image) ⁻¹ ; right-inverse-law = β ⁻¹ } where chosen : Factorization f (id D) chosen = factors (id D) g : MAP D C g = factor chosen β : (f ∘ g) =₁ id D β = triangle chosen image : (f ∘ (g ∘ f)) =₁ (f ∘ id C) image = (comp-unitʳ f) ⁻¹ ∙ (comp-unitˡ f ∙ ((β ▷ f) ∙ (comp-assoc f g f) ⁻¹))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Factorizations 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.
Agda Equivalences as naive bijections step 5
factor-and-reflection-isEquiv
Derivation, checked
factor-and-reflection-isEquiv : {C D : CAT Γ} (f : MAP C D) → ((T : CAT Γ) → ReflectsIdentifications f T) → ({T : CAT Γ} (d : MAP T D) → Factorization f d) → IsEquiv f
Proof / implementation
factor-and-reflection-isEquiv {C} {D} f reflect factors = record { inverse = g ; left-inverse-law = (reflect C (g ∘ f) (id C) image) ⁻¹ ; right-inverse-law = β ⁻¹ } where chosen : Factorization f (id D) chosen = factors (id D) g : MAP D C g = factor chosen β : (f ∘ g) =₁ id D β = triangle chosen image : (f ∘ (g ∘ f)) =₁ (f ∘ id C) image = (comp-unitʳ f) ⁻¹ ∙ (comp-unitˡ f ∙ ((β ▷ f) ∙ (comp-assoc f g f) ⁻¹))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Factorizations 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.
Definition 1.3.2 (Section/retraction). Consider a functor \(f\colon C \to D\). A section of \(f\) is a functor \(s\colon D \to C\) equipped with an identification \(fs = \id _D\). A retraction of \(f\) is a functor \(r\colon D \to C\) equipped with an identification \(\id _C = rf\).
Agda Section
Section
Definition, checked
record Section {C D : CAT Γ} (f : MAP C D) : Set m where field section : MAP D C section-law : (id D) =₁ (f ∘ 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.Section03.Equivalences where
module _ {Γ : Context} whereRetraction
Definition, checked
record Retraction {C D : CAT Γ} (f : MAP C D) : Set m where field retraction : MAP D C retraction-law : (id C) =₁ (retraction ∘ 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.Equivalences 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 Section step 1
Section
Definition, checked
record Section {C D : CAT Γ} (f : MAP C D) : Set m where field section : MAP D C section-law : (id D) =₁ (f ∘ 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.Section03.Equivalences where
module _ {Γ : Context} whereRetraction
Definition, checked
record Retraction {C D : CAT Γ} (f : MAP C D) : Set m where field retraction : MAP D C retraction-law : (id C) =₁ (retraction ∘ 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.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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.3.3. A functor \(f\colon C \to D\) is an equivalence if and only if it admits both a section \(s\) and a retraction \(r\). In this case there exists an identification \(s = r\) and \(s\) is an inverse of \(f\).
Agda Inverse on both sides implies equivalence
section-retraction-isEquiv
Derivation, checked
section-retraction-isEquiv : {C D : CAT Γ} {f : MAP C D} → Section f → Retraction f → IsEquiv f
Proof / implementation
section-retraction-isEquiv {f = f} s r = record { inverse = Section.section s ; left-inverse-law = ((section-retraction-equal s r) ⁻¹ ▷ f) ∙ Retraction.retraction-law r ; right-inverse-law = Section.section-law 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-section
Derivation, checked
equiv-section : {C D : CAT Γ} {f : MAP C D} → IsEquiv f → Section f
Proof / implementation
equiv-section e = record { section = IsEquiv.inverse e ; section-law = IsEquiv.right-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereequiv-retraction
Derivation, checked
equiv-retraction : {C D : CAT Γ} {f : MAP C D} → IsEquiv f → Retraction f
Proof / implementation
equiv-retraction e = record { retraction = IsEquiv.inverse e ; retraction-law = IsEquiv.left-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} wheresection-retraction-equal
Derivation, checked
section-retraction-equal : {C D : CAT Γ} {f : MAP C D} (s : Section f) (r : Retraction f) → (Section.section s) =₁ (Retraction.retraction r)
Proof / implementation
section-retraction-equal {f = f} s r = let u = Section.section s v = Retraction.retraction r in comp-unitʳ v ∙ ((v ◁ (Section.section-law s) ⁻¹) ∙ (comp-assoc u f v ∙ ((Retraction.retraction-law r ▷ u) ∙ (comp-unitˡ u) ⁻¹)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences 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. If \(f\) is an equivalence with inverse \(g\colon D \to C\), then clearly \(g\) is both a section and a retraction of \(f\). Conversely, given a section \(s\colon D \to C\), \(fs = \id _D\) and a retraction \(r\colon D \to C\), \(\id _C = rf\), we obtain an identification \(s = r\) by composing the following chain of identifications: Agda\[ s = \id _C \circ s = (r \circ f) \circ s = r \circ (f \circ s) = r \circ \id _D = r. \] It follows that \(f\) is an equivalence with inverse \(s\), since there are identifications \(fs = \id _{D}\) and \(sf = rf = \id _{C}\). □
Agda Inverse on both sides implies equivalence step 1
section-retraction-isEquiv
Derivation, checked
section-retraction-isEquiv : {C D : CAT Γ} {f : MAP C D} → Section f → Retraction f → IsEquiv f
Proof / implementation
section-retraction-isEquiv {f = f} s r = record { inverse = Section.section s ; left-inverse-law = ((section-retraction-equal s r) ⁻¹ ▷ f) ∙ Retraction.retraction-law r ; right-inverse-law = Section.section-law 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-section
Derivation, checked
equiv-section : {C D : CAT Γ} {f : MAP C D} → IsEquiv f → Section f
Proof / implementation
equiv-section e = record { section = IsEquiv.inverse e ; section-law = IsEquiv.right-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereequiv-retraction
Derivation, checked
equiv-retraction : {C D : CAT Γ} {f : MAP C D} → IsEquiv f → Retraction f
Proof / implementation
equiv-retraction e = record { retraction = IsEquiv.inverse e ; retraction-law = IsEquiv.left-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} wheresection-retraction-equal
Derivation, checked
section-retraction-equal : {C D : CAT Γ} {f : MAP C D} (s : Section f) (r : Retraction f) → (Section.section s) =₁ (Retraction.retraction r)
Proof / implementation
section-retraction-equal {f = f} s r = let u = Section.section s v = Retraction.retraction r in comp-unitʳ v ∙ ((v ◁ (Section.section-law s) ⁻¹) ∙ (comp-assoc u f v ∙ ((Retraction.retraction-law r ▷ u) ∙ (comp-unitˡ u) ⁻¹)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Inverse on both sides implies equivalence step 2
section-retraction-isEquiv
Derivation, checked
section-retraction-isEquiv : {C D : CAT Γ} {f : MAP C D} → Section f → Retraction f → IsEquiv f
Proof / implementation
section-retraction-isEquiv {f = f} s r = record { inverse = Section.section s ; left-inverse-law = ((section-retraction-equal s r) ⁻¹ ▷ f) ∙ Retraction.retraction-law r ; right-inverse-law = Section.section-law 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-section
Derivation, checked
equiv-section : {C D : CAT Γ} {f : MAP C D} → IsEquiv f → Section f
Proof / implementation
equiv-section e = record { section = IsEquiv.inverse e ; section-law = IsEquiv.right-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereequiv-retraction
Derivation, checked
equiv-retraction : {C D : CAT Γ} {f : MAP C D} → IsEquiv f → Retraction f
Proof / implementation
equiv-retraction e = record { retraction = IsEquiv.inverse e ; retraction-law = IsEquiv.left-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} wheresection-retraction-equal
Derivation, checked
section-retraction-equal : {C D : CAT Γ} {f : MAP C D} (s : Section f) (r : Retraction f) → (Section.section s) =₁ (Retraction.retraction r)
Proof / implementation
section-retraction-equal {f = f} s r = let u = Section.section s v = Retraction.retraction r in comp-unitʳ v ∙ ((v ◁ (Section.section-law s) ⁻¹) ∙ (comp-assoc u f v ∙ ((Retraction.retraction-law r ▷ u) ∙ (comp-unitˡ u) ⁻¹)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Inverse on both sides implies equivalence step 3
section-retraction-isEquiv
Derivation, checked
section-retraction-isEquiv : {C D : CAT Γ} {f : MAP C D} → Section f → Retraction f → IsEquiv f
Proof / implementation
section-retraction-isEquiv {f = f} s r = record { inverse = Section.section s ; left-inverse-law = ((section-retraction-equal s r) ⁻¹ ▷ f) ∙ Retraction.retraction-law r ; right-inverse-law = Section.section-law 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-section
Derivation, checked
equiv-section : {C D : CAT Γ} {f : MAP C D} → IsEquiv f → Section f
Proof / implementation
equiv-section e = record { section = IsEquiv.inverse e ; section-law = IsEquiv.right-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereequiv-retraction
Derivation, checked
equiv-retraction : {C D : CAT Γ} {f : MAP C D} → IsEquiv f → Retraction f
Proof / implementation
equiv-retraction e = record { retraction = IsEquiv.inverse e ; retraction-law = IsEquiv.left-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} wheresection-retraction-equal
Derivation, checked
section-retraction-equal : {C D : CAT Γ} {f : MAP C D} (s : Section f) (r : Retraction f) → (Section.section s) =₁ (Retraction.retraction r)
Proof / implementation
section-retraction-equal {f = f} s r = let u = Section.section s v = Retraction.retraction r in comp-unitʳ v ∙ ((v ◁ (Section.section-law s) ⁻¹) ∙ (comp-assoc u f v ∙ ((Retraction.retraction-law r ▷ u) ∙ (comp-unitˡ u) ⁻¹)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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.3.4. Any two inverses \(g\) and \(h\) of an equivalence \(f\) are identified. □
Agda Uniqueness of equivalence inverses
inverse-unique
Derivation, checked
inverse-unique : {C D : CAT Γ} {f : MAP C D} (e e′ : IsEquiv f) → (IsEquiv.inverse e) =₁ (IsEquiv.inverse e′)
Proof / implementation
inverse-unique e e′ = section-retraction-equal (equiv-section e) (equiv-retraction 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.Section03.Equivalences 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.3.5. If \(f\colon C \to D\) and \(f'\colon D \to E\) are equivalences with inverses \(g\colon D \to C\) and \(g'\colon E \to D\), then also the composite \(f'f\colon C \to E\) is an equivalence with inverse \(gg'\colon E \to C\).
Agda Composite of equivalences
equiv-compose
Derivation, checked
equiv-compose : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv g → IsEquiv (g ∘ f)
Proof / implementation
equiv-compose {C} {D} {E} f g ef eg = let u : MAP D C u = IsEquiv.inverse ef v : MAP E D v = IsEquiv.inverse eg --! begin equiv-compose-left left : ((u ∘ v) ∘ (g ∘ f)) =₁ (id C) left = (IsEquiv.left-inverse-law ef) ⁻¹ ∙ ((u ◁ comp-unitˡ f) ∙ ((u ◁ ((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f)) ∙ ((u ◁ (comp-assoc f g v) ⁻¹) ∙ comp-assoc (g ∘ f) v u))) --! end equiv-compose-left --! begin equiv-compose-right right : ((g ∘ f) ∘ (u ∘ v)) =₁ (id E) right = (IsEquiv.right-inverse-law eg) ⁻¹ ∙ ((g ◁ comp-unitˡ v) ∙ ((g ◁ ((IsEquiv.right-inverse-law ef) ⁻¹ ▷ v)) ∙ ((g ◁ (comp-assoc v u f) ⁻¹) ∙ comp-assoc (u ∘ v) f g))) --! end equiv-compose-right in record { inverse = u ∘ v ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Equivalences 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 have \(gg'f'f = g\id _{D}f = gf = \id _{C}\) and \(f'fgg' = f'\id _{D}g'= f'g' = \id _{E}\). □
Agda Composite of equivalences step 1
equiv-compose
Derivation, checked
equiv-compose : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv g → IsEquiv (g ∘ f)
Proof / implementation
equiv-compose {C} {D} {E} f g ef eg = let u : MAP D C u = IsEquiv.inverse ef v : MAP E D v = IsEquiv.inverse eg --! begin equiv-compose-left left : ((u ∘ v) ∘ (g ∘ f)) =₁ (id C) left = (IsEquiv.left-inverse-law ef) ⁻¹ ∙ ((u ◁ comp-unitˡ f) ∙ ((u ◁ ((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f)) ∙ ((u ◁ (comp-assoc f g v) ⁻¹) ∙ comp-assoc (g ∘ f) v u))) --! end equiv-compose-left --! begin equiv-compose-right right : ((g ∘ f) ∘ (u ∘ v)) =₁ (id E) right = (IsEquiv.right-inverse-law eg) ⁻¹ ∙ ((g ◁ comp-unitˡ v) ∙ ((g ◁ ((IsEquiv.right-inverse-law ef) ⁻¹ ▷ v)) ∙ ((g ◁ (comp-assoc v u f) ⁻¹) ∙ comp-assoc (u ∘ v) f g))) --! end equiv-compose-right in record { inverse = u ∘ v ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Composite of equivalences step 2
equiv-compose
Derivation, checked
equiv-compose : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv g → IsEquiv (g ∘ f)
Proof / implementation
equiv-compose {C} {D} {E} f g ef eg = let u : MAP D C u = IsEquiv.inverse ef v : MAP E D v = IsEquiv.inverse eg --! begin equiv-compose-left left : ((u ∘ v) ∘ (g ∘ f)) =₁ (id C) left = (IsEquiv.left-inverse-law ef) ⁻¹ ∙ ((u ◁ comp-unitˡ f) ∙ ((u ◁ ((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f)) ∙ ((u ◁ (comp-assoc f g v) ⁻¹) ∙ comp-assoc (g ∘ f) v u))) --! end equiv-compose-left --! begin equiv-compose-right right : ((g ∘ f) ∘ (u ∘ v)) =₁ (id E) right = (IsEquiv.right-inverse-law eg) ⁻¹ ∙ ((g ◁ comp-unitˡ v) ∙ ((g ◁ ((IsEquiv.right-inverse-law ef) ⁻¹ ▷ v)) ∙ ((g ◁ (comp-assoc v u f) ⁻¹) ∙ comp-assoc (u ∘ v) f g))) --! end equiv-compose-right in record { inverse = u ∘ v ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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.3.6. Equivalences of categories satisfy the 2-out-of-3 property: given functors \(f\colon C \to D\) and \(g\colon D \to E\), if two of the three functors \(f\), \(g\) and \(gf\) are equivalences, then so is the third.
Agda Equivalences satisfy 2 out of 3
equiv-compose
Derivation, checked
equiv-compose : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv g → IsEquiv (g ∘ f)
Proof / implementation
equiv-compose {C} {D} {E} f g ef eg = let u : MAP D C u = IsEquiv.inverse ef v : MAP E D v = IsEquiv.inverse eg --! begin equiv-compose-left left : ((u ∘ v) ∘ (g ∘ f)) =₁ (id C) left = (IsEquiv.left-inverse-law ef) ⁻¹ ∙ ((u ◁ comp-unitˡ f) ∙ ((u ◁ ((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f)) ∙ ((u ◁ (comp-assoc f g v) ⁻¹) ∙ comp-assoc (g ∘ f) v u))) --! end equiv-compose-left --! begin equiv-compose-right right : ((g ∘ f) ∘ (u ∘ v)) =₁ (id E) right = (IsEquiv.right-inverse-law eg) ⁻¹ ∙ ((g ◁ comp-unitˡ v) ∙ ((g ◁ ((IsEquiv.right-inverse-law ef) ⁻¹ ▷ v)) ∙ ((g ◁ (comp-assoc v u f) ⁻¹) ∙ comp-assoc (u ∘ v) f g))) --! end equiv-compose-right in record { inverse = u ∘ v ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-cancel-right
Derivation, checked
equiv-cancel-right : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv (g ∘ f) → IsEquiv g
Proof / implementation
equiv-cancel-right f g ef egf = let u = IsEquiv.inverse ef cancel-f : ((g ∘ f) ∘ u) =₁ g cancel-f = comp-unitʳ g ∙ ((g ◁ (IsEquiv.right-inverse-law ef) ⁻¹) ∙ comp-assoc u f g) in equiv-transport cancel-f (equiv-compose u (g ∘ f) (equiv-inverse ef) 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-cancel-left
Derivation, checked
equiv-cancel-left : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv g → IsEquiv (g ∘ f) → IsEquiv f
Proof / implementation
equiv-cancel-left f g eg egf = let v = IsEquiv.inverse eg cancel-g : (v ∘ (g ∘ f)) =₁ f cancel-g = comp-unitˡ f ∙ (((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f) ∙ (comp-assoc f g v) ⁻¹) in equiv-transport cancel-g (equiv-compose (g ∘ f) v egf (equiv-inverse 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-transport
Derivation, checked
equiv-transport : {C D : CAT Γ} {f g : MAP C D} → f =₁ g → IsEquiv f → IsEquiv g
Proof / implementation
equiv-transport α e = record { inverse = IsEquiv.inverse e ; left-inverse-law = (IsEquiv.inverse e ◁ α) ∙ IsEquiv.left-inverse-law e ; right-inverse-law = (α ▷ IsEquiv.inverse e) ∙ IsEquiv.right-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences 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. If \(g\) and \(f\) are equivalences, then so is \(gf\) by Lemma 1.3.5. If \(f\) and \(gf\) are equivalences, then we may rewrite \(g\) as the composite \(g = g \circ \id _{D} = g \circ f \circ f^{-1} = gf \circ f^{-1}\), so that \(g\) is the composite of two equivalences and hence itself an equivalence. A similar argument shows that \(f\) is an equivalence whenever \(g\) and \(gf\) are equivalences. □
Agda Equivalences satisfy 2 out of 3 step 1
equiv-compose
Derivation, checked
equiv-compose : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv g → IsEquiv (g ∘ f)
Proof / implementation
equiv-compose {C} {D} {E} f g ef eg = let u : MAP D C u = IsEquiv.inverse ef v : MAP E D v = IsEquiv.inverse eg --! begin equiv-compose-left left : ((u ∘ v) ∘ (g ∘ f)) =₁ (id C) left = (IsEquiv.left-inverse-law ef) ⁻¹ ∙ ((u ◁ comp-unitˡ f) ∙ ((u ◁ ((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f)) ∙ ((u ◁ (comp-assoc f g v) ⁻¹) ∙ comp-assoc (g ∘ f) v u))) --! end equiv-compose-left --! begin equiv-compose-right right : ((g ∘ f) ∘ (u ∘ v)) =₁ (id E) right = (IsEquiv.right-inverse-law eg) ⁻¹ ∙ ((g ◁ comp-unitˡ v) ∙ ((g ◁ ((IsEquiv.right-inverse-law ef) ⁻¹ ▷ v)) ∙ ((g ◁ (comp-assoc v u f) ⁻¹) ∙ comp-assoc (u ∘ v) f g))) --! end equiv-compose-right in record { inverse = u ∘ v ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-cancel-right
Derivation, checked
equiv-cancel-right : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv (g ∘ f) → IsEquiv g
Proof / implementation
equiv-cancel-right f g ef egf = let u = IsEquiv.inverse ef cancel-f : ((g ∘ f) ∘ u) =₁ g cancel-f = comp-unitʳ g ∙ ((g ◁ (IsEquiv.right-inverse-law ef) ⁻¹) ∙ comp-assoc u f g) in equiv-transport cancel-f (equiv-compose u (g ∘ f) (equiv-inverse ef) 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-cancel-left
Derivation, checked
equiv-cancel-left : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv g → IsEquiv (g ∘ f) → IsEquiv f
Proof / implementation
equiv-cancel-left f g eg egf = let v = IsEquiv.inverse eg cancel-g : (v ∘ (g ∘ f)) =₁ f cancel-g = comp-unitˡ f ∙ (((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f) ∙ (comp-assoc f g v) ⁻¹) in equiv-transport cancel-g (equiv-compose (g ∘ f) v egf (equiv-inverse 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-transport
Derivation, checked
equiv-transport : {C D : CAT Γ} {f g : MAP C D} → f =₁ g → IsEquiv f → IsEquiv g
Proof / implementation
equiv-transport α e = record { inverse = IsEquiv.inverse e ; left-inverse-law = (IsEquiv.inverse e ◁ α) ∙ IsEquiv.left-inverse-law e ; right-inverse-law = (α ▷ IsEquiv.inverse e) ∙ IsEquiv.right-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Equivalences satisfy 2 out of 3 step 2
equiv-compose
Derivation, checked
equiv-compose : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv g → IsEquiv (g ∘ f)
Proof / implementation
equiv-compose {C} {D} {E} f g ef eg = let u : MAP D C u = IsEquiv.inverse ef v : MAP E D v = IsEquiv.inverse eg --! begin equiv-compose-left left : ((u ∘ v) ∘ (g ∘ f)) =₁ (id C) left = (IsEquiv.left-inverse-law ef) ⁻¹ ∙ ((u ◁ comp-unitˡ f) ∙ ((u ◁ ((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f)) ∙ ((u ◁ (comp-assoc f g v) ⁻¹) ∙ comp-assoc (g ∘ f) v u))) --! end equiv-compose-left --! begin equiv-compose-right right : ((g ∘ f) ∘ (u ∘ v)) =₁ (id E) right = (IsEquiv.right-inverse-law eg) ⁻¹ ∙ ((g ◁ comp-unitˡ v) ∙ ((g ◁ ((IsEquiv.right-inverse-law ef) ⁻¹ ▷ v)) ∙ ((g ◁ (comp-assoc v u f) ⁻¹) ∙ comp-assoc (u ∘ v) f g))) --! end equiv-compose-right in record { inverse = u ∘ v ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-cancel-right
Derivation, checked
equiv-cancel-right : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv (g ∘ f) → IsEquiv g
Proof / implementation
equiv-cancel-right f g ef egf = let u = IsEquiv.inverse ef cancel-f : ((g ∘ f) ∘ u) =₁ g cancel-f = comp-unitʳ g ∙ ((g ◁ (IsEquiv.right-inverse-law ef) ⁻¹) ∙ comp-assoc u f g) in equiv-transport cancel-f (equiv-compose u (g ∘ f) (equiv-inverse ef) 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-cancel-left
Derivation, checked
equiv-cancel-left : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv g → IsEquiv (g ∘ f) → IsEquiv f
Proof / implementation
equiv-cancel-left f g eg egf = let v = IsEquiv.inverse eg cancel-g : (v ∘ (g ∘ f)) =₁ f cancel-g = comp-unitˡ f ∙ (((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f) ∙ (comp-assoc f g v) ⁻¹) in equiv-transport cancel-g (equiv-compose (g ∘ f) v egf (equiv-inverse 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-transport
Derivation, checked
equiv-transport : {C D : CAT Γ} {f g : MAP C D} → f =₁ g → IsEquiv f → IsEquiv g
Proof / implementation
equiv-transport α e = record { inverse = IsEquiv.inverse e ; left-inverse-law = (IsEquiv.inverse e ◁ α) ∙ IsEquiv.left-inverse-law e ; right-inverse-law = (α ▷ IsEquiv.inverse e) ∙ IsEquiv.right-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Equivalences satisfy 2 out of 3 step 3
equiv-compose
Derivation, checked
equiv-compose : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv g → IsEquiv (g ∘ f)
Proof / implementation
equiv-compose {C} {D} {E} f g ef eg = let u : MAP D C u = IsEquiv.inverse ef v : MAP E D v = IsEquiv.inverse eg --! begin equiv-compose-left left : ((u ∘ v) ∘ (g ∘ f)) =₁ (id C) left = (IsEquiv.left-inverse-law ef) ⁻¹ ∙ ((u ◁ comp-unitˡ f) ∙ ((u ◁ ((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f)) ∙ ((u ◁ (comp-assoc f g v) ⁻¹) ∙ comp-assoc (g ∘ f) v u))) --! end equiv-compose-left --! begin equiv-compose-right right : ((g ∘ f) ∘ (u ∘ v)) =₁ (id E) right = (IsEquiv.right-inverse-law eg) ⁻¹ ∙ ((g ◁ comp-unitˡ v) ∙ ((g ◁ ((IsEquiv.right-inverse-law ef) ⁻¹ ▷ v)) ∙ ((g ◁ (comp-assoc v u f) ⁻¹) ∙ comp-assoc (u ∘ v) f g))) --! end equiv-compose-right in record { inverse = u ∘ v ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-cancel-right
Derivation, checked
equiv-cancel-right : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv f → IsEquiv (g ∘ f) → IsEquiv g
Proof / implementation
equiv-cancel-right f g ef egf = let u = IsEquiv.inverse ef cancel-f : ((g ∘ f) ∘ u) =₁ g cancel-f = comp-unitʳ g ∙ ((g ◁ (IsEquiv.right-inverse-law ef) ⁻¹) ∙ comp-assoc u f g) in equiv-transport cancel-f (equiv-compose u (g ∘ f) (equiv-inverse ef) 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-cancel-left
Derivation, checked
equiv-cancel-left : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → IsEquiv g → IsEquiv (g ∘ f) → IsEquiv f
Proof / implementation
equiv-cancel-left f g eg egf = let v = IsEquiv.inverse eg cancel-g : (v ∘ (g ∘ f)) =₁ f cancel-g = comp-unitˡ f ∙ (((IsEquiv.left-inverse-law eg) ⁻¹ ▷ f) ∙ (comp-assoc f g v) ⁻¹) in equiv-transport cancel-g (equiv-compose (g ∘ f) v egf (equiv-inverse 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.Section03.Equivalences where
module _ {Γ : Context} whereequiv-transport
Derivation, checked
equiv-transport : {C D : CAT Γ} {f g : MAP C D} → f =₁ g → IsEquiv f → IsEquiv g
Proof / implementation
equiv-transport α e = record { inverse = IsEquiv.inverse e ; left-inverse-law = (IsEquiv.inverse e ◁ α) ∙ IsEquiv.left-inverse-law e ; right-inverse-law = (α ▷ IsEquiv.inverse e) ∙ IsEquiv.right-inverse-law e }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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.3.7. Equivalences of categories satisfy the 2-out-of-6 property: given functors \(f\colon C \to D\), \(g\colon D \to E\) and \(h\colon E \to F\) such that \(gf\) and \(hg\) are equivalences, also the functors \(f\), \(g\), \(h\) and \(hgf\) are equivalences.
Agda Two out of six for equivalences
TwoOutOfSix
Definition, checked
record TwoOutOfSix {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) : Set m where field first : IsEquiv f middle : IsEquiv g last : IsEquiv h composite : IsEquiv (h ∘ (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.Section03.Equivalences where
module _ {Γ : Context} wheretwo-out-of-six
Derivation, checked
two-out-of-six : {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) → IsEquiv (g ∘ f) → IsEquiv (h ∘ g) → TwoOutOfSix f g h
Proof / implementation
two-out-of-six f g h egf ehg = --! begin two-out-of-six-inverses let u = IsEquiv.inverse egf v = IsEquiv.inverse ehg --! end two-out-of-six-inverses --! begin two-out-of-six-section s : Section g s = record { section = f ∘ u ; section-law = comp-assoc u f g ∙ IsEquiv.right-inverse-law egf } --! end two-out-of-six-section --! begin two-out-of-six-retraction r : Retraction g r = record { retraction = v ∘ h ; retraction-law = (comp-assoc g h v) ⁻¹ ∙ IsEquiv.left-inverse-law ehg } --! end two-out-of-six-retraction --! begin two-out-of-six-middle eg : IsEquiv g eg = section-retraction-isEquiv s r --! end two-out-of-six-middle --! begin two-out-of-six-conclusion ef = equiv-cancel-left f g eg egf eh = equiv-cancel-right g h eg ehg in record { first = ef ; middle = eg ; last = eh ; composite = equiv-compose (g ∘ f) h egf eh } --! end two-out-of-six-conclusion
Enclosing interface 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.Equivalences 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. Consider the functors \(f' := f \circ (gf)^{-1}\colon E \to D\) and \(h' := (hg)^{-1} \circ h \colon E \to D\). Then there are identifications Agda\[ g \circ f' = g \circ f \circ (gf)^{-1} = gf \circ (gf)^{-1} = \id _{E} \] and Agda\[ h' \circ g = (hg)^{-1} \circ h \circ g = (hg)^{-1} \circ hg = \id _{D}. \] Hence it follows from Lemma 1.3.3 that \(g\) is an equivalence. In light of Lemma 1.3.6, we then get that also \(f\) and \(h\) are equivalences, and then so is \(hgf\). □
Agda Two out of six for equivalences step 1
TwoOutOfSix
Definition, checked
record TwoOutOfSix {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) : Set m where field first : IsEquiv f middle : IsEquiv g last : IsEquiv h composite : IsEquiv (h ∘ (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.Section03.Equivalences where
module _ {Γ : Context} wheretwo-out-of-six
Derivation, checked
two-out-of-six : {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) → IsEquiv (g ∘ f) → IsEquiv (h ∘ g) → TwoOutOfSix f g h
Proof / implementation
two-out-of-six f g h egf ehg = --! begin two-out-of-six-inverses let u = IsEquiv.inverse egf v = IsEquiv.inverse ehg --! end two-out-of-six-inverses --! begin two-out-of-six-section s : Section g s = record { section = f ∘ u ; section-law = comp-assoc u f g ∙ IsEquiv.right-inverse-law egf } --! end two-out-of-six-section --! begin two-out-of-six-retraction r : Retraction g r = record { retraction = v ∘ h ; retraction-law = (comp-assoc g h v) ⁻¹ ∙ IsEquiv.left-inverse-law ehg } --! end two-out-of-six-retraction --! begin two-out-of-six-middle eg : IsEquiv g eg = section-retraction-isEquiv s r --! end two-out-of-six-middle --! begin two-out-of-six-conclusion ef = equiv-cancel-left f g eg egf eh = equiv-cancel-right g h eg ehg in record { first = ef ; middle = eg ; last = eh ; composite = equiv-compose (g ∘ f) h egf eh } --! end two-out-of-six-conclusion
Enclosing interface 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.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Two out of six for equivalences step 2
TwoOutOfSix
Definition, checked
record TwoOutOfSix {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) : Set m where field first : IsEquiv f middle : IsEquiv g last : IsEquiv h composite : IsEquiv (h ∘ (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.Section03.Equivalences where
module _ {Γ : Context} wheretwo-out-of-six
Derivation, checked
two-out-of-six : {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) → IsEquiv (g ∘ f) → IsEquiv (h ∘ g) → TwoOutOfSix f g h
Proof / implementation
two-out-of-six f g h egf ehg = --! begin two-out-of-six-inverses let u = IsEquiv.inverse egf v = IsEquiv.inverse ehg --! end two-out-of-six-inverses --! begin two-out-of-six-section s : Section g s = record { section = f ∘ u ; section-law = comp-assoc u f g ∙ IsEquiv.right-inverse-law egf } --! end two-out-of-six-section --! begin two-out-of-six-retraction r : Retraction g r = record { retraction = v ∘ h ; retraction-law = (comp-assoc g h v) ⁻¹ ∙ IsEquiv.left-inverse-law ehg } --! end two-out-of-six-retraction --! begin two-out-of-six-middle eg : IsEquiv g eg = section-retraction-isEquiv s r --! end two-out-of-six-middle --! begin two-out-of-six-conclusion ef = equiv-cancel-left f g eg egf eh = equiv-cancel-right g h eg ehg in record { first = ef ; middle = eg ; last = eh ; composite = equiv-compose (g ∘ f) h egf eh } --! end two-out-of-six-conclusion
Enclosing interface 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.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Two out of six for equivalences step 3
TwoOutOfSix
Definition, checked
record TwoOutOfSix {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) : Set m where field first : IsEquiv f middle : IsEquiv g last : IsEquiv h composite : IsEquiv (h ∘ (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.Section03.Equivalences where
module _ {Γ : Context} wheretwo-out-of-six
Derivation, checked
two-out-of-six : {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) → IsEquiv (g ∘ f) → IsEquiv (h ∘ g) → TwoOutOfSix f g h
Proof / implementation
two-out-of-six f g h egf ehg = --! begin two-out-of-six-inverses let u = IsEquiv.inverse egf v = IsEquiv.inverse ehg --! end two-out-of-six-inverses --! begin two-out-of-six-section s : Section g s = record { section = f ∘ u ; section-law = comp-assoc u f g ∙ IsEquiv.right-inverse-law egf } --! end two-out-of-six-section --! begin two-out-of-six-retraction r : Retraction g r = record { retraction = v ∘ h ; retraction-law = (comp-assoc g h v) ⁻¹ ∙ IsEquiv.left-inverse-law ehg } --! end two-out-of-six-retraction --! begin two-out-of-six-middle eg : IsEquiv g eg = section-retraction-isEquiv s r --! end two-out-of-six-middle --! begin two-out-of-six-conclusion ef = equiv-cancel-left f g eg egf eh = equiv-cancel-right g h eg ehg in record { first = ef ; middle = eg ; last = eh ; composite = equiv-compose (g ∘ f) h egf eh } --! end two-out-of-six-conclusion
Enclosing interface 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.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Two out of six for equivalences step 4
TwoOutOfSix
Definition, checked
record TwoOutOfSix {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) : Set m where field first : IsEquiv f middle : IsEquiv g last : IsEquiv h composite : IsEquiv (h ∘ (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.Section03.Equivalences where
module _ {Γ : Context} wheretwo-out-of-six
Derivation, checked
two-out-of-six : {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) → IsEquiv (g ∘ f) → IsEquiv (h ∘ g) → TwoOutOfSix f g h
Proof / implementation
two-out-of-six f g h egf ehg = --! begin two-out-of-six-inverses let u = IsEquiv.inverse egf v = IsEquiv.inverse ehg --! end two-out-of-six-inverses --! begin two-out-of-six-section s : Section g s = record { section = f ∘ u ; section-law = comp-assoc u f g ∙ IsEquiv.right-inverse-law egf } --! end two-out-of-six-section --! begin two-out-of-six-retraction r : Retraction g r = record { retraction = v ∘ h ; retraction-law = (comp-assoc g h v) ⁻¹ ∙ IsEquiv.left-inverse-law ehg } --! end two-out-of-six-retraction --! begin two-out-of-six-middle eg : IsEquiv g eg = section-retraction-isEquiv s r --! end two-out-of-six-middle --! begin two-out-of-six-conclusion ef = equiv-cancel-left f g eg egf eh = equiv-cancel-right g h eg ehg in record { first = ef ; middle = eg ; last = eh ; composite = equiv-compose (g ∘ f) h egf eh } --! end two-out-of-six-conclusion
Enclosing interface 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.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Two out of six for equivalences step 5
TwoOutOfSix
Definition, checked
record TwoOutOfSix {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) : Set m where field first : IsEquiv f middle : IsEquiv g last : IsEquiv h composite : IsEquiv (h ∘ (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.Section03.Equivalences where
module _ {Γ : Context} wheretwo-out-of-six
Derivation, checked
two-out-of-six : {C D E F : CAT Γ} (f : MAP C D) (g : MAP D E) (h : MAP E F) → IsEquiv (g ∘ f) → IsEquiv (h ∘ g) → TwoOutOfSix f g h
Proof / implementation
two-out-of-six f g h egf ehg = --! begin two-out-of-six-inverses let u = IsEquiv.inverse egf v = IsEquiv.inverse ehg --! end two-out-of-six-inverses --! begin two-out-of-six-section s : Section g s = record { section = f ∘ u ; section-law = comp-assoc u f g ∙ IsEquiv.right-inverse-law egf } --! end two-out-of-six-section --! begin two-out-of-six-retraction r : Retraction g r = record { retraction = v ∘ h ; retraction-law = (comp-assoc g h v) ⁻¹ ∙ IsEquiv.left-inverse-law ehg } --! end two-out-of-six-retraction --! begin two-out-of-six-middle eg : IsEquiv g eg = section-retraction-isEquiv s r --! end two-out-of-six-middle --! begin two-out-of-six-conclusion ef = equiv-cancel-left f g eg egf eh = equiv-cancel-right g h eg ehg in record { first = ef ; middle = eg ; last = eh ; composite = equiv-compose (g ∘ f) h egf eh } --! end two-out-of-six-conclusion
Enclosing interface 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.Equivalences where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Definition 1.3.8. We say that a functor \(f\colon C \to D\) is a retract of a functor \(f'\colon C' \to D'\) if there exists a commutative diagram of the form
Agda Retract
Retract
Definition, checked
record Retract {C D C′ D′ : CAT Γ} (f : MAP C D) (f′ : MAP C′ D′) : Set m where field map : Square f f′ retraction : Square f′ f retraction-law : SquareEquality (comp-square retraction map) (id-square 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.Retracts 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.
together with identifications \(\alpha \colon \id _{C} = h \circ g\) and \(\beta \colon j \circ k = \id _{D}\), and an identification between \(\id _f\colon f= f\) and the composite identification \[ f = f \circ \id _C \overset {\alpha }{=} f \circ h \circ g = j \circ f' \circ g = j \circ k \circ f \overset {\beta }{=} \id _D \circ f = f. \]
Agda Retract step 1
Retract
Definition, checked
record Retract {C D C′ D′ : CAT Γ} (f : MAP C D) (f′ : MAP C′ D′) : Set m where field map : Square f f′ retraction : Square f′ f retraction-law : SquareEquality (comp-square retraction map) (id-square 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.Retracts where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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.3.9. Assume that \(f\colon C \to D\) is a retract of \(f'\colon C' \to D'\). If \(f'\) is an equivalence, then so is \(f\).
Agda Equivalences closed under retracts
retract-isEquiv
Derivation, checked
retract-isEquiv : {C D C′ D′ : CAT Γ} {f : MAP C D} {f′ : MAP C′ D′} → Retract f f′ → IsEquiv f′ → IsEquiv f
Proof / implementation
retract-isEquiv {C = C} {D = D} {f = f} {f′} R e = let inclusion = Retract.map R retraction = Retract.retraction R law = Retract.retraction-law R g = Square.source-map inclusion h = Square.source-map retraction k = Square.target-map inclusion j = Square.target-map retraction section-square = Square.cell inclusion retraction-square = Square.cell retraction source-law = SquareEquality.source-identification law target-law = SquareEquality.target-identification law u = IsEquiv.inverse e w : MAP D C w = h ∘ (u ∘ k) right : (f ∘ w) =₁ (id D) right = target-law ∙ ((j ◁ comp-unitˡ k) ∙ ((j ◁ ((IsEquiv.right-inverse-law e) ⁻¹ ▷ k)) ∙ ((j ◁ (comp-assoc k u f′) ⁻¹) ∙ (comp-assoc (u ∘ k) f′ j ∙ ((retraction-square ▷ (u ∘ k)) ∙ (comp-assoc (u ∘ k) h f) ⁻¹))))) left : (w ∘ f) =₁ (id C) left = source-law ∙ ((h ◁ comp-unitˡ g) ∙ ((h ◁ ((IsEquiv.left-inverse-law e) ⁻¹ ▷ g)) ∙ ((h ◁ (comp-assoc g f′ u) ⁻¹) ∙ ((h ◁ (u ◁ section-square ⁻¹)) ∙ ((h ◁ comp-assoc f k u) ∙ comp-assoc f (u ∘ k) h))))) in record { inverse = w ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Retracts 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. Let \((f')^{-1}\colon D' \to C'\) be an inverse of \(f'\). We claim that the composite \(w := h \circ (f')^{-1} \circ k\colon D \to C\) is inverse to \(f\). Indeed, we have identifications Agda\[ f \circ w = f \circ h \circ (f')^{-1} \circ k = j \circ f' \circ (f')^{-1} \circ k = j \circ k = \id _{D} \] and Agda\[ w \circ f = h \circ (f')^{-1} \circ k \circ f = h \circ (f')^{-1} \circ f' \circ g = h \circ g = \id _{C}. \] This finishes the proof. □
Agda Equivalences closed under retracts step 1
retract-isEquiv
Derivation, checked
retract-isEquiv : {C D C′ D′ : CAT Γ} {f : MAP C D} {f′ : MAP C′ D′} → Retract f f′ → IsEquiv f′ → IsEquiv f
Proof / implementation
retract-isEquiv {C = C} {D = D} {f = f} {f′} R e = let inclusion = Retract.map R retraction = Retract.retraction R law = Retract.retraction-law R g = Square.source-map inclusion h = Square.source-map retraction k = Square.target-map inclusion j = Square.target-map retraction section-square = Square.cell inclusion retraction-square = Square.cell retraction source-law = SquareEquality.source-identification law target-law = SquareEquality.target-identification law u = IsEquiv.inverse e w : MAP D C w = h ∘ (u ∘ k) right : (f ∘ w) =₁ (id D) right = target-law ∙ ((j ◁ comp-unitˡ k) ∙ ((j ◁ ((IsEquiv.right-inverse-law e) ⁻¹ ▷ k)) ∙ ((j ◁ (comp-assoc k u f′) ⁻¹) ∙ (comp-assoc (u ∘ k) f′ j ∙ ((retraction-square ▷ (u ∘ k)) ∙ (comp-assoc (u ∘ k) h f) ⁻¹))))) left : (w ∘ f) =₁ (id C) left = source-law ∙ ((h ◁ comp-unitˡ g) ∙ ((h ◁ ((IsEquiv.left-inverse-law e) ⁻¹ ▷ g)) ∙ ((h ◁ (comp-assoc g f′ u) ⁻¹) ∙ ((h ◁ (u ◁ section-square ⁻¹)) ∙ ((h ◁ comp-assoc f k u) ∙ comp-assoc f (u ∘ k) h))))) in record { inverse = w ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Retracts where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Equivalences closed under retracts step 2
retract-isEquiv
Derivation, checked
retract-isEquiv : {C D C′ D′ : CAT Γ} {f : MAP C D} {f′ : MAP C′ D′} → Retract f f′ → IsEquiv f′ → IsEquiv f
Proof / implementation
retract-isEquiv {C = C} {D = D} {f = f} {f′} R e = let inclusion = Retract.map R retraction = Retract.retraction R law = Retract.retraction-law R g = Square.source-map inclusion h = Square.source-map retraction k = Square.target-map inclusion j = Square.target-map retraction section-square = Square.cell inclusion retraction-square = Square.cell retraction source-law = SquareEquality.source-identification law target-law = SquareEquality.target-identification law u = IsEquiv.inverse e w : MAP D C w = h ∘ (u ∘ k) right : (f ∘ w) =₁ (id D) right = target-law ∙ ((j ◁ comp-unitˡ k) ∙ ((j ◁ ((IsEquiv.right-inverse-law e) ⁻¹ ▷ k)) ∙ ((j ◁ (comp-assoc k u f′) ⁻¹) ∙ (comp-assoc (u ∘ k) f′ j ∙ ((retraction-square ▷ (u ∘ k)) ∙ (comp-assoc (u ∘ k) h f) ⁻¹))))) left : (w ∘ f) =₁ (id C) left = source-law ∙ ((h ◁ comp-unitˡ g) ∙ ((h ◁ ((IsEquiv.left-inverse-law e) ⁻¹ ▷ g)) ∙ ((h ◁ (comp-assoc g f′ u) ⁻¹) ∙ ((h ◁ (u ◁ section-square ⁻¹)) ∙ ((h ◁ comp-assoc f k u) ∙ comp-assoc f (u ∘ k) h))))) in record { inverse = w ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Retracts where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Equivalences closed under retracts step 3
retract-isEquiv
Derivation, checked
retract-isEquiv : {C D C′ D′ : CAT Γ} {f : MAP C D} {f′ : MAP C′ D′} → Retract f f′ → IsEquiv f′ → IsEquiv f
Proof / implementation
retract-isEquiv {C = C} {D = D} {f = f} {f′} R e = let inclusion = Retract.map R retraction = Retract.retraction R law = Retract.retraction-law R g = Square.source-map inclusion h = Square.source-map retraction k = Square.target-map inclusion j = Square.target-map retraction section-square = Square.cell inclusion retraction-square = Square.cell retraction source-law = SquareEquality.source-identification law target-law = SquareEquality.target-identification law u = IsEquiv.inverse e w : MAP D C w = h ∘ (u ∘ k) right : (f ∘ w) =₁ (id D) right = target-law ∙ ((j ◁ comp-unitˡ k) ∙ ((j ◁ ((IsEquiv.right-inverse-law e) ⁻¹ ▷ k)) ∙ ((j ◁ (comp-assoc k u f′) ⁻¹) ∙ (comp-assoc (u ∘ k) f′ j ∙ ((retraction-square ▷ (u ∘ k)) ∙ (comp-assoc (u ∘ k) h f) ⁻¹))))) left : (w ∘ f) =₁ (id C) left = source-law ∙ ((h ◁ comp-unitˡ g) ∙ ((h ◁ ((IsEquiv.left-inverse-law e) ⁻¹ ▷ g)) ∙ ((h ◁ (comp-assoc g f′ u) ⁻¹) ∙ ((h ◁ (u ◁ section-square ⁻¹)) ∙ ((h ◁ comp-assoc f k u) ∙ comp-assoc f (u ∘ k) h))))) in record { inverse = w ; left-inverse-law = left ⁻¹ ; right-inverse-law = 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.Section03.Retracts where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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.3.10. Prewhiskering or postwhiskering by an equivalence induces equivalences of animae of identifications.
Agda Whiskering by equivalence
postWhisker-isEquiv
Derivation, checked
postWhisker-isEquiv : {B C D : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP B C) → IsEquiv (postWhisker {f = f} {g} F)
Proof / implementation
postWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = postWhisker-composite-isEquiv f g F G (postWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) f g (postWhisker-id-isEquiv f g)) second = postWhisker-composite-isEquiv (F ∘ f) (F ∘ g) G F (postWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) (F ∘ f) (F ∘ g) (postWhisker-id-isEquiv (F ∘ f) (F ∘ g))) in TwoOutOfSix.first (two-out-of-six (postWhisker F) (postWhisker G) (postWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} wherepreWhisker-isEquiv
Derivation, checked
preWhisker-isEquiv : {C D E : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP D E) → IsEquiv (preWhisker {f = f} {g} F)
Proof / implementation
preWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = preWhisker-composite-isEquiv f g F G (preWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) f g (preWhisker-id-isEquiv f g)) second = preWhisker-composite-isEquiv (f ∘ F) (g ∘ F) G F (preWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) (f ∘ F) (g ∘ F) (preWhisker-id-isEquiv (f ∘ F) (g ∘ F))) in TwoOutOfSix.first (two-out-of-six (preWhisker F) (preWhisker G) (preWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence 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. Composition with a fixed identification is an equivalence, with inverse given by composition with its inverse. This follows from the vertical unit, associativity, and inverse laws.
Agda Whiskering by equivalence step 1
postWhisker-isEquiv
Derivation, checked
postWhisker-isEquiv : {B C D : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP B C) → IsEquiv (postWhisker {f = f} {g} F)
Proof / implementation
postWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = postWhisker-composite-isEquiv f g F G (postWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) f g (postWhisker-id-isEquiv f g)) second = postWhisker-composite-isEquiv (F ∘ f) (F ∘ g) G F (postWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) (F ∘ f) (F ∘ g) (postWhisker-id-isEquiv (F ∘ f) (F ∘ g))) in TwoOutOfSix.first (two-out-of-six (postWhisker F) (postWhisker G) (postWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} wherepreWhisker-isEquiv
Derivation, checked
preWhisker-isEquiv : {C D E : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP D E) → IsEquiv (preWhisker {f = f} {g} F)
Proof / implementation
preWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = preWhisker-composite-isEquiv f g F G (preWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) f g (preWhisker-id-isEquiv f g)) second = preWhisker-composite-isEquiv (f ∘ F) (g ∘ F) G F (preWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) (f ∘ F) (g ∘ F) (preWhisker-id-isEquiv (f ∘ F) (g ∘ F))) in TwoOutOfSix.first (two-out-of-six (preWhisker F) (preWhisker G) (preWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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.
Let \(F\colon C\to D\) have inverse \(G\), and consider two functors \(a,b\colon T\to C\). We wish to show that the first functor \(F \star -\) in the following diagram is an equivalence: \[ (a= b)\xrightarrow {F\star -}(Fa= Fb) \xrightarrow {G\star -}(GFa= GFb) \xrightarrow {F\star -}(FGFa= FGFb). \] Interchange with \(GF=\id _C\) identifies the composite of the first two functors with transport along the identifications \(GFa = a\) and \(b = GFb\), and so that composite is an equivalence. The composite of the last two is an equivalence for the same reason, using \(FG=\id _D\), and so the claim follows from the 2-out-of-6 property. Prewhiskering is treated in the same way. □
Agda Whiskering by equivalence step 2
postWhisker-isEquiv
Derivation, checked
postWhisker-isEquiv : {B C D : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP B C) → IsEquiv (postWhisker {f = f} {g} F)
Proof / implementation
postWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = postWhisker-composite-isEquiv f g F G (postWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) f g (postWhisker-id-isEquiv f g)) second = postWhisker-composite-isEquiv (F ∘ f) (F ∘ g) G F (postWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) (F ∘ f) (F ∘ g) (postWhisker-id-isEquiv (F ∘ f) (F ∘ g))) in TwoOutOfSix.first (two-out-of-six (postWhisker F) (postWhisker G) (postWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} wherepreWhisker-isEquiv
Derivation, checked
preWhisker-isEquiv : {C D E : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP D E) → IsEquiv (preWhisker {f = f} {g} F)
Proof / implementation
preWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = preWhisker-composite-isEquiv f g F G (preWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) f g (preWhisker-id-isEquiv f g)) second = preWhisker-composite-isEquiv (f ∘ F) (g ∘ F) G F (preWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) (f ∘ F) (g ∘ F) (preWhisker-id-isEquiv (f ∘ F) (g ∘ F))) in TwoOutOfSix.first (two-out-of-six (preWhisker F) (preWhisker G) (preWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence 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.
Agda Whiskering by equivalence step 3
postWhisker-isEquiv
Derivation, checked
postWhisker-isEquiv : {B C D : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP B C) → IsEquiv (postWhisker {f = f} {g} F)
Proof / implementation
postWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = postWhisker-composite-isEquiv f g F G (postWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) f g (postWhisker-id-isEquiv f g)) second = postWhisker-composite-isEquiv (F ∘ f) (F ∘ g) G F (postWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) (F ∘ f) (F ∘ g) (postWhisker-id-isEquiv (F ∘ f) (F ∘ g))) in TwoOutOfSix.first (two-out-of-six (postWhisker F) (postWhisker G) (postWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} wherepreWhisker-isEquiv
Derivation, checked
preWhisker-isEquiv : {C D E : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP D E) → IsEquiv (preWhisker {f = f} {g} F)
Proof / implementation
preWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = preWhisker-composite-isEquiv f g F G (preWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) f g (preWhisker-id-isEquiv f g)) second = preWhisker-composite-isEquiv (f ∘ F) (g ∘ F) G F (preWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) (f ∘ F) (g ∘ F) (preWhisker-id-isEquiv (f ∘ F) (g ∘ F))) in TwoOutOfSix.first (two-out-of-six (preWhisker F) (preWhisker G) (preWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Whiskering by equivalence step 4
postWhisker-isEquiv
Derivation, checked
postWhisker-isEquiv : {B C D : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP B C) → IsEquiv (postWhisker {f = f} {g} F)
Proof / implementation
postWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = postWhisker-composite-isEquiv f g F G (postWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) f g (postWhisker-id-isEquiv f g)) second = postWhisker-composite-isEquiv (F ∘ f) (F ∘ g) G F (postWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) (F ∘ f) (F ∘ g) (postWhisker-id-isEquiv (F ∘ f) (F ∘ g))) in TwoOutOfSix.first (two-out-of-six (postWhisker F) (postWhisker G) (postWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} wherepreWhisker-isEquiv
Derivation, checked
preWhisker-isEquiv : {C D E : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP D E) → IsEquiv (preWhisker {f = f} {g} F)
Proof / implementation
preWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = preWhisker-composite-isEquiv f g F G (preWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) f g (preWhisker-id-isEquiv f g)) second = preWhisker-composite-isEquiv (f ∘ F) (g ∘ F) G F (preWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) (f ∘ F) (g ∘ F) (preWhisker-id-isEquiv (f ∘ F) (g ∘ F))) in TwoOutOfSix.first (two-out-of-six (preWhisker F) (preWhisker G) (preWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence 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.
Consequently an equivalence lifts a specified identification, together with an identification of its image with that identification. Applying the same result to functors into an anima of identifications also lifts identifications between identifications.
Agda Lifting identifications through equivalences
postWhisker-isEquiv
Derivation, checked
postWhisker-isEquiv : {B C D : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP B C) → IsEquiv (postWhisker {f = f} {g} F)
Proof / implementation
postWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = postWhisker-composite-isEquiv f g F G (postWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) f g (postWhisker-id-isEquiv f g)) second = postWhisker-composite-isEquiv (F ∘ f) (F ∘ g) G F (postWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) (F ∘ f) (F ∘ g) (postWhisker-id-isEquiv (F ∘ f) (F ∘ g))) in TwoOutOfSix.first (two-out-of-six (postWhisker F) (postWhisker G) (postWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} wherepreWhisker-isEquiv
Derivation, checked
preWhisker-isEquiv : {C D E : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP D E) → IsEquiv (preWhisker {f = f} {g} F)
Proof / implementation
preWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = preWhisker-composite-isEquiv f g F G (preWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) f g (preWhisker-id-isEquiv f g)) second = preWhisker-composite-isEquiv (f ∘ F) (g ∘ F) G F (preWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) (f ∘ F) (g ∘ F) (preWhisker-id-isEquiv (f ∘ F) (g ∘ F))) in TwoOutOfSix.first (two-out-of-six (preWhisker F) (preWhisker G) (preWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence 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.
Agda Lifting and reflecting identifications
postWhisker-isEquiv
Derivation, checked
postWhisker-isEquiv : {B C D : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP B C) → IsEquiv (postWhisker {f = f} {g} F)
Proof / implementation
postWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = postWhisker-composite-isEquiv f g F G (postWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) f g (postWhisker-id-isEquiv f g)) second = postWhisker-composite-isEquiv (F ∘ f) (F ∘ g) G F (postWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) (F ∘ f) (F ∘ g) (postWhisker-id-isEquiv (F ∘ f) (F ∘ g))) in TwoOutOfSix.first (two-out-of-six (postWhisker F) (postWhisker G) (postWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} wherepreWhisker-isEquiv
Derivation, checked
preWhisker-isEquiv : {C D E : CAT Γ} (F : MAP C D) → IsEquiv F → (f g : MAP D E) → IsEquiv (preWhisker {f = f} {g} F)
Proof / implementation
preWhisker-isEquiv F e f g = let G = IsEquiv.inverse e first = preWhisker-composite-isEquiv f g F G (preWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) f g (preWhisker-id-isEquiv f g)) second = preWhisker-composite-isEquiv (f ∘ F) (g ∘ F) G F (preWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) (f ∘ F) (g ∘ F) (preWhisker-id-isEquiv (f ∘ F) (g ∘ F))) in TwoOutOfSix.first (two-out-of-six (preWhisker F) (preWhisker G) (preWhisker F) first second)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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.
From the universal property of products, we may directly deduce that products are commutative, unital, and associative. For commutativity of products, one argues as follows:
Lemma 1.3.11. For categories \(C\) and \(D\), the functor \((\pr _2,\pr _1)\colon C \times D \to D \times C\) is an equivalence, with inverse given by \((\pr _2,\pr _1)\colon D \times C \to C \times D\).
Agda Symmetry of products
swap
Definition, checked
swap : {C D : CAT Γ} → MAP (C × D) (D × C)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereswap-swap
Derivation, checked
swap-swap : (C D : CAT Γ) → (swap ∘ swap) =₁ (id (C × D))
Proof / implementation
swap-swap C D = pair₌ --! begin swap-swap-first-projection ((comp-unitʳ pr₁) ⁻¹ ∙ (pair-β₂ pr₂ pr₁ ∙ project-pair₁ pr₂ pr₁ swap)) --! end swap-swap-first-projection --! begin swap-swap-second-projection ((comp-unitʳ pr₂) ⁻¹ ∙ (pair-β₁ pr₂ pr₁ ∙ project-pair₂ pr₂ pr₁ swap)) --! end swap-swap-second-projection
Enclosing interface 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.ProductConstructions where
module _ {Γ : Context} whereswap-isEquiv
Derivation, checked
swap-isEquiv : (C D : CAT Γ) → IsEquiv (swap {C = C} {D = D})
Proof / implementation
swap-isEquiv C D = record { inverse = swap ; left-inverse-law = (swap-swap C D) ⁻¹ ; right-inverse-law = (swap-swap D C) ⁻¹ }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions 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 need to provide identifications \((\pr _2,\pr _1) \circ (\pr _2,\pr _1) = \id _{C \times D}\) and \((\pr _2,\pr _1) \circ (\pr _2,\pr _1) = \id _{D \times C}\). By symmetry, it will suffice to produce the first identification. For this, it will in turn suffice to produce identifications after composing with the functors \(\pr _1\) and \(\pr _2\). For the composition with \(\pr _1\) we compute that \[ \pr _1 \circ ((\pr _2,\pr _1) \circ (\pr _2,\pr _1)) = (\pr _1 \circ (\pr _2,\pr _1)) \circ (\pr _2,\pr _1) = \pr _2 \circ (\pr _2,\pr _1) = \pr _1, \] which is indeed identified with \(\pr _1 \circ \id _{C \times D}\). The case for composition with \(\pr _2\) is analogous. This finishes the proof. □
Agda Symmetry of products step 1
swap
Definition, checked
swap : {C D : CAT Γ} → MAP (C × D) (D × C)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereswap-swap
Derivation, checked
swap-swap : (C D : CAT Γ) → (swap ∘ swap) =₁ (id (C × D))
Proof / implementation
swap-swap C D = pair₌ --! begin swap-swap-first-projection ((comp-unitʳ pr₁) ⁻¹ ∙ (pair-β₂ pr₂ pr₁ ∙ project-pair₁ pr₂ pr₁ swap)) --! end swap-swap-first-projection --! begin swap-swap-second-projection ((comp-unitʳ pr₂) ⁻¹ ∙ (pair-β₁ pr₂ pr₁ ∙ project-pair₂ pr₂ pr₁ swap)) --! end swap-swap-second-projection
Enclosing interface 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.ProductConstructions where
module _ {Γ : Context} whereswap-isEquiv
Derivation, checked
swap-isEquiv : (C D : CAT Γ) → IsEquiv (swap {C = C} {D = D})
Proof / implementation
swap-isEquiv C D = record { inverse = swap ; left-inverse-law = (swap-swap C D) ⁻¹ ; right-inverse-law = (swap-swap D C) ⁻¹ }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Symmetry of products step 2
swap
Definition, checked
swap : {C D : CAT Γ} → MAP (C × D) (D × C)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereswap-swap
Derivation, checked
swap-swap : (C D : CAT Γ) → (swap ∘ swap) =₁ (id (C × D))
Proof / implementation
swap-swap C D = pair₌ --! begin swap-swap-first-projection ((comp-unitʳ pr₁) ⁻¹ ∙ (pair-β₂ pr₂ pr₁ ∙ project-pair₁ pr₂ pr₁ swap)) --! end swap-swap-first-projection --! begin swap-swap-second-projection ((comp-unitʳ pr₂) ⁻¹ ∙ (pair-β₁ pr₂ pr₁ ∙ project-pair₂ pr₂ pr₁ swap)) --! end swap-swap-second-projection
Enclosing interface 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.ProductConstructions where
module _ {Γ : Context} whereswap-isEquiv
Derivation, checked
swap-isEquiv : (C D : CAT Γ) → IsEquiv (swap {C = C} {D = D})
Proof / implementation
swap-isEquiv C D = record { inverse = swap ; left-inverse-law = (swap-swap C D) ⁻¹ ; right-inverse-law = (swap-swap D C) ⁻¹ }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Symmetry of products step 3
swap
Definition, checked
swap : {C D : CAT Γ} → MAP (C × D) (D × C)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereswap-swap
Derivation, checked
swap-swap : (C D : CAT Γ) → (swap ∘ swap) =₁ (id (C × D))
Proof / implementation
swap-swap C D = pair₌ --! begin swap-swap-first-projection ((comp-unitʳ pr₁) ⁻¹ ∙ (pair-β₂ pr₂ pr₁ ∙ project-pair₁ pr₂ pr₁ swap)) --! end swap-swap-first-projection --! begin swap-swap-second-projection ((comp-unitʳ pr₂) ⁻¹ ∙ (pair-β₁ pr₂ pr₁ ∙ project-pair₂ pr₂ pr₁ swap)) --! end swap-swap-second-projection
Enclosing interface 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.ProductConstructions where
module _ {Γ : Context} whereswap-isEquiv
Derivation, checked
swap-isEquiv : (C D : CAT Γ) → IsEquiv (swap {C = C} {D = D})
Proof / implementation
swap-isEquiv C D = record { inverse = swap ; left-inverse-law = (swap-swap C D) ⁻¹ ; right-inverse-law = (swap-swap D C) ⁻¹ }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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.
Unitality may be argued similarly:
Lemma 1.3.12. For every category \(C\), the projection functor \(\pr _1\colon C \times * \to C\) is an equivalence, with inverse given by the functor \((\id _{C}, p_{C})\colon C \to C \times *\).
Agda Unitality product of categories
product-unitʳ-inverse
Definition, checked
product-unitʳ-inverse : (C : CAT Γ) → MAP C (C × One)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereproduct-unitʳ-isEquiv
Derivation, checked
product-unitʳ-isEquiv : (C : CAT Γ) → IsEquiv (pr₁ {C = C} {D = One})
Proof / implementation
product-unitʳ-isEquiv C = record { inverse = product-unitʳ-inverse C ; left-inverse-law = (product-unitʳ-inverse-pr₁ C) ⁻¹ --! begin product-unit-retraction ; right-inverse-law = (pair-β₁ (id C) (terminate C)) ⁻¹ --! end product-unit-retraction }
Enclosing interface 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.ProductConstructions 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.
Proof
Proof. The composite \(\pr _1 \circ (\id _{C}, p_{C})\colon C \to C\) is identified with \(\id _{C}\) by the defining property of \((\id _{C}, p_{C})\). To show that the composite \((\id _{C}, p_{C}) \circ \pr _1\colon C \times * \to C \times *\) is identified with \(\id _{C \times *}\), it will suffice to do so after composing with \(\pr _1\) and with \(\pr _2\). The case for \(\pr _2\) is clear, since any two functors \(C \times * \to *\) are identified. In the case of \(\pr _1\) we compute \[ \pr _1 \circ ((\id _{C}, p_{C}) \circ \pr _1) = (\pr _1 \circ (\id _{C}, p_{C})) \circ \pr _1 = \id _{C} \circ \pr _1 = \pr _1 = \pr _1 \circ \id _{C \times *}, \] where the first identification is associativity, the second is the relation proved in the first paragraph, and the third and fourth are unitality. This finishes the proof. □
Agda Unitality product of categories step 1
product-unitʳ-inverse
Definition, checked
product-unitʳ-inverse : (C : CAT Γ) → MAP C (C × One)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereproduct-unitʳ-isEquiv
Derivation, checked
product-unitʳ-isEquiv : (C : CAT Γ) → IsEquiv (pr₁ {C = C} {D = One})
Proof / implementation
product-unitʳ-isEquiv C = record { inverse = product-unitʳ-inverse C ; left-inverse-law = (product-unitʳ-inverse-pr₁ C) ⁻¹ --! begin product-unit-retraction ; right-inverse-law = (pair-β₁ (id C) (terminate C)) ⁻¹ --! end product-unit-retraction }
Enclosing interface 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.ProductConstructions where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof is organized differently. This link opens the current result and its full proof, rather than identifying this individual prose step with a specific code line.
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 Unitality product of categories step 2
product-unitʳ-inverse
Definition, checked
product-unitʳ-inverse : (C : CAT Γ) → MAP C (C × One)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereproduct-unitʳ-isEquiv
Derivation, checked
product-unitʳ-isEquiv : (C : CAT Γ) → IsEquiv (pr₁ {C = C} {D = One})
Proof / implementation
product-unitʳ-isEquiv C = record { inverse = product-unitʳ-inverse C ; left-inverse-law = (product-unitʳ-inverse-pr₁ C) ⁻¹ --! begin product-unit-retraction ; right-inverse-law = (pair-β₁ (id C) (terminate C)) ⁻¹ --! end product-unit-retraction }
Enclosing interface 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.ProductConstructions 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.
Agda Unitality product of categories step 3
product-unitʳ-inverse
Definition, checked
product-unitʳ-inverse : (C : CAT Γ) → MAP C (C × One)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.ProductConstructions where
module _ {Γ : Context} whereproduct-unitʳ-isEquiv
Derivation, checked
product-unitʳ-isEquiv : (C : CAT Γ) → IsEquiv (pr₁ {C = C} {D = One})
Proof / implementation
product-unitʳ-isEquiv C = record { inverse = product-unitʳ-inverse C ; left-inverse-law = (product-unitʳ-inverse-pr₁ C) ⁻¹ --! begin product-unit-retraction ; right-inverse-law = (pair-β₁ (id C) (terminate C)) ⁻¹ --! end product-unit-retraction }
Enclosing interface 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.ProductConstructions 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.
Remark 1.3.13. In the previous proofs, we have been very explicit about the usage of associativity and naturality identifications. In the remainder of this book, we will often leave the usage of such identifications implicit in order to make the proofs more concise.
Exercise 1.3.14 (Exercise 1.9.1 (outside selection)). Formulate and prove the associativity of the product of categories.
Agda Product associativity exercise
forward
Definition, checked
forward : MAP ((C × D) × E) (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.Section03.ProductConstructions where
module _ {Γ : Context} where
module Associativity (C D E : CAT Γ) wherebackward
Definition, checked
backward : MAP (C × (D × E)) ((C × D) × E)
Proof / implementation
backward = Backward.triple
Enclosing interface 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.ProductConstructions where
module _ {Γ : Context} where
module Associativity (C D E : CAT Γ) wherebackward-forward
Derivation, checked
backward-forward : (backward ∘ forward) =₁ (id ((C × D) × E))
Proof / implementation
backward-forward = pair-projections ∙ (pair⁼ (pair-η pr₁) (id₌ pr₂) ∙ (pair⁼ (pair⁼ forward-first forward-second ∙ pair-pre pr₁ (pr₁ ∘ pr₂) forward) forward-third ∙ pair-pre (pair pr₁ (pr₁ ∘ pr₂)) (pr₂ ∘ pr₂) forward))
Enclosing interface 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.ProductConstructions where
module _ {Γ : Context} where
module Associativity (C D E : CAT Γ) whereforward-backward
Derivation, checked
forward-backward : (forward ∘ backward) =₁ (id (C × (D × E)))
Proof / implementation
forward-backward = pair-projections ∙ (pair⁼ (id₌ pr₁) (pair-η pr₂) ∙ (pair⁼ backward-first (pair⁼ backward-second backward-third ∙ pair-pre (pr₂ ∘ pr₁) pr₂ backward) ∙ pair-pre (pr₁ ∘ pr₁) (pair (pr₂ ∘ pr₁) pr₂) backward))
Enclosing interface 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.ProductConstructions where
module _ {Γ : Context} where
module Associativity (C D E : CAT Γ) whereforward-isEquiv
Derivation, checked
forward-isEquiv : IsEquiv forward
Proof / implementation
forward-isEquiv = record { inverse = backward ; left-inverse-law = backward-forward ⁻¹ ; right-inverse-law = forward-backward ⁻¹ }
Enclosing interface 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.ProductConstructions where
module _ {Γ : Context} where
module Associativity (C D E : 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.
Construction 1.3.15 (Pairing of identifications). Given functors \(f,f'\colon T \to C\) and \(g,g'\colon T \to D\), pairing defines a functor \[ (-,-)\colon (f=f')\times (g=g')\longrightarrow ((f,g)=(f',g')). \] For \(\varphi :f=f'\) and \(\psi :g=g'\), its value \((\varphi ,\psi )\) is equipped with identifications \begin {align*} \beta ^1_{f',g'}\circ \bigl (\pr _1\star (\varphi ,\psi )\bigr ) &=\varphi \circ \beta ^1_{f,g},\\ \beta ^2_{f',g'}\circ \bigl (\pr _2\star (\varphi ,\psi )\bigr ) &=\psi \circ \beta ^2_{f,g}. \end {align*}
There are identifications \[ (\id _f,\id _g)=\id _{(f,g)},\qquad (\varphi '\circ \varphi ,\psi '\circ \psi ) =(\varphi ',\psi ')\circ (\varphi ,\psi ), \] where \(\varphi ':f'=f''\) and \(\psi ':g'=g''\).
Proof
Proof. Under the identifications \(\beta ^1_{f,g}:\pr _1(f,g)=f\) and \(\beta ^2_{f,g}:\pr _2(f,g)=g\), \(\phi \) and \(\psi \) correspond to two absolute objects of the two factors of the following product: \[ \bigl (\pr _1(f,g)=\pr _1(f',g')\bigr ) \times \bigl (\pr _2(f,g)=\pr _2(f',g')\bigr ). \] Since this product is equivalent to the anima \((f,g) = (f',g')\) by Axiom B.2, this provides the identification \((\phi ,\psi )\) with the two claimed identification.
We leave the identity law and composition law as exercises for the reader. □
Agda Finite compatibility of products step 1
pair⁼-functor
Derivation, checked
pair⁼-functor : {C D : CAT Γ} (x x′ : Term C) (y y′ : Term D) → MAP ((Equal x x′) × (Equal y y′)) (Equal (pair x y) (pair x′ y′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherepair⁼-cong
Derivation, checked
pair⁼-cong : {C D : CAT Γ} {x x′ : Term C} {y y′ : Term D} {α α′ : x ＝ x′} {β β′ : y ＝ y′} → α =₁ α′ → β =₁ β′ → pair⁼ α β =₁ pair⁼ α′ β′
Proof / implementation
pair⁼-cong {α = α} {α′} {β} {β′} p q = pair₌-unique (pair⁼-triangle₁ α β) (pair⁼-triangle₂ α β) (replace-edges₌ (id₌ (pr₁ ◁ pair⁼ α′ β′)) (p ⁻¹) (pair⁼-triangle₁ α′ β′)) (replace-edges₌ (id₌ (pr₂ ◁ pair⁼ α′ β′)) (q ⁻¹) (pair⁼-triangle₂ α′ β′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-comp
Derivation, checked
pair⁼-comp : {C D : CAT Γ} {x₀ x₁ x₂ : Term C} {y₀ y₁ y₂ : Term D} (α₂ : x₁ ＝ x₂) (α₁ : x₀ ＝ x₁) (β₂ : y₁ ＝ y₂) (β₁ : y₀ ＝ y₁) → pair⁼ (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (pair⁼ α₂ β₂ ∙ pair⁼ α₁ β₁)
Proof / implementation
pair⁼-comp α₂ α₁ β₂ β₁ = pair₌-unique (pair⁼-triangle₁ (α₂ ∙ α₁) (β₂ ∙ β₁)) (pair⁼-triangle₂ (α₂ ∙ α₁) (β₂ ∙ β₁)) (lies-over-comp pr₁ (pair⁼-triangle₁ α₁ β₁) (pair⁼-triangle₁ α₂ β₂)) (lies-over-comp pr₂ (pair⁼-triangle₂ α₁ β₁) (pair⁼-triangle₂ α₂ β₂))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-id
Derivation, checked
pair⁼-id : {C D : CAT Γ} (x : Term C) (y : Term D) → pair⁼ (const {P = A} (id₌ x)) (const (id₌ y)) =₁ const (id₌ (pair x y))
Proof / implementation
pair⁼-id x y = pair₌-unique (pair⁼-triangle₁ (const (id₌ x)) (const (id₌ y))) (pair⁼-triangle₂ (const (id₌ x)) (const (id₌ y))) (lies-over-id pr₁ (pair-β₁ x y)) (lies-over-id pr₂ (pair-β₂ x y))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} whereproductMap₌
Derivation, checked
productMap₌ : {C C′ D D′ : CAT Γ} (f f′ : MAP C C′) (g g′ : MAP D D′) → MAP ((Equal f f′) × (Equal g g′)) (Equal (productMap f g) (productMap f′ g′))
Proof / implementation
productMap₌ f f′ g g′ = productMap-cong pr₁ pr₂
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} whereproductMap-cong₂
Derivation, checked
productMap-cong₂ : {C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} {α α′ : f ＝ f′} {β β′ : g ＝ g′} → α =₁ α′ → β =₁ β′ → productMap-cong α β =₁ productMap-cong α′ β′
Proof / implementation
productMap-cong₂ p q = pair⁼-cong (preWhisker pr₁ ◁ p) (preWhisker pr₂ ◁ q)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-comp
Derivation, checked
productMap-cong-comp : {C C′ D D′ : CAT Γ} {f₀ f₁ f₂ : MAP C C′} {g₀ g₁ g₂ : MAP D D′} (α₂ : f₁ ＝ f₂) (α₁ : f₀ ＝ f₁) (β₂ : g₁ ＝ g₂) (β₁ : g₀ ＝ g₁) → productMap-cong (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (productMap-cong α₂ β₂ ∙ productMap-cong α₁ β₁)
Proof / implementation
productMap-cong-comp α₂ α₁ β₂ β₁ = pair⁼-comp (α₂ ▷ pr₁) (α₁ ▷ pr₁) (β₂ ▷ pr₂) (β₁ ▷ pr₂) ∙ pair⁼-cong (preWhisker-comp₌ α₂ α₁ pr₁) (preWhisker-comp₌ β₂ β₁ pr₂)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-pre
Derivation, checked
productMap-cong-pre : {B C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} (α : f ＝ f′) (β : g ＝ g′) (r : MAP B A) → (productMap-cong α β ∘ r) =₁ productMap-cong (α ∘ r) (β ∘ r)
Proof / implementation
productMap-cong-pre α β r = pair⁼-cong (preWhisker-pre α pr₁ r) (preWhisker-pre β pr₂ r) ∙ pair⁼-pre (α ▷ pr₁) (β ▷ pr₂) 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.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} wherepair-pre-id
Derivation, checked
pair-pre-id : {C D : CAT Γ} (x : Term C) (y : Term D) → (pair⁼ (comp-unitʳ x) (comp-unitʳ y) ∙ pair-pre x y (id X)) =₂ comp-unitʳ (pair x y)
Proof / implementation
pair-pre-id x y = pair₌-unique (pair-evaluation-over₁-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) (pair-evaluation-over₂-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) ((restrict-triangle-id pr₁ (pair x y) x (pair-β₁ x y)) ⁻¹) ((restrict-triangle-id pr₂ (pair x y) y (pair-β₂ x y)) ⁻¹)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.PairingRestriction where
module _ {Γ : Context} where
module _ {X : 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.
Lemma 1.3.16 (Pairing and precomposition). Let \(f\colon T\to C\), \(g\colon T\to D\), and \(\sigma \colon S\to T\) be functors. Pairing commutes with precomposition: there is an identification \[ (f,g)\circ \sigma =(f\circ \sigma ,g\circ \sigma ). \] This comparison is compatible with identifications of the input functors, with successive precomposition, and with precomposition by an identity functor, using the associativity and unitality identifications.
Agda Finite compatibility of products
pair⁼-functor
Derivation, checked
pair⁼-functor : {C D : CAT Γ} (x x′ : Term C) (y y′ : Term D) → MAP ((Equal x x′) × (Equal y y′)) (Equal (pair x y) (pair x′ y′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherepair⁼-cong
Derivation, checked
pair⁼-cong : {C D : CAT Γ} {x x′ : Term C} {y y′ : Term D} {α α′ : x ＝ x′} {β β′ : y ＝ y′} → α =₁ α′ → β =₁ β′ → pair⁼ α β =₁ pair⁼ α′ β′
Proof / implementation
pair⁼-cong {α = α} {α′} {β} {β′} p q = pair₌-unique (pair⁼-triangle₁ α β) (pair⁼-triangle₂ α β) (replace-edges₌ (id₌ (pr₁ ◁ pair⁼ α′ β′)) (p ⁻¹) (pair⁼-triangle₁ α′ β′)) (replace-edges₌ (id₌ (pr₂ ◁ pair⁼ α′ β′)) (q ⁻¹) (pair⁼-triangle₂ α′ β′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-comp
Derivation, checked
pair⁼-comp : {C D : CAT Γ} {x₀ x₁ x₂ : Term C} {y₀ y₁ y₂ : Term D} (α₂ : x₁ ＝ x₂) (α₁ : x₀ ＝ x₁) (β₂ : y₁ ＝ y₂) (β₁ : y₀ ＝ y₁) → pair⁼ (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (pair⁼ α₂ β₂ ∙ pair⁼ α₁ β₁)
Proof / implementation
pair⁼-comp α₂ α₁ β₂ β₁ = pair₌-unique (pair⁼-triangle₁ (α₂ ∙ α₁) (β₂ ∙ β₁)) (pair⁼-triangle₂ (α₂ ∙ α₁) (β₂ ∙ β₁)) (lies-over-comp pr₁ (pair⁼-triangle₁ α₁ β₁) (pair⁼-triangle₁ α₂ β₂)) (lies-over-comp pr₂ (pair⁼-triangle₂ α₁ β₁) (pair⁼-triangle₂ α₂ β₂))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-id
Derivation, checked
pair⁼-id : {C D : CAT Γ} (x : Term C) (y : Term D) → pair⁼ (const {P = A} (id₌ x)) (const (id₌ y)) =₁ const (id₌ (pair x y))
Proof / implementation
pair⁼-id x y = pair₌-unique (pair⁼-triangle₁ (const (id₌ x)) (const (id₌ y))) (pair⁼-triangle₂ (const (id₌ x)) (const (id₌ y))) (lies-over-id pr₁ (pair-β₁ x y)) (lies-over-id pr₂ (pair-β₂ x y))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} whereproductMap₌
Derivation, checked
productMap₌ : {C C′ D D′ : CAT Γ} (f f′ : MAP C C′) (g g′ : MAP D D′) → MAP ((Equal f f′) × (Equal g g′)) (Equal (productMap f g) (productMap f′ g′))
Proof / implementation
productMap₌ f f′ g g′ = productMap-cong pr₁ pr₂
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} whereproductMap-cong₂
Derivation, checked
productMap-cong₂ : {C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} {α α′ : f ＝ f′} {β β′ : g ＝ g′} → α =₁ α′ → β =₁ β′ → productMap-cong α β =₁ productMap-cong α′ β′
Proof / implementation
productMap-cong₂ p q = pair⁼-cong (preWhisker pr₁ ◁ p) (preWhisker pr₂ ◁ q)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-comp
Derivation, checked
productMap-cong-comp : {C C′ D D′ : CAT Γ} {f₀ f₁ f₂ : MAP C C′} {g₀ g₁ g₂ : MAP D D′} (α₂ : f₁ ＝ f₂) (α₁ : f₀ ＝ f₁) (β₂ : g₁ ＝ g₂) (β₁ : g₀ ＝ g₁) → productMap-cong (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (productMap-cong α₂ β₂ ∙ productMap-cong α₁ β₁)
Proof / implementation
productMap-cong-comp α₂ α₁ β₂ β₁ = pair⁼-comp (α₂ ▷ pr₁) (α₁ ▷ pr₁) (β₂ ▷ pr₂) (β₁ ▷ pr₂) ∙ pair⁼-cong (preWhisker-comp₌ α₂ α₁ pr₁) (preWhisker-comp₌ β₂ β₁ pr₂)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-pre
Derivation, checked
productMap-cong-pre : {B C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} (α : f ＝ f′) (β : g ＝ g′) (r : MAP B A) → (productMap-cong α β ∘ r) =₁ productMap-cong (α ∘ r) (β ∘ r)
Proof / implementation
productMap-cong-pre α β r = pair⁼-cong (preWhisker-pre α pr₁ r) (preWhisker-pre β pr₂ r) ∙ pair⁼-pre (α ▷ pr₁) (β ▷ pr₂) 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.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} wherepair-pre-id
Derivation, checked
pair-pre-id : {C D : CAT Γ} (x : Term C) (y : Term D) → (pair⁼ (comp-unitʳ x) (comp-unitʳ y) ∙ pair-pre x y (id X)) =₂ comp-unitʳ (pair x y)
Proof / implementation
pair-pre-id x y = pair₌-unique (pair-evaluation-over₁-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) (pair-evaluation-over₂-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) ((restrict-triangle-id pr₁ (pair x y) x (pair-β₁ x y)) ⁻¹) ((restrict-triangle-id pr₂ (pair x y) y (pair-β₂ x y)) ⁻¹)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.PairingRestriction 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.
Agda Finite compatibility of products step 2
pair⁼-functor
Derivation, checked
pair⁼-functor : {C D : CAT Γ} (x x′ : Term C) (y y′ : Term D) → MAP ((Equal x x′) × (Equal y y′)) (Equal (pair x y) (pair x′ y′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherepair⁼-cong
Derivation, checked
pair⁼-cong : {C D : CAT Γ} {x x′ : Term C} {y y′ : Term D} {α α′ : x ＝ x′} {β β′ : y ＝ y′} → α =₁ α′ → β =₁ β′ → pair⁼ α β =₁ pair⁼ α′ β′
Proof / implementation
pair⁼-cong {α = α} {α′} {β} {β′} p q = pair₌-unique (pair⁼-triangle₁ α β) (pair⁼-triangle₂ α β) (replace-edges₌ (id₌ (pr₁ ◁ pair⁼ α′ β′)) (p ⁻¹) (pair⁼-triangle₁ α′ β′)) (replace-edges₌ (id₌ (pr₂ ◁ pair⁼ α′ β′)) (q ⁻¹) (pair⁼-triangle₂ α′ β′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-comp
Derivation, checked
pair⁼-comp : {C D : CAT Γ} {x₀ x₁ x₂ : Term C} {y₀ y₁ y₂ : Term D} (α₂ : x₁ ＝ x₂) (α₁ : x₀ ＝ x₁) (β₂ : y₁ ＝ y₂) (β₁ : y₀ ＝ y₁) → pair⁼ (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (pair⁼ α₂ β₂ ∙ pair⁼ α₁ β₁)
Proof / implementation
pair⁼-comp α₂ α₁ β₂ β₁ = pair₌-unique (pair⁼-triangle₁ (α₂ ∙ α₁) (β₂ ∙ β₁)) (pair⁼-triangle₂ (α₂ ∙ α₁) (β₂ ∙ β₁)) (lies-over-comp pr₁ (pair⁼-triangle₁ α₁ β₁) (pair⁼-triangle₁ α₂ β₂)) (lies-over-comp pr₂ (pair⁼-triangle₂ α₁ β₁) (pair⁼-triangle₂ α₂ β₂))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-id
Derivation, checked
pair⁼-id : {C D : CAT Γ} (x : Term C) (y : Term D) → pair⁼ (const {P = A} (id₌ x)) (const (id₌ y)) =₁ const (id₌ (pair x y))
Proof / implementation
pair⁼-id x y = pair₌-unique (pair⁼-triangle₁ (const (id₌ x)) (const (id₌ y))) (pair⁼-triangle₂ (const (id₌ x)) (const (id₌ y))) (lies-over-id pr₁ (pair-β₁ x y)) (lies-over-id pr₂ (pair-β₂ x y))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} whereproductMap₌
Derivation, checked
productMap₌ : {C C′ D D′ : CAT Γ} (f f′ : MAP C C′) (g g′ : MAP D D′) → MAP ((Equal f f′) × (Equal g g′)) (Equal (productMap f g) (productMap f′ g′))
Proof / implementation
productMap₌ f f′ g g′ = productMap-cong pr₁ pr₂
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} whereproductMap-cong₂
Derivation, checked
productMap-cong₂ : {C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} {α α′ : f ＝ f′} {β β′ : g ＝ g′} → α =₁ α′ → β =₁ β′ → productMap-cong α β =₁ productMap-cong α′ β′
Proof / implementation
productMap-cong₂ p q = pair⁼-cong (preWhisker pr₁ ◁ p) (preWhisker pr₂ ◁ q)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-comp
Derivation, checked
productMap-cong-comp : {C C′ D D′ : CAT Γ} {f₀ f₁ f₂ : MAP C C′} {g₀ g₁ g₂ : MAP D D′} (α₂ : f₁ ＝ f₂) (α₁ : f₀ ＝ f₁) (β₂ : g₁ ＝ g₂) (β₁ : g₀ ＝ g₁) → productMap-cong (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (productMap-cong α₂ β₂ ∙ productMap-cong α₁ β₁)
Proof / implementation
productMap-cong-comp α₂ α₁ β₂ β₁ = pair⁼-comp (α₂ ▷ pr₁) (α₁ ▷ pr₁) (β₂ ▷ pr₂) (β₁ ▷ pr₂) ∙ pair⁼-cong (preWhisker-comp₌ α₂ α₁ pr₁) (preWhisker-comp₌ β₂ β₁ pr₂)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-pre
Derivation, checked
productMap-cong-pre : {B C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} (α : f ＝ f′) (β : g ＝ g′) (r : MAP B A) → (productMap-cong α β ∘ r) =₁ productMap-cong (α ∘ r) (β ∘ r)
Proof / implementation
productMap-cong-pre α β r = pair⁼-cong (preWhisker-pre α pr₁ r) (preWhisker-pre β pr₂ r) ∙ pair⁼-pre (α ▷ pr₁) (β ▷ pr₂) 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.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} wherepair-pre-id
Derivation, checked
pair-pre-id : {C D : CAT Γ} (x : Term C) (y : Term D) → (pair⁼ (comp-unitʳ x) (comp-unitʳ y) ∙ pair-pre x y (id X)) =₂ comp-unitʳ (pair x y)
Proof / implementation
pair-pre-id x y = pair₌-unique (pair-evaluation-over₁-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) (pair-evaluation-over₂-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) ((restrict-triangle-id pr₁ (pair x y) x (pair-β₁ x y)) ⁻¹) ((restrict-triangle-id pr₂ (pair x y) y (pair-β₂ x y)) ⁻¹)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.PairingRestriction where
module _ {Γ : Context} where
module _ {X : 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.
Proof
Proof. After composition with \(\pr _1\) and \(\pr _2\), both sides identify with \(f\circ \sigma \) and \(g\circ \sigma \), respectively. The product axiom therefore supplies the comparison, with these prescribed projections. Its compatibilities can likewise be checked after applying both projections, where they reduce to the coherence laws for composition and identifications. For compatibility with identity functors, one also uses \[ \rho _{ab}=(a\star \rho _b)\circ \alpha _{\id ,b,a} \tag{1.1}\] for composable functors \(b,a\). This follows by prewhiskering with the identity, applying the pentagon for \(a,b,\id ,\id \) and the triangle identities, and cancelling by Lemma 1.3.10. We leave the remaining checks to the reader. □
Agda Finite compatibility of products step 5
pair⁼-functor
Derivation, checked
pair⁼-functor : {C D : CAT Γ} (x x′ : Term C) (y y′ : Term D) → MAP ((Equal x x′) × (Equal y y′)) (Equal (pair x y) (pair x′ y′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherepair⁼-cong
Derivation, checked
pair⁼-cong : {C D : CAT Γ} {x x′ : Term C} {y y′ : Term D} {α α′ : x ＝ x′} {β β′ : y ＝ y′} → α =₁ α′ → β =₁ β′ → pair⁼ α β =₁ pair⁼ α′ β′
Proof / implementation
pair⁼-cong {α = α} {α′} {β} {β′} p q = pair₌-unique (pair⁼-triangle₁ α β) (pair⁼-triangle₂ α β) (replace-edges₌ (id₌ (pr₁ ◁ pair⁼ α′ β′)) (p ⁻¹) (pair⁼-triangle₁ α′ β′)) (replace-edges₌ (id₌ (pr₂ ◁ pair⁼ α′ β′)) (q ⁻¹) (pair⁼-triangle₂ α′ β′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-comp
Derivation, checked
pair⁼-comp : {C D : CAT Γ} {x₀ x₁ x₂ : Term C} {y₀ y₁ y₂ : Term D} (α₂ : x₁ ＝ x₂) (α₁ : x₀ ＝ x₁) (β₂ : y₁ ＝ y₂) (β₁ : y₀ ＝ y₁) → pair⁼ (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (pair⁼ α₂ β₂ ∙ pair⁼ α₁ β₁)
Proof / implementation
pair⁼-comp α₂ α₁ β₂ β₁ = pair₌-unique (pair⁼-triangle₁ (α₂ ∙ α₁) (β₂ ∙ β₁)) (pair⁼-triangle₂ (α₂ ∙ α₁) (β₂ ∙ β₁)) (lies-over-comp pr₁ (pair⁼-triangle₁ α₁ β₁) (pair⁼-triangle₁ α₂ β₂)) (lies-over-comp pr₂ (pair⁼-triangle₂ α₁ β₁) (pair⁼-triangle₂ α₂ β₂))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-id
Derivation, checked
pair⁼-id : {C D : CAT Γ} (x : Term C) (y : Term D) → pair⁼ (const {P = A} (id₌ x)) (const (id₌ y)) =₁ const (id₌ (pair x y))
Proof / implementation
pair⁼-id x y = pair₌-unique (pair⁼-triangle₁ (const (id₌ x)) (const (id₌ y))) (pair⁼-triangle₂ (const (id₌ x)) (const (id₌ y))) (lies-over-id pr₁ (pair-β₁ x y)) (lies-over-id pr₂ (pair-β₂ x y))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} whereproductMap₌
Derivation, checked
productMap₌ : {C C′ D D′ : CAT Γ} (f f′ : MAP C C′) (g g′ : MAP D D′) → MAP ((Equal f f′) × (Equal g g′)) (Equal (productMap f g) (productMap f′ g′))
Proof / implementation
productMap₌ f f′ g g′ = productMap-cong pr₁ pr₂
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} whereproductMap-cong₂
Derivation, checked
productMap-cong₂ : {C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} {α α′ : f ＝ f′} {β β′ : g ＝ g′} → α =₁ α′ → β =₁ β′ → productMap-cong α β =₁ productMap-cong α′ β′
Proof / implementation
productMap-cong₂ p q = pair⁼-cong (preWhisker pr₁ ◁ p) (preWhisker pr₂ ◁ q)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-comp
Derivation, checked
productMap-cong-comp : {C C′ D D′ : CAT Γ} {f₀ f₁ f₂ : MAP C C′} {g₀ g₁ g₂ : MAP D D′} (α₂ : f₁ ＝ f₂) (α₁ : f₀ ＝ f₁) (β₂ : g₁ ＝ g₂) (β₁ : g₀ ＝ g₁) → productMap-cong (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (productMap-cong α₂ β₂ ∙ productMap-cong α₁ β₁)
Proof / implementation
productMap-cong-comp α₂ α₁ β₂ β₁ = pair⁼-comp (α₂ ▷ pr₁) (α₁ ▷ pr₁) (β₂ ▷ pr₂) (β₁ ▷ pr₂) ∙ pair⁼-cong (preWhisker-comp₌ α₂ α₁ pr₁) (preWhisker-comp₌ β₂ β₁ pr₂)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-pre
Derivation, checked
productMap-cong-pre : {B C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} (α : f ＝ f′) (β : g ＝ g′) (r : MAP B A) → (productMap-cong α β ∘ r) =₁ productMap-cong (α ∘ r) (β ∘ r)
Proof / implementation
productMap-cong-pre α β r = pair⁼-cong (preWhisker-pre α pr₁ r) (preWhisker-pre β pr₂ r) ∙ pair⁼-pre (α ▷ pr₁) (β ▷ pr₂) 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.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} wherepair-pre-id
Derivation, checked
pair-pre-id : {C D : CAT Γ} (x : Term C) (y : Term D) → (pair⁼ (comp-unitʳ x) (comp-unitʳ y) ∙ pair-pre x y (id X)) =₂ comp-unitʳ (pair x y)
Proof / implementation
pair-pre-id x y = pair₌-unique (pair-evaluation-over₁-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) (pair-evaluation-over₂-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) ((restrict-triangle-id pr₁ (pair x y) x (pair-β₁ x y)) ⁻¹) ((restrict-triangle-id pr₂ (pair x y) y (pair-β₂ x y)) ⁻¹)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.PairingRestriction where
module _ {Γ : Context} where
module _ {X : 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.
Agda Finite compatibility of products step 8
pair⁼-functor
Derivation, checked
pair⁼-functor : {C D : CAT Γ} (x x′ : Term C) (y y′ : Term D) → MAP ((Equal x x′) × (Equal y y′)) (Equal (pair x y) (pair x′ y′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherepair⁼-cong
Derivation, checked
pair⁼-cong : {C D : CAT Γ} {x x′ : Term C} {y y′ : Term D} {α α′ : x ＝ x′} {β β′ : y ＝ y′} → α =₁ α′ → β =₁ β′ → pair⁼ α β =₁ pair⁼ α′ β′
Proof / implementation
pair⁼-cong {α = α} {α′} {β} {β′} p q = pair₌-unique (pair⁼-triangle₁ α β) (pair⁼-triangle₂ α β) (replace-edges₌ (id₌ (pr₁ ◁ pair⁼ α′ β′)) (p ⁻¹) (pair⁼-triangle₁ α′ β′)) (replace-edges₌ (id₌ (pr₂ ◁ pair⁼ α′ β′)) (q ⁻¹) (pair⁼-triangle₂ α′ β′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-comp
Derivation, checked
pair⁼-comp : {C D : CAT Γ} {x₀ x₁ x₂ : Term C} {y₀ y₁ y₂ : Term D} (α₂ : x₁ ＝ x₂) (α₁ : x₀ ＝ x₁) (β₂ : y₁ ＝ y₂) (β₁ : y₀ ＝ y₁) → pair⁼ (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (pair⁼ α₂ β₂ ∙ pair⁼ α₁ β₁)
Proof / implementation
pair⁼-comp α₂ α₁ β₂ β₁ = pair₌-unique (pair⁼-triangle₁ (α₂ ∙ α₁) (β₂ ∙ β₁)) (pair⁼-triangle₂ (α₂ ∙ α₁) (β₂ ∙ β₁)) (lies-over-comp pr₁ (pair⁼-triangle₁ α₁ β₁) (pair⁼-triangle₁ α₂ β₂)) (lies-over-comp pr₂ (pair⁼-triangle₂ α₁ β₁) (pair⁼-triangle₂ α₂ β₂))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-id
Derivation, checked
pair⁼-id : {C D : CAT Γ} (x : Term C) (y : Term D) → pair⁼ (const {P = A} (id₌ x)) (const (id₌ y)) =₁ const (id₌ (pair x y))
Proof / implementation
pair⁼-id x y = pair₌-unique (pair⁼-triangle₁ (const (id₌ x)) (const (id₌ y))) (pair⁼-triangle₂ (const (id₌ x)) (const (id₌ y))) (lies-over-id pr₁ (pair-β₁ x y)) (lies-over-id pr₂ (pair-β₂ x y))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} whereproductMap₌
Derivation, checked
productMap₌ : {C C′ D D′ : CAT Γ} (f f′ : MAP C C′) (g g′ : MAP D D′) → MAP ((Equal f f′) × (Equal g g′)) (Equal (productMap f g) (productMap f′ g′))
Proof / implementation
productMap₌ f f′ g g′ = productMap-cong pr₁ pr₂
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} whereproductMap-cong₂
Derivation, checked
productMap-cong₂ : {C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} {α α′ : f ＝ f′} {β β′ : g ＝ g′} → α =₁ α′ → β =₁ β′ → productMap-cong α β =₁ productMap-cong α′ β′
Proof / implementation
productMap-cong₂ p q = pair⁼-cong (preWhisker pr₁ ◁ p) (preWhisker pr₂ ◁ q)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-comp
Derivation, checked
productMap-cong-comp : {C C′ D D′ : CAT Γ} {f₀ f₁ f₂ : MAP C C′} {g₀ g₁ g₂ : MAP D D′} (α₂ : f₁ ＝ f₂) (α₁ : f₀ ＝ f₁) (β₂ : g₁ ＝ g₂) (β₁ : g₀ ＝ g₁) → productMap-cong (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (productMap-cong α₂ β₂ ∙ productMap-cong α₁ β₁)
Proof / implementation
productMap-cong-comp α₂ α₁ β₂ β₁ = pair⁼-comp (α₂ ▷ pr₁) (α₁ ▷ pr₁) (β₂ ▷ pr₂) (β₁ ▷ pr₂) ∙ pair⁼-cong (preWhisker-comp₌ α₂ α₁ pr₁) (preWhisker-comp₌ β₂ β₁ pr₂)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-pre
Derivation, checked
productMap-cong-pre : {B C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} (α : f ＝ f′) (β : g ＝ g′) (r : MAP B A) → (productMap-cong α β ∘ r) =₁ productMap-cong (α ∘ r) (β ∘ r)
Proof / implementation
productMap-cong-pre α β r = pair⁼-cong (preWhisker-pre α pr₁ r) (preWhisker-pre β pr₂ r) ∙ pair⁼-pre (α ▷ pr₁) (β ▷ pr₂) 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.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} wherepair-pre-id
Derivation, checked
pair-pre-id : {C D : CAT Γ} (x : Term C) (y : Term D) → (pair⁼ (comp-unitʳ x) (comp-unitʳ y) ∙ pair-pre x y (id X)) =₂ comp-unitʳ (pair x y)
Proof / implementation
pair-pre-id x y = pair₌-unique (pair-evaluation-over₁-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) (pair-evaluation-over₂-One x y (id _) (comp-unitʳ x) (comp-unitʳ y)) ((restrict-triangle-id pr₁ (pair x y) x (pair-β₁ x y)) ⁻¹) ((restrict-triangle-id pr₂ (pair x y) y (pair-β₂ x y)) ⁻¹)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.PairingRestriction where
module _ {Γ : Context} where
module _ {X : 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.
Construction 1.3.17. The formation of products of categories is functorial: given \(f\colon C\to C'\) and \(g\colon D\to D'\), we obtain a functor \[ f\times g:=(f\pr _1,g\pr _2):C\times D\to C'\times D'. \] For identifications \(\varphi : f = f'\) and \(\psi : g = g'\) between functors with these same sources and targets, we define \[ \varphi \times \psi :=(\varphi \star \pr _1,\psi \star \pr _2). \] This gives a functor on the product of the two animae of identifications. It preserves identity identifications and vertical composition by Construction 1.3.15 and the corresponding laws for whiskering.
Agda Functoriality of products
pair⁼-functor
Derivation, checked
pair⁼-functor : {C D : CAT Γ} (x x′ : Term C) (y y′ : Term D) → MAP ((Equal x x′) × (Equal y y′)) (Equal (pair x y) (pair x′ y′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherepair⁼-cong
Derivation, checked
pair⁼-cong : {C D : CAT Γ} {x x′ : Term C} {y y′ : Term D} {α α′ : x ＝ x′} {β β′ : y ＝ y′} → α =₁ α′ → β =₁ β′ → pair⁼ α β =₁ pair⁼ α′ β′
Proof / implementation
pair⁼-cong {α = α} {α′} {β} {β′} p q = pair₌-unique (pair⁼-triangle₁ α β) (pair⁼-triangle₂ α β) (replace-edges₌ (id₌ (pr₁ ◁ pair⁼ α′ β′)) (p ⁻¹) (pair⁼-triangle₁ α′ β′)) (replace-edges₌ (id₌ (pr₂ ◁ pair⁼ α′ β′)) (q ⁻¹) (pair⁼-triangle₂ α′ β′))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-comp
Derivation, checked
pair⁼-comp : {C D : CAT Γ} {x₀ x₁ x₂ : Term C} {y₀ y₁ y₂ : Term D} (α₂ : x₁ ＝ x₂) (α₁ : x₀ ＝ x₁) (β₂ : y₁ ＝ y₂) (β₁ : y₀ ＝ y₁) → pair⁼ (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (pair⁼ α₂ β₂ ∙ pair⁼ α₁ β₁)
Proof / implementation
pair⁼-comp α₂ α₁ β₂ β₁ = pair₌-unique (pair⁼-triangle₁ (α₂ ∙ α₁) (β₂ ∙ β₁)) (pair⁼-triangle₂ (α₂ ∙ α₁) (β₂ ∙ β₁)) (lies-over-comp pr₁ (pair⁼-triangle₁ α₁ β₁) (pair⁼-triangle₁ α₂ β₂)) (lies-over-comp pr₂ (pair⁼-triangle₂ α₁ β₁) (pair⁼-triangle₂ α₂ β₂))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} wherepair⁼-id
Derivation, checked
pair⁼-id : {C D : CAT Γ} (x : Term C) (y : Term D) → pair⁼ (const {P = A} (id₌ x)) (const (id₌ y)) =₁ const (id₌ (pair x y))
Proof / implementation
pair⁼-id x y = pair₌-unique (pair⁼-triangle₁ (const (id₌ x)) (const (id₌ y))) (pair⁼-triangle₂ (const (id₌ x)) (const (id₌ y))) (lies-over-id pr₁ (pair-β₁ x y)) (lies-over-id pr₂ (pair-β₂ x y))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.Pairing where
module _ {Γ : Context} where
module _ {A X : CAT Γ} whereproductMap₌
Derivation, checked
productMap₌ : {C C′ D D′ : CAT Γ} (f f′ : MAP C C′) (g g′ : MAP D D′) → MAP ((Equal f f′) × (Equal g g′)) (Equal (productMap f g) (productMap f′ g′))
Proof / implementation
productMap₌ f f′ g g′ = productMap-cong pr₁ pr₂
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} whereproductMap-cong₂
Derivation, checked
productMap-cong₂ : {C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} {α α′ : f ＝ f′} {β β′ : g ＝ g′} → α =₁ α′ → β =₁ β′ → productMap-cong α β =₁ productMap-cong α′ β′
Proof / implementation
productMap-cong₂ p q = pair⁼-cong (preWhisker pr₁ ◁ p) (preWhisker pr₂ ◁ q)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-comp
Derivation, checked
productMap-cong-comp : {C C′ D D′ : CAT Γ} {f₀ f₁ f₂ : MAP C C′} {g₀ g₁ g₂ : MAP D D′} (α₂ : f₁ ＝ f₂) (α₁ : f₀ ＝ f₁) (β₂ : g₁ ＝ g₂) (β₁ : g₀ ＝ g₁) → productMap-cong (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (productMap-cong α₂ β₂ ∙ productMap-cong α₁ β₁)
Proof / implementation
productMap-cong-comp α₂ α₁ β₂ β₁ = pair⁼-comp (α₂ ▷ pr₁) (α₁ ▷ pr₁) (β₂ ▷ pr₂) (β₁ ▷ pr₂) ∙ pair⁼-cong (preWhisker-comp₌ α₂ α₁ pr₁) (preWhisker-comp₌ β₂ β₁ pr₂)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-pre
Derivation, checked
productMap-cong-pre : {B C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} (α : f ＝ f′) (β : g ＝ g′) (r : MAP B A) → (productMap-cong α β ∘ r) =₁ productMap-cong (α ∘ r) (β ∘ r)
Proof / implementation
productMap-cong-pre α β r = pair⁼-cong (preWhisker-pre α pr₁ r) (preWhisker-pre β pr₂ r) ∙ pair⁼-pre (α ▷ pr₁) (β ▷ pr₂) 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.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : 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.
Exercise 1.3.18 (Exercise 1.9.3 (outside selection)). Show that there are identifications \begin {align*} \id _C\times \id _D&=\id _{C\times D},\\ (f'\times g')\circ (f\times g)&=(f'f)\times (g'g) \end {align*}
Agda Functoriality products
productMap₌
Derivation, checked
productMap₌ : {C C′ D D′ : CAT Γ} (f f′ : MAP C C′) (g g′ : MAP D D′) → MAP ((Equal f f′) × (Equal g g′)) (Equal (productMap f g) (productMap f′ g′))
Proof / implementation
productMap₌ f f′ g g′ = productMap-cong pr₁ pr₂
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} whereproductMap-cong₂
Derivation, checked
productMap-cong₂ : {C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} {α α′ : f ＝ f′} {β β′ : g ＝ g′} → α =₁ α′ → β =₁ β′ → productMap-cong α β =₁ productMap-cong α′ β′
Proof / implementation
productMap-cong₂ p q = pair⁼-cong (preWhisker pr₁ ◁ p) (preWhisker pr₂ ◁ q)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-comp
Derivation, checked
productMap-cong-comp : {C C′ D D′ : CAT Γ} {f₀ f₁ f₂ : MAP C C′} {g₀ g₁ g₂ : MAP D D′} (α₂ : f₁ ＝ f₂) (α₁ : f₀ ＝ f₁) (β₂ : g₁ ＝ g₂) (β₁ : g₀ ＝ g₁) → productMap-cong (α₂ ∙ α₁) (β₂ ∙ β₁) =₁ (productMap-cong α₂ β₂ ∙ productMap-cong α₁ β₁)
Proof / implementation
productMap-cong-comp α₂ α₁ β₂ β₁ = pair⁼-comp (α₂ ▷ pr₁) (α₁ ▷ pr₁) (β₂ ▷ pr₂) (β₁ ▷ pr₂) ∙ pair⁼-cong (preWhisker-comp₌ α₂ α₁ pr₁) (preWhisker-comp₌ β₂ β₁ pr₂)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereproductMap-cong-pre
Derivation, checked
productMap-cong-pre : {B C C′ D D′ : CAT Γ} {f f′ : MAP C C′} {g g′ : MAP D D′} (α : f ＝ f′) (β : g ＝ g′) (r : MAP B A) → (productMap-cong α β ∘ r) =₁ productMap-cong (α ∘ r) (β ∘ r)
Proof / implementation
productMap-cong-pre α β r = pair⁼-cong (preWhisker-pre α pr₁ r) (preWhisker-pre β pr₂ r) ∙ pair⁼-pre (α ▷ pr₁) (β ▷ pr₂) 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.Section03.Products.ProductFunctor where
module _ {Γ : Context} where
module _ {A : 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.
for \(f\colon C\to C'\), \(f'\colon C'\to C''\), \(g\colon D\to D'\), and \(g'\colon D'\to D''\).
Supplementary notes
- Changing endpoints in identification animae AI-generated
- Pairing and precomposition AI-generated