SCT.VolumeI.Chapter01.Section03.Identifications.Triangles

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

# Specified triangles under restriction and postcomposition

A *triangle* is an identification `b : π ∘ h =₁ x`: the functor `x` factors
through `π` with factor `h` (Section03.Factorizations views it so). Many
constructions specify such triangles and must compute how they change when
the factor is restricted along a functor `r`, or when `π` is postcomposed with
a functor `F`. This module provides the two operations,

    restrict-triangle π h b r : π ∘ (h ∘ r) =₁ x ∘ r
    post-triangle F π h b     : (F ∘ π) ∘ h =₁ F ∘ x,

and their effect on *squares of triangles*. Given triangles `b` for `h` and
`b′` for `h′`, an identification family `δ : h = h′` *lies over*
`α : x = x′` when the identification square

    SquareCell₌ (π ◁ δ) α b b′,   that is   b′ ∙ (π ◁ δ) =₁ α ∙ b,

commutes. For families, the fixed triangles enter as constant families;
`unconst-sides₌` converts the instance at `One` into the individual equation.
Restriction and postcomposition carry squares to squares. Postcomposing
twice agrees with postcomposing with the composite, and restricting twice
agrees with restricting along the composite, both up to the external
associators: these two laws use the whiskered pentagon. The final part
records the unit computations, which use Kelly's lemmas.

```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Identifications.Triangles where

open import SCT.VolumeI.Chapter01.Section01.Vocabulary hiding (_＝_)
import SCT.VolumeI.Chapter01.Section01.Terms as Terms
open Terms using (Equal)
open Operations
open import SCT.VolumeI.Chapter01.Section01.Terminal using (module Constructions)
open Constructions
open import SCT.VolumeI.Chapter01.Section02.Coherence
  using (id₌; comp-unitˡ; comp-unitʳ; comp-assoc; postWhisker-id₌; preWhisker-id₌;
    module Composition; module Boundaries)
open Composition
open Boundaries using (SquareCell₌)
open import SCT.VolumeI.Chapter01.Section02.Specialization
open import SCT.VolumeI.Chapter01.Section02.Whiskering
open import SCT.VolumeI.Chapter01.Section03.Identifications.Inverses
open import SCT.VolumeI.Chapter01.Section03.Identifications.IdentificationSquares
open import SCT.VolumeI.Chapter01.Section03.Identifications.FunctorCoherence
```

## Restriction and postcomposition

A triangle whose value is itself a composite `f ∘ ρ` is the cell of a square
of functors; postcomposing it with `F` and reassociating the value gives
`post-square-cell`.

```agda
module _ {Γ : Context} where
  module _ {R X : CAT Γ} where
    open Terms.InContext X using (Term)

    restrict-triangle : {K C : CAT Γ} (π : MAP K C) (z : Term K) {x : Term C}
      → (π ∘ z) =₁ x → (r : MAP R X) → (π ∘ (z ∘ r)) =₁ (x ∘ r)
    restrict-triangle π z b r = (b ▷ r) ∙ (comp-assoc r z π) ⁻¹

  module _ {X : CAT Γ} where
    open Terms.InContext X using (Term)

    post-triangle : {K A B : CAT Γ} (F : MAP A B) (π : MAP K A) (z : Term K)
      {x : Term A} → (π ∘ z) =₁ x → ((F ∘ π) ∘ z) =₁ (F ∘ x)
    post-triangle F π z b = (F ◁ b) ∙ comp-assoc z π F

  module _ {R X : CAT Γ} where
    open Terms.InContext X using (Term)

    post-square-cell : {K C D : CAT Γ} (F : MAP C D)
      (ρ : MAP R X) (x : Term C) (π : MAP K C) (h : MAP R K)
      → (π ∘ h) =₁ (x ∘ ρ) → ((F ∘ π) ∘ h) =₁ ((F ∘ x) ∘ ρ)
    post-square-cell F ρ x π h b = (comp-assoc ρ x F) ⁻¹ ∙ post-triangle F π h b
```

## Squares of triangles

Restricting a square of triangles along `r` gives a square of the restricted
triangles: whisker the square by `r`, then move the restriction inside the
postwhiskering by the mixed whiskering law. Changing the functor along which
a fixed triangle is restricted gives the corresponding square by
interchange. Both are stated for families; the instances at `One` are
recorded with the individual triangles as sides.

