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.2 Coherences
So far, we have introduced functors and their identifications, but we have essentially no relations between them. We next specify the coherence relations we will use. We first describe composition of identifications and its compatibility with whiskering. We then introduce the unit and associativity identifications for composition of functors, and the relations among them.
For readability, we write most of these coherences in their ‘term notation’, cf. Notation 1.1.3. In each case, the axiom introduces a specified identification of functors, which we will often leave nameless to avoid cluttering of notation.
1.2.1 Composition of identifications
Identifications can be composed: given identifications \(\sigma :f=g\) and \(\tau :g=h\), we obtain an identification \(\tau \circ \sigma :f=h\). We call this vertical composition to distinguish it from the horizontal composition introduced below. Every functor has an identity identification, and every identification has an inverse.
Axiom A.3 (Composition of identifications). For every functor \(f\), there is an identity identification \(\id _f\colon f= f\). For parallel functors \(f,g,h\colon C\to D\), there is a composition functor \[ -\circ -\colon (g= h)\times (f= g)\longrightarrow (f= h). \] There is also an inverse functor \[ (-)^{-1}\colon (f=g)\to (g=f). \] This composition is unital and associative, and the inverse functor supplies two-sided inverses, through specified identifications of functors on the corresponding animae of identifications. For \(\alpha :f=g\), \(\beta :g=h\), and \(\gamma :h=k\), where \(k\colon C\to D\), these laws read \[ \id _g\circ \alpha =\alpha ,\qquad \alpha \circ \id _f=\alpha , \] \[ (\gamma \circ \beta )\circ \alpha =\gamma \circ (\beta \circ \alpha ), \] \[ \alpha ^{-1}\circ \alpha =\id _f,\qquad \alpha \circ \alpha ^{-1}=\id _g. \]
Agda Inversion
inv₌
Assumption, type checked
inv₌ : {C D : CAT Γ} {f g : MAP C D} → MAP (f ＝ g) (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.Section02.Coherence where
module _ {Γ : Context} where_⁻¹
Definition, checked
_⁻¹ : {P C D : CAT Γ} {f g : MAP C D} → MAP P (f ＝ g) → MAP P (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.Section02.Coherence where
module Composition 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 Identity identifications
id₌
Assumption, type checked
id₌ : {C D : CAT Γ} (f : MAP C D) → f =₁ 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.Section02.Coherence 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 Vertical composition
comp₌
Assumption, type checked
comp₌ : {C D : CAT Γ} {f g h : MAP C D} → MAP ((g ＝ h) × (f ＝ g)) (f ＝ h)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where
module _ {Γ : Context} where_∙_
Definition, checked
_∙_ : {X C D : CAT Γ} {f g h : MAP C D} → MAP X (g ＝ h) → MAP X (f ＝ g) → MAP X (f ＝ h)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where
module Composition where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The vertical unit comparisons
comp₌-unitˡ
Assumption, type checked
comp₌-unitˡ : {C D : CAT Γ} (f g : MAP C D) → let α = id (f ＝ g) in (const (id₌ g) ∙ α) =₁ α
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where
module _ {Γ : Context} wherecomp₌-unitʳ
Assumption, type checked
comp₌-unitʳ : {C D : CAT Γ} (f g : MAP C D) → let α = id (f ＝ g) in (α ∙ const (id₌ 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.Section02.Coherence where
module _ {Γ : Context} wherecomp₌-unitˡ
Derivation, checked
comp₌-unitˡ : {C D : CAT Γ} {f g : MAP C D} (α : f ＝ g) → (const (id₌ g) ∙ α) =₁ α
Proof / implementation
comp₌-unitˡ {f = f} {g} α = specialize (Coherence.comp₌-unitˡ f g) α (comp₌-evaluate-One (const (id₌ g)) (id (Equal f g)) α (const-pre (id₌ g) α) (comp-unitˡ α)) (comp-unitˡ α)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Specialization where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherecomp₌-unitʳ
Derivation, checked
comp₌-unitʳ : {C D : CAT Γ} {f g : MAP C D} (α : f ＝ g) → (α ∙ const (id₌ f)) =₁ α
Proof / implementation
comp₌-unitʳ {f = f} {g} α = specialize (Coherence.comp₌-unitʳ f g) α (comp₌-evaluate-One (id (Equal f g)) (const (id₌ f)) α (comp-unitˡ α) (const-pre (id₌ f) α)) (comp-unitˡ α)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Specialization 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 Vertical associativity
comp₌-assoc
Assumption, type checked
comp₌-assoc : {C D : CAT Γ} (f g h k : MAP C D) → let X = (h ＝ k) × ((g ＝ h) × (f ＝ g)) α : MAP X (f ＝ g) α = pr₂ ∘ pr₂ β : MAP X (g ＝ h) β = pr₁ ∘ pr₂ γ : MAP X (h ＝ k) γ = pr₁ in ((γ ∙ β) ∙ α) =₁ (γ ∙ (β ∙ α))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where
module _ {Γ : Context} wherecomp₌-assoc
Derivation, checked
comp₌-assoc : {C D : CAT Γ} {f g h k : MAP C D} (γ : h ＝ k) (β : g ＝ h) (α : f ＝ g) → ((γ ∙ β) ∙ α) =₁ (γ ∙ (β ∙ α))
Proof / implementation
comp₌-assoc {f = f} {g} {h} {k} γ β α = let parameters = pair γ (pair β α) first : (pr₁ ∘ parameters) =₁ γ first = pair-β₁ γ (pair β α) second : ((pr₁ ∘ pr₂) ∘ parameters) =₁ β second = pair-β₁ β α ∙ ((pr₁ ◁ pair-β₂ γ (pair β α)) ∙ comp-assoc parameters pr₂ pr₁) third : ((pr₂ ∘ pr₂) ∘ parameters) =₁ α third = pair-β₂ β α ∙ ((pr₂ ◁ pair-β₂ γ (pair β α)) ∙ comp-assoc parameters pr₂ pr₂) in specialize (Coherence.comp₌-assoc f g h k) parameters (comp₌-evaluate-One (pr₁ ∙ (pr₁ ∘ pr₂)) (pr₂ ∘ pr₂) parameters (comp₌-evaluate-One pr₁ (pr₁ ∘ pr₂) parameters first second) third) (comp₌-evaluate-One pr₁ ((pr₁ ∘ pr₂) ∙ (pr₂ ∘ pr₂)) parameters first (comp₌-evaluate-One (pr₁ ∘ pr₂) (pr₂ ∘ pr₂) parameters second third))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Specialization 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 Two-sided inverses
comp₌-inverseˡ
Assumption, type checked
comp₌-inverseˡ : {C D : CAT Γ} (f g : MAP C D) → let α = id (f ＝ g) in (α ⁻¹ ∙ α) =₁ (const (id₌ 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.Section02.Coherence where
module _ {Γ : Context} wherecomp₌-inverseʳ
Assumption, type checked
comp₌-inverseʳ : {C D : CAT Γ} (f g : MAP C D) → let α = id (f ＝ g) in (α ∙ α ⁻¹) =₁ (const (id₌ g))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where
module _ {Γ : Context} wherecomp₌-inverseˡ
Derivation, checked
comp₌-inverseˡ : {C D : CAT Γ} {f g : MAP C D} (α : f ＝ g) → (α ⁻¹ ∙ α) =₁ (const (id₌ f))
Proof / implementation
comp₌-inverseˡ {f = f} {g} α = specialize (Coherence.comp₌-inverseˡ f g) α (comp₌-evaluate-One ((id (Equal f g)) ⁻¹) (id (Equal f g)) α ((inv₌ ◁ comp-unitˡ α) ∙ ⁻¹-pre (id (Equal f g)) α) (comp-unitˡ α)) (const-pre (id₌ 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.Section02.Specialization where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherecomp₌-inverseʳ
Derivation, checked
comp₌-inverseʳ : {C D : CAT Γ} {f g : MAP C D} (α : f ＝ g) → (α ∙ α ⁻¹) =₁ (const (id₌ g))
Proof / implementation
comp₌-inverseʳ {f = f} {g} α = specialize (Coherence.comp₌-inverseʳ f g) α (comp₌-evaluate-One (id (Equal f g)) ((id (Equal f g)) ⁻¹) α (comp-unitˡ α) ((inv₌ ◁ comp-unitˡ α) ∙ ⁻¹-pre (id (Equal f g)) α)) (const-pre (id₌ g) α)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Specialization 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.
The displayed laws are specified identifications of functors on the relevant animae of inputs. For parallel functors \(f,g,h,k\colon C\to D\), the associativity law compares the two functors \[ (h=k)\times \bigl ((g=h)\times (f=g)\bigr )\longrightarrow (f=k) \] given by \((\gamma ,(\beta ,\alpha ))\mapsto (\gamma \circ \beta )\circ \alpha \) and \((\gamma ,(\beta ,\alpha ))\mapsto \gamma \circ (\beta \circ \alpha )\). Precomposing these comparisons with a functor into the input anima gives the same laws for the resulting expressions.
We can now also speak of commutative squares, triangles, and more general diagrams of identifications, using the convention of Definition 1.1.4 with vertical composition along their boundaries.
Agda Squares of identifications
SquareCell₌
Definition, checked
SquareCell₌ : {X C D : CAT Γ} {f g f′ g′ : MAP C D} → MAP X (f ＝ g) → MAP X (f′ ＝ g′) → MAP X (f ＝ f′) → MAP X (g ＝ g′) → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where
module Boundaries where
module _ {Γ : Context} whereSquareCommutes
Definition, checked
SquareCommutes : {X C D : CAT Γ} {f g f′ g′ : MAP C D} → SquareBoundary {X = X} f g f′ g′ → Set m
Proof / implementation
SquareCommutes S = SquareCell₌ top bottom left right where open SquareBoundary 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.Section02.Coherence where
module Boundaries 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 Triangles of identifications
TriangleDiagram
Definition, checked
record TriangleDiagram {X C D : CAT Γ} (v₀ v₁ v₂ : MAP C D) : Set m where constructor triangle-diagram field direct : MAP X (v₀ ＝ v₂) first : MAP X (v₀ ＝ v₁) second : MAP X (v₁ ＝ 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.Chapter01.Section02.Coherence where
module Boundaries where
module _ {Γ : Context} whereTriangleCommutes
Definition, checked
TriangleCommutes : TriangleDiagram {X = X} v₀ v₁ v₂ → Set m
Proof / implementation
TriangleCommutes T = TriangleSource T =₁ TriangleTarget T
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where
module Boundaries where
module _ {Γ : Context} where
module _ {X C D : CAT Γ} {v₀ v₁ v₂ : MAP C D} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
1.2.2 Whiskering and horizontal composition
Whiskering composes an identification with a functor on either side. We first require that it respect identity identifications and vertical composition.
Axiom A.4 (Whiskering and vertical composition). Prewhiskering and postwhiskering preserve identity identifications and vertical composition through specified identifications of functors on the input animae of identifications. For functors \(f,g,h\colon C\to D\), \(k\colon B\to C\) and \(u\colon D\to E\), these laws read \[ u\star \id _f=\id _{u\circ f},\qquad \id _f\star k=\id _{f\circ k}, \] \[ u\star (\tau \circ \sigma ) =(u\star \tau )\circ (u\star \sigma ),\qquad (\tau \circ \sigma )\star k =(\tau \star k)\circ (\sigma \star k), \] where \(\sigma \colon f= g\) and \(\tau \colon g= h\). The two vertical-composition comparisons are identifications of functors on \((g=h)\times (f=g)\).
Agda Whiskering preserves identities
postWhisker-id₌
Assumption, type checked
postWhisker-id₌ : {C D E : CAT Γ} (u : MAP D E) (f : MAP C D) → (u ◁ id₌ f) =₂ (id₌ (u ∘ 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.Section02.Coherence where
module _ {Γ : Context} wherepreWhisker-id₌
Assumption, type checked
preWhisker-id₌ : {B C D : CAT Γ} (f : MAP C D) (k : MAP B C) → (id₌ f ▷ k) =₂ (id₌ (f ∘ k))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence 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 Whiskering preserves vertical composition
postWhisker-comp₌
Assumption, type checked
postWhisker-comp₌ : {C D E : CAT Γ} (f g h : MAP C D) (u : MAP D E) → let X = (g ＝ h) × (f ＝ g) σ : MAP X (f ＝ g) σ = pr₂ τ : MAP X (g ＝ h) τ = pr₁ in (u ◁ (τ ∙ σ)) =₁ ((u ◁ τ) ∙ (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.Section02.Coherence where
module _ {Γ : Context} wherepreWhisker-comp₌
Assumption, type checked
preWhisker-comp₌ : {B C D : CAT Γ} (f g h : MAP C D) (k : MAP B C) → let X = (g ＝ h) × (f ＝ g) σ : MAP X (f ＝ g) σ = pr₂ τ : MAP X (g ＝ h) τ = pr₁ in ((τ ∙ σ) ▷ k) =₁ ((τ ▷ k) ∙ (σ ▷ k))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Given identifications \(\tau :F=G\) and \(\sigma :h=k\), where \(F,G\colon D\to E\) and \(h,k\colon T\to D\), there are two ways to obtain an identification \(Fh=Gk\): one can first change \(h\) to \(k\), or first change \(F\) to \(G\). The interchange rule compares these two constructions.
Axiom A.5 (Interchange). The two ways of pasting identifications are identified. More precisely, for \(\tau \colon F= G\) with \(F,G\colon D\to E\) and \(h,k\colon T\to D\), there is an identification of functors \((h= k)\to (Fh= Gk)\) \[ (\tau \star k)\circ (F\star -) \ =\ (G\star -)\circ (\tau \star h). \] Here composition with a fixed identification uses it as a constant input. Likewise, for fixed \(\sigma \colon h= k\), the two functors \((F= G)\to (Fh= Gk)\) given by \[ (-\star k)\circ (F\star \sigma ) \quad \text {and}\quad (G\star \sigma )\circ (-\star h) \] are identified.
Agda Interchange with a fixed input
interchange
Derivation, checked
interchange : {B C D : CAT Γ} {F G : MAP C D} {h k : MAP B C} (τ : F ＝ G) (σ : h ＝ k) → ((τ ▷ k) ∙ (F ◁ σ)) =₁ ((G ◁ σ) ∙ (τ ▷ h))
Proof / implementation
interchange {F = F} {G} {h} {k} τ σ = let parameters = pair τ σ in specialize (Coherence.interchange F G h k) parameters (comp₌-evaluate-One (pr₁ ▷ k) (F ◁ pr₂) parameters (preWhisker-evaluate-One pr₁ k parameters (pair-β₁ τ σ)) (postWhisker-evaluate-One F pr₂ parameters (pair-β₂ τ σ))) (comp₌-evaluate-One (G ◁ pr₂) (pr₁ ▷ h) parameters (postWhisker-evaluate-One G pr₂ parameters (pair-β₂ τ σ)) (preWhisker-evaluate-One pr₁ h parameters (pair-β₁ τ σ)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Specialization where
module _ {Γ : Context} where
module _ {X : CAT Γ} whereinterchange-fixedOuter
Derivation, checked
interchange-fixedOuter : {B C D : CAT Γ} {F G : MAP C D} {h k : MAP B C} (τ : F =₁ G) (σ : h ＝ k) → (const (τ ▷ k) ∙ (F ◁ σ)) =₁ ((G ◁ σ) ∙ const (τ ▷ h))
Proof / implementation
interchange-fixedOuter {F = F} {G} {h} {k} τ σ = comp₌-cong (id₌ (G ◁ σ)) (pre-constant τ h) ∙ (interchange (const τ) σ ∙ (comp₌-cong (pre-constant τ k) (id₌ (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.Section02.Specialization where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereinterchange-fixedInner
Derivation, checked
interchange-fixedInner : {B C D : CAT Γ} {F G : MAP C D} {h k : MAP B C} (τ : F ＝ G) (σ : h =₁ k) → ((τ ▷ k) ∙ const (F ◁ σ)) =₁ (const (G ◁ σ) ∙ (τ ▷ h))
Proof / implementation
interchange-fixedInner {F = F} {G} {h} {k} τ σ = comp₌-cong (post-constant G σ) (id₌ (τ ▷ h)) ∙ (interchange τ (const σ) ∙ (comp₌-cong (id₌ (τ ▷ k)) (post-constant 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.Section02.Specialization 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.
Agda The two fixed-input interchange clauses
interchange
Derivation, checked
interchange : {B C D : CAT Γ} {F G : MAP C D} {h k : MAP B C} (τ : F ＝ G) (σ : h ＝ k) → ((τ ▷ k) ∙ (F ◁ σ)) =₁ ((G ◁ σ) ∙ (τ ▷ h))
Proof / implementation
interchange {F = F} {G} {h} {k} τ σ = let parameters = pair τ σ in specialize (Coherence.interchange F G h k) parameters (comp₌-evaluate-One (pr₁ ▷ k) (F ◁ pr₂) parameters (preWhisker-evaluate-One pr₁ k parameters (pair-β₁ τ σ)) (postWhisker-evaluate-One F pr₂ parameters (pair-β₂ τ σ))) (comp₌-evaluate-One (G ◁ pr₂) (pr₁ ▷ h) parameters (postWhisker-evaluate-One G pr₂ parameters (pair-β₂ τ σ)) (preWhisker-evaluate-One pr₁ h parameters (pair-β₁ τ σ)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Specialization where
module _ {Γ : Context} where
module _ {X : CAT Γ} whereinterchange-fixedOuter
Derivation, checked
interchange-fixedOuter : {B C D : CAT Γ} {F G : MAP C D} {h k : MAP B C} (τ : F =₁ G) (σ : h ＝ k) → (const (τ ▷ k) ∙ (F ◁ σ)) =₁ ((G ◁ σ) ∙ const (τ ▷ h))
Proof / implementation
interchange-fixedOuter {F = F} {G} {h} {k} τ σ = comp₌-cong (id₌ (G ◁ σ)) (pre-constant τ h) ∙ (interchange (const τ) σ ∙ (comp₌-cong (pre-constant τ k) (id₌ (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.Section02.Specialization where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereinterchange-fixedInner
Derivation, checked
interchange-fixedInner : {B C D : CAT Γ} {F G : MAP C D} {h k : MAP B C} (τ : F ＝ G) (σ : h =₁ k) → ((τ ▷ k) ∙ const (F ◁ σ)) =₁ (const (G ◁ σ) ∙ (τ ▷ h))
Proof / implementation
interchange-fixedInner {F = F} {G} {h} {k} τ σ = comp₌-cong (post-constant G σ) (id₌ (τ ▷ h)) ∙ (interchange τ (const σ) ∙ (comp₌-cong (id₌ (τ ▷ k)) (post-constant 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.Section02.Specialization 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.
Given \(\alpha \colon f= f'\) and \(\beta \colon g= g'\), we write \[ \beta \ast \alpha :=(\beta \star f')\circ (g\star \alpha ): gf= g'f' \] for their horizontal composite. Interchange compares this with \((g'\star \alpha )\circ (\beta \star f)\). In particular, horizontal composition preserves identities and vertical composites. For fixed functors \(f,f',g,g'\), this construction defines a functor \[ - \ast - \colon (g = g') \times (f = f') \to (gf = g'f'). \]
Agda Horizontal composition
_⋆_
Definition, checked
_⋆_ : {X C D E : CAT Γ} {f f′ : MAP C D} {g g′ : MAP D E} → MAP X (g ＝ g′) → MAP X (f ＝ f′) → MAP X ((g ∘ 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.Section02.Coherence where
module Composition where
module _ {Γ : Context} wherehcomp
Definition, checked
hcomp : {C D E : CAT Γ} {f f′ : MAP C D} {g g′ : MAP D E} → MAP ((g ＝ g′) × (f ＝ f′)) ((g ∘ 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.Section02.Coherence where
module Composition where
module _ {Γ : Context} wherehcomp-cong
Derivation, checked
hcomp-cong : {C D E : CAT Γ} {f f′ : MAP C D} {g g′ : MAP D E} {β β′ : g ＝ g′} {α α′ : f ＝ f′} → β =₁ β′ → α =₁ α′ → (β ⋆ α) =₁ (β′ ⋆ α′)
Proof / implementation
hcomp-cong {f′ = f′} {g = g} b a = comp₌-cong (preWhisker f′ ◁ b) (postWhisker g ◁ 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.Chapter01.Section02.Specialization 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 The other horizontal pasting
interchange
Derivation, checked
interchange : {B C D : CAT Γ} {F G : MAP C D} {h k : MAP B C} (τ : F ＝ G) (σ : h ＝ k) → ((τ ▷ k) ∙ (F ◁ σ)) =₁ ((G ◁ σ) ∙ (τ ▷ h))
Proof / implementation
interchange {F = F} {G} {h} {k} τ σ = let parameters = pair τ σ in specialize (Coherence.interchange F G h k) parameters (comp₌-evaluate-One (pr₁ ▷ k) (F ◁ pr₂) parameters (preWhisker-evaluate-One pr₁ k parameters (pair-β₁ τ σ)) (postWhisker-evaluate-One F pr₂ parameters (pair-β₂ τ σ))) (comp₌-evaluate-One (G ◁ pr₂) (pr₁ ▷ h) parameters (postWhisker-evaluate-One G pr₂ parameters (pair-β₂ τ σ)) (preWhisker-evaluate-One pr₁ h parameters (pair-β₁ τ σ)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Specialization where
module _ {Γ : Context} where
module _ {X : CAT Γ} whereinterchange-fixedOuter
Derivation, checked
interchange-fixedOuter : {B C D : CAT Γ} {F G : MAP C D} {h k : MAP B C} (τ : F =₁ G) (σ : h ＝ k) → (const (τ ▷ k) ∙ (F ◁ σ)) =₁ ((G ◁ σ) ∙ const (τ ▷ h))
Proof / implementation
interchange-fixedOuter {F = F} {G} {h} {k} τ σ = comp₌-cong (id₌ (G ◁ σ)) (pre-constant τ h) ∙ (interchange (const τ) σ ∙ (comp₌-cong (pre-constant τ k) (id₌ (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.Section02.Specialization where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereinterchange-fixedInner
Derivation, checked
interchange-fixedInner : {B C D : CAT Γ} {F G : MAP C D} {h k : MAP B C} (τ : F ＝ G) (σ : h =₁ k) → ((τ ▷ k) ∙ const (F ◁ σ)) =₁ (const (G ◁ σ) ∙ (τ ▷ h))
Proof / implementation
interchange-fixedInner {F = F} {G} {h} {k} τ σ = comp₌-cong (post-constant G σ) (id₌ (τ ▷ h)) ∙ (interchange τ (const σ) ∙ (comp₌-cong (id₌ (τ ▷ k)) (post-constant 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.Section02.Specialization 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.
Agda Horizontal preservation
hcomp-id₌
Derivation, checked
hcomp-id₌ : {X C D E : CAT Γ} (g : MAP D E) (f : MAP C D) → (const {P = X} (id₌ g) ⋆ const (id₌ f)) =₁ (const (id₌ (g ∘ f)))
Proof / implementation
hcomp-id₌ g f = const-cong (postWhisker-id₌ g f) ∙ (post-constant g (id₌ f) ∙ hcomp-id-outer g (const (id₌ 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.Section02.Specialization where
module _ {Γ : Context} wherehcomp-comp₌
Derivation, checked
hcomp-comp₌ : {D E : CAT Γ} {f₀ f₁ f₂ : MAP C D} {g₀ g₁ g₂ : MAP D E} (β₂ : g₁ ＝ g₂) (β₁ : g₀ ＝ g₁) (α₂ : f₁ ＝ f₂) (α₁ : f₀ ＝ f₁) → ((β₂ ∙ β₁) ⋆ (α₂ ∙ α₁)) =₁ ((β₂ ⋆ α₂) ∙ (β₁ ⋆ α₁))
Proof / implementation
hcomp-comp₌ {f₁ = f₁} {f₂} {g₀ = g₀} {g₁} β₂ β₁ α₂ α₁ = let δ = β₂ ▷ f₂ γ = β₁ ▷ f₂ β = g₀ ◁ α₂ α = g₀ ◁ α₁ γ′ = g₁ ◁ α₂ β′ = β₁ ▷ f₁ expand : ((β₂ ∙ β₁) ⋆ (α₂ ∙ α₁)) =₁ ((δ ∙ γ) ∙ (β ∙ α)) expand = comp₌-cong (preWhisker-comp₌ β₂ β₁ f₂) (postWhisker-comp₌ g₀ α₂ α₁) exchange : (δ ∙ ((γ ∙ β) ∙ α)) =₁ (δ ∙ ((γ′ ∙ β′) ∙ α)) exchange = comp₌-cong (id₌ δ) (comp₌-cong (interchange β₁ α₂) (id₌ α)) in (reassociateFour δ γ′ β′ α) ⁻¹ ∙ (exchange ∙ (reassociateFour δ γ β α ∙ expand))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.HorizontalComposition where
module _ {Γ : Context} where
module _ {X C : CAT Γ} whereAbout this correspondence
Joint preservation is now proved in HorizontalComposition.hcomp-comp₌ using the current interchange axiom. Identity preservation is hcomp-id₌.
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.2.3 Units and associativity of functor composition
Composition of functors is unital and associative through specified identifications, called the unitors and associator.
Axiom A.6 (Unitors and associator). For functors \(f\colon C\to D\), \(g\colon D\to E\) and \(h\colon E\to F\), there are identifications \[ \lambda _f\colon \id _D\circ f= f,\qquad \rho _f\colon f\circ \id _C= f,\qquad \alpha _{f,g,h}\colon (h\circ g)\circ f= h\circ (g\circ f). \]
Agda Functor unitors and associator
comp-unitˡ
Assumption, type checked
comp-unitˡ : {C D : CAT Γ} (f : MAP C D) → (id D ∘ f) =₁ 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.Section02.Coherence where
module _ {Γ : Context} wherecomp-unitʳ
Assumption, type checked
comp-unitʳ : {C D : CAT Γ} (f : MAP C D) → (f ∘ id C) =₁ 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.Section02.Coherence where
module _ {Γ : Context} wherecomp-assoc
Assumption, type checked
comp-assoc : {B C D E : CAT Γ} (f : MAP B C) (g : MAP C D) (h : MAP D E) → ((h ∘ g) ∘ f) =₁ (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.Section02.Coherence 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.
The unitors and associator are compatible with identifications of the functors to which they are applied, in the following sense.
Axiom A.7 (Compatibility with horizontal composition). Horizontal composition of identifications is compatible with the unitality and associativity identifications from Axiom A.6:
-
For an identification \(\alpha \colon f = f'\) of functors \(C \to D\) there are commutative squares of identifications
Agda Horizontal unit comparisons
hcomp-id-outerDerivation, checked
hcomp-id-outer : {C D E : CAT Γ} {f f′ : MAP C D} (g : MAP D E) (α : f ＝ f′) → (const (id₌ g) ⋆ α) =₁ (g ◁ α)
Proof / implementation
hcomp-id-outer {f′ = f′} g α = comp₌-unitˡ (g ◁ α) ∙ comp₌-cong (const-cong (preWhisker-id₌ g f′) ∙ pre-constant (id₌ g) f′) (id₌ (g ◁ α))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section02.Specialization where module _ {Γ : Context} where module _ {X : CAT Γ} wherehcomp-id-innerDerivation, checked
hcomp-id-inner : {C D E : CAT Γ} {g g′ : MAP D E} (β : g ＝ g′) (f : MAP C D) → (β ⋆ const (id₌ f)) =₁ (β ▷ f)
Proof / implementation
hcomp-id-inner {g = g} β f = comp₌-unitʳ (β ▷ f) ∙ comp₌-cong (id₌ (β ▷ f)) (const-cong (postWhisker-id₌ g f) ∙ post-constant g (id₌ 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.Section02.Specialization where module _ {Γ : Context} where module _ {X : CAT Γ} wherepostWhisker-idDerivation, checked
postWhisker-id : {C D : CAT Γ} {f g : MAP C D} (α : f ＝ g) → (const (comp-unitˡ g) ∙ (id D ◁ α)) =₁ (α ∙ const (comp-unitˡ f))
Proof / implementation
postWhisker-id {D = D} {g = g} α = unitˡ-natural α ∙ (comp₌-cong (id₌ (const (comp-unitˡ g))) (hcomp-id-outer (id D) α)) ⁻¹
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section02.Whiskering where module _ {Γ : Context} where module _ {X : CAT Γ} wherepreWhisker-idDerivation, checked
preWhisker-id : {C D : CAT Γ} {f g : MAP C D} (α : f ＝ g) → (const (comp-unitʳ g) ∙ (α ▷ id C)) =₁ (α ∙ const (comp-unitʳ f))
Proof / implementation
preWhisker-id {C = C} {g = g} α = unitʳ-natural α ∙ (comp₌-cong (id₌ (const (comp-unitʳ g))) (hcomp-id-inner α (id 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.Section02.Whiskering 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.
-
For identifications \(\alpha \colon f = f'\), \(\beta \colon g = g'\) and \(\gamma \colon h = h'\), the following square of identifications commutes:
Agda Horizontal associativity comparison
postWhisker-compDerivation, checked
postWhisker-comp : {C D E F : CAT Γ} {f g : MAP C D} (α : f ＝ g) (u : MAP D E) (v : MAP E F) → N.NaturalityAt (N.Post (v ∘ u) (N.Input C D)) (N.Post v (N.Post u (N.Input C D))) (λ q → comp-assoc q u v) α
Proof / implementation
postWhisker-comp {f = f} {g} α u v = let normalize-top : ((const (id₌ v) ⋆ const (id₌ u)) ⋆ α) =₁ ((v ∘ u) ◁ α) normalize-top = hcomp-id-outer (v ∘ u) α ∙ hcomp-cong (hcomp-id₌ v u) (id₌ α) normalize-bottom : (const (id₌ v) ⋆ (const (id₌ u) ⋆ α)) =₁ (v ◁ (u ◁ α)) normalize-bottom = (postWhisker v ◁ hcomp-id-outer u α) ∙ hcomp-id-outer v (const (id₌ u) ⋆ α) in comp₌-cong normalize-bottom (id₌ (const (comp-assoc f u v))) ∙ (assoc-natural (const (id₌ v)) (const (id₌ u)) α ∙ (comp₌-cong (id₌ (const (comp-assoc g u v))) normalize-top) ⁻¹)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section02.Whiskering where module _ {Γ : Context} where module _ {X : CAT Γ} wherepreWhisker-compDerivation, checked
preWhisker-comp : {A B C D : CAT Γ} {f g : MAP C D} (α : f ＝ g) (k : MAP B C) (l : MAP A B) → (const (comp-assoc l k g) ∙ ((α ▷ k) ▷ l)) =₁ ((α ▷ (k ∘ l)) ∙ const (comp-assoc l k f))
Proof / implementation
preWhisker-comp {f = f} {g} α k l = let normalize-top : ((α ⋆ const (id₌ k)) ⋆ const (id₌ l)) =₁ ((α ▷ k) ▷ l) normalize-top = (preWhisker l ◁ hcomp-id-inner α k) ∙ hcomp-id-inner (α ⋆ const (id₌ k)) l normalize-bottom : (α ⋆ (const (id₌ k) ⋆ const (id₌ l))) =₁ (α ▷ (k ∘ l)) normalize-bottom = hcomp-id-inner α (k ∘ l) ∙ hcomp-cong (id₌ α) (hcomp-id₌ k l) in comp₌-cong normalize-bottom (id₌ (const (comp-assoc l k f))) ∙ (assoc-natural α (const (id₌ k)) (const (id₌ l)) ∙ (comp₌-cong (id₌ (const (comp-assoc l k g))) normalize-top) ⁻¹)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section02.Whiskering where module _ {Γ : Context} where module _ {X : CAT Γ} wherewhisker-mixedDerivation, checked
whisker-mixed : {B C D E : CAT Γ} {f g : MAP C D} (α : f ＝ g) (k : MAP B C) (u : MAP D E) → (const (comp-assoc k g u) ∙ ((u ◁ α) ▷ k)) =₁ ((u ◁ (α ▷ k)) ∙ const (comp-assoc k f u))
Proof / implementation
whisker-mixed {f = f} {g} α k u = let normalize-top : ((const (id₌ u) ⋆ α) ⋆ const (id₌ k)) =₁ ((u ◁ α) ▷ k) normalize-top = (preWhisker k ◁ hcomp-id-outer u α) ∙ hcomp-id-inner (const (id₌ u) ⋆ α) k normalize-bottom : (const (id₌ u) ⋆ (α ⋆ const (id₌ k))) =₁ (u ◁ (α ▷ k)) normalize-bottom = (postWhisker u ◁ hcomp-id-inner α k) ∙ hcomp-id-outer u (α ⋆ const (id₌ k)) in comp₌-cong normalize-bottom (id₌ (const (comp-assoc k f u))) ∙ (assoc-natural (const (id₌ u)) α (const (id₌ k)) ∙ (comp₌-cong (id₌ (const (comp-assoc k g u))) normalize-top) ⁻¹)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section02.Whiskering 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.
These comparisons are identifications of the corresponding functors on products of the input animae of identifications. Their restrictions along functors into those animae give the same formulas for identifications.
Remark 1.2.1. Taking some of the input identifications to be identities gives compatibility with identifications in each individual functor.
It will sometimes be convenient to abbreviate the conditions from Axiom A.7 as follows: \[ \id \ast \alpha = \alpha = \alpha \ast \id \qquadtext { and } (\gamma \ast \beta ) \ast \alpha = \gamma \ast (\beta \ast \alpha ). \] More generally, if we are given identifications \(\alpha \colon f = g\) and \(\alpha ' \colon f' = g'\) of functors \(C \to D\), and we happen to be given identifications \(f = f'\) and \(g = g'\), we will write \(\alpha = \alpha '\) to indicate the existence of a commutative square of identifications as follows:
Agda Comparison squares with different endpoints
SquareCell₌
Definition, checked
SquareCell₌ : {X C D : CAT Γ} {f g f′ g′ : MAP C D} → MAP X (f ＝ g) → MAP X (f′ ＝ g′) → MAP X (f ＝ f′) → MAP X (g ＝ g′) → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where
module Boundaries 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.2.4 The pentagon and triangle identities
Finally, the unitors and associator must themselves be compatible. The pentagon compares the two ways of reassociating a composite of four functors. The triangle compares removing an identity functor before or after reassociation.
Axiom A.8 (Pentagon and triangle identities). For functors \(f\colon A \to B\), \(g\colon B \to C\), \(h\colon C \to D\) and \(k\colon D \to E\), the following pentagon of identifications commutes:
Agda The pentagon
comp-pentagon
Assumption, type checked
comp-pentagon : {A B C D E : CAT Γ} (f : MAP A B) (g : MAP B C) (h : MAP C D) (k : MAP D E) → PentagonCommutes (associativityPentagon f g h k)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence 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.
Moreover, for composable functors \(f\colon C\to D\) and \(g\colon D\to E\), the following triangle of identifications commutes:
Agda The triangle identity
comp-triangle
Assumption, type checked
comp-triangle : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E) → TriangleCommutes (unitTriangle f g)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence 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.
Supplementary notes
- Specializing coherence laws AI-generated
- Whiskering and horizontal composition AI-generated