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..3fa4ac3a8 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 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 @@ -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..010b7f534 100644 --- a/src/Cat/Diagram/Colimit/Representable.lagda.md +++ b/src/Cat/Diagram/Colimit/Representable.lagda.md @@ -1,7 +1,7 @@ @@ -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/Instances/Family.lagda.md b/src/Cat/Displayed/Instances/Family.lagda.md index 49a6f5e77..4ab841d3a 100644 --- a/src/Cat/Displayed/Instances/Family.lagda.md +++ b/src/Cat/Displayed/Instances/Family.lagda.md @@ -8,7 +8,7 @@ open import Cat.Displayed.Cartesian open import Cat.Displayed.Fibre open import Cat.Displayed.GenericObject -open import Cat.Functor.Base +open import Cat.Functor.Properties open import Cat.Functor.Equivalence open import Cat.Gaunt open import Cat.Instances.Discrete diff --git a/src/Cat/Displayed/Instances/Lifting.lagda.md b/src/Cat/Displayed/Instances/Lifting.lagda.md index dfda25341..29ce1de4c 100644 --- a/src/Cat/Displayed/Instances/Lifting.lagda.md +++ b/src/Cat/Displayed/Instances/Lifting.lagda.md @@ -1,6 +1,6 @@ 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..b45c1eb79 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 @@ -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.Instances.Functor.Univalent.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..afef88324 --- /dev/null +++ b/src/Cat/Functor/Closed.lagda.md @@ -0,0 +1,74 @@ + + +```agda +module Cat.Functor.Closed where +``` + + + +```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 + + 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..9b689a281 100644 --- a/src/Cat/Functor/Dense.lagda.md +++ b/src/Cat/Functor/Dense.lagda.md @@ -4,7 +4,7 @@ open import Cat.Instances.Shape.Terminal open import Cat.Diagram.Colimit.Base open import Cat.Functor.Kan.Nerve open import Cat.Instances.Comma -open import Cat.Functor.Base +open import Cat.Functor.Properties 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..2ef793fb1 100644 --- a/src/Cat/Functor/Equivalence.lagda.md +++ b/src/Cat/Functor/Equivalence.lagda.md @@ -1,5 +1,6 @@ ```agda -open import Cat.Instances.Functor +open import Cat.Functor.Properties +open import Cat.Functor.Naturality open import Cat.Functor.Adjoint open import Cat.Functor.Adjoint.Compose open import Cat.Functor.Base @@ -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 @@ -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..1851360ff 100644 --- a/src/Cat/Functor/FullSubcategory.lagda.md +++ b/src/Cat/Functor/FullSubcategory.lagda.md @@ -1,7 +1,7 @@ @@ -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..a4a03ca35 100644 --- a/src/Cat/Functor/Kan/Unique.lagda.md +++ b/src/Cat/Functor/Kan/Unique.lagda.md @@ -1,7 +1,9 @@ @@ -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ⁿ ``` --> @@ -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..3aedc31df 100644 --- a/src/Cat/Functor/Pullback.lagda.md +++ b/src/Cat/Functor/Pullback.lagda.md @@ -6,7 +6,7 @@ open import Cat.Diagram.Initial open import Cat.Functor.Adjoint open import Cat.Instances.Comma open import Cat.Instances.Slice -open import Cat.Functor.Base +open import Cat.Functor.Properties open import Cat.Prelude import Cat.Reasoning diff --git a/src/Cat/Functor/Reasoning/FullyFaithful.lagda.md b/src/Cat/Functor/Reasoning/FullyFaithful.lagda.md index 13e6e7971..75f670d37 100644 --- a/src/Cat/Functor/Reasoning/FullyFaithful.lagda.md +++ b/src/Cat/Functor/Reasoning/FullyFaithful.lagda.md @@ -1,5 +1,6 @@ + +```agda +module Cat.Functor.Univalence where +``` + + + +Our previous results about [paths between functors], [componentwise +invertibility], and general reasoning in univalent categories assemble +into the following very straightforward proof that $[\cC,\cD]$ is +univalent whenever $\cD$ is. + +[identity of functors]: 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..113def3eb 100644 --- a/src/Cat/Functor/WideSubcategory.lagda.md +++ b/src/Cat/Functor/WideSubcategory.lagda.md @@ -1,6 +1,6 @@ - - - - -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..7557e0b68 100644 --- a/src/Cat/Instances/InternalFunctor.lagda.md +++ b/src/Cat/Instances/InternalFunctor.lagda.md @@ -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