```agda
module _ {Γ : Context} where
  private
    module _ {A R X : CAT Γ} where
      open Terms.InContext X using (Term)

      restricted-side : {K C : CAT Γ} (π : MAP K C) (z : Term K) {x : Term C}
        (b : (π ∘ z) =₁ x) (r : MAP R X)
        → ((const {P = A} b ▷ r) ∙ (const (comp-assoc r z π)) ⁻¹) =₁
            const (restrict-triangle π z b r)
      restricted-side  π z b r =
        const-comp {X = A} (b ▷ r) ((comp-assoc r z π) ⁻¹) ∙
          comp₌-cong (pre-constant b r) ((const-inv (comp-assoc r z π)) ⁻¹)

  module _ {A R X : CAT Γ} where
    open Terms.InContext X using (Term)
    open Terms.Equalities A using (_＝_)

    restrict-square : {K C : CAT Γ} (π : MAP K C)
      {z z′ : Term K} {x x′ : Term C}
      (δ : z ＝ z′) (α : x ＝ x′)
      (b : (π ∘ z) =₁ x) (b′ : (π ∘ z′) =₁ x′) (r : MAP R X)
      → SquareCell₌ (π ◁ δ) α (const b) (const b′)
      → SquareCell₌ (π ◁ (δ ▷ r)) (α ▷ r)
          (const (restrict-triangle π z b r)) (const (restrict-triangle π z′ b′ r))
    restrict-square π {z} {z′} δ α b b′ r square =
      replace-sides₌ (restricted-side π z b r) (restricted-side π z′ b′ r)
        (paste-square₌ {t = π ◁ (δ ▷ r)} {m = (π ◁ δ) ▷ r} {b = α ▷ r}
          (inverse-square₌ {t = (π ◁ δ) ▷ r} {b = π ◁ (δ ▷ r)}
            {l = const (comp-assoc r z π)} {r = const (comp-assoc r z′ π)}
            (whisker-mixed δ r π))
          (pre-square₌ r square))

    restrict-change-square : {K C : CAT Γ} (π : MAP K C)
      (z : Term K) (x : Term C) (b : (π ∘ z) =₁ x)
      {r s : MAP R X} (γ : r ＝ s)
      → SquareCell₌ (π ◁ (z ◁ γ)) (x ◁ γ)
          (const (restrict-triangle π z b r)) (const (restrict-triangle π z b s))
    restrict-change-square π z x b {r} {s} γ =
      replace-sides₌ (restricted-side π z b r) (restricted-side π z b s)
        (paste-square₌ {t = π ◁ (z ◁ γ)} {m = (π ∘ z) ◁ γ} {b = x ◁ γ}
          (inverse-square₌ {t = (π ∘ z) ◁ γ} {b = π ◁ (z ◁ γ)}
            {l = const (comp-assoc r z π)} {r = const (comp-assoc s z π)}
            (postWhisker-comp γ z π))
          (replace-sides₌ ((pre-constant b r) ⁻¹) ((pre-constant b s) ⁻¹)
            (interchange-fixedOuter b γ)))

  module _ {R X : CAT Γ} where
    open Terms.InContext X using (Term)

    restrict-square-One : {K C : CAT Γ} (π : MAP K C)
      {z z′ : Term K} {x x′ : Term C}
      (δ : z =₁ z′) (α : x =₁ x′)
      (b : (π ∘ z) =₁ x) (b′ : (π ∘ z′) =₁ x′) (r : MAP R X)
      → SquareCell₌ (π ◁ δ) α b b′
      → SquareCell₌ (π ◁ (δ ▷ r)) (α ▷ r)
          (restrict-triangle π z b r) (restrict-triangle π z′ b′ r)
    restrict-square-One π δ α b b′ r square =
      unconst-sides₌ (restrict-square π δ α b b′ r (const-sides₌ square))

    restrict-change-square-One : {K C : CAT Γ} (π : MAP K C)
      (z : Term K) (x : Term C) (b : (π ∘ z) =₁ x)
      {r s : MAP R X} (γ : r =₁ s)
      → SquareCell₌ (π ◁ (z ◁ γ)) (x ◁ γ)
          (restrict-triangle π z b r) (restrict-triangle π z b s)
    restrict-change-square-One π z x b γ =
      unconst-sides₌ (restrict-change-square π z x b γ)
```

A square of triangles can also be stated before restricting the triangles:
moving the associator from the restricted triangle to the edge gives an
equivalent square, recorded in the forward direction used by its clients.

```agda
  module _ {R T X : CAT Γ} where
    open Terms.InContext X using (Term)

    unrestrict-square : {A : CAT Γ} (π : Term A)
      (q : MAP T X) (r : MAP R T) (q′ : MAP R X)
      {p : MAP T A} {p′ : MAP R A}
      (δ : (q ∘ r) =₁ q′) (b : (π ∘ q) =₁ p)
      (b′ : (π ∘ q′) =₁ p′) (c : (p ∘ r) =₁ p′)
      → (b′ ∙ (π ◁ δ)) =₂ (c ∙ restrict-triangle π q b r)
      → (b′ ∙ ((π ◁ δ) ∙ comp-assoc r q π)) =₂ (c ∙ (b ▷ r))
    unrestrict-square π q r q′ δ b b′ c square =
      let A = comp-assoc r q π
      in comp₌-cong (id₌ c) (inv-comp-right (b ▷ r) A) ∙
        (comp₌-assoc c ((b ▷ r) ∙ A ⁻¹) A ∙
          (comp₌-cong square (id₌ A) ∙ (comp₌-assoc b′ (π ◁ δ) A) ⁻¹))
```

Two triangles and a square identify two projected composites. Cancelling the
common triangle `c` reflects the comparison of projected routes.

```agda
  module _ {A X : CAT Γ} where
    open Terms.InContext X using (Term)
    open Terms.Equalities A using (_＝_)

    projected-square : {K C : CAT Γ} {z₀ h₁ z₂ h₃ : Term K} {z₁ z₃ : Term C}
      (π : MAP K C) (ρ : h₁ ＝ h₃) (τ : z₀ ＝ h₁)
      (υ : z₂ ＝ h₃) (δ : z₀ ＝ z₂)
      (b : (π ∘ h₁) =₁ z₁) (c : (π ∘ h₃) =₁ z₃)
      (α : z₁ ＝ z₃)
      (q : ((π ∘ z₀) ＝ z₁)) (q′ : ((π ∘ z₂) ＝ z₃))
      → SquareCell₌ (π ◁ ρ) α (const b) (const c)
      → (const b ∙ (π ◁ τ)) =₁ q
      → (const c ∙ (π ◁ υ)) =₁ q′
      → (q′ ∙ (π ◁ δ)) =₁ (α ∙ q)
      → (π ◁ (ρ ∙ τ)) =₁ (π ◁ (υ ∙ δ))
    projected-square π ρ τ υ δ b c α q q′ top left bottom square =
      let left-normal = comp₌-cong (id₌ α) left ∙
            (comp₌-assoc α (const b) (π ◁ τ) ∙
              (comp₌-cong top (id₌ (π ◁ τ)) ∙ project-composite π ρ τ (const c)))
          right-normal = square ∙
            (comp₌-cong bottom (id₌ (π ◁ δ)) ∙ project-composite π υ δ (const c))
      in cancel-left (const c) (right-normal ⁻¹ ∙ left-normal)
```

## Naturality of postcomposition

Postcomposing a triangle is natural in the postcomposed functor and,
given a square of triangles, in the factor. The same holds for
postcomposition of square cells. All four are stated for families.

