From 3c46e0563d1b3fd3d60abf8d20c8304e70e87f05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia?= Date: Mon, 31 Jul 2023 18:13:42 -0300 Subject: [PATCH 1/5] Explode Cat.Instances.Functor (#244) Disappear. This module is an eyesore. --- src/Algebra/Group/Cat/Base.lagda.md | 1 + src/Algebra/Group/Cat/Monadic.lagda.md | 2 +- src/Algebra/Monoid/Category.lagda.md | 6 +- src/Cat/Abelian/Instances/Functor.lagda.md | 2 +- src/Cat/Base.lagda.md | 12 + src/Cat/Bi/Base.lagda.md | 5 +- src/Cat/Bi/Instances/InternalCats.lagda.md | 15 +- src/Cat/Diagram/Colimit/Base.lagda.md | 23 +- .../Diagram/Colimit/Representable.lagda.md | 6 +- src/Cat/Diagram/Idempotent.lagda.md | 2 +- src/Cat/Diagram/Image.lagda.md | 2 +- src/Cat/Diagram/Limit/Base.lagda.md | 27 +- src/Cat/Diagram/Monad.lagda.md | 2 +- src/Cat/Displayed/Cartesian/Weak.lagda.md | 22 +- src/Cat/Displayed/Cocartesian/Weak.lagda.md | 22 +- src/Cat/Displayed/Comprehension.lagda.md | 13 +- src/Cat/Displayed/GenericObject.lagda.md | 6 +- .../Displayed/Instances/CT-Structure.lagda.md | 9 +- .../Instances/Externalisation.lagda.md | 10 +- src/Cat/Displayed/Instances/Family.lagda.md | 15 +- src/Cat/Displayed/Instances/Lifting.lagda.md | 4 +- src/Cat/Displayed/Instances/Objects.lagda.md | 5 +- src/Cat/Displayed/Instances/Simple.lagda.md | 11 +- src/Cat/Displayed/Instances/Slice.lagda.md | 2 +- .../Displayed/Instances/Subobjects.lagda.md | 10 +- src/Cat/Displayed/Total.lagda.md | 3 +- src/Cat/Displayed/Univalence/Thin.lagda.md | 2 +- src/Cat/Functor/Adjoint.lagda.md | 26 +- src/Cat/Functor/Adjoint/Compose.lagda.md | 58 +- src/Cat/Functor/Adjoint/Hom.lagda.md | 10 +- src/Cat/Functor/Adjoint/Reflective.lagda.md | 6 +- src/Cat/Functor/Adjoint/Unique.lagda.md | 3 +- src/Cat/Functor/Base.lagda.md | 479 +++++++--------- src/Cat/Functor/Closed.lagda.md | 101 ++++ src/Cat/Functor/Coherence.agda | 5 +- .../{Instances => }/Functor/Compose.lagda.md | 39 +- src/Cat/Functor/Dense.lagda.md | 2 +- src/Cat/Functor/Equivalence.lagda.md | 27 +- src/Cat/Functor/Equivalence/Path.lagda.md | 4 +- src/Cat/Functor/Everything.agda | 25 - src/Cat/Functor/FullSubcategory.lagda.md | 6 +- src/Cat/Functor/Hom.lagda.md | 8 +- src/Cat/Functor/Hom/Coyoneda.lagda.md | 2 +- src/Cat/Functor/Hom/Representable.lagda.md | 16 +- src/Cat/Functor/Kan/Adjoint.lagda.md | 2 +- src/Cat/Functor/Kan/Base.lagda.md | 4 +- src/Cat/Functor/Kan/Global.lagda.md | 4 +- src/Cat/Functor/Kan/Nerve.lagda.md | 2 +- src/Cat/Functor/Kan/Pointwise.lagda.md | 17 +- src/Cat/Functor/Kan/Representable.lagda.md | 21 +- src/Cat/Functor/Kan/Unique.lagda.md | 101 ++-- src/Cat/Functor/Naturality.lagda.md | 189 +++++++ src/Cat/Functor/Properties.lagda.md | 321 +++++++++++ src/Cat/Functor/Pullback.lagda.md | 2 +- .../Functor/Reasoning/FullyFaithful.lagda.md | 1 + src/Cat/Functor/Slice.lagda.md | 1 + src/Cat/Functor/Univalence.lagda.md | 95 ++++ src/Cat/Functor/WideSubcategory.lagda.md | 8 +- src/Cat/Gaunt.lagda.md | 5 +- src/Cat/Instances/Comma/Univalent.lagda.md | 4 +- src/Cat/Instances/Core.lagda.md | 4 +- src/Cat/Instances/Functor.lagda.md | 514 +----------------- src/Cat/Instances/InternalFunctor.lagda.md | 14 +- .../InternalFunctor/Compose.lagda.md | 10 +- src/Cat/Instances/Karoubi.lagda.md | 4 +- src/Cat/Instances/OuterFunctor.lagda.md | 5 +- src/Cat/Instances/Shape/Involution.lagda.md | 6 +- src/Cat/Instances/Shape/Terminal.lagda.md | 5 +- src/Cat/Instances/Slice.lagda.md | 2 +- src/Cat/Instances/Slice/Presheaf.lagda.md | 2 +- src/Cat/Internal/Functor/Outer.lagda.md | 13 +- src/Cat/Internal/Instances/Discrete.lagda.md | 4 +- src/Cat/Internal/Morphism.lagda.md | 5 +- src/Cat/Internal/Sets.lagda.md | 5 +- .../Diagram/Monoid/Representable.lagda.md | 5 +- src/Cat/Morphism/Orthogonal.lagda.md | 2 +- src/Cat/Reasoning.lagda.md | 13 +- src/Cat/Regular/Instances/Sets.lagda.md | 2 +- src/Cat/Regular/Slice.lagda.md | 2 +- src/Cat/Skeletal.lagda.md | 2 +- src/Cat/Univalent/Instances/Algebra.lagda.md | 2 +- src/Cat/Univalent/Rezk.lagda.md | 15 +- src/Cat/Univalent/Rezk/Universal.lagda.md | 6 +- src/HoTT.lagda.md | 9 +- src/Topoi/Base.lagda.md | 12 +- src/Topoi/Classifying/Diaconescu.lagda.md | 3 +- src/Topoi/Reasoning.lagda.md | 4 +- src/autorefs.txt | 4 +- src/index.lagda.md | 8 +- 89 files changed, 1315 insertions(+), 1200 deletions(-) create mode 100644 src/Cat/Functor/Closed.lagda.md rename src/Cat/{Instances => }/Functor/Compose.lagda.md (81%) delete mode 100644 src/Cat/Functor/Everything.agda create mode 100644 src/Cat/Functor/Naturality.lagda.md create mode 100644 src/Cat/Functor/Properties.lagda.md create mode 100644 src/Cat/Functor/Univalence.lagda.md diff --git a/src/Algebra/Group/Cat/Base.lagda.md b/src/Algebra/Group/Cat/Base.lagda.md index 127d3fe1c..054d32846 100644 --- a/src/Algebra/Group/Cat/Base.lagda.md +++ b/src/Algebra/Group/Cat/Base.lagda.md @@ -4,6 +4,7 @@ open import Algebra.Prelude open import Algebra.Group open import Cat.Displayed.Univalence.Thin +open import Cat.Functor.Properties open import Cat.Prelude ``` --> diff --git a/src/Algebra/Group/Cat/Monadic.lagda.md b/src/Algebra/Group/Cat/Monadic.lagda.md index 20b501819..6efc1701d 100644 --- a/src/Algebra/Group/Cat/Monadic.lagda.md +++ b/src/Algebra/Group/Cat/Monadic.lagda.md @@ -9,8 +9,8 @@ open import Algebra.Group open import Cat.Functor.Adjoint.Monadic open import Cat.Functor.Adjoint.Monad open import Cat.Functor.Equivalence +open import Cat.Functor.Properties open import Cat.Diagram.Monad -open import Cat.Functor.Base import Algebra.Group.Cat.Base as Grp diff --git a/src/Algebra/Monoid/Category.lagda.md b/src/Algebra/Monoid/Category.lagda.md index ffe1ca65c..56f7289fd 100644 --- a/src/Algebra/Monoid/Category.lagda.md +++ b/src/Algebra/Monoid/Category.lagda.md @@ -8,8 +8,8 @@ open import Cat.Displayed.Univalence.Thin open import Cat.Functor.Adjoint.Monadic open import Cat.Functor.Equivalence open import Cat.Instances.Delooping +open import Cat.Functor.Properties open import Cat.Functor.Adjoint -open import Cat.Functor.Base open import Cat.Prelude open import Data.List @@ -228,8 +228,8 @@ are equivalent to monoid homomorphisms) and that it is [split essentially surjective][eso]. [monadic]: Cat.Functor.Adjoint.Monadic.html -[ff]: Cat.Functor.Base.html#ff-functors -[eso]: Cat.Functor.Base.html#essential-fibres +[ff]: Cat.Functor.Properties.html#ff-functors +[eso]: Cat.Functor.Properties.html#essential-fibres ```agda Monoid-is-monadic : ∀ {ℓ} → is-monadic (Free⊣Forget {ℓ}) diff --git a/src/Cat/Abelian/Instances/Functor.lagda.md b/src/Cat/Abelian/Instances/Functor.lagda.md index 313a4735d..2c52e0a1e 100644 --- a/src/Cat/Abelian/Instances/Functor.lagda.md +++ b/src/Cat/Abelian/Instances/Functor.lagda.md @@ -48,7 +48,7 @@ a group homomorphism. [$\Ab$-categories]: Cat.Abelian.Base.html#ab-enriched-categories [$\Ab$-functors]: Cat.Abelian.Functor.html#ab-enriched-functors -[functor category]: Cat.Instances.Functor.html +[functor category]: Cat.Functor.Base.html ```agda Ab-functors : Precategory _ _ diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md index 5172aedca..d0690dee2 100644 --- a/src/Cat/Base.lagda.md +++ b/src/Cat/Base.lagda.md @@ -466,6 +466,18 @@ Natural transformations also dualize. The opposite of $\eta : F @@ -57,7 +56,7 @@ the identity internal natural isomorphism as-is. ```agda ƛ : ∀ {A B : Internal-cat} - → natural-iso Id (Right (Fi∘-functor A B B) Idi) + → Id ≅ⁿ Right (Fi∘-functor A B B) Idi ƛ {B = B} = to-natural-iso ni where open Cat.Internal.Reasoning B ni : make-natural-iso _ _ @@ -77,7 +76,7 @@ the identity internal natural isomorphism as-is. idri _ ∙ id-commi ρ : ∀ {A B : Internal-cat} - → natural-iso Id (Left (Fi∘-functor A A B) Idi) + → Id ≅ⁿ Left (Fi∘-functor A A B) Idi ρ {B = B} = to-natural-iso ni where open Cat.Internal.Reasoning B ni : make-natural-iso _ _ @@ -97,7 +96,7 @@ the identity internal natural isomorphism as-is. idri _ ∙ ap (_∘i _) (G .Fi-id) α : {A B C D : Internal-cat} - → natural-iso + → _≅ⁿ_ {C = Internal-functors _ C D ×ᶜ Internal-functors _ B C ×ᶜ Internal-functors _ A B} (compose-assocˡ (λ {A} {B} {C} → Fi∘-functor A B C)) (compose-assocʳ λ {A} {B} {C} → Fi∘-functor A B C) diff --git a/src/Cat/Diagram/Colimit/Base.lagda.md b/src/Cat/Diagram/Colimit/Base.lagda.md index 25cf69aca..12bcb621b 100644 --- a/src/Cat/Diagram/Colimit/Base.lagda.md +++ b/src/Cat/Diagram/Colimit/Base.lagda.md @@ -405,7 +405,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory @@ -477,7 +476,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory → is-lan !F D K' eta is-invertible→is-colimitp {K' = K'} {eta = eta} eps p q invert = generalize-colimitp - (is-invertible→is-lan Cy $ componentwise-invertible→invertible _ λ _ → invert) + (is-invertible→is-lan Cy $ invertible→invertibleⁿ _ λ _ → invert) q ``` @@ -488,8 +487,8 @@ coapex of $C$ is also a colimit of $Dia'$. ```agda natural-iso-diagram→is-colimitp : ∀ {D′ : Functor J C} {eta : D′ => K F∘ !F} - → (isos : natural-iso D D′) - → (∀ {j} → Cy.ψ j C.∘ natural-iso.from isos .η j ≡ eta .η j) + → (isos : D ≅ⁿ D′) + → (∀ {j} → Cy.ψ j C.∘ Isoⁿ.from isos .η j ≡ eta .η j) → is-lan !F D′ K eta natural-iso-diagram→is-colimitp {D′ = D′} isos q = generalize-colimitp (natural-iso-of→is-lan Cy isos) @@ -501,11 +500,9 @@ coapex of $C$ is also a colimit of $Dia'$. module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D D′ : Functor J C} where natural-iso→colimit - : natural-iso D D′ - → Colimit D - → Colimit D′ + : D ≅ⁿ D′ → Colimit D → Colimit D′ natural-iso→colimit isos C .Lan.Ext = Lan.Ext C - natural-iso→colimit isos C .Lan.eta = Lan.eta C ∘nt natural-iso.from isos + natural-iso→colimit isos C .Lan.eta = Lan.eta C ∘nt Isoⁿ.from isos natural-iso→colimit isos C .Lan.has-lan = natural-iso-of→is-lan (Lan.has-lan C) isos ``` --> @@ -618,7 +615,7 @@ module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategor open _=>_ natural-iso→preserves-colimits - : natural-iso F F' + : F ≅ⁿ F' → preserves-colimit F Dia → preserves-colimit F' Dia natural-iso→preserves-colimits α F-preserves {K = K} {eps} colim = @@ -631,7 +628,7 @@ module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategor F' .F₁ (eps .η j) ∎) (F-preserves colim) where - module α = natural-iso α + module α = Isoⁿ α ``` --> diff --git a/src/Cat/Diagram/Colimit/Representable.lagda.md b/src/Cat/Diagram/Colimit/Representable.lagda.md index 8b048e504..c428d16d1 100644 --- a/src/Cat/Diagram/Colimit/Representable.lagda.md +++ b/src/Cat/Diagram/Colimit/Representable.lagda.md @@ -1,13 +1,13 @@ @@ -762,7 +759,7 @@ module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategor open _=>_ natural-iso→preserves-limits - : natural-iso F F' + : F ≅ⁿ F' → preserves-limit F Dia → preserves-limit F' Dia natural-iso→preserves-limits α F-preserves {K = K} {eps} lim = @@ -775,7 +772,7 @@ module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategor F' .F₁ (eps .η j) ∎) (F-preserves lim) where - module α = natural-iso α + module α = Isoⁿ α ``` --> diff --git a/src/Cat/Diagram/Monad.lagda.md b/src/Cat/Diagram/Monad.lagda.md index 97ec9c4ba..4c179735e 100644 --- a/src/Cat/Diagram/Monad.lagda.md +++ b/src/Cat/Diagram/Monad.lagda.md @@ -1,7 +1,7 @@ @@ -669,9 +669,7 @@ module _ (fib : Cartesian-fibration) where fibration→hom-iso-from : ∀ {x y x′} (u : Hom x y) - → natural-iso - (Hom-over-from ℰ u x′) - (Hom-from (Fibre ℰ x) x′ F∘ base-change u) + → Hom-over-from ℰ u x′ ≅ⁿ Hom-from (Fibre ℰ x) x′ F∘ base-change u fibration→hom-iso-from {x} {y} {x′} u = to-natural-iso mi where open make-natural-iso @@ -711,9 +709,7 @@ module _ (fib : Cartesian-fibration) where fibration→hom-iso-into : ∀ {x y y′} (u : Hom x y) - → natural-iso - (Hom-over-into ℰ u y′) - (Hom-into (Fibre ℰ x) (has-lift.x′ u y′)) + → Hom-over-into ℰ u y′ ≅ⁿ Hom-into (Fibre ℰ x) (has-lift.x′ u y′) fibration→hom-iso-into u = weak-fibration→hom-iso-into (fibration→weak-fibration fib) u ``` @@ -725,13 +721,13 @@ a natural iso between $\cE_{u}(-,-)$ and $\cE_{id}(-,u^{*}(-))$. ```agda fibration→hom-iso : ∀ {x y} (u : Hom x y) - → natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u)) + → Hom-over ℰ u ≅ⁿ Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u) fibration→hom-iso {x = x} u = to-natural-iso mi where open make-natural-iso open _=>_ - module into-iso {y′} = natural-iso (fibration→hom-iso-into {y′ = y′} u) - module from-iso {x′} = natural-iso (fibration→hom-iso-from {x′ = x′} u) + module into-iso {y′} = Isoⁿ (fibration→hom-iso-into {y′ = y′} u) + module from-iso {x′} = Isoⁿ (fibration→hom-iso-from {x′ = x′} u) mi : make-natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u)) mi .eta x u′ = has-lift.universalv u _ u′ diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md index d749ab0bb..1f6376a0e 100644 --- a/src/Cat/Displayed/Cocartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Weak.lagda.md @@ -602,7 +602,7 @@ Furthermore, this equivalence is natural. ```agda weak-opfibration→hom-iso-from : ∀ {x y x′} (u : Hom x y) - → natural-iso (Hom-over-from ℰ u x′) (Hom-from (Fibre ℰ y) (weak-lift.y′ u x′)) + → Hom-over-from ℰ u x′ ≅ⁿ Hom-from (Fibre ℰ y) (weak-lift.y′ u x′) weak-opfibration→hom-iso-from {y = y} {x′ = x′} u = to-natural-iso mi where open make-natural-iso @@ -660,15 +660,15 @@ module _ (U : ∀ {x y} → Hom x y → Functor (Fibre ℰ x) (Fibre ℰ y)) whe hom-iso→weak-opfibration : (∀ {x y x′} (u : Hom x y) - → natural-iso (Hom-over-from ℰ u x′) (Hom-from (Fibre ℰ y) (U u .F₀ x′))) + → Hom-over-from ℰ u x′ ≅ⁿ Hom-from (Fibre ℰ y) (U u .F₀ x′)) → is-weak-cocartesian-fibration hom-iso→weak-opfibration hom-iso = vertical-equiv→weak-opfibration (λ u → U u .F₀) - (λ u′ → natural-iso.to (hom-iso _) .η _ u′) + (λ u′ → Isoⁿ.to (hom-iso _) .η _ u′) (natural-iso-to-is-equiv (hom-iso _) _) λ f′ g′ → to-pathp⁻ $ - happly (natural-iso.to (hom-iso _) .is-natural _ _ f′) g′ + happly (Isoⁿ.to (hom-iso _) .is-natural _ _ f′) g′ ``` --> @@ -680,15 +680,13 @@ module _ (opfib : Cocartesian-fibration) where opfibration→hom-iso-from : ∀ {x y x′} (u : Hom x y) - → natural-iso (Hom-over-from ℰ u x′) (Hom-from (Fibre ℰ y) (has-lift.y′ u x′)) + → Hom-over-from ℰ u x′ ≅ⁿ Hom-from (Fibre ℰ y) (has-lift.y′ u x′) opfibration→hom-iso-from u = weak-opfibration→hom-iso-from (opfibration→weak-opfibration opfib) u opfibration→hom-iso-into : ∀ {x y y′} (u : Hom x y) - → natural-iso - (Hom-over-into ℰ u y′) - (Hom-into (Fibre ℰ y) y′ F∘ Functor.op (cobase-change u) ) + → Hom-over-into ℰ u y′ ≅ⁿ Hom-into (Fibre ℰ y) y′ F∘ Functor.op (cobase-change u) opfibration→hom-iso-into {y = y} {y′ = y′} u = to-natural-iso mi where open make-natural-iso @@ -711,16 +709,14 @@ module _ (opfib : Cocartesian-fibration) where opfibration→hom-iso : ∀ {x y} (u : Hom x y) - → natural-iso - (Hom-over ℰ u) - (Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id)) + → Hom-over ℰ u ≅ⁿ Hom[-,-] (Fibre ℰ y) F∘ (Functor.op (cobase-change u) F× Id) opfibration→hom-iso {y = y} u = to-natural-iso mi where open make-natural-iso open _=>_ open Functor - module into-iso {y′} = natural-iso (opfibration→hom-iso-into {y′ = y′} u) - module from-iso {x′} = natural-iso (opfibration→hom-iso-from {x′ = x′} u) + module into-iso {y′} = Isoⁿ (opfibration→hom-iso-into {y′ = y′} u) + module from-iso {x′} = Isoⁿ (opfibration→hom-iso-from {x′ = x′} u) module Fibre {x} = CR (Fibre ℰ x) mi : make-natural-iso diff --git a/src/Cat/Displayed/Comprehension.lagda.md b/src/Cat/Displayed/Comprehension.lagda.md index 4138f3c74..795d04f69 100644 --- a/src/Cat/Displayed/Comprehension.lagda.md +++ b/src/Cat/Displayed/Comprehension.lagda.md @@ -1,19 +1,18 @@ diff --git a/src/Cat/Displayed/GenericObject.lagda.md b/src/Cat/Displayed/GenericObject.lagda.md index aabf52e5b..53cf3a412 100644 --- a/src/Cat/Displayed/GenericObject.lagda.md +++ b/src/Cat/Displayed/GenericObject.lagda.md @@ -1,12 +1,12 @@ diff --git a/src/Cat/Displayed/Instances/CT-Structure.lagda.md b/src/Cat/Displayed/Instances/CT-Structure.lagda.md index 5ec624728..b96f62dfe 100644 --- a/src/Cat/Displayed/Instances/CT-Structure.lagda.md +++ b/src/Cat/Displayed/Instances/CT-Structure.lagda.md @@ -1,13 +1,12 @@ diff --git a/src/Cat/Displayed/Instances/Family.lagda.md b/src/Cat/Displayed/Instances/Family.lagda.md index 49a6f5e77..811c1be5b 100644 --- a/src/Cat/Displayed/Instances/Family.lagda.md +++ b/src/Cat/Displayed/Instances/Family.lagda.md @@ -2,21 +2,20 @@ ```agda open import 1Lab.Path.IdentitySystem.Strict -open import Cat.Displayed.Base +open import Cat.Displayed.GenericObject open import Cat.Displayed.Cartesian open import Cat.Displayed.Cartesian -open import Cat.Displayed.Fibre -open import Cat.Displayed.GenericObject - -open import Cat.Functor.Base open import Cat.Functor.Equivalence -open import Cat.Gaunt +open import Cat.Functor.Properties open import Cat.Instances.Discrete open import Cat.Instances.Functor -open import Cat.Skeletal -open import Cat.Strict +open import Cat.Displayed.Fibre +open import Cat.Displayed.Base open import Cat.Univalent +open import Cat.Skeletal open import Cat.Prelude +open import Cat.Strict +open import Cat.Gaunt import Cat.Reasoning ``` diff --git a/src/Cat/Displayed/Instances/Lifting.lagda.md b/src/Cat/Displayed/Instances/Lifting.lagda.md index dfda25341..a5d805343 100644 --- a/src/Cat/Displayed/Instances/Lifting.lagda.md +++ b/src/Cat/Displayed/Instances/Lifting.lagda.md @@ -1,10 +1,10 @@ diff --git a/src/Cat/Functor/Adjoint/Compose.lagda.md b/src/Cat/Functor/Adjoint/Compose.lagda.md index 896f3f0e5..351562e3c 100644 --- a/src/Cat/Functor/Adjoint/Compose.lagda.md +++ b/src/Cat/Functor/Adjoint/Compose.lagda.md @@ -7,6 +7,7 @@ description: We compute the composite of two adjunctions. open import Cat.Functor.Adjoint open import Cat.Prelude +import Cat.Functor.Reasoning import Cat.Reasoning ``` --> @@ -46,10 +47,10 @@ private module A = Cat.Reasoning A module B = Cat.Reasoning B module C = Cat.Reasoning C - module F = Functor F - module G = Functor G - module L = Functor L - module R = Functor R + module F = Cat.Functor.Reasoning F + module G = Cat.Functor.Reasoning G + module L = Cat.Functor.Reasoning L + module R = Cat.Functor.Reasoning R open _⊣_ open _=>_ module LF = Functor (L F∘ F) @@ -62,38 +63,29 @@ LF⊣GR : (L F∘ F) ⊣ (G F∘ R) LF⊣GR .unit .η x = G.₁ (lr.unit.η _) A.∘ fg.unit.η _ LF⊣GR .counit .η x = lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _) -LF⊣GR .unit .is-natural x y f = path where abstract - path : LF⊣GR .unit .η y A.∘ f ≡ GR.₁ (LF.₁ f) A.∘ LF⊣GR .unit .η x - path = - (G.₁ (lr.unit.η _) A.∘ fg.unit.η _) A.∘ f ≡⟨ A.pullr (fg.unit.is-natural _ _ _) ⟩ - G.₁ (lr.unit.η _) A.∘ G.₁ (F.₁ f) A.∘ fg.unit.η _ ≡⟨ A.pulll (sym (G.F-∘ _ _)) ⟩ - G.₁ ⌜ lr.unit.η _ B.∘ F.₁ f ⌝ A.∘ fg.unit.η _ ≡⟨ ap! (lr.unit.is-natural _ _ _) ⟩ - G.₁ (R.₁ (L.₁ (F.₁ f)) B.∘ lr.unit .η _) A.∘ fg.unit.η _ ≡⟨ A.pushl (G.F-∘ _ _) ⟩ - GR.₁ (LF.₁ f) A.∘ G.₁ (lr.unit.η _) A.∘ (fg.unit.η _) ∎ +LF⊣GR .unit .is-natural x y f = + (G.₁ (lr.unit.η _) A.∘ fg.unit.η _) A.∘ f ≡⟨ A.pullr (fg.unit.is-natural _ _ _) ⟩ + G.₁ (lr.unit.η _) A.∘ G.₁ (F.₁ f) A.∘ fg.unit.η _ ≡⟨ A.pulll (sym (G.F-∘ _ _)) ⟩ + G.₁ ⌜ lr.unit.η _ B.∘ F.₁ f ⌝ A.∘ fg.unit.η _ ≡⟨ ap₂ A._∘_ (ap G.₁ (lr.unit.is-natural _ _ _)) refl ⟩ + G.₁ (R.₁ (L.₁ (F.₁ f)) B.∘ lr.unit .η _) A.∘ fg.unit.η _ ≡⟨ A.pushl (G.F-∘ _ _) ⟩ + GR.₁ (LF.₁ f) A.∘ G.₁ (lr.unit.η _) A.∘ (fg.unit.η _) ∎ -LF⊣GR .counit .is-natural x y f = path where abstract - path : LF⊣GR .counit .η y C.∘ LF.₁ (GR.₁ f) ≡ f C.∘ LF⊣GR .counit .η x - path = - (lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _)) C.∘ LF.₁ (GR.₁ f) ≡⟨ C.pullr (sym (L.F-∘ _ _)) ⟩ - lr.counit.ε _ C.∘ L.₁ ⌜ fg.counit.ε _ B.∘ F.₁ (GR.₁ f) ⌝ ≡⟨ ap! (fg.counit.is-natural _ _ _) ⟩ - lr.counit.ε _ C.∘ ⌜ L.₁ (R.F₁ f B.∘ fg.counit.ε _) ⌝ ≡⟨ ap! (L.F-∘ _ _) ⟩ - lr.counit.ε _ C.∘ L.₁ (R.F₁ f) C.∘ L.₁ (fg.counit.ε _) ≡⟨ C.extendl (lr.counit.is-natural _ _ _) ⟩ - f C.∘ lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _) ∎ +LF⊣GR .counit .is-natural x y f = + (lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _)) C.∘ LF.₁ (GR.₁ f) ≡⟨ C.pullr (sym (L.F-∘ _ _)) ⟩ + lr.counit.ε _ C.∘ L.₁ ⌜ fg.counit.ε _ B.∘ F.₁ (GR.₁ f) ⌝ ≡⟨ ap₂ C._∘_ refl (ap L.₁ (fg.counit.is-natural _ _ _)) ⟩ + lr.counit.ε _ C.∘ ⌜ L.₁ (R.F₁ f B.∘ fg.counit.ε _) ⌝ ≡⟨ ap₂ C._∘_ refl (L.F-∘ _ _) ⟩ + lr.counit.ε _ C.∘ L.₁ (R.F₁ f) C.∘ L.₁ (fg.counit.ε _) ≡⟨ C.extendl (lr.counit.is-natural _ _ _) ⟩ + f C.∘ lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _) ∎ LF⊣GR .zig = - (lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _)) C.∘ ⌜ LF.₁ (G.₁ (lr.unit.η _) A.∘ fg.unit.η _) ⌝ ≡⟨ ap! (LF.F-∘ _ _) ⟩ - (lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _)) C.∘ LF.₁ (G.₁ (lr.unit.η _)) C.∘ LF.₁ (fg.unit.η _) ≡⟨ cat! C ⟩ - lr.counit.ε _ C.∘ (⌜ L.₁ (fg.counit.ε _) C.∘ LF.₁ (G.₁ (lr.unit.η _)) ⌝ C.∘ LF.₁ (fg.unit.η _)) ≡⟨ ap! (sym (L.F-∘ _ _) ·· ap L.₁ (fg.counit.is-natural _ _ _) ·· L.F-∘ _ _) ⟩ - lr.counit.ε _ C.∘ (L.₁ (lr.unit.η _) C.∘ L.₁ (fg.counit.ε _)) C.∘ LF.₁ (fg.unit.η _) ≡⟨ cat! C ⟩ - (lr.counit.ε _ C.∘ L.₁ (lr.unit.η _)) C.∘ (L.₁ (fg.counit.ε _) C.∘ LF.₁ (fg.unit.η _)) ≡⟨ ap₂ C._∘_ lr.zig (sym (L.F-∘ _ _) ∙ ap L.₁ fg.zig ∙ L.F-id) ⟩ - C.id C.∘ C.id ≡⟨ C.eliml refl ⟩ - C.id ∎ + (lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _)) C.∘ ⌜ LF.₁ (G.₁ (lr.unit.η _) A.∘ fg.unit.η _) ⌝ ≡⟨ C.extendr (ap₂ C._∘_ refl (LF.F-∘ _ _) ∙ L.extendl (fg.counit.is-natural _ _ _)) ⟩ + (lr.counit.ε _ C.∘ L.₁ (lr.unit.η _)) C.∘ (L.₁ (fg.counit.ε _) C.∘ LF.₁ (fg.unit.η _)) ≡⟨ C.elimr (L.annihilate fg.zig) ⟩ + lr.counit.ε _ C.∘ L.₁ (lr.unit.η _) ≡⟨ lr.zig ⟩ + C.id ∎ LF⊣GR .zag = - GR.₁ (lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _)) A.∘ G.₁ (lr.unit.η _) A.∘ fg.unit .η _ ≡⟨ A.pulll (sym (G.F-∘ _ _)) ⟩ - G.₁ ⌜ R.₁ (lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _)) B.∘ lr.unit.η _ ⌝ A.∘ fg.unit .η _ ≡˘⟨ ap¡ (B.pulll (sym (R.F-∘ _ _))) ⟩ - G.₁ (R.₁ (lr.counit.ε _) B.∘ ⌜ R.₁ (L.₁ (fg.counit.ε _)) B.∘ lr.unit.η _ ⌝) A.∘ fg.unit .η _ ≡˘⟨ ap¡ (lr.unit.is-natural _ _ _) ⟩ - G.₁ (⌜ R.₁ (lr.counit.ε _) B.∘ lr.unit.η _ B.∘ fg.counit.ε _ ⌝) A.∘ fg.unit .η _ ≡⟨ ap! (B.cancell lr.zag) ⟩ - G.₁ (fg.counit.ε _) A.∘ fg.unit .η _ ≡⟨ fg.zag ⟩ - A.id ∎ + GR.₁ (lr.counit.ε _ C.∘ L.₁ (fg.counit.ε _)) A.∘ G.₁ (lr.unit.η _) A.∘ fg.unit .η _ ≡⟨ A.pulll (G.collapse (B.pushl (R.F-∘ _ _) ∙ ap₂ B._∘_ refl (sym (lr.unit.is-natural _ _ _)))) ⟩ + G.₁ (⌜ R.₁ (lr.counit.ε _) B.∘ lr.unit.η _ B.∘ fg.counit.ε _ ⌝) A.∘ fg.unit .η _ ≡⟨ ap₂ A._∘_ (ap G.₁ (B.cancell lr.zag)) refl ⟩ + G.₁ (fg.counit.ε _) A.∘ fg.unit .η _ ≡⟨ fg.zag ⟩ + A.id ∎ ``` diff --git a/src/Cat/Functor/Adjoint/Hom.lagda.md b/src/Cat/Functor/Adjoint/Hom.lagda.md index 618fba0c5..109337f4d 100644 --- a/src/Cat/Functor/Adjoint/Hom.lagda.md +++ b/src/Cat/Functor/Adjoint/Hom.lagda.md @@ -147,13 +147,13 @@ module _ {o ℓ o′} {C : Precategory o ℓ} {D : Precategory o′ ℓ} hom-natural-iso→adjoints - : natural-iso (Hom[-,-] C F∘ (Functor.op L F× Id)) (Hom[-,-] D F∘ (Id F× R)) + : (Hom[-,-] C F∘ (Functor.op L F× Id)) ≅ⁿ (Hom[-,-] D F∘ (Id F× R)) → L ⊣ R hom-natural-iso→adjoints eta = hom-iso→adjoints (to .η _) (natural-iso-to-is-equiv eta (_ , _)) λ g h x → happly (to .is-natural _ _ (h , g)) x where - open natural-iso eta + open Isoⁿ eta open _=>_ module _ {o ℓ o′} {C : Precategory o ℓ} {D : Precategory o′ ℓ} @@ -167,7 +167,7 @@ module _ {o ℓ o′} {C : Precategory o ℓ} {D : Precategory o′ ℓ} module R = Func R adjunct-hom-iso-from - : ∀ a → natural-iso (Hom-from C (L.₀ a)) (Hom-from D a F∘ R) + : ∀ a → (Hom-from C (L.₀ a)) ≅ⁿ (Hom-from D a F∘ R) adjunct-hom-iso-from a = to-natural-iso mi where open make-natural-iso @@ -179,7 +179,7 @@ module _ {o ℓ o′} {C : Precategory o ℓ} {D : Precategory o′ ℓ} mi .natural _ _ f = funext λ g → sym (L-adjunct-naturalr adj f g) adjunct-hom-iso-into - : ∀ b → natural-iso (Hom-into C b F∘ Functor.op L) (Hom-into D (R.₀ b)) + : ∀ b → (Hom-into C b F∘ Functor.op L) ≅ⁿ (Hom-into D (R.₀ b)) adjunct-hom-iso-into b = to-natural-iso mi where open make-natural-iso @@ -191,7 +191,7 @@ module _ {o ℓ o′} {C : Precategory o ℓ} {D : Precategory o′ ℓ} mi .natural _ _ f = funext λ g → sym $ L-adjunct-naturall adj g f adjunct-hom-iso - : natural-iso (Hom[-,-] C F∘ (Functor.op L F× Id)) (Hom[-,-] D F∘ (Id F× R)) + : (Hom[-,-] C F∘ (Functor.op L F× Id)) ≅ⁿ (Hom[-,-] D F∘ (Id F× R)) adjunct-hom-iso = to-natural-iso mi where open make-natural-iso diff --git a/src/Cat/Functor/Adjoint/Reflective.lagda.md b/src/Cat/Functor/Adjoint/Reflective.lagda.md index 71744af1b..d666377bd 100644 --- a/src/Cat/Functor/Adjoint/Reflective.lagda.md +++ b/src/Cat/Functor/Adjoint/Reflective.lagda.md @@ -10,10 +10,10 @@ description: | ```agda open import Cat.Functor.Adjoint.Monadic open import Cat.Functor.Equivalence +open import Cat.Functor.Properties open import Cat.Instances.Functor open import Cat.Functor.Adjoint open import Cat.Diagram.Monad -open import Cat.Functor.Base open import Cat.Prelude import Cat.Functor.Reasoning as Func @@ -44,7 +44,7 @@ all groups, or the inclusion $\Props \mono \Sets$) participate in an adjunction [full subcategory]: Cat.Functor.FullSubcategory.html -[fully faithful functors]: Cat.Functor.Base.html#ff-functors +[fully faithful functors]: Cat.Functor.Properties.html#ff-functors ~~~{.quiver .short-15} \[\begin{tikzcd} @@ -112,7 +112,7 @@ module is-reflective→counit-iso : (F F∘ G) DD.≅ Id is-reflective→counit-iso = DD.invertible→iso counit invs where - invs = componentwise-invertible→invertible counit λ x → + invs = invertible→invertibleⁿ counit λ x → D.iso→invertible (is-reflective→counit-is-iso {o = x}) ``` diff --git a/src/Cat/Functor/Adjoint/Unique.lagda.md b/src/Cat/Functor/Adjoint/Unique.lagda.md index 19f476f60..d597ede2f 100644 --- a/src/Cat/Functor/Adjoint/Unique.lagda.md +++ b/src/Cat/Functor/Adjoint/Unique.lagda.md @@ -1,7 +1,8 @@ @@ -9,47 +12,189 @@ import Cat.Reasoning module Cat.Functor.Base where ``` +# Functor precategories + +Fix a pair of (completely arbitrary!) precategories $\cC$ and $\cD$. +We'll show how to make the type of functors $\cC \to \cD$ into a +precategory on its own right, with the _natural transformations_ $F \To +G$ as the morphisms. First, given $F : \cC \to \cD$, we construct the +identity natural transformation by having every component be the +identity: + -# Functors +```agda + idnt : {F : Functor C D} → F => F + idnt .η _ = D.id + idnt .is-natural _ _ _ = D.id-comm-sym +``` -This module defines the most important clases of functors: Full, -faithful, fully faithful (abbreviated ff), _split_ essentially -surjective and ("_merely_") essentially surjective. +Moreover, if we have a pair of composable-looking natural +transformations $\alpha : G \To H$ and $\beta : F \To G$, then we can +indeed make their pointwise composite into a natural transformation: -A functor is **full** when its action on hom-sets is surjective: +```agda + _∘nt_ : ∀ {F G H : Functor C D} → G => H → F => G → F => H + (f ∘nt g) .η x = f .η x D.∘ g .η x + _∘nt_ {F} {G} {H} f g .is-natural x y h = + (f .η y D.∘ g .η y) D.∘ F .F₁ h ≡⟨ D.pullr (g .is-natural x y h) ⟩ + f .η y D.∘ G .F₁ h D.∘ g .η x ≡⟨ D.extendl (f .is-natural x y h) ⟩ + H .F₁ h D.∘ f .η x D.∘ g .η x ∎ + + infixr 40 _∘nt_ +``` + +Since we already know that identity of natural transformations is +determined by identity of the underlying family of morphisms, and the +identities and composition we've just defined are _componentwise_ just +identity and composition in $\cD$, then the category laws we have to +prove are, once again, those of $\cD$: ```agda -is-full : Functor C D → Type _ -is-full {C = C} {D = D} F = - ∀ {x y} (g : D .Hom (F₀ F x) (F₀ F y)) → ∃[ f ∈ C .Hom x y ] (F₁ F f ≡ g) +Cat[_,_] + : Precategory o ℓ → Precategory o₁ ℓ₁ + → Precategory (o ⊔ ℓ ⊔ o₁ ⊔ ℓ₁) (o ⊔ ℓ ⊔ ℓ₁) +Cat[ C , D ] .Pc.Ob = Functor C D +Cat[ C , D ] .Pc.Hom = _=>_ +Cat[ C , D ] .Pc.Hom-set F G = Nat-is-set + +Cat[ C , D ] .Pc.id = idnt +Cat[ C , D ] .Pc._∘_ = _∘nt_ + +Cat[ C , D ] .Pc.idr f = Nat-path λ x → Pc.idr D _ +Cat[ C , D ] .Pc.idl f = Nat-path λ x → Pc.idl D _ +Cat[ C , D ] .Pc.assoc f g h = Nat-path λ x → Pc.assoc D _ _ _ ``` -A functor is **faithful** when its action on hom-sets is injective: +We'll also need the following foundational tool, characterising paths +between functors. It says that, given a homotopy $p_0$ between the +object-parts of functors $F, G : \cC \to \cD$, and, over this, an +identification between the actions of $F$ and $G$ on morphisms, we can +construct a path $F \equiv G$. + +## Paths between functors ```agda -is-faithful : Functor C D → Type _ -is-faithful F = ∀ {x y} → injective (F₁ F {x = x} {y}) +Functor-path + : {F G : Functor C D} + → (p0 : ∀ x → F₀ F x ≡ F₀ G x) + → (p1 : ∀ {x y} (f : C .Pc.Hom x y) + → PathP (λ i → D .Pc.Hom (p0 x i) (p0 y i)) (F .F₁ f) (G .F₁ f)) + → F ≡ G ``` +Note that this lemma is a bit unusual: we're characterising the identity +type of the _objects_ of a precategory, rather than, as is more common, +the _morphisms_ of a precategory. However, this characterisation will +let us swiftly establish necessary conditions for [univalence of functor +categories]. + +[univalence of functor categories]: Cat.Functor.Univalence.html + + +## Action on isomorphisms + + + +We have also to make note of the following fact: absolutely all functors +preserve isomorphisms, and, more generally, preserve invertibility. +```agda F-map-iso : ∀ {x y} (F : Functor C D) → x C.≅ y → F₀ F x D.≅ F₀ F y F-map-iso F x .to = F .F₁ (x .to) F-map-iso F x .from = F .F₁ (x .from) @@ -65,183 +210,37 @@ module _ {C : Precategory o h} {D : Precategory o₁ h₁} where (sym (F-∘ F _ _) ·· ap (F₁ F) x.invl ·· F-id F) (sym (F-∘ F _ _) ·· ap (F₁ F) x.invr ·· F-id F) where module x = C.is-invertible inv - - faithful→iso-fibre-prop - : ∀ (F : Functor C D) - → is-faithful F - → ∀ {x y} → (f : F₀ F x D.≅ F₀ F y) - → is-prop (Σ[ g ∈ x C.≅ y ] (F-map-iso F g ≡ f)) - faithful→iso-fibre-prop F faithful f (g , p) (g' , q) = - Σ-prop-path (λ _ → D.≅-is-set _ _) $ - C.≅-pathp refl refl (faithful (ap D.to (p ∙ sym q))) -``` ---> - -## ff Functors - -A functor is **fully faithful** (abbreviated **ff**) when its action on -hom-sets is an equivalence. Since Hom-sets are sets, it suffices for the -functor to be full and faithful; Rather than taking this conjunction as -a definition, we use the more directly useful data as a definition and -prove the conjunction as a theorem. - -```agda -is-fully-faithful : Functor C D → Type _ -is-fully-faithful F = ∀ {x y} → is-equiv (F₁ F {x = x} {y}) - -fully-faithful→faithful : {F : Functor C D} → is-fully-faithful F → is-faithful F -fully-faithful→faithful {F = F} ff {_} {_} {x} {y} p = - x ≡⟨ sym (equiv→unit ff x) ⟩ - equiv→inverse ff (F₁ F x) ≡⟨ ap (equiv→inverse ff) p ⟩ - equiv→inverse ff (F₁ F y) ≡⟨ equiv→unit ff y ⟩ - y ∎ - -fully-faithful→full : {F : Functor C D} → is-fully-faithful F → is-full F -fully-faithful→full {F = F} ff g = inc (equiv→inverse ff g , equiv→counit ff g) - -full+faithful→ff - : (F : Functor C D) → is-full F → is-faithful F → is-fully-faithful F -full+faithful→ff {C = C} {D = D} F surj inj .is-eqv = p where - img-is-prop : ∀ {x y} f → is-prop (fibre (F₁ F {x = x} {y}) f) - img-is-prop f (g , p) (h , q) = Σ-prop-path (λ _ → D .Hom-set _ _ _ _) (inj (p ∙ sym q)) - - p : ∀ {x y} f → is-contr (fibre (F₁ F {x = x} {y}) f) - p f .centre = ∥-∥-elim (λ _ → img-is-prop f) (λ x → x) (surj f) - p f .paths = img-is-prop f _ -``` - -A very important property of fully faithful functors (like $F$) is that -they are **conservative**: If the image of $f : x \to y$ under $F$ is an -isomorphism $Fx \cong Fy$, then $f$ was really an isomorphism $f : x -\cong y$. - -```agda -module _ {C : Precategory o h} {D : Precategory o₁ h₁} where - private - module C = Precategory C - module D = Precategory D - - import Cat.Morphism C as Cm - import Cat.Morphism D as Dm - - is-ff→is-conservative - : {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 - open Cm.is-invertible - open Cm.Inverses -``` - -Since the functor is ff, we can find a map "$F_1^{-1}(f) : y \to x$" in -the domain category to serve as an inverse for $f$: - -```agda - g : C.Hom _ _ - g = equiv→inverse ff (isinv .Dm.is-invertible.inv) - module ff {a} {b} = Equiv (_ , ff {a} {b}) - - Ffog = - F₁ F (f C.∘ g) ≡⟨ F-∘ F _ _ ⟩ - F₁ F f D.∘ F₁ F g ≡⟨ ap₂ D._∘_ refl (ff.ε _) ∙ isinv .Dm.is-invertible.invl ⟩ - D.id ∎ - - Fgof = - F₁ F (g C.∘ f) ≡⟨ F-∘ F _ _ ⟩ - F₁ F g D.∘ F₁ F f ≡⟨ ap₂ D._∘_ (ff.ε _) refl ∙ isinv .Dm.is-invertible.invr ⟩ - D.id ∎ - - i : Cm.is-invertible _ - i .inv = g - i .inverses .invl = - f C.∘ g ≡⟨ sym (ff.η _) ⟩ - ff.from ⌜ F₁ F (f C.∘ g) ⌝ ≡⟨ ap! (Ffog ∙ sym (F-id F)) ⟩ - ff.from (F₁ F C.id) ≡⟨ ff.η _ ⟩ - C.id ∎ - i .inverses .invr = - g C.∘ f ≡⟨ sym (ff.η _) ⟩ - ff.from ⌜ F₁ F (g C.∘ f) ⌝ ≡⟨ ap! (Fgof ∙ sym (F-id F)) ⟩ - ff.from (F₁ F C.id) ≡⟨ ff.η _ ⟩ - C.id ∎ - - is-ff→essentially-injective - : {F : Functor C D} → is-fully-faithful F - → ∀ {X Y} → F₀ F X Dm.≅ F₀ F Y - → X Cm.≅ Y - is-ff→essentially-injective {F = F} ff im = im′ where - -- Cm.make-iso (equiv→inverse ff to) inv invl invr - open Dm._≅_ im using (to ; from ; inverses) - D-inv′ : Dm.is-invertible (F₁ F (equiv→inverse ff to)) - D-inv′ .Dm.is-invertible.inv = from - 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′) - - im′ : _ Cm.≅ _ - im′ .to = equiv→inverse ff to - im′ .from = inv - im′ .inverses .Cm.Inverses.invl = invl - im′ .inverses .Cm.Inverses.invr = invr -``` - -## Essential Fibres - -The **essential fibre** of a functor $F : C \to D$ over an object $y : -D$ is the space of objects of $C$ which $F$ takes, up to isomorphism, to -$y$. - -```agda -Essential-fibre : Functor C D → D .Ob → Type _ -Essential-fibre {D = D} F y = Σ[ x ∈ _ ] (F₀ F x ≅ y) - where open import Cat.Morphism D ``` -A functor is **split essentially surjective** (abbreviated **split -eso**) if there is a procedure for finding points in the essential fibre -over any object. It's **essentially surjective** if the this procedure -_merely_, i.e. truncatedly, finds a point: +If the categories the functor maps between are univalent, there is a +competing notion of preserving isomorphisms: the action on paths of the +object-part of the functor. We first turn the isomorphism into a path +(using univalence of the domain), run it through the functor, then turn +the resulting path back into an isomorphism. Fortunately, functors are +already coherent enough to ensure that these actions agree: ```agda -is-split-eso : Functor C D → Type _ -is-split-eso F = ∀ y → Essential-fibre F y - -is-eso : Functor C D → Type _ -is-eso F = ∀ y → ∥ Essential-fibre F y ∥ + F-map-path + : (ccat : is-category C) (dcat : is-category D) + → ∀ (F : Functor C D) {x y} (i : x C.≅ y) + → ap (F₀ F) (Univalent.iso→path ccat i) ≡ Univalent.iso→path dcat (F-map-iso F i) + F-map-path ccat dcat F {x} = Univalent.J-iso ccat P pr where + P : (b : C.Ob) → C.Isomorphism x b → Type _ + P b im = ap (F₀ F) (Univalent.iso→path ccat im) + ≡ Univalent.iso→path dcat (F-map-iso F im) + + pr : P x C.id-iso + pr = + ap (F₀ F) (Univalent.iso→path ccat C.id-iso) ≡⟨ ap (ap (F₀ F)) (Univalent.iso→path-id ccat) ⟩ + ap (F₀ F) refl ≡˘⟨ Univalent.iso→path-id dcat ⟩ + dcat .to-path D.id-iso ≡⟨ ap (dcat .to-path) (D.≅-path (sym (F .F-id))) ⟩ + dcat .to-path (F-map-iso F C.id-iso) ∎ ``` -## Pseudomonic Functors +# Presheaf precategories -A functor is **pseudomonic** if it is faithful and full on isomorphisms. -Pseudomonic functors are arguably the correct notion of subcategory, as -they ensure that we are not able to distinguish between isomorphic objects -when creating a subcategory. +Of principal importance among the functor categories are those to the +category $\Sets$: these are the _presheaf categories_. - - -```agda - is-full-on-isos : Functor C D → Type (o ⊔ h ⊔ h₁) - is-full-on-isos F = - ∀ {x y} → (f : (F .F₀ x) D.≅ (F .F₀ y)) → ∃[ g ∈ x C.≅ y ] (F-map-iso F g ≡ f) - - record is-pseudomonic (F : Functor C D) : Type (o ⊔ h ⊔ h₁) where - no-eta-equality - field - faithful : is-faithful F - isos-full : is-full-on-isos F - - open is-pseudomonic -``` - -Somewhat surprisingly, pseudomonic functors are [conservative]. -As $F$ is full on isos, there merely exists some iso $g$ in the fibre -of $f$. However, Invertability is a property of morphisms, so we can -untruncate the mere existence. Once we have our hands on the isomorphism, -we perform a simple calculation to note that it yields an inverse to $f$. - -[conservative]: Cat.Functor.Conservative.html - -```agda - pseudomonic→conservative - : ∀ {F : Functor C D} - → is-pseudomonic F - → ∀ {x y} (f : C.Hom x y) → D.is-invertible (F₁ F f) - → C.is-invertible f - pseudomonic→conservative {F = F} pseudo {x} {y} f inv = - ∥-∥-rec C.is-invertible-is-prop - (λ (g , p) → - C.make-invertible (C.from g) - (sym (ap (C._∘ _) (pseudo .faithful (ap D.to p))) ∙ C.invl g) - (sym (ap (_ C.∘_) (pseudo .faithful (ap D.to p))) ∙ C.invr g)) - (pseudo .isos-full (D.invertible→iso _ inv)) -``` - -In a similar vein, pseudomonic functors are essentially injective. -The proof follows a similar path to the prior one, hinging on the -fact that faithful functors are an embedding on isos. - -```agda - pseudomonic→essentially-injective - : ∀ {F : Functor C D} - → is-pseudomonic F - → ∀ {x y} → F₀ F x D.≅ F₀ F y - → x C.≅ y - pseudomonic→essentially-injective {F = F} pseudo f = - ∥-∥-rec (faithful→iso-fibre-prop F (pseudo .faithful) f) - (λ x → x) - (pseudo .isos-full f) .fst -``` - -Fully faithful functors are pseudomonic, as they are faithful and -essentially injective. - -```agda - ff→pseudomonic - : ∀ {F : Functor C D} - → is-fully-faithful F - → is-pseudomonic F - ff→pseudomonic {F} ff .faithful = fully-faithful→faithful {F = F} ff - ff→pseudomonic {F} ff .isos-full f = - inc (is-ff→essentially-injective {F = F} ff f , - D.≅-pathp refl refl (equiv→counit ff (D.to f))) -``` - -## Equivalence on Objects Functors - -A functor $F : \cC \to \cD$ is an **equivalence on objects** if its action -on objects is an equivalence. - -```agda -is-equiv-on-objects : (F : Functor C D) → Type _ -is-equiv-on-objects F = is-equiv (F .F₀) -``` - -If $F$ is an equivalence-on-objects functor, then it is (split) -essentially surjective. - -```agda -equiv-on-objects→split-eso - : ∀ (F : Functor C D) → is-equiv-on-objects F → is-split-eso F -equiv-on-objects→split-eso {D = D} F eqv y = - equiv→inverse eqv y , path→iso (equiv→counit eqv y) - -equiv-on-objects→eso : ∀ (F : Functor C D) → is-equiv-on-objects F → is-eso F -equiv-on-objects→eso F eqv y = inc (equiv-on-objects→split-eso F eqv y) +PSh : ∀ κ {o ℓ} → Precategory o ℓ → Precategory _ _ +PSh κ C = Cat[ C ^op , Sets κ ] ``` diff --git a/src/Cat/Functor/Closed.lagda.md b/src/Cat/Functor/Closed.lagda.md new file mode 100644 index 000000000..be67bdeb3 --- /dev/null +++ b/src/Cat/Functor/Closed.lagda.md @@ -0,0 +1,101 @@ + + +```agda +module Cat.Functor.Closed where +``` + + + +When taken as a [(bi)category][cat], the collection of (pre)categories +is, in a suitably weak sense, [Cartesian closed]: there is an +[equivalence] between the [functor categories] $[\cC \times \cD, \cE]$ +and $[\cC, [\cD, \cE]]$. We do not define the full equivalence here, +leaving the natural isomorphisms aside and focusing on the inverse +functors themselves: `Curry`{.Agda} and `Uncurry`{.Agda}. + +[cat]: Cat.Bi.Base.html#the-bicategory-of-categories +[Cartesian closed]: Cat.CartesianClosed.Base.html +[equivalence]: Cat.Functor.Equivalence.html +[functor categories]: Cat.Functor.Base.html + +The two conversion functions act on objects essentially in the same way +as currying and uncurrying behave on funct*ions*: the difference is that +we must properly stage the action on morphisms. Currying a functor $F : +\cC \times \cD \to \cE$ fixes a morphism $f : x \to y \in \cC$, and we +must show that $g \mapsto F(f,g)$ is natural in $g$. It follows from a +bit of calculation using the functoriality of $F$. + +```agda +Curry : Functor (C ×ᶜ D) E → Functor C Cat[ D , E ] +Curry {C = C} {D = D} {E = E} F = curried where + open import Cat.Functor.Bifunctor {C = C} {D = D} {E = E} F + + curried : Functor C Cat[ D , E ] + curried .F₀ = Right + curried .F₁ x→y = NT (λ f → first x→y) λ x y f → + sym (F-∘ F _ _) + ·· ap (F₁ F) (Σ-pathp (C .idr _ ∙ sym (C .idl _)) (D .idl _ ∙ sym (D .idr _))) + ·· F-∘ F _ _ + curried .F-id = Nat-path λ x → F-id F + curried .F-∘ f g = Nat-path λ x → + ap (λ x → F₁ F (_ , x)) (sym (D .idl _)) ∙ F-∘ F _ _ + +Uncurry : Functor C Cat[ D , E ] → Functor (C ×ᶜ D) E +Uncurry {C = C} {D = D} {E = E} F = uncurried where + import Cat.Reasoning C as C + import Cat.Reasoning D as D + import Cat.Reasoning E as E + module F = Functor F + + uncurried : Functor (C ×ᶜ D) E + uncurried .F₀ (c , d) = F₀ (F.₀ c) d + uncurried .F₁ (f , g) = F.₁ f .η _ E.∘ F₁ (F.₀ _) g +``` + +The other direction must do slightly more calculation: Given a functor +into functor-categories, and a pair of arguments, we must apply it +twice: but at the level of morphisms, this involves composition in the +codomain category, which throws a fair bit of complication into the +functoriality constraints. + +```agda + uncurried .F-id {x = x , y} = path where abstract + path : E ._∘_ (F.₁ (C .id) .η y) (F₁ (F.₀ x) (D .id)) ≡ E .id + path = + F.₁ C.id .η y E.∘ F₁ (F.₀ x) D.id ≡⟨ E.elimr (F-id (F.₀ x)) ⟩ + F.₁ C.id .η y ≡⟨ (λ i → F.F-id i .η y) ⟩ + E.id ∎ + + uncurried .F-∘ (f , g) (f′ , g′) = path where abstract + path : uncurried .F₁ (f C.∘ f′ , g D.∘ g′) + ≡ uncurried .F₁ (f , g) E.∘ uncurried .F₁ (f′ , g′) + path = + F.₁ (f C.∘ f′) .η _ E.∘ F₁ (F.₀ _) (g D.∘ g′) ≡˘⟨ E.pulll (λ i → F.F-∘ f f′ (~ i) .η _) ⟩ + F.₁ f .η _ E.∘ F.₁ f′ .η _ E.∘ ⌜ F₁ (F.₀ _) (g D.∘ g′) ⌝ ≡⟨ ap! (F-∘ (F.₀ _) _ _) ⟩ + F.₁ f .η _ E.∘ F.₁ f′ .η _ E.∘ F₁ (F.₀ _) g E.∘ F₁ (F.₀ _) g′ ≡⟨ cat! E ⟩ + F.₁ f .η _ E.∘ ⌜ F.₁ f′ .η _ E.∘ F₁ (F.₀ _) g ⌝ E.∘ F₁ (F.₀ _) g′ ≡⟨ ap! (F.₁ f′ .is-natural _ _ _) ⟩ + F.₁ f .η _ E.∘ (F₁ (F.₀ _) g E.∘ F.₁ f′ .η _) E.∘ F₁ (F.₀ _) g′ ≡⟨ cat! E ⟩ + ((F.₁ f .η _ E.∘ F₁ (F.₀ _) g) E.∘ (F.₁ f′ .η _ E.∘ F₁ (F.₀ _) g′)) ∎ +``` diff --git a/src/Cat/Functor/Coherence.agda b/src/Cat/Functor/Coherence.agda index 447d5393f..f2e14d3ea 100644 --- a/src/Cat/Functor/Coherence.agda +++ b/src/Cat/Functor/Coherence.agda @@ -2,11 +2,12 @@ open import 1Lab.Reflection open import Cat.Prelude -import Cat.Instances.Functor.Compose +import Cat.Functor.Compose module Cat.Functor.Coherence where -open Cat.Instances.Functor.Compose public +open Cat.Functor.Compose public + private variable o ℓ : Level diff --git a/src/Cat/Instances/Functor/Compose.lagda.md b/src/Cat/Functor/Compose.lagda.md similarity index 81% rename from src/Cat/Instances/Functor/Compose.lagda.md rename to src/Cat/Functor/Compose.lagda.md index e792103a7..4184ca2c3 100644 --- a/src/Cat/Instances/Functor/Compose.lagda.md +++ b/src/Cat/Functor/Compose.lagda.md @@ -1,7 +1,8 @@ ```agda -module Cat.Instances.Functor.Compose where +module Cat.Functor.Compose where ``` # Functoriality of functor composition @@ -140,17 +141,15 @@ module _ {F G : Functor C D} where open Cat.Morphism open Fr - _◂ni_ : natural-iso F G → (H : Functor B C) → natural-iso (F F∘ H) (G F∘ H) - (α ◂ni H) = - make-iso _ (α .to ◂ H) (α .from ◂ H) - (Nat-path λ _ → α .invl ηₚ _) - (Nat-path λ _ → α .invr ηₚ _) - - _▸ni_ : (H : Functor D E) → natural-iso F G → natural-iso (H F∘ F) (H F∘ G) - (H ▸ni α) = - make-iso _ (H ▸ α .to) (H ▸ α .from) - (Nat-path λ _ → annihilate H (α .invl ηₚ _)) - (Nat-path λ _ → annihilate H (α .invr ηₚ _)) + _◂ni_ : F ≅ⁿ G → (H : Functor B C) → (F F∘ H) ≅ⁿ (G F∘ H) + (α ◂ni H) = make-iso _ (α .to ◂ H) (α .from ◂ H) + (Nat-path λ _ → α .invl ηₚ _) + (Nat-path λ _ → α .invr ηₚ _) + + _▸ni_ : (H : Functor D E) → F ≅ⁿ G → (H F∘ F) ≅ⁿ (H F∘ G) + (H ▸ni α) = make-iso _ (H ▸ α .to) (H ▸ α .from) + (Nat-path λ _ → annihilate H (α .invl ηₚ _)) + (Nat-path λ _ → annihilate H (α .invr ηₚ _)) ``` --> @@ -161,5 +160,19 @@ module _ {F G : Functor C D} where ▸-distribr : F ▸ (α ∘nt β) ≡ (F ▸ α) ∘nt (F ▸ β) ▸-distribr {F = F} = Nat-path λ _ → F .F-∘ _ _ + +module _ where + open Cat.Reasoning + + -- [TODO: Reed M, 14/03/2023] Extend the coherence machinery to handle natural + -- isos. + ni-assoc : {F : Functor D E} {G : Functor C D} {H : Functor B C} + → (F F∘ G F∘ H) ≅ⁿ ((F F∘ G) F∘ H) + ni-assoc {E = E} = to-natural-iso λ where + .make-natural-iso.eta _ → E .id + .make-natural-iso.inv _ → E .id + .make-natural-iso.eta∘inv _ → E .idl _ + .make-natural-iso.inv∘eta _ → E .idl _ + .make-natural-iso.natural _ _ _ → E .idr _ ∙ sym (E .idl _) ``` --> diff --git a/src/Cat/Functor/Dense.lagda.md b/src/Cat/Functor/Dense.lagda.md index 31434101c..5153ca465 100644 --- a/src/Cat/Functor/Dense.lagda.md +++ b/src/Cat/Functor/Dense.lagda.md @@ -2,9 +2,9 @@ ```agda open import Cat.Instances.Shape.Terminal open import Cat.Diagram.Colimit.Base +open import Cat.Functor.Properties open import Cat.Functor.Kan.Nerve open import Cat.Instances.Comma -open import Cat.Functor.Base open import Cat.Prelude import Cat.Functor.Reasoning as Fr diff --git a/src/Cat/Functor/Equivalence.lagda.md b/src/Cat/Functor/Equivalence.lagda.md index b1c05f18b..0c466e736 100644 --- a/src/Cat/Functor/Equivalence.lagda.md +++ b/src/Cat/Functor/Equivalence.lagda.md @@ -1,7 +1,8 @@ ```agda -open import Cat.Instances.Functor -open import Cat.Functor.Adjoint open import Cat.Functor.Adjoint.Compose +open import Cat.Functor.Naturality +open import Cat.Functor.Properties +open import Cat.Functor.Adjoint open import Cat.Functor.Base open import Cat.Univalent open import Cat.Prelude @@ -31,7 +32,7 @@ immediately implies that our adjoint pair $F \dashv G$ extends to an adjoint triple $F \dashv G \dashv F$. [right adjoint]: Cat.Functor.Adjoint.html -[natural isomorphisms]: Cat.Instances.Functor.html#functor-categories +[natural isomorphisms]: Cat.Functor.Naturality.html ```agda record is-equivalence (F : Functor C D) : Type (adj-level C D) where @@ -59,12 +60,12 @@ morphisms gives isomorphisms in the respective functor categories: F∘F⁻¹≅Id : (F F∘ F⁻¹) [D,D].≅ Id F∘F⁻¹≅Id = [D,D].invertible→iso counit - (componentwise-invertible→invertible _ counit-iso) + (invertible→invertibleⁿ _ counit-iso) Id≅F⁻¹∘F : Id [C,C].≅ (F⁻¹ F∘ F) Id≅F⁻¹∘F = [C,C].invertible→iso unit - (componentwise-invertible→invertible _ unit-iso) + (invertible→invertibleⁿ _ unit-iso) unit⁻¹ = [C,C]._≅_.from Id≅F⁻¹∘F counit⁻¹ = [D,D]._≅_.from F∘F⁻¹≅Id @@ -127,8 +128,8 @@ picking out an essential fibre over any object $d : \cD$: an object $F^*(d) : \cC$ together with a specified isomorphism $F^*(d) \cong d$. -[ff]: Cat.Functor.Base.html#ff-functors -[eso]: Cat.Functor.Base.html#essential-fibres +[ff]: Cat.Functor.Properties.html#ff-functors +[eso]: Cat.Functor.Properties.html#essential-fibres ```agda module _ {F : Functor C D} (ff : is-fully-faithful F) (eso : is-split-eso F) where @@ -402,7 +403,7 @@ between univalent categories has propositional [essential fibres], so a _both_ the domain _and_ codomain have to be categories for the argument to go through. -[essential fibres]: Cat.Functor.Base.html#essential-fibres +[essential fibres]: Cat.Functor.Properties.html#essential-fibres ```agda module @@ -474,7 +475,7 @@ _are_ indeed the same path: abstract square : ap (F₀ F) x≡y ≡ Fx≡Fy square = - ap (F₀ F) x≡y ≡⟨ F-map-path F x≅y ccat dcat ⟩ + ap (F₀ F) x≡y ≡⟨ F-map-path ccat dcat F x≅y ⟩ dcat .to-path ⌜ F-map-iso F x≅y ⌝ ≡⟨ ap! (equiv→counit (is-ff→F-map-iso-is-equiv {F = F} ff) _) ⟩ dcat .to-path Fx≅Fy ∎ @@ -780,12 +781,12 @@ As a corollary, equivalences preserve all families over hom sets. ``` --> -Equivalences are also invariant under natural isomorphisms. +Being an equivalence is also invariant under natural isomorphism. ```agda is-equivalence-natural-iso : ∀ {F G : Functor C D} - → natural-iso F G + → F ≅ⁿ G → is-equivalence F → is-equivalence G is-equivalence-natural-iso {C = C} {D = D} {F = F} {G = G} α F-eqv = G-eqv where open is-equivalence @@ -798,7 +799,7 @@ is-equivalence-natural-iso {C = C} {D = D} {F = F} {G = G} α F-eqv = G-eqv wher G-eqv .unit-iso x = C.invertible-∘ (C.invertible-∘ - (F-map-invertible (F-eqv .F⁻¹) (natural-iso→invertible α x)) + (F-map-invertible (F-eqv .F⁻¹) (isoⁿ→is-invertible α x)) C.id-invertible) (F-eqv .unit-iso x) G-eqv .counit-iso x = @@ -806,7 +807,7 @@ is-equivalence-natural-iso {C = C} {D = D} {F = F} {G = G} α F-eqv = G-eqv wher (F-eqv .counit-iso x) (D.invertible-∘ (F-map-invertible F C.id-invertible) - (natural-iso→invertible α _ D.invertible⁻¹)) + (isoⁿ→is-invertible α _ D.invertible⁻¹)) ``` Equivalences are invertible. diff --git a/src/Cat/Functor/Equivalence/Path.lagda.md b/src/Cat/Functor/Equivalence/Path.lagda.md index 10fdc9873..84a960678 100644 --- a/src/Cat/Functor/Equivalence/Path.lagda.md +++ b/src/Cat/Functor/Equivalence/Path.lagda.md @@ -317,6 +317,6 @@ necessary paths for showing that $F_0$ is an equivalence of types. eqv→iso .has-is-ff = is-equivalence→is-ff F eqv eqv→iso .has-is-iso = is-iso→is-equiv λ where .is-iso.inv → eqv .F⁻¹ .F₀ - .is-iso.rinv x → dcat .to-path $ Nat-iso→Iso (F∘F⁻¹≅Id eqv) _ - .is-iso.linv x → sym $ ccat .to-path $ Nat-iso→Iso (Id≅F⁻¹∘F eqv) _ + .is-iso.rinv x → dcat .to-path $ isoⁿ→iso (F∘F⁻¹≅Id eqv) _ + .is-iso.linv x → sym $ ccat .to-path $ isoⁿ→iso (Id≅F⁻¹∘F eqv) _ ``` diff --git a/src/Cat/Functor/Everything.agda b/src/Cat/Functor/Everything.agda deleted file mode 100644 index 45f19e588..000000000 --- a/src/Cat/Functor/Everything.agda +++ /dev/null @@ -1,25 +0,0 @@ -module Cat.Functor.Everything where -open import Cat.Functor.Adjoint.Compose public -open import Cat.Functor.Adjoint.Continuous public -open import Cat.Functor.Adjoint.Hom public -open import Cat.Functor.Adjoint public -open import Cat.Functor.Adjoint.Monadic public -open import Cat.Functor.Adjoint.Monad public -open import Cat.Functor.Adjoint.Reflective public -open import Cat.Functor.Monadic.Beck public -open import Cat.Functor.Monadic.Crude public -open import Cat.Functor.Amnestic public -open import Cat.Functor.Base public -open import Cat.Functor.Conservative public -open import Cat.Functor.Equivalence.Complete public -open import Cat.Functor.Equivalence public -open import Cat.Functor.FullSubcategory public -open import Cat.Functor.Hom public -open import Cat.Functor.Hom.Cocompletion public -open import Cat.Functor.Hom.Coyoneda public -open import Cat.Functor.Hom.Representable public -open import Cat.Functor.Kan.Base public -open import Cat.Functor.Kan.Nerve public -open import Cat.Functor.Kan.Pointwise public -open import Cat.Functor.Pullback public -open import Cat.Functor.Slice public diff --git a/src/Cat/Functor/FullSubcategory.lagda.md b/src/Cat/Functor/FullSubcategory.lagda.md index 97831c74c..dbda716e1 100644 --- a/src/Cat/Functor/FullSubcategory.lagda.md +++ b/src/Cat/Functor/FullSubcategory.lagda.md @@ -1,6 +1,6 @@ diff --git a/src/Cat/Functor/Kan/Base.lagda.md b/src/Cat/Functor/Kan/Base.lagda.md index 3dbace04d..2fb71deaa 100644 --- a/src/Cat/Functor/Kan/Base.lagda.md +++ b/src/Cat/Functor/Kan/Base.lagda.md @@ -1,9 +1,9 @@ @@ -77,7 +78,7 @@ left Kan extension of $F$ along $p$. ```agda represents→is-lan : (eta : F => G F∘ p) - → is-natural-invertible (Hom-from-precompose eta) + → is-invertibleⁿ (Hom-from-precompose eta) → is-lan p F G eta represents→is-lan eta nat-inv = lan where ``` @@ -89,7 +90,7 @@ factorization/uniqueness follow directly from the fact that we have a natural isomorphism. ```agda - module nat-inv = is-natural-invertible nat-inv + module nat-inv = is-invertibleⁿ nat-inv lan : is-lan p F G eta lan .σ {M} α = nat-inv.inv .η M α @@ -105,9 +106,9 @@ exercise in moving data around. is-lan→represents : {eta : F => G F∘ p} → is-lan p F G eta - → is-natural-invertible (Hom-from-precompose eta) + → is-invertibleⁿ (Hom-from-precompose eta) is-lan→represents {eta} lan = - to-is-natural-invertible inv + to-is-invertibleⁿ inv (λ M → funext λ α → lan .σ-comm) (λ M → funext λ α → lan .σ-uniq refl) where @@ -135,7 +136,7 @@ module _ open Lan open is-lan open Corepresentation - open natural-iso + open Isoⁿ ``` --> @@ -143,14 +144,14 @@ module _ lan→represents : Lan p F → Corepresentation (Hom-from Cat[ C , D ] F F∘ precompose p) lan→represents lan .corep = lan .Ext lan→represents lan .corepresents = - (is-natural-invertible→natural-iso (is-lan→represents (lan .has-lan))) ni⁻¹ + (is-invertibleⁿ→isoⁿ (is-lan→represents (lan .has-lan))) ni⁻¹ represents→lan : Corepresentation (Hom-from Cat[ C , D ] F F∘ precompose p) → Lan p F represents→lan has-corep .Ext = has-corep .corep represents→lan has-corep .eta = has-corep .corepresents .from .η _ idnt represents→lan has-corep .has-lan = represents→is-lan (Corep.to has-corep idnt) $ - to-is-natural-invertible (has-corep .corepresents .to) + to-is-invertibleⁿ (has-corep .corepresents .to) (λ M → funext λ α → (Corep.from has-corep α ◂ p) ∘nt Corep.to has-corep idnt ≡˘⟨ has-corep .corepresents .from .is-natural _ _ _ $ₚ idnt ⟩ Corep.to has-corep (Corep.from has-corep α ∘nt idnt) ≡⟨ ap (Corep.to has-corep) ([C',D].idr _) ⟩ diff --git a/src/Cat/Functor/Kan/Unique.lagda.md b/src/Cat/Functor/Kan/Unique.lagda.md index b9e7dd7cf..8aa693f9e 100644 --- a/src/Cat/Functor/Kan/Unique.lagda.md +++ b/src/Cat/Functor/Kan/Unique.lagda.md @@ -1,8 +1,10 @@ @@ -169,7 +171,7 @@ left extension of $F$ along $p$. ```agda is-invertible→is-lan : ∀ {G' : Functor C′ D} {eta' : F => G' F∘ p} - → is-natural-invertible (lan.σ eta') + → is-invertibleⁿ (lan.σ eta') → is-lan p F G' eta' is-invertible→is-lan {G' = G'} {eta'} invert = lan' where open is-lan @@ -192,11 +194,11 @@ left extension of $F$ along $p$. ```agda natural-iso-of→is-lan : {F' : Functor C D} - → (isos : natural-iso F F') - → is-lan p F' G (eta ∘nt natural-iso.from isos) + → (isos : F ≅ⁿ F') + → is-lan p F' G (eta ∘nt Isoⁿ.from isos) natural-iso-of→is-lan {F' = F'} isos = lan' where open is-lan - module isos = natural-iso isos + module isos = Isoⁿ isos lan' : is-lan p F' G (eta ∘nt isos.from) lan' .σ α = lan.σ (α ∘nt isos.to) @@ -212,11 +214,11 @@ left extension of $F$ along $p$. natural-iso-ext→is-lan : {G' : Functor C′ D} - → (isos : natural-iso G G') - → is-lan p F G' ((natural-iso.to isos ◂ p) ∘nt eta) + → (isos : G ≅ⁿ G') + → is-lan p F G' ((Isoⁿ.to isos ◂ p) ∘nt eta) natural-iso-ext→is-lan {G' = G'} isos = lan' where open is-lan - module isos = natural-iso isos + module isos = Isoⁿ isos lan' : is-lan p F G' ((isos.to ◂ p) ∘nt eta) lan' .σ α = lan.σ α ∘nt isos.from @@ -231,14 +233,14 @@ left extension of $F$ along $p$. natural-iso-along→is-lan : {p' : Functor C C′} - → (isos : natural-iso p p') - → is-lan p' F G ((G ▸ natural-iso.to isos) ∘nt eta) + → (isos : p ≅ⁿ p') + → is-lan p' F G ((G ▸ Isoⁿ.to isos) ∘nt eta) natural-iso-along→is-lan {p'} isos = lan' where open is-lan - module isos = natural-iso isos + module isos = Isoⁿ isos open Cat.Functor.Reasoning - lan' : is-lan p' F G ((G ▸ natural-iso.to isos) ∘nt eta) + lan' : is-lan p' F G ((G ▸ Isoⁿ.to isos) ∘nt eta) lan' .σ {M} α = lan.σ ((M ▸ isos.from) ∘nt α) lan' .σ-comm {M = M} = Nat-path λ j → D.pulll ((lan.σ _ .is-natural _ _ _)) @@ -278,10 +280,10 @@ which is propositionally equal to the whiskering: ```agda natural-isos→is-lan - : (p-iso : natural-iso p p') - → (F-iso : natural-iso F F') - → (G-iso : natural-iso G G') - → (natural-iso.to G-iso ◆ natural-iso.to p-iso) ∘nt eps ∘nt natural-iso.from F-iso ≡ eps' + : (p-iso : p ≅ⁿ p') + → (F-iso : F ≅ⁿ F') + → (G-iso : G ≅ⁿ G') + → ((Isoⁿ.to G-iso ◆ Isoⁿ.to p-iso) ∘nt eps ∘nt Isoⁿ.from F-iso) ≡ eps' → is-lan p F G eps → is-lan p' F' G' eps' ``` @@ -291,16 +293,12 @@ which is propositionally equal to the whiskering: natural-isos→is-lan p-iso F-iso G-iso q lan = universal-path→is-lan (natural-iso-ext→is-lan - (natural-iso-of→is-lan - (natural-iso-along→is-lan - lan - p-iso) - F-iso) + (natural-iso-of→is-lan (natural-iso-along→is-lan lan p-iso) F-iso) G-iso) (Nat-path λ x → D.extendl (D.pulll (G-iso .to .is-natural _ _ _)) ∙ q ηₚ _) - where open natural-iso + where open Isoⁿ ``` --> @@ -338,7 +336,7 @@ tiny lemma stating that this isomorphism "sends $\eta_1$ to $\eta_2$" is precisely the data of a dependent identification $\eta_1 \equiv \eta_2$ over $i'$. -[Functor-is-category]: Cat.Instances.Functor.html#Functor-is-category +[Functor-is-category]: Cat.Functor.Univalence.html#Functor-is-category ```agda functor-path : L₁.Ext ≡ L₂.Ext @@ -385,7 +383,7 @@ module : ∀ {α : G₂ => G₁} {β : G₁ => G₂} → (ε₁ ∘nt (α ◂ p)) ≡ ε₂ → (ε₂ ∘nt (β ◂ p)) ≡ ε₁ - → natural-inverses α β + → Inversesⁿ α β σ-inversesp α-factor β-factor = C′D.make-inverses (r₁.σ-uniq₂ ε₁ @@ -398,17 +396,17 @@ module σ-is-invertiblep : ∀ {α : G₂ => G₁} → (ε₁ ∘nt (α ◂ p)) ≡ ε₂ - → is-natural-invertible α + → is-invertibleⁿ α σ-is-invertiblep {α} α-factor = C′D.inverses→invertible (σ-inversesp {α} α-factor r₂.σ-comm) - σ-inverses : natural-inverses (r₁.σ ε₂) (r₂.σ ε₁) + σ-inverses : Inversesⁿ (r₁.σ ε₂) (r₂.σ ε₁) σ-inverses = σ-inversesp r₁.σ-comm r₂.σ-comm - σ-is-invertible : is-natural-invertible (r₁.σ ε₂) + σ-is-invertible : is-invertibleⁿ (r₁.σ ε₂) σ-is-invertible = σ-is-invertiblep r₁.σ-comm - unique : natural-iso G₁ G₂ + unique : G₁ ≅ⁿ G₂ unique = C′D.invertible→iso (r₁.σ ε₂) (σ-is-invertiblep r₁.σ-comm) ni⁻¹ counit : ε₁ ∘nt (r₁.σ ε₂ ◂ p) ≡ ε₂ @@ -430,7 +428,7 @@ module _ -- due to the natural isos. is-invertible→is-ran : ∀ {G' : Functor C′ D} {eps'} - → is-natural-invertible (ran.σ eps') + → is-invertibleⁿ (ran.σ eps') → is-ran p F G' eps' is-invertible→is-ran {G' = G'} {eps'} invert = ran' where open is-ran @@ -448,11 +446,11 @@ module _ natural-iso-of→is-ran : {F' : Functor C D} - → (isos : natural-iso F F') - → is-ran p F' G (natural-iso.to isos ∘nt eps) + → (isos : F ≅ⁿ F') + → is-ran p F' G (Isoⁿ.to isos ∘nt eps) natural-iso-of→is-ran {F'} isos = ran' where open is-ran - module isos = natural-iso isos + module isos = Isoⁿ isos ran' : is-ran p F' G (isos.to ∘nt eps) ran' .σ β = ran.σ (isos.from ∘nt β) @@ -466,11 +464,11 @@ module _ natural-iso-ext→is-ran : {G' : Functor C′ D} - → (isos : natural-iso G G') - → is-ran p F G' (eps ∘nt (natural-iso.from isos ◂ p)) + → (isos : G ≅ⁿ G') + → is-ran p F G' (eps ∘nt (Isoⁿ.from isos ◂ p)) natural-iso-ext→is-ran {G'} isos = ran' where open is-ran - module isos = natural-iso isos + module isos = Isoⁿ isos ran' : is-ran p F G' (eps ∘nt (isos.from ◂ p)) ran' .σ β = isos.to ∘nt ran.σ β @@ -483,15 +481,15 @@ module _ natural-iso-along→is-ran : {p' : Functor C C′} - → (isos : natural-iso p p') - → is-ran p' F G (eps ∘nt (G ▸ natural-iso.from isos)) + → (isos : p ≅ⁿ p') + → is-ran p' F G (eps ∘nt (G ▸ Isoⁿ.from isos)) natural-iso-along→is-ran {p'} isos = ran' where open is-ran - module isos = natural-iso isos + module isos = Isoⁿ isos open Cat.Functor.Reasoning - ran' : is-ran p' F G (eps ∘nt (G ▸ natural-iso.from isos)) - ran' .σ {M} β = ran.σ (β ∘nt (M ▸ natural-iso.to isos)) + ran' : is-ran p' F G (eps ∘nt (G ▸ Isoⁿ.from isos)) + ran' .σ {M} β = ran.σ (β ∘nt (M ▸ Isoⁿ.to isos)) ran' .σ-comm {M = M} = Nat-path λ j → D.pullr (sym (ran.σ _ .is-natural _ _ _)) ∙ D.pulll (ran.σ-comm ηₚ _) @@ -521,17 +519,16 @@ module _ open _=>_ natural-isos→is-ran - : (p-iso : natural-iso p p') - → (F-iso : natural-iso F F') - → (G-iso : natural-iso G G') - → (natural-iso.to F-iso ∘nt eps ∘nt (natural-iso.from G-iso ◆ natural-iso.from p-iso)) ≡ eps' + : (p-iso : p ≅ⁿ p') + → (F-iso : F ≅ⁿ F') + → (G-iso : G ≅ⁿ G') + → (Isoⁿ.to F-iso ∘nt eps ∘nt (Isoⁿ.from G-iso ◆ Isoⁿ.from p-iso)) ≡ eps' → is-ran p F G eps → is-ran p' F' G' eps' natural-isos→is-ran p-iso F-iso G-iso p ran = universal-path→is-ran (natural-iso-ext→is-ran - (natural-iso-of→is-ran - (natural-iso-along→is-ran ran p-iso) + (natural-iso-of→is-ran (natural-iso-along→is-ran ran p-iso) F-iso) G-iso) (Nat-path λ c → diff --git a/src/Cat/Functor/Naturality.lagda.md b/src/Cat/Functor/Naturality.lagda.md new file mode 100644 index 000000000..0df712773 --- /dev/null +++ b/src/Cat/Functor/Naturality.lagda.md @@ -0,0 +1,189 @@ + + +```agda +module Cat.Functor.Naturality where +``` + +# Working with natural transformations + +Working with natural transformations can often be more cumbersome than +working directly with the underlying families of morphisms; moreover, we +often have to convert between a property of natural transformations and +a (universally quantified) property of the underlying morphisms. This +module collects some notation that will help us with that task. + + + +We'll refer to the natural-transformation versions of predicates on +morphisms by a superscript `ⁿ`: + +```agda + Inversesⁿ : {F G : Functor C D} → F => G → G => F → Type _ + Inversesⁿ = CD.Inverses + + is-invertibleⁿ : {F G : Functor C D} → F => G → Type _ + is-invertibleⁿ = CD.is-invertible + + _≅ⁿ_ : Functor C D → Functor C D → Type _ + F ≅ⁿ G = CD.Isomorphism F G +``` + + + +A fundamental lemma that will let us work with natural isomorphisms more +conveniently is the following: if $\alpha : F \To G$ is a natural +transformation which is componentwise inverted by $\beta_{-} : G(-) \to +F(-)$, then $\beta$ is itself a natural transformation $G \To F$. This +means that, when constructing a natural isomorphism from scratch, we +only have to establish naturality in one direction, rather than both. + +```agda + inverse-is-natural + : ∀ {F G : Functor C D} (α : F => G) (β : ∀ x → D.Hom (G .F₀ x) (F .F₀ x) ) + → (∀ x → α .η x D.∘ β x ≡ D.id) + → (∀ x → β x D.∘ α .η x ≡ D.id) + → is-natural-transformation G F β + inverse-is-natural {F = F} {G = G} α β invl invr x y f = + β y D.∘ G .F₁ f ≡⟨ D.refl⟩∘⟨ D.intror (invl x) ⟩ + β y D.∘ G .F₁ f D.∘ α .η x D.∘ β x ≡⟨ D.refl⟩∘⟨ D.extendl (sym (α .is-natural x y f)) ⟩ + β y D.∘ α .η y D.∘ F .F₁ f D.∘ β x ≡⟨ D.cancell (invr y) ⟩ + F .F₁ f D.∘ β x ∎ +``` + +We can then create a natural isomorphism $F \cong^n G$ from the +following data: + +```agda + record make-natural-iso (F G : Functor C D) : Type (o ⊔ ℓ ⊔ ℓ′) where + no-eta-equality + field + eta : ∀ x → D.Hom (F .F₀ x) (G .F₀ x) + inv : ∀ x → D.Hom (G .F₀ x) (F .F₀ x) + eta∘inv : ∀ x → eta x D.∘ inv x ≡ D.id + inv∘eta : ∀ x → inv x D.∘ eta x ≡ D.id + natural : ∀ x y f → G .F₁ f D.∘ eta x ≡ eta y D.∘ F .F₁ f + + open make-natural-iso + + to-natural-iso : ∀ {F G} → make-natural-iso F G → F ≅ⁿ G + to-natural-iso mk .Isoⁿ.to .η = mk .eta + to-natural-iso mk .Isoⁿ.to .is-natural x y f = sym (mk .natural x y f) + to-natural-iso mk .Isoⁿ.from .η = mk .inv + to-natural-iso {F = F} {G} mk .Isoⁿ.from .is-natural = + inverse-is-natural {F} {G} (NT _ (λ x y f → sym (mk .natural x y f))) + (mk .inv) (mk .eta∘inv) (mk .inv∘eta) + to-natural-iso mk .Isoⁿ.inverses .Inversesⁿ.invl = Nat-path (mk .eta∘inv) + to-natural-iso mk .Isoⁿ.inverses .Inversesⁿ.invr = Nat-path (mk .inv∘eta) +``` + +Moreover, the following family of functions project out the +componentwise invertibility, resp. componentwise isomorphism, associated +to an invertible natural transformation, resp. natural isomorphism. + +```agda + is-invertibleⁿ→is-invertible + : ∀ {F G} {α : F => G} + → is-invertibleⁿ α + → ∀ x → D.is-invertible (α .η x) + is-invertibleⁿ→is-invertible inv x = + D.make-invertible + (CD.is-invertible.inv inv .η x) + (CD.is-invertible.invl inv ηₚ x) + (CD.is-invertible.invr inv ηₚ x) + + isoⁿ→iso + : ∀ {F G} → F ≅ⁿ G + → ∀ x → F .F₀ x D.≅ G .F₀ x + isoⁿ→iso α x = + D.make-iso (α.to .η x) (α.from .η x) (α.invl ηₚ x) (α.invr ηₚ x) + where module α = Isoⁿ α + + is-invertibleⁿ→isoⁿ : ∀ {F G} {α : F => G} → is-invertibleⁿ α → F ≅ⁿ G + is-invertibleⁿ→isoⁿ nat-inv = CD.invertible→iso _ nat-inv + + isoⁿ→is-invertible + : ∀ {F G} (α : F ≅ⁿ G) + → ∀ x → D.is-invertible (α .Isoⁿ.to .η x) + isoⁿ→is-invertible α x = D.iso→invertible (isoⁿ→iso α x) +``` + + diff --git a/src/Cat/Functor/Properties.lagda.md b/src/Cat/Functor/Properties.lagda.md new file mode 100644 index 000000000..41186b62b --- /dev/null +++ b/src/Cat/Functor/Properties.lagda.md @@ -0,0 +1,321 @@ + + +```agda +module Cat.Functor.Properties where +``` + + + +# Functors + +This module defines the most important clases of functors: Full, +faithful, fully faithful (abbreviated ff), _split_ essentially +surjective and ("_merely_") essentially surjective. + +A functor is **full** when its action on hom-sets is surjective: + +```agda +is-full : Functor C D → Type _ +is-full {C = C} {D = D} F = + ∀ {x y} (g : D .Hom (F₀ F x) (F₀ F y)) → ∃[ f ∈ C .Hom x y ] (F₁ F f ≡ g) +``` + +A functor is **faithful** when its action on hom-sets is injective: + +```agda +is-faithful : Functor C D → Type _ +is-faithful F = ∀ {x y} → injective (F₁ F {x = x} {y}) +``` + + + +## ff Functors + +A functor is **fully faithful** (abbreviated **ff**) when its action on +hom-sets is an equivalence. Since Hom-sets are sets, it suffices for the +functor to be full and faithful; Rather than taking this conjunction as +a definition, we use the more directly useful data as a definition and +prove the conjunction as a theorem. + +```agda +is-fully-faithful : Functor C D → Type _ +is-fully-faithful F = ∀ {x y} → is-equiv (F₁ F {x = x} {y}) + +fully-faithful→faithful : {F : Functor C D} → is-fully-faithful F → is-faithful F +fully-faithful→faithful f = Equiv.injective (_ , f) + +fully-faithful→full : {F : Functor C D} → is-fully-faithful F → is-full F +fully-faithful→full {F = F} ff g = inc (equiv→inverse ff g , equiv→counit ff g) + +full+faithful→ff + : (F : Functor C D) → is-full F → is-faithful F → is-fully-faithful F +full+faithful→ff {C = C} {D = D} F surj inj .is-eqv = p where + img-is-prop : ∀ {x y} f → is-prop (fibre (F₁ F {x = x} {y}) f) + img-is-prop f (g , p) (h , q) = Σ-prop-path (λ _ → D .Hom-set _ _ _ _) (inj (p ∙ sym q)) + + p : ∀ {x y} f → is-contr (fibre (F₁ F {x = x} {y}) f) + p f .centre = ∥-∥-elim (λ _ → img-is-prop f) (λ x → x) (surj f) + p f .paths = img-is-prop f _ +``` + +A very important property of fully faithful functors (like $F$) is that +they are **conservative**: If the image of $f : x \to y$ under $F$ is an +isomorphism $Fx \cong Fy$, then $f$ was really an isomorphism $f : x +\cong y$. + +```agda +module _ {C : Precategory o h} {D : Precategory o₁ h₁} where + private + module C = Precategory C + module D = Precategory D + + import Cat.Morphism C as Cm + import Cat.Morphism D as Dm + + is-ff→is-conservative + : {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 + open Cm.is-invertible + open Cm.Inverses +``` + +Since the functor is ff, we can find a map "$F_1^{-1}(f) : y \to x$" in +the domain category to serve as an inverse for $f$: + +```agda + g : C.Hom _ _ + g = equiv→inverse ff (isinv .Dm.is-invertible.inv) + module ff {a} {b} = Equiv (_ , ff {a} {b}) + + Ffog = + F₁ F (f C.∘ g) ≡⟨ F-∘ F _ _ ⟩ + F₁ F f D.∘ F₁ F g ≡⟨ ap₂ D._∘_ refl (ff.ε _) ∙ isinv .Dm.is-invertible.invl ⟩ + D.id ∎ + + Fgof = + F₁ F (g C.∘ f) ≡⟨ F-∘ F _ _ ⟩ + F₁ F g D.∘ F₁ F f ≡⟨ ap₂ D._∘_ (ff.ε _) refl ∙ isinv .Dm.is-invertible.invr ⟩ + D.id ∎ + + i : Cm.is-invertible _ + i .inv = g + i .inverses .invl = + f C.∘ g ≡⟨ sym (ff.η _) ⟩ + ff.from ⌜ F₁ F (f C.∘ g) ⌝ ≡⟨ ap! (Ffog ∙ sym (F-id F)) ⟩ + ff.from (F₁ F C.id) ≡⟨ ff.η _ ⟩ + C.id ∎ + i .inverses .invr = + g C.∘ f ≡⟨ sym (ff.η _) ⟩ + ff.from ⌜ F₁ F (g C.∘ f) ⌝ ≡⟨ ap! (Fgof ∙ sym (F-id F)) ⟩ + ff.from (F₁ F C.id) ≡⟨ ff.η _ ⟩ + C.id ∎ + + is-ff→essentially-injective + : {F : Functor C D} → is-fully-faithful F + → ∀ {X Y} → F₀ F X Dm.≅ F₀ F Y + → X Cm.≅ Y + is-ff→essentially-injective {F = F} ff im = im′ where + -- Cm.make-iso (equiv→inverse ff to) inv invl invr + open Dm._≅_ im using (to ; from ; inverses) + D-inv′ : Dm.is-invertible (F₁ F (equiv→inverse ff to)) + D-inv′ .Dm.is-invertible.inv = from + 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′) + + im′ : _ Cm.≅ _ + im′ .to = equiv→inverse ff to + im′ .from = inv + im′ .inverses .Cm.Inverses.invl = invl + im′ .inverses .Cm.Inverses.invr = invr +``` + +## Essential Fibres + +The **essential fibre** of a functor $F : C \to D$ over an object $y : +D$ is the space of objects of $C$ which $F$ takes, up to isomorphism, to +$y$. + +```agda +Essential-fibre : Functor C D → D .Ob → Type _ +Essential-fibre {D = D} F y = Σ[ x ∈ _ ] (F₀ F x ≅ y) + where open import Cat.Morphism D +``` + +A functor is **split essentially surjective** (abbreviated **split +eso**) if there is a procedure for finding points in the essential fibre +over any object. It's **essentially surjective** if the this procedure +_merely_, i.e. truncatedly, finds a point: + +```agda +is-split-eso : Functor C D → Type _ +is-split-eso F = ∀ y → Essential-fibre F y + +is-eso : Functor C D → Type _ +is-eso F = ∀ y → ∥ Essential-fibre F y ∥ +``` + + + +## Pseudomonic Functors + +A functor is **pseudomonic** if it is faithful and full on isomorphisms. +Pseudomonic functors are arguably the correct notion of subcategory, as +they ensure that we are not able to distinguish between isomorphic objects +when creating a subcategory. + + + +```agda + is-full-on-isos : Functor C D → Type (o ⊔ h ⊔ h₁) + is-full-on-isos F = + ∀ {x y} → (f : (F .F₀ x) D.≅ (F .F₀ y)) → ∃[ g ∈ x C.≅ y ] (F-map-iso F g ≡ f) + + record is-pseudomonic (F : Functor C D) : Type (o ⊔ h ⊔ h₁) where + no-eta-equality + field + faithful : is-faithful F + isos-full : is-full-on-isos F + + open is-pseudomonic +``` + +Somewhat surprisingly, pseudomonic functors are [conservative]. +As $F$ is full on isos, there merely exists some iso $g$ in the fibre +of $f$. However, invertibility is a property of morphisms, so we can +untruncate the mere existence. Once we have our hands on the isomorphism, +we perform a simple calculation to note that it yields an inverse to $f$. + +[conservative]: Cat.Functor.Conservative.html + +```agda + pseudomonic→conservative + : ∀ {F : Functor C D} + → is-pseudomonic F + → ∀ {x y} (f : C.Hom x y) → D.is-invertible (F₁ F f) + → C.is-invertible f + pseudomonic→conservative {F = F} pseudo {x} {y} f inv = + ∥-∥-rec C.is-invertible-is-prop + (λ (g , p) → + C.make-invertible (C.from g) + (sym (ap (C._∘ _) (pseudo .faithful (ap D.to p))) ∙ C.invl g) + (sym (ap (_ C.∘_) (pseudo .faithful (ap D.to p))) ∙ C.invr g)) + (pseudo .isos-full (D.invertible→iso _ inv)) +``` + +In a similar vein, pseudomonic functors are essentially injective. +The proof follows a similar path to the prior one, hinging on the +fact that faithful functors are an embedding on isos. + +```agda + pseudomonic→essentially-injective + : ∀ {F : Functor C D} + → is-pseudomonic F + → ∀ {x y} → F₀ F x D.≅ F₀ F y + → x C.≅ y + pseudomonic→essentially-injective {F = F} pseudo f = + ∥-∥-rec (faithful→iso-fibre-prop F (pseudo .faithful) f) + (λ x → x) + (pseudo .isos-full f) .fst +``` + +Fully faithful functors are pseudomonic, as they are faithful and +essentially injective. + +```agda + ff→pseudomonic + : ∀ {F : Functor C D} + → is-fully-faithful F + → is-pseudomonic F + ff→pseudomonic {F} ff .faithful = fully-faithful→faithful {F = F} ff + ff→pseudomonic {F} ff .isos-full f = + inc (is-ff→essentially-injective {F = F} ff f , + D.≅-pathp refl refl (equiv→counit ff (D.to f))) +``` + +## Equivalence on Objects Functors + +A functor $F : \cC \to \cD$ is an **equivalence on objects** if its action +on objects is an equivalence. + +```agda +is-equiv-on-objects : (F : Functor C D) → Type _ +is-equiv-on-objects F = is-equiv (F .F₀) +``` + +If $F$ is an equivalence-on-objects functor, then it is (split) +essentially surjective. + +```agda +equiv-on-objects→split-eso + : ∀ (F : Functor C D) → is-equiv-on-objects F → is-split-eso F +equiv-on-objects→split-eso {D = D} F eqv y = + equiv→inverse eqv y , path→iso (equiv→counit eqv y) + +equiv-on-objects→eso : ∀ (F : Functor C D) → is-equiv-on-objects F → is-eso F +equiv-on-objects→eso F eqv y = inc (equiv-on-objects→split-eso F eqv y) +``` diff --git a/src/Cat/Functor/Pullback.lagda.md b/src/Cat/Functor/Pullback.lagda.md index c93d13940..84eb295d1 100644 --- a/src/Cat/Functor/Pullback.lagda.md +++ b/src/Cat/Functor/Pullback.lagda.md @@ -1,12 +1,12 @@ + +```agda +module Cat.Functor.Univalence where +``` + + + +Our previous results about [paths between functors][pbf], [componentwise +invertibility], and general reasoning in univalent categories assemble +into the following very straightforward proof that $[\cC,\cD]$ is +univalent whenever $\cD$ is. + +[pbf]: Cat.Functor.Base.html#paths-between-functors +[componentwise invertibility]: Cat.Functor.Naturality.html + +```agda +Functor-is-category : is-category D → is-category Cat[ C , D ] +Functor-is-category {D = D} {C = C} d-cat .to-path {F} {G} im = + Functor-path (λ x → d-cat .to-path (isoⁿ→iso im x)) coh + where + open Univalent d-cat using (Hom-pathp-iso ; pulll ; cancelr) + abstract + coh : ∀ {x y : C .Ob} (f : C .Hom x y) + → PathP (λ i → D .Hom (d-cat .to-path (isoⁿ→iso im x) i) (d-cat .to-path (isoⁿ→iso im y) i)) + (F .F₁ f) (G .F₁ f) + coh f = Hom-pathp-iso ( pulll (Isoⁿ.to im .is-natural _ _ _) + ∙ cancelr (Isoⁿ.invl im ηₚ _)) +Functor-is-category {D = D} d-cat .to-path-over p = + ≅ⁿ-pathp _ _ (λ x → Hom-pathp-reflr-iso (Precategory.idr D (Isoⁿ.to p .η x))) + where open Univalent d-cat +``` + + diff --git a/src/Cat/Functor/WideSubcategory.lagda.md b/src/Cat/Functor/WideSubcategory.lagda.md index cef27e724..a68f87eb8 100644 --- a/src/Cat/Functor/WideSubcategory.lagda.md +++ b/src/Cat/Functor/WideSubcategory.lagda.md @@ -1,6 +1,6 @@ diff --git a/src/Cat/Instances/Comma/Univalent.lagda.md b/src/Cat/Instances/Comma/Univalent.lagda.md index 8b5257e85..7d424c1be 100644 --- a/src/Cat/Instances/Comma/Univalent.lagda.md +++ b/src/Cat/Instances/Comma/Univalent.lagda.md @@ -96,8 +96,8 @@ an identification $o \equiv o'$. lemma′ : PathP (λ i → X.Hom (F.₀ (objs i .x)) (G.₀ (objs i .y))) (ob .map) (ob′ .map) lemma′ = transport - (λ i → PathP (λ j → X.Hom (F-map-path F x-is-x yuniv xuniv (~ i) j) - (F-map-path G y-is-y zuniv xuniv (~ i) j)) + (λ i → PathP (λ j → X.Hom (F-map-path yuniv xuniv F x-is-x (~ i) j) + (F-map-path zuniv xuniv G y-is-y (~ i) j)) (ob .map) (ob′ .map)) $ Univalent.Hom-pathp-iso xuniv $ X.pulll (sym (isom.to .sq)) ∙ diff --git a/src/Cat/Instances/Core.lagda.md b/src/Cat/Instances/Core.lagda.md index 0e20bd958..c81cd460f 100644 --- a/src/Cat/Instances/Core.lagda.md +++ b/src/Cat/Instances/Core.lagda.md @@ -1,9 +1,9 @@ - - - - -We can then show that these definitions assemble into a category where -the objects are functors $F, G : C \to D$, and the morphisms are natural -transformations $F \To G$. This is because natural -transformations inherit the identity and associativity laws from the -codomain category $D$, and since hom-sets are sets, `is-natural`{.Agda} -does not matter. - -```agda -module _ {o₁ h₁ o₂ h₂} (C : Precategory o₁ h₁) (D : Precategory o₂ h₂) where - open Precategory - - Cat[_,_] : Precategory (o₁ ⊔ o₂ ⊔ h₁ ⊔ h₂) (o₁ ⊔ h₁ ⊔ h₂) - Cat[_,_] .Ob = Functor C D - Cat[_,_] .Hom F G = F => G - Cat[_,_] .id = idnt - Cat[_,_] ._∘_ = _∘nt_ -``` - -All of the properties that make up a `Precategory`{.Agda} follow from -the characterisation of equalities in natural transformations: They `are -a set`{.Agda ident=Nat-is-set}, and equality of the components -`determines`{.Agda ident=Nat-path} equality of the transformation. - -```agda - Cat[_,_] .Hom-set F G = Nat-is-set - Cat[_,_] .idr f = Nat-path λ x → D .idr _ - Cat[_,_] .idl f = Nat-path λ x → D .idl _ - Cat[_,_] .assoc f g h = Nat-path λ x → D .assoc _ _ _ -``` - -Before moving on, we prove the following lemma which characterises -equality in `Functor`{.Agda} (between definitionally equal categories). -Given an identification $p : F_0(x) \equiv G_0(x)$ between the object -mappings, and an identification of morphism parts that lies over $p$, we -can identify the functors $F \equiv G$. - -```agda -Functor-path : {F G : Functor C D} - → (p0 : ∀ x → F₀ F x ≡ F₀ G x) - → (p1 : ∀ {x y} (f : C .Hom x y) - → PathP (λ i → D .Hom (p0 x i) (p0 y i)) (F₁ F f) (F₁ G f)) - → F ≡ G -Functor-path p0 p1 i .F₀ x = p0 x i -Functor-path p0 p1 i .F₁ f = p1 f i -``` - - ## Functor categories @@ -196,150 +40,8 @@ natural inverse) are themselves isomorphisms in $D$. [univalent]: Cat.Univalent.html - - -```agda - Nat-iso→Iso : F [C,D].≅ G → ∀ x → F₀ F x D.≅ F₀ G x - Nat-iso→Iso natiso x = - D.make-iso (to .η x) (from .η x) - (λ i → invl i .η x) (λ i → invr i .η x) - where open [C,D]._≅_ natiso -``` - -We can now prove that $[C,D]$ `is a category`{.Agda ident=is-category}, -by showing that, for a fixed functor $F : C \to D$, the space of -functors $G$ equipped with natural isomorphisms $F \cong G$ is -contractible. The centre of contraction is the straightforward part: We -have the canonical choice of $(F, id)$. - - - -```agda - Functor-is-category : is-category D → is-category Cat[ C , D ] -``` - -The hard part is showing that, given some other functor $G : C \to D$ -with a natural isomorphism $F \cong G$, we can give a continuous -deformation $p : G \equiv F$, such that, over this $p$, the given -isomorphism looks like the identity. - -```agda - Functor-is-category DisCat = functor-cat where -``` - -The first thing we must note is that we can recover the components of a -natural isomorphism while passing to/from paths in $D$. Since $D$ is a -category, `path→iso`{.Agda} is an equivalence; The lemmas we need then -follow from `equivalences having sections`{.Agda ident=iso→path→iso}. - -```agda - open Cat.Univalent.Univalent DisCat - using (iso→path ; iso→path→iso ; path→iso→path ; Hom-pathp-iso ; Hom-pathp-reflr-iso) - - module _ {F G} (F≅G : _) where - ptoi-to - : ∀ x → path→iso (iso→path (Nat-iso→Iso F≅G _)) .D._≅_.to ≡ F≅G .to .η x - ptoi-to x = ap (λ e → e .D._≅_.to) (iso→path→iso (Nat-iso→Iso F≅G x)) - - ptoi-from : ∀ x → path→iso (iso→path (Nat-iso→Iso F≅G _)) .D._≅_.from - ≡ F≅G .from .η x - ptoi-from x = ap (λ e → e .D._≅_.from) (iso→path→iso (Nat-iso→Iso F≅G x)) -``` - -We can then show that the natural isomorphism $F \cong G$ induces a -homotopy between the object parts of $F$ and $G$: - -```agda - F₀≡G₀ : ∀ x → F₀ F x ≡ F₀ G x - F₀≡G₀ x = iso→path (Nat-iso→Iso F≅G x) -``` - -A slightly annoying calculation tells us that pre/post composition with -$F \cong G$ does in fact turn $F_1(f)$ into $G_1(f)$; This is because $F -\cong G$ is natural, so we can push it "past" the morphism part of $F$ -so that the two halves of the isomorphism annihilate. - -```agda - F₁≡G₁ : ∀ {x y} (f : C .Hom x y) - → PathP (λ i → D.Hom (F₀≡G₀ x i) (F₀≡G₀ y i)) (F .F₁ {x} {y} f) (G .F₁ {x} {y} f) - F₁≡G₁ {x = x} {y} f = Hom-pathp-iso $ - (D.extendl (F≅G .to .is-natural x y f) ∙ D.elimr (F≅G .invl ηₚ x)) - - F≡G : F ≡ G - F≡G = Functor-path F₀≡G₀ λ f → F₁≡G₁ f -``` - -Putting these homotopies together defines a path `F≡G`{.Agda}. It -remains to show that, over this path, the natural isomorphism we started -with is homotopic to the identity; Equality of `isomorphisms`{.Agda -ident=≅-pathp} and `natural transformations`{.Agda ident=Nat-pathp} are -both tested componentwise, so we can "push down" the relevant equalities -to the level of families of morphisms; By computation, all we have to -show is that $\eta{}_x \circ \id \circ \id = f$. - -```agda - id≡F≅G : PathP (λ i → F ≅ F≡G i) id-iso F≅G - id≡F≅G = ≅-pathp refl F≡G $ Nat-pathp refl F≡G λ x → - Hom-pathp-reflr-iso (D.idr _) - - functor-cat : is-category Cat[ C , D ] - functor-cat .to-path = F≡G - functor-cat .to-path-over = id≡F≅G -``` - -A useful lemma is that if you have a natural transformation where each -component is an isomorphism, the evident inverse transformation is -natural too, thus defining an inverse to `Nat-iso→Iso`{.Agda} defined -above. - -```agda -module _ {C : Precategory o h} {D : Precategory o₁ h₁} {F G : Functor C D} where - import Cat.Reasoning D as D - import Cat.Reasoning Cat[ C , D ] as [C,D] - private - module F = Functor F - module G = Functor G - - open D.is-invertible - - componentwise-invertible→invertible - : (eta : F => G) - → (∀ x → D.is-invertible (eta .η x)) - → [C,D].is-invertible eta - componentwise-invertible→invertible eta invs = are-invs where - module eta = _=>_ eta - - eps : G => F - eps .η x = invs x .inv - eps .is-natural x y f = - invs y .inv D.∘ ⌜ G.₁ f ⌝ ≡⟨ ap! (sym (D.idr _) ∙ ap (G.₁ f D.∘_) (sym (invs x .invl))) ⟩ - invs y .inv D.∘ ⌜ G.₁ f D.∘ eta.η x D.∘ invs x .inv ⌝ ≡⟨ ap! (D.extendl (sym (eta.is-natural _ _ _))) ⟩ - invs y .inv D.∘ eta.η y D.∘ F.₁ f D.∘ invs x .inv ≡⟨ D.cancell (invs y .invr) ⟩ - F.₁ f D.∘ invs x .inv ∎ - - are-invs : [C,D].is-invertible eta - are-invs = - record - { inv = eps - ; inverses = - record - { invl = Nat-path λ x → invs x .invl - ; invr = Nat-path λ x → invs x .invr - } - } +open import Cat.Functor.Univalence public ``` # Currying @@ -419,8 +121,6 @@ module _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {J : Precategory o' ℓ'} where diff --git a/src/Cat/Instances/InternalFunctor.lagda.md b/src/Cat/Instances/InternalFunctor.lagda.md index d2213fe37..992c239a8 100644 --- a/src/Cat/Instances/InternalFunctor.lagda.md +++ b/src/Cat/Instances/InternalFunctor.lagda.md @@ -2,8 +2,8 @@ ```agda open import Cat.Prelude -import Cat.Internal.Base import Cat.Internal.Reasoning +import Cat.Internal.Base import Cat.Reasoning ``` --> @@ -31,7 +31,7 @@ If $\cC$ and $\cD$ are categories internal to $\cB$, we can define the of the ordinary [functor categories]. This relativisation plays a similar role in the theory of internal categories. -[functor categories]: Cat.Instances.Functor.html +[functor categories]: Cat.Functor.Base.html Before we define the category, we need some simple constructions on internal natural transformations. First, we note that there is an @@ -119,11 +119,11 @@ module _ {ℂ 𝔻 : Internal-cat} where --> ```agda - Internal-natural-inverses + Internal-Inversesⁿ : {F G : Internal-functor ℂ 𝔻} → F =>i G → G =>i F → Type _ - Internal-natural-inverses = ℂ𝔻.Inverses + Internal-Inversesⁿ = ℂ𝔻.Inverses is-internal-natural-invertible : {F G : Internal-functor ℂ 𝔻} @@ -137,10 +137,10 @@ module _ {ℂ 𝔻 : Internal-cat} where @@ -21,7 +21,7 @@ on [internal functor categories]. This mirrors [the similar results] for composition of ordinary functors. [internal functor categories]: Cat.Instances.InternalFunctor.html -[the similar results]: Cat.Instances.Functor.Compose.html +[the similar results]: Cat.Functor.Compose.html To show this, we will need to define whiskering and horizontal composition of internal natural transformations. @@ -59,7 +59,7 @@ module _ {o ℓ} {C : Precategory o ℓ} {𝔸 𝔹 ℂ : Internal.Internal-cat counterparts], so we omit their definitions. -[1-categorical counterparts]: Cat.Instances.Functor.Compose.html +[1-categorical counterparts]: Cat.Functor.Compose.html ```agda (α ◂i H) .ηi x = α .ηi (H .Fi₀ x) @@ -121,7 +121,7 @@ difference is the addition of extra naturality conditions, which are easy to prove. -[functor composition]: Cat.Instances.Functor.Compose.html +[functor composition]: Cat.Functor.Compose.html ```agda Fi∘-functor .F₁ {F , G} {H , K} (α , β) = α ◆i β diff --git a/src/Cat/Instances/Karoubi.lagda.md b/src/Cat/Instances/Karoubi.lagda.md index 345c0ac3c..5373f004a 100644 --- a/src/Cat/Instances/Karoubi.lagda.md +++ b/src/Cat/Instances/Karoubi.lagda.md @@ -1,6 +1,6 @@ diff --git a/src/Cat/Instances/Shape/Involution.lagda.md b/src/Cat/Instances/Shape/Involution.lagda.md index d74a3fa92..90abaadce 100644 --- a/src/Cat/Instances/Shape/Involution.lagda.md +++ b/src/Cat/Instances/Shape/Involution.lagda.md @@ -1,9 +1,9 @@ @@ -33,11 +32,11 @@ open Internal-hom The category $\Sets$ is not [strict], so it is not [internal] to any category of sets, even setting aside size issues. However, $\Sets$ still plays an important role in (strict) category theory, by passing to the -co[presheaf] categories $\cC \to \thecat{Sets}$. +co[presheaf] categories $\cC \to \Sets$. [strict]: Cat.Strict.html [internal]: Cat.Internal.Base.html -[presheaf]: Cat.Instances.Functor.html +[presheaf]: Cat.Functor.Base.html#presheaf-precategories We wish to relativize this to an arbitrary base category $\cC$, not just $\thecat{Sets}$. Specifically, if $\bC$ is a category internal to $\cC$, diff --git a/src/Cat/Internal/Instances/Discrete.lagda.md b/src/Cat/Internal/Instances/Discrete.lagda.md index 94cbc8fde..b70d2fa0c 100644 --- a/src/Cat/Internal/Instances/Discrete.lagda.md +++ b/src/Cat/Internal/Instances/Discrete.lagda.md @@ -1,8 +1,8 @@ diff --git a/src/Cat/Internal/Morphism.lagda.md b/src/Cat/Internal/Morphism.lagda.md index 3db659701..848cd55d0 100644 --- a/src/Cat/Internal/Morphism.lagda.md +++ b/src/Cat/Internal/Morphism.lagda.md @@ -1,12 +1,11 @@ diff --git a/src/Cat/Internal/Sets.lagda.md b/src/Cat/Internal/Sets.lagda.md index 35bf808c0..0b1abac40 100644 --- a/src/Cat/Internal/Sets.lagda.md +++ b/src/Cat/Internal/Sets.lagda.md @@ -1,9 +1,8 @@ + +```agda +module Cat.Allegory.Morphism {o ℓ ℓ'} (A : Allegory o ℓ ℓ') where +``` + + + +# Morphisms in an Allegory + +This module defines a couple of important classes of morphisms that can +be found in an allegory. + +# Reflexive Morphisms + +A morphism $f : X \to X$ in an allegory is **reflexive** if $id \le f$. + +```agda +is-reflexive : Hom x x → Type _ +is-reflexive f = id ≤ f +``` + +The composition of two reflexive morphisms is reflexive, and the +identity morphism is trivially reflexive. + +```agda +reflexive-id : is-reflexive (id {x}) +reflexive-id = ≤-refl + +reflexive-∘ : is-reflexive f → is-reflexive g → is-reflexive (f ∘ g) +reflexive-∘ {f = f} {g = g} f-refl g-refl = + id =⟨ sym (idl _) ⟩ + id ∘ id ≤⟨ f-refl ◆ g-refl ⟩ + f ∘ g ≤∎ +``` + +The intersection of reflexive morphisms is reflexive. + +```agda +reflexive-∩ : is-reflexive f → is-reflexive g → is-reflexive (f ∩ g) +reflexive-∩ f-refl g-refl = ∩-univ f-refl g-refl +``` + +The dual of a reflexive morphism is also reflexive. + +```agda +reflexive-dual : is-reflexive f → is-reflexive (f †) +reflexive-dual {f = f} f-refl = + dual-≤ᵣ A $ + id † =⟨ dual-id A ⟩ + id ≤⟨ f-refl ⟩ + f ≤∎ +``` + +If $f \le g$ and $f$ is reflexive, then $g$ is reflexive. + +```agda +reflexive-≤ : f ≤ g → is-reflexive f → is-reflexive g +reflexive-≤ w f-refl = ≤-trans f-refl w +``` + +If $f$ is reflexive, then $id \le f \cap f^o$. + +```agda +reflexive→diagonal + : is-reflexive f → id ≤ f ∩ f † +reflexive→diagonal f-refl = ∩-univ f-refl (reflexive-dual f-refl) +``` + + +# Symmetric Morphisms + +A morphism $f : X \to X$ is **symmetric** if $f \le f^o$. + +```agda +is-symmetric : Hom x x → Type _ +is-symmetric f = f ≤ f † +``` + +The identity morphism is trivially symmetric. + +```agda +symmetric-id : is-symmetric (id {x}) +symmetric-id {x = x} = subst (id {x} ≤_) (sym $ dual-id A) (≤-refl {f = id {x}}) +``` + +The composition of symmetric morphisms $f$ and $g$ is symmetric if +$g \circ f \le f \circ g$. + +```agda +symmetric-∘ + : is-symmetric f → is-symmetric g + → g ∘ f ≤ f ∘ g + → is-symmetric (f ∘ g) +symmetric-∘ {f = f} {g = g} f-sym g-sym w = + f ∘ g ≤⟨ f-sym ◆ g-sym ⟩ + f † ∘ g † =⟨ sym dual-∘ ⟩ + (g ∘ f) † ≤⟨ dual-≤ w ⟩ + (f ∘ g) † ≤∎ +``` + +The dual of a symmetric morphism is symmetric. + +```agda +symmetric-dual : is-symmetric f → is-symmetric (f †) +symmetric-dual {f = f} f-sym = dual-≤ᵣ A $ + f † † =⟨ dual f ⟩ + f ≤⟨ f-sym ⟩ + f † ≤∎ +``` + +The intersection of symmetric morphisms is symmetric. + +```agda +symmetric-∩ : is-symmetric f → is-symmetric g → is-symmetric (f ∩ g) +symmetric-∩ {f = f} {g = g} f-sym g-sym = + f ∩ g ≤⟨ ∩-pres f-sym g-sym ⟩ + f † ∩ g † =⟨ sym $ dual-∩ A ⟩ + (f ∩ g) † ≤∎ +``` + +If $f$ is symmetric, then it is equal to its dual. + +```agda +symmetric→self-dual + : is-symmetric f → f ≡ f † +symmetric→self-dual f-sym = + ≤-antisym f-sym (dual-≤ₗ A f-sym) +``` + +# Transitive Morphisms + +A morphism $f : X \to X$ is **transitive** if $f \circ f \le f$. + +```agda +is-transitive : Hom x x → Type _ +is-transitive f = f ∘ f ≤ f +``` + +The identity morphism is transitive. + +```agda +transitive-id : is-transitive (id {x}) +transitive-id = ≤-eliml ≤-refl +``` + +The composition of two transitive morphisms $f$ and $g$ is transitive +if $g \circ f \le f \circ g$. + +```agda +transitive-∘ + : is-transitive f → is-transitive g + → g ∘ f ≤ f ∘ g + → is-transitive (f ∘ g) +transitive-∘ {f = f} {g = g} f-trans g-trans w = + (f ∘ g) ∘ (f ∘ g) ≤⟨ ≤-extend-inner w ⟩ + (f ∘ f) ∘ (g ∘ g) ≤⟨ f-trans ◆ g-trans ⟩ + f ∘ g ≤∎ +``` + +A useful little lemma is that if $f$ is transitive, then +$(f \cap g) \circ (f \cap h) \le f$. + +```agda +transitive-∩l : is-transitive f → (f ∩ g) ∘ (f ∩ h) ≤ f +transitive-∩l f-trans = ≤-trans (∩-le-l ◆ ∩-le-l) f-trans + +transitive-∩r : is-transitive h → (f ∩ h) ∘ (g ∩ h) ≤ h +transitive-∩r h-trans = ≤-trans (∩-le-r ◆ ∩-le-r) h-trans +``` + +We can use these lemmas to show that the intersection of transitive +morphisms is transitive. + +```agda +transitive-∩ + : is-transitive f → is-transitive g → is-transitive (f ∩ g) +transitive-∩ {f = f} {g = g} f-trans g-trans = + ∩-univ (transitive-∩l f-trans) (transitive-∩r g-trans) +``` + +If $f$ is transitive, then so is its dual. + +```agda +transitive-dual : is-transitive f → is-transitive (f †) +transitive-dual {f = f} f-trans = + f † ∘ f † =⟨ sym dual-∘ ⟩ + (f ∘ f) † ≤⟨ dual-≤ f-trans ⟩ + f † ≤∎ +``` + +# Cotransitive Morphisms + +A morphism $f : X \to X$ is **cotransitive** if $f \le f \circ f$. + +::: warning +**Warning**: There is another notion of cotransitive relation, which +stipulates that for all $x, y, z$, if $R(x,z)$, then either $R(x,y)$ +or $R(y,z)$. This is a poor choice of a name, as it is **not** a +transitive relation in $\Rel^{co}$. + +Other sources call cotransitive morphisms "symmetric idempotents", though +we avoid this terminology, as cotranstive morphisms are not symmetric. +::: + +```agda +is-cotransitive : Hom x x → Type _ +is-cotransitive f = f ≤ f ∘ f +``` + +The identity morphism is cotransitive. + +```agda +cotransitive-id : is-cotransitive (id {x}) +cotransitive-id = ≤-introl ≤-refl +``` + +The composition of two cotransitive morphisms $f$ and $g$ is cotransitive +if $f \circ g \le g \circ f$. + +```agda +cotransitive-∘ + : is-cotransitive f → is-cotransitive g + → f ∘ g ≤ g ∘ f + → is-cotransitive (f ∘ g) +cotransitive-∘ {f = f} {g = g} f-cotrans g-cotrans w = + f ∘ g ≤⟨ f-cotrans ◆ g-cotrans ⟩ + (f ∘ f) ∘ (g ∘ g) ≤⟨ ≤-extend-inner w ⟩ + (f ∘ g) ∘ (f ∘ g) ≤∎ +``` + +If the intersection of $f$ and $g$ is cotransitive, then +$f \cap g \le f \circ g$. + +```agda +cotransitive-∩-∘ + : is-cotransitive (f ∩ g) + → f ∩ g ≤ f ∘ g +cotransitive-∩-∘ {f = f} {g = g} f∩g-cotrans = + f ∩ g ≤⟨ f∩g-cotrans ⟩ + (f ∩ g) ∘ (f ∩ g) ≤⟨ ∩-le-l ◆ ∩-le-r ⟩ + f ∘ g ≤∎ +``` + +If $f$ is reflexive, then it is cotransitive. + +```agda +reflexive→cotransitive + : is-reflexive f → is-cotransitive f +reflexive→cotransitive {f = f} f-refl = + f =⟨ sym (idl f) ⟩ + id ∘ f ≤⟨ f-refl ◀ f ⟩ + f ∘ f ≤∎ +``` + +If $f$ is transitive and symmetric, then it is cotransitive. + +```agda +transitive+symmetric→cotransitive + : is-transitive f → is-symmetric f → is-cotransitive f +transitive+symmetric→cotransitive {f = f} f-trans f-sym = + f ≤⟨ ≤-conj f ⟩ + f ∘ f † ∘ f ≤⟨ f ▶ dual-≤ₗ A f-sym ◀ f ⟩ + f ∘ f ∘ f ≤⟨ f ▶ f-trans ⟩ + f ∘ f ≤∎ +``` + +# Coreflexive Morphisms + +```agda +is-coreflexive : Hom x x → Type _ +is-coreflexive f = f ≤ id +``` + +The composition of two coreflexive morphisms is coreflexive, and the +identity morphism is trivially coreflexive. + +```agda +coreflexive-∘ : is-coreflexive f → is-coreflexive g → is-coreflexive (f ∘ g) +coreflexive-∘ {f = f} {g = g} f-corefl g-corefl = + f ∘ g ≤⟨ f-corefl ◆ g-corefl ⟩ + id ∘ id =⟨ idl _ ⟩ + id ≤∎ + +coreflexive-id : is-coreflexive (id {x}) +coreflexive-id = ≤-refl +``` + +Coreflexive morphisms are closed under intersection. + +```agda +coreflexive-∩ + : ∀ {x} {f g : Hom x x} + → is-coreflexive f → is-coreflexive g → is-coreflexive (f ∩ g) +coreflexive-∩ {f = f} {g = g} f-corefl g-corefl = + f ∩ g ≤⟨ ∩-pres f-corefl g-corefl ⟩ + id ∩ id =⟨ ∩-idempotent ⟩ + id ≤∎ +``` + +Coreflexive morphisms are closed under duals. + +```agda +coreflexive-dual : is-coreflexive f → is-coreflexive (f †) +coreflexive-dual {f = f} f-corefl = dual-≤ₗ A $ + f ≤⟨ f-corefl ⟩ + id =⟨ sym $ dual-id A ⟩ + id † ≤∎ +``` + +If $f \le g$ and $g$ is coreflexive, then $f$ is coreflexive. + +```agda +coreflexive-≤ : f ≤ g → is-coreflexive g → is-coreflexive f +coreflexive-≤ w g-corefl = ≤-trans w g-corefl +``` + +If $f$ is coreflexive, then it is transitive, cotransitive, and symmetric. + +```agda +coreflexive→transitive + : is-coreflexive f → is-transitive f +coreflexive→transitive {f = f} f-corefl = + f ∘ f ≤⟨ f-corefl ◀ f ⟩ + id ∘ f =⟨ idl _ ⟩ + f ≤∎ + +coreflexive→cotransitive + : is-coreflexive f → is-cotransitive f +coreflexive→cotransitive {f = f} f-corefl = + f ≤⟨ ≤-conj f ⟩ + f ∘ f † ∘ f ≤⟨ f ▶ ≤-eliml (coreflexive-dual f-corefl) ⟩ + f ∘ f ≤∎ + +coreflexive→symmetric + : is-coreflexive f → is-symmetric f +coreflexive→symmetric {f = f} f-corefl = + f ≤⟨ ≤-conj f ⟩ + f ∘ f † ∘ f ≤⟨ f-corefl ◆ ≤-refl ◆ f-corefl ⟩ + id ∘ f † ∘ id =⟨ idl _ ∙ idr _ ⟩ + f † ≤∎ +``` +Furthermore, composition of coreflexive morphisms is equivalent to +intersection. + +```agda +coreflexive-∘-∩ + : ∀ {x} {f g : Hom x x} + → is-coreflexive f → is-coreflexive g + → f ∘ g ≡ f ∩ g +coreflexive-∘-∩ {f = f} {g = g} f-corefl g-corefl = + ≤-antisym ≤-to ≤-from + where + ≤-to : f ∘ g ≤ f ∩ g + ≤-to = ∩-univ (≤-elimr g-corefl) (≤-eliml f-corefl) + + ≤-from : f ∩ g ≤ f ∘ g + ≤-from = + cotransitive-∩-∘ $ + coreflexive→cotransitive $ + coreflexive-∩ f-corefl g-corefl +``` + +## Domains + +The domain of a morphism $f : X \to Y$ is defined as +$id \cap (f^o \circ f)$, denoted $\rm{dom}(f)$. +In $\Rel$, the domain of a relation $R : X \times Y \to \Omega$ is a +relation $X \times X \to \Omega$ that relates two elements $x, x' : X$ +whenever $x = x'$, and $R(x,y)$ for some $y$. + +```agda +domain : Hom x y → Hom x x +domain f = id ∩ f † ∘ f +``` + +The domain of a morphism is always coreflexive. + +```agda +domain-coreflexive : ∀ (f : Hom x y) → is-coreflexive (domain f) +domain-coreflexive f = ∩-le-l +``` + +Furthermore, the domain enjoys the following universal property: +Let $f : X \to Y$ and $g : X \to X$ such that $g$ is coreflexive. +Then $\rm{dom}(f) \le g$ if and only if $f \le f \circ g$. + +```agda +domain-universalr : is-coreflexive g → domain f ≤ g → f ≤ f ∘ g +domain-universalr {g = g} {f = f} g-corefl w = + f ≤⟨ ∩-univ (≤-intror ≤-refl) ≤-refl ⟩ + (f ∘ id) ∩ f ≤⟨ modular id f f ⟩ + f ∘ (id ∩ f † ∘ f) ≤⟨ f ▶ w ⟩ + f ∘ g ≤∎ + +domain-universall : is-coreflexive g → f ≤ f ∘ g → domain f ≤ g +domain-universall {g = g} {f = f} g-corefl w = + id ∩ (f † ∘ f) ≤⟨ ∩-pres-r (≤-pushr w) ⟩ + id ∩ ((f † ∘ f) ∘ g) =⟨ ∩-comm ⟩ + ((f † ∘ f) ∘ g) ∩ id ≤⟨ modular′ g (f † ∘ f) id ⟩ + (f † ∘ f ∩ id ∘ g †) ∘ g ≤⟨ ≤-trans ∩-le-r (≤-eliml ≤-refl) ◀ g ⟩ + g † ∘ g ≤⟨ ≤-eliml (coreflexive-dual g-corefl) ⟩ + g ≤∎ +``` + +We can nicely characterize the domain of an intersection. + +```agda +domain-∩ : domain (f ∩ g) ≡ id ∩ f † ∘ g +domain-∩ {f = f} {g = g} = ≤-antisym ≤-to ≤-from where + ≤-to : domain (f ∩ g) ≤ id ∩ f † ∘ g + ≤-to = + ∩-univ + (domain-coreflexive (f ∩ g)) + (≤-trans ∩-le-r (dual-≤ ∩-le-l ◆ ∩-le-r)) + + ≤-from : id ∩ f † ∘ g ≤ domain (f ∩ g) + ≤-from = + id ∩ f † ∘ g ≤⟨ ∩-univ ∩-le-l (∩-univ (∩-univ ∩-le-r ∩-le-l) ∩-le-l ) ⟩ + id ∩ (f † ∘ g ∩ id) ∩ id ≤⟨ ∩-pres-r (∩-pres-l (modular g (f †) id)) ⟩ + id ∩ (f † ∘ (g ∩ ⌜ f † † ∘ id ⌝)) ∩ id =⟨ ap! (idr _ ∙ dual f) ⟩ + id ∩ (f † ∘ (g ∩ f)) ∩ id ≤⟨ ∩-pres-r (modular′ (g ∩ f) (f †) id) ⟩ + id ∩ (f † ∩ ⌜ id ∘ (g ∩ f) † ⌝) ∘ (g ∩ f) =⟨ ap! (idl _) ⟩ + id ∩ (f † ∩ ⌜ g ∩ f ⌝ †) ∘ ⌜ g ∩ f ⌝ =⟨ ap! ∩-comm ⟩ + id ∩ (f † ∩ (f ∩ g) †) ∘ (f ∩ g) ≤⟨ ∩-pres-r (∩-le-r ◀ (f ∩ g)) ⟩ + id ∩ (f ∩ g) † ∘ (f ∩ g) ≤∎ +``` + +Furthermore, the domain of $f \circ g$ is contained in the domain of +$g$. + +```agda +domain-∘ : domain (f ∘ g) ≤ domain g +domain-∘ {f = f} {g = g} = + domain-universall (domain-coreflexive g) $ + ≤-pushr (domain-universalr (domain-coreflexive g) ≤-refl) +``` + +If $f \le g$, then $\rm{dom}(f) \le \rm{dom}(g)$. + +```agda +domain-≤ : f ≤ g → domain f ≤ domain g +domain-≤ w = ∩-pres-r (dual-≤ w ◆ w) +``` + +The domain of the identity morphism is simply the identity morphism. + +```agda +domain-id : domain (id {x}) ≡ id +domain-id = ≤-antisym ∩-le-l (∩-univ ≤-refl (≤-introl symmetric-id)) +``` + +# Antisymmetric Morphisms + +A morphism is **anti-symmetric** if $f \cap f^o \le id$. + +```agda +is-antisymmetric : Hom x x → Type _ +is-antisymmetric f = f ∩ f † ≤ id +``` + +Identity morphisms are anti-symmetric. + +```agda +antisymmetric-id + : is-antisymmetric (id {x}) +antisymmetric-id = + id ∩ ⌜ id † ⌝ =⟨ ap! (dual-id A) ⟩ + id ∩ id =⟨ ∩-idempotent ⟩ + id ≤∎ +``` + +If $f \le g$ and $g$ is anti-symmetric, then $f$ is anti-symmetric. + +```agda +antisymmetric-≤ + : f ≤ g → is-antisymmetric g → is-antisymmetric f +antisymmetric-≤ {f = f} {g = g} w g-antisym = + f ∩ f † ≤⟨ ∩-pres w (dual-≤ w) ⟩ + g ∩ g † ≤⟨ g-antisym ⟩ + id ≤∎ +``` + +If $f$ is anti-symmetric and reflexive, then $f \cap f^o = id$. + +```agda +reflexive+antisymmetric→diagonal + : is-reflexive f → is-antisymmetric f → f ∩ f † ≡ id +reflexive+antisymmetric→diagonal f-refl f-antisym = + ≤-antisym f-antisym (reflexive→diagonal f-refl) +``` diff --git a/src/Cat/Allegory/Reasoning.lagda.md b/src/Cat/Allegory/Reasoning.lagda.md index cac1bead3..26355c4d6 100644 --- a/src/Cat/Allegory/Reasoning.lagda.md +++ b/src/Cat/Allegory/Reasoning.lagda.md @@ -16,7 +16,7 @@ module Cat.Allegory.Reasoning {o ℓ ℓ′} (A : Allegory o ℓ ℓ′) where ```agda open Allegory A public open Cat.Reasoning (A .Allegory.cat) - hiding (module HLevel-instance ; Ob ; Hom ; id ; idl ; idr ; assoc ; _∘_) + hiding (module HLevel-instance ; Ob ; Hom; Hom-set ; id ; idl ; idr ; assoc ; _∘_) public ``` @@ -32,7 +32,7 @@ inequality, and rewriting by an equality: ```agda private variable w x y z : Ob - f f′ g g′ h : Hom x y + a b c d f f′ g g′ h : Hom x y _≤⟨_⟩_ : ∀ (f : Hom x y) → f ≤ g → g ≤ h → f ≤ h _=⟨_⟩_ : ∀ (f : Hom x y) → f ≡ g → g ≤ h → f ≤ h @@ -69,6 +69,7 @@ ordering in both of its arguments. ```agda ∩-pres-r : g ≤ g′ → f ∩ g ≤ f ∩ g′ ∩-pres-l : f ≤ f′ → f ∩ g ≤ f′ ∩ g +∩-pres : f ≤ f′ → g ≤ g′ → f ∩ g ≤ f′ ∩ g′ ∩-distribl : f ∘ (g ∩ h) ≤ (f ∘ g) ∩ (f ∘ h) ∩-distribr : (g ∩ h) ∘ f ≤ (g ∘ f) ∩ (h ∘ f) ∩-assoc : (f ∩ g) ∩ h ≡ f ∩ (g ∩ h) @@ -80,6 +81,7 @@ ordering in both of its arguments. ```agda ∩-pres-r w = ∩-univ ∩-le-l (≤-trans ∩-le-r w) ∩-pres-l w = ∩-univ (≤-trans ∩-le-l w) ∩-le-r +∩-pres w v = ∩-univ (≤-trans ∩-le-l w) (≤-trans ∩-le-r v) ∩-distribl = ∩-univ (_ ▶ ∩-le-l) (_ ▶ ∩-le-r) ∩-distribr = ∩-univ (∩-le-l ◀ _) (∩-le-r ◀ _) ∩-assoc = ≤-antisym @@ -112,3 +114,92 @@ modular′ f g h = †-inner p = ap₂ _∘_ refl dual-∘ ∙ sym (assoc _ _ _) ∙ ap₂ _∘_ refl (assoc _ _ _ ∙ ap₂ _∘_ p refl) ``` + +## Identities + +```agda +abstract + ≤-eliml : f ≤ id → f ∘ g ≤ g + ≤-eliml {f = f} {g = g} w = + f ∘ g ≤⟨ w ◀ g ⟩ + id ∘ g =⟨ idl _ ⟩ + g ≤∎ + + ≤-elimr : g ≤ id → f ∘ g ≤ f + ≤-elimr {g = g} {f = f} w = + f ∘ g ≤⟨ f ▶ w ⟩ + f ∘ id =⟨ idr _ ⟩ + f ≤∎ + + ≤-introl : id ≤ f → g ≤ f ∘ g + ≤-introl {f = f} {g = g} w = + g =⟨ sym (idl _) ⟩ + id ∘ g ≤⟨ w ◀ g ⟩ + f ∘ g ≤∎ + + ≤-intror : id ≤ g → f ≤ f ∘ g + ≤-intror {g = g} {f = f} w = + f =⟨ sym (idr _) ⟩ + f ∘ id ≤⟨ f ▶ w ⟩ + f ∘ g ≤∎ +``` + +## Associations + +```agda + ≤-pushl : a ≤ b ∘ c → a ∘ f ≤ b ∘ c ∘ f + ≤-pushl {a = a} {b = b} {c = c} {f = f} w = + a ∘ f ≤⟨ w ◀ f ⟩ + (b ∘ c) ∘ f =⟨ sym (assoc b c f) ⟩ + b ∘ c ∘ f ≤∎ + + ≤-pushr : a ≤ b ∘ c → f ∘ a ≤ (f ∘ b) ∘ c + ≤-pushr {a = a} {b = b} {c = c} {f = f} w = + f ∘ a ≤⟨ f ▶ w ⟩ + f ∘ b ∘ c =⟨ assoc f b c ⟩ + (f ∘ b) ∘ c ≤∎ + + ≤-pulll : a ∘ b ≤ c → a ∘ b ∘ f ≤ c ∘ f + ≤-pulll {a = a} {b = b} {c = c} {f = f} w = + a ∘ b ∘ f =⟨ assoc a b f ⟩ + (a ∘ b) ∘ f ≤⟨ w ◀ f ⟩ + c ∘ f ≤∎ + + ≤-pullr : a ∘ b ≤ c → (f ∘ a) ∘ b ≤ f ∘ c + ≤-pullr {a = a} {b = b} {c = c} {f = f} w = + (f ∘ a) ∘ b =⟨ sym (assoc f a b) ⟩ + f ∘ a ∘ b ≤⟨ f ▶ w ⟩ + f ∘ c ≤∎ + + ≤-extendl : a ∘ b ≤ c ∘ d → a ∘ b ∘ f ≤ c ∘ d ∘ f + ≤-extendl {a = a} {b = b} {c = c} {d = d} {f = f} w = + a ∘ b ∘ f ≤⟨ ≤-pulll w ⟩ + (c ∘ d) ∘ f =⟨ sym (assoc c d f) ⟩ + c ∘ d ∘ f ≤∎ + + ≤-extendr : a ∘ b ≤ c ∘ d → (f ∘ a) ∘ b ≤ (f ∘ c) ∘ d + ≤-extendr {a = a} {b = b} {c = c} {d = d} {f = f} w = + (f ∘ a) ∘ b ≤⟨ ≤-pullr w ⟩ + f ∘ c ∘ d =⟨ assoc f c d ⟩ + (f ∘ c) ∘ d ≤∎ + + ≤-pull-inner : a ∘ b ≤ c → (f ∘ a) ∘ (b ∘ g) ≤ f ∘ c ∘ g + ≤-pull-inner w = ≤-pullr (≤-pulll w) + + ≤-pull-outer : a ∘ b ≤ f → c ∘ d ≤ g → a ∘ (b ∘ c) ∘ d ≤ f ∘ g + ≤-pull-outer w v = ≤-trans (≤-pulll (≤-pulll w)) (≤-pullr v) + + ≤-extend-inner : a ∘ b ≤ c ∘ d → (f ∘ a) ∘ (b ∘ g) ≤ (f ∘ c) ∘ (d ∘ g) + ≤-extend-inner w = ≤-extendr (≤-extendl w) +``` + +## Duals + +```agda + ≤-conj : ∀ (f : Hom x x) → f ≤ f ∘ f † ∘ f + ≤-conj f = + f ≤⟨ ∩-univ (≤-introl ≤-refl) ≤-refl ⟩ + (id ∘ f) ∩ f ≤⟨ modular′ f id f ⟩ + (id ∩ (f ∘ f †)) ∘ f ≤⟨ ≤-pushl ∩-le-r ⟩ + f ∘ f † ∘ f ≤∎ +``` diff --git a/src/index.lagda.md b/src/index.lagda.md index 4c33ee3b7..e3f5ef206 100644 --- a/src/index.lagda.md +++ b/src/index.lagda.md @@ -603,6 +603,7 @@ the extra coherence that is necessary for specifying a bicategory. ```agda open import Cat.Allegory.Base -- The definition open import Cat.Allegory.Maps -- Functional relations in an allegory +open import Cat.Allegory.Morphism -- Morphisms in allegories open import Cat.Allegory.Reasoning -- Reasoning combinators ``` From e7af7527ce7da67f3aa18b7ab966247d0481783f Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sun, 6 Aug 2023 07:32:58 +0100 Subject: [PATCH 3/5] Restriction categories (#247) This PR defines restriction categories, and proves that every allegory has a restriction structure on its category of partial maps. --- src/Cat/Allegory/Maps.lagda.md | 39 +- src/Cat/Allegory/Morphism.lagda.md | 283 +++++++++- src/Cat/Allegory/Reasoning.lagda.md | 46 +- src/Cat/Restriction/Base.lagda.md | 100 ++++ src/Cat/Restriction/Functor.lagda.md | 148 +++++ .../Restriction/Instances/Allegory.lagda.md | 70 +++ src/Cat/Restriction/Reasoning.lagda.md | 525 ++++++++++++++++++ src/Cat/Restriction/Total.lagda.md | 64 +++ src/index.lagda.md | 24 + src/preamble.tex | 2 + 10 files changed, 1260 insertions(+), 41 deletions(-) create mode 100644 src/Cat/Restriction/Base.lagda.md create mode 100644 src/Cat/Restriction/Functor.lagda.md create mode 100644 src/Cat/Restriction/Instances/Allegory.lagda.md create mode 100644 src/Cat/Restriction/Reasoning.lagda.md create mode 100644 src/Cat/Restriction/Total.lagda.md diff --git a/src/Cat/Allegory/Maps.lagda.md b/src/Cat/Allegory/Maps.lagda.md index fa115c72c..8517a158f 100644 --- a/src/Cat/Allegory/Maps.lagda.md +++ b/src/Cat/Allegory/Maps.lagda.md @@ -3,7 +3,7 @@ open import Cat.Allegory.Base open import Cat.Prelude -import Cat.Allegory.Reasoning as Ar +import Cat.Allegory.Morphism ``` --> @@ -20,28 +20,32 @@ some category of "sets and relations", to recover the associated category of "sets and functions". So, let's start by thinking about $\Rel$! If you have a relation $R \mono A \times B$, when does it correspond to -a function $A \to B$? Well, it must definitely be _functional_: if we +a function $A \to B$? Well, it must definitely be [functional]: if we want $R(x, y)$ to represent "$f(x) = y$", then surely if $R(x, y) \land R(x, z)$, we must have $y = z$. In allegorical language, we would say $RR^o \le \id$, which we can calculate to mean (in $\Rel$) that, for all $x, y$, +[functional]: Cat.Allegory.Morphism.html#functional-morphisms + $$ (\exists z, R(z, x) \land R(z, y)) \to (x = y)\text{.} $$ -It must also be an _entire_ relation: Every $x$ must at least one $y$ it +It must also be an [entire] relation: Every $x$ must at least one $y$ it is related to, and by functionality, _exactly_ one $y$ it is related to. This is the "value of" the function at $y$. +[entire]: Cat.Allegory.Morphism.html#entire-morphisms + ```agda module _ {o ℓ h} (A : Allegory o ℓ h) where - open Allegory A + open Cat.Allegory.Morphism A record is-map x y (f : Hom x y) : Type h where constructor mapping field - functional : f ∘ f † ≤ id - entire : id ≤ f † ∘ f + functional : is-functional f + entire : is-entire f module _ {o ℓ h} {A : Allegory o ℓ h} where open Allegory A @@ -87,7 +91,7 @@ arbitrary relations). ```agda module _ {o ℓ h} (A : Allegory o ℓ h) where - private module A = Ar A + private module A = Cat.Allegory.Morphism A open is-map open Precategory hiding (_∘_ ; id) open A using (_† ; _∘_ ; id ; _◀_ ; _▶_) @@ -106,21 +110,12 @@ using those words. ```agda Maps[_] .Precategory.id = A.id , mapping - (subst (A._≤ id) (sym (A.idl _ ∙ dual-id A)) A.≤-refl) - (subst (id A.≤_) (sym (A.idr _ ∙ dual-id A)) A.≤-refl) - - Maps[_] .Precategory._∘_ (f , m) (g , m′) = f A.∘ g , mapping - ( (f ∘ g) ∘ (f ∘ g) † A.=⟨ A.†-inner refl ⟩ - f ∘ (g ∘ g †) ∘ f † A.≤⟨ f ▶ m′ .functional ◀ f † ⟩ - f ∘ id ∘ f † A.=⟨ A.refl⟩∘⟨ A.idl _ ⟩ - f ∘ f † A.≤⟨ m .functional ⟩ - id A.≤∎ ) - ( id A.≤⟨ m′ .entire ⟩ - g † ∘ g A.=⟨ ap (g † ∘_) (sym (A.idl _)) ⟩ - g † ∘ id ∘ g A.≤⟨ g † ▶ m .entire ◀ g ⟩ - g † ∘ (f † ∘ f) ∘ g A.=⟨ A.pulll (A.pulll (sym A.dual-∘)) ∙ A.pullr refl ⟩ - (f ∘ g) † ∘ (f ∘ g) A.≤∎ ) - + A.functional-id + A.entire-id + Maps[_] .Precategory._∘_ (f , m) (g , m′) = + f A.∘ g , mapping + (A.functional-∘ (m .functional) (m′ .functional)) + (A.entire-∘ (m .entire) (m′ .entire)) Maps[_] .idr f = Σ-prop-path (λ _ → hlevel 1) (A.idr _) Maps[_] .idl f = Σ-prop-path (λ _ → hlevel 1) (A.idl _) Maps[_] .assoc f g h = Σ-prop-path (λ _ → hlevel 1) (A.assoc _ _ _) diff --git a/src/Cat/Allegory/Morphism.lagda.md b/src/Cat/Allegory/Morphism.lagda.md index a045f3ac2..10b81626c 100644 --- a/src/Cat/Allegory/Morphism.lagda.md +++ b/src/Cat/Allegory/Morphism.lagda.md @@ -1,9 +1,11 @@ @@ -14,6 +16,7 @@ module Cat.Allegory.Morphism {o ℓ ℓ'} (A : Allegory o ℓ ℓ') where + Furthermore, the domain enjoys the following universal property: Let $f : X \to Y$ and $g : X \to X$ such that $g$ is coreflexive. -Then $\rm{dom}(f) \le g$ if and only if $f \le f \circ g$. +Then $\rm{dom}(f) \le g$ if and only if $f \le fg$. ```agda domain-universalr : is-coreflexive g → domain f ≤ g → f ≤ f ∘ g @@ -418,6 +553,16 @@ domain-universall {g = g} {f = f} g-corefl w = g ≤∎ ``` +This has a nice corollary: $f\rm{dom}(f) = f$. + +```agda +domain-absorb : ∀ (f : Hom x y) → f ∘ domain f ≡ f +domain-absorb f = + ≤-antisym + domain-elimr + (domain-universalr (domain-coreflexive f) ≤-refl) +``` + We can nicely characterize the domain of an intersection. ```agda @@ -441,8 +586,7 @@ domain-∩ {f = f} {g = g} = ≤-antisym ≤-to ≤-from where id ∩ (f ∩ g) † ∘ (f ∩ g) ≤∎ ``` -Furthermore, the domain of $f \circ g$ is contained in the domain of -$g$. +Furthermore, the domain of $fg$ is contained in the domain of $g$. ```agda domain-∘ : domain (f ∘ g) ≤ domain g @@ -465,6 +609,111 @@ domain-id : domain (id {x}) ≡ id domain-id = ≤-antisym ∩-le-l (∩-univ ≤-refl (≤-introl symmetric-id)) ``` +Characterizing composition of domains is somewhat more difficult, +though it is possible. Namely, we shall show the following: + +$$\rm{dom}(f\rm{dom}(g)) = \rm{dom}(f)\rm{dom}(g)$$ + +```agda +domain-smashr + : ∀ (f : Hom x z) (g : Hom x y) + → domain (f ∘ domain g) ≡ domain f ∘ domain g +domain-smashr f g = ≤-antisym ≤-to ≤-from where +``` + +We begin by noting that the composition $\rm{dom}(f)\rm{dom}(g)$ +is coreflexive. + +```agda + fg-corefl : is-coreflexive (domain f ∘ domain g) + fg-corefl = coreflexive-∘ (domain-coreflexive f) (domain-coreflexive g) +``` + +To show the forward direction, we can apply the universal property of +domains to transform the goal into + +$$f\rm{dom}(g) \le (f\rm{dom}(g))(\rm{dom}(f)\rm{dom}(g))$$ + +We can then solve this goal by repeatedly appealing to the fact that +domains are coreflexive. + +```agda + ≤-to : domain (f ∘ domain g) ≤ domain f ∘ domain g + ≤-to = + domain-universall fg-corefl $ + f ∘ domain g =˘⟨ ap₂ _∘_ (domain-absorb f) domain-idempotent ⟩ + (f ∘ domain f) ∘ (domain g ∘ domain g) =⟨ extendl (extendr domain-comm) ⟩ + (f ∘ domain g) ∘ (domain f ∘ domain g) ≤∎ +``` + +To show the reverse direction, we apply the universal property of the +intersection, reducing the goal to + +$$\rm{dom}(f)\rm{dom}(g) \le (f\rm{dom}(g))^of\rm{dom}(g)$$ + +We then solve the goal by an extended series of appeals to the +coreflexivity of domains. + +```agda + ≤-from : domain f ∘ domain g ≤ domain (f ∘ domain g) + ≤-from = ∩-univ fg-corefl $ + domain f ∘ domain g =˘⟨ ap (domain f ∘_) domain-idempotent ⟩ + domain f ∘ domain g ∘ domain g =⟨ extendl domain-comm ⟩ + domain g ∘ domain f ∘ domain g =⟨ ap (_∘ domain f ∘ domain g) (sym domain-dual) ⟩ + domain g † ∘ domain f ∘ domain g ≤⟨ domain g † ▶ ∩-le-r ◀ domain g ⟩ + domain g † ∘ (f † ∘ f) ∘ domain g =⟨ extendl (pulll (sym dual-∘)) ⟩ + (f ∘ domain g) † ∘ f ∘ domain g ≤∎ +``` + +We can also characterize postcomposition by a domain, though this +is restricted to an inequality in the general case. + +```agda +domain-swapl + : ∀ (f : Hom y z) (g : Hom x y) + → domain f ∘ g ≤ g ∘ domain (f ∘ g) +domain-swapl f g = + (id ∩ (f † ∘ f)) ∘ g ≤⟨ ∩-distribr ⟩ + (id ∘ g ∩ (f † ∘ f) ∘ g) =⟨ ap₂ _∩_ id-comm-sym (sym (assoc (f †) f g)) ⟩ + (g ∘ id ∩ f † ∘ f ∘ g) ≤⟨ modular id g (f † ∘ f ∘ g) ⟩ + g ∘ (id ∩ ⌜ g † ∘ f † ∘ f ∘ g ⌝) =⟨ ap! (pulll (sym dual-∘)) ⟩ + g ∘ (id ∩ (f ∘ g) † ∘ (f ∘ g)) ≤∎ +``` + +We can strengthen this to an equality when $g$ is functional. + +```agda +domain-swap + : ∀ (f : Hom y z) (g : Hom x y) + → is-functional g + → domain f ∘ g ≡ g ∘ domain (f ∘ g) +domain-swap f g w = + ≤-antisym (domain-swapl f g) $ + g ∘ (id ∩ (f ∘ g) † ∘ (f ∘ g)) ≤⟨ ∩-distribl ⟩ + g ∘ id ∩ g ∘ (f ∘ g) † ∘ (f ∘ g) ≤⟨ ∩-pres-r (≤-extendl (†-pulll w)) ⟩ + g ∘ id ∩ id ∘ f † ∘ f ∘ g =⟨ ap₂ _∩_ id-comm (idl _) ⟩ + id ∘ g ∩ f † ∘ f ∘ g ≤⟨ modular′ g id (f † ∘ f ∘ g) ⟩ + (id ∩ (f † ∘ f ∘ g) ∘ g †) ∘ g ≤⟨ ∩-pres-r (≤-pullr (≤-cancelr w)) ◀ g ⟩ + (id ∩ f † ∘ f) ∘ g ≤∎ +``` + +We also note that domains are always functional. + +```agda +domain-functional : (f : Hom x y) → is-functional (domain f) +domain-functional f = coreflexive→functional (domain-coreflexive f) +``` + +The domain of an entire morphism is the identity. + +```agda +domain-entire : is-entire f → domain f ≡ id +domain-entire f-entire = + ≤-antisym + (domain-coreflexive _) + (∩-univ ≤-refl f-entire) +``` + # Antisymmetric Morphisms A morphism is **anti-symmetric** if $f \cap f^o \le id$. @@ -504,3 +753,13 @@ reflexive+antisymmetric→diagonal reflexive+antisymmetric→diagonal f-refl f-antisym = ≤-antisym f-antisym (reflexive→diagonal f-refl) ``` + +If $f$ is coreflexive, then it is anti-symmetric. + +```agda +coreflexive→antisymmetric : is-coreflexive f → is-antisymmetric f +coreflexive→antisymmetric {f = f} f-corefl = + f ∩ f † ≤⟨ ∩-pres f-corefl (coreflexive-dual f-corefl) ⟩ + id ∩ id =⟨ ∩-idempotent ⟩ + id ≤∎ +``` diff --git a/src/Cat/Allegory/Reasoning.lagda.md b/src/Cat/Allegory/Reasoning.lagda.md index 26355c4d6..ac35dbc85 100644 --- a/src/Cat/Allegory/Reasoning.lagda.md +++ b/src/Cat/Allegory/Reasoning.lagda.md @@ -32,7 +32,7 @@ inequality, and rewriting by an equality: ```agda private variable w x y z : Ob - a b c d f f′ g g′ h : Hom x y + a b c d f f′ g g′ h i : Hom x y _≤⟨_⟩_ : ∀ (f : Hom x y) → f ≤ g → g ≤ h → f ≤ h _=⟨_⟩_ : ∀ (f : Hom x y) → f ≡ g → g ≤ h → f ≤ h @@ -72,6 +72,7 @@ ordering in both of its arguments. ∩-pres : f ≤ f′ → g ≤ g′ → f ∩ g ≤ f′ ∩ g′ ∩-distribl : f ∘ (g ∩ h) ≤ (f ∘ g) ∩ (f ∘ h) ∩-distribr : (g ∩ h) ∘ f ≤ (g ∘ f) ∩ (h ∘ f) +∩-distrib : (f ∩ g) ∘ (h ∩ i) ≤ (f ∘ h ∩ g ∘ h) ∩ (f ∘ i ∩ g ∘ i) ∩-assoc : (f ∩ g) ∩ h ≡ f ∩ (g ∩ h) ∩-comm : f ∩ g ≡ g ∩ f ∩-idempotent : f ∩ f ≡ f @@ -84,6 +85,7 @@ ordering in both of its arguments. ∩-pres w v = ∩-univ (≤-trans ∩-le-l w) (≤-trans ∩-le-r v) ∩-distribl = ∩-univ (_ ▶ ∩-le-l) (_ ▶ ∩-le-r) ∩-distribr = ∩-univ (∩-le-l ◀ _) (∩-le-r ◀ _) +∩-distrib = ≤-trans ∩-distribl (∩-pres ∩-distribr ∩-distribr) ∩-assoc = ≤-antisym (∩-univ (≤-trans ∩-le-l ∩-le-l) (∩-univ (≤-trans ∩-le-l ∩-le-r) ∩-le-r)) @@ -109,12 +111,6 @@ modular′ f g h = (g ∩ h ∘ f †) ∘ f ≤∎ ``` -```agda -†-inner : (p : g ∘ g′ † ≡ h) → (f ∘ g) ∘ (f′ ∘ g′) † ≡ f ∘ h ∘ f′ † -†-inner p = ap₂ _∘_ refl dual-∘ ∙ sym (assoc _ _ _) - ∙ ap₂ _∘_ refl (assoc _ _ _ ∙ ap₂ _∘_ p refl) -``` - ## Identities ```agda @@ -193,6 +189,17 @@ abstract ≤-extend-inner w = ≤-extendr (≤-extendl w) ``` +## Cancellations + +```agda + ≤-cancell : a ∘ b ≤ id → a ∘ b ∘ f ≤ f + ≤-cancell w = ≤-trans (≤-pulll w) (≤-eliml ≤-refl) + + ≤-cancelr : a ∘ b ≤ id → (f ∘ a) ∘ b ≤ f + ≤-cancelr w = ≤-trans (≤-pullr w) (≤-elimr ≤-refl) +``` + + ## Duals ```agda @@ -202,4 +209,29 @@ abstract (id ∘ f) ∩ f ≤⟨ modular′ f id f ⟩ (id ∩ (f ∘ f †)) ∘ f ≤⟨ ≤-pushl ∩-le-r ⟩ f ∘ f † ∘ f ≤∎ + + †-pulll : a ∘ b † ≤ c → a ∘ (f ∘ b) † ≤ c ∘ f † + †-pulll {a = a} {b = b} {c = c} {f = f} w = + a ∘ (f ∘ b) † =⟨ ap (a ∘_) dual-∘ ⟩ + a ∘ b † ∘ f † ≤⟨ ≤-pulll w ⟩ + c ∘ f † ≤∎ + + †-pullr : a † ∘ b ≤ c → (a ∘ f) † ∘ b ≤ f † ∘ c + †-pullr {a = a} {b = b} {c = c} {f = f} w = + (a ∘ f) † ∘ b =⟨ ap (_∘ b) dual-∘ ⟩ + (f † ∘ a †) ∘ b ≤⟨ ≤-pullr w ⟩ + f † ∘ c ≤∎ + + †-inner : (p : g ∘ g′ † ≡ h) → (f ∘ g) ∘ (f′ ∘ g′) † ≡ f ∘ h ∘ f′ † + †-inner p = ap₂ _∘_ refl dual-∘ ∙ sym (assoc _ _ _) + ∙ ap₂ _∘_ refl (assoc _ _ _ ∙ ap₂ _∘_ p refl) + + †-cancell : a ∘ b † ≤ id → a ∘ (f ∘ b) † ≤ f † + †-cancell w = ≤-trans (†-pulll w) (≤-eliml ≤-refl) + + †-cancelr : a † ∘ b ≤ id → (a ∘ f) † ∘ b ≤ f † + †-cancelr w = ≤-trans (†-pullr w) (≤-elimr ≤-refl) + + †-cancel-inner : a ∘ b † ≤ id → (f ∘ a) ∘ (g ∘ b) † ≤ f ∘ g † + †-cancel-inner w = †-pulll (≤-cancelr w) ``` diff --git a/src/Cat/Restriction/Base.lagda.md b/src/Cat/Restriction/Base.lagda.md new file mode 100644 index 000000000..cf126f4ec --- /dev/null +++ b/src/Cat/Restriction/Base.lagda.md @@ -0,0 +1,100 @@ + + +```agda +module Cat.Restriction.Base where +``` + +# Restriction Categories + +Much of computer science involves the study of partial functions. +Unfortunately, partial functions are somewhat tedious to work with, +as they aren't really functions; they're relations! Furthermore, +we are often interested in *computable* partial functions; this means that +we can not identify partial functions $A \rightharpoonup B$ with total functions +$A \to \rm{Maybe}(B)$[^1]. This leaves us with a few possible approaches. +The most first approach that may come to mind is to encode partial functions +$A \rightharpoonup B$ as total functions from a subobject $X \mono A$. +Alternatively, we could find some construction that classifies +partial maps; this is what the naive `Maybe` approach attempted to do. +We could also just work with functional relations directly, though this +is ill-advised. + + + +[^1]: We can easily determine if functions into `Maybe` "diverge" +by checking if they return `nothing`. If we identify partial functions +with total functions into `Maybe`, we can decide if a partial function +terminates, which is extremely uncomputable! + +Each of these approaches has its own benefits and drawbacks, which +makes choosing one difficult. **Restriction categories** offer an +alternative, algebraic approach to the problem, allowing us to neatly +sidestep any questions about encodings. + +Our prototypical restriction category will be $\Par$, the category of +sets and partial functions. The key insight is that every partial function +$f : A \rightharpoonup B$ is defined on some domain $X \subseteq A$; +this yields a partial function $f \downarrow : A \rightharpoonup A$ +that maps $x$ to itself iff $f(x)$ is defined. We can generalize this +insight to an arbitrary category $\cC$ by equipping $\cC$ with an operation +$\restrict{(-)} : \cC(x,y) \to \cC(x,x)$. + +-- + + +```agda +record Restriction-category + {o ℓ} (C : Precategory o ℓ) + : Type (o ⊔ ℓ) where + no-eta-equality + open Cat.Reasoning C + field + _↓ : ∀ {x y} → Hom x y → Hom x x + + infix 50 _↓ +``` + +We require that $\restrict{(-)}$ satisfies 4 axioms: +- $f\restrict{f} = f$. In $\Par$, this corresponds to the fact that +$\restrict{f}(x)$ is defined to be $x$ iff $f$ is defined, so +precomposing with it does nothing. + +```agda + field + ↓-dom : ∀ {x y} → (f : Hom x y) → f ∘ (f ↓) ≡ f +``` + +- $\restrict{f}\restrict{g} = \restrict{g}\restrict{f}$. In $\Par$, +this falls out of the fact that restriction maps do not modify their +arguments, and it doesn't matter if $f$ diverges first or $g$ does; +all that matters is that it diverges! + +```agda + field + ↓-comm : ∀ {x y z} → (f : Hom x z) (g : Hom x y) → f ↓ ∘ g ↓ ≡ g ↓ ∘ f ↓ +``` + +- $\restrict{(g\restrict{f})} = \restrict{g}\restrict{f}$. This axiom +holds in the $\Par$, as $\restrict{(g\restrict{f})}(x)$ ignores the +action of $g$ on $x$, and focuses only on its termination. + +```agda + field + ↓-smashr : ∀ {x y z} → (f : Hom x z) (g : Hom x y) → (g ∘ f ↓) ↓ ≡ g ↓ ∘ f ↓ +``` + +- $\restrict{f} g = g \restrict{(f g)}$. This is the trickiest of the +bunch to understand in $\Par$. Note that if we postcompose $g$ with a +domain map $\restrict{f}$, then we still need to take into account the +action of $g$; furthermore, its domain of definition needs to be +restricted to image of $g$. + +```agda + field + ↓-swap : ∀ {x y z} → (f : Hom y z) (g : Hom x y) → f ↓ ∘ g ≡ g ∘ (f ∘ g) ↓ +``` diff --git a/src/Cat/Restriction/Functor.lagda.md b/src/Cat/Restriction/Functor.lagda.md new file mode 100644 index 000000000..7309d7668 --- /dev/null +++ b/src/Cat/Restriction/Functor.lagda.md @@ -0,0 +1,148 @@ + + +```agda +module Cat.Restriction.Functor where +``` + + + +# Restriction Functors + +A functor $F : \cC \to \cD$ between [restriction categories] is a +**restriction functor** if $F (\restrict{f}) = \restrict{(F f)}$. + +[restriction categories]: Cat.Restriction.Base.html + +```agda +is-restriction-functor + : ∀ {oc ℓc od ℓd} {C : Precategory oc ℓc} {D : Precategory od ℓd} + → (F : Functor C D) + → (C↓ : Restriction-category C) + → (D↓ : Restriction-category D) + → Type _ +is-restriction-functor {C = C} {D = D} F C↓ D↓ = + ∀ {x y} (f : C.Hom x y) → F .F₁ (f C.↓) ≡ (F .F₁ f D.↓) + where + module C = Cat.Restriction.Reasoning C↓ + module D = Cat.Restriction.Reasoning D↓ +``` + +The identity functor is a restriction functor, and restriction functors +are closed under composition. + +```agda +Id-restriction + : ∀ {oc ℓc} {C : Precategory oc ℓc} {C↓ : Restriction-category C} + → is-restriction-functor Id C↓ C↓ +Id-restriction f = refl + +F∘-restriction + : ∀ {oc ℓc od ℓd oe ℓe} + → {C : Precategory oc ℓc} {D : Precategory od ℓd} {E : Precategory oe ℓe} + → {C↓ : Restriction-category C} + → {D↓ : Restriction-category D} + → {E↓ : Restriction-category E} + → (F : Functor D E) (G : Functor C D) + → is-restriction-functor F D↓ E↓ → is-restriction-functor G C↓ D↓ + → is-restriction-functor (F F∘ G) C↓ E↓ +F∘-restriction F G F↓ G↓ f = ap (F .F₁) (G↓ f) ∙ F↓ (G .F₁ f) +``` + +# Properties of Restriction Functors + +Let $F : \cC \to \cD$ be a restriction functor. Note that $F$ preserves +[total morphisms] and [restriction idempotents]. + +[total morphisms]: Cat.Restriction.Reasoning.html#total-morphisms +[restriction idempotents]: Cat.Restriction.Reasoning.html#restriction-idempotents + + + +```agda + F-total : ∀ {x y} {f : C.Hom x y} → C.is-total f → D.is-total (F .F₁ f) + F-total {f = f} f-total = sym (F↓ f) ·· ap (F .F₁) f-total ·· F .F-id + + F-restrict-idem + : ∀ {x} {f : C.Hom x x} + → C.is-restriction-idempotent f + → D.is-restriction-idempotent (F .F₁ f) + F-restrict-idem {f = f} f-ridem = + F .F₁ f D.↓ ≡˘⟨ F↓ f ⟩ + F .F₁ (f C.↓) ≡⟨ ap (F .F₁) f-ridem ⟩ + F .F₁ f ∎ +``` + +Furthermore, if $g$ refines $f$, then $F(g)$ refines $F(f)$. + +```agda + F-≤ : ∀ {x y} {f g : C.Hom x y} → f C.≤ g → (F .F₁ f) D.≤ (F .F₁ g) + F-≤ {f = f} {g = g} f≤g = + F .F₁ g D.∘ F .F₁ f D.↓ ≡⟨ ap (F .F₁ g D.∘_) (sym (F↓ f)) ⟩ + F .F₁ g D.∘ F .F₁ (f C.↓) ≡⟨ sym (F .F-∘ g (f C.↓)) ⟩ + F .F₁ (g C.∘ f C.↓) ≡⟨ ap (F .F₁) f≤g ⟩ + F .F₁ f ∎ +``` + +Restriction functors also preserve restricted isomorphisms. + +```agda + F-restricted-inverses + : ∀ {x y} {f : C.Hom x y} {g : C.Hom y x} + → C.restricted-inverses f g + → D.restricted-inverses (F .F₁ f) (F .F₁ g) + F-restricted-inverses {f = f} {g = g} fg-inv = record + { ↓-invl = + F .F₁ f D.∘ F .F₁ g ≡˘⟨ F .F-∘ f g ⟩ + F .F₁ (f C.∘ g) ≡⟨ ap (F .F₁) fg-inv.↓-invl ⟩ + F .F₁ (g C.↓) ≡⟨ F↓ g ⟩ + F .F₁ g D.↓ ∎ + ; ↓-invr = + F .F₁ g D.∘ F .F₁ f ≡˘⟨ F .F-∘ g f ⟩ + F .F₁ (g C.∘ f) ≡⟨ ap (F .F₁) fg-inv.↓-invr ⟩ + F .F₁ (f C.↓) ≡⟨ F↓ f ⟩ + F .F₁ f D.↓ ∎ + } + where module fg-inv = C.restricted-inverses fg-inv + + F-restricted-invertible + : ∀ {x y} {f : C.Hom x y} + → C.is-restricted-invertible f + → D.is-restricted-invertible (F .F₁ f) + F-restricted-invertible f-inv = record + { ↓-inv = F .F₁ f-inv.↓-inv + ; ↓-inverses = F-restricted-inverses f-inv.↓-inverses + } + where module f-inv = C.is-restricted-invertible f-inv + + F-↓≅ : ∀ {x y} → x C.↓≅ y → F .F₀ x D.↓≅ F .F₀ y + F-↓≅ f = record + { ↓-to = F .F₁ f.↓-to + ; ↓-from = F .F₁ f.↓-from + ; ↓-inverses = F-restricted-inverses f.↓-inverses + } + where module f = C._↓≅_ f +``` diff --git a/src/Cat/Restriction/Instances/Allegory.lagda.md b/src/Cat/Restriction/Instances/Allegory.lagda.md new file mode 100644 index 000000000..b0abbe8c8 --- /dev/null +++ b/src/Cat/Restriction/Instances/Allegory.lagda.md @@ -0,0 +1,70 @@ + + +```agda +module Cat.Restriction.Instances.Allegory where +``` + +# Restriction Categories from Allegories + +Let $\cA$ be an [allegory], considered as a sort of generalized category +of "sets and relations". Much like we can recover a category of "sets and +functions" via the associated [category of maps], we can recover a category +of "sets and partial functions" by only restricting to [functional] +relations instead of functional _and_ [entire] relations. + +[allegory]: Cat.Allegory.Base.html +[category of maps]: Cat.Allegory.Maps.html +[functional]: Cat.Allegory.Morphism.html#functional-morphisms +[entire]: Cat.Allegory.Morphism.html#entire-morphisms + + + +```agda + Partial-maps-subcat : Wide-subcat {C = cat} ℓ' + Partial-maps-subcat .Wide-subcat.P = is-functional + Partial-maps-subcat .Wide-subcat.P-prop f = ≤-thin + Partial-maps-subcat .Wide-subcat.P-id = + functional-id + Partial-maps-subcat .Wide-subcat.P-∘ f-partial g-partial = + functional-∘ f-partial g-partial + + Partial-maps : Precategory o (ℓ ⊔ ℓ') + Partial-maps = Wide Partial-maps-subcat +``` + +This category can be equipped with a restriction structure, defining +$\restrict{f}$ to be the [domain] of the partial maps. +Note that the first 3 axioms don't actually require the relation to be +functional; it's only relevant in the converse direction of the 4th axiom! + +[domain]: Cat.Allegory.Morphism.html#domains + +```agda + Partial-maps-restriction : Restriction-category Partial-maps + Partial-maps-restriction ._↓ f .hom = domain (f .hom) + Partial-maps-restriction ._↓ f .witness = domain-functional (f .hom) + Partial-maps-restriction .↓-dom f = + Wide-hom-path $ domain-absorb (f .hom) + Partial-maps-restriction .↓-comm f g = + Wide-hom-path $ domain-comm + Partial-maps-restriction .↓-smashr f g = + Wide-hom-path $ domain-smashr (g .hom) (f .hom) + Partial-maps-restriction .↓-swap f g = + Wide-hom-path $ domain-swap (f .hom) (g .hom) (g .witness) +``` diff --git a/src/Cat/Restriction/Reasoning.lagda.md b/src/Cat/Restriction/Reasoning.lagda.md new file mode 100644 index 000000000..ac4638203 --- /dev/null +++ b/src/Cat/Restriction/Reasoning.lagda.md @@ -0,0 +1,525 @@ + + +```agda +module Cat.Restriction.Reasoning + {o ℓ} {C : Precategory o ℓ} + (C-restrict : Restriction-category C) + where +``` + + + +# Reasoning in Restriction Categories + +This module provides some useful lemmas about restriction categories. +We begin by noting that for every $f$, $\restrict{f}$ is an [idempotent]. + +[idempotent]: Cat.Diagram.Idempotent.html + +```agda +↓-idem : ∀ {x y} (f : Hom x y) → is-idempotent (f ↓) +↓-idem f = + f ↓ ∘ f ↓ ≡˘⟨ ↓-smashr f f ⟩ + (f ∘ f ↓) ↓ ≡⟨ ap _↓ (↓-dom f) ⟩ + f ↓ ∎ +``` + +Next, some useful lemmas about pre and postcomposition of a restriction +map. + +```agda +↓-cancelr : ∀ {x y z} (f : Hom y z) (g : Hom x y) → (f ∘ g) ↓ ∘ g ↓ ≡ (f ∘ g) ↓ +↓-cancelr f g = + (f ∘ g) ↓ ∘ g ↓ ≡˘⟨ ↓-smashr g (f ∘ g) ⟩ + ((f ∘ g) ∘ g ↓) ↓ ≡⟨ ap _↓ (pullr (↓-dom g)) ⟩ + (f ∘ g) ↓ ∎ + + +↓-cancell : ∀ {x y z} (f : Hom y z) (g : Hom x y) → g ↓ ∘ (f ∘ g) ↓ ≡ (f ∘ g) ↓ +↓-cancell f g = + g ↓ ∘ (f ∘ g) ↓ ≡⟨ ↓-comm g (f ∘ g) ⟩ + (f ∘ g) ↓ ∘ g ↓ ≡⟨ ↓-cancelr f g ⟩ + (f ∘ g) ↓ ∎ +``` + +We can use these to show that $\restrict{(\restrict{f}g)} = \restrict{(f \circ g)}$, +which is somewhat hard to motivate, but ends up being a useful algebraic +manipulation. + +```agda +↓-smashl : ∀ {x y z} (f : Hom y z) (g : Hom x y) → (f ↓ ∘ g) ↓ ≡ (f ∘ g) ↓ +↓-smashl f g = + ((f ↓) ∘ g) ↓ ≡⟨ ap _↓ (↓-swap f g) ⟩ + (g ∘ (f ∘ g) ↓) ↓ ≡⟨ ↓-smashr (f ∘ g) g ⟩ + g ↓ ∘ (f ∘ g) ↓ ≡⟨ ↓-cancell f g ⟩ + (f ∘ g) ↓ ∎ + +↓-smash : ∀ {x y z} (f : Hom x z) (g : Hom x y) → (f ↓ ∘ g ↓) ↓ ≡ f ↓ ∘ g ↓ +↓-smash f g = + (f ↓ ∘ g ↓) ↓ ≡⟨ ↓-smashl f (g ↓) ⟩ + (f ∘ g ↓) ↓ ≡⟨ ↓-smashr g f ⟩ + f ↓ ∘ g ↓ ∎ +``` + +Next, we note that iterating $(-)downarrow$ does nothing. + +```agda +↓-join : ∀ {x y} (f : Hom x y) → (f ↓) ↓ ≡ f ↓ +↓-join f = + (f ↓) ↓ ≡⟨ ap _↓ (sym (↓-idem f)) ⟩ + (f ↓ ∘ f ↓) ↓ ≡⟨ ↓-smashr f (f ↓) ⟩ + (f ↓) ↓ ∘ f ↓ ≡⟨ ↓-comm (f ↓) f ⟩ + f ↓ ∘ (f ↓) ↓ ≡⟨ ↓-dom (f ↓) ⟩ + f ↓ ∎ +``` + +## Total Morphisms + +We say that a morphism $f : X \to Y$ in a restriction category is **total** +if its restriction $\restrict{f}$ is the identity morphism. + +```agda +is-total : ∀ {x y} → Hom x y → Type _ +is-total f = f ↓ ≡ id + +record Total (x y : Ob) : Type ℓ where + no-eta-equality + field + mor : Hom x y + has-total : is-total mor + +open Total public +``` + +Being total is a proposition, so the collection of total morphisms +forms a set. + +```agda +is-total-is-prop : ∀ {x y} → (f : Hom x y) → is-prop (is-total f) +is-total-is-prop f = Hom-set _ _ _ _ + +Total-is-set : ∀ {x y} → is-set (Total x y) +``` + + + + +If $f$ is [monic], then it is a total morphism. + +[monic]: Cat.Morphism.html#monos + +```agda +monic→total : ∀ {x y} {f : Hom x y} → is-monic f → is-total f +monic→total {f = f} monic = monic (f ↓) id (↓-dom f ∙ sym (idr _)) +``` + +As a corollary, every isomorphism is total. + +```agda +invertible→total : ∀ {x y} {f : Hom x y} → is-invertible f → is-total f +invertible→total f-inv = monic→total (invertible→monic f-inv) +``` + +The identity morphism is total, as it is monic. + +```agda +id-total : ∀ {x} → is-total (id {x}) +id-total = monic→total id-monic +``` + +Total morphisms are closed under composition. + +```agda +total-∘ + : ∀ {x y z} {f : Hom y z} {g : Hom x y} + → is-total f → is-total g → is-total (f ∘ g) +total-∘ {f = f} {g = g} f-total g-total = + (f ∘ g) ↓ ≡˘⟨ ↓-smashl f g ⟩ + (f ↓ ∘ g) ↓ ≡⟨ ap _↓ (eliml f-total) ⟩ + g ↓ ≡⟨ g-total ⟩ + id ∎ + +_∘Total_ : ∀ {x y z} → Total y z → Total x y → Total x z +(f ∘Total g) .mor = f .mor ∘ g .mor +(f ∘Total g) .has-total = total-∘ (f .has-total) (g .has-total) +``` + +Furthermore, if $f \circ g$ is total, then $g$ must also be total. + +```agda +total-cancell + : ∀ {x y z} {f : Hom y z} {g : Hom x y} + → is-total (f ∘ g) → is-total g +total-cancell {f = f} {g = g} fg-total = + g ↓ ≡⟨ intror fg-total ⟩ + g ↓ ∘ (f ∘ g) ↓ ≡⟨ ↓-cancell f g ⟩ + (f ∘ g) ↓ ≡⟨ fg-total ⟩ + id ∎ +``` + +If $f$ is total, then $\restrict{(fg)} = \restrict{g}$. + +```agda +total-smashl + : ∀ {x y z} {f : Hom y z} {g : Hom x y} + → is-total f → (f ∘ g) ↓ ≡ g ↓ +total-smashl {f = f} {g = g} f-total = + (f ∘ g) ↓ ≡˘⟨ ↓-smashl f g ⟩ + (f ↓ ∘ g) ↓ ≡⟨ ap _↓ (eliml f-total) ⟩ + g ↓ ∎ +``` + +## Restriction Idempotents + +We say that a morphism $f : X \to X$ is a **restriction idempotent** if +$\restrict{f} = f$. + +```agda +is-restriction-idempotent : ∀ {x} → (f : Hom x x) → Type _ +is-restriction-idempotent f = f ↓ ≡ f +``` + +As the name suggests, restriction idempotents are idempotents. + +```agda +restriction-idempotent→idempotent + : ∀ {x} {f : Hom x x} + → is-restriction-idempotent f → is-idempotent f +restriction-idempotent→idempotent {f = f} f-dom = + f ∘ f ≡⟨ ap (f ∘_) (sym f-dom) ⟩ + f ∘ f ↓ ≡⟨ ↓-dom f ⟩ + f ∎ +``` + +Furthermore, every morphism $\restrict{f}$ is a restriction idempotent. + +```agda +↓-restriction-idempotent : ∀ {x y} (f : Hom x y) → is-restriction-idempotent (f ↓) +↓-restriction-idempotent f = ↓-join f +``` + +If $f$ and $g$ are restriction idempotents, then they commute. + +```agda +restriction-idem-comm + : ∀ {x} {f g : Hom x x} + → is-restriction-idempotent f → is-restriction-idempotent g + → f ∘ g ≡ g ∘ f +restriction-idem-comm f-dom g-dom = + ap₂ _∘_ (sym f-dom) (sym g-dom) + ·· ↓-comm _ _ + ·· ap₂ _∘_ g-dom f-dom +``` + +## Restricted Monics + +A morphism $f : X \to Y$ is a **restricted monic** if for all +$g, h : A \to X$, $fg = fh$ implies that $\restrict{f}g = \restrict{f}h$. +Intuitively, this is the correct notion of monic for a partial function; +we cannot guarantee that $g$ and $h$ are equal if $fg = fh$, as $f$ may +diverge on some inputs where $g$ and $h$ disagree. + +```agda +is-restricted-monic : ∀ {x y} → Hom x y → Type _ +is-restricted-monic {x} {y} f = + ∀ {a} → (g h : Hom a x) → f ∘ g ≡ f ∘ h → f ↓ ∘ g ≡ f ↓ ∘ h +``` + +If $f$ is a total restricted monic, then $f$ is monic. + +```agda +restricted-monic+total→monic + : ∀ {x y} {f : Hom x y} + → is-restricted-monic f → is-total f + → is-monic f +restricted-monic+total→monic {f = f} f-rmonic f-total g1 g2 p = + g1 ≡⟨ introl f-total ⟩ + f ↓ ∘ g1 ≡⟨ f-rmonic g1 g2 p ⟩ + f ↓ ∘ g2 ≡⟨ eliml f-total ⟩ + g2 ∎ +``` + +Restricted monics are closed under composition. + +```agda +restricted-monic-∘ + : ∀ {x y z} {f : Hom y z} {g : Hom x y} + → is-restricted-monic f → is-restricted-monic g + → is-restricted-monic (f ∘ g) +restricted-monic-∘ {f = f} {g = g} f-rmonic g-rmonic h1 h2 p = + (f ∘ g) ↓ ∘ h1 ≡⟨ pushl (sym (↓-cancell f g)) ⟩ + g ↓ ∘ (f ∘ g) ↓ ∘ h1 ≡⟨ g-rmonic _ _ g-lemma ⟩ + (g ↓) ∘ (f ∘ g) ↓ ∘ h2 ≡⟨ pulll (↓-cancell f g) ⟩ + (f ∘ g) ↓ ∘ h2 ∎ + where + p-assoc : f ∘ g ∘ h1 ≡ f ∘ g ∘ h2 + p-assoc = assoc _ _ _ ·· p ·· sym (assoc _ _ _) + + g-lemma : g ∘ (f ∘ g) ↓ ∘ h1 ≡ g ∘ (f ∘ g) ↓ ∘ h2 + g-lemma = + g ∘ (f ∘ g) ↓ ∘ h1 ≡⟨ extendl (sym (↓-swap f g)) ⟩ + f ↓ ∘ g ∘ h1 ≡⟨ f-rmonic _ _ p-assoc ⟩ + f ↓ ∘ g ∘ h2 ≡⟨ extendl (↓-swap f g) ⟩ + g ∘ (f ∘ g) ↓ ∘ h2 ∎ +``` + +Furthermore, if $fg$ is a restricted monic and $f$ is total, +then $g$ is a restricted monic. + +```agda +restricted-monic-cancell + : ∀ {x y z} {f : Hom y z} {g : Hom x y} + → is-restricted-monic (f ∘ g) + → is-total f + → is-restricted-monic g +restricted-monic-cancell {f = f} {g = g} fg-rmonic f-total h1 h2 p = + g ↓ ∘ h1 ≡⟨ ap (_∘ h1) (sym (total-smashl f-total)) ⟩ + (f ∘ g) ↓ ∘ h1 ≡⟨ fg-rmonic h1 h2 (sym (assoc _ _ _) ·· ap (f ∘_) p ·· assoc _ _ _) ⟩ + (f ∘ g) ↓ ∘ h2 ≡⟨ ap (_∘ h2) (total-smashl f-total) ⟩ + g ↓ ∘ h2 ∎ +``` + +## Restricted Retracts + +Let $r : X \to Y$ and $s : Y \to X$ be a pair of morphisms. The map +$r$ is a **restricted retract** of $s$ when $rs = \restrict{s}$. + +```agda +_restricted-retract-of_ : ∀ {x y} (r : Hom x y) (s : Hom y x) → Type _ +r restricted-retract-of s = r ∘ s ≡ s ↓ + +record has-restricted-retract {x y} (s : Hom y x) : Type ℓ where + no-eta-equality + field + ↓-retract : Hom x y + is-restricted-retract : ↓-retract restricted-retract-of s + +open has-restricted-retract public +``` + +If $f$ is total and has a restricted retract, then it has a retract. + +```agda +has-restricted-retract+total→has-retract + : ∀ {x y} {f : Hom x y} + → has-restricted-retract f → is-total f → has-retract f +has-restricted-retract+total→has-retract {f = f} f-sect f-total = + make-retract (f-sect .↓-retract) $ + f-sect .↓-retract ∘ f ≡⟨ f-sect .is-restricted-retract ⟩ + f ↓ ≡⟨ f-total ⟩ + id ∎ +``` + +If $s$ has a restricted retract, then it is a restricted mono. + +```agda +has-restricted-retract→restricted-monic + : ∀ {x y} {f : Hom x y} + → has-restricted-retract f + → is-restricted-monic f +has-restricted-retract→restricted-monic {f = f} f-sect g1 g2 p = + f ↓ ∘ g1 ≡⟨ pushl (sym $ f-sect .is-restricted-retract) ⟩ + f-sect .↓-retract ∘ f ∘ g1 ≡⟨ ap (f-sect .↓-retract ∘_) p ⟩ + f-sect .↓-retract ∘ f ∘ g2 ≡⟨ pulll (f-sect .is-restricted-retract) ⟩ + f ↓ ∘ g2 ∎ +``` + +If $f$ and $g$ have restricted retracts, then so does $fg$. + +```agda +restricted-retract-∘ + : ∀ {x y z} {f : Hom y z} {g : Hom x y} + → has-restricted-retract f → has-restricted-retract g + → has-restricted-retract (f ∘ g) +restricted-retract-∘ {f = f} {g = g} f-sect g-sect .↓-retract = + g-sect .↓-retract ∘ f-sect .↓-retract +restricted-retract-∘ {f = f} {g = g} f-sect g-sect .is-restricted-retract = + (g-sect .↓-retract ∘ f-sect .↓-retract) ∘ f ∘ g ≡⟨ pull-inner (f-sect .is-restricted-retract) ⟩ + g-sect .↓-retract ∘ f ↓ ∘ g ≡⟨ ap (g-sect .↓-retract ∘_) (↓-swap f g) ⟩ + g-sect .↓-retract ∘ g ∘ (f ∘ g) ↓ ≡⟨ pulll (g-sect .is-restricted-retract) ⟩ + g ↓ ∘ (f ∘ g) ↓ ≡⟨ ↓-cancell f g ⟩ + (f ∘ g) ↓ ∎ +``` + + +If $fg$ has a restricted retract and $f$ is total, then $g$ has a +restricted retract. + +```agda +has-restricted-retract-cancell + : ∀ {x y z} {f : Hom y z} {g : Hom x y} + → has-restricted-retract (f ∘ g) + → is-total f + → has-restricted-retract g +has-restricted-retract-cancell {f = f} fg-sect f-total .↓-retract = + fg-sect .↓-retract ∘ f +has-restricted-retract-cancell {f = f} {g = g} fg-sect f-total .is-restricted-retract = + (fg-sect .↓-retract ∘ f) ∘ g ≡⟨ sym (assoc _ _ _) ∙ fg-sect .is-restricted-retract ⟩ + (f ∘ g) ↓ ≡⟨ total-smashl f-total ⟩ + g ↓ ∎ +``` + +## Restricted Isomorphisms + +Let $f : X \to Y$ and $g : Y \to X$ be a pair of morphisms. $f$ and $g$ +are **restricted inverses** if $fg = \restrict{g}$ and +$gf = \restrict{f}$. + +```agda +record restricted-inverses + {x y} (f : Hom x y) (g : Hom y x) + : Type ℓ where + no-eta-equality + field + ↓-invl : f ∘ g ≡ g ↓ + ↓-invr : g ∘ f ≡ f ↓ + +open restricted-inverses + +record is-restricted-invertible {x y} (f : Hom x y) : Type ℓ where + no-eta-equality + field + ↓-inv : Hom y x + ↓-inverses : restricted-inverses f ↓-inv + + open restricted-inverses ↓-inverses public + +record _↓≅_ (x y : Ob) : Type ℓ where + no-eta-equality + field + ↓-to : Hom x y + ↓-from : Hom y x + ↓-inverses : restricted-inverses ↓-to ↓-from + + open restricted-inverses ↓-inverses public + +open _↓≅_ public +``` + +A given morphism is a has a unique restricted inverse. + +```agda +restricted-inverses-is-prop + : ∀ {x y} {f : Hom x y} {g : Hom y x} + → is-prop (restricted-inverses f g) +restricted-inverses-is-prop x y i .↓-invl = + Hom-set _ _ _ _ (x .↓-invl) (y .↓-invl) i +restricted-inverses-is-prop x y i .↓-invr = + Hom-set _ _ _ _ (x .↓-invr) (y .↓-invr) i + +is-restricted-invertible-is-prop + : ∀ {x y} {f : Hom x y} + → is-prop (is-restricted-invertible f) +is-restricted-invertible-is-prop {f = f} g h = p where + module g = is-restricted-invertible g + module h = is-restricted-invertible h + + g≡h : g.↓-inv ≡ h.↓-inv + g≡h = + g.↓-inv ≡˘⟨ ↓-dom _ ⟩ + g.↓-inv ∘ g.↓-inv ↓ ≡⟨ ap (g.↓-inv ∘_) (sym g.↓-invl) ⟩ + g.↓-inv ∘ f ∘ g.↓-inv ≡⟨ extendl (g.↓-invr ∙ sym h.↓-invr) ⟩ + h.↓-inv ∘ ⌜ f ⌝ ∘ g.↓-inv ≡⟨ ap! (sym (↓-dom f) ∙ ap (f ∘_) (sym h.↓-invr)) ⟩ + h.↓-inv ∘ (f ∘ h.↓-inv ∘ f) ∘ g.↓-inv ≡⟨ ap (h.↓-inv ∘_) (pullr (pullr g.↓-invl) ∙ pulll h.↓-invl) ⟩ + h.↓-inv ∘ h.↓-inv ↓ ∘ g.↓-inv ↓ ≡⟨ ap (h.↓-inv ∘_) (↓-comm _ _) ⟩ + h.↓-inv ∘ g.↓-inv ↓ ∘ h.↓-inv ↓ ≡⟨ ap (h.↓-inv ∘_) (pushl (sym g.↓-invl) ∙ pushr (pushr (sym h.↓-invl))) ⟩ + h.↓-inv ∘ ⌜ f ∘ g.↓-inv ∘ f ⌝ ∘ h.↓-inv ≡⟨ ap! (ap (f ∘_) g.↓-invr ∙ ↓-dom f) ⟩ + h.↓-inv ∘ f ∘ h.↓-inv ≡⟨ ap (h.↓-inv ∘_) (h.↓-invl) ⟩ + h.↓-inv ∘ h.↓-inv ↓ ≡⟨ ↓-dom _ ⟩ + h.↓-inv ∎ + + p : g ≡ h + p i .is-restricted-invertible.↓-inv = g≡h i + p i .is-restricted-invertible.↓-inverses = + is-prop→pathp (λ i → restricted-inverses-is-prop {f = f} {g = g≡h i}) + g.↓-inverses h.↓-inverses i +``` + +If $f$ and $g$ are both total and restricted inverses, then they are inverses. + +```agda +restricted-inverses+total→inverses + : ∀ {x y} {f : Hom x y} {g : Hom y x} + → restricted-inverses f g + → is-total f + → is-total g + → Inverses f g +restricted-inverses+total→inverses {f = f} {g = g} fg-inv f-total g-total = record + { invl = fg-inv .↓-invl ∙ g-total + ; invr = fg-inv .↓-invr ∙ f-total + } +``` + +## Refining Morphisms + +Let $\cC$ be a restriction category, and $f, g : \cC(X,Y)$. We say that +$g$ **refines** $f$ if $g$ agrees with $f$ when restricted to the domain of +$f$. + +```agda +_≤_ : ∀ {x y} → Hom x y → Hom x y → Type ℓ +f ≤ g = g ∘ f ↓ ≡ f +``` + +The refinement relation is reflexive, transitive, and anti-symmetric. + +```agda +≤-refl : ∀ {x y} {f : Hom x y} → f ≤ f +≤-refl {f = f} = ↓-dom f + +≤-trans : ∀ {x y} {f g h : Hom x y} → f ≤ g → g ≤ h → f ≤ h +≤-trans {f = f} {g = g} {h = h} p q = + h ∘ ⌜ f ⌝ ↓ ≡⟨ ap! (sym p) ⟩ + h ∘ (g ∘ (f ↓)) ↓ ≡⟨ ap (h ∘_) (↓-smashr f g) ⟩ + h ∘ g ↓ ∘ f ↓ ≡⟨ pulll q ⟩ + g ∘ f ↓ ≡⟨ p ⟩ + f ∎ + +≤-antisym : ∀ {x y} {f g : Hom x y} → f ≤ g → g ≤ f → f ≡ g +≤-antisym {f = f} {g = g} p q = + f ≡⟨ sym p ⟩ + g ∘ f ↓ ≡⟨ pushl (sym q) ⟩ + f ∘ g ↓ ∘ f ↓ ≡⟨ ap (f ∘_) (↓-comm g f) ⟩ + f ∘ f ↓ ∘ g ↓ ≡⟨ pulll (↓-dom f) ⟩ + f ∘ (g ↓) ≡⟨ q ⟩ + g ∎ +``` + +Furthermore, composition preserves refinement. + +```agda +∘-preserves-≤ + : ∀ {x y z} {f g : Hom y z} {h i : Hom x y} + → f ≤ g → h ≤ i → (f ∘ h) ≤ (g ∘ i) +∘-preserves-≤ {f = f} {g = g} {h = h} {i = i} p q = + (g ∘ i) ∘ ⌜ f ∘ h ⌝ ↓ ≡⟨ ap! (pushr (sym q)) ⟩ + (g ∘ i) ∘ ((f ∘ i) ∘ (h ↓)) ↓ ≡⟨ ap ((g ∘ i) ∘_) (↓-smashr h (f ∘ i)) ⟩ + (g ∘ i) ∘ (f ∘ i) ↓ ∘ h ↓ ≡⟨ extendr (extendl (sym (↓-swap f i))) ⟩ + (g ∘ f ↓) ∘ (i ∘ h ↓) ≡⟨ ap₂ _∘_ p q ⟩ + f ∘ h ∎ +``` diff --git a/src/Cat/Restriction/Total.lagda.md b/src/Cat/Restriction/Total.lagda.md new file mode 100644 index 000000000..154ab552e --- /dev/null +++ b/src/Cat/Restriction/Total.lagda.md @@ -0,0 +1,64 @@ + + +```agda +module Cat.Restriction.Total where +``` + +# The Subcategory of Total Maps + +Let $\cC$ be a restriction category. We can construct a +[wide subcategory] of $\cC$ containing only the [total maps] of $\cC$, +denoted $\thecat{Total}(\cC)$. + +[wide subcategory]: Cat.Functor.WideSubcategory.html +[total maps]: Cat.Restriction.Reasoning.html#total-morphisms + + + +```agda + Total-wide-subcat : Wide-subcat {C = C} ℓ + Total-wide-subcat .Wide-subcat.P = is-total + Total-wide-subcat .Wide-subcat.P-prop = is-total-is-prop + Total-wide-subcat .Wide-subcat.P-id = id-total + Total-wide-subcat .Wide-subcat.P-∘ = total-∘ + + Total-maps : Precategory o ℓ + Total-maps = Wide Total-wide-subcat +``` + + + +Furthermore, the injection from $\thecat{Total}(\cC)$ into $\cC$ is +[pseudomonic], as all isomorphisms in $\cC$ are total. + +[pseudomonic]: Cat.Functor.Properties.html#pseudomonic-functors + +```agda + + Forget-total : Functor (Total-maps C↓) C + Forget-total = Forget-wide-subcat + + Forget-total-pseudomonic + : is-pseudomonic Forget-total + Forget-total-pseudomonic = + is-pseudomonic-Forget-wide-subcat invertible→total +``` diff --git a/src/index.lagda.md b/src/index.lagda.md index e3f5ef206..6eb571ae1 100644 --- a/src/index.lagda.md +++ b/src/index.lagda.md @@ -607,6 +607,30 @@ open import Cat.Allegory.Morphism -- Morphisms in allegories open import Cat.Allegory.Reasoning -- Reasoning combinators ``` +## Restriction Categories + +Restriction categories axiomatize categories of partial maps by adding +n restriction operation $(-)\downarrow : \cC(X,Y) \to \cC(X,X)$ that +takes a morphism $f$ to a subobject of the identity morphism that is +defined precisely when $f$ is. + +```agda +open import Cat.Restriction.Base + -- The definition +open import Cat.Restriction.Functor + -- Functors between restriction categories +open import Cat.Restriction.Reasoning + -- Reasoning combinators and morphism classes +open import Cat.Restriction.Total + -- Categories of total maps +``` + +```agda +open import Cat.Restriction.Instances.Allegory + -- Restriction structures on partial maps of an allegory. +``` + + ## Displayed categories A category displayed over $\cB$ is a particular concrete presentation diff --git a/src/preamble.tex b/src/preamble.tex index f740b178a..edacb4994 100644 --- a/src/preamble.tex +++ b/src/preamble.tex @@ -38,6 +38,7 @@ \knowncat{Rings} \knowncat{Grp} \knowncat{Rel} +\knowncat{Par} \knownbicat{Cat} \knownbicat{Topos} \knownbicat{Grpd} @@ -76,6 +77,7 @@ \DeclareMathOperator{\src}{src} \DeclareMathOperator{\tgt}{tgt} +\newcommand{\restrict}[1]{#1^{\downarrow}} \newcommand{\NN}{\mathbb{N}} \newcommand{\ZZ}{\mathbb{Z}} From 09ed1f3eb8e59311ebb1dc47ec53c363c33a3125 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia?= Date: Thu, 10 Aug 2023 07:44:21 -0300 Subject: [PATCH 4/5] defn: Allegory of matrices with values in a frame (#248) --- src/1Lab/Type/Pi.lagda.md | 11 +++ src/1Lab/Type/Sigma.lagda.md | 7 ++ src/Cat/Allegory/Instances/Mat.lagda.md | 115 ++++++++++++++++++++++++ src/Order/Frame/Reasoning.lagda.md | 49 ++++++++++ 4 files changed, 182 insertions(+) create mode 100644 src/Cat/Allegory/Instances/Mat.lagda.md diff --git a/src/1Lab/Type/Pi.lagda.md b/src/1Lab/Type/Pi.lagda.md index 72dd0a8bf..76395483b 100644 --- a/src/1Lab/Type/Pi.lagda.md +++ b/src/1Lab/Type/Pi.lagda.md @@ -176,3 +176,14 @@ hetero-homotopy≃homotopy {A = A} {B} {f} {g} = Iso→Equiv isom where j (h (SinglP-is-contr A x₀ .paths (x₁ , p) j .snd)) ``` + + diff --git a/src/1Lab/Type/Sigma.lagda.md b/src/1Lab/Type/Sigma.lagda.md index 8bb2d0df4..03ef364c0 100644 --- a/src/1Lab/Type/Sigma.lagda.md +++ b/src/1Lab/Type/Sigma.lagda.md @@ -279,5 +279,12 @@ infixr 4 _,ₚ_ Σ-swap₂ .snd .is-eqv y = contr (f .fst) (f .snd) where f = strict-fibres _ y -- agda can actually infer the inverse here, which is neat + +×-swap + : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} + → (A × B) ≃ (B × A) +×-swap .fst (x , y) = y , x +×-swap .snd .is-eqv y = contr (f .fst) (f .snd) where + f = strict-fibres _ y ``` --> diff --git a/src/Cat/Allegory/Instances/Mat.lagda.md b/src/Cat/Allegory/Instances/Mat.lagda.md new file mode 100644 index 000000000..41afaf64f --- /dev/null +++ b/src/Cat/Allegory/Instances/Mat.lagda.md @@ -0,0 +1,115 @@ + + +```agda +module Cat.Allegory.Instances.Mat where +``` + +# Frame-valued matrices + +Let $L$ be a [frame]: it could be the frame of opens of a locale, for +example. It turns out that $L$ has enough structure that we can define +an [allegory], where the objects are sets, and the morphisms $A \rel B$ +are given by $A \times B$-matrices valued in $L$. + +[frame]: Order.Frame.html +[allegory]: Cat.Allegory.Base.html + + + +The identity matrix has an entry $\top$ at position $(i, j)$ iff $i = +j$, which we can express independently of whether $i = j$ is decidable +by saying that the identity matrix has $(i,j)$th entry $\bigvee_{i = j} +\top$. The composition of $M : B \rel C$ and $N : A \rel B$ has $(a,c)$th +entry given by + +$$ +\bigvee_{b : B} N(a,b) \wedge M(b,c) \text{,} +$$ + +which is easily seen to be an analogue of the $\sum_{b = 0}^{B} +N(a,b)M(b,c)$ which implements composition when matrices take values in +a ring. The infinite distributive law is applied frequently to establish +that this is, indeed, a category: + +```agda + Mat : Precategory (lsuc o) o + Mat .Ob = Set o + Mat .Hom A B = ∣ A ∣ → ∣ B ∣ → ⌞ L ⌟ + Mat .Hom-set x y = hlevel! + + Mat .id x y = ⋃ λ (_ : x ≡ y) → top + Mat ._∘_ {y = y} M N i j = ⋃ λ k → N i k ∩ M k j + + Mat .idr M = funext² λ i j → + ⋃ (λ k → ⋃ (λ _ → top) ∩ M k j) ≡⟨ ⋃-apᶠ (λ k → ∩-commutative ∙ ⋃-distrib _ _) ⟩ + ⋃ (λ k → ⋃ (λ _ → M k j ∩ top)) ≡⟨ ⋃-apᶠ (λ k → ap ⋃ (funext λ i → ∩-idr)) ⟩ + ⋃ (λ k → ⋃ (λ _ → M k j)) ≡⟨ ⋃-twice _ ⟩ + ⋃ (λ (k , _) → M k j) ≡⟨ ⋃-singleton (contr _ Singleton-is-contr) ⟩ + M i j ∎ + Mat .idl M = funext² λ i j → + ⋃ (λ k → M i k ∩ ⋃ (λ _ → top)) ≡⟨ ⋃-apᶠ (λ k → ⋃-distrib _ _) ⟩ + ⋃ (λ k → ⋃ (λ _ → M i k ∩ top)) ≡⟨ ⋃-apᶠ (λ k → ⋃-apᶠ λ j → ∩-idr) ⟩ + ⋃ (λ x → ⋃ (λ _ → M i x)) ≡⟨ ⋃-twice _ ⟩ + ⋃ (λ (k , _) → M i k) ≡⟨ ⋃-singleton (contr _ (λ p i → p .snd (~ i) , λ j → p .snd (~ i ∨ j))) ⟩ + M i j ∎ + + Mat .assoc M N O = funext² λ i j → + ⋃ (λ k → ⋃ (λ l → O i l ∩ N l k) ∩ M k j) ≡⟨ ⋃-apᶠ (λ k → ⋃-distribʳ) ⟩ + ⋃ (λ k → ⋃ (λ l → (O i l ∩ N l k) ∩ M k j)) ≡⟨ ⋃-twice _ ⟩ + ⋃ (λ (k , l) → (O i l ∩ N l k) ∩ M k j) ≡⟨ ⋃-apᶠ (λ _ → sym ∩-assoc) ⟩ + ⋃ (λ (k , l) → O i l ∩ (N l k ∩ M k j)) ≡⟨ ⋃-apⁱ ×-swap ⟩ + ⋃ (λ (l , k) → O i l ∩ (N l k ∩ M k j)) ≡˘⟨ ⋃-twice _ ⟩ + ⋃ (λ l → ⋃ (λ k → O i l ∩ (N l k ∩ M k j))) ≡⟨ ap ⋃ (funext λ k → sym (⋃-distrib _ _)) ⟩ + ⋃ (λ l → O i l ∩ ⋃ (λ k → N l k ∩ M k j)) ∎ +``` + +Most of the structure of an allegory now follows directly from the fact +that frames are also [semilattices]: the ordering, duals, and +intersections are all computed pointwise. The only thing which requires +a bit more algebra is the verification of the modular law: + +[semilattices]: Order.Semilattice.html + +```agda + Matrices : Allegory (lsuc o) o o + Matrices .A.cat = Mat + Matrices .A._≤_ M N = ∀ i j → M i j ≤ N i j + + Matrices .A.≤-thin = hlevel! + Matrices .A.≤-refl i j = ≤-refl + Matrices .A.≤-trans p q i j = ≤-trans (p i j) (q i j) + Matrices .A.≤-antisym p q = funext² λ i j → ≤-antisym (p i j) (q i j) + Matrices .A._◆_ p q i j = ⋃≤⋃ (λ k → ∩≤∩ (q i k) (p k j)) + + Matrices .A._† M i j = M j i + Matrices .A.dual-≤ x i j = x j i + Matrices .A.dual M = refl + Matrices .A.dual-∘ = funext² λ i j → ⋃-apᶠ λ k → ∩-commutative + + Matrices .A._∩_ M N i j = M i j ∩ N i j + Matrices .A.∩-le-l i j = ∩≤l + Matrices .A.∩-le-r i j = ∩≤r + Matrices .A.∩-univ p q i j = ∩-univ _ (p i j) (q i j) + + Matrices .A.modular f g h i j = + ⋃ (λ k → f i k ∩ g k j) ∩ h i j =⟨ ⋃-distribʳ ∙ ⋃-apᶠ (λ _ → sym ∩-assoc) ⟩ + ⋃ (λ k → f i k ∩ (g k j ∩ h i j)) =⟨ ⋃-apᶠ (λ k → ap₂ _∩_ refl ∩-commutative) ⟩ + ⋃ (λ k → f i k ∩ (h i j ∩ g k j)) ≤⟨ ⋃≤⋃ (λ i → ∩-univ _ (∩-univ _ ∩≤l (≤-trans ∩≤r (⋃-colimiting _ _))) (≤-trans ∩≤r ∩≤r)) ⟩ + ⋃ (λ k → (f i k ∩ ⋃ (λ l → h i l ∩ g k l)) ∩ g k j) ≤∎ +``` diff --git a/src/Order/Frame/Reasoning.lagda.md b/src/Order/Frame/Reasoning.lagda.md index 0c852c5bc..1bb1f6cc0 100644 --- a/src/Order/Frame/Reasoning.lagda.md +++ b/src/Order/Frame/Reasoning.lagda.md @@ -3,6 +3,7 @@ open import Cat.Prelude open import Order.Diagram.Lub +open import Order.Diagram.Glb open import Order.Semilattice open import Order.Frame open import Order.Base @@ -74,4 +75,52 @@ But this result relies on the cocontinuity of meets. ⋃ (λ i → ⋃ F ∩ G i) ≡⟨ ap ⋃ (funext λ i → ∩-commutative ∙ ⋃-distrib (G i) F) ⟩ ⋃ (λ i → ⋃ λ j → G i ∩ F j) ≡⟨ ⋃-product F G ⟩ ⋃ (λ i → F (i .fst) ∩ G (i .snd)) ∎ + +⋃-twice + : ∀ {I : Type ℓ} {J : I → Type ℓ} (F : (i : I) → J i → ⌞ B ⌟) + → ⋃ (λ i → ⋃ λ j → F i j) + ≡ ⋃ {I = Σ I J} (λ p → F (p .fst) (p .snd)) +⋃-twice F = ≤-antisym + (⋃-universal _ (λ i → ⋃-universal _ (λ j → ⋃-colimiting _ _))) + (⋃-universal _ λ (i , j) → ≤-trans (⋃-colimiting j _) (⋃-colimiting i _)) + +⋃-ap + : ∀ {I I′ : Type ℓ} {f : I → ⌞ B ⌟} {g : I′ → ⌞ B ⌟} + → (e : I ≃ I′) + → (∀ i → f i ≡ g (e .fst i)) + → ⋃ f ≡ ⋃ g +⋃-ap e p = ap₂ (λ I f → ⋃ {I = I} f) (ua e) (ua→ p) + +-- raised i for "index", raised f for "family" +⋃-apⁱ : ∀ {I I′ : Type ℓ} {f : I′ → ⌞ B ⌟} (e : I ≃ I′) → ⋃ (λ i → f (e .fst i)) ≡ ⋃ f +⋃-apᶠ : ∀ {I : Type ℓ} {f g : I → ⌞ B ⌟} → (∀ i → f i ≡ g i) → ⋃ f ≡ ⋃ g + +⋃-apⁱ e = ⋃-ap e (λ i → refl) +⋃-apᶠ p = ⋃-ap (_ , id-equiv) p + +⋃-singleton + : ∀ {I : Type ℓ} {f : I → ⌞ B ⌟} + → (p : is-contr I) + → ⋃ f ≡ f (p .centre) +⋃-singleton {f = f} p = ≤-antisym + (⋃-universal _ (λ i → sym ∩-idempotent ∙ ap₂ _∩_ refl (ap f (sym (p .paths _))))) + (⋃-colimiting _ _) + +⋃-distribʳ + : ∀ {I : Type ℓ} {f : I → ⌞ B ⌟} {x} + → ⋃ f ∩ x ≡ ⋃ (λ i → f i ∩ x) +⋃-distribʳ = ∩-commutative ∙ ⋃-distrib _ _ ∙ ap ⋃ (funext λ _ → ∩-commutative) + +⋃≤⋃ + : ∀ {I : Type ℓ} {f g : I → ⌞ B ⌟} + → (∀ i → f i ≤ g i) + → ⋃ f ≤ ⋃ g +⋃≤⋃ p = ⋃-universal _ (λ i → ≤-trans (p i) (⋃-colimiting _ _)) + +∩≤∩ + : ∀ {x y x' y'} + → x ≤ x' + → y ≤ y' + → (x ∩ y) ≤ (x' ∩ y') +∩≤∩ p q = ∩-univ _ (≤-trans ∩≤l p) (≤-trans ∩≤r q) ``` From 08b3d7e9f44312f0369bb36c338683f196d884ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia?= Date: Thu, 10 Aug 2023 08:10:56 -0300 Subject: [PATCH 5/5] defn: Ordered families of equivalences (#245) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit OFEs are a presentation of certain metric spaces which see some use in the literature on guarded recursion/step indexing, e.g. the “standard” model of the Iris logic lives in the category of COFEs. --- .github/workflows/build.yml | 4 +- src/1Lab/Reflection.lagda.md | 4 +- src/1Lab/Reflection/HLevel.agda | 7 +- src/1Lab/Reflection/Marker.agda | 2 +- src/1Lab/Reflection/Record.agda | 1 - src/1Lab/Reflection/Variables.agda | 2 +- src/Cat/Instances/OFE.lagda.md | 403 +++++++++++++++++++++++ src/Cat/Instances/OFE/Closed.lagda.md | 52 +++ src/Cat/Instances/OFE/Complete.lagda.md | 264 +++++++++++++++ src/Cat/Instances/OFE/Coproduct.lagda.md | 198 +++++++++++ src/Cat/Instances/OFE/Discrete.lagda.md | 43 +++ src/Cat/Instances/OFE/Later.lagda.md | 130 ++++++++ src/Cat/Instances/OFE/Product.lagda.md | 188 +++++++++++ src/Data/List.lagda.md | 52 ++- src/Data/List/Base.lagda.md | 39 +++ src/Meta/Traverse.lagda.md | 1 + src/Prim/Data/String.lagda.md | 2 +- src/preamble.tex | 2 + 18 files changed, 1348 insertions(+), 46 deletions(-) create mode 100644 src/Cat/Instances/OFE.lagda.md create mode 100644 src/Cat/Instances/OFE/Closed.lagda.md create mode 100644 src/Cat/Instances/OFE/Complete.lagda.md create mode 100644 src/Cat/Instances/OFE/Coproduct.lagda.md create mode 100644 src/Cat/Instances/OFE/Discrete.lagda.md create mode 100644 src/Cat/Instances/OFE/Later.lagda.md create mode 100644 src/Cat/Instances/OFE/Product.lagda.md diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 033a6cacc..2ca98805c 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -32,8 +32,8 @@ jobs: uses: actions/cache@v3 with: path: _build - key: shake-3-${{ env.shake_version }}-${{ github.run_id }} - restore-keys: shake-3-${{ env.shake_version }}- + key: shake-4-${{ env.shake_version }}-${{ github.run_id }} + restore-keys: shake-4-${{ env.shake_version }}- - name: Build 🛠️ run: | diff --git a/src/1Lab/Reflection.lagda.md b/src/1Lab/Reflection.lagda.md index 2b6107fab..f1fb984e5 100644 --- a/src/1Lab/Reflection.lagda.md +++ b/src/1Lab/Reflection.lagda.md @@ -8,7 +8,7 @@ open import 1Lab.Type hiding (absurd) open import Data.Product.NAry open import Data.Vec.Base open import Data.Bool -open import Data.List +open import Data.List.Base ``` --> @@ -27,7 +27,7 @@ open import Meta.Alt public open Data.Vec.Base using (Vec ; [] ; _∷_ ; lookup ; tabulate) public open Data.Product.NAry using ([_]) public -open Data.List public +open Data.List.Base public open Data.Bool public ``` diff --git a/src/1Lab/Reflection/HLevel.agda b/src/1Lab/Reflection/HLevel.agda index a2e91bf0a..6c09cb642 100644 --- a/src/1Lab/Reflection/HLevel.agda +++ b/src/1Lab/Reflection/HLevel.agda @@ -10,7 +10,7 @@ open import 1Lab.Path open import 1Lab.Type open import Data.Bool -open import Data.List +open import Data.List.Base open import Meta.Foldable @@ -678,11 +678,6 @@ instance decomp-univalence : ∀ {ℓ} {A B : Type ℓ} → hlevel-decomposition (A ≡ B) decomp-univalence = decomp (quote ≡-is-hlevel) (`level ∷ `search ∷ `search ∷ [] ) - -- List isn't really a type on the same footing as all the others, but - -- we're here, so we might as well, right? - decomp-list : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (List A) - decomp-list = decomp (quote ListPath.List-is-hlevel) (`level-minus 2 ∷ `search ∷ []) - -- This one really ought to work with instance selection only, but -- Agda has trouble with the (1 + k + n) level in H-Level-n-Type. The -- decomposition here is a bit more flexible. diff --git a/src/1Lab/Reflection/Marker.agda b/src/1Lab/Reflection/Marker.agda index da773b286..4133cc79a 100644 --- a/src/1Lab/Reflection/Marker.agda +++ b/src/1Lab/Reflection/Marker.agda @@ -3,7 +3,7 @@ open import 1Lab.Path open import 1Lab.Type open import Data.Maybe.Base -open import Data.List +open import Data.List.Base open import Prim.Data.Nat diff --git a/src/1Lab/Reflection/Record.agda b/src/1Lab/Reflection/Record.agda index ffab8cdb6..3696d6446 100644 --- a/src/1Lab/Reflection/Record.agda +++ b/src/1Lab/Reflection/Record.agda @@ -4,7 +4,6 @@ open import 1Lab.Equiv open import 1Lab.Path open import 1Lab.Type -open import Data.List import Prim.Data.Sigma as S import Prim.Data.Nat as N diff --git a/src/1Lab/Reflection/Variables.agda b/src/1Lab/Reflection/Variables.agda index fe58f68a3..8626dfe0c 100644 --- a/src/1Lab/Reflection/Variables.agda +++ b/src/1Lab/Reflection/Variables.agda @@ -3,7 +3,7 @@ open import 1Lab.Type open import Data.Fin.Base open import Data.Nat.Base -open import Data.List hiding (reverse) +open import Data.List.Base hiding (reverse) module 1Lab.Reflection.Variables where diff --git a/src/Cat/Instances/OFE.lagda.md b/src/Cat/Instances/OFE.lagda.md new file mode 100644 index 000000000..3cabc84e1 --- /dev/null +++ b/src/Cat/Instances/OFE.lagda.md @@ -0,0 +1,403 @@ + + +```agda +module Cat.Instances.OFE where +``` + +# Ordered families of equivalence relations + +An **ordered family of equivalence relations** (OFE, for short) is a set +$X$ equipped with a family of equivalence relations, indexed by natural +numbers $n$ and written $x \within{n} y$, that _approximate_ the +equality on $X$. The family of equivalence relations can be thought of +as equipping $X$ with a notion of _fractional distance_: $x \within{n} +y$ means that $x$ and $y$ are "within distance $2^{-n}$ of each other". +The axioms of an OFE are essentially that + +- The maximal distance between two points is $1$, i.e., $x +\within{n} y$ is the total relation; + +- Points that are within some distance $d$ of eachother are also within +$d'$, for any $d' \le d$; + +- Arbitrarily close points are the same. + +::: warning +We remark that the term OFE generally stands for ordered family of +_equivalences_, rather than _equivalence relations_; However, this +terminology is mathematically incorrect: there is no meaningful sense in +which an OFE is a family $I \to (A \equiv B)$. + +To preserve the connection with the literature, we shall maintain the +acronym "OFE"; Keep in mind that we do it with disapproval. +::: + +Another perspective on OFEs, and indeed a large part for the +justification of their study, is in the semantics of programming +languages: in that case, the relation $x \within{n} y$ should be +interpreted as _equivalent for $n$ steps of computation_: a program +running for at most $n$ steps can not tell $\within{n}$-related elements +apart. Our axioms are then that a program running for no steps can not +distinguish anything, so we have $x \within{0} y$ for any $x, y$, and +that our approximations become finer with an increasing number of steps: +with arbitrarily many steps, the only indistinguishable elements must +actually be equal. + +```agda +record is-ofe {ℓ ℓ'} {X : Type ℓ} (within : Nat → X → X → Type ℓ') : Type (ℓ ⊔ ℓ') where + no-eta-equality + + field + has-is-prop : ∀ n x y → is-prop (within n x y) + + ≈-refl : ∀ n {x} → within n x x + ≈-sym : ∀ n {x y} → within n x y → within n y x + ≈-trans : ∀ n {x y z} → within n y z → within n x y → within n x z + + bounded : ∀ x y → within 0 x y + step : ∀ n x y → within (suc n) x y → within n x y + limit : ∀ x y → (∀ n → within n x y) → x ≡ y + + ofe→ids : is-identity-system (λ x y → ∀ n → within n x y) (λ x n → ≈-refl n) + ofe→ids = set-identity-system + (λ x y → Π-is-hlevel 1 λ n → has-is-prop n x y) + (limit _ _) +``` + +From a HoTT perspective, this definition works extremely smoothly: note +that since we require the approximate equalities $x \within{n} y$ to be +propositions, every subsequent field of the record is _also_ a +proposition, so equality of `is-ofe`{.Agda} is trivial, like we would +expect. Moreover, since "equality at the limit", the relation + +$$ +R(x, y) = \forall n, x \within{n} y +$$ + +is a reflexive relation (since each $x \within{n} y$ is reflexive) that +implies equality, the type underlying a OFE is automatically a set; its +identity type is _equivalent_ to equality at the limit. + + + +The correct notion of morphism between OFEs is that of **non-expansive +maps**, once again appealing to the notion of distance for intuition. A +function $f : X \to Y$ is non-expansive if points under $f$ do not get +farther. Apart from the intuitive justification, we note that the +[structure identity principle][sip] essentially forces non-expansivity +to be the definition of morphism of OFEs: the type of OFEs is equivalent +to a $\Sigma$-type that starts + +$$ +\Sigma (X : \ty) \Sigma (R : X \to \bN \to X \to \ty) \Sigma ...\text{,} +$$ + +where all the components in $...$ are propositional. Its identity type +can be _computed_ to consist of equivalences between the underlying +types that preserve the relations $R$, and since the relations are +propositions, bi-implication suffices: an identification between OFEs is +a non-expansive equivalence of types with non-expansive inverse. + +[sip]: 1Lab.Univalence.SIP.html + +```agda + record is-non-expansive : Type (ℓ ⊔ ℓ' ⊔ ℓ₁') where + no-eta-equality + field + pres-≈ : ∀ {x y n} → O.within n x y → P.within n (f x) (f y) +``` + + + +## Examples + +A canonical class of examples for OFEs is given by strings, or, more +generally, lists: if $X$ is a set, then, for $x, y : \rm{List}(X)$, we +can define the relations $x \within{n} y$ to mean _the length-$n$ +prefixes of $x$ and $y$ are equal_. Let's quickly go over the axioms +informally before looking at the formalisation: + +- Each relation $\within{n}$ is an equivalence relation, since it is + defined to be equality; + +- At the limit, suppose we have lists $x, y$: we do not yet know that + their lengths agree, but we _do_ know that taking a "prefix" longer than + the list gives back the entire list. + + So, writing $l_x$ and $l_y$ for the lengths, we can use our assumption + that $x$ and $y$ agree at length $l = \max(l_x, l_y)$: the length $l$ + prefixes of both $x$ and $y$ are both the entire lists $x$ and $y$, so + we have + + $$ + x = \rm{take}(l,x) = \rm{take}(l,y) = y\text{,} + $$ + + where the middle step is $x \within{l} y$. + +- Finally, since a length $l+1$ prefix is necessarily adding an element + onto a length $l$ prefix, we satisfy the monotonicity requirement. In + the formalisation, we use a direct inductive argument for this. We'll + show that, for all $xs, ys, n$, if $\rm{take}(1 + n, xs) = \rm{take}(1 + + n, ys)$, then $\rm{take}(n, xs) = \rm{take}(n, ys)$. + + On the _one_ interesting case, we assume that $x :: \rm{take}(1 + n, + xs) = y :: \rm{take}(1 + n, ys)$, which we can split into $x = y$ and + $\rm{take}(1 + n, xs) = \rm{take}(1 + n, ys)$. The induction + hypothesis lets us turn this latter equality into $\rm{take}(n,xs) = + \rm{take}(n,ys)$, which pairs up with $x = y$ to conclude exactly what + we want. + +```agda +Lists : ∀ {ℓ} {X : Type ℓ} → is-set X → OFE-on ℓ (List X) +Lists X-set .within n xs ys = take n xs ≡ take n ys +Lists X-set .has-is-ofe .has-is-prop n xs ys = ListPath.is-set→List-is-set X-set _ _ +Lists X-set .has-is-ofe .≈-refl n = refl +Lists X-set .has-is-ofe .≈-sym n p = sym p +Lists X-set .has-is-ofe .≈-trans n p q = q ∙ p +Lists X-set .has-is-ofe .bounded x y = refl + +Lists X-set .has-is-ofe .limit x y wit = sym rem₁ ·· agree ·· rem₂ where + enough = max (length x) (length y) + agree : take enough x ≡ take enough y + agree = wit enough + + rem₁ : take enough x ≡ x + rem₁ = take-length-more x enough (max-≤l _ _) + rem₂ : take enough y ≡ y + rem₂ = take-length-more y enough (max-≤r _ _) + +Lists X-set .has-is-ofe .step n x y p = steps x y n p where + steps : ∀ {ℓ} {A : Type ℓ} (x y : List A) n + → take (suc n) x ≡ take (suc n) y → take n x ≡ take n y + steps (x ∷ xs) (y ∷ ys) (suc n) p = + ap₂ _∷_ (ap (head x) p) (steps xs ys n (ap tail p)) +``` + +Since the rest of this proof is a simple case bash[^5 cases are +reflexivity, 2 assume an impossibility], we've hidden it on the website. +You can choose to display comments on the side bar, or check out this +module on GitHub. + + + +This example generalises incredibly straightforwardly to possibly +infinite sequences in a set: that is, functions $\bN \to X$. Our +definition of $x \within{n} y$ is now that, for all $k \lt n$, $x(k) = +y(k)$. Once again we are using equality to approximate equality, so this +is levelwise an equivalence relation; surprisingly, the other three +properties are _simpler_ to establish for sequences than for lists! + +```agda +Sequences : ∀ {ℓ} {X : Type ℓ} → is-set X → OFE-on ℓ (Nat → X) +Sequences _ .within n xs ys = ∀ k (le : k < n) → xs k ≡ ys k +Sequences {X = X} X-set .has-is-ofe .has-is-prop n xs ys = hlevel 1 where instance + _ : H-Level X 2 + _ = basic-instance 2 X-set +Sequences _ .has-is-ofe .≈-refl n k le = refl +Sequences _ .has-is-ofe .≈-sym n p k le = sym (p k le) +Sequences _ .has-is-ofe .≈-trans n p q k le = q k le ∙ p k le + +Sequences _ .has-is-ofe .bounded xs ys k () +Sequences _ .has-is-ofe .step n xs ys p k le = p k (≤-sucr le) +Sequences _ .has-is-ofe .limit xs ys wit = funext λ k → wit (suc k) k ≤-refl +``` + +# Contractive maps + + + +```agda + record is-contractive : Type (ℓ ⊔ ℓ' ⊔ ℓ₁') where + no-eta-equality + field + contract : ∀ {x y n} → O.within n x y → P.within (suc n) (f x) (f y) +``` + + + + diff --git a/src/Cat/Instances/OFE/Closed.lagda.md b/src/Cat/Instances/OFE/Closed.lagda.md new file mode 100644 index 000000000..c574e5488 --- /dev/null +++ b/src/Cat/Instances/OFE/Closed.lagda.md @@ -0,0 +1,52 @@ + + +```agda +module Cat.Instances.OFE.Closed where +``` + +# Function OFEs + +If $A$ and $B$ are [OFEs], then so is the space of non-expansive +functions $A \overset{ne}{\to} B$: this makes the category OFE into a +Cartesian closed category. + +[OFEs]: Cat.Instances.OFE.html + + + +```agda +``` + +```agda + Function-OFE : OFE-on (ℓa ⊔ ℓb') (O →ⁿᵉ P) + Function-OFE .within n f g = ∀ x → f .map x ≈[ n ] g .map x + Function-OFE .has-is-ofe .has-is-prop n x y = hlevel 1 + where open OFE-H-Level P + Function-OFE .has-is-ofe .≈-refl n x = P.≈-refl n + Function-OFE .has-is-ofe .≈-sym n p x = P.≈-sym n (p x) + Function-OFE .has-is-ofe .≈-trans n p q x = P.≈-trans n (p x) (q x) + Function-OFE .has-is-ofe .bounded f g x = P.bounded (f .map x) (g .map x) + Function-OFE .has-is-ofe .step n f g α x = P.step n (f .map x) (g .map x) (α x) + Function-OFE .has-is-ofe .limit f g α = Nonexp-ext λ x → + P.limit (f .map x) (g .map x) (λ n → α n x) +``` diff --git a/src/Cat/Instances/OFE/Complete.lagda.md b/src/Cat/Instances/OFE/Complete.lagda.md new file mode 100644 index 000000000..fef981e4c --- /dev/null +++ b/src/Cat/Instances/OFE/Complete.lagda.md @@ -0,0 +1,264 @@ + + +```agda +module Cat.Instances.OFE.Complete where +``` + + + +# Limits and complete OFEs + +Since [OFEs] are metric-space-_like_[^1] structures, there is a natural +notion of sequences getting closer to a value: we say a sequence $f : \bN +\to A$ is a _chain_ if, given $n \le m$, we have $f(m) \within{n} f(n)$. +Looking at the case where $m = 1 + n$, this says that we have a sequence + +$$ +f(0) \within{0} f(1) \within{1} f(2) \within{2} f(3) \within{3} \dots +$$ + +where the metric interpretation of OFEs lets us read this as the +_distance_ between successive points approaching +$\lim_{n\to\infty}2^{-n} = 0$. + +```agda + is-chain : (x : Nat → A) → Type _ + is-chain f = ∀ m n → n ≤ m → f m ≈[ n ] f n +``` + +[^1]: An OFE is a _1-bounded, bisected ultrametric space_. + +[OFEs]: Cat.Instances.OFE.html + +However, in a general OFE, there is not necessarily anything "at +$\infty$": the values of the sequence get closer to each other, but +there's no specific _point_ they're getting closer to. An example of +chain without limit is as follows: let $a : A$ be an element of a set, +and consider the sequence + +$$ +f(n) = \underbrace{a,\dots,a}_\text{$n$ times} +$$ + +in the OFE of finite sequences. Clearly this satisfies the chain +condition: w.l.o.g. we can assume $m = n + k$ for some $k$, and $f(n + +k)$ certainly shares the first $n$ elements with $f(n)$. However, there +is no single list of $A$s $l$ which shares its first $n$ elements +with $f(n)$: $l$ must have a definite length, independent of $n$, which +bounds the size of its prefixes. Choosing any $n > \rm{length}(l)$ +results in a value of $f(n)$ has more elements than the length-$n$ +prefix of $l$. + +The previous paragraph contains an unfolding of the definition of a +sequence having a limit, or, more specifically, it contains a definition +of what it means for a point to be the limit of a sequence: $a$ is the +limit of $f$ if, for all $n$, $a \within{n} f(a)$. + +```agda + is-limit : (x : Nat → A) → A → Type _ + is-limit f a = ∀ n → a ≈[ n ] f n +``` + +It follows at once that _the_ limit of a sequence is uniquely +determined: if $a$ and $b$ both claim to be limits of $f$, we have, for +arbitrary $n$, $a \within{n} f(a) \within{n} b$, meaning $a = b$. + +```agda + limit-is-unique + : ∀ (f : Nat → A) {x y} + → is-limit f x → is-limit f y → x ≡ y + limit-is-unique f l1 l2 = P.limit _ _ λ n → + P.≈-trans n (P.≈-sym n (l2 n)) (l1 n) +``` + + + +However, some OFEs _do_ have limits for all chains: the OFE of infinite +sequences is one, for example. We refer to such an OFE as a **complete +ordered family of equivalences**, or COFE^[Feel free to pronounce it +"coffee".] for short. + +```agda + is-cofe : Type _ + is-cofe = ∀ (f : Nat → A) → is-chain f → Limit f +``` + + + +We can actually compute the limit of a sequence of sequences pretty +easily: we have a function $s : \bN \times \bN \to A$, our sequence, and +the chain condition says that, given $j \le i$ and $k \lt j$, we get +$s(i,k) = s(j,k)$. Our limit is the sequence $l(i) = s(1 + i, i)$: we +must show that $l \within{n} s(n)$, which means that, given +$k \lt n$, we must have $s(1 + k, k) = s(n,k)$. This follows by the +chain condition: $k \lt 1 + k$, and $(1 + k) \le n$, so we conclude $s(1 ++ k, k) = s(n, k)$. + +```agda + Sequences-is-cofe : is-cofe (Sequences X-set) + Sequences-is-cofe seq chain = (λ j → seq (suc j) j) , λ n k k + +In passing, let us note that non-expansive maps preserve both chains +_and_ their limits. + +```agda + non-expansive→chain + : (f : A → B) (s : Nat → A) + → is-non-expansive f P Q → is-chain P s → is-chain Q (λ n → f (s n)) + non-expansive→chain f s ne p m n n≤m = ne .pres-≈ (p m n n≤m) + + non-expansive→limit + : (f : A → B) (s : Nat → A) (x : A) + → is-non-expansive f P Q → is-limit P s x → is-limit Q (λ n → f (s n)) (f x) + non-expansive→limit f s x ne lim n = ne .pres-≈ (lim n) +``` + +## Banach's fixed point theorem + + + +**Banach's fixed point theorem**, in our setting, says that any +contractive $f : P \to P$ on an _inhabited_ COFE has a unique fixed +point. We'll start with uniqueness: suppose that some $a, b$ satisfy +$f(a) = a$ and $f(b) = b$. It will suffice to show that $f(a) = f(b)$, +and, working in an OFE, this further reduces to $f(a) \within{n} f(b)$ +for an arbitrary $n$. + +By induction, with a trivial base case, we can assume $f(a) \within{n} +f(b)$ to show $f(a) \within{1+n} f(b)$: but $f$ is contractive, so it +acts on the induction hypothesis to produce $f(f(a)) \within{1+n} +f(f(b))$. But we assumed both $a$ and $b$ are fixed points, so this is +exactly what we want. + +```agda + banach : ∥ A ∥ → (f : P →ᶜᵒⁿ P) → Σ A λ x → f .map x ≡ x + banach inhab f = ∥-∥-proj {ap = fp-unique} fp' where + fp-unique : is-prop (Σ A λ x → f .map x ≡ x) + fp-unique (a , p) (b , q) = + Σ-prop-path (λ x → from-ofe-on P .fst .is-tr _ _) + (sym p ·· P.limit _ _ climb ·· q) + where + + climb : ∀ n → f .map a ≈[ n ] f .map b + climb zero = P.bounded _ _ + climb (suc n) = transport (λ i → f .map (p i) ≈[ suc n ] f .map (q i)) (f .contract n (climb n)) +``` + +The point of showing uniqueness is that the fixed point is independent +of _how_ $P$ is inhabited: in other words, for a contractive mapping on +a COFE to have a fixed point, we needn't $x : P$ --- $x : \| P \|$ will +suffice. That aside justifes this sentence: Fix a starting point $x_0 : +P$, and consider the sequence + +$$ +s = x_0, f(x_0), f(f(x_0)), f(f(f(x_0))), \dots +$$ + +which is a chain again by an inductive argument involving contractivity +(formalised below for the curious). + +```agda + approx : A → Nat → A + approx a zero = a + approx a (suc n) = f .map (approx a n) + + chain : ∀ a → is-chain P (approx a) + chain a m zero x = P.bounded (approx a m) a + chain a (suc m) (suc n) (s≤s x) = f .contract n (chain a m n x) +``` + +I claim that the limit of $s$ is a fixed point of $f$: we can calculate + +$$ +f(\lim_n s(n)) = \lim_n f(s(n)) = \lim_n s(n+1) = \lim_n s(n) +$$ + +where we have, in turn, that non-expansive mappings preserve limits, the +very definition of $s$, and the fact that limits are insensitive to +dropping an element at the start. + +```agda + fp' : ∥ _ ∥ + fp' = do + pt ← inhab + let + (it , is) = lim (approx pt) (chain pt) + + ne : is-non-expansive (f .map) P P + ne = record { pres-≈ = λ p → P.step _ _ _ (f .contract _ p) } + + prf : f .map it ≡ it + prf = + f .map it ≡⟨ limit-is-unique P _ (non-expansive→limit _ _ _ _ _ ne is) (lim _ _ .snd) ⟩ + lim (λ n → f .map (approx pt n)) _ .fst ≡⟨ ap fst (ap (lim _) (λ i → non-expansive→chain _ _ _ _ ne (chain pt))) ⟩ + lim (λ n → approx pt (suc n)) _ .fst ≡⟨ limit-is-unique P _ (lim _ _ .snd) (limit-to-tail P (approx pt) _ (chain pt) is) ⟩ + it ∎ + + pure (it , prf) +``` diff --git a/src/Cat/Instances/OFE/Coproduct.lagda.md b/src/Cat/Instances/OFE/Coproduct.lagda.md new file mode 100644 index 000000000..5b4a49fd3 --- /dev/null +++ b/src/Cat/Instances/OFE/Coproduct.lagda.md @@ -0,0 +1,198 @@ + + +```agda +module Cat.Instances.OFE.Coproduct where +``` + +# Coroducts of OFEs + +The [category of OFEs][OFE] admits binary [coproducts]. Unlike the +[construction of products][ofe-prod], in which we could define the +approximations $(a, b) \within{n} (a', b')$ by lifting those of the +factor OFEs, the definition of coproducts requires a fair bit more +busywork. + +[OFE]: Cat.Instances.OFE.html +[coproducts]: Cat.Diagram.Coproduct.html +[ofe-prod]: Cat.Instances.OFE.Product.html + + + + + +To get it right, let's use the computational interpretation of OFEs. +Having done no steps of computation, we have not yet managed to +distinguish the left summand from the right summand. Motivated by this, +and to satisfy the boundedness axiom, we simply define $x \within{0} y$ +to be the unit type everywhere. + +Having taken some positive number of steps, it is possible to +distinguish the summands, and we must do so, defining the relations by +cases. The relations $\rm{in}_d(x) \within{1+n} \rm{in}_d(y)$, where $d +\in {l,r}$ ranges over the coproduct injections, are defined to be $x +\within{1+n} y$. Note the index: we do not want to take a step back! In +case the summands are mismatched, e.g. $\rm{inr}(x) \within{1+n} +\rm{inl}(y)$, we give back the bottom type: we have taken enough steps +that it is impossible for them to be equal. + +```agda + ⊎-OFE : OFE-on (ℓa' ⊔ ℓb') (A ⊎ B) + ⊎-OFE .within zero p q = Lift (ℓa' ⊔ ℓb') ⊤ + ⊎-OFE .within (suc n) (inl x) (inl y) = Lift ℓb' (x ≈[ suc n ] y) + ⊎-OFE .within (suc n) (inr x) (inr y) = Lift ℓa' (x ≈[ suc n ] y) + ⊎-OFE .within (suc n) (inl x) (inr y) = Lift (ℓa' ⊔ ℓb') ⊥ + ⊎-OFE .within (suc n) (inr x) (inl y) = Lift (ℓa' ⊔ ℓb') ⊥ +``` + +The proofs of all the axioms will have to make the same case +distinctions to get at a concrete type for the approximations. Let's see +it for reflexivity: + +- We first distinguish on the number of steps. If we've not taken any + yet, then our relation is trivial, and we can (have to!) give back its + trivial point. + +- Having taken a number of steps, we distinguish on the summand. Having + exposed the underlying relation, we can lift its proof of reflexivity to + the sum. + +```agda + ⊎-OFE .has-is-ofe .≈-refl zero = lift tt + ⊎-OFE .has-is-ofe .≈-refl (suc n) {inl _} = lift (O.≈-refl (suc n)) + ⊎-OFE .has-is-ofe .≈-refl (suc n) {inr _} = lift (P.≈-refl (suc n)) +``` + +
+The other fields are essentially the same, so there's not a lot +to write about. + +```agda + ⊎-OFE .has-is-ofe .has-is-prop zero x y _ _ = refl + ⊎-OFE .has-is-ofe .has-is-prop (suc n) (inl _) (inl _) = hlevel! + ⊎-OFE .has-is-ofe .has-is-prop (suc n) (inr _) (inr _) = hlevel! + + ⊎-OFE .has-is-ofe .≈-sym zero p = lift tt + ⊎-OFE .has-is-ofe .≈-sym (suc n) {inl _} {inl _} p = lift (O.≈-sym _ (p .Lift.lower)) + ⊎-OFE .has-is-ofe .≈-sym (suc n) {inr _} {inr _} p = lift (P.≈-sym _ (p .Lift.lower)) + + ⊎-OFE .has-is-ofe .≈-trans zero p q = lift tt + ⊎-OFE .has-is-ofe .≈-trans (suc n) {inl _} {inl _} {inl _} p q = lift (O.≈-trans _ (p .Lift.lower) (q .Lift.lower)) + ⊎-OFE .has-is-ofe .≈-trans (suc n) {inr _} {inr _} {inr _} p q = lift (P.≈-trans _ (p .Lift.lower) (q .Lift.lower)) + + ⊎-OFE .has-is-ofe .bounded a b = lift tt + ⊎-OFE .has-is-ofe .step zero _ _ p = lift tt + ⊎-OFE .has-is-ofe .step (suc n) (inl x) (inl y) p = lift (O.step _ x y (p .Lift.lower)) + ⊎-OFE .has-is-ofe .step (suc n) (inr x) (inr y) p = lift (P.step _ x y (p .Lift.lower)) +``` + +This minor quibble might be of note to the reader curious enough to +expand this note: To prove that our approximations converge, we _also_ +need a case distinction. At the zeroth entry, we appeal to boundedness +of the summand OFEs to get a witness of $x \within{0} y$, since +$\rm{inr}(x) \within{0} \rm{inr}(y)$ is uninformative. + +```agda + ⊎-OFE .has-is-ofe .limit (inl x) (inl y) f = ap inl (O.limit x y f') where + f' : ∀ n → O.within n x y + f' zero = O.bounded x y + f' (suc n) = f (suc n) .Lift.lower + ⊎-OFE .has-is-ofe .limit (inr x) (inr y) f = ap inr (P.limit x y f') where + f' : ∀ n → P.within n x y + f' zero = P.bounded x y + f' (suc n) = f (suc n) .Lift.lower + ⊎-OFE .has-is-ofe .limit (inl x) (inr y) f = absurd (f 1 .Lift.lower) + ⊎-OFE .has-is-ofe .limit (inr x) (inl y) f = absurd (f 1 .Lift.lower) +``` + +
+ + + +We now prove that this construction, which despite my best efforts may +still feel unmotivated, _is_ the categorical product in OFEs. We start +by defining the coproduct of morphisms, the operation taking $f : A \to +Q$ and $g : B \to Q$ to $[f,g] : A \uplus B \to Q$. Once again, it's a +case bash, and we have to use boundedness of the codomain when showing +that points with distance 1 stay with distance 1. + +```agda +OFE-Coproduct : ∀ {ℓ ℓ'} A B → Coproduct (OFEs ℓ ℓ') A B +OFE-Coproduct A B = mk where + module A = OFE-on (A .snd) + module B = OFE-on (B .snd) + + it = from-ofe-on (⊎-OFE (A .snd) (B .snd)) + + disj : ∀ {Q} → OFEs.Hom A Q → OFEs.Hom B Q → OFEs.Hom it Q + disj f g .hom (inl x) = f # x + disj f g .hom (inr x) = g # x + disj {Q = Q} f g .preserves .pres-≈ {n = zero} _ = OFE-on.bounded (Q .snd) _ _ + disj f g .preserves .pres-≈ {inl x} {inl y} {suc n} (lift α) = + f .preserves .pres-≈ α + disj f g .preserves .pres-≈ {inr x} {inr y} {suc n} (lift α) = + g .preserves .pres-≈ α +``` + +We can then define the coprojections: since we must now produce an +approximation _in_ the sum, if our points have distance 1, we can +produce a trivial datum. + +```agda + in0 : OFEs.Hom A it + in0 .hom = inl + in0 .preserves .pres-≈ {n = zero} _ = lift tt + in0 .preserves .pres-≈ {n = suc n} α = lift α + + in1 : OFEs.Hom B it + in1 .hom = inr + in1 .preserves .pres-≈ {n = zero} _ = lift tt + in1 .preserves .pres-≈ {n = suc n} α = lift α +``` + +It suffices to show that all the relevant diagrams in the definition of +a coproduct actually commute, and that the coproduct of morphisms is +unique: but it suffices to reason at the level of sets. + +```agda + mk : Coproduct (OFEs _ _) A B + mk .coapex = it + mk .in₀ = in0 + mk .in₁ = in1 + mk .has-is-coproduct .is-coproduct.[_,_] {Q = Q} f g = disj f g + mk .has-is-coproduct .in₀∘factor = Homomorphism-path λ x → refl + mk .has-is-coproduct .in₁∘factor = Homomorphism-path λ x → refl + mk .has-is-coproduct .unique other p q = Homomorphism-path λ where + (inl x) → p #ₚ x + (inr x) → q #ₚ x +``` diff --git a/src/Cat/Instances/OFE/Discrete.lagda.md b/src/Cat/Instances/OFE/Discrete.lagda.md new file mode 100644 index 000000000..53f175a87 --- /dev/null +++ b/src/Cat/Instances/OFE/Discrete.lagda.md @@ -0,0 +1,43 @@ + + +```agda +module Cat.Instances.OFE.Discrete where +``` + +# Discrete OFEs + +Given a set $X$, we can make it into a **discrete [OFE]** by equipping +it with the relation that _takes one step_ to approximate equality: $x +\within{0} y$ is trivial, but $x \within{1 + n} y$ is defined to be $x = +y$, no matter what $n$ is. + +[OFE]: Cat.Instances.OFE.html + +```agda +Discrete-OFE : ∀ {ℓ} (A : Type ℓ) → is-set A → OFE-on ℓ A +Discrete-OFE A A-set .within zero x y = Lift _ ⊤ +Discrete-OFE A A-set .within (suc n) x y = x ≡ y +Discrete-OFE A A-set .has-is-ofe .has-is-prop zero _ _ _ _ _ = _ +Discrete-OFE A A-set .has-is-ofe .has-is-prop (suc n) = A-set + +Discrete-OFE A A-set .has-is-ofe .≈-refl zero = _ +Discrete-OFE A A-set .has-is-ofe .≈-refl (suc n) = refl + +Discrete-OFE A A-set .has-is-ofe .≈-sym zero = _ +Discrete-OFE A A-set .has-is-ofe .≈-sym (suc n) p = sym p + +Discrete-OFE A A-set .has-is-ofe .≈-trans zero = _ +Discrete-OFE A A-set .has-is-ofe .≈-trans (suc n) p q = q ∙ p + +Discrete-OFE A A-set .has-is-ofe .bounded = _ +Discrete-OFE A A-set .has-is-ofe .step zero = _ +Discrete-OFE A A-set .has-is-ofe .step (suc n) x y p = p +Discrete-OFE A A-set .has-is-ofe .limit x y α = α 1 +``` diff --git a/src/Cat/Instances/OFE/Later.lagda.md b/src/Cat/Instances/OFE/Later.lagda.md new file mode 100644 index 000000000..7d81fd437 --- /dev/null +++ b/src/Cat/Instances/OFE/Later.lagda.md @@ -0,0 +1,130 @@ + + +```agda +module Cat.Instances.OFE.Later where +``` + +# The "Later" OFE + +Given a [OFE] $A$, we define an OFE $\later A$, the **later** modality +of systems of guarded recursion. The idea is that $\later A$ is like +$A$, but we have to wait a bit to think about it: at level zero, $\later +A$ is an indiscrete blob, but at positive time steps, it looks just like +$A$. + +The $\later A$ construction extends to an endofunctor of OFE, equipped +with a natural transformation $\rm{next} : A \to \later A$, expressing +that if we have something now, we can very well stop thinking about it +for a step. This natural transformation actually has a universal +property, within the category of OFEs: Non-expansive maps $\later A \to +B$ are equivalent to contractive maps $A \to B$. + +[OFE]: Cat.Instances.OFE.html +[complete OFE]: Cat.Instances.OFE.Complete.html +[bfpt]: Cat.Instances.OFE.Complete.html#banachs-fixed-point-theorem + + + +To emphasize that the distinction between $A$ and $\later A$ is entirely +in skipping a step, we have formatted the construction below so the +cases are split between time zero and positive time. + +```agda + Later : OFE-on ℓ' A + Later .within zero x y = Lift ℓ' ⊤ + Later .within (suc n) x y = x ≈[ n ] y + + -- Trivial! + Later .has-is-ofe .has-is-prop zero = λ _ _ _ _ _ → _ + Later .has-is-ofe .≈-trans zero = _ + Later .has-is-ofe .≈-refl zero = _ + Later .has-is-ofe .≈-sym zero = _ + Later .has-is-ofe .step zero = _ + + -- Just like A! + Later .has-is-ofe .has-is-prop (suc n) = P.has-is-prop n + Later .has-is-ofe .≈-trans (suc n) = P.≈-trans n + Later .has-is-ofe .≈-refl (suc n) = P.≈-refl n + Later .has-is-ofe .≈-sym (suc n) = P.≈-sym n + Later .has-is-ofe .step (suc n) = P.step n + + Later .has-is-ofe .bounded x y = _ + Later .has-is-ofe .limit x y a = P.limit x y λ n → a (suc n) +``` + +```agda +▶ : ∀ {ℓ ℓ'} → OFE ℓ ℓ' → OFE ℓ ℓ' +▶ (A , O) = from-ofe-on (Later O) + +to-later : ∀ {ℓ ℓ'} (A : OFE ℓ ℓ') → OFEs.Hom A (▶ A) +to-later A .hom x = x +to-later A .preserves .pres-≈ {n = zero} α = lift tt +to-later A .preserves .pres-≈ {n = suc n} α = A .snd .OFE-on.step n _ _ α +``` + + + +The universal property promised, that $\later P$ represents the +contractive maps with domain $P$, is a short exercise in shuffling +indices: + +```agda + later-contractive + : (f : A → B) + → is-non-expansive f (Later P) Q ≃ is-contractive f P Q + later-contractive f = prop-ext! {A = is-non-expansive _ _ _} {B = is-contractive _ _ _} + (λ { r .contract {n = n} α → r .pres-≈ {n = suc n} α }) + (λ { r .pres-≈ {n = zero} α → Q.bounded _ _ + ; r .pres-≈ {n = suc n} α → r .contract α + }) +``` + + + +We can put this together to define something akin to **Löb induction**: +if $A$ is an inhabited, [complete OFE], Banach's fixed point theorem +implies that non-expansive functions $\later P \to P$ have fixed points. + +```agda + löb : ∥ A ∥ → is-cofe P → (f : Later P →ⁿᵉ P) → Σ A λ x → f .map x ≡ x + löb pt lim f = banach P lim pt record { + contract = λ n p → f .pres-≈ (suc n) p } +``` diff --git a/src/Cat/Instances/OFE/Product.lagda.md b/src/Cat/Instances/OFE/Product.lagda.md new file mode 100644 index 000000000..7dc3ea053 --- /dev/null +++ b/src/Cat/Instances/OFE/Product.lagda.md @@ -0,0 +1,188 @@ + + +```agda +module Cat.Instances.OFE.Product where +``` + +# Products of OFEs + +The [category of OFEs][OFE] admits [products]: the relations are, +levelwise, pairwise! That is, $(x, y) \within{n} (x', y')$ if $x +\within{n} x'$ and $y \within{n} y'$. Distributing the axioms over +products is enough to establish that this is actually an OFE. + +[OFE]: Cat.Instances.OFE.html +[products]: Cat.Diagram.Product.html + + + +```agda + ×-OFE : OFE-on (ℓa' ⊔ ℓb') (A × B) + ×-OFE .within n (x , y) (x' , y') = (x ≈[ n ] x') × (y ≈[ n ] y') + ×-OFE .has-is-ofe .has-is-prop n x y = hlevel 1 + + ×-OFE .has-is-ofe .≈-refl n = O.≈-refl n , P.≈-refl n + ×-OFE .has-is-ofe .≈-sym n (p , q) = O.≈-sym n p , P.≈-sym n q + ×-OFE .has-is-ofe .≈-trans n (p , q) (p' , q') = + O.≈-trans n p p' , P.≈-trans n q q' + + ×-OFE .has-is-ofe .bounded (a , b) (a' , b') = O.bounded a a' , P.bounded b b' + ×-OFE .has-is-ofe .step n _ _ (p , p') = O.step n _ _ p , P.step n _ _ p' + ×-OFE .has-is-ofe .limit x y f = + ap₂ _,_ (O.limit _ _ λ n → f n .fst) (P.limit _ _ λ n → f n .snd) +``` + + + +By construction, this OFE is actually the proper categorical product of +the OFE structures we started with: since this is a very concrete +category, most of the reasoning piggy-backs off of that for types, which +is almost definitional. Other than the noise inherent to formalisation, +the argument is immediate: + +```agda +OFE-Product : ∀ {ℓ ℓ'} A B → Product (OFEs ℓ ℓ') A B +OFE-Product A B .apex = from-ofe-on (×-OFE (A .snd) (B .snd)) +OFE-Product A B .π₁ .hom = fst +OFE-Product A B .π₁ .preserves .pres-≈ = fst + +OFE-Product A B .π₂ .hom = snd +OFE-Product A B .π₂ .preserves .pres-≈ = snd + +OFE-Product A B .has-is-product .⟨_,_⟩ f g .hom x = f # x , g # x +OFE-Product A B .has-is-product .⟨_,_⟩ f g .preserves .pres-≈ p = + f .preserves .pres-≈ p , g .preserves .pres-≈ p + +OFE-Product A B .has-is-product .π₁∘factor = Homomorphism-path λ x → refl +OFE-Product A B .has-is-product .π₂∘factor = Homomorphism-path λ x → refl +OFE-Product A B .has-is-product .unique o p q = Homomorphism-path λ x → + ap₂ _,_ (p #ₚ x) (q #ₚ x) +``` + + + +## Indexed products + +We now turn to a slightly more complicated case: _indexed_ products of +OFEs: because Agda is, by default, a predicative theory, we run into +some issues with universe levels when defining the indexed product. +Let's see them: + +Suppose we have an index type $I : \ty$ in the $i$th universe, and +a family $P_i : \ty$, valued now in the $p$th universe. Moreover, +the family $P_i$ should be pointwise an OFE, with nearness relation +living in, let's say, the $r$th universe. We will define the relation on +$\prod P$ to be + +$$ +\forall i, f(i) \within{n} g(i) \text{,} \tag 1 +$$ + +but this type is _too large_: Since we quantify over $i : I$, and return +one of the approximate equalities, it must live in the $(r \sqcup i)$th +universe; but if we want indexed products to be in the same category we +started with, it should live in the $r$th! + +Fortunately, to us, this is an annoyance, not an impediment: here in the +1Lab, we assume [propositional resizing][omega] throughout. Since the +product type $(1)$ is a proposition, it is equivalent to a small type, +so we can put it in any universe, including the $r$th. + +[omega]: 1Lab.Resizing.html + +The construction is essentially the same as for binary products: +however, since resizing is explicit, we have to do a bit more faffing +about to get the actual inhabitant of $(1)$ that we're interested in. + +```agda + Π-OFE : OFE-on ℓr (∀ i → F i) + Π-OFE .within n f g = Lift ℓr (□ (∀ i → f i ≈[ n ] g i)) + Π-OFE .has-is-ofe .has-is-prop n x y = Lift-is-hlevel 1 squash + Π-OFE .has-is-ofe .≈-refl n = lift (inc λ i → P.≈-refl n) + Π-OFE .has-is-ofe .≈-sym n (lift x) = lift do + x ← x + pure λ i → P.≈-sym n (x i) + Π-OFE .has-is-ofe .≈-trans n (lift p) (lift q) = lift do + p ← p + q ← q + pure λ i → P.≈-trans n (p i) (q i) + Π-OFE .has-is-ofe .bounded x y = lift (inc λ i → P.bounded (x i) (y i)) + Π-OFE .has-is-ofe .step n x y (lift p) = lift do + p ← p + pure λ i → P.step n (x i) (y i) (p i) + Π-OFE .has-is-ofe .limit x y wit i j = P.limit (x j) (y j) (λ n → wit' n j) i + where + wit' : ∀ n i → within (P i) n (x i) (y i) + wit' n i = out! {pa = hlevel 1} (wit n .Lift.lower) i +``` + + + +And, again, by essentially the same argument, we can establish that this +is the categorical [_indexed_ product][ip] of $P$ in the category of +OFEs, as long as all the sizes match up. + +[ip]: Cat.Diagram.Product.Indexed.html + +```agda +OFE-Indexed-product + : ∀ {ℓo ℓr} {I : Type ℓo} (F : I → OFE ℓo ℓr) + → Indexed-product (OFEs ℓo ℓr) F +OFE-Indexed-product F .ΠF = from-ofe-on $ + Π-OFE (λ i → ∣ F i .fst ∣) (λ i → F i .snd) +OFE-Indexed-product F .π i .hom f = f i +OFE-Indexed-product F .π i .preserves .pres-≈ α = + out! {pa = F i .snd .has-is-prop _ _ _} ((_$ i) <$> α .Lift.lower) +OFE-Indexed-product F .has-is-ip .tuple f .hom x i = f i # x +OFE-Indexed-product F .has-is-ip .tuple f .preserves .pres-≈ wit = + lift $ inc λ i → f i .preserves .pres-≈ wit +OFE-Indexed-product F .has-is-ip .commute = Homomorphism-path λ x → refl +OFE-Indexed-product F .has-is-ip .unique f prf = + Homomorphism-path λ x → funext λ y → prf y #ₚ x +``` diff --git a/src/Data/List.lagda.md b/src/Data/List.lagda.md index 345d5306a..f8d8c4f71 100644 --- a/src/Data/List.lagda.md +++ b/src/Data/List.lagda.md @@ -1,11 +1,13 @@ @@ -156,37 +158,23 @@ ap-∷ x≡y xs≡ys i = x≡y i ∷ xs≡ys i ⚠️ TODO: Explain these ⚠️ ```agda -mapUp : (Nat → A → B) → Nat → List A → List B -mapUp f _ [] = [] -mapUp f n (x ∷ xs) = f n x ∷ mapUp f (suc n) xs - -length : List A → Nat -length [] = zero -length (x ∷ x₁) = suc (length x₁) - -concat : List (List A) → List A -concat [] = [] -concat (x ∷ xs) = x ++ concat xs - -reverse : List A → List A -reverse = go [] where - go : List A → List A → List A - go acc [] = acc - go acc (x ∷ xs) = go (x ∷ acc) xs - -_∷r_ : List A → A → List A -xs ∷r x = xs ++ (x ∷ []) - -all=? : (A → A → Bool) → List A → List A → Bool -all=? eq=? [] [] = true -all=? eq=? [] (x ∷ ys) = false -all=? eq=? (x ∷ xs) [] = false -all=? eq=? (x ∷ xs) (y ∷ ys) = and (eq=? x y) (all=? eq=? xs ys) - -enumerate : ∀ {ℓ} {A : Type ℓ} → List A → List (Nat × A) -enumerate = go 0 where - go : Nat → List _ → List (Nat × _) - go x [] = [] - go x (a ∷ b) = (x , a) ∷ go (suc x) b + +take-length : ∀ {ℓ} {A : Type ℓ} (xs : List A) → take (length xs) xs ≡ xs +take-length [] = refl +take-length (x ∷ xs) = ap (x ∷_) (take-length xs) + +take-length-more + : ∀ {ℓ} {A : Type ℓ} (xs : List A) (n : Nat) + → length xs ≤ n + → take n xs ≡ xs +take-length-more [] zero wit = refl +take-length-more [] (suc n) wit = refl +take-length-more (x ∷ xs) (suc n) (s≤s wit) = ap (x ∷_) (take-length-more xs n wit) + +instance + -- List isn't really a type on the same footing as all the others, but + -- we're here, so we might as well, right? + decomp-list : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (List A) + decomp-list = decomp (quote ListPath.List-is-hlevel) (`level-minus 2 ∷ `search ∷ []) ``` --> diff --git a/src/Data/List/Base.lagda.md b/src/Data/List/Base.lagda.md index c54a756d2..fa7df9cb2 100644 --- a/src/Data/List/Base.lagda.md +++ b/src/Data/List/Base.lagda.md @@ -4,6 +4,7 @@ open import 1Lab.Path open import 1Lab.Type open import Data.Product.NAry +open import Data.Bool ``` --> @@ -111,4 +112,42 @@ _++_ : ∀ {ℓ} {A : Type ℓ} → List A → List A → List A (x ∷ xs) ++ ys = x ∷ (xs ++ ys) infixr 5 _++_ + +mapUp : (Nat → A → B) → Nat → List A → List B +mapUp f _ [] = [] +mapUp f n (x ∷ xs) = f n x ∷ mapUp f (suc n) xs + +length : List A → Nat +length [] = zero +length (x ∷ x₁) = suc (length x₁) + +concat : List (List A) → List A +concat [] = [] +concat (x ∷ xs) = x ++ concat xs + +reverse : List A → List A +reverse = go [] where + go : List A → List A → List A + go acc [] = acc + go acc (x ∷ xs) = go (x ∷ acc) xs + +_∷r_ : List A → A → List A +xs ∷r x = xs ++ (x ∷ []) + +all=? : (A → A → Bool) → List A → List A → Bool +all=? eq=? [] [] = true +all=? eq=? [] (x ∷ ys) = false +all=? eq=? (x ∷ xs) [] = false +all=? eq=? (x ∷ xs) (y ∷ ys) = and (eq=? x y) (all=? eq=? xs ys) + +enumerate : ∀ {ℓ} {A : Type ℓ} → List A → List (Nat × A) +enumerate = go 0 where + go : Nat → List _ → List (Nat × _) + go x [] = [] + go x (a ∷ b) = (x , a) ∷ go (suc x) b + +take : ∀ {ℓ} {A : Type ℓ} → Nat → List A → List A +take 0 xs = [] +take (suc n) [] = [] +take (suc n) (x ∷ xs) = x ∷ take n xs ``` diff --git a/src/Meta/Traverse.lagda.md b/src/Meta/Traverse.lagda.md index e21cfe5d4..497cf5864 100644 --- a/src/Meta/Traverse.lagda.md +++ b/src/Meta/Traverse.lagda.md @@ -48,3 +48,4 @@ instance Traverse-Maybe : Traverse (eff Maybe) Traverse-Maybe .Traverse.traverse f (just x) = just <$> f x Traverse-Maybe .Traverse.traverse f nothing = pure nothing +``` diff --git a/src/Prim/Data/String.lagda.md b/src/Prim/Data/String.lagda.md index d467e1786..f328d9259 100644 --- a/src/Prim/Data/String.lagda.md +++ b/src/Prim/Data/String.lagda.md @@ -2,7 +2,7 @@ ```agda open import 1Lab.Type -open import Data.List +open import Data.List.Base open import Prim.Data.Maybe open import Prim.Literals diff --git a/src/preamble.tex b/src/preamble.tex index edacb4994..1f020ed0a 100644 --- a/src/preamble.tex +++ b/src/preamble.tex @@ -54,6 +54,7 @@ \newcommand{\eps}{\varepsilon} \newcommand{\To}{\Rightarrow} +\newcommand{\later}{\mathop{\blacktriangleright}} \newcommand{\adj}{\rightleftarrows} \newcommand{\epi}{\twoheadrightarrow} \newcommand{\mono}{\hookrightarrow} @@ -65,6 +66,7 @@ \newcommand{\xot}[1]{\xleftarrow{#1}} \newcommand{\xepi}[1]{\xtwoheadrightarrow{#1}} \newcommand{\xmono}[1]{\xhookrightarrow{#1}} +\newcommand{\within}[1]{\overset{#1}{\approx}} \DeclareMathOperator{\coker}{coker} \DeclareMathOperator*{\colim}{colim}