open import Cat.Morphism.Factorisation.Orthogonal
open import Cat.Functor.Adjoint.Reflective
open import Cat.Functor.WideSubcategory
open import Cat.Functor.Conservative
open import Cat.Direct.Generalized
open import Cat.Functor.Properties
open import Cat.Functor.Adjoint
open import Cat.Morphism.Class
open import Cat.Prelude

open import Data.Wellfounded.Properties
open import Data.Nat.Order
open import Data.Nat.Base

import Cat.Functor.Reasoning.FullyFaithful
import Cat.Functor.Reasoning
import Cat.Reasoning

module Cat.Reedy.Generalized where

module _ {o ℓ} (A : Precategory o ℓ) where
  private module A = Cat.Reasoning A

Generalized Reedy categories🔗

A generalized Reedy structure on a precategory $A$ consists of:

two classes of morphisms $A^{-}, A^{+} \subseteq A,$ and
a function $dim : A_{0} \to N$

  record is-generalized-reedy
    {ℓ⁻ ℓ⁺} (Neg : Arrows A ℓ⁻) (Pos : Arrows A ℓ⁺)
    (dim : A.Ob → Nat)
    : Type (o ⊔ ℓ ⊔ ℓ⁺ ⊔ ℓ⁻) where

subject to the following conditions:

The pair $(A^{-}, A^{+})$ forms an orthogonal factorisation system. In particular, this means that both $A^{-}$ and $A^{+}$ contain all isomorphism of $A$ and are closed under composition.

    field
      neg-pos-ofs : is-ofs A Neg Pos

    open is-ofs neg-pos-ofs renaming
      ( is-iso→in-L to is-iso→neg
      ; is-iso→in-R to is-iso→pos
      ; L-is-stable to neg-∘
      ; R-is-stable to pos-∘
      ; L-subcat to Neg-subcat
      ; R-subcat to Pos-subcat
      )
      public

If $f : A (x, y)$ is invertible, then $dim (x) = dim (y) .$
If $f : A^{-} (x, y)$ is non-invertible then $dim (x) > dim (y) .$
If $f : A^{+} (x, y)$ is non-invertible then $dim (x) < dim (y) .$

    field
      dim-iso : ∀ {x y} {f : A.Hom x y} → A.is-invertible f → dim x ≡ dim y
      dim-neg : ∀ {x y} {f : A.Hom x y} → f ∈ Neg → ¬ (A.is-invertible f) → dim x > dim y
      dim-pos : ∀ {x y} {f : A.Hom x y} → f ∈ Pos → ¬ (A.is-invertible f) → dim x < dim y

If $f : A (x, y)$ is in $A^{-} \cap A^{+},$ then $f$ must be invertible¹.

    field
      neg+pos→invertible
        : ∀ {x y} {f : A.Hom x y}
        → f ∈ Neg
        → f ∈ Pos
        → A.is-invertible f

Finally, we require that for every $f : y ≅ y$ and $p : A^{-} (x, y),$ if $f \circ p = p$ then $p = id .$ In other words, the stabilizer subgroup of $Aut (y)$ relative to $p : A^{-} (x, y)$ is trivial.

    field
      neg-trivial-stabilizer
        : ∀ {x y} {f : A.Hom y y} {p : A.Hom x y}
        → A.is-invertible f
        → p ∈ Neg
        → f A.∘ p ≡ p
        → f ≡ A.id

The purpose of this final axiom is to ensure that isomorphisms in $A$ view morphisms in $A^{-}$ as epimorphisms.

    iso-neg-epic
      : ∀ {x y z} {f₁ f₂ : A.Hom y z} {p : A.Hom x y}
      → A.is-invertible f₁
      → A.is-invertible f₂
      → p ∈ Neg
      → f₁ A.∘ p ≡ f₂ A.∘ p
      → f₁ ≡ f₂

