SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence

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

# Whiskering by an equivalence

Whiskering by an equivalence induces equivalences between identification
animae. First, composing with a fixed identification gives an equivalence.
Squares between functors then handle changes of endpoints, identities and
composites. The two main proofs use two-out-of-six and the fixed-input forms
of interchange.

```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.WhiskeringEquivalence 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
open Constructions
open import SCT.VolumeI.Chapter01.Section02.Coherence
  using (id₌; comp-unitˡ; comp-unitʳ; comp-assoc; 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.Squares
open import SCT.VolumeI.Chapter01.Section03.Equivalences
open import SCT.VolumeI.Chapter01.Section03.Factorizations
  using (Factorization; factor-through-equiv)
```

## Composing with a fixed identification

Postcomposition with `β : g =₁ h` and precomposition with `β : f =₁ g` are
functors between identification animae. Evaluated at a family they give
the expected vertical composites with constant families. Their inverses
compose with `β ⁻¹`; the inverse laws are the family inverse reductions,
after identifying the constant family of `β ⁻¹` with the inverse of the
constant family of `β`.

```agda
module _ {Γ : Context} where
  postcomp₌ : {C D : CAT Γ} {f g h : MAP C D}
    → g =₁ h → MAP (Equal f g) (Equal f h)
  postcomp₌ β = const β ∙ id _

  precomp₌ : {C D : CAT Γ} {f g h : MAP C D}
    → f =₁ g → MAP (Equal g h) (Equal f h)
  precomp₌ β = id _ ∙ const β

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

    postcomp₌-evaluate : {C D : CAT Γ} {f g h : MAP C D}
      (β : g =₁ h) (α : f ＝ g)
      → (postcomp₌ β ∘ α) =₁ (const β ∙ α)
    postcomp₌-evaluate β α = comp₌-evaluate-One (const β) (id _) α
      (const-pre β α) (comp-unitˡ α)

    precomp₌-evaluate : {C D : CAT Γ} {f g h : MAP C D}
      (β : f =₁ g) (α : g ＝ h)
      → (precomp₌ β ∘ α) =₁ (α ∙ const β)
    precomp₌-evaluate β α = comp₌-evaluate-One (id _) (const β) α
      (comp-unitˡ α) (const-pre β α)

  postcomp₌-isEquiv : {C D : CAT Γ} {f g h : MAP C D}
    (β : g =₁ h) → IsEquiv (postcomp₌ {f = f} β)
  postcomp₌-isEquiv {f = f} β =
    let back : (postcomp₌ (β ⁻¹) ∘ postcomp₌ β) =₁ id _
        back = inv-comp-left (const β) (id _) ∙
          (comp₌-cong (const-inv β) (id₌ (postcomp₌ β)) ∙
            postcomp₌-evaluate (β ⁻¹) (postcomp₌ β))
        forth : (postcomp₌ β ∘ postcomp₌ (β ⁻¹)) =₁ id _
        forth = comp-inv-left (const β) (id _) ∙
          (comp₌-cong (id₌ (const β)) (comp₌-cong (const-inv β) (id₌ (id _))) ∙
            postcomp₌-evaluate β (postcomp₌ (β ⁻¹)))
    in record
      { inverse = postcomp₌ (β ⁻¹)
      ; left-inverse-law = back ⁻¹
      ; right-inverse-law = forth ⁻¹ }

  precomp₌-isEquiv : {C D : CAT Γ} {f g h : MAP C D}
    (β : f =₁ g) → IsEquiv (precomp₌ {h = h} β)
  precomp₌-isEquiv {h = h} β =
    let back : (precomp₌ (β ⁻¹) ∘ precomp₌ β) =₁ id _
        back = comp-inv-right (id _) (const β) ∙
          (comp₌-cong (id₌ (precomp₌ β)) (const-inv β) ∙
            precomp₌-evaluate (β ⁻¹) (precomp₌ β))
        forth : (precomp₌ β ∘ precomp₌ (β ⁻¹)) =₁ id _
        forth = inv-comp-right (id _) (const β) ∙
          (comp₌-cong (comp₌-cong (id₌ (id _)) (const-inv β)) (id₌ (const β)) ∙
            precomp₌-evaluate β (precomp₌ (β ⁻¹)))
    in record
      { inverse = precomp₌ (β ⁻¹)
      ; left-inverse-law = back ⁻¹
      ; right-inverse-law = forth ⁻¹ }
```

