Read the Agda code alongside the book.Click dotted-underlined prose to read its Agda code alongside the book. Browse all code.
2.2 The Segal axiom
In this section, we will introduce the Segal axiom, which will provide unique compositions of morphisms in categories.
Axiom E (Segal axiom). For any category \(C\), the functor \[ (d_2^*,d_0^*)\colon \Triang (C) \to \Ar (C) \times _C \Ar (C) \] is an equivalence.
Agda The Segal axiom
segal-isEquiv
Assumption, type checked
segal-isEquiv : (C : CAT Γ) → IsEquiv (short-edges C)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.SegalAxiom where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
In particular, for every pair of composable morphisms \(f\colon x \to y\) and \(g\colon y \to z\) in \(C\) the category \(\Comp _{f,g}(C)\) of composites of \(f\) and \(g\) is contractible, being defined as the fiber of the equivalence \((d_2^*,d_0^*)\).
Agda The category of composites is contractible
composites-contractible
Derivation, checked
composites-contractible : {C : CAT Γ} (p : MAP One (Composable C)) → IsContractible (Composites p)
Proof / implementation
composites-contractible p = equiv-transport (terminal-identification (Completions.base p) (terminate (Composites p))) (completion-projection-isEquiv p)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.SegalAxiom where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Notation 2.2.1. In a common categorical context \(\Gamma \), composable morphisms \(\Gamma \vdash f\colon x\to y\) and \(\Gamma \vdash g\colon y\to z\) determine a term \[ \Gamma \vdash g\circ f\colon x\to z, \] which we call their unique composite. It comes with a chosen \(2\)-simplex \(\sigma \) and specified identifications \(d_2^*(\sigma )= f\), \(d_0^*(\sigma )= g\), and \(d_1^*(\sigma )= g\circ f\).
Agda The chosen composite
compose
Definition, checked
compose : {P : CAT Γ} {f g h : MAP P C} → MorphismFamily g h → MorphismFamily f g → MorphismFamily f h
Proof / implementation
compose = Composite.value
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module Composition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda A triangle presenting the composite
composition-presentation
Definition, checked
composition-presentation : {P : CAT Γ} {f g h : MAP P C} (beta : MorphismFamily g h) (alpha : MorphismFamily f g) → TrianglePresentation alpha beta (Chosen.compose beta alpha)
Proof / implementation
composition-presentation beta alpha = ReplacePresentation.value Completed.presentation (id-family-comparison alpha) (id-family-comparison beta) (inverse-family-comparison Completed.composite) where module Completed = CompletePair segal alpha beta
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionComparisons where
module CompositionComparisons {Γ : Context} (C : CAT Γ) (segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Observation 2.2.2 (Exercise 2.6.1). Let \(C_0\) and \(C_1\) be categories and consider morphisms \(f_0\colon x_0 \to y_0\) and \(g_0\colon y_0 \to z_0\) in \(C_0\) and morphisms \(f_1\colon x_1 \to y_1\) and \(g_1\colon y_1 \to z_1\) in \(C_1\). Then the composite \((g_0,g_1) \circ (f_0,f_1)\colon (x_0,x_1) \to (z_0,z_1)\) in \(C_0 \times C_1\) is given by \((g_0 \circ f_0, g_1 \circ f_1)\).
Agda Composition in products
product-composition
Derivation, checked
product-composition : MorphismFamilyIdentification One chosen-product-composite paired-component-composite
Proof / implementation
product-composition = product-family-reflect {alpha = chosen-product-composite} {beta = paired-component-composite} first-projected-product-composition second-projected-product-composition
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.ProductMorphismFamilies where
module ProductComposition {Γ : Context} (C D : CAT Γ)
(product-segal : IsEquiv (short-edges (C × D)))
(left-segal : IsEquiv (short-edges C)) (right-segal : IsEquiv (short-edges D)) where
module _ {P : CAT Γ} {x₁ y₁ z₁ : MAP P C} {x₂ y₂ z₂ : MAP P D}
(beta₁ : MorphismFamily y₁ z₁) (alpha₁ : MorphismFamily x₁ y₁)
(beta₂ : MorphismFamily y₂ z₂) (alpha₂ : MorphismFamily x₂ y₂) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
For fixed objects \(x,y,z:C\), the definition of \(g\circ f\) works for expressions with values in \(C(x,y)\) and \(C(y,z)\) and a common source. Thus composition is functorial in \(f\) and \(g\). We may make this functoriality more explicit as follows:
Agda Composition is functorial
value
Definition, checked
value : MAP (Hom C y z × Hom C x y) (Hom C x z)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module HomComposition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) (x y z : MAP One C) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Construction 2.2.3 (Composition functors). The Segal axiom gives an equivalence \[ q_C=(d_2^*,d_0^*)\colon \Triang (C)\longrightarrow \Ar (C) \times _C \Ar (C). \] Here the identification joining the two short edges is induced by \(d_2(1)=\overline 1=d_0(0)\) from Lemma 2.1.16. The vertex identifications of that lemma make \(q_C\) a functor over \(C^3\): on triangles we evaluate at \(\overline 0,\overline 1,\overline 2\), and on composable pairs we take the source and target of the first edge and the target of the second.
Agda The composition functor
compose
Definition, checked
compose : {P : CAT Γ} {f g h : MAP P C} → MorphismFamily g h → MorphismFamily f g → MorphismFamily f h
Proof / implementation
compose = Composite.value
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module Composition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) wherevalue
Definition, checked
value : MAP (Hom C y z × Hom C x y) (Hom C x z)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module HomComposition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) (x y z : MAP One C) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Choose an inverse \(j_C\) over \(C^3\), together with an identification \(\varepsilon _C\colon q_Cj_C=\id \) over \(C^3\). Composition is the functor \[ \Ar (C) \times _C \Ar (C) \xrightarrow {j_C}\Triang (C) \xrightarrow {d_1^*}\Ar (C). \] Thus we first complete a composable pair \((f,g)\) to a triangle, and then take its long edge. We denote this edge by \(g\circ f\).
Agda The chosen Segal inverse
completion
Definition, checked
completion : MAP (Composable C) (Triangles C)
Proof / implementation
completion = FunctorOverBase.functor completion-over
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.SegalComposition where
module ChosenComposition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The short-edge counit
completion-image
Derivation, checked
completion-image : ConeIdentification₁ (cone-restrict completion (triangle-cone C)) (pullback-cone (ev₁ {C = C}) ev₀)
Proof / implementation
completion-image = inverse-cone-comparison (triangle-cone C) segal
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.SegalComposition where
module ChosenComposition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Take the long edge
composition
Definition, checked
composition : MAP (Composable C) (Ar C)
Proof / implementation
composition = FunctorOverBase.functor composition-over
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.SegalComposition where
module ChosenComposition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The vertex identifications of Lemma 2.1.16 also identify the endpoints of the long edge with the first and last vertices. Hence composition is a functor over \(C\times C\). Passing to fibers over prescribed vertices \(x,y,z\) gives a functor \[ -\circ -\colon C(y,z)\times C(x,y)\longrightarrow C(x,z). \] The source and target identifications of \(g\circ f\) are obtained from these vertex comparisons followed by the corresponding components of \(\varepsilon _C\). Different choices of the inverse give identified composition functors over \(C\times C\).
Agda Endpoints of composition
endpoint-frame
Derivation, checked
endpoint-frame : (pair ev₀ ev₁ ∘ arrow) =₁ pair f h
Proof / implementation
endpoint-frame = Input.outer-frame ∙ FunctorOverBase.cell over
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module Composition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) where
module Composite {P : CAT Γ} {f g h : MAP P C}
(β : MorphismFamily g h) (α : MorphismFamily f g) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The fixed-endpoint composition functor
value
Definition, checked
value : MAP (Hom C y z × Hom C x y) (Hom C x z)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module HomComposition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) (x y z : MAP One C) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The specified endpoint identifications
endpoint-frame
Derivation, checked
endpoint-frame : (pair ev₀ ev₁ ∘ arrow) =₁ pair f h
Proof / implementation
endpoint-frame = Input.outer-frame ∙ FunctorOverBase.cell over
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module Composition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) where
module Composite {P : CAT Γ} {f g h : MAP P C}
(β : MorphismFamily g h) (α : MorphismFamily f g) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Independence of the composition choice
presented-composition
Derivation, checked
presented-composition : {P C : CAT Γ} {f g h : MAP P C} (segal : IsEquiv (short-edges C)) (alpha : MorphismFamily f g) (beta : MorphismFamily g h) (gamma : MorphismFamily f h) → TrianglePresentation alpha beta gamma → MorphismFamilyIdentification One (MC.Composition.compose C segal beta alpha) gamma
Proof / implementation
presented-composition {C = C} segal alpha beta gamma given = Chosen.comparison gamma T.long Endpoint.compatible where module T = PresentedTriangle given module Endpoint = TriangleEndpointComparison alpha beta gamma T.triangle T.short-comparison T.long T.source-compatible T.target-compatible module Chosen = CompositionPresentation C segal beta alpha T.triangle Endpoint.Short.identification
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.FramedTrianglePresentations where
module _ {Γ : Context} whereAbout this correspondence
Related supporting result only: presented-composition compares a fixed chosen composition with a supplied triangle presentation for one Segal witness. It does not prove the manuscript’s comparison between arbitrary choices of the Segal inverse as functors over C × C.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Convention 2.2.4 (Composition of morphism expressions). For functors \(f,g,h\colon C\to D\), consider morphism expressions \(\alpha (x):f(x)\to g(x)\) and \(\beta (x):g(x)\to h(x)\) in context \(x:C\). Their endpoint identifications define a functor \(C\to \Ar (D)\times _D\Ar (D)\). Composing with the composition functor gives a morphism expression \[ \beta (x)\circ \alpha (x):f(x)\to h(x). \] This construction also acts on identifications of morphism expressions that retain the endpoints.
Agda Composition of morphism expressions
compose
Definition, checked
compose : {P : CAT Γ} {f g h : MAP P C} → MorphismFamily g h → MorphismFamily f g → MorphismFamily f h
Proof / implementation
compose = Composite.value
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module Composition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda A composable pair of expressions
pair-map
Definition, checked
pair-map : MAP P (Composable C)
Proof / implementation
pair-map = pullback-factor cone
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module ComposableFamilies {Γ : Context} {P C : CAT Γ}
{f g h : MAP P C} (α : MorphismFamily f g) (β : MorphismFamily g h) wherepair-image
Derivation, checked
pair-image : ConeIdentification₁ (cone-restrict pair-map (pullback-cone ev₁ ev₀)) cone
Proof / implementation
pair-image = pullback-factor-β cone
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismComposition where
module ComposableFamilies {Γ : Context} {P C : CAT Γ}
{f g h : MAP P C} (α : MorphismFamily f g) (β : MorphismFamily g h) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Composition acts on endpoint-preserving identifications
composition-comparison
Derivation, checked
composition-comparison : {P : CAT Γ} {f g h : MAP P C} {alpha alpha′ : MorphismFamily f g} {beta beta′ : MorphismFamily g h} → MorphismFamilyIdentification One beta beta′ → MorphismFamilyIdentification One alpha alpha′ → MorphismFamilyIdentification One (Chosen.compose beta alpha) (Chosen.compose beta′ alpha′)
Proof / implementation
composition-comparison {alpha = alpha} {alpha′} {beta} {beta′} second first = inverse-family-comparison (presented-composition segal alpha′ beta′ (Chosen.compose beta alpha) (ReplacePresentation.value (composition-presentation beta alpha) first second (id-family-comparison (Chosen.compose beta alpha))))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionComparisons where
module CompositionComparisons {Γ : Context} (C : CAT Γ) (segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Lemma 2.2.5. For a functor \(F\colon C \to D\) and morphisms \(f\colon x \to y\) and \(g\colon y \to z\) in \(C\), there is an identification \[ F(g \circ f) = F(g) \circ F(f) \] in \(D(F(x),F(z))\). This identification is natural in the pair \((g,f)\): it forms an identification over \(D \times D\) between two functors \(\Ar (C) \times _C \Ar (C) \to \Ar (D)\).
Agda Functors preserve composition
preserves-composition
Derivation, checked
preserves-composition : {P : CAT Γ} {f g h : MAP P C} (beta : MorphismFamily g h) (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (map-morphism-family F (MC.Composition.compose C source-segal beta alpha)) (MC.Composition.compose D target-segal (map-morphism-family F beta) (map-morphism-family F alpha))
Proof / implementation
preserves-composition beta alpha = family-comparison _ _ ((Target.identification ⁻¹) ∙ Source.identification) (compatible-quotient ev₀ _ _ _ Source.identification Target.identification Source.source Target.source) (compatible-quotient ev₁ _ _ _ Source.identification Target.identification Source.target Target.target) where module Completed = CompletePair source-segal alpha beta module Source = FamilyComparison (post-family-comparison F Completed.composite) module Target = FamilyComparison (PostPresentation.composite F Completed.presentation target-segal)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionPostcomposition where
module FunctorComposition {Γ : Context} {C D : CAT Γ} (F : MAP C D)
(source-segal : IsEquiv (short-edges C)) (target-segal : IsEquiv (short-edges D)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. Consider the chosen triangle in \(C\) expressing \(g \circ f\) as a composite. Applying \(F\) to this triangle produces a triangle in \(D\) with short edges \(F(f),F(g)\). By the Segal axiom, this triangle is identified with the chosen triangle in \(D\) expressing \(F(g) \circ F(f)\) as a composite of \(F(f)\) and \(F(g)\), in a way compatible with the two short-edge comparison identifications. The relation \(F(g \circ f) = F(g) \circ F(f)\) now follows by passing to the long edges of these identified triangles. On source and target, this identification is the restriction of the two a priori identifications on the short edges, and so it is compatible with the vertex identifications.
Agda Apply the functor to the composition triangle
value
Definition, checked
value : TrianglePresentation (map-morphism-family F alpha) (map-morphism-family F beta) (map-morphism-family F gamma)
Proof / implementation
value = triangle-presentation (funPost F ∘ T.triangle) Middle.first-image Middle.second-image Source.first-image (Middle.compatibility T.middle-compatible) (Source.compatibility T.source-compatible) (Target.compatibility T.target-compatible)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.TrianglePresentationPostcomposition where
module PostPresentation {Γ : Context} {P C D : CAT Γ} (F : MAP C D)
{f g h : MAP P C} {alpha : MorphismFamily f g} {beta : MorphismFamily g h}
{gamma : MorphismFamily f h} (given : TrianglePresentation alpha beta gamma) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Compare the two composition triangles
presented-composition
Derivation, checked
presented-composition : {P C : CAT Γ} {f g h : MAP P C} (segal : IsEquiv (short-edges C)) (alpha : MorphismFamily f g) (beta : MorphismFamily g h) (gamma : MorphismFamily f h) → TrianglePresentation alpha beta gamma → MorphismFamilyIdentification One (MC.Composition.compose C segal beta alpha) gamma
Proof / implementation
presented-composition {C = C} segal alpha beta gamma given = Chosen.comparison gamma T.long Endpoint.compatible where module T = PresentedTriangle given module Endpoint = TriangleEndpointComparison alpha beta gamma T.triangle T.short-comparison T.long T.source-compatible T.target-compatible module Chosen = CompositionPresentation C segal beta alpha T.triangle Endpoint.Short.identification
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.FramedTrianglePresentations where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Preservation retains endpoint comparisons
preserves-composition
Derivation, checked
preserves-composition : {P : CAT Γ} {f g h : MAP P C} (beta : MorphismFamily g h) (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (map-morphism-family F (MC.Composition.compose C source-segal beta alpha)) (MC.Composition.compose D target-segal (map-morphism-family F beta) (map-morphism-family F alpha))
Proof / implementation
preserves-composition beta alpha = family-comparison _ _ ((Target.identification ⁻¹) ∙ Source.identification) (compatible-quotient ev₀ _ _ _ Source.identification Target.identification Source.source Target.source) (compatible-quotient ev₁ _ _ _ Source.identification Target.identification Source.target Target.target) where module Completed = CompletePair source-segal alpha beta module Source = FamilyComparison (post-family-comparison F Completed.composite) module Target = FamilyComparison (PostPresentation.composite F Completed.presentation target-segal)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionPostcomposition where
module FunctorComposition {Γ : Context} {C D : CAT Γ} (F : MAP C D)
(source-segal : IsEquiv (short-edges C)) (target-segal : IsEquiv (short-edges D)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
For naturality, we apply this argument to terms in the categorical context \(\Ar (C) \times _C \Ar (C)\). □
Agda The universal composable pair
preserves-composition
Derivation, checked
preserves-composition : {P : CAT Γ} {f g h : MAP P C} (beta : MorphismFamily g h) (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (map-morphism-family F (MC.Composition.compose C source-segal beta alpha)) (MC.Composition.compose D target-segal (map-morphism-family F beta) (map-morphism-family F alpha))
Proof / implementation
preserves-composition beta alpha = family-comparison _ _ ((Target.identification ⁻¹) ∙ Source.identification) (compatible-quotient ev₀ _ _ _ Source.identification Target.identification Source.source Target.source) (compatible-quotient ev₁ _ _ _ Source.identification Target.identification Source.target Target.target) where module Completed = CompletePair source-segal alpha beta module Source = FamilyComparison (post-family-comparison F Completed.composite) module Target = FamilyComparison (PostPresentation.composite F Completed.presentation target-segal)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionPostcomposition where
module FunctorComposition {Γ : Context} {C D : CAT Γ} (F : MAP C D)
(source-segal : IsEquiv (short-edges C)) (target-segal : IsEquiv (short-edges D)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Lemma 2.2.6 (Unitality). For every morphism \(f\colon x\to y\), there are identifications \[ \id _y\circ f= f= f\circ \id _x \] in \(C(x,y)\), with its given endpoint identifications. They are natural in \(f\): they define identifications of functors \(\Ar (C)\to \Ar (C)\) over \(C\times C\).
Agda Unitality with fixed endpoints
source-unit
Derivation, checked
source-unit : {P : CAT Γ} {f g : MAP P C} (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (MC.Composition.compose C segal alpha (identity-family f)) alpha
Proof / implementation
source-unit {f = f} alpha = presented-composition segal (identity-family f) alpha alpha (FamilyUnitPresentations.source alpha)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module MorphismCompositionUnits {Γ : Context} (C : CAT Γ) (segal : IsEquiv (short-edges C)) wheretarget-unit
Derivation, checked
target-unit : {P : CAT Γ} {f g : MAP P C} (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (MC.Composition.compose C segal (identity-family g) alpha) alpha
Proof / implementation
target-unit {g = g} alpha = presented-composition segal alpha (identity-family g) alpha (FamilyUnitPresentations.target alpha)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module MorphismCompositionUnits {Γ : Context} (C : CAT Γ) (segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. We use the degenerate triangle
Agda The degenerate unit triangle
source
Definition, checked
source : TrianglePresentation (identity-family (ev₀ {C = C})) U.universal-arrow U.universal-arrow
Proof / implementation
source = triangle-presentation S.Source.triangle U.Source.First.comparison U.Source.Second.comparison U.Source.Long.comparison V.Source.MiddleVertex.vertex-equation V.Source.SourceVertex.vertex-equation V.Source.TargetVertex.vertex-equation
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module UniversalUnitPresentations {Γ : Context} (C : CAT Γ) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
obtained by restricting \(f\) along \(s_0\). Its short edges are \((\id _x,f)\) and its long edge is \(f\). These identifications respect the three vertices: after uncurrying, their compatibility is given by the vertex identifications of Lemma 2.1.16.
Agda The unit triangle retains its vertices
source
Definition, checked
source : TrianglePresentation (identity-family (ev₀ {C = C})) U.universal-arrow U.universal-arrow
Proof / implementation
source = triangle-presentation S.Source.triangle U.Source.First.comparison U.Source.Second.comparison U.Source.Long.comparison V.Source.MiddleVertex.vertex-equation V.Source.SourceVertex.vertex-equation V.Source.TargetVertex.vertex-equation
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module UniversalUnitPresentations {Γ : Context} (C : CAT Γ) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The chosen triangle \(j_C(\id _x,f)\) has the same short edges, with comparison given by \(\varepsilon _C\). The Segal equivalence therefore identifies these two triangles, with this comparison on their short edges. Restriction to the long edge gives an identification \[ f\circ \id _x=d_1^*j_C(\id _x,f) = d_1^*s_0^*(f) = f. \] This identification also respects the prescribed source and target: the interchange law allows us to compare endpoints before or after comparing the triangles. The short-edge identifications of the degenerate triangle then cancel with their inverses, leaving the vertex comparisons followed by the components of \(\varepsilon _C\). These are exactly the source and target identifications used to define composition.
Agda Compare chosen and degenerate triangles
source
Definition, checked
source : TrianglePresentation (identity-family f) alpha alpha
Proof / implementation
source = ReplacePresentation.value source-triangle source-identity universal universal
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module FamilyUnitPresentations {Γ : Context} {P C : CAT Γ} {f g : MAP P C}
(alpha : MorphismFamily f g) whereAbout this correspondence
This constructs the degenerate unit-triangle presentation. The comparison with the chosen composite is packaged in presented-composition; the individual short-edge comparison is not exposed here under the manuscript’s proof-step name.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The unit identification
source-unit
Derivation, checked
source-unit : {P : CAT Γ} {f g : MAP P C} (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (MC.Composition.compose C segal alpha (identity-family f)) alpha
Proof / implementation
source-unit {f = f} alpha = presented-composition segal (identity-family f) alpha alpha (FamilyUnitPresentations.source alpha)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module MorphismCompositionUnits {Γ : Context} (C : CAT Γ) (segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The unit identification preserves endpoints
source-unit
Derivation, checked
source-unit : {P : CAT Γ} {f g : MAP P C} (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (MC.Composition.compose C segal alpha (identity-family f)) alpha
Proof / implementation
source-unit {f = f} alpha = presented-composition segal (identity-family f) alpha alpha (FamilyUnitPresentations.source alpha)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module MorphismCompositionUnits {Γ : Context} (C : CAT Γ) (segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The same argument with \(s_1\) gives \(\id _y\circ f=f\).
Agda The other unit identification
target-unit
Derivation, checked
target-unit : {P : CAT Γ} {f g : MAP P C} (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (MC.Composition.compose C segal (identity-family g) alpha) alpha
Proof / implementation
target-unit {g = g} alpha = presented-composition segal alpha (identity-family g) alpha (FamilyUnitPresentations.target alpha)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module MorphismCompositionUnits {Γ : Context} (C : CAT Γ) (segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
For naturality in \(f\), we apply both constructions to the universal arrow on \(\Ar (C)\), working with term expressions in context \(\Ar (C)\). (In terms of actual functors, this translates to restriction and lifting through the Segal equivalence.) This results in the required identifications of functors over \(C\times C\). □
Agda The universal arrow gives natural unit laws
source-unit
Derivation, checked
source-unit : {P : CAT Γ} {f g : MAP P C} (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (MC.Composition.compose C segal alpha (identity-family f)) alpha
Proof / implementation
source-unit {f = f} alpha = presented-composition segal (identity-family f) alpha alpha (FamilyUnitPresentations.source alpha)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module MorphismCompositionUnits {Γ : Context} (C : CAT Γ) (segal : IsEquiv (short-edges C)) wheretarget-unit
Derivation, checked
target-unit : {P : CAT Γ} {f g : MAP P C} (alpha : MorphismFamily f g) → MorphismFamilyIdentification One (MC.Composition.compose C segal (identity-family g) alpha) alpha
Proof / implementation
target-unit {g = g} alpha = presented-composition segal alpha (identity-family g) alpha (FamilyUnitPresentations.target alpha)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionUnits where
module MorphismCompositionUnits {Γ : Context} (C : CAT Γ) (segal : IsEquiv (short-edges C)) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proposition 2.2.7 (Associativity, cf. [RS17, Proposition 5.9]). For composable morphisms \(f\colon x\to y\), \(g\colon y\to z\), and \(h\colon z\to w\), there is an identification \[ h\circ (g\circ f)=(h\circ g)\circ f \] in \(C(x,w)\). These identifications are natural in the composable triple: they form an identification over \(C\times C\) between the two composition functors from \(\Ar (C)\times _C\Ar (C)\times _C\Ar (C)\) to \(\Ar (C)\).
Agda Associativity with fixed endpoints
associativity
Derivation, checked
associativity : (alpha : MorphismFamily x y) (beta : MorphismFamily y z) (gamma : MorphismFamily z w) → MorphismFamilyIdentification One (MC.Composition.compose C (segal-isEquiv C) gamma (MC.Composition.compose C (segal-isEquiv C) beta alpha)) (MC.Composition.compose C (segal-isEquiv C) (MC.Composition.compose C (segal-isEquiv C) gamma beta) alpha)
Proof / implementation
associativity alpha beta gamma = compose-family-comparisons (MorphismCompositionUnits.target-unit C (segal-isEquiv C) Square.top) (compose-family-comparisons (SquareCommutativity.comparison C (segal-isEquiv C) Square.value) (inverse-family-comparison (MorphismCompositionUnits.source-unit C (segal-isEquiv C) Square.bottom))) where module Square = AssociativitySquare alpha beta gamma using (top; bottom; value)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
module _ {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C} wherenaturality
Derivation, checked
naturality : IdentificationOver {A = One} left-over right-over
Proof / implementation
naturality = family-comparison-over-endpoints left-bracketing right-bracketing comparison
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
module UniversalTriple {Γ : Context} (C : CAT Γ) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. As in the proof of unitality, we establish the desired identification (including the source and target compatibilities) for term expressions \(f\colon x \to y\), \(g\colon y \to z\) and \(h\colon z \to w\) in an arbitrary categorical context. Taking this context to be \(\Ar (C) \times _C \Ar (C) \times _C \Ar (C)\) then gives the final claim.
Consider the commutative triangle presenting the composite of \(f\) and \(g\), which has \(g \circ f\) as its long edge. Consider also the commutative triangle presenting the composite of \(\id _x\) and \(g \circ f\). Using the unitality of composition from Lemma 2.2.6, we may identify its long edge with \(g \circ f\) in \(C(x,z)\). Using the commutative square axiom, we may glue these two triangles into a commutative square
Agda Glue triangles along the specified long edge
value
Definition, checked
value : FramedSquare top right left bottom
Proof / implementation
value = Assembled.value
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.GluedFramedSquares where
module Glue {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
{long : MorphismFamily x z}
(given-upper : TrianglePresentation top right long)
(given-lower : TrianglePresentation left bottom long) wherecommon-diagonal
Derivation, checked
common-diagonal : ConeIdentification₁.left lower-source =₂ ConeIdentification₁.left upper-source
Proof / implementation
common-diagonal = Sides.diagonal-compatible
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.GluedFramedSquares where
module Glue {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
{long : MorphismFamily x z}
(given-upper : TrianglePresentation top right long)
(given-lower : TrianglePresentation left bottom long) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The pullback property in the commutative square axiom gives identifications of its two triangle restrictions with the chosen triangles, compatible with the specified identification of their long edges. Since this last identification lies in \(C(x,z)\), the endpoint comparisons agree at the two corners on the diagonal. At the other two corners, compatibility follows from the corresponding triangle. To identify these with the corners of the displayed square, recall that \(j_0=(s_0,s_1)\) and \(j_1=(s_1,s_0)\). The simplicial identities identify their boundary edges with the coordinate edges of \([1]\times [1]\); for example, \(j_0d_2=(0,\id _{[1]})\) and \(j_1d_2=(\id _{[1]},0)\). The vertex compatibilities of Lemma 2.1.16 give the specified comparisons under both product projections, so the product universal property identifies the corner comparisons as well. Thus all four edges have their prescribed endpoints, including the identification of the left side with \(\id _x\).
Agda The gluing comparison retains the diagonal matching
common-diagonal
Derivation, checked
common-diagonal : ConeIdentification₁.left lower-source =₂ ConeIdentification₁.left upper-source
Proof / implementation
common-diagonal = Sides.diagonal-compatible
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.GluedFramedSquares where
module Glue {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
{long : MorphismFamily x z}
(given-upper : TrianglePresentation top right long)
(given-lower : TrianglePresentation left bottom long) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The glued square retains its four endpoints
corner₀₀
Derivation, checked
corner₀₀ : ConeIdentification₁ (Endpoint.NativeCorner.cone zero zero) (framed-cone ev₀ ev₀ T.arrow L.arrow T.source-frame L.source-frame)
Proof / implementation
corner₀₀ = unframe-source Transfer.TopSource.Source.frame Transfer.LeftSource.Source.frame (Endpoint.NativeCorner.matching zero zero) Native₀₀.Frames.compatibility Source.comparison
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.GluedFramedSquares where
module Glue {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
{long : MorphismFamily x z}
(given-upper : TrianglePresentation top right long)
(given-lower : TrianglePresentation left bottom long) wherecorner₀₁
Derivation, checked
corner₀₁ : ConeIdentification₁ (Endpoint.NativeCorner.cone zero one) (framed-cone ev₁ ev₀ T.arrow R.arrow T.target-frame R.source-frame)
Proof / implementation
corner₀₁ = unframe-source Transfer.TopTarget.Source.frame Transfer.RightSource.Source.frame (Endpoint.NativeCorner.matching zero one) Native₀₁.Frames.compatibility upper-middle
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.GluedFramedSquares where
module Glue {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
{long : MorphismFamily x z}
(given-upper : TrianglePresentation top right long)
(given-lower : TrianglePresentation left bottom long) wherecorner₁₀
Derivation, checked
corner₁₀ : ConeIdentification₁ (Endpoint.NativeCorner.cone one zero) (framed-cone ev₀ ev₁ Bottom.arrow L.arrow Bottom.source-frame L.target-frame)
Proof / implementation
corner₁₀ = unframe-source Transfer.BottomSource.Source.frame Transfer.LeftTarget.Source.frame (Endpoint.NativeCorner.matching one zero) Native₁₀.Frames.compatibility lower-middle-swapped
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.GluedFramedSquares where
module Glue {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
{long : MorphismFamily x z}
(given-upper : TrianglePresentation top right long)
(given-lower : TrianglePresentation left bottom long) wherecorner₁₁
Derivation, checked
corner₁₁ : ConeIdentification₁ (Endpoint.NativeCorner.cone one one) (framed-cone ev₁ ev₁ Bottom.arrow R.arrow Bottom.target-frame R.target-frame)
Proof / implementation
corner₁₁ = unframe-source Transfer.BottomTarget.Source.frame Transfer.RightTarget.Source.frame (Endpoint.NativeCorner.matching one one) Native₁₁.Frames.compatibility Target.comparison
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.GluedFramedSquares where
module Glue {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
{long : MorphismFamily x z}
(given-upper : TrianglePresentation top right long)
(given-lower : TrianglePresentation left bottom long) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
In a similar fashion, gluing the triangles for \((g,h)\) and \((h\circ g,\id _w)\) along the unitality identification in \(C(y,w)\) gives a commutative square
Agda The second glued square
second-square
Definition, checked
second-square : FramedSquare second-composite (identity-family w) beta gamma
Proof / implementation
second-square = Glue.value (FamilyUnitPresentations.target second-composite) (Presentations.composition-presentation gamma beta)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
module AssociativitySquare {Γ : Context} {P C : CAT Γ}
{x y z w : MAP P C}
(alpha : MorphismFamily x y) (beta : MorphismFamily y z)
(gamma : MorphismFamily z w) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
again with the displayed endpoint identifications.
Under the equivalence \(\Sq (C) \simeq \Ar (\Ar (C))\), we may regard these commutative squares as morphisms \(\id _x \to g\) and \(g \to \id _w\) in \(\Ar (C)\). Their composition in \(\Ar (C)\) corresponds to a commutative square in \(C\) of the form
Agda Squares as arrows in the arrow category
FramedSquare
Definition, checked
FramedSquare : {P C : CAT Γ} {x y z w : MAP P C} (top : MorphismFamily x y) (right : MorphismFamily y z) (left : MorphismFamily x w) (bottom : MorphismFamily w z) → Set m
Proof / implementation
FramedSquare {C = C} top right left bottom = Data.Σ (MorphismFamily (MorphismFamily.arrow left) (MorphismFamily.arrow right)) λ vertical → Data.Σ (MorphismFamilyIdentification One (framed-image (ev₀ {C = C}) vertical (MorphismFamily.source-frame left) (MorphismFamily.source-frame right)) top) λ _ → MorphismFamilyIdentification One (framed-image (ev₁ {C = C}) vertical (MorphismFamily.target-frame left) (MorphismFamily.target-frame right)) bottom
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.FramedSquares where
module _ {Γ : Context} wherevertical
Definition, checked
vertical : MorphismFamily (MorphismFamily.arrow left) (MorphismFamily.arrow right)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.FramedSquares where
module _ {Γ : Context} where
module SquareFamily {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
(given : FramedSquare top right left bottom) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Compose the two squares
value
Definition, checked
value : FramedSquare top (identity-family w) (identity-family x) bottom
Proof / implementation
value = SquareComposition.Compose.value C (segal-isEquiv C) (segal-isEquiv (Ar C)) first-square second-square
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
module AssociativitySquare {Γ : Context} {P C : CAT Γ}
{x y z w : MAP P C}
(alpha : MorphismFamily x y) (beta : MorphismFamily y z)
(gamma : MorphismFamily z w) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Here the top and bottom edges are identified with \((h \circ g) \circ f\) and \(h \circ (g \circ f)\) by applying Lemma 2.2.5 to the two evaluation functors \(\ev _0,\ev _1\colon \Ar (C) \to C\). That lemma also ensures that these identifications retain the prescribed endpoints.
Agda Evaluation identifies the outer edges
evaluated-composition
Derivation, checked
evaluated-composition : {P : CAT Γ} {l k r : MAP P (Ar C)} (B : MorphismFamily k r) (A : MorphismFamily l k) (v : MAP (Ar C) C) {x y z : MAP P C} (p : (v ∘ l) =₁ x) (q : (v ∘ k) =₁ y) (s : (v ∘ r) =₁ z) → MorphismFamilyIdentification One (framed-image v (Arrow.compose B A) p s) (Base.compose (framed-image v B q s) (framed-image v A p q))
Proof / implementation
evaluated-composition B A v p q s = compose-family-comparisons (Transport.retarget-composition (map-morphism-family v B) (map-morphism-family v A) p q s) (retarget-family-comparison p s (FunctorComposition.preserves-composition v arrow-segal segal B A))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.FramedSquares where
module SquareComposition {Γ : Context} (C : CAT Γ)
(segal : IsEquiv (short-edges C)) (arrow-segal : IsEquiv (short-edges (Ar C))) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The two triangle restrictions of this square identify its diagonal with the composites along the top and right, and along the left and bottom, respectively. Indeed, the Segal equivalence compares each triangle with the chosen triangle for its two short edges. By Lemma 2.2.6, these composites are identified with the top and bottom edges themselves in \(C(x,w)\). We obtain the required identification \[ h\circ (g\circ f)=(h\circ g)\circ f. \] All constructions use restriction, the two axioms’ universal properties, and composition in \(\Ar (C)\), so they apply to the universal composable triple as asserted at the start. □
Agda The universal composable triple
Triples
Definition, checked
Triples : CAT Γ
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
module UniversalTriple {Γ : Context} (C : CAT Γ) wherefirst
Definition, checked
first : MorphismFamily x y
Proof / implementation
first = record { arrow = first-arrow; source-frame = id₌ x; target-frame = id₌ y }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
module UniversalTriple {Γ : Context} (C : CAT Γ) wheresecond
Definition, checked
second : MorphismFamily y z
Proof / implementation
second = record { arrow = second-arrow; source-frame = first-matching ⁻¹; target-frame = id₌ z }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
module UniversalTriple {Γ : Context} (C : CAT Γ) wherethird
Definition, checked
third : MorphismFamily z w
Proof / implementation
third = record { arrow = third-arrow ; source-frame = comp-assoc pairs (pullback₂ {f = ev₁ {C = C}} {g = ev₀}) ev₁ ∙ (second-matching ⁻¹) ; target-frame = id₌ w }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
module UniversalTriple {Γ : Context} (C : CAT Γ) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Compare the two routes through the outside square
comparison
Derivation, checked
comparison : (C : CAT Γ) (segal : IsEquiv (short-edges C)) {P : CAT Γ} {x y z w : MAP P C} {top : MorphismFamily x y} {right : MorphismFamily y z} {left : MorphismFamily x w} {bottom : MorphismFamily w z} → FramedSquare top right left bottom → MorphismFamilyIdentification One (MC.Composition.compose C segal bottom left) (MC.Composition.compose C segal right top)
Proof / implementation
comparison C segal {top = top} {right} {left} {bottom} given = compose-family-comparisons (inverse-family-comparison (presented-composition segal top right Presentations.long Presentations.upper)) (presented-composition segal left bottom Presentations.long Presentations.lower) where module Presentations = BoundaryPresentations given using (long; upper; lower)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section02.FramedSquareCommutativity where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Remove identity edges
associativity
Derivation, checked
associativity : (alpha : MorphismFamily x y) (beta : MorphismFamily y z) (gamma : MorphismFamily z w) → MorphismFamilyIdentification One (MC.Composition.compose C (segal-isEquiv C) gamma (MC.Composition.compose C (segal-isEquiv C) beta alpha)) (MC.Composition.compose C (segal-isEquiv C) (MC.Composition.compose C (segal-isEquiv C) gamma beta) alpha)
Proof / implementation
associativity alpha beta gamma = compose-family-comparisons (MorphismCompositionUnits.target-unit C (segal-isEquiv C) Square.top) (compose-family-comparisons (SquareCommutativity.comparison C (segal-isEquiv C) Square.value) (inverse-family-comparison (MorphismCompositionUnits.source-unit C (segal-isEquiv C) Square.bottom))) where module Square = AssociativitySquare alpha beta gamma using (top; bottom; value)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.MorphismCompositionAssociativity where
module _ {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Observe that another way of formulating the Segal axiom, Axiom E, is that the commutative square
is a pullback square. This has the following corollary:
Agda The Segal pullback square
segal-isEquiv
Assumption, type checked
segal-isEquiv : (C : CAT Γ) → IsEquiv (short-edges C)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.SegalAxiom where
module _ {Γ : Context} wheretriangle-cone
Definition, checked
triangle-cone : (C : CAT Γ) → Cone (ev₁ {C = C}) ev₀ (Triangles C)
Proof / implementation
triangle-cone C = record { left = edge₂; right = edge₀ ; match = (evAt-pre zero d₀) ⁻¹ ∙ (evAt-cong (face-middle ⁻¹) ∙ evAt-pre one d₂) }
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section01.Triangles where
module _ {Γ : Context} whereAbout this correspondence
IsPullback for this specified cone is defined by the equivalence of its comparison functor. The displayed Segal equivalence is therefore the pullback formulation for triangle-cone.
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 2.2.8. For every category \(C\), the commutative squares
Agda Triangles as squares with a constant side
vertex-square-isPullback
Derivation, checked
vertex-square-isPullback : IsPullback vertex-square
Proof / implementation
vertex-square-isPullback = isPullback-cone-identification vertex-image square-isPullback
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.TrianglePullbacks where
module At {Γ : Context} (C : CAT Γ) where
module Left wherevertex-square-isPullback
Derivation, checked
vertex-square-isPullback : IsPullback vertex-square
Proof / implementation
vertex-square-isPullback = isPullback-cone-identification vertex-image square-isPullback
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.TrianglePullbacks where
module At {Γ : Context} (C : CAT Γ) where
module Right whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
are pullback squares.
Proof
Proof. We will prove the claim for the left square and leave the analogous proof of the right square to the reader. Note that this square can be written as the outer square in the following commutative diagram:
and so it will suffice that each of these two squares is a pullback square. The first one follows from applying the pasting law of pullback squares to the following commutative diagram:
Agda Cancel the square-axiom pullback
square-isPullback
Derivation, checked
square-isPullback : IsPullback square
Proof / implementation
square-isPullback = isPullback-change-left side-comparison pasted pasted-isPullback
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.TrianglePullbacks where
module At {Γ : Context} (C : CAT Γ) where
module Left whereAbout this correspondence
This points to the corresponding pullback conclusion in rebuild2; the intermediate pasting steps are organized differently.
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.
Here the outer square is evidently a pullback, and the right square is a pullback by the commutative square axiom, Axiom D. The second one similarly follows from applying the pasting law of pullback squares to the following commutative diagram:
Agda Cancel the Segal pullback
left-constant-isPullback
Derivation, checked
left-constant-isPullback : IsPullback left-constant-cone
Proof / implementation
left-constant-isPullback = LowerLeft.unpaste-isPullback left-constant-cone (horizontal-equivalences (LowerLeft.Paste.paste left-constant-cone) (equiv-transport (identity-target ⁻¹) (id-isEquiv C)) (equiv-transport ((funPre-id [1] C ∙ (funPre⁼ s₀-d₀ ∙ funPre-comp d₀ s₀)) ⁻¹) (id-isEquiv (Ar C))))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.TrianglePullbacks where
module At {Γ : Context} (C : CAT Γ) whereAbout this correspondence
This points to the corresponding pullback conclusion in rebuild2; the intermediate pasting steps are organized differently.
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.
Here the outer rectangle is again evidently a pullback square, and the right square is a pullback square by the Segal axiom, Axiom E. □
Remark 2.2.9. Informally, the previous corollary says that commutative triangles in \(C\) may equivalently be encoded in the following three ways:
- (1)
-
One might consider commutative triangles \([2] \to C\), which we will display as
- (2)
-
One might consider commutative squares \([1] \times [1] \to C\) whose restriction to \([1] \times \{0\}\) is constant, which we will display as
- (3)
-
One might consider commutative squares \([1] \times [1] \to C\) whose restriction to \([1] \times \{1\}\) is constant, which we will display as
We now explain how the usual naturality relation follows from our definition of natural transformations. Let \(\alpha \colon f\to g\) be a natural transformation between functors \(f,g\colon C\to D\). For a morphism \(u\colon a\to b\) in \(C\), precomposition of the interval diagram of \(\alpha \) \(C\times [1]\to D\) with \(u\times \id _{[1]}\) gives a commutative square
Agda The naturality square
value
Definition, checked
value : FramedSquare top right left bottom
Proof / implementation
value = framed-square vertical (Pasting.comparison Transformation.arrow ev₀ F Transformation.source-frame u) (Pasting.comparison Transformation.arrow ev₁ G Transformation.target-frame 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.Chapter02.Section02.NaturalTransformationNaturality where
module NaturalitySquare {Γ : Context} {P C D : CAT Γ} {F G : MAP C D}
(alpha : MorphismFamily F G) {a b : MAP P C} (u : MorphismFamily a b) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Its two triangles have the same long edge. After taking composites, we write \[ \alpha (u):g(u)\circ \alpha (a)=\alpha (b)\circ f(u) \] for the resulting comparison in \(D(f(a),g(b))\). Its endpoint identifications are those supplied by Lemma 2.1.16 and the comparison with the chosen composites in Construction 2.2.3.
Agda The naturality identification
naturality
Derivation, checked
naturality : (alpha : MorphismFamily F G) {a b : MAP P C} (u : MorphismFamily a b) → MorphismFamilyIdentification One (MC.Composition.compose D (segal-isEquiv D) (map-morphism-family G u) (restrict-family alpha a)) (MC.Composition.compose D (segal-isEquiv D) (restrict-family alpha b) (map-morphism-family F u))
Proof / implementation
naturality alpha u = SquareCommutativity.comparison D (segal-isEquiv D) (NaturalitySquare.value alpha 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.Chapter02.Section02.NaturalTransformationNaturality where
module _ {Γ : Context} {P C D : CAT Γ} {F G : MAP C D} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The same construction gives the following interchange law.
Lemma 2.2.10 (Interchange for natural transformations). Let \(F,G\colon C\to D\) and \(u,v\colon B\to C\) be functors, and let \(\alpha \colon F\to G\) and \(\beta \colon u\to v\) be natural transformations. There is a commutative square in \(\Fun (B,D)\)
Agda Interchange of natural transformations
interchange
Derivation, checked
interchange : (alpha : MorphismFamily (funName F) (funName G)) (beta : MorphismFamily (funName u) (funName v)) → MorphismFamilyIdentification One (MC.Composition.compose (Fun B D) (segal-isEquiv (Fun B D)) (post-whisker G beta) (pre-whisker u alpha)) (MC.Composition.compose (Fun B D) (segal-isEquiv (Fun B D)) (pre-whisker v alpha) (post-whisker F beta))
Proof / implementation
interchange alpha beta = At.comparison alpha beta
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section02.Interchange where
module _ {Γ : Context} {B C D : CAT Γ} {F G : MAP C D} {u v : MAP B C} whereinterchange-square
Definition, checked
interchange-square : (alpha : MorphismFamily (funName F) (funName G)) (beta : MorphismFamily (funName u) (funName v)) → FramedSquare (pre-whisker u alpha) (post-whisker G beta) (post-whisker F beta) (pre-whisker v alpha)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section02.Interchange where
module _ {Γ : Context} {B C D : CAT Γ} {F G : MAP C D} {u v : MAP B C} whereAbout this correspondence
The rebuild2 proof compares both composites with the image of a paired family using product composition and unit laws, then supplies the corresponding square. It does not follow the manuscript’s double-currying proof.
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.
This gives an identification in \(\Hom _{\Fun (B,D)}(Fu,Gv)\) of the form \[ (G\beta )\circ (\alpha u)=(\alpha v)\circ (F\beta ). \]
Proof
Proof. Let \(A\colon [1]\times C\to D\) and \(H\colon [1]\times B\to C\) encode \(\alpha \) and \(\beta \), respectively. The composite \[ [1]\times [1]\times B \xrightarrow {\id _{[1]}\times H}[1]\times C \xrightarrow {A}D \] curries to a functor \([1]\times [1]\to \Fun (B,D)\). Its four edges, with the endpoint identifications supplied by \(A\) and \(H\), are precisely the four transformations displayed above. Restricting to the two triangles, using the restriction identifications fixed above, gives the two composites with a common long edge and the prescribed source/target. This gives the displayed identification. □
Agda The four whiskered transformations
pre-whisker
Definition, checked
pre-whisker : {B C D : CAT Γ} (u : MAP B C) {F G : MAP C D} → MorphismFamily (funName F) (funName G) → MorphismFamily (funName (F ∘ u)) (funName (G ∘ 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.Chapter02.Section02.NaturalTransformationWhiskering where
module _ {Γ : Context} wherepost-whisker
Definition, checked
post-whisker : {B C D : CAT Γ} (F : MAP C D) {u v : MAP B C} → MorphismFamily (funName u) (funName v) → MorphismFamily (funName (F ∘ u)) (funName (F ∘ v))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.NaturalTransformationWhiskering where
module _ {Γ : Context} whereAbout this correspondence
The rebuild2 proof compares both composites with the image of a paired family using product composition and unit laws, then supplies the corresponding square. It does not follow the manuscript’s double-currying proof.
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.
Finally, the conversion of Construction 2.1.5 is compatible with composition of primitive identifications. For \(\alpha \colon f=g\) and \(\beta \colon g=h\), consider the constant triangle at \(f\), with vertex identifications \(\id _f\), \(\alpha \), and \(\beta \circ \alpha \). Its short edges represent \(\alpha \) and \(\beta \), using \(\alpha \) to identify the second short edge with the constant interval at \(g\). Its long edge represents \(\beta \circ \alpha \). The Segal equivalence identifies this triangle with the chosen composite triangle, retaining the short-edge comparisons. Passing to the long edge therefore gives the required compatibility with the prescribed source/target, as in Construction 2.2.3.
Agda Primitive identifications respect composition
identification-composition
Derivation, checked
identification-composition : (p : x =₁ y) (q : y =₁ z) → MorphismFamilyIdentification One (MC.Composition.compose C (segal-isEquiv C) (identification-family q) (identification-family p)) (identification-family (q ∙ p))
Proof / implementation
identification-composition p q = presented-composition (segal-isEquiv C) (identification-family p) (identification-family q) (identification-family (q ∙ p)) (ConvertedTriangle.presentation p 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.Chapter02.Section02.PrimitiveIdentificationComposition where
module _ {Γ : Context} {P C : CAT Γ} {x y z : MAP P C} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda Identify the second constant edge
second
Derivation, checked
second : MorphismFamilyIdentification One (retarget-family (identity-family x) p (q ∙ p)) (identification-family q)
Proof / implementation
second = family-comparison _ _ Changed.identification Changed.source ((comp₌-assoc q p X.target-frame) ⁻¹ ∙ (comp₌-cong (id₌ q) Changed.target ∙ comp₌-assoc q Y.target-frame (ev₁ ◁ Changed.identification)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section02.PrimitiveIdentificationComposition where
module ConvertedTriangle {Γ : Context} {P C : CAT Γ} {x y z : MAP P C}
(p : x =₁ y) (q : y =₁ z) whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Supplementary notes
- Substitution in morphism expressions AI-generated