open import Cat.Functor.Conservative
open import Cat.Prelude

open import Data.Wellfounded.Properties
open import Data.Wellfounded.Base

import Cat.Reasoning

module Cat.Direct.Generalized where

Generalized direct categories🔗

module _ {od ℓd} (D : Precategory od ℓd) where
  private
    module D = Cat.Reasoning D

  record is-generalized-direct : Type (od ⊔ ℓd) where
    _≺_ : D.Ob → D.Ob → Type ℓd
    x ≺ y = ∃[ f ∈ D.Hom x y ] ¬ D.is-invertible f

    field
      ≺-wf : Wf _≺_

Closure properties🔗

module _
  {oc ℓc od ℓd}
  {C : Precategory oc ℓc} {D : Precategory od ℓd}
  (F : Functor C D)
  where

If $F:\mathcal{C}\to \mathcal{D}$ is a conservative functor and $\mathcal{D}$ is a generalized direct category, then $\mathcal{C}$ is generalized direct as well.

  conservative→reflect-direct
    : is-conservative F
    → is-generalized-direct D
    → is-generalized-direct C
  conservative→reflect-direct F-conservative D-direct = C-direct where

    module D where
      open Cat.Reasoning D public
      open is-generalized-direct D-direct public

    open Functor F
    open is-generalized-direct

Note that if $F$ is conservative, then it also reflects non-invertibility of morphisms. This lets us pull back well-foundedness of $F(x)\prec F(y)$ in $\mathcal{D}$ to well-foundedness of $x\prec y$ in $\mathcal{C}\text{.}$

    C-direct : is-generalized-direct C
    C-direct .≺-wf =
      reflect-wf D.≺-wf F₀ $ rec! λ f ¬f-inv →
        pure (F₁ f , ¬f-inv ⊙ F-conservative)