open import Cat.Instances.Shape.Interval
open import Cat.Displayed.Section
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Func
import Cat.Reasoning

module Cat.Displayed.Instances.Factorisations where

open Displayed
open Functor
open _=>s_
open _=>_

module _ {o ℓ} (C : Precategory o ℓ) where
  open Cat.Reasoning C

The displayed category of factorisations🔗

Given a category $C,$ we can define a displayed category $C^{3} Arr (C)$ over the arrow category $Arr (C)$ where an object over $f : X \to Y$ consists of a factorisation $X f Y = X m I e Y$ of $f$ through some choice of object $M .$ This is akin to the non-displayed notion of factorisation, but without the reference to pre-existing classes $M$ and $E$ for $m$ and $e$ to belong to.

  record Splitting {X Y : ⌞ C ⌟} (f : Hom X Y) : Type (o ⊔ ℓ) where
    no-eta-equality
    field
      {mid}   : ⌞ C ⌟
      left    : Hom X mid
      right   : Hom mid Y
      factors : f ≡ right ∘ left

  {-# INLINE Splitting.constructor #-}

  open Splitting

A morphism between splittings lying over a square from $f$ to $g$ in the arrow category, depicted in blue in the diagram below, is a map $i : I \to I^{'}$ between the “middle” objects of the two factorisations making both the top and bottom rectangles commute.

  record
    Interpolant
      {X X' Y Y'} {f : Hom X Y} {g : Hom X' Y'}
      (sq : Homᵃ C f g) (s : Splitting f) (t : Splitting g)
      : Type ℓ where

    no-eta-equality
    private
      module s = Splitting s
      module t = Splitting t

    field
      map : Hom (s .mid) (t .mid)
      sq₀ : t.left ∘ sq .top ≡ map     ∘ s.left
      sq₁ : t.right ∘ map    ≡ sq .bot ∘ s.right

In the literature on factorisation systems, the total category of this displayed category is identified with the diagram category $C^{3}$ of composable triples¹ in $C,$ and its projection functor $C^{3} \to Arr (C)$ sends each triple to its composite. In a proof assistant, defining this as a displayed category is superior because it lets us define sections of the composition functor— which send each arrow to a factorisation— where the domain and codomain of a factored arrow are definitionally the ones we started with.

  {-# INLINE Interpolant.constructor #-}
  open Interpolant public
unquoteDecl H-Level-Interpolant = declare-record-hlevel 2 H-Level-Interpolant (quote Interpolant)

module _ {o ℓ} {C : Precategory o ℓ} where
  open Precategory C
  open Splitting

  Interpolant-pathp
    : ∀ {X X' Y Y'} {f : Hom X Y} {g : Hom X' Y'} {sq sq' : Homᵃ C f g} {p : sq ≡ sq'} {s : Splitting C f} {t : Splitting C g}
    → {f : Interpolant C sq s t} {g : Interpolant C sq' s t}
    → f .map ≡ g .map
    → PathP (λ i → Interpolant C (p i) s t) f g
  Interpolant-pathp p i .map = p i
  Interpolant-pathp {p = q} {s} {t} {f} {g} p i .sq₀ = is-prop→pathp (λ i → Hom-set _ _ (t .left ∘ q i .top) (p i ∘ s .left)) (f .sq₀) (g .sq₀) i
  Interpolant-pathp {p = q} {s} {t} {f} {g} p i .sq₁ = is-prop→pathp (λ i → Hom-set _ _ (t .right ∘ p i) (q i .bot ∘ s .right)) (f .sq₁) (g .sq₁) i

  instance
    Extensional-Interpolant
      : ∀ {X X' Y Y' ℓr} {f : Hom X Y} {g : Hom X' Y'} {sq : Homᵃ C f g} {s : Splitting C f} {t : Splitting C g}
      → ⦃ _ : Extensional (Hom (s .mid) (t .mid)) ℓr ⦄
      → Extensional (Interpolant C sq s t) ℓr
    Extensional-Interpolant = injection→extensional! Interpolant-pathp auto

module _ {o ℓ} (C : Precategory o ℓ) where
  open Cat.Reasoning C

  Factorisations' : Displayed (Arr C) _ _
  Factorisations' .Ob[_]  (_ , _ , f) = Splitting C f
  Factorisations' .Hom[_]     sq s s' = Interpolant C sq s s'

  Factorisations' .id' = record { sq₀ = id-comm ; sq₁ = id-comm }

  Factorisations' ._∘'_ f g = record where
    map = f .map ∘ g .map
    sq₀ = pulll (f .sq₀) ∙ extendr (g .sq₀)
    sq₁ = pulll (f .sq₁) ∙ extendr (g .sq₁)

The only interesting thing to note about the coherence data here is that we can reindex Interpolants over identifications between squares without disturbing the middle map.

  Factorisations' .Hom[_]-set f x y = hlevel 2

  Factorisations' .idr'   f     = Interpolant-pathp (idr _)
  Factorisations' .idl'   f     = Interpolant-pathp (idl _)
  Factorisations' .assoc' f g h = Interpolant-pathp (assoc _ _ _)

  Factorisations' .hom[_] p' f = record where
    map = f .map
    sq₀ = ap₂ _∘_ refl (sym (ap top p')) ∙ f .sq₀
    sq₁ = f .sq₁ ∙ ap₂ _∘_ (ap bot p') refl
  Factorisations' .coh[_] p' f = Interpolant-pathp refl

Functorial factorisations🔗

A (functorial) factorisation on $C$ is a section of Factorisations'. These naturally assemble into a category.

  Factorisation : Type _
  Factorisation = Section Factorisations'

  Factorisations : Precategory _ _
  Factorisations = Sections Factorisations'

We shall now identify some first properties of functorial factorisations.

module Factorisation {o ℓ} {C : Precategory o ℓ} (fac : Factorisation C) where
  open Cat.Reasoning C
  open Section fac
  private module Arr = Cat.Reasoning (Arr C)

  module _ {X Y : ⌞ C ⌟} (f : Hom X Y) where
    open Splitting (Section.S₀ fac (X , Y , f))
      renaming (mid to Mid₀ ; left to λ→ ; right to ρ→)
      public

  module _ {u v w x : ⌞ C ⌟} {f : Hom u v} {g : Hom w x} (sq : Homᵃ C f g) where
    open Interpolant (Section.S₁ fac sq) using (map) public

Because the morphism-assignment of sections has a pretty dependent type, we can not immediately reuse the functor reasoning combinators for functorial factorisations.

However, we can define a functor that assigns each arrow to its midpoint and re-use the combinators for that functor.

  Mid : Functor (Arr C) C
  Mid = record where
    F₀ x = Mid₀ (x .snd .snd)
    F₁ f = S₁ f .map
    F-id    = apd (λ i → map) S-id
    F-∘ f g = apd (λ i → map) (S-∘ _ _)

  module Mid = Func Mid
  open Mid using (elim ; expand ; weave ; collapse) renaming (⟨_⟩ to adjust) public

Given a functorial factorisation, we can define two endofunctors on $Arr (C),$ referred to simply as its left and right parts, which send a morphism $X f Y$ to $L (f) = X m I (f)$ and $R (f) = I (f) o Y,$ respectively, while sending a square to either the top or bottom rectangles in the definition of Interpolant.

If $F$ is a functorial factorisation on $C,$ splitting an $X f Y$ into $X λ M ρ Y$ the left factor functor on $Arr (C)$ is $L (f) = X λ M .$ This is naturally made into a copointed endofunctor, with the counit assigning to each arrow $X f Y$ the square

If $F$ is a functorial factorisation on $C,$ splitting an $X f Y$ into $X λ M ρ Y$ the right factor functor on $Arr (C)$ is $R (f) = M ρ Y .$ This is naturally made into a pointed endofunctor, with the unit assigning to each arrow $X f Y$ the square

  L : Functor (Arr C) (Arr C)
  L .F₀ (X , Y , f) = X , Mid₀ f , λ→ f
  L .F₁ {X , Z , f} {X' , Z' , f'} sq = record
    { top = sq .top
    ; bot = S₁ sq .map
    ; com = S₁ sq .sq₀
    }
  L .F-id    = ext (refl ,ₚ Mid.elim refl)
  L .F-∘ f g = ext (refl ,ₚ Mid.expand refl)

  R : Functor (Arr C) (Arr C)
  R .F₀ (X , Y , f) = Mid₀ f , Y , ρ→ f
  R .F₁ {X , Z , f} {X' , Z' , f'} sq = record
    { top = S₁ sq .map
    ; bot = sq .bot
    ; com = S₁ sq .sq₁
    }
  R .F-id    = ext (Mid.elim refl   ,ₚ refl)
  R .F-∘ f g = ext (Mid.expand refl ,ₚ refl)

  open Functor L renaming (F₁ to L₁) using () public
  open Functor R renaming (F₁ to R₁) using () public

These endofunctors are naturally (co)pointed, meaning that the left (resp. right) functor admits a natural transformation to (resp. from) the identity on $Arr (C) .$ These transformations send a morphism to a triangle consisting of the complementary part of the factorisation.

  L-ε : L => Id
  L-ε .η (X , Y , f) = record
    { top = id
    ; bot = ρ→ f
    ; com = elimr refl ∙ factors f
    }
  L-ε .is-natural x y f = ext (id-comm-sym ,ₚ S₁ f .sq₁)

  R-η : Id => R
  R-η .η (X , Y , f) = record
    { top = λ→ f
    ; bot = id
    ; com = sym (factors f) ∙ introl refl
    }
  R-η .is-natural x y f = ext (S₁ f .sq₀ ,ₚ id-comm-sym)

-- This is an ugly hack to pretend that morphisms in Factorisations have
-- record fields themselves. Note that we have to choose different names
-- to not clash with those from _=>s_, and that these can not be
-- overloaded.

module
  _ {o ℓ} {C : Precategory o ℓ} {X Y : ⌞ Factorisation C ⌟}
    (f : Factorisations C .Precategory.Hom X Y)
  where
  open Cat.Reasoning C

  private
    module X = Factorisation X
    module Y = Factorisation Y

    record Hack : Type (o ⊔ ℓ) where
      field
        mapᶠᶠ : ∀ {x y} (g : Hom x y) → Hom (X.Mid₀ g) (Y.Mid₀ g)

        sq₀ᶠᶠ : ∀ {x y} (g : Hom x y) → Y.λ→ g ≡ mapᶠᶠ g ∘ X.λ→ g
        sq₁ᶠᶠ : ∀ {x y} (g : Hom x y) → Y.ρ→ g ∘ mapᶠᶠ g ≡ X.ρ→ g

        comᶠᶠ
          : ∀ {w x y z} {g : Hom w x} {h : Hom y z} (i : Homᵃ C g h)
          → mapᶠᶠ h ∘ X .Section.S₁ i .map ≡ Y .Section.S₁ i .map ∘ mapᶠᶠ g

    hack : Hack
    hack = record
      { mapᶠᶠ = λ g → f .map (_ , _ , g) .map
      ; sq₀ᶠᶠ = λ g → intror refl ∙ f .map (_ , _ , g) .sq₀
      ; sq₁ᶠᶠ = λ g → f .map (_ , _ , g) .sq₁ ∙ eliml refl
      ; comᶠᶠ = λ i → apd (λ i → map) (f .com _ _ i)
      }

  open Hack hack public

Note that here $3$ denotes the ordinal ${0 \leq 1 \leq 2},$ and not the set with three elements.↩︎