```agda
module _ {Γ : Context} where
  module _ {A X : CAT Γ} where
    open Terms.InContext X using (Term)
    open Terms.Equalities A using (_＝_)

    post-triangle-outer : {K C D : CAT Γ} {F G : MAP C D}
      (θ : F ＝ G) (π : MAP K C) (t : Term K) {p : Term C}
      (b : (π ∘ t) =₁ p)
      → SquareCell₌ ((θ ▷ π) ▷ t) (θ ▷ p)
          (const (post-triangle F π t b)) (const (post-triangle G π t b))
    post-triangle-outer  {F = F} {G} θ π t {p} b =
      replace-sides₌ (const-comp {X = A} (F ◁ b) (comp-assoc t π F))
        (const-comp {X = A} (G ◁ b) (comp-assoc t π G))
        (paste-square₌ {t = (θ ▷ π) ▷ t} {m = θ ▷ (π ∘ t)} {b = θ ▷ p}
          (preWhisker-comp θ π t) ((interchange-fixedInner θ b) ⁻¹))

    post-triangle-inner : {K C D : CAT Γ} (F : MAP C D) (π : MAP K C)
      {t t′ : Term K} {p p′ : Term C}
      (δ : t ＝ t′) (α : p ＝ p′)
      (b : (π ∘ t) =₁ p) (b′ : (π ∘ t′) =₁ p′)
      → SquareCell₌ (π ◁ δ) α (const b) (const b′)
      → SquareCell₌ ((F ∘ π) ◁ δ) (F ◁ α)
          (const (post-triangle F π t b)) (const (post-triangle F π t′ b′))
    post-triangle-inner  F π {t} {t′} δ α b b′ square =
      replace-sides₌
        (const-comp {X = A} (F ◁ b) (comp-assoc t π F) ∙
          comp₌-cong (post-constant F b) (id₌ (const (comp-assoc t π F))))
        (const-comp {X = A} (F ◁ b′) (comp-assoc t′ π F) ∙
          comp₌-cong (post-constant F b′) (id₌ (const (comp-assoc t′ π F))))
        (paste-square₌ {t = (F ∘ π) ◁ δ} {m = F ◁ (π ◁ δ)} {b = F ◁ α}
          (postWhisker-comp δ π F) (post-square₌ F square))

  module _ {A R X : CAT Γ} where
    open Terms.InContext X using (Term)
    open Terms.Equalities A using (_＝_)

    post-square-cell-outer : {K C D : CAT Γ}
      (ρ : MAP R X) (x : Term C) (π : MAP K C) (h : MAP R K)
      (b : (π ∘ h) =₁ (x ∘ ρ)) {F F′ : MAP C D} (θ : F ＝ F′)
      → SquareCell₌ ((θ ▷ π) ▷ h) ((θ ▷ x) ▷ ρ)
          (const (post-square-cell F ρ x π h b)) (const (post-square-cell F′ ρ x π h b))
    post-square-cell-outer  ρ x π h b {F} {F′} θ =
      replace-sides₌
        (const-comp {X = A} ((comp-assoc ρ x F) ⁻¹) (post-triangle F π h b) ∙
          comp₌-cong ((const-inv (comp-assoc ρ x F)) ⁻¹) (id₌ (const (post-triangle F π h b))))
        (const-comp {X = A} ((comp-assoc ρ x F′) ⁻¹) (post-triangle F′ π h b) ∙
          comp₌-cong ((const-inv (comp-assoc ρ x F′)) ⁻¹) (id₌ (const (post-triangle F′ π h b))))
        (paste-square₌ {t = (θ ▷ π) ▷ h} {m = θ ▷ (x ∘ ρ)} {b = (θ ▷ x) ▷ ρ}
          (post-triangle-outer θ π h b)
          (inverse-square₌ {t = (θ ▷ x) ▷ ρ} {b = θ ▷ (x ∘ ρ)}
            {l = const (comp-assoc ρ x F)} {r = const (comp-assoc ρ x F′)}
            (preWhisker-comp θ x ρ)))

    post-square-cell-inner : {K C D : CAT Γ}
      (ρ : MAP R X) (π : MAP K C) (F : MAP C D)
      {x x′ : Term C} {h h′ : MAP R K}
      (b : (π ∘ h) =₁ (x ∘ ρ)) (b′ : (π ∘ h′) =₁ (x′ ∘ ρ))
      (α : x ＝ x′) (δ : h ＝ h′)
      → SquareCell₌ (π ◁ δ) (α ▷ ρ) (const b) (const b′)
      → SquareCell₌ ((F ∘ π) ◁ δ) ((F ◁ α) ▷ ρ)
          (const (post-square-cell F ρ x π h b)) (const (post-square-cell F ρ x′ π h′ b′))
    post-square-cell-inner  ρ π F {x} {x′} {h} {h′} b b′ α δ square =
      replace-sides₌
        (const-comp {X = A} ((comp-assoc ρ x F) ⁻¹) (post-triangle F π h b) ∙
          comp₌-cong ((const-inv (comp-assoc ρ x F)) ⁻¹) (id₌ (const (post-triangle F π h b))))
        (const-comp {X = A} ((comp-assoc ρ x′ F) ⁻¹) (post-triangle F π h′ b′) ∙
          comp₌-cong ((const-inv (comp-assoc ρ x′ F)) ⁻¹) (id₌ (const (post-triangle F π h′ b′))))
        (paste-square₌ {t = (F ∘ π) ◁ δ} {m = F ◁ (α ▷ ρ)} {b = (F ◁ α) ▷ ρ}
          (post-triangle-inner F π δ (α ▷ ρ) b b′ square)
          (inverse-square₌ {t = (F ◁ α) ▷ ρ} {b = F ◁ (α ▷ ρ)}
            {l = const (comp-assoc ρ x F)} {r = const (comp-assoc ρ x′ F)}
            (whisker-mixed α ρ F)))
```