This follows from some isomorphism shuffling. All isomorphisms are monomorphisms, so it suffices to prove that $f_{2}^{- 1} \circ f_{1} = f_{2}^{- 1} \circ f_{2} = id .$ However, $f_{2}^{- 1} \circ f_{1}$ is also an iso, so we can apply our axiom to reduce the goal to showing that $f_{2}^{- 1} \circ f_{1} \circ p = p,$ which follows from our assumption that $f_{1} \circ p = f_{2} \circ p .$

    iso-neg-epic {f₁ = f₁} {f₂ = f₂} {p = p} f₁-inv f₂-inv p∈A⁻ f₁∘p=f₂∘p =
      A.invertible→monic f₂⁻¹-inv f₁ f₂ $
        f₂.inv A.∘ f₁ ≡⟨ f₂⁻¹∘f₁∘p=id ⟩
        A.id          ≡˘⟨ f₂.invr ⟩
        f₂.inv A.∘ f₂ ∎
      where
        module f₁ = A.is-invertible f₁-inv
        module f₂ = A.is-invertible f₂-inv

        f₂⁻¹-inv : A.is-invertible f₂.inv
        f₂⁻¹-inv = A.is-invertible-inverse f₂-inv

        f₂⁻¹∘f₁∘p=id : f₂.inv A.∘ f₁ ≡ A.id
        f₂⁻¹∘f₁∘p=id =
          neg-trivial-stabilizer (A.invertible-∘ f₂⁻¹-inv f₁-inv) p∈A⁻
          $ A.reassocl.from
          $ A.pre-invl.from f₂-inv f₁∘p=f₂∘p

We can also upgrade the stabilizer condition to an equivalence.

    neg-trivial-stabilizer-equiv
      : ∀ {x y} {f : A.Hom y y} {p : A.Hom x y}
      → p ∈ Neg
      → (A.is-invertible f × f A.∘ p ≡ p) ≃ (f ≡ A.id)
    neg-trivial-stabilizer-equiv p∈A⁻ = prop-ext!
      (λ (f-inv , fp=p) → neg-trivial-stabilizer f-inv p∈A⁻ fp=p)
      (λ f=id → (A.subst-is-invertible (sym f=id) A.id-invertible) , A.eliml f=id)

  record Generalized-reedy (ℓ⁻ ℓ⁺ : Level) : Type (o ⊔ ℓ ⊔ lsuc ℓ⁻ ⊔ lsuc ℓ⁺) where
    field
      Neg : Arrows A ℓ⁻
      Pos : Arrows A ℓ⁺
      dim : A.Ob → Nat
      has-generalized-reedy : is-generalized-reedy Neg Pos dim
    open is-generalized-reedy has-generalized-reedy public

Reedy structures and direct categories🔗

module _
  {oc ℓc oa ℓa ℓ⁻ ℓ⁺}
  {C : Precategory oc ℓc} {A : Precategory oa ℓa}
  {Neg : Arrows A ℓ⁻} {Pos : Arrows A ℓ⁺} {dim : Precategory.Ob A → Nat}
  (A-reedy : is-generalized-reedy A Neg Pos dim)
  where
  private
    module A where
      open Cat.Reasoning A public
      open is-generalized-reedy A-reedy public
    open is-generalized-direct

If $(A, A^{-}, A^{+}, dim)$ is a generalized Reedy structure, then the wide subcategory spanned by $A^{+}$ is a generalized direct category.

  generalized-reedy→pos-direct
    : is-generalized-direct (Wide A.Pos-subcat)

First, note that the inclusion functor $ι : A^{+} \to A$ is pseudomonic and thus conservative, as $A^{+}$ contains all isos. This means that if some $f : A^{+} (x, y)$ is non-invertible in $A^{+},$ then it must also be non-invertible in $A .$

In particular, this means that $dim : A_{0} \to N$ is strictly monotone with respect to the relation

x ≺ y := \exists (f : A^{+} (x, y)) . f is not invertible

as non-invertible maps in $A^{+}$ increase dimension. This lets us pull back well-foundedness of $dim (x) < dim (y)$ to $x ≺ y,$ which completes the proof.

  generalized-reedy→pos-direct .≺-wf =
    reflect-wf <-wf dim $ rec! λ f ¬f-inv → A.dim-pos
      (f .witness)
      (¬f-inv ⊙ Forget-conservative)
     where
       Forget-conservative : is-conservative Forget-wide-subcat
       Forget-conservative = pseudomonic→conservative
         (is-pseudomonic-Forget-wide-subcat (A.is-iso→pos _))
         _

Reflecting generalized Reedy structures🔗

Let $(A, A^{-}, A^{+}, dim)$ be a generalized Reedy category, and $ι : C \to A$ be a reflective subcategory with reflector $r ⊣ ι .If$ $A^{-} \subseteq (ι \circ r)^{*} (A^{-})$ and $A^{+} \subseteq (ι \circ r)^{*} (A^{+}),$ then $(ι^{*} (A^{-}), ι^{*} (A^{+}), dim \circ ι)$ is a generalized Reedy structure on $C .$

