SCT.VolumeI.Chapter01.Section02.Coherence

Chapter 1, rebuild2, checked 14 October 2026 · source revision b982f5a.

# Composition and its coherences

The supplied coherence families are organized alongside Section 1.2.
The primitive interface uses a single interchange law over the product of
the two identification animae.
Whiskering compatibility is derived later from these axioms. The operations `α ∙ β`, `u ◁ α`, `α ▷ k`, and `β ⋆ α` apply to families
with a common source. That source is inferred, including when it is an
identification anima or a product of them. `const` is the ordinary constant
functor. Prescribed diagrams below make the naturality and coherence boundaries explicit.

```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section02.Coherence where

open import SCT.VolumeI.Chapter01.Section01.Vocabulary
open Operations
open import SCT.VolumeI.Chapter01.Section01.Terminal using (module Constructions)
open Constructions

module _ {Γ : Context} where
  postulate
    id₌ : {C D : CAT Γ} (f : MAP C D) → f =₁ f
    inv₌ : {C D : CAT Γ} {f g : MAP C D} → MAP (f ＝ g) (g ＝ f)
    comp₌ : {C D : CAT Γ} {f g h : MAP C D}
      → MAP ((g ＝ h) × (f ＝ g)) (f ＝ h)

module Composition where
  module _ {Γ : Context} where
    infixr  _∙_
    infixr  _⋆_
    infix  _⁻¹

    _⁻¹ : {P C D : CAT Γ} {f g : MAP C D} → MAP P (f ＝ g) → MAP P (g ＝ f)
    α ⁻¹ = inv₌ ∘ α

    _∙_ : {X C D : CAT Γ} {f g h : MAP C D}
      → MAP X (g ＝ h) → MAP X (f ＝ g) → MAP X (f ＝ h)
    β ∙ α = comp₌ ∘ pair β α

    _⋆_ : {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′))
    _⋆_ {f′ = f′} {g = g} β α = (β ▷ f′) ∙ (g ◁ α)

    hcomp : {C D E : CAT Γ} {f f′ : MAP C D} {g g′ : MAP D E}
      → MAP ((g ＝ g′) × (f ＝ f′)) ((g ∘ f) ＝ (g′ ∘ f′))
    hcomp = pr₁ ⋆ pr₂

module _ {Γ : Context} where
  postulate
    comp-unitˡ : {C D : CAT Γ} (f : MAP C D) → (id D ∘ f) =₁ f
    comp-unitʳ : {C D : CAT Γ} (f : MAP C D) → (f ∘ id C) =₁ f
    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))

```

Identity identifications, inversion and vertical composition are supplied;
horizontal composition and its parameterized functor are definitions.
The unit and associativity operations are supplied
early because later signatures use them.

## Vertical coherence

The next five axioms follow
`post:Composition_Of_Identifications`. Each is an identification
between actual functors on the displayed parameter category.

```agda
module _ {Γ : Context} where
  open Composition
  postulate
    comp₌-unitˡ : {C D : CAT Γ} (f g : MAP C D)
      → let α = id (f ＝ g)
        in (const (id₌ g) ∙ α) =₁ α

    comp₌-unitʳ : {C D : CAT Γ} (f g : MAP C D)
      → let α = id (f ＝ g)
        in (α ∙ const (id₌ f)) =₁ α

    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 ((γ ∙ β) ∙ α) =₁ (γ ∙ (β ∙ α))

    comp₌-inverseˡ : {C D : CAT Γ} (f g : MAP C D)
      → let α = id (f ＝ g)
        in (α ⁻¹ ∙ α) =₁ (const (id₌ f))

    comp₌-inverseʳ : {C D : CAT Γ} (f g : MAP C D)
      → let α = id (f ＝ g)
        in (α ∙ α ⁻¹) =₁ (const (id₌ g))
```

The next axioms supply whiskering and interchange comparisons.
Identity preservation has no varying identification input. The remaining
laws are parameterized. Interchange is supplied jointly in both inputs,
using the two projections from their product as universal families.

```agda
module _ {Γ : Context} where
  open Composition
  postulate
    postWhisker-id₌ : {C D E : CAT Γ} (u : MAP D E) (f : MAP C D)
      → (u ◁ id₌ f) =₂ (id₌ (u ∘ f))

    preWhisker-id₌ : {B C D : CAT Γ} (f : MAP C D) (k : MAP B C)
      → (id₌ f ▷ k) =₂ (id₌ (f ∘ k))

    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 ◁ σ))

    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))

    interchange : {B C D : CAT Γ} (F G : MAP C D) (h k : MAP B C)
      → let τ : MAP ((F ＝ G) × (h ＝ k)) (F ＝ G)
            τ = pr₁
            σ : MAP ((F ＝ G) × (h ＝ k)) (h ＝ k)
            σ = pr₂
        in ((τ ▷ k) ∙ (F ◁ σ)) =₁ ((G ◁ σ) ∙ (τ ▷ h))

```

