Other Agda modules in this section (31)
# Factorizations and extensions
A factorization of `d : X → D` through `f : C → D` solves for a factor
functor `X → C` together with a specified triangle. It is a view of the
relative language: a functor over `D` from the category `X` with structural
functor `d` to the category `C` with structural functor `f`. Identity,
composition, inversion, uniqueness and mutual factorizations are therefore
the corresponding operations of RelativeFunctors, applied to these objects.
This file adds the constructions that are naturally phrased as solving for
a factor: changing the factored functor, restricting it, factoring through
an equivalence, and factorizations supplied by commuting squares.
Extensions are the dual view, using categories under a base. Their triangle
has the opposite orientation from the under-base cell.
```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section03.Factorizations where
open import SCT.VolumeI.Chapter01.Section01.Vocabulary hiding (_＝_)
import SCT.VolumeI.Chapter01.Section01.Terms as Terms
open Terms using (Equal)
open import SCT.VolumeI.Chapter01.Section02.Coherence
using (comp-unitˡ; comp-unitʳ; comp-assoc; module Composition)
open import SCT.VolumeI.Chapter01.Section03.RelativeFunctors
open import SCT.VolumeI.Chapter01.Section03.Equivalences using (ReflectsIdentifications)
open Operations
open Composition
```
## Factorizations as functors over a base
`factor` and `triangle` are the two components of the view. The triangle
is the cell of the functor over the base, with the same orientation as the
original factorization record: `f ∘ factor l =₁ d`.
```agda
module _ {Γ : Context} where
module _ {C D X : CAT Γ} where
open Terms.InContext X using (Term)
Factorization : (f : MAP C D) (d : Term D) → Set m
Factorization f d = FunctorOverBase (category-over X d) (category-over C f)
factor : {f : MAP C D} {d : Term D} → Factorization f d → Term C
factor l = FunctorOverBase.functor l
triangle : {f : MAP C D} {d : Term D}
→ (l : Factorization f d) → (f ∘ factor l) =₁ d
triangle l = FunctorOverBase.cell l
```
## Changing and restricting the factored functor
An identification `d =₁ d′` changes the factored functor. Precomposition
with `p : Y → X` restricts a factorization of `d` to one of `d ∘ p`.
```agda
module _ {C D X : CAT Γ} where
open Terms.InContext X using (Term)
factorization-retarget : {f : MAP C D} {d d′ : Term D}
→ d =₁ d′ → Factorization f d → Factorization f d′
factorization-retarget α l = functor-over (factor l) (α ∙ triangle l)
factorization-restrict : {Y : CAT Γ} {f : MAP C D} {d : Term D}
→ Factorization f d → (p : MAP Y X) → Factorization f (d ∘ p)
factorization-restrict {f = f} l p = functor-over (factor l ∘ p)
((triangle l ▷ p) ∙ (comp-assoc p (factor l) f) ⁻¹)
```
## Factorizations from commuting squares
A commuting square `k ∘ m =₁ m′ ∘ k′` makes `k′` a factor of `k ∘ m`
through `m′`. Composing along `k`, a factorization of `d` through `m` then
gives a factorization of `k ∘ d` through `m′`. This is `comp-over-map` for
the square, viewed as a functor over `k`.
```agda
square-factorization : {C C′ D E : CAT Γ} {k : MAP D E} {m : MAP C D}
{m′ : MAP C′ E} {k′ : MAP C C′}
→ (k ∘ m) =₁ (m′ ∘ k′) → Factorization m′ (k ∘ m)
square-factorization {k′ = k′} σ = functor-over k′ (σ ⁻¹)
module _ {C C′ D E X : CAT Γ} where
open Terms.InContext X using (Term)
factorization-along-square : {k : MAP D E} {m : MAP C D}
{m′ : MAP C′ E} {k′ : MAP C C′} {d : Term D}
→ (k ∘ m) =₁ (m′ ∘ k′) → Factorization m d → Factorization m′ (k ∘ d)
factorization-along-square {k = k} {m} σ F =
comp-over-map k {Y = category-over C m} (square-factorization σ) F
```
## Factoring through an equivalence
The chosen inverse of an equivalence `f` gives a factorization of any `d`
through `f`. If `f ∘ u =₁ g ∘ v` with `u` an equivalence, then `f` factors
through `g` via `v` and the chosen inverse of `u`.
```agda
module _ {C D X : CAT Γ} where
open Terms.InContext X using (Term)
factor-through-equiv : {f : MAP C D} (e : IsEquiv f)
(d : Term D) → Factorization f d
factor-through-equiv {f = f} e d = functor-over (IsEquiv.inverse e ∘ d)
(comp-unitˡ d ∙
(((IsEquiv.right-inverse-law e) ⁻¹ ▷ d) ∙ (comp-assoc d (IsEquiv.inverse e) f) ⁻¹))
module _ {X : CAT Γ} where
open Terms.InContext X using (Term)
factorization-from-equivalent-source : {A B Z : CAT Γ}
(f : MAP A Z) (g : MAP B Z) (u : MAP X A) (v : MAP X B)
→ IsEquiv u → (f ∘ u) =₁ (g ∘ v) → Factorization g f
factorization-from-equivalent-source f g u v eu β = functor-over (v ∘ IsEquiv.inverse eu)
(comp-unitʳ f ∙
((f ◁ (IsEquiv.right-inverse-law eu) ⁻¹) ∙
(comp-assoc (IsEquiv.inverse eu) u f ∙
((β ⁻¹ ▷ IsEquiv.inverse eu) ∙ (comp-assoc (IsEquiv.inverse eu) v g) ⁻¹))))
```
## Recognizing an equivalence
If every functor into the target factors through `f`, and postcomposition
with `f` reflects identifications at every testing category, then `f` is
an equivalence. Factor the identity of the target to choose the inverse;
reflection at the source gives its other inverse law. This is the criterion
of `prop:equivalences_as_naive_bijections`, without a separate data record.
```agda
factor-and-reflection-isEquiv : {C D : CAT Γ} (f : MAP C D)
→ ((T : CAT Γ) → ReflectsIdentifications f T)
→ ({T : CAT Γ} (d : MAP T D) → Factorization f d)
→ IsEquiv f
factor-and-reflection-isEquiv {C} {D} f reflect factors = record
{ inverse = g
; left-inverse-law = (reflect C (g ∘ f) (id C) image) ⁻¹
; right-inverse-law = β ⁻¹ }
where
chosen : Factorization f (id D)
chosen = factors (id D)
g : MAP D C
g = factor chosen
β : (f ∘ g) =₁ id D
β = triangle chosen
image : (f ∘ (g ∘ f)) =₁ (f ∘ id C)
image = (comp-unitʳ f) ⁻¹ ∙
(comp-unitˡ f ∙ ((β ▷ f) ∙ (comp-assoc f g f) ⁻¹))
```
## Extensions
An extension of `d : C → D` along `l : C → T` is a functor `T → D` with a
specified identification of its restriction along `l` with `d`. It is a
functor under `C` from `T`, with structural functor `l`, to `D`, with
structural functor `d`. The under-base cell `d =₁ extension ∘ l` is the
inverse of the triangle of the original extension record; `extension-triangle`
recovers that orientation. Identity, composition, uniqueness and mutual
extensions are `id-under`, `comp-under`, `functor-under-unique` and
`mutual-under-isEquiv`. Changing the extended functor composes the cell with
the inverse of the given identification.
```agda
Extension : {C D T : CAT Γ} (l : MAP C T) (d : MAP C D) → Set m
Extension {D = D} {T} l d = FunctorUnderBase (category-under T l) (category-under D d)
extension : {C D T : CAT Γ} {l : MAP C T} {d : MAP C D} → Extension l d → MAP T D
extension E = FunctorUnderBase.functor E
extension-triangle : {C D T : CAT Γ} {l : MAP C T} {d : MAP C D}
→ (E : Extension l d) → (extension E ∘ l) =₁ d
extension-triangle E = (FunctorUnderBase.cell E) ⁻¹
extension-retarget : {C D T : CAT Γ} {l : MAP C T} {d d′ : MAP C D}
→ d =₁ d′ → Extension l d → Extension l d′
extension-retarget α E = functor-under (extension E) (FunctorUnderBase.cell E ∙ α ⁻¹)
```