## Successive restriction and postcomposition

Restricting along `σ` and then `τ` agrees with restricting along `σ ∘ τ`:
the factor associator lies over the value associator. Postcomposing a square
cell with `g` and then `f` agrees with postcomposing with `f ∘ g`, up to the
associators at the source and target. Both proofs solve a whiskered
pentagon for a corner.

```agda
module _ {Γ : Context} where
  module _ {Q R X : CAT Γ} where
    open Terms.InContext X using (Term)

    restrict-triangle-assoc : {K C : CAT Γ} (π : MAP K C) (z : Term K)
      {x : Term C} (b : (π ∘ z) =₁ x) (σ : MAP R X) (τ : MAP Q R)
      → SquareCell₌ (π ◁ comp-assoc τ σ z) (comp-assoc τ σ x)
          (restrict-triangle π (z ∘ σ) (restrict-triangle π z b σ) τ)
          (restrict-triangle π z b (σ ∘ τ))
    restrict-triangle-assoc π z {x} b σ τ =
      let A = comp-assoc τ σ x
          B = (b ▷ σ) ▷ τ
          E = comp-assoc σ z π ▷ τ
          D′ = comp-assoc τ (z ∘ σ) π
          B′ = comp-assoc τ σ (π ∘ z)
          A′ = comp-assoc (σ ∘ τ) z π
          C′ = π ◁ comp-assoc τ σ z
          b′ = b ▷ (σ ∘ τ)
          tail = E ⁻¹ ∙ D′ ⁻¹
          expand = comp₌-cong
            ((comp₌-assoc A B (E ⁻¹)) ⁻¹ ∙
              comp₌-cong (id₌ A)
                (comp₌-cong (id₌ B) (preWhisker-inverse (comp-assoc σ z π) τ) ∙
                  preWhisker-comp₌ (b ▷ σ) ((comp-assoc σ z π) ⁻¹) τ))
            (id₌ (D′ ⁻¹))
          exchange = comp₌-cong
            (comp₌-cong (preWhisker-comp-One b σ τ) (id₌ (E ⁻¹)))
            (id₌ (D′ ⁻¹))
          regroup = comp₌-assoc b′ B′ tail ∙ comp₌-assoc (b′ ∙ B′) (E ⁻¹) (D′ ⁻¹)
          corner = solve-pentagon A′ B′ C′ D′ E (pentagon-whiskered τ σ z π)
          original : ((A ∙ (restrict-triangle π z b σ ▷ τ)) ∙ D′ ⁻¹) =₂
            (restrict-triangle π z b (σ ∘ τ) ∙ C′)
          original = (comp₌-assoc b′ (A′ ⁻¹) C′) ⁻¹ ∙
            (comp₌-cong (id₌ b′) corner ∙ (regroup ∙ (exchange ∙ expand)))
      in comp₌-assoc A (restrict-triangle π z b σ ▷ τ) (D′ ⁻¹) ∙ original ⁻¹

    restrict-triangle-twice : {K C : CAT Γ} (π : MAP K C) (z : Term K)
      {x : Term C} (b : (π ∘ z) =₁ x) (σ : MAP R X) (τ : MAP Q R)
      → ((comp-assoc τ σ x ∙ (restrict-triangle π z b σ ▷ τ)) ∙
            (comp-assoc τ (z ∘ σ) π) ⁻¹) =₂
          (restrict-triangle π z b (σ ∘ τ) ∙ (π ◁ comp-assoc τ σ z))
    restrict-triangle-twice π z {x} b σ τ = (restrict-triangle-assoc π z b σ τ) ⁻¹ ∙
      comp₌-assoc (comp-assoc τ σ x) (restrict-triangle π z b σ ▷ τ)
        ((comp-assoc τ (z ∘ σ) π) ⁻¹)

  module _ {R X : CAT Γ} where
    open Terms.InContext X using (Term)

    post-square-cell-comp : {K C D E : CAT Γ}
      (ρ : MAP R X) (s : Term C) (π : MAP K C) (h : MAP R K)
      (b : (π ∘ h) =₁ (s ∘ ρ)) (g : MAP C D) (f : MAP D E)
      → SquareCell₌ (comp-assoc π g f ▷ h) (comp-assoc s g f ▷ ρ)
          (post-square-cell (f ∘ g) ρ s π h b)
          (post-square-cell f ρ (g ∘ s) (g ∘ π) h (post-square-cell g ρ s π h b))
    post-square-cell-comp ρ s π h b g f =
      let inputLeft = comp-assoc h π (f ∘ g)
          middleLeft = (f ∘ g) ◁ b
          outputLeft = (comp-assoc ρ s (f ∘ g)) ⁻¹
          inputRight = (f ◁ comp-assoc h π g) ∙ comp-assoc h (g ∘ π) f
          middleRight = f ◁ (g ◁ b)
          outputRight = (comp-assoc ρ (g ∘ s) f) ⁻¹ ∙ (f ◁ (comp-assoc ρ s g) ⁻¹)
          atSource = comp-assoc π g f ▷ h
          afterInput = comp-assoc (π ∘ h) g f
          beforeOutput = comp-assoc (s ∘ ρ) g f
          atTarget = comp-assoc s g f ▷ ρ
          inputSquare : SquareCell₌ atSource afterInput inputLeft inputRight
          inputSquare = (pentagon-whiskered h π g f) ⁻¹
          middleSquare : SquareCell₌ afterInput beforeOutput middleLeft middleRight
          middleSquare = (postWhisker-comp-One b g f) ⁻¹
          outputSquare : SquareCell₌ beforeOutput atTarget outputLeft outputRight
          outputSquare = pentagon-left-corner beforeOutput (comp-assoc ρ s (f ∘ g))
              (f ◁ comp-assoc ρ s g) (comp-assoc ρ (g ∘ s) f) atTarget
              (pentagon-whiskered ρ s g f) ∙
            (comp₌-assoc ((comp-assoc ρ (g ∘ s) f) ⁻¹)
              ((f ◁ comp-assoc ρ s g) ⁻¹) beforeOutput ∙
            comp₌-cong
              (comp₌-cong (id₌ ((comp-assoc ρ (g ∘ s) f) ⁻¹))
                (postWhisker-inverse f (comp-assoc ρ s g)))
              (id₌ beforeOutput))
          assembled : SquareCell₌ atSource atTarget
            (outputLeft ∙ (middleLeft ∙ inputLeft)) (outputRight ∙ (middleRight ∙ inputRight))
          assembled = paste-square₌ (paste-square₌ inputSquare middleSquare) outputSquare
          outside = (comp-assoc ρ (g ∘ s) f) ⁻¹
          firstImage = f ◁ (comp-assoc ρ s g) ⁻¹
          lastImage = f ◁ comp-assoc h π g
          finalInput = comp-assoc h (g ∘ π) f
          mergeImages : (firstImage ∙ (middleRight ∙ lastImage)) =₂
            (f ◁ post-square-cell g ρ s π h b)
          mergeImages = (postWhisker-comp₌ f ((comp-assoc ρ s g) ⁻¹) ((g ◁ b) ∙ comp-assoc h π g)) ⁻¹ ∙
            comp₌-cong (id₌ firstImage) ((postWhisker-comp₌ f (g ◁ b) (comp-assoc h π g)) ⁻¹)
          normalizeRight : (outputRight ∙ (middleRight ∙ inputRight)) =₂
            post-square-cell f ρ (g ∘ s) (g ∘ π) h (post-square-cell g ρ s π h b)
          normalizeRight = comp₌-cong (id₌ outside)
            (comp₌-cong mergeImages (id₌ finalInput) ∙
            ((comp₌-assoc firstImage (middleRight ∙ lastImage) finalInput) ⁻¹ ∙
              comp₌-cong (id₌ firstImage) ((comp₌-assoc middleRight lastImage finalInput) ⁻¹))) ∙
            comp₌-assoc outside firstImage (middleRight ∙ (lastImage ∙ finalInput))
      in assembled ∙ (comp₌-cong normalizeRight (id₌ atSource)) ⁻¹
```

