diff --git a/src/Cat/Diagram/Monad/Kleisli.lagda.md b/src/Cat/Diagram/Monad/Kleisli.lagda.md index a6c4ba5c5..abf3720fd 100644 --- a/src/Cat/Diagram/Monad/Kleisli.lagda.md +++ b/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 diff --git a/src/Cat/Direct/Generalized.lagda.md b/src/Cat/Direct/Generalized.lagda.md new file mode 100644 index 000000000..555a56bc5 --- /dev/null +++ b/src/Cat/Direct/Generalized.lagda.md @@ -0,0 +1,94 @@ +--- +description: | + Direct categories. +--- + + + +```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 + 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 + + + +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 +``` + + + +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) +``` diff --git a/src/Cat/Displayed/Instances/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md index 684a2bdc9..1440d0c80 100644 --- a/src/Cat/Displayed/Instances/Subobjects.lagda.md +++ b/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) diff --git a/src/Cat/Functor/Conservative.lagda.md b/src/Cat/Functor/Conservative.lagda.md index fce410d60..07597b37a 100644 --- a/src/Cat/Functor/Conservative.lagda.md +++ b/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 diff --git a/src/Cat/Functor/Properties.lagda.md b/src/Cat/Functor/Properties.lagda.md index 251a4f93c..cf4153ef5 100644 --- a/src/Cat/Functor/Properties.lagda.md +++ b/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 diff --git a/src/Cat/Functor/Reasoning.lagda.md b/src/Cat/Functor/Reasoning.lagda.md index 5b1da251d..032bff2ec 100644 --- a/src/Cat/Functor/Reasoning.lagda.md +++ b/src/Cat/Functor/Reasoning.lagda.md @@ -1,5 +1,6 @@ + +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 +``` diff --git a/src/Cat/Morphism/Factorisation/Orthogonal.lagda.md b/src/Cat/Morphism/Factorisation/Orthogonal.lagda.md index 5ccdf9f0b..307f0e2a2 100644 --- a/src/Cat/Morphism/Factorisation/Orthogonal.lagda.md +++ b/src/Cat/Morphism/Factorisation/Orthogonal.lagda.md @@ -1,11 +1,16 @@ @@ -82,6 +87,22 @@ a function $f : A \to B$ through the image of $f$.[^regular] ([[strong epimorphism]], [[monomorphism]]) orthogonal factorisation system on a [[regular category]]. + + + +```agda + reflect-ofs + : (r⊣ι : r ⊣ ι) + → is-reflective r⊣ι + → L ⊆ F-restrict-arrows (ι F∘ r) L + → R ⊆ F-restrict-arrows (ι F∘ r) R + → is-ofs D L R + → is-ofs C (F-restrict-arrows ι L) (F-restrict-arrows ι R) + reflect-ofs r⊣ι ι-ff ι∘r-in-L ι∘r-in-R D-ofs = C-ofs where +``` + + + +First, some preliminaries. Note that $\iota^*(L)$ is closed under composition +and inverses, as $\iota$ preserves isomorphisms and is functorial. + +```agda + is-iso→in-ι^*L + : ∀ {a b} + → (f : C.Hom a b) + → C.is-invertible f + → ι.₁ f ∈ L + is-iso→in-ι^*L f f-inv = D.is-iso→in-L (ι.F₁ f) (ι.F-map-invertible f-inv) + + ι^*L-is-stable + : ∀ {a b c} + → (f : C.Hom b c) (g : C.Hom a b) + → ι.₁ f ∈ L → ι.₁ g ∈ L + → ι.₁ (f C.∘ g) ∈ L + ι^*L-is-stable f g ι[f]∈L ι[g]∈L = + subst (_∈ L) (sym (ι.F-∘ f g)) $ + D.L-is-stable (ι.F₁ f) (ι.F₁ g) ι[f]∈L ι[g]∈L +``` + +A similar argument lets us conclude that $\iota^{*}(R)$ is also +closed under composition and inverses. + +```agda + is-iso→in-ι^*R + : ∀ {a b} + → (f : C.Hom a b) + → C.is-invertible f + → ι.₁ f ∈ R + is-iso→in-ι^*R f f-inv = D.is-iso→in-R (ι.F₁ f) (ι.F-map-invertible f-inv) + + ι^*R-is-stable + : ∀ {a b c} + → (f : C.Hom b c) (g : C.Hom a b) + → ι.₁ f ∈ R → ι.₁ g ∈ R + → ι.₁ (f C.∘ g) ∈ R + ι^*R-is-stable f g ι[f]∈R ι[g]∈R = + subst (_∈ R) (sym (ι.F-∘ f g)) $ + D.R-is-stable (ι.F₁ f) (ι.F₁ g) ι[f]∈R ι[g]∈R +``` + +Next, recall that if $r \dashv \iota$ is reflective, then the counit +of the adjunction must be invertible. + +```agda + ε-inv : ∀ (x : C.Ob) → C.is-invertible (ε x) + ε-inv x = is-reflective→counit-is-invertible r⊣ι ι-ff + + module ε (x : C.Ob) = C.is-invertible (ε-inv x) +``` + +With those preliminaries out of the way, we can get into the meat of the proof. +We've already proved the requisite closure properties of $\iota^{*}(L)$ and $\iota^{*}(R)$, +so we can get that out of the way. + +```agda + C-ofs : is-ofs C (F-restrict-arrows ι L) (F-restrict-arrows ι R) + C-ofs .is-iso→in-L = is-iso→in-ι^*L + C-ofs .L-is-stable = ι^*L-is-stable + C-ofs .is-iso→in-R = is-iso→in-ι^*R + C-ofs .R-is-stable = ι^*R-is-stable +``` + +Moreover, $\iota^{*}(L)$ and $\iota^{*}(R)$ are orthogonal, as fully faithful +functors reflect orthogonality. + +```agda + C-ofs .L⊥R f ι[f]∈L g ι[g]∈R = + ff→reflect-orthogonal ι ι-ff (D.L⊥R (ι.₁ f) ι[f]∈L (ι.₁ g) ι[g]∈R) +``` + +The final step is the most difficult. Let $f : \cC(a, b)$ be a morphism in $\cC$: +we somehow need to factor it into a $u : \cC(a, x)$ and $v : \cC(x, b)$ +with $\iota(u) \in L$ and $\iota(v) \in R$. + +We start by factoring $\iota(f)$ into a $u : \cD(\iota(a), x)$ and $v : \cD(x, \iota(b))$. +We can take an adjoint transpose of $u$ to find a map $\cC(r(x), b)$, but this same trick +does not work for $u$. Luckily the counit $\eps : \cC(r(\iota(x)), x)$ is invertible, so +we can transpose $u$ to a map in $\cC$ via $r(u) \circ \eps^{-1} : \cC(a, r(x))$. + +```agda + C-ofs .factor {a} {b} f = f-factor + where + module ι[f] = Factorisation (D.factor (ι.₁ f)) + + f-factor : Factorisation C (F-restrict-arrows ι L) (F-restrict-arrows ι R) f + f-factor .mid = r.₀ ι[f].mid + f-factor .left = r.₁ ι[f].left C.∘ ε.inv a + f-factor .right = ε b C.∘ r.₁ ι[f].right +``` + +A bit of quick algebra shows that these two transposes actually factor $f$. + +```agda + f-factor .factors = + f ≡⟨ C.intror (ε.invl a) ⟩ + f C.∘ ε _ C.∘ ε.inv a ≡⟨ C.extendl (sym $ counit.is-natural a b f) ⟩ + ε b C.∘ r.F₁ (ι.₁ f) C.∘ ε.inv a ≡⟨ C.push-inner (r.expand ι[f].factors) ⟩ + (ε b C.∘ r.₁ ι[f].right) C.∘ (r.₁ ι[f].left C.∘ ε.inv a) ∎ +``` + +Finally, we need to show that $\iota(r(u) \circ \eps^{-1}) \in L$ and +$\iota(\eps \circ r(v)) \in R$. Both $\iota(L)$ and $\iota(R)$ are +closed under inverses and composition, so it suffices to show that +$\iota(r(u)) \in L$ and $\iota(r(v)) \in R$. By assumption, we +have $L \subseteq (\iota \circ r)^{*}(L)$ and $R \subseteq (\iota \circ r)^{*}(R)$, +so it suffices to show that $u \in L$ and $v \in R$. This follows from the +construction of $u$ and $v$ via an $(L,R)$ factorisation, which completes the proof. + +```agda + f-factor .left∈L = + ι^*L-is-stable (r.₁ ι[f].left) (ε.inv a) + (ι∘r-in-L ι[f].left ι[f].left∈L) + (is-iso→in-ι^*L (ε.inv a) (ε.op a)) + f-factor .right∈R = + ι^*R-is-stable (ε b) (r.₁ ι[f].right) + (is-iso→in-ι^*R (ε b) (ε-inv b)) + (ι∘r-in-R ι[f].right ι[f].right∈R) +``` diff --git a/src/Cat/Morphism/Lifts.lagda.md b/src/Cat/Morphism/Lifts.lagda.md index 08e55588b..80f53c2ed 100644 --- a/src/Cat/Morphism/Lifts.lagda.md +++ b/src/Cat/Morphism/Lifts.lagda.md @@ -6,9 +6,12 @@ description: | @@ -379,3 +382,58 @@ a proposition. right-monic→lift-is-prop g-mono vf=gu (l , _ , gl=v) (k , _ , gk=v) = Σ-prop-path! (g-mono l k (gl=v ∙ sym gk=v)) ``` + +## Mapping liftings + + + +```agda + F-map-lifting + : ∀ {A B X Y} {f : C.Hom A B} {g : C.Hom X Y} {u : C.Hom A X} {v : C.Hom B Y} + → Lifting C f g u v + → Lifting D (F.₁ f) (F.₁ g) (F.₁ u) (F.₁ v) + F-map-lifting {f = f} (w , w∘f=u , g∘w=v) = + F.₁ w , F.collapse w∘f=u , F.collapse g∘w=v +``` + + +## Reflecting liftings + + + +If $\iota : \cC \to \cD$ is a [[fully faithful functor]], then +we can reflect liftings along $\iota$. + +```agda + ff→reflect-lifting + : ∀ {A B X Y} {f : C.Hom A B} {g : C.Hom X Y} {u : C.Hom A X} {v : C.Hom B Y} + → Lifting D (ι.₁ f) (ι.₁ g) (ι.₁ u) (ι.₁ v) + → Lifting C f g u v + ff→reflect-lifting {f = f} (w , w∘ι[f]=ι[u] , ι[g]∘w=ι[v]) = + ι.from w , + ι.whackl w∘ι[f]=ι[u] , + ι.whackr ι[g]∘w=ι[v] +``` diff --git a/src/Cat/Morphism/Orthogonal.lagda.md b/src/Cat/Morphism/Orthogonal.lagda.md index fbf3fe1f8..140e024b0 100644 --- a/src/Cat/Morphism/Orthogonal.lagda.md +++ b/src/Cat/Morphism/Orthogonal.lagda.md @@ -8,6 +8,7 @@ open import Cat.Morphism.Class open import Cat.Morphism.Lifts open import Cat.Prelude +import Cat.Functor.Reasoning.FullyFaithful import Cat.Functor.Reasoning import Cat.Reasoning ``` @@ -217,6 +218,54 @@ to every other class. ``` --> +## Fully faithful functors + + + +If $\iota : \cC \to \cD$ is a [[fully faithful functor]] and $\iota(f) \ortho \iota(g)$ +in $\cD$, then $f \ortho g$ in $\cC$. + +```agda + ff→reflect-orthogonal + : ∀ {A B X Y} {f : C.Hom A B} {g : C.Hom X Y} + → Orthogonal D (ι.₁ f) (ι.₁ g) + → Orthogonal C f g +``` + +Suppose that $\iota(f) \ortho \iota(g)$, and let $v \circ f = g \circ u$ be a square +in $\cD$. Functors preserve all commutative diagrams, so we also have a square +$\iota(v) \circ \iota(f) = \iota(g) \circ \iota(u)$ in $\cD$. This in turn gives us a +lift $w$ of the square in $\cD$, as $\iota(f) \ortho \iota(g)$. Moreover, $\iota$ is +fully faithful, so we can reflect this lift back to $\cC$. + +```agda + ff→reflect-orthogonal {f = f} {g = g} ι[f]⊥ι[g] u v vf=gu .centre = + ff→reflect-lifting ι ι-ff (ι[f]⊥ι[g] (ι.₁ u) (ι.₁ v) (ι.weave vf=gu) .centre) +``` + +Uniqueness of the lift follows from a similar argument. Let $w'$ be a lift of the square +$v \circ f = g \circ u$. Functors preserve liftings, so $\iota(w')$ is a lift of +$\iota(v) \circ \iota(f) = \iota(g) \circ \iota(u)$. However, $\iota(f) \ortho \iota(g)$, +so $\iota(w') = w$. Finally, $\iota$ is an equivalence on hom sets, so we get $w' = \iota^{-1}(w)$. + +```agda + ff→reflect-orthogonal {f = f} {g = g} ι[f]⊥ι[g] u v vf=gu .paths w = + Σ-prop-path! $ sym $ ι.adjunctl $ sym $ ap fst + $ ι[f]⊥ι[g] (ι.₁ u) (ι.₁ v) (ι.weave vf=gu) .paths (F-map-lifting ι w) +``` + ## Regarding reflections diff --git a/src/Cat/Reedy/Generalized.lagda.md b/src/Cat/Reedy/Generalized.lagda.md new file mode 100644 index 000000000..5946df6a0 --- /dev/null +++ b/src/Cat/Reedy/Generalized.lagda.md @@ -0,0 +1,331 @@ +--- +description: | + Generalized Reedy categories. +--- + + + +```agda +module Cat.Reedy.Generalized where +``` + + + +# Generalized Reedy categories + +:::{.definition #generalized-reedy-structure} +A *generalized Reedy structure* on a [[precategory]] $\cA$ consists of: + +- two classes of morphisms $\cA^{-}, \cA^{+} \subseteq \cA$, and +- a function $\mathrm{dim} : \cA_{0} \to \NN$ + +```agda + record is-generalized-reedy + {ℓ⁻ ℓ⁺} (Neg : Arrows A ℓ⁻) (Pos : Arrows A ℓ⁺) + (dim : A.Ob → Nat) + : Type (o ⊔ ℓ ⊔ ℓ⁺ ⊔ ℓ⁻) where +``` + +subject to the following conditions: + +- The pair $(\cA^{-}, \cA^{+})$ forms an [[orthogonal factorisation system]]. + In particular, this means that both $\cA^{-}$ and $\cA^{+}$ contain all + isomorphism of $\cA$ and are closed under composition. +::: + + +```agda + 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 : \cA(x, y)$ is invertible, then $\mathrm{dim}(x) = \mathrm{dim}(y)$. +- If $f : \cA^{-}(x, y)$ is non-invertible then $\mathrm{dim}(x) > \mathrm{dim}(y)$. +- If $f : \cA^{+}(x, y)$ is non-invertible then $\mathrm{dim}(x) < \mathrm{dim}(y)$. + +```agda + 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 : \cA(x, y)$ is in $\cA^{-} \cap \cA^{+}$, then $f$ must be + invertible[^1]. + +[^1]: In the presence of [[excluded middle]], the previous three axioms + imply that every map $f : \cA(x, y)$ with $f \in \cA^{-} \cap \cA^{+}$ + must be invertible, as otherwise we'd have $\mathrm{dim}(x) < \mathrm{dim}(y) < \mathrm{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. + +```agda + 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 \iso y$ and $p : \cA^{-}(x, y)$, + if $f \circ p = p$ then $p = \id$. In other words, the stabilizer subgroup + of $\mathrm{Aut}(y)$ relative to $p : \cA^{-}(x, y)$ is trivial. + +```agda + 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 $\cA$ view +morphisms in $\cA^{-}$ as [[epimorphisms]]. + +```agda + 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$. + +```agda + 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. + +```agda + 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) +``` + + + +## Reedy structures and direct categories + +```agda +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 $(\cA, \cA^{-}, \cA^{+}, \mathrm{dim})$ is a generalized Reedy structure, +then the wide subcategory spanned by $\cA^{+}$ is a [[generalized direct category]]. + +```agda + generalized-reedy→pos-direct + : is-generalized-direct (Wide A.Pos-subcat) +``` + +First, note that the inclusion functor $\iota : \cA^{+} \to \cA$ is +[[pseudomonic]] and thus [[conservative]], as $\cA^{+}$ contains +all isos. This means that if some $f : \cA^{+}(x, y)$ is non-invertible +in $\cA^{+}$, then it must also be non-invertible in $\cA$. + +In particular, this means that $\mathrm{dim} : \cA_{0} \to \NN$ is +strictly monotone with respect to the relation + +$$ +x \prec y := \exists(f : \cA^{+}(x, y)).\ \text{\(f\) is not invertible} +$$ + +as non-invertible maps in $\cA^{+}$ increase dimension. This lets us +pull back well-foundedness of $\mathrm{dim}(x) < \mathrm{dim}(y)$ to +$x \prec y$, which completes the proof. + +```agda + 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 $(\cA, \cA^{-}, \cA^{+}, \mathrm{dim})$ be a generalized Reedy +category, and $\iota : \cC \to \cA$ be a [[reflective subcategory]] +with reflector $r \dashv \iota$.If $\cA^{-} \subseteq (\iota \circ r)^{*}(\cA^{-})$ +and $\cA^{+} \subseteq (\iota \circ r)^{*}(\cA^{+})$, then +$(\iota^{*}(\cA^{-}), \iota^{*}(\cA^{+}), \mathrm{dim} \circ \iota)$ is a +generalized Reedy structure on $\cC$. + + + +```agda + 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 +``` + + + +Our first goal is to show that $(\iota^{*}\cA^{-}, \iota^{*}\cA^{+})$ +forms an orthogonal factorisation system on $\cC$. This follows from +some general results about reflecting OFSs onto reflective subcategories. + +```agda + 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 $\mathrm{dim}$ along $\iota$ +is well-behaved. By definition $\iota$ is [[fully faithful]], and thus +[[conservative]]. This means that we can reflect the (non)-existence +of isomorphisms in $\cA$ into $\cA$, which in turn lets us reflect +all of the properties of dimensions. + +```agda + 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 : \cC(x,y)$ +with $\iota(p) \in \cA^{-}$ are trivial. First, note that a map $f : \cC(y, y)$ +is equal to $\id_{y}$ if and only if $\iota(f) = \id_{\iota(y)}$. However, +$\iota(p) \in \cA^{-}$ has trivial stabilizers in $\mathrm{Aut}(\iota(y))$, +so this is only true if $\iota(f)$ is invertible and $\iota(f)$ fixes $\iota(p)$. +Finally, $\iota$ is fully faithful, so this is true if and only if $f$ +is invertible and $f \circ p = p$. + +```agda + 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 + ≃∎ +``` diff --git a/src/Cat/Univalent/Rezk/Universal.lagda.md b/src/Cat/Univalent/Rezk/Universal.lagda.md index d2c7a85c8..23df623ab 100644 --- a/src/Cat/Univalent/Rezk/Universal.lagda.md +++ b/src/Cat/Univalent/Rezk/Universal.lagda.md @@ -335,7 +335,7 @@ candidate over it. Σ-prop-pathp! $ funextP λ a → funextP λ h → C.≅-pathp _ _ $ Univalent.Hom-pathp-reflr-iso c-cat {q = c≅c'} - ( C.pullr (F.eliml (H.from-id (h₀ .invr))) + ( C.pullr (F.eliml (H.from-id.to (h₀ .invr))) ∙ β _ _ _ (H.ε-lswizzle (h₀ .invl))) where ckα = obj' (a₀ , h₀) diff --git a/src/Data/Nat/Base.lagda.md b/src/Data/Nat/Base.lagda.md index 907b1c02a..846ef0439 100644 --- a/src/Data/Nat/Base.lagda.md +++ b/src/Data/Nat/Base.lagda.md @@ -252,6 +252,10 @@ infix 7 _<_ _≤_ @@ -55,3 +55,43 @@ suc-wf = Induction-wf (λ x y → y ≡ suc x) λ P m → k' : ∀ x → x < suc y → Acc _<_ x k' x' w' = go x x' (≤-trans (≤-peel w') (≤-peel w)) ``` + +Let $(A, R)$ and $(B, S)$ be a pair of types equipped with relations, +and $f : A \to B$ be a map that satisfies + +$$ +\forall x y.\ R(x, y) \to S(f(x), f(y)) +$$. + +If $S$ is a well-founded relation on $B$, then $R$ must also be well-founded. + +```agda +reflect-wf + : Wf S + → (f : A → B) + → (∀ {x y} → R x y → S (f x) (f y)) + → Wf R +``` + +The idea here is to use the fact that every $b$ in the image of $f$ must be accessible. +Let $a : A$, $b : B$ such that $f(a) = b$ and $b$ is accessible via $S$. To show that +$a$ is accessible via $R$, we must show that $a'$ is accessible for every $R(a', a)$. However, +monotonicity of $f$ means that $S(f(a'), f(a))$, and $f(a) = b$, which means that $f(a')$ must +be accessible via $S$. We can then recurse to show that $a'$ is accessible. + +```agda +reflect-wf {B = B} {S = S} {A = A} {R = R} S-wf f f-mono a = im-acc (f a) a refl (S-wf (f a)) where + im-acc : (b : B) (a : A) → f a ≡ b → Acc S b → Acc R a + im-acc b a fa=b (acc rec) = acc λ a' R[a',a] → + im-acc (f a') a' refl (rec (f a') (subst (S (f a')) fa=b (f-mono R[a',a]))) +``` + +As a corollary, we can pull back accessibility along arbitrary functions. + +```agda +pullback-wf + : (f : A → B) + → Wf R + → Wf (λ x y → R (f x) (f y)) +pullback-wf f R-wf = reflect-wf R-wf f id +```