Generalized Reedy categories, Direct categories

src/Cat/Diagram/Monad/Kleisli.lagda.md

@@ -220,7 +220,7 @@ adjoint.
 
   Forget-Kleisli-maps-is-conservative : is-conservative Forget-Kleisli-maps
   Forget-Kleisli-maps-is-conservative f-inv =
-    is-ff→is-conservative {F = Kleisli-maps→Kleisli M} (Kleisli-maps→Kleisli-is-ff M) _ $
+    is-ff→is-conservative (Kleisli-maps→Kleisli M) (Kleisli-maps→Kleisli-is-ff M) _ $
     super-inv→sub-inv _ $
     Forget-EM-is-conservative f-inv
 

src/Cat/Direct/Generalized.lagda.md

@@ -0,0 +1,94 @@
+---
+description: |
+  Direct categories.
+---
+
+<!--
+```agda
+open import Cat.Functor.Conservative
+open import Cat.Prelude
+
+open import Data.Wellfounded.Properties
+open import Data.Wellfounded.Base
+
+import Cat.Reasoning
+```
+-->
+
+```agda
+module Cat.Direct.Generalized where
+```
+
+# Generalized direct categories
+
+:::{.definition #generalized-direct-category}
+A [[precategory]] $\cD$ is **direct** if the relation
+
+$$
+x \prec y := \exists(f : \cD(x, y)).\ \text{$f$ is not invertible}
+$$
+
+is a [[well-founded]] relation.
+:::
+
+<!--
+```agda
+module _ {od ℓd} (D : Precategory od ℓd) where
+  private
+    module D = Cat.Reasoning D
+```
+-->
+
+```agda
+  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
+
+<!--
+```agda
+module _
+  {oc ℓc od ℓd}
+  {C : Precategory oc ℓc} {D : Precategory od ℓd}
+  (F : Functor C D)
+  where
+```
+-->
+
+If $F : \cC \to \cD$ is a [[conservative functor]] and $\cD$ is a generalized
+direct category, then $\cC$ is generalized direct as well.
+
+```agda
+  conservative→reflect-direct
+    : is-conservative F
+    → is-generalized-direct D
+    → is-generalized-direct C
+  conservative→reflect-direct F-conservative D-direct = C-direct where
+```
+
+<!--
+```agda
+    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 $\cD$ to well-foundedness of $x \prec y$ in $\cC$.
+
+```agda
+    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)
+```

src/Cat/Displayed/Instances/Subobjects.lagda.md

@@ -415,7 +415,7 @@ Sub-cod y = Forget/ F∘ Sub→Slice y
 Sub→Slice-conservative
   : ∀ y → is-conservative (Sub→Slice y)
 Sub→Slice-conservative y = is-ff→is-conservative
-  {F = Sub→Slice y} (Sub→Slice-is-ff y) _
+  (Sub→Slice y) (Sub→Slice-is-ff y) _
 
 Sub-cod-conservative
   : ∀ y → is-conservative (Sub-cod y)

src/Cat/Functor/Conservative.lagda.md

@@ -71,7 +71,7 @@ equiv→conservative
   → is-equivalence F
   → is-conservative F
 equiv→conservative F eqv =
-  is-ff→is-conservative {F = F} (is-equivalence→is-ff F eqv) _
+  is-ff→is-conservative F (is-equivalence→is-ff F eqv) _
 ```
 
 ## Conservative functors reflect (co)limits that they preserve

src/Cat/Functor/Properties.lagda.md

@@ -72,6 +72,20 @@ module _ {C : Precategory o h} {D : Precategory o₁ h₁} where
     → is-faithful F → is-faithful G
     → is-faithful (F F∘ G)
   is-faithful-∘ Ff Gf p = Gf (Ff p)
+
+  faithful→embedding
+    : ∀ (F : Functor C D)
+    → is-faithful F
+    → ∀ {x y} → is-embedding (F .F₁ {x = x} {y = y})
+  faithful→embedding F F-faithful = injective→is-embedding! F-faithful
+
+  faithful→cancellable
+    : ∀ (F : Functor C D)
+    → is-faithful F
+    → ∀ {x y} {f g : C.Hom x y}
+    → (f ≡ g) ≃ (F .F₁ f ≡ F .F₁ g)
+  faithful→cancellable F F-faithful =
+    ap (F .F₁) , embedding→cancellable (faithful→embedding F F-faithful)
 ```
 -->
 
@@ -119,10 +133,11 @@ module _ {C : Precategory o h} {D : Precategory o₁ h₁} where
   import Cat.Morphism D as Dm
 
   is-ff→is-conservative
-    : {F : Functor C D} → is-fully-faithful F
+    : (F : Functor C D)
+    → is-fully-faithful F
     → ∀ {X Y} (f : C.Hom X Y) → Dm.is-invertible (F .F₁ f)
     → Cm.is-invertible f
-  is-ff→is-conservative {F = F} ff f isinv = i where
+  is-ff→is-conservative F ff f isinv = i where
     open Cm.is-invertible
     open Cm.Inverses
 ```
@@ -169,7 +184,7 @@ the domain category to serve as an inverse for $f$:
     D-inv' .Dm.is-invertible.inverses =
       subst (λ e → Dm.Inverses e from) (sym (equiv→counit ff _)) inverses
 
-    open Cm.is-invertible (is-ff→is-conservative {F = F} ff (equiv→inverse ff to) D-inv')
+    open Cm.is-invertible (is-ff→is-conservative F ff (equiv→inverse ff to) D-inv')
 
     im' : _ Cm.≅ _
     im' .to   = equiv→inverse ff to

src/Cat/Functor/Reasoning.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+open import 1Lab.Equiv
 open import 1Lab.Path
 
 open import Cat.Functor.Base using (module F-iso)
@@ -65,6 +66,17 @@ module _ (a≡id : a ≡ 𝒞.id) where
 
   intror : f ≡ f 𝒟.∘ F₁ a
   intror = 𝒟.intror elim
+
+module _ {X : 𝒞.Ob} {f : 𝒟.Hom (F₀ X) (F₀ X)} where
+
+  id-equivr : (f ≡ F₁ 𝒞.id) ≃ (f ≡ 𝒟.id)
+  id-equivr = ∙-post-equiv F-id
+
+  id-equivl : (F₁ 𝒞.id ≡ f) ≃ (𝒟.id ≡ f)
+  id-equivl = ∙-pre-equiv (sym F-id)
+
+  module id-equivr = Equiv id-equivr
+  module id-equivl = Equiv id-equivl
 ```
 
 ## Reassociations
@@ -134,6 +146,12 @@ popl p = 𝒟.pushr (F-∘ _ _) ∙ ap₂ 𝒟._∘_ p refl
 popr : F₁ b 𝒟.∘ f ≡ g → F₁ (a 𝒞.∘ b) 𝒟.∘ f ≡ F₁ a 𝒟.∘ g
 popr p = 𝒟.pushl (F-∘ _ _) ∙ ap₂ 𝒟._∘_ refl p
 
+pokel : g ≡ f 𝒟.∘ F₁ a → g 𝒟.∘ F₁ b ≡ f 𝒟.∘ F₁ (a 𝒞.∘ b)
+pokel p = ap₂ 𝒟._∘_ p refl ∙ 𝒟.pullr (sym (F-∘ _ _))
+
+poker : g ≡ F₁ b 𝒟.∘ f → F₁ a 𝒟.∘ g ≡ F₁ (a 𝒞.∘ b) 𝒟.∘ f
+poker p = ap₂ 𝒟._∘_ refl p ∙ 𝒟.pulll (sym (F-∘ _ _))
+
 shufflel : f 𝒟.∘ F₁ a ≡ g 𝒟.∘ h → f 𝒟.∘ F₁ (a 𝒞.∘ b) ≡ g 𝒟.∘ h 𝒟.∘ F₁ b
 shufflel p = popl p ∙ sym (𝒟.assoc _ _ _)
 

src/Cat/Functor/Reasoning/FullyFaithful.lagda.md

@@ -41,9 +41,18 @@ private variable
 module _ {a} {b} where
   open Equiv (F₁ {a} {b} , ff) public
 
+invertible-equiv
+  : ∀ {a b} {f : C.Hom a b}
+  → C.is-invertible f ≃ D.is-invertible (F₁ f)
+invertible-equiv {f = f} =
+  prop-ext! F-map-invertible (is-ff→is-conservative F ff f)
+
 iso-equiv : ∀ {a b} → (a C.≅ b) ≃ (F₀ a D.≅ F₀ b)
 iso-equiv {a} {b} = (F-map-iso {x = a} {b} , is-ff→F-map-iso-is-equiv {F = F} ff)
 
+module invertible {a} {b} {f : C.Hom a b} =
+  Equiv (invertible-equiv {f = f})
+
 module iso {a} {b} =
   Equiv (F-map-iso {x = a} {b} , is-ff→F-map-iso-is-equiv {F = F} ff)
 ```
@@ -53,8 +62,14 @@ module iso {a} {b} =
 fromn't : w ≡ F₁ f → from w ≡ f
 fromn't p = ap from p ∙ η _
 
-from-id : w ≡ D.id → from w ≡ C.id
-from-id p = injective₂ (ε _ ∙ p) F-id
+from-id : (w ≡ D.id) ≃ (from w ≡ C.id)
+from-id = ap-equiv ((F₁ , ff) e⁻¹) ∙e ∙-post-equiv (injective₂ (ε D.id) F-id)
+
+to-id : (f ≡ C.id) ≃ (F₁ f ≡ D.id)
+to-id = ap-equiv (F₁ , ff) ∙e id-equivr
+
+module from-id {α} {w : D.Hom (F₀ α) (F₀ α)} = Equiv (from-id {w = w})
+module to-id {a} {f : C.Hom a a} = Equiv (to-id {f = f})
 
 from-∘ : from (w D.∘ x) ≡ from w C.∘ from x
 from-∘ = injective (ε _ ∙ sym (F-∘ _ _ ∙ ap₂ D._∘_ (ε _) (ε _)))
@@ -76,10 +91,10 @@ inv∘l : x D.∘ F₁ f ≡ y → from x C.∘ f ≡ from y
 inv∘l x = sym (ε-twist (D.eliml F-id ∙ sym x)) ∙ C.idl _
 
 whackl : x D.∘ F₁ f ≡ F₁ g → from x C.∘ f ≡ g
-whackl p = sym (ε-twist (D.idr _ ∙ sym p)) ∙ C.elimr (from-id refl)
+whackl p = sym (ε-twist (D.idr _ ∙ sym p)) ∙ C.elimr (from-id.to refl)
 
 whackr : F₁ f D.∘ x ≡ F₁ g → f C.∘ from x ≡ g
-whackr p = ε-twist (p ∙ sym (D.idl _)) ∙ C.eliml (from-id refl)
+whackr p = ε-twist (p ∙ sym (D.idl _)) ∙ C.eliml (from-id.to refl)
 
 pouncer : F₁ f D.∘ x ≡ z → f C.∘ from x ≡ from z
 pouncer p = ε-twist (p ∙ intror refl) ∙ C.idr _
@@ -99,3 +114,19 @@ pouncer p = ε-twist (p ∙ intror refl) ∙ C.idr _
 unwhackr : f C.∘ from w ≡ g → F₁ f D.∘ w ≡ F₁ g
 unwhackr {f = f} {w = w} p = sym (η-twist $ C.idr _ ∙∙ η _ ∙∙ sym p) ∙ elimr refl
 ```
+
+## Lifting Shapes
+
+```agda
+module _ {f : C.Hom b c} {g : C.Hom a b} {h : C.Hom a c} where
+
+  triangle-equivl : (F₁ f D.∘ F₁ g ≡ F₁ h) ≃ (f C.∘ g ≡ h)
+  triangle-equivl =
+    F₁ f D.∘ F₁ g ≡ F₁ h
+      ≃˘⟨ ∙-pre-equiv (sym (F-∘ f g)) ⟩
+    F₁ (f C.∘ g) ≡ F₁ h
+      ≃˘⟨ ap-equiv (F₁ , ff) ⟩
+    f C.∘ g ≡ h ≃∎
+
+  module triangle-equivl = Equiv triangle-equivl
+```

src/Cat/Morphism/Class.lagda.md

@@ -104,3 +104,20 @@ We can take intersections of morphism classes.
   (S ∩ₐ T) .arrows f = f ∈ S × f ∈ T
   (S ∩ₐ T) .is-tr = hlevel 1
 ```
+
+<!--
+```agda
+module _ {oc ℓc od ℓd} {C : Precategory oc ℓc} {D : Precategory od ℓd} where
+  open Functor
+```
+-->
+
+When $F : \cC \to \cD$ is a functor and $S \subseteq \cD$ is a class of morphisms,
+then we can form a class of morphisms $F^{*}(S) \subseteq \cC$ spanned by all
+morphisms of the form $f : \cC(x, y)$ such that $F(f) \in S$.
+
+```agda
+  F-restrict-arrows : ∀ {κ} → Functor C D → Arrows D κ → Arrows C κ
+  F-restrict-arrows F S .arrows f = F .F₁ f ∈ S
+  F-restrict-arrows F S .is-tr = S .is-tr
+```