## Prescribed boundaries

The diagrams below have identification families as edges, all over one
common parameter category `X`, between parallel functors. They are distinct
from the squares between functors in Section03, whose edges are functors.

A square of identification families with prescribed sides commutes when
its two composite routes are identified. `SquareCell₌ top bottom left right`
is that single equation, for families given directly. `SquareBoundary`
bundles the same four edges when a named diagram is useful, and
`SquareCommutes` is the same cell for the bundled edges. Neither is a record
containing a proof, and a square with unspecified sides would be weaker.

```agda
module Boundaries where
  module _ {Γ : Context} where
    open Composition

    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
    SquareCell₌ top bottom left right = (right ∙ top) =₁ (bottom ∙ left)

    record SquareBoundary {X C D : CAT Γ} (f g f′ g′ : MAP C D) : Set m where
      constructor square-boundary
      field
        top : MAP X (f ＝ g)
        bottom : MAP X (f′ ＝ g′)
        left : MAP X (f ＝ f′)
        right : MAP X (g ＝ g′)

    SquareCommutes : {X C D : CAT Γ} {f g f′ g′ : MAP C D}
      → SquareBoundary {X = X} f g f′ g′ → Set m
    SquareCommutes S = SquareCell₌ top bottom left right
      where open SquareBoundary S

    associator-naturality-square : {X B C D E : CAT Γ}
      {f f′ : MAP B C} {g g′ : MAP C D} {h h′ : MAP D E}
      (γ : MAP X (h ＝ h′)) (β : MAP X (g ＝ g′)) (α : MAP X (f ＝ f′))
      → SquareBoundary {X = X} ((h ∘ g) ∘ f) ((h′ ∘ g′) ∘ f′)
          (h ∘ (g ∘ f)) (h′ ∘ (g′ ∘ f′))
    associator-naturality-square {f = f} {f′} {g} {g′} {h} {h′} γ β α =
      square-boundary ((γ ⋆ β) ⋆ α) (γ ⋆ (β ⋆ α))
        (const (comp-assoc f g h)) (const (comp-assoc f′ g′ h′))

    unitˡ-naturality-square : {R C D : CAT Γ} {f f′ : MAP C D}
      (α : MAP R (f ＝ f′))
      → SquareBoundary {X = R} (id D ∘ f) (id D ∘ f′) f f′
    unitˡ-naturality-square {D = D} {f = f} {f′ = f′} α =
      square-boundary (const (id₌ (id D)) ⋆ α) α
        (const (comp-unitˡ f)) (const (comp-unitˡ f′))

    unitʳ-naturality-square : {R C D : CAT Γ} {f f′ : MAP C D}
      (α : MAP R (f ＝ f′))
      → SquareBoundary {X = R} (f ∘ id C) (f′ ∘ id C) f f′
    unitʳ-naturality-square {C = C} {f = f} {f′ = f′} α =
      square-boundary (α ⋆ const (id₌ (id C))) α
        (const (comp-unitʳ f)) (const (comp-unitʳ f′))

```

A triangle has three vertices `v₀`, `v₁`, `v₂`. Its source route is the
direct edge from `v₀` to `v₂`; its target route passes through `v₁`.
A pentagon has five vertices. Its source route has two edges,
`v₀ → v₁ → v₂`, and its target route has three edges,
`v₀ → v₃ → v₄ → v₂`, composed in the left-associated order
`(third ∙ second) ∙ first`. Commutativity identifies the two routes.

```agda
    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₂)

    module _ {X C D : CAT Γ} {v₀ v₁ v₂ : MAP C D} where
      TriangleSource : TriangleDiagram {X = X} v₀ v₁ v₂ → MAP X (v₀ ＝ v₂)
      TriangleSource T = TriangleDiagram.direct T

      TriangleTarget : TriangleDiagram {X = X} v₀ v₁ v₂ → MAP X (v₀ ＝ v₂)
      TriangleTarget T = second ∙ first
        where open TriangleDiagram T

      TriangleCommutes : TriangleDiagram {X = X} v₀ v₁ v₂ → Set m
      TriangleCommutes T = TriangleSource T =₁ TriangleTarget T

    record PentagonDiagram {X C D : CAT Γ} (v₀ v₁ v₂ v₃ v₄ : MAP C D) : Set m where
      constructor pentagon-diagram
      field
        source-first : MAP X (v₀ ＝ v₁)
        source-second : MAP X (v₁ ＝ v₂)
        target-first : MAP X (v₀ ＝ v₃)
        target-second : MAP X (v₃ ＝ v₄)
        target-third : MAP X (v₄ ＝ v₂)

    module _ {X C D : CAT Γ} {v₀ v₁ v₂ v₃ v₄ : MAP C D} where
      PentagonSource : PentagonDiagram {X = X} v₀ v₁ v₂ v₃ v₄ → MAP X (v₀ ＝ v₂)
      PentagonSource P = source-second ∙ source-first
        where open PentagonDiagram P

      PentagonTarget : PentagonDiagram {X = X} v₀ v₁ v₂ v₃ v₄ → MAP X (v₀ ＝ v₂)
      PentagonTarget P = (target-third ∙ target-second) ∙ target-first
        where open PentagonDiagram P

      PentagonCommutes : PentagonDiagram {X = X} v₀ v₁ v₂ v₃ v₄ → Set m
      PentagonCommutes P = PentagonSource P =₁ PentagonTarget P

```

