def: adjoints are invariant under natural isos

the1lab · Jul 17, 2023 · da71f83 · da71f83
1 parent 31dac64
commit da71f83
Show file tree

Hide file tree

Showing 5 changed files with 270 additions and 69 deletions.
diff --git a/src/Cat/Functor/Adjoint.lagda.md b/src/Cat/Functor/Adjoint.lagda.md
@@ -9,6 +9,8 @@ description: |
 ```agda
 open import Cat.Diagram.Initial
 open import Cat.Instances.Comma
+open import Cat.Instances.Functor
+open import Cat.Instances.Functor.Compose
 open import Cat.Prelude
 
 import Cat.Functor.Reasoning as Func
@@ -732,7 +734,76 @@ record make-left-adjoint (R : Functor D C) : Type (adj-level C D) where
   to-left-adjoint : to-functor ⊣ R
   to-left-adjoint = universal-maps→L⊣R R to-universal-arrows
 
-open make-left-adjoint
 module Ml = make-left-adjoint
 ```
 -->
+
+<!--
+```agda
+adjoint-natural-iso
+  : ∀ {L L' : Functor C D} {R R' : Functor D C}
+  → natural-iso L L' → natural-iso R R'
+  → L ⊣ R
+  → L' ⊣ R'
+adjoint-natural-iso {C = C} {D = D} {L} {L'} {R} {R'} α β L⊣R = L'⊣R' where
+  open _⊣_ L⊣R
+  module α = natural-iso α
+  module β = natural-iso β
+  open _=>_
+  module C = Cat.Reasoning C
+  module D = Cat.Reasoning D
+  module L = Func L
+  module L' = Func L'
+  module R = Func R
+  module R' = Func R'
+
+  -- Abbreviations for equational reasoning
+  α→ : ∀ {x} → D.Hom (L.₀ x) (L'.₀ x)
+  α→ {x} = α.to .η x
+
+  α← : ∀ {x} → D.Hom (L'.₀ x) (L.₀ x)
+  α← {x} = α.from .η x
+
+  β→ : ∀ {x} → C.Hom (R.₀ x) (R'.₀ x)
+  β→ {x} = β.to .η x
+
+  β← : ∀ {x} → C.Hom (R'.₀ x) (R.₀ x)
+  β← {x} = β.from .η x
+
+  L'⊣R' : L' ⊣ R'
+  L'⊣R' ._⊣_.unit =  (β.to ◆ α.to) ∘nt unit
+  L'⊣R' ._⊣_.counit = counit ∘nt (α.from ◆ β.from)
+  L'⊣R' ._⊣_.zig =
+    (counit.ε _ D.∘ (L.₁ β← D.∘ α←)) D.∘ L'.₁ (⌜ R'.₁ α→ C.∘ β→ ⌝ C.∘ unit.η _) ≡⟨ ap! (sym $ β.to .is-natural _ _ _) ⟩
+    (counit.ε _ D.∘ ⌜ L.₁ β← D.∘ α← ⌝) D.∘ L'.₁ ((β→ C.∘ R.₁ α→) C.∘ unit.η _)  ≡⟨ ap! (sym $ α.from .is-natural _ _ _) ⟩
+    (counit.ε _ D.∘ α← D.∘ L'.₁ β←) D.∘ L'.₁ ((β→ C.∘ R.₁ α→) C.∘ unit.η _)     ≡⟨ D.pullr (D.pullr (L'.collapse (C.pulll (C.cancell (β.invr ηₚ _))))) ⟩
+    counit.ε _ D.∘ α← D.∘ L'.₁ (R.₁ α→ C.∘ unit.η _)                            ≡⟨ ap (counit.ε _ D.∘_) (α.from .is-natural _ _ _) ⟩
+    counit.ε _ D.∘ L.₁ (R.₁ α→ C.∘ unit.η _) D.∘ α←                             ≡⟨ D.push-inner (L.F-∘ _ _) ⟩
+    (counit.ε _ D.∘ L.₁ (R.₁ α→)) D.∘ (L.₁ (unit.η _) D.∘ α←)                   ≡⟨ D.pushl (counit.is-natural _ _ _) ⟩
+    α→ D.∘ counit.ε _ D.∘ L.₁ (unit.η _) D.∘ α←                                 ≡⟨ ap (α→ D.∘_) (D.cancell zig) ⟩
+    α→ D.∘ α←                                                                   ≡⟨ α.invl ηₚ _ ⟩
+    D.id ∎
+  L'⊣R' ._⊣_.zag =
+    R'.₁ (counit.ε _ D.∘ L.₁ β← D.∘ α←) C.∘ ((R'.₁ α→ C.∘ β→) C.∘ unit.η _) ≡⟨ C.extendl (C.pulll (R'.collapse (D.pullr (D.cancelr (α.invr ηₚ _))))) ⟩
+    R'.₁ (counit.ε _ D.∘ L.₁ β←) C.∘ β→ C.∘ unit.η _                        ≡⟨ C.extendl (sym (β.to .is-natural _ _ _)) ⟩
+    β→ C.∘ R.₁ (counit.ε _ D.∘ L.₁ β←) C.∘ unit.η _                         ≡⟨ C.push-inner (R.F-∘ _ _) ⟩
+    ((β→ C.∘ R.₁ (counit.ε _)) C.∘ (R.₁ (L.₁ β←) C.∘ unit.η _))             ≡⟨ ap₂ C._∘_ refl (sym $ unit.is-natural _ _ _) ⟩
+    (β→ C.∘ R.₁ (counit.ε _)) C.∘ (unit.η _ C.∘ β←)                         ≡⟨ C.cancel-inner zag ⟩
+    β→ C.∘ β←                                                               ≡⟨ β.invl ηₚ _ ⟩
+    C.id ∎
+
+adjoint-natural-isol
+  : ∀ {L L' : Functor C D} {R : Functor D C}
+  → natural-iso L L'
+  → L ⊣ R
+  → L' ⊣ R
+adjoint-natural-isol α = adjoint-natural-iso α idni
+
+adjoint-natural-isor
+  : ∀ {L : Functor C D} {R R' : Functor D C}
+  → natural-iso R R'
+  → L ⊣ R
+  → L ⊣ R'
+adjoint-natural-isor β = adjoint-natural-iso idni β
+```
+-->
diff --git a/src/Cat/Functor/Equivalence.lagda.md b/src/Cat/Functor/Equivalence.lagda.md
@@ -778,3 +778,32 @@ As a corollary, equivalences preserve all families over hom sets.
       (λ c c' → Lift-is-hlevel n (C-hlevel c c')) d d'
 ```
 -->
+
+Equivalences are also invariant under natural isomorphisms.
+
+```agda
+is-equivalence-natural-iso
+  : ∀ {F G : Functor C D}
+  → natural-iso 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
+  module C = Cat.Reasoning C
+  module D = Cat.Reasoning D
+
+  G-eqv : is-equivalence G
+  G-eqv .F⁻¹ = F-eqv .F⁻¹
+  G-eqv .F⊣F⁻¹ = adjoint-natural-isol α (F-eqv .F⊣F⁻¹)
+  G-eqv .unit-iso x =
+    C.invertible-∘
+      (C.invertible-∘
+        (F-map-invertible (F-eqv .F⁻¹) (natural-iso→invertible α x))
+        C.id-invertible)
+      (F-eqv .unit-iso x)
+  G-eqv .counit-iso x =
+    D.invertible-∘
+      (F-eqv .counit-iso x)
+      (D.invertible-∘
+        (F-map-invertible F C.id-invertible)
+        (natural-iso→invertible α _ D.invertible⁻¹))
+```
diff --git a/src/Cat/Instances/Functor.lagda.md b/src/Cat/Instances/Functor.lagda.md
@@ -574,6 +574,13 @@ module
       (CD.is-invertible.invl inv ηₚ x)
       (CD.is-invertible.invr inv ηₚ x)
 
+  natural-iso→iso
+    : natural-iso F G
+    → ∀ x → F .F₀ x D.≅ G .F₀ x
+  natural-iso→iso α x =
+    D.make-iso (α.to .η x) (α.from .η x) (α.invl ηₚ x) (α.invr ηₚ x)
+    where module α = natural-iso α
+
   is-natural-invertible→natural-iso
     : ∀ {α : F => G}
     → is-natural-invertible α
@@ -587,6 +594,13 @@ module
   natural-iso→is-natural-invertible i =
     CD.iso→invertible i
 
+  natural-iso→invertible
+    : (α : natural-iso F G)
+    → ∀ x → D.is-invertible (α .CD._≅_.to .η x)
+  natural-iso→invertible α x =
+    is-natural-invertible→invertible (natural-iso→is-natural-invertible α) x
+
+
 open _=>_
 
 _ni^op : natural-iso F G → natural-iso (Functor.op F) (Functor.op G)

diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md
@@ -396,13 +396,15 @@ choice of map $A \to B$, together with a specified inverse.
 
 ```agda
 record Inverses (f : Hom a b) (g : Hom b a) : Type h where
+  no-eta-equality
   field
     invl : f ∘ g ≡ id
     invr : g ∘ f ≡ id
 
 open Inverses
 
 record is-invertible (f : Hom a b) : Type h where
+  no-eta-equality
   field
     inv : Hom b a
     inverses : Inverses f inv
@@ -415,6 +417,7 @@ record is-invertible (f : Hom a b) : Type h where
   op .inverses .Inverses.invr = invl inverses
 
 record _≅_ (a b : Ob) : Type h where
+  no-eta-equality
   field
     to       : Hom a b
     from     : Hom b a
@@ -453,6 +456,76 @@ is-invertible-is-prop {a = a} {b = b} {f = f} g h = p where
 
 We note that the identity morphism is always iso, and that isos compose:
 
+```agda
+id-invertible : ∀ {a} → is-invertible (id {a})
+id-invertible .is-invertible.inv = id
+id-invertible .is-invertible.inverses .invl = idl id
+id-invertible .is-invertible.inverses .invr = idl id
+
+id-iso : a ≅ a
+id-iso .to = id
+id-iso .from = id
+id-iso .inverses .invl = idl id
+id-iso .inverses .invr = idl id
+
+Isomorphism = _≅_
+
+Inverses-∘ : {f : Hom a b} {f⁻¹ : Hom b a} {g : Hom b c} {g⁻¹ : Hom c b}
+           → Inverses f f⁻¹ → Inverses g g⁻¹ → Inverses (g ∘ f) (f⁻¹ ∘ g⁻¹)
+Inverses-∘ {f = f} {f⁻¹} {g} {g⁻¹} finv ginv = record { invl = l ; invr = r } where
+  module finv = Inverses finv
+  module ginv = Inverses ginv
+
+  abstract
+    l : (g ∘ f) ∘ f⁻¹ ∘ g⁻¹ ≡ id
+    l = (g ∘ f) ∘ f⁻¹ ∘ g⁻¹ ≡⟨ cat! C ⟩
+        g ∘ (f ∘ f⁻¹) ∘ g⁻¹ ≡⟨ (λ i → g ∘ finv.invl i ∘ g⁻¹) ⟩
+        g ∘ id ∘ g⁻¹        ≡⟨ cat! C ⟩
+        g ∘ g⁻¹             ≡⟨ ginv.invl ⟩
+        id                  ∎
+
+    r : (f⁻¹ ∘ g⁻¹) ∘ g ∘ f ≡ id
+    r = (f⁻¹ ∘ g⁻¹) ∘ g ∘ f ≡⟨ cat! C ⟩
+        f⁻¹ ∘ (g⁻¹ ∘ g) ∘ f ≡⟨ (λ i → f⁻¹ ∘ ginv.invr i ∘ f) ⟩
+        f⁻¹ ∘ id ∘ f        ≡⟨ cat! C ⟩
+        f⁻¹ ∘ f             ≡⟨ finv.invr ⟩
+        id                  ∎
+
+_∘Iso_ : a ≅ b → b ≅ c → a ≅ c
+(f ∘Iso g) .to = g .to ∘ f .to
+(f ∘Iso g) .from = f .from ∘ g .from
+(f ∘Iso g) .inverses = Inverses-∘ (f .inverses) (g .inverses)
+
+infixr 40 _∘Iso_
+
+invertible-∘
+  : ∀ {f : Hom b c} {g : Hom a b}
+  → is-invertible f → is-invertible g
+  → is-invertible (f ∘ g)
+invertible-∘ f-inv g-inv = record
+  { inv = g-inv.inv ∘ f-inv.inv
+  ; inverses = Inverses-∘ g-inv.inverses f-inv.inverses
+  }
+  where
+    module f-inv = is-invertible f-inv
+    module g-inv = is-invertible g-inv
+
+_invertible⁻¹
+  : ∀ {f : Hom a b} → (f-inv : is-invertible f)
+  → is-invertible (is-invertible.inv f-inv)
+_invertible⁻¹ {f = f} f-inv .is-invertible.inv = f
+_invertible⁻¹ f-inv .is-invertible.inverses .invl =
+  is-invertible.invr f-inv
+_invertible⁻¹ f-inv .is-invertible.inverses .invr =
+  is-invertible.invl f-inv
+
+_Iso⁻¹ : a ≅ b → b ≅ a
+(f Iso⁻¹) .to = f .from
+(f Iso⁻¹) .from = f .to
+(f Iso⁻¹) .inverses .invl = f .inverses .invr
+(f Iso⁻¹) .inverses .invr = f .inverses .invl
+```
+
 <!--
 ```agda
 make-inverses : {f : Hom a b} {g : Hom b a} → f ∘ g ≡ id → g ∘ f ≡ id → Inverses f g
@@ -550,6 +623,18 @@ abstract
   → PathP (λ i → p i ≅ q i) f g
 ≅-pathp p q {f = f} {g = g} r = ≅-pathp-internal p q r (inverse-unique p q {f = f} {g = g} r)
 
+≅-pathp-from
+  : (p : a ≡ c) (q : b ≡ d) {f : a ≅ b} {g : c ≅ d}
+  → PathP (λ i → Hom (q i) (p i)) (f ._≅_.from) (g ._≅_.from)
+  → PathP (λ i → p i ≅ q i) f g
+≅-pathp-from p q {f = f} {g = g} r = ≅-pathp-internal p q (inverse-unique q p {f = f Iso⁻¹} {g = g Iso⁻¹} r) r
+
+≅-path : {f g : a ≅ b} → f ._≅_.to ≡ g ._≅_.to → f ≡ g
+≅-path = ≅-pathp refl refl
+
+≅-path-from : {f g : a ≅ b} → f ._≅_.from ≡ g ._≅_.from → f ≡ g
+≅-path-from = ≅-pathp-from refl refl
+
 ↪-pathp
   : {a : I → Ob} {b : I → Ob} {f : a i0 ↪ b i0} {g : a i1 ↪ b i1}
   → PathP (λ i → Hom (a i) (b i)) (f .mor) (g .mor)
@@ -586,73 +671,6 @@ abstract
 ```
 -->
 
-```agda
-id-invertible : ∀ {a} → is-invertible (id {a})
-id-invertible .is-invertible.inv = id
-id-invertible .is-invertible.inverses .invl = idl id
-id-invertible .is-invertible.inverses .invr = idl id
-
-id-iso : a ≅ a
-id-iso .to = id
-id-iso .from = id
-id-iso .inverses .invl = idl id
-id-iso .inverses .invr = idl id
-
-Isomorphism = _≅_
-
-Inverses-∘ : {f : Hom a b} {f⁻¹ : Hom b a} {g : Hom b c} {g⁻¹ : Hom c b}
-           → Inverses f f⁻¹ → Inverses g g⁻¹ → Inverses (g ∘ f) (f⁻¹ ∘ g⁻¹)
-Inverses-∘ {f = f} {f⁻¹} {g} {g⁻¹} finv ginv = record { invl = l ; invr = r } where
-  module finv = Inverses finv
-  module ginv = Inverses ginv
-
-  abstract
-    l : (g ∘ f) ∘ f⁻¹ ∘ g⁻¹ ≡ id
-    l = (g ∘ f) ∘ f⁻¹ ∘ g⁻¹ ≡⟨ cat! C ⟩
-        g ∘ (f ∘ f⁻¹) ∘ g⁻¹ ≡⟨ (λ i → g ∘ finv.invl i ∘ g⁻¹) ⟩
-        g ∘ id ∘ g⁻¹        ≡⟨ cat! C ⟩
-        g ∘ g⁻¹             ≡⟨ ginv.invl ⟩
-        id                  ∎
-
-    r : (f⁻¹ ∘ g⁻¹) ∘ g ∘ f ≡ id
-    r = (f⁻¹ ∘ g⁻¹) ∘ g ∘ f ≡⟨ cat! C ⟩
-        f⁻¹ ∘ (g⁻¹ ∘ g) ∘ f ≡⟨ (λ i → f⁻¹ ∘ ginv.invr i ∘ f) ⟩
-        f⁻¹ ∘ id ∘ f        ≡⟨ cat! C ⟩
-        f⁻¹ ∘ f             ≡⟨ finv.invr ⟩
-        id                  ∎
-
-_∘Iso_ : a ≅ b → b ≅ c → a ≅ c
-(f ∘Iso g) .to = g .to ∘ f .to
-(f ∘Iso g) .from = f .from ∘ g .from
-(f ∘Iso g) .inverses = Inverses-∘ (f .inverses) (g .inverses)
-
-invertible-∘
-  : ∀ {f : Hom b c} {g : Hom a b}
-  → is-invertible f → is-invertible g
-  → is-invertible (f ∘ g)
-invertible-∘ f-inv g-inv = record
-  { inv = g-inv.inv ∘ f-inv.inv
-  ; inverses = Inverses-∘ g-inv.inverses f-inv.inverses
-  }
-  where
-    module f-inv = is-invertible f-inv
-    module g-inv = is-invertible g-inv
-
-_invertible⁻¹
-  : ∀ {f : Hom a b} → (f-inv : is-invertible f)
-  → is-invertible (is-invertible.inv f-inv)
-_invertible⁻¹ {f = f} f-inv .is-invertible.inv = f
-_invertible⁻¹ f-inv .is-invertible.inverses .invl =
-  is-invertible.invr f-inv
-_invertible⁻¹ f-inv .is-invertible.inverses .invr =
-  is-invertible.invl f-inv
-
-_Iso⁻¹ : a ≅ b → b ≅ a
-(f Iso⁻¹) .to = f .from
-(f Iso⁻¹) .from = f .to
-(f Iso⁻¹) .inverses .invl = f .inverses .invr
-(f Iso⁻¹) .inverses .invr = f .inverses .invl
-```
 
 We also note that invertible morphisms are both epic and monic.