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🔗

A precategory $D$ is direct if the relation

x ≺ y := \exists (f : D (x, y)) . f is not invertible

is a well-founded relation.

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 : C \to D$ is a conservative functor and $D$ is a generalized direct category, then $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) ≺ F (y)$ in $D$ to well-foundedness of $x ≺ y$ in $C .$

    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)