The next axioms supply comparisons concerning the **derived** horizontal
operation (`post:Horizontal_Composition_Is_Unital_And_Associative`). Naming the
operation does not promote it to an additional primitive.

```agda
module _ {Γ : Context} where
  open Composition
  open Boundaries
  postulate
    unitˡ-natural : {C D : CAT Γ} (f f′ : MAP C D)
      → let α = id (f ＝ f′)
        in (const (comp-unitˡ f′) ∙ (const (id₌ (id D)) ⋆ α)) =₁
          (α ∙ const (comp-unitˡ f))

    unitʳ-natural : {C D : CAT Γ} (f f′ : MAP C D)
      → let α = id (f ＝ f′)
        in (const (comp-unitʳ f′) ∙ (α ⋆ const (id₌ (id C)))) =₁
          (α ∙ const (comp-unitʳ f))

    assoc-natural : {B C D E : CAT Γ} (f f′ : MAP B C) (g g′ : MAP C D) (h h′ : MAP D E)
      → let X = ((h ＝ h′) × (g ＝ g′)) × (f ＝ f′)
            α : MAP X (f ＝ f′)
            α = pr₂
            β : MAP X (g ＝ g′)
            β = pr₂ ∘ pr₁
            γ : MAP X (h ＝ h′)
            γ = pr₁ ∘ pr₁
        in (const (comp-assoc f′ g′ h′) ∙ ((γ ⋆ β) ⋆ α)) =₁
          ((γ ⋆ (β ⋆ α)) ∙ const (comp-assoc f g h))
```

The final axioms retain the book's horizontal composites literally
(`post:Pentagon_And_Triangle_Identities`). Four composable functors generate
the associativity pentagon. Its source route reassociates twice through
`(k ∘ h) ∘ (g ∘ f)`; its target route passes through `(k ∘ (h ∘ g)) ∘ f`
and `k ∘ ((h ∘ g) ∘ f)` and is left associated. The outer edges of the
target route are horizontal composites with identity identifications, kept
literally rather than replaced by whiskerings. Two composable functors
generate the unit triangle, through `g ∘ (id D ∘ f)`. Both diagrams have
the parameter `One`, so their commutativity is an identification of
absolute identifications. These axioms compare pastings; they are not
Agda equalities.

```agda
module _ {Γ : Context} where
  open Composition
  open Boundaries

  associativityPentagon : {A B C D E : CAT Γ} (f : MAP A B) (g : MAP B C)
    (h : MAP C D) (k : MAP D E)
    → PentagonDiagram {X = One}
        (((k ∘ h) ∘ g) ∘ f) ((k ∘ h) ∘ (g ∘ f)) (k ∘ (h ∘ (g ∘ f)))
        ((k ∘ (h ∘ g)) ∘ f) (k ∘ ((h ∘ g) ∘ f))
  associativityPentagon f g h k = pentagon-diagram
    (comp-assoc f g (k ∘ h)) (comp-assoc (g ∘ f) h k)
    (comp-assoc g h k ⋆ id₌ f) (comp-assoc f (h ∘ g) k) (id₌ k ⋆ comp-assoc f g h)

  unitTriangle : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E)
    → TriangleDiagram {X = One} ((g ∘ id D) ∘ f) (g ∘ (id D ∘ f)) (g ∘ f)
  unitTriangle {D = D} f g = triangle-diagram
    (comp-unitʳ g ⋆ id₌ f) (comp-assoc f (id D) g) (id₌ g ⋆ comp-unitˡ f)

  postulate
    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)

    comp-triangle : {C D E : CAT Γ} (f : MAP C D) (g : MAP D E)
      → TriangleCommutes (unitTriangle f g)
```

Unfolding the definitions, `comp-pentagon f g h k` is the original equation

    comp-assoc (g ∘ f) h k ∙ comp-assoc f g (k ∘ h) =₂
      ((id₌ k ⋆ comp-assoc f g h) ∙ comp-assoc f (h ∘ g) k) ∙ (comp-assoc g h k ⋆ id₌ f)

and `comp-triangle f g` is
`(comp-unitʳ g ⋆ id₌ f) =₂ ((id₌ g ⋆ comp-unitˡ f) ∙ comp-assoc f (id D) g)`.