## Unit computations

Restricting a triangle along an identity functor agrees with the right
unitors, and postcomposing with an identity functor agrees with the left
unitors (Kelly's lemmas). The projected unit arguments below combine these
computations with three supplied triangles; they are used for the unit
laws of product functors and of first-factor substitution.

```agda
module _ {Γ : Context} where
  module _ {X : CAT Γ} where
    open Terms.InContext X using (Term)

    restrict-triangle-id : {K C : CAT Γ} (π : MAP K C)
      (z : Term K) (x : Term C) (b : (π ∘ z) =₁ x)
      → (comp-unitʳ x ∙ restrict-triangle π z b (id X)) =₂ (b ∙ (π ◁ comp-unitʳ z))
    restrict-triangle-id  π z x b =
      let A = comp-assoc (id X) z π
          normalize = comp-inv-right (π ◁ comp-unitʳ z) A ∙
            comp₌-cong (right-unitor-comp z π) (id₌ (A ⁻¹))
      in comp₌-cong (id₌ b) normalize ∙
        (comp₌-assoc b (comp-unitʳ (π ∘ z)) (A ⁻¹) ∙
        (comp₌-cong (preWhisker-id-One b) (id₌ (A ⁻¹)) ∙
          (comp₌-assoc (comp-unitʳ x) (b ▷ id X) (A ⁻¹)) ⁻¹))

  module _ {R X : CAT Γ} where
    open Terms.InContext X using (Term)

    post-square-cell-id : {K C : CAT Γ}
      (ρ : MAP R X) (x : Term C) (π : MAP K C) (h : MAP R K)
      (b : (π ∘ h) =₁ (x ∘ ρ))
      → ((comp-unitˡ x ▷ ρ) ∙ post-square-cell (id C) ρ x π h b) =₂
          (b ∙ (comp-unitˡ π ▷ h))
    post-square-cell-id ρ x π h b =
      let A = comp-assoc ρ x (id _)
          B = comp-assoc h π (id _)
          first = comp-inv-right (comp-unitˡ (x ∘ ρ)) A ∙
            comp₌-cong ((left-unitor-comp ρ x) ⁻¹) (id₌ (A ⁻¹))
      in comp₌-cong (id₌ b) (left-unitor-comp h π) ∙
        (comp₌-assoc b (comp-unitˡ (π ∘ h)) B ∙
        (comp₌-cong (postWhisker-id-One b) (id₌ B) ∙
        ((comp₌-assoc (comp-unitˡ (x ∘ ρ)) (id _ ◁ b) B) ⁻¹ ∙
        (comp₌-cong first (id₌ ((id _ ◁ b) ∙ B)) ∙
          (comp₌-assoc (comp-unitˡ x ▷ ρ) (A ⁻¹) ((id _ ◁ b) ∙ B)) ⁻¹))))

  module _ {X : CAT Γ} where
    open Terms.InContext X using (Term)

    post-triangle-id : {Y A : CAT Γ} (π : MAP Y A) (t : Term Y)
      {q : Term A} (b : (π ∘ t) =₁ q)
      → (comp-unitˡ q ∙ post-triangle (id A) π t b) =₂ (b ∙ (comp-unitˡ π ▷ t))
    post-triangle-id π t b = comp₌-cong (id₌ b) (left-unitor-comp t π) ∙
      (comp₌-assoc b (comp-unitˡ (π ∘ t)) (comp-assoc t π (id _)) ∙
      (comp₌-cong (postWhisker-id-One b) (id₌ (comp-assoc t π (id _))) ∙
        (comp₌-assoc (comp-unitˡ _) (id _ ◁ b) (comp-assoc t π (id _))) ⁻¹))
```

The projected-triangle calculation pastes three supplied triangles after
projecting a composite. It is pure vertical calculus.

```agda
  module _ {X : CAT Γ} where
    open Terms.InContext X using (Term)

    projected-triangles : {C : CAT Γ} {a b c c′ d y z : Term C}
      (frame : c =₁ z) (out : b =₁ c) (step : a =₁ b)
      (unit : y =₁ z) (middle : b =₁ y)
      (coordinate : d =₁ y) (transport : a =₁ d)
      (result-frame : c′ =₁ z) (result : d =₁ c′)
      (projected : a =₁ z)
      → projected =₂ ((frame ∙ out) ∙ step)
      → (frame ∙ out) =₂ (unit ∙ middle)
      → (middle ∙ step) =₂ (coordinate ∙ transport)
      → (unit ∙ coordinate) =₂ (result-frame ∙ result)
      → projected =₂ (result-frame ∙ (result ∙ transport))
    projected-triangles frame out step unit middle coordinate transport result-frame result
      projected project out-triangle step-triangle coordinate-unit =
      comp₌-assoc result-frame result transport ∙
        (comp₌-cong coordinate-unit (id₌ transport) ∙
        ((comp₌-assoc unit coordinate transport) ⁻¹ ∙
        (comp₌-cong (id₌ unit) step-triangle ∙
        (comp₌-assoc unit middle step ∙
        (comp₌-cong out-triangle (id₌ step) ∙ project)))))
```

The left unit argument identifies the projection of a composite `out ∙ step`
with the projection of the restricted unit route, when `step` is a
postcomposition with an endofunctor `J` identified with the identity by
`δ`. The right unit argument is dual, with `J` acting on the source.

```agda
  module _ {R X : CAT Γ} where
    open Terms.InContext X using (Term)

    left-unit-projection : {K C : CAT Γ}
      (ρ : MAP R X) (x : Term C) (π : MAP K C) (h h′ : MAP R K)
      (J : MAP K K) (δ : J =₁ (id K))
      (b : (π ∘ h) =₁ (x ∘ ρ))
      (b′ : (π ∘ h′) =₁ ((id C ∘ x) ∘ ρ))
      (bJ : (π ∘ J) =₁ (id C ∘ π))
      (out : h′ =₁ h) (step : (J ∘ h) =₁ h′)
      → (comp-unitʳ π ∙ (π ◁ δ)) =₂ (comp-unitˡ π ∙ bJ)
      → (b ∙ (π ◁ out)) =₂ ((comp-unitˡ x ▷ ρ) ∙ b′)
      → (b′ ∙ (π ◁ step)) =₂
          (post-square-cell (id C) ρ x π h b ∙ restrict-triangle π J bJ h)
      → (π ◁ (out ∙ step)) =₂ (π ◁ (comp-unitˡ h ∙ (δ ▷ h)))
    left-unit-projection ρ x π h h′ J δ b b′ bJ out step unit-triangle out-triangle step-triangle =
      let e = post-square-cell (id _) ρ x π h b
          left-normal = projected-triangles
            b (π ◁ out) (π ◁ step) (comp-unitˡ x ▷ ρ) b′
            e (restrict-triangle π J bJ h) b (comp-unitˡ π ▷ h) (b ∙ (π ◁ (out ∙ step)))
            (project-composite π out step b) out-triangle step-triangle
            (post-square-cell-id ρ x π h b)
          A = comp-assoc h (id _) π
          triangle-solved : (π ◁ comp-unitˡ h) =₂ ((comp-unitʳ π ▷ h) ∙ A ⁻¹)
          triangle-solved =
            (comp-inv-right (π ◁ comp-unitˡ h) A ∙
              comp₌-cong (triangle-whiskered h π) (id₌ (A ⁻¹))) ⁻¹
          pre-square = restrict-square-One π δ (comp-unitˡ π) bJ (comp-unitʳ π) h unit-triangle
          right-normal = comp₌-cong (id₌ b)
              (pre-square ∙ comp₌-cong triangle-solved (id₌ (π ◁ (δ ▷ h)))) ∙
            (comp₌-assoc b (π ◁ comp-unitˡ h) (π ◁ (δ ▷ h)) ∙
              project-composite π (comp-unitˡ h) (δ ▷ h) b)
      in cancel-left b (right-normal ⁻¹ ∙ left-normal)

  post-square-cell-right-unit : {R C D : CAT Γ}
    (ρ : MAP R C) (f : MAP C D) (J : MAP R R) (δ : J =₁ (id R))
    (bJ : (ρ ∘ J) =₁ (id C ∘ ρ))
    → (comp-unitʳ ρ ∙ (ρ ◁ δ)) =₂ (comp-unitˡ ρ ∙ bJ)
    → ((comp-unitʳ f ▷ ρ) ∙ post-square-cell f ρ (id C) ρ J bJ) =₂
        (comp-unitʳ (f ∘ ρ) ∙ ((f ∘ ρ) ◁ δ))
  post-square-cell-right-unit ρ f J δ bJ unit-triangle =
    let A = comp-assoc ρ (id _) f
        B = comp-assoc J ρ f
        C′ = comp-assoc (id _) ρ f
        q = (f ∘ ρ) ◁ δ
        first = comp-inv-right (f ◁ comp-unitˡ ρ) A ∙
          comp₌-cong (triangle-whiskered ρ f) (id₌ (A ⁻¹))
    in comp₌-cong ((right-unitor-comp ρ f) ⁻¹) (id₌ q) ∙
      ((comp₌-assoc (f ◁ comp-unitʳ ρ) C′ q) ⁻¹ ∙
      (comp₌-cong (id₌ (f ◁ comp-unitʳ ρ)) ((postWhisker-comp-One δ ρ f) ⁻¹) ∙
      (comp₌-assoc (f ◁ comp-unitʳ ρ) (f ◁ (ρ ◁ δ)) B ∙
      (comp₌-cong
        (postWhisker-comp₌ f (comp-unitʳ ρ) (ρ ◁ δ) ∙
          ((postWhisker f ◁ unit-triangle ⁻¹) ∙
            (postWhisker-comp₌ f (comp-unitˡ ρ) bJ) ⁻¹)) (id₌ B) ∙
      ((comp₌-assoc (f ◁ comp-unitˡ ρ) (f ◁ bJ) B) ⁻¹ ∙
      (comp₌-cong first (id₌ ((f ◁ bJ) ∙ B)) ∙
        (comp₌-assoc (comp-unitʳ f ▷ ρ) (A ⁻¹) ((f ◁ bJ) ∙ B)) ⁻¹))))))

  restrict-triangle-right-unit : {R K C : CAT Γ}
    (π : MAP K C) (h : MAP R K) (F : MAP R C) (b : (π ∘ h) =₁ F)
    (J : MAP R R) (δ : J =₁ (id R))
    → (b ∙ (π ◁ (comp-unitʳ h ∙ (h ◁ δ)))) =₂
        (comp-unitʳ F ∙ ((F ◁ δ) ∙ restrict-triangle π h b J))
  restrict-triangle-right-unit π h F b J δ =
    let A = comp-assoc (id _) h π
        solved = (comp-inv-right (π ◁ comp-unitʳ h) A ∙
          comp₌-cong (right-unitor-comp h π) (id₌ (A ⁻¹))) ⁻¹
        head = comp₌-assoc (comp-unitʳ F) (b ▷ id _) (A ⁻¹) ∙
          (comp₌-cong ((preWhisker-id-One b) ⁻¹) (id₌ (A ⁻¹)) ∙
          ((comp₌-assoc b (comp-unitʳ (π ∘ h)) (A ⁻¹)) ⁻¹ ∙
            comp₌-cong (id₌ b) solved))
    in comp₌-cong (id₌ (comp-unitʳ F)) (restrict-change-square-One π h F b δ) ∙
      (comp₌-assoc (comp-unitʳ F) ((b ▷ id _) ∙ A ⁻¹) (π ◁ (h ◁ δ)) ∙
      (comp₌-cong head (id₌ (π ◁ (h ◁ δ))) ∙
        project-composite π (comp-unitʳ h) (h ◁ δ) b))

  module _ {R X : CAT Γ} where
    open Terms.InContext X using (Term)

    right-unit-projection : {K C : CAT Γ}
      (ρ : MAP R X) (x : Term C) (π : MAP K C) (h h′ : MAP R K)
      (J : MAP R R) (δ : J =₁ (id R))
      (b : (π ∘ h) =₁ (x ∘ ρ))
      (b′ : (π ∘ h′) =₁ ((x ∘ id X) ∘ ρ))
      (bJ : (ρ ∘ J) =₁ (id X ∘ ρ))
      (out : h′ =₁ h) (step : (h ∘ J) =₁ h′)
      → (comp-unitʳ ρ ∙ (ρ ◁ δ)) =₂ (comp-unitˡ ρ ∙ bJ)
      → (b ∙ (π ◁ out)) =₂ ((comp-unitʳ x ▷ ρ) ∙ b′)
      → (b′ ∙ (π ◁ step)) =₂
          (post-square-cell x ρ (id X) ρ J bJ ∙ restrict-triangle π h b J)
      → (π ◁ (out ∙ step)) =₂ (π ◁ (comp-unitʳ h ∙ (h ◁ δ)))
    right-unit-projection ρ x π h h′ J δ b b′ bJ out step unit-triangle out-triangle step-triangle =
      let e = post-square-cell x ρ (id _) ρ J bJ
          left-normal = projected-triangles
            b (π ◁ out) (π ◁ step) (comp-unitʳ x ▷ ρ) b′
            e (restrict-triangle π h b J) (comp-unitʳ (x ∘ ρ)) ((x ∘ ρ) ◁ δ)
            (b ∙ (π ◁ (out ∙ step)))
            (project-composite π out step b) out-triangle step-triangle
            (post-square-cell-right-unit ρ x J δ bJ unit-triangle)
      in cancel-left b
        ((restrict-triangle-right-unit π h (x ∘ ρ) b J δ) ⁻¹ ∙ left-normal)
```

## An identification of an endofunctor with the identity

If `η : H = id` satisfies the unit triangle against a supplied `b : π ∘ H = π`,
then its postcompositions and restrictions satisfy the corresponding
triangles. (Formerly `eta-post-coordinate` and `eta-pre-coordinate`.)

```agda
module _ {Γ : Context} where
  module _ {X : CAT Γ} where
    open Terms.InContext X using (Term)

    identity-post-coordinate : {A B : CAT Γ} (π : Term A) (F : MAP A B)
      (H : Term X) (η : H =₁ (id X)) (b : (π ∘ H) =₁ π)
      → (comp-unitʳ π ∙ (π ◁ η)) =₂ b
      → (comp-unitʳ (F ∘ π) ∙ ((F ∘ π) ◁ η)) =₂ post-triangle F π H b
    identity-post-coordinate π F H η b triangle =
      comp₌-cong (postWhisker F ◁ triangle) (id₌ (comp-assoc H π F)) ∙
      (comp₌-cong ((postWhisker-comp₌ F (comp-unitʳ π) (π ◁ η)) ⁻¹)
          (id₌ (comp-assoc H π F)) ∙
      ((comp₌-assoc (F ◁ comp-unitʳ π) (F ◁ (π ◁ η)) (comp-assoc H π F)) ⁻¹ ∙
      (comp₌-cong (id₌ (F ◁ comp-unitʳ π)) (postWhisker-comp-One η π F) ∙
      (comp₌-assoc (F ◁ comp-unitʳ π) (comp-assoc (id _) π F) ((F ∘ π) ◁ η) ∙
        comp₌-cong (right-unitor-comp π F) (id₌ ((F ∘ π) ◁ η))))))

  module _ {R X : CAT Γ} where
    open Terms.InContext X using (Term)

    identity-pre-coordinate : {C : CAT Γ} (π : Term C) (s : MAP R X)
      (H : Term X) (η : H =₁ (id X)) (b : (π ∘ H) =₁ π)
      → (comp-unitʳ π ∙ (π ◁ η)) =₂ b
      → (π ◁ (comp-unitˡ s ∙ (η ▷ s))) =₂ restrict-triangle π H b s
    identity-pre-coordinate π s H η b triangle =
      let A = comp-assoc s (id _) π
          triangle-solved = (comp-inv-right (π ◁ comp-unitˡ s) A ∙
            comp₌-cong (triangle-whiskered s π) (id₌ (A ⁻¹))) ⁻¹
          square = restrict-square-One π η (id₌ π) b (comp-unitʳ π) s
            ((comp₌-unitˡ-One b) ⁻¹ ∙ triangle)
          tail = restrict-triangle π H b s
      in comp₌-unitˡ-One tail ∙
        (comp₌-cong (preWhisker-id₌ π s) (id₌ tail) ∙
        (square ∙
        (comp₌-cong triangle-solved (id₌ (π ◁ (η ▷ s))) ∙
          postWhisker-comp₌ π (comp-unitˡ s) (η ▷ s))))
```

## Identifications lying over identifications

A square `SquareCell₌ (π ◁ ε) α b b′` says that `ε` lies over `α` with
respect to the triangles `b` and `b′` (constant families of triangles for a
family `ε`, the triangles themselves for an individual identification).
Composites of identifications lying over `α₁` and `α₂` lie over `α₂ ∙ α₁`,
inverses lie over inverses, and an identity lies over an identity. These are
the operations used to recognize an identification into a product by its
projections, and identifications between functors over a base.

```agda
module _ {Γ : Context} where
  module _ {A X : CAT Γ} where
    open Terms.InContext X using (Term)
    open Terms.Equalities A using (_＝_)

    lies-over-comp : {K C : CAT Γ} (π : MAP K C)
      {h₀ h₁ h₂ : Term K} {z₀ z₁ z₂ : Term C}
      {b₀ : ((π ∘ h₀) ＝ z₀)} {b₁ : ((π ∘ h₁) ＝ z₁)} {b₂ : ((π ∘ h₂) ＝ z₂)}
      {ε₂ : h₁ ＝ h₂} {ε₁ : h₀ ＝ h₁}
      {α₂ : z₁ ＝ z₂} {α₁ : z₀ ＝ z₁}
      → SquareCell₌ (π ◁ ε₁) α₁ b₀ b₁
      → SquareCell₌ (π ◁ ε₂) α₂ b₁ b₂
      → SquareCell₌ (π ◁ (ε₂ ∙ ε₁)) (α₂ ∙ α₁) b₀ b₂
    lies-over-comp π {ε₂ = ε₂} {ε₁} {α₂} {α₁} first second =
      replace-edges₌ ((postWhisker-comp₌ π ε₂ ε₁) ⁻¹) (id₌ (α₂ ∙ α₁))
        (adjoin-square₌ first second)

    lies-over-inverse : {K C : CAT Γ} (π : MAP K C)
      {h h′ : Term K} {z z′ : Term C}
      {b : ((π ∘ h) ＝ z)} {b′ : ((π ∘ h′) ＝ z′)}
      {ε : h ＝ h′} {α : z ＝ z′}
      → SquareCell₌ (π ◁ ε) α b b′
      → SquareCell₌ (π ◁ ε ⁻¹) (α ⁻¹) b′ b
    lies-over-inverse π {b = b} {b′} {ε} {α} square =
      replace-edges₌ ((postWhisker-inverse π ε) ⁻¹) (id₌ (α ⁻¹))
        (transpose-square₌ (inverse-square₌ {t = b} {b = b′} {l = π ◁ ε} {r = α}
          (transpose-square₌ square)))
```

Lying over is invariant under a change of frame: if `ε` lies over `α` along
`π`, and `v : q = π`, then `ε` lies over `α` along `q`, with the triangles
precomposed by the restrictions of `v`. The required square of the two
projections of `ε` is the interchange law.

```agda
    lies-over-reframe : {K C : CAT Γ} {π q : MAP K C} (v : q ＝ π)
      {h h′ : Term K} {z z′ : Term C}
      {b : ((π ∘ h) ＝ z)} {b′ : ((π ∘ h′) ＝ z′)}
      {ε : h ＝ h′} {α : z ＝ z′}
      → SquareCell₌ (π ◁ ε) α b b′
      → SquareCell₌ (q ◁ ε) α (b ∙ (v ▷ h)) (b′ ∙ (v ▷ h′))
    lies-over-reframe {π = π} {q} v {ε = ε} {α} square =
      paste-square₌ {t = q ◁ ε} {m = π ◁ ε} {b = α} (interchange v ε) square

  module _ {A X : CAT Γ} where
    open Terms.InContext X using (Term)

    lies-over-id : {K C : CAT Γ} (π : MAP K C) {h : Term K} {z : Term C}
      (b : (π ∘ h) =₁ z)
      → SquareCell₌ (π ◁ const {P = A} (id₌ h)) (const (id₌ z)) (const b) (const b)
    lies-over-id  π {h} b =
      replace-edges₌
        ((const-cong {X = A} (postWhisker-id₌ π h) ∙ post-constant π (id₌ h)) ⁻¹)
        (id₌ (const (id₌ _)))
        (transpose-square₌ (identity-square₌ (const {P = A} b)))

  module _ {X : CAT Γ} where
    open Terms.InContext X using (Term)

    lies-over-id-One : {K C : CAT Γ} (π : MAP K C) {h : Term K} {z : Term C}
      (b : (π ∘ h) =₁ z)
      → SquareCell₌ (π ◁ id₌ h) (id₌ z) b b
    lies-over-id-One π {h} {z} b =
      replace-edges₌ ((postWhisker-id₌ π h) ⁻¹ ∙ const-One (id₌ (π ∘ h))) (const-One (id₌ z))
        (transpose-square₌ (identity-square₌ b))
```