module _
  {oc ℓc oa ℓa ℓ⁻ ℓ⁺}
  {C : Precategory oc ℓc} {A : Precategory oa ℓa}
  {Neg : Arrows A ℓ⁻} {Pos : Arrows A ℓ⁺} {dim : Precategory.Ob A → Nat}
  {ι : Functor C A} {r : Functor A C}
  where
  open Functor

  reflect-generalized-reedy
    : (r⊣ι : r ⊣ ι)
    → is-reflective r⊣ι
    → Neg ⊆ F-restrict-arrows (ι F∘ r) Neg
    → Pos ⊆ F-restrict-arrows (ι F∘ r) Pos
    → is-generalized-reedy A Neg Pos dim
    → is-generalized-reedy C
        (F-restrict-arrows ι Neg)
        (F-restrict-arrows ι Pos)
        (dim ⊙ ι .F₀)
  reflect-generalized-reedy r⊣ι ι-ff ι∘r-pos ι∘r-neg A-reedy = C-reedy where

    module A where
      open Cat.Reasoning A public
      open is-generalized-reedy A-reedy public

    module C = Cat.Reasoning C
    open is-generalized-reedy

    module ι = Cat.Functor.Reasoning.FullyFaithful ι ι-ff

Our first goal is to show that $(ι^{*} A^{-}, ι^{*} A^{+})$ forms an orthogonal factorisation system on $C .$ This follows from some general results about reflecting OFSs onto reflective subcategories.

    C-reedy : is-generalized-reedy C _ _ _
    C-reedy .neg-pos-ofs =
      reflect-ofs r⊣ι ι-ff ι∘r-pos ι∘r-neg A.neg-pos-ofs

Next, let’s show that the restriction of $dim$ along $ι$ is well-behaved. By definition $ι$ is fully faithful, and thus conservative. This means that we can reflect the (non)-existence of isomorphisms in $A$ into $A,$ which in turn lets us reflect all of the properties of dimensions.

    C-reedy .dim-iso f-inv =
      A.dim-iso (ι.F-map-invertible f-inv)
    C-reedy .dim-neg ι[f]∈A⁻ ¬f-inv =
      A.dim-neg ι[f]∈A⁻ (¬f-inv ⊙ ι.invertible.from)
    C-reedy .dim-pos ι[f]∈A⁺ ¬f-inv =
      A.dim-pos ι[f]∈A⁺ (¬f-inv ⊙ ι.invertible.from)
    C-reedy .neg+pos→invertible ι[f]∈A⁻ ι[f]∈A⁺ =
      ι.invertible.from (A.neg+pos→invertible ι[f]∈A⁻ ι[f]∈A⁺)

Finally, we need to show that the stabilizer subgroups of a $p : C (x, y)$ with $ι (p) \in A^{-}$ are trivial. First, note that a map $f : C (y, y)$ is equal to $id_{y}$ if and only if $ι (f) = id_{ι (y)} .$ However, $ι (p) \in A^{-}$ has trivial stabilizers in $Aut (ι (y)),$ so this is only true if $ι (f)$ is invertible and $ι (f)$ fixes $ι (p) .$ Finally, $ι$ is fully faithful, so this is true if and only if $f$ is invertible and $f \circ p = p .$

    C-reedy .neg-trivial-stabilizer {f = f} {p = p} f-inv ι[p]∈A⁻ f∘p=p =
      flip Equiv.from (f-inv , f∘p=p) $
        f ≡ C.id
          ≃⟨ ι.to-id ⟩
        ι.₁ f ≡ A.id
          ≃˘⟨ A.neg-trivial-stabilizer-equiv ι[p]∈A⁻ ⟩
        A.is-invertible (ι.₁ f) × ι.₁ f A.∘ ι.F₁ p ≡ ι.F₁ p
          ≃⟨ Σ-ap (ι.invertible-equiv e⁻¹) (λ _ → ι.triangle-equivl) ⟩
        C.is-invertible f × f C.∘ p ≡ p
          ≃∎

In the presence of excluded middle, the previous three axioms imply that every map $f : A (x, y)$ with $f \in A^{-} \cap A^{+}$ must be invertible, as otherwise we’d have $dim (x) < dim (y) < dim (x) .$ However, in constructive foundations the best we can do is show that $f$ is not non-invertible, which is why we explicitly require this as an axiom.↩︎