## Changing endpoints through a square

Let `u : MAP X (f ＝ g)` and `v : MAP X (f′ ＝ g′)` be families, and let
`α : f =₁ f′` and `β : g =₁ g′` change their endpoints. A commuting square of
identification families with top `u`, bottom `v` and prescribed constant
sides `const α` and `const β` gives a square between functors from `v` to
`postcomp₌ β`: its source map is `u`, its target map is `precomp₌ α`, and
the evaluation laws convert the family square into its cell. Postcomposition
and precomposition are equivalences, so the square results of Equivalences
transfer the equivalence property between `u` and `v` in both directions.

```agda
module _ {Γ : Context} where
  endpoint-square : {X C D : CAT Γ} {f g f′ g′ : MAP C D}
    (u : MAP X (Equal f g)) (v : MAP X (Equal f′ g′))
    (α : f =₁ f′) (β : g =₁ g′)
    → SquareCell₌ u v (const α) (const β)
    → Square v (postcomp₌ β)
  endpoint-square u v α β κ = square u (precomp₌ α)
    ((precomp₌-evaluate α v) ⁻¹ ∙ (κ ∙ postcomp₌-evaluate β u))

  endpoint-change-reflects-isEquiv : {X C D : CAT Γ} {f g f′ g′ : MAP C D}
    (u : MAP X (Equal f g)) (v : MAP X (Equal f′ g′))
    (α : f =₁ f′) (β : g =₁ g′)
    → SquareCell₌ u v (const α) (const β) → IsEquiv v → IsEquiv u
  endpoint-change-reflects-isEquiv u v α β κ =
    square-source-map-isEquiv (endpoint-square u v α β κ)
      (postcomp₌-isEquiv β) (precomp₌-isEquiv α)

  endpoint-change-preserves-isEquiv : {X C D : CAT Γ} {f g f′ g′ : MAP C D}
    (u : MAP X (Equal f g)) (v : MAP X (Equal f′ g′))
    (α : f =₁ f′) (β : g =₁ g′)
    → SquareCell₌ u v (const α) (const β) → IsEquiv u → IsEquiv v
  endpoint-change-preserves-isEquiv u v α β κ =
    square-functor-isEquiv (endpoint-square u v α β κ)
      (postcomp₌-isEquiv β) (precomp₌-isEquiv α)
```

## Identity functors and identified functors

Whiskering by an identity functor is identified with the identity of the
identification anima after changing endpoints by the unitors. The required
family square is the whiskering law for identity functors at the universal
family `id (f ＝ g)`. Whiskering by identified functors `F` and `G` is
related by changing endpoints along the whiskered identification. The family
square is fixed-input interchange at the universal family.

```agda
module _ {Γ : Context} where
  postWhisker-id-isEquiv : {C D : CAT Γ} (f g : MAP C D)
    → IsEquiv (postWhisker {f = f} {g} (id D))
  postWhisker-id-isEquiv {D = D} f g =
    endpoint-change-reflects-isEquiv (postWhisker (id D)) (id (Equal f g))
      (comp-unitˡ f) (comp-unitˡ g)
      (postWhisker-id (id (Equal f g)) ∙
        (comp₌-cong (id₌ _) (comp-unitʳ (postWhisker (id D)))) ⁻¹)
      (id-isEquiv (Equal f g))

  preWhisker-id-isEquiv : {C D : CAT Γ} (f g : MAP C D)
    → IsEquiv (preWhisker {f = f} {g} (id C))
  preWhisker-id-isEquiv {C} f g =
    endpoint-change-reflects-isEquiv (preWhisker (id C)) (id (Equal f g))
      (comp-unitʳ f) (comp-unitʳ g)
      (preWhisker-id (id (Equal f g)) ∙
        (comp₌-cong (id₌ _) (comp-unitʳ (preWhisker (id C)))) ⁻¹)
      (id-isEquiv (Equal f g))

  postWhisker-transport-isEquiv : {B C D : CAT Γ} {F G : MAP C D}
    (τ : F =₁ G) (f g : MAP B C)
    → IsEquiv (postWhisker {f = f} {g} G) → IsEquiv (postWhisker {f = f} {g} F)
  postWhisker-transport-isEquiv {F = F} {G} τ f g =
    endpoint-change-reflects-isEquiv (postWhisker F) (postWhisker G)
      (τ ▷ f) (τ ▷ g)
      (comp₌-cong (comp-unitʳ (postWhisker G)) (id₌ _) ∙
        (interchange-fixedOuter τ (id (Equal f g)) ∙
          (comp₌-cong (id₌ _) (comp-unitʳ (postWhisker F))) ⁻¹))

  preWhisker-transport-isEquiv : {B C D : CAT Γ} {h k : MAP B C}
    (σ : h =₁ k) (f g : MAP C D)
    → IsEquiv (preWhisker {f = f} {g} k) → IsEquiv (preWhisker {f = f} {g} h)
  preWhisker-transport-isEquiv {h = h} {k} σ f g =
    endpoint-change-reflects-isEquiv (preWhisker h) (preWhisker k)
      (f ◁ σ) (g ◁ σ)
      (comp₌-cong (comp-unitʳ (preWhisker k)) (id₌ _) ∙
        ((interchange-fixedInner (id (Equal f g)) σ) ⁻¹ ∙
          (comp₌-cong (id₌ _) (comp-unitʳ (preWhisker h))) ⁻¹))
```

## Whiskering by composites and equivalences

The composition laws transfer equivalence between whiskering by a composite
and composing the whiskering functors, keeping both endpoint associators.
For a chosen inverse `G` of `F`, the two successive composites in the
alternating sequence of whiskering by `F`, `G`, `F` are equivalences.
Two-out-of-six proves that whiskering by `F` is an equivalence, without
constructing a separate corrected inverse.

```agda
module _ {Γ : Context} where
  postWhisker-composite-isEquiv : {B C D E : CAT Γ} (f g : MAP B C) (u : MAP C D) (v : MAP D E)
    → IsEquiv (postWhisker {f = f} {g} (v ∘ u))
    → IsEquiv (postWhisker v ∘ postWhisker {f = f} {g} u)
  postWhisker-composite-isEquiv f g u v =
    endpoint-change-preserves-isEquiv (postWhisker (v ∘ u))
      (postWhisker v ∘ postWhisker u) (comp-assoc f u v) (comp-assoc g u v)
      (comp₌-cong (postWhisker v ◁ comp-unitʳ (postWhisker u)) (id₌ _) ∙
        (postWhisker-comp (id (Equal f g)) u v ∙
          (comp₌-cong (id₌ _) (comp-unitʳ (postWhisker (v ∘ u)))) ⁻¹))

  preWhisker-composite-isEquiv : {A B C D : CAT Γ} (f g : MAP C D) (k : MAP B C) (l : MAP A B)
    → IsEquiv (preWhisker {f = f} {g} (k ∘ l))
    → IsEquiv (preWhisker l ∘ preWhisker {f = f} {g} k)
  preWhisker-composite-isEquiv f g k l =
    endpoint-change-reflects-isEquiv (preWhisker l ∘ preWhisker k)
      (preWhisker (k ∘ l)) (comp-assoc l k f) (comp-assoc l k g)
      (comp₌-cong (comp-unitʳ (preWhisker (k ∘ l))) (id₌ _) ∙
        (preWhisker-comp (id (Equal f g)) k l ∙
          (comp₌-cong (id₌ _) (preWhisker l ◁ comp-unitʳ (preWhisker k))) ⁻¹))

  postWhisker-isEquiv : {B C D : CAT Γ} (F : MAP C D) → IsEquiv F
    → (f g : MAP B C) → IsEquiv (postWhisker {f = f} {g} F)
  postWhisker-isEquiv F e f g =
    let G = IsEquiv.inverse e
        first = postWhisker-composite-isEquiv f g F G
          (postWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) f g
            (postWhisker-id-isEquiv f g))
        second = postWhisker-composite-isEquiv (F ∘ f) (F ∘ g) G F
          (postWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) (F ∘ f) (F ∘ g)
            (postWhisker-id-isEquiv (F ∘ f) (F ∘ g)))
    in TwoOutOfSix.first (two-out-of-six (postWhisker F) (postWhisker G)
         (postWhisker F) first second)

  preWhisker-isEquiv : {C D E : CAT Γ} (F : MAP C D) → IsEquiv F
    → (f g : MAP D E) → IsEquiv (preWhisker {f = f} {g} F)
  preWhisker-isEquiv F e f g =
    let G = IsEquiv.inverse e
        first = preWhisker-composite-isEquiv f g F G
          (preWhisker-transport-isEquiv ((IsEquiv.right-inverse-law e) ⁻¹) f g
            (preWhisker-id-isEquiv f g))
        second = preWhisker-composite-isEquiv (f ∘ F) (g ∘ F) G F
          (preWhisker-transport-isEquiv ((IsEquiv.left-inverse-law e) ⁻¹) (f ∘ F) (g ∘ F)
            (preWhisker-id-isEquiv (f ∘ F) (g ∘ F)))
    in TwoOutOfSix.first (two-out-of-six (preWhisker F) (preWhisker G)
         (preWhisker F) first second)
```

## Factoring through whiskering

Whiskering by an equivalence is an equivalence, so every family of
identifications between the whiskered functors factors through it, with a
specified triangle. The family parameter `A` is arbitrary. Applying the
construction again to identification animae factors families of higher
identifications; the suffix ₂ marks these second-level inputs.

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

    factor-through-postWhisker : {B C D : CAT Γ} (F : MAP C D) → IsEquiv F
      → {f g : MAP B C} → (α : (F ∘ f) ＝ (F ∘ g))
      → Factorization (postWhisker F) α
    factor-through-postWhisker F e {f} {g} α =
      factor-through-equiv (postWhisker-isEquiv F e f g) α

    factor-through-preWhisker : {C D E : CAT Γ} (F : MAP C D) → IsEquiv F
      → {f g : MAP D E} → (α : (f ∘ F) ＝ (g ∘ F))
      → Factorization (preWhisker F) α
    factor-through-preWhisker F e {f} {g} α =
      factor-through-equiv (preWhisker-isEquiv F e f g) α

  factor-through-postWhisker₂ : {A A′ B C D : CAT Γ} (F : MAP C D) → IsEquiv F
    → {f g : MAP B C} (α β : MAP A (Equal f g))
    → (p : MAP A′ (Equal (F ◁ α) (F ◁ β)))
    → Factorization (postWhisker (postWhisker F)) p
  factor-through-postWhisker₂ F e {f} {g} α β p =
    factor-through-postWhisker (postWhisker F) (postWhisker-isEquiv F e f g) p

  factor-through-preWhisker₂ : {A A′ C D E : CAT Γ} (F : MAP C D) → IsEquiv F
    → {f g : MAP D E} (α β : MAP A (Equal f g))
    → (p : MAP A′ (Equal (α ▷ F) (β ▷ F)))
    → Factorization (postWhisker (preWhisker F)) p
  factor-through-preWhisker₂ F e {f} {g} α β p =
    factor-through-postWhisker (preWhisker F) (preWhisker-isEquiv F e f g) p
```

## Contractible codomains

Postwhiskering with the terminal equivalence identifies the full
identification anima with its contractible terminal target.

```agda
module _ {Γ : Context} where
  contractible-identifications : {C X : CAT Γ} → IsContractible C
    → (f g : MAP X C) → IsContractible (Equal f g)
  contractible-identifications {C} e f g =
    contractible-source (postWhisker (terminate C))
      (postWhisker-isEquiv (terminate C) e f g)
      (terminal-identifications-isEquiv (terminate C ∘ f) (terminate C ∘ g))
```