From 343254ab4d6861b719c0d766067dc210ab557e15 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Fri, 1 Jan 2021 17:03:44 -0800 Subject: [PATCH 01/11] Define Monadic Adjunctions --- src/Categories/Adjoint/Monadic.agda | 32 +++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 src/Categories/Adjoint/Monadic.agda diff --git a/src/Categories/Adjoint/Monadic.agda b/src/Categories/Adjoint/Monadic.agda new file mode 100644 index 000000000..a86a01319 --- /dev/null +++ b/src/Categories/Adjoint/Monadic.agda @@ -0,0 +1,32 @@ +{-# OPTIONS --without-K --safe #-} + +-- Monadic Adjunctions +-- https://ncatlab.org/nlab/show/monadic+adjunction +module Categories.Adjoint.Monadic where + +open import Level + +open import Categories.Adjoint +open import Categories.Adjoint.Properties +open import Categories.Category +open import Categories.Category.Equivalence +open import Categories.Functor +open import Categories.Monad + +open import Categories.Category.Construction.EilenbergMoore +open import Categories.Category.Construction.Properties.EilenbergMoore + +private + variable + o ℓ e : Level + 𝒞 𝒟 : Category o ℓ e + +-- An adjunction is monadic if the adjunction "comes from" the induced monad in some sense. +record IsMonadicAdjunction {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) : Set (levelOfTerm 𝒞 ⊔ levelOfTerm 𝒟) where + private + T : Monad 𝒞 + T = adjoint⇒monad adjoint + + field + Comparison⁻¹ : Functor (EilenbergMoore T) 𝒟 + comparison-equiv : WeakInverse (ComparisonF adjoint) Comparison⁻¹ From ee163fc3480f217e6ccc47368cf4f5e1b775d2c2 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Fri, 1 Jan 2021 17:04:23 -0800 Subject: [PATCH 02/11] Define Reflexive Pairs --- src/Categories/Diagram/ReflexivePair.agda | 38 +++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 src/Categories/Diagram/ReflexivePair.agda diff --git a/src/Categories/Diagram/ReflexivePair.agda b/src/Categories/Diagram/ReflexivePair.agda new file mode 100644 index 000000000..cf61bf709 --- /dev/null +++ b/src/Categories/Diagram/ReflexivePair.agda @@ -0,0 +1,38 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Core + +-- Reflexive pairs and reflexive coequalizers +-- https://ncatlab.org/nlab/show/reflexive+coequalizer +module Categories.Diagram.ReflexivePair {o ℓ e} (𝒞 : Category o ℓ e) where + +open import Level + +open import Categories.Diagram.Coequalizer 𝒞 + +open Category 𝒞 +open HomReasoning +open Equiv + +private + variable + A B R : Obj + +-- A reflexive pair can be thought of as a vast generalization of a reflexive relation. +-- To see this, consider the case in 'Set' where 'R ⊆ A × A', and 'f' and 'g' are the projections. +-- Then, our morphism 's' would have to look something like the diagonal morphism due to the +-- restriction it is a section of both 'f' and 'g'. +record IsReflexivePair (f g : R ⇒ A) (s : A ⇒ R) : Set e where + field + sectionₗ : f ∘ s ≈ id + sectionᵣ : g ∘ s ≈ id + + section : f ∘ s ≈ g ∘ s + section = sectionₗ ○ ⟺ sectionᵣ + +record ReflexivePair (f g : R ⇒ A) : Set (ℓ ⊔ e) where + field + s : A ⇒ R + isReflexivePair : IsReflexivePair f g s + + open IsReflexivePair isReflexivePair public From 6d8ed610da645de5571bdc670450d990f52ccac2 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Fri, 1 Jan 2021 17:04:37 -0800 Subject: [PATCH 03/11] Add some helper lemmas to Coequalizer --- src/Categories/Diagram/Coequalizer.agda | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/Categories/Diagram/Coequalizer.agda b/src/Categories/Diagram/Coequalizer.agda index 7563b689f..cb63c9339 100644 --- a/src/Categories/Diagram/Coequalizer.agda +++ b/src/Categories/Diagram/Coequalizer.agda @@ -7,11 +7,15 @@ module Categories.Diagram.Coequalizer {o ℓ e} (𝒞 : Category o ℓ e) where open Category 𝒞 open HomReasoning +open import Categories.Morphism.Reasoning 𝒞 + open import Level +open import Function using (_$_) private variable A B C : Obj + f g h i j k : A ⇒ B record Coequalizer (f g : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where field @@ -22,3 +26,21 @@ record Coequalizer (f g : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where coequalize : {h : B ⇒ C} → h ∘ f ≈ h ∘ g → obj ⇒ C universal : {h : B ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ coequalize eq ∘ arr unique : {h : B ⇒ C} {i : obj ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ i ∘ arr → i ≈ coequalize eq + + unique′ : (eq eq′ : h ∘ f ≈ h ∘ g) → coequalize eq ≈ coequalize eq′ + unique′ eq eq′ = unique universal + + coequalize-resp-≈ : ∀ {eq : h ∘ f ≈ h ∘ g} {eq′ : i ∘ f ≈ i ∘ g} → + h ≈ i → coequalize eq ≈ coequalize eq′ + coequalize-resp-≈ {h = h} {i = i} {eq = eq} {eq′ = eq′} h≈i = unique $ begin + i ≈˘⟨ h≈i ⟩ + h ≈⟨ universal ⟩ + coequalize eq ∘ arr ∎ + + coequalize-resp-≈′ : (eq : h ∘ f ≈ h ∘ g) → (eq′ : i ∘ f ≈ i ∘ g) → + h ≈ i → j ≈ coequalize eq → k ≈ coequalize eq′ → j ≈ k + coequalize-resp-≈′ {j = j} {k = k} eq eq′ h≈i eqj eqk = begin + j ≈⟨ eqj ⟩ + coequalize eq ≈⟨ coequalize-resp-≈ h≈i ⟩ + coequalize eq′ ≈˘⟨ eqk ⟩ + k ∎ From dd1d1fa632fe29717548b428207426294e18706f Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Fri, 1 Jan 2021 17:04:56 -0800 Subject: [PATCH 04/11] Prove the first portion of the Crude Monadicity Theorem --- src/Categories/Adjoint/Monadic/Crude.agda | 159 ++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 src/Categories/Adjoint/Monadic/Crude.agda diff --git a/src/Categories/Adjoint/Monadic/Crude.agda b/src/Categories/Adjoint/Monadic/Crude.agda new file mode 100644 index 000000000..0f209a4fc --- /dev/null +++ b/src/Categories/Adjoint/Monadic/Crude.agda @@ -0,0 +1,159 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Adjoint +open import Categories.Category +open import Categories.Functor + +-- The crude monadicity theorem. +module Categories.Adjoint.Monadic.Crude {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′} + {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) where + +open import Level +open import Function using (_$_) + +open import Categories.Adjoint.Properties +open import Categories.Adjoint.Monadic +open import Categories.NaturalTransformation.NaturalIsomorphism +open import Categories.NaturalTransformation +open import Categories.Monad + +open import Categories.Diagram.Coequalizer +open import Categories.Diagram.ReflexivePair + +open import Categories.Category.Construction.EilenbergMoore +open import Categories.Category.Construction.Properties.EilenbergMoore + +open import Categories.Morphism +import Categories.Morphism.Reasoning as MR + +private + module L = Functor L + module R = Functor R + + module 𝒞 = Category 𝒞 + module 𝒟 = Category 𝒟 + + module adjoint = Adjoint adjoint + + T : Monad 𝒞 + T = adjoint⇒monad adjoint + + 𝒞ᵀ : Category _ _ _ + 𝒞ᵀ = EilenbergMoore T + + Comparison : Functor 𝒟 𝒞ᵀ + Comparison = ComparisonF adjoint + + module Comparison = Functor Comparison + + open Coequalizer + +-- If 𝒟 has coequalizers of reflexive pairs, then the comparison functor has a left adjoint. +module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where + + -- The key part of the proof. As we have all reflexive coequalizers, we can create the following coequalizer. + -- We can think of this as identifying the action of the algebra lifted to a "free" structure + -- and the counit of the adjunction, as the unit of the adjunction (also lifted to the "free structure") is a section of both. + coeq : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) + coeq M = has-reflexive-coequalizers record + { s = L.F₁ (adjoint.unit.η (Module.A M)) + ; isReflexivePair = record + { sectionₗ = begin + 𝒟 [ L.F₁ (Module.action M) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈˘⟨ L.homomorphism ⟩ + L.F₁ (𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ) ≈⟨ L.F-resp-≈ (Module.identity M) ⟩ + L.F₁ 𝒞.id ≈⟨ L.identity ⟩ + 𝒟.id ∎ + ; sectionᵣ = begin + 𝒟 [ adjoint.counit.η (L.₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈⟨ adjoint.zig ⟩ + 𝒟.id ∎ + } + } + where + open 𝒟.HomReasoning + + -- If we have coequalizers of reflexive pairs, then we can define an "inverse" to the comparison functor. + Comparison⁻¹ : Functor 𝒞ᵀ 𝒟 + Comparison⁻¹ = record + { F₀ = λ M → obj (coeq M) + ; F₁ = λ {M} {N} α → coequalize (coeq M) $ begin + 𝒟 [ 𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr α) ] ∘ L.F₁ (Module.action M) ] ≈⟨ pullʳ (⟺ L.homomorphism) ⟩ + 𝒟 [ arr (coeq N) ∘ L.F₁ (𝒞 [ Module⇒.arr α ∘ Module.action M ]) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (Module⇒.commute α) ⟩ + 𝒟 [ arr (coeq N) ∘ L.F₁ (𝒞 [ Module.action N ∘ R.F₁ (L.F₁ (Module⇒.arr α)) ]) ] ≈⟨ refl⟩∘⟨ L.homomorphism ⟩ + 𝒟 [ arr (coeq N) ∘ 𝒟 [ L.F₁ (Module.action N) ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ] ≈⟨ pullˡ (equality (coeq N)) ⟩ + 𝒟 [ 𝒟 [ arr (coeq N) ∘ adjoint.counit.η (L.F₀ (Module.A N)) ] ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ≈⟨ extendˡ (adjoint.counit.commute (L.F₁ (Module⇒.arr α))) ⟩ + 𝒟 [ 𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr α) ] ∘ adjoint.counit.η (L.₀ (Module.A M)) ] ∎ + ; identity = λ {A} → ⟺ $ unique (coeq A) $ begin + 𝒟 [ arr (coeq A) ∘ L.F₁ 𝒞.id ] ≈⟨ refl⟩∘⟨ L.identity ⟩ + 𝒟 [ arr (coeq A) ∘ 𝒟.id ] ≈⟨ id-comm ⟩ + 𝒟 [ 𝒟.id ∘ arr (coeq A) ] ∎ + ; homomorphism = λ {X} {Y} {Z} {f} {g} → ⟺ $ unique (coeq X) $ begin + 𝒟 [ arr (coeq Z) ∘ L.F₁ (𝒞 [ Module⇒.arr g ∘ Module⇒.arr f ]) ] ≈⟨ 𝒟.∘-resp-≈ʳ L.homomorphism ○ 𝒟.sym-assoc ⟩ + 𝒟 [ 𝒟 [ arr (coeq Z) ∘ L.F₁ (Module⇒.arr g) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (coeq Y) ⟩∘⟨refl ⟩ + 𝒟 [ 𝒟 [ coequalize (coeq Y) _ ∘ arr (coeq Y) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ extendˡ (universal (coeq X)) ⟩ + 𝒟 [ 𝒟 [ coequalize (coeq Y) _ ∘ coequalize (coeq X) _ ] ∘ arr (coeq X) ] ∎ + ; F-resp-≈ = λ {A} {B} {f} {g} eq → unique (coeq A) $ begin + 𝒟 [ arr (coeq B) ∘ L.F₁ (Module⇒.arr g) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (𝒞.Equiv.sym eq) ⟩ + 𝒟 [ arr (coeq B) ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (coeq A) ⟩ + 𝒟 [ coequalize (coeq A) _ ∘ arr (coeq A) ] ∎ + } + where + open 𝒟.HomReasoning + open MR 𝒟 + + module Comparison⁻¹ = Functor Comparison⁻¹ + + -- If 𝒟 has reflexive coequalizers, then the "inverse" to the comparison functor is actually adjoint. + Comparison⁻¹⊣Comparison : Comparison⁻¹ ⊣ Comparison + Adjoint.unit Comparison⁻¹⊣Comparison = ntHelper record + { η = λ M → record + { arr = 𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M) ] + ; commute = begin + 𝒞 [ 𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ] ≈⟨ pullʳ (adjoint.unit.commute (Module.action M)) ⟩ + -- It would be nice to have a reasoning combinator doing this "⟺ homomorphism ... homomorphism" pattern + 𝒞 [ R.F₁ (arr (coeq M)) ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩ + 𝒞 [ R.F₁ (𝒟 [ arr (coeq M) ∘ L.F₁ (Module.action M) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.F-resp-≈ (equality (coeq M)) ⟩∘⟨refl) ⟩ + 𝒞 [ R.F₁ (𝒟 [ arr (coeq M) ∘ adjoint.counit.η (L.F₀ (Module.A M)) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.homomorphism ⟩∘⟨refl) ⟩ + 𝒞 [ 𝒞 [ R.F₁ (arr (coeq M)) ∘ R.F₁ (adjoint.counit.η (L.F₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ cancelʳ adjoint.zag ⟩ + -- FIXME Use something like cancel here + R.F₁ (arr (coeq M)) ≈˘⟨ R.F-resp-≈ (𝒟.identityʳ) ⟩ + R.F₁ (𝒟 [ arr (coeq M) ∘ 𝒟.id ]) ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ adjoint.zig) ⟩ + R.F₁ (𝒟 [ arr (coeq M) ∘ 𝒟 [ adjoint.counit.η (L.F₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ]) ≈⟨ R.F-resp-≈ (MR.extendʳ 𝒟 (adjoint.counit.sym-commute (arr (coeq M)))) ⟩ + R.F₁ (𝒟 [ adjoint.counit.η (obj (coeq M)) ∘ 𝒟 [ L.F₁ (R.F₁ (arr (coeq M))) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ]) ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ L.homomorphism) ⟩ + R.F₁ (𝒟 [ adjoint.counit.η (obj (coeq M)) ∘ L.F₁ (𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M)])]) ≈⟨ R.homomorphism ⟩ + 𝒞 [ R.F₁ (adjoint.counit.η (obj (coeq M))) ∘ R.F₁ (L.F₁ (𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M)])) ] ∎ + } + ; commute = λ {M} {N} f → begin + 𝒞 [ 𝒞 [ R.F₁ (arr (coeq N)) ∘ adjoint.unit.η (Module.A N) ] ∘ Module⇒.arr f ] ≈⟨ extendˡ (adjoint.unit.commute (Module⇒.arr f)) ⟩ + 𝒞 [ 𝒞 [ R.F₁ (arr (coeq N)) ∘ R.F₁ (L.F₁ (Module⇒.arr f)) ] ∘ adjoint.unit.η (Module.A M) ] ≈˘⟨ R.homomorphism ⟩∘⟨refl ⟩ + 𝒞 [ R.F₁ (𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr f) ]) ∘ adjoint.unit.η (Module.A M) ] ≈⟨ R.F-resp-≈ (universal (coeq M)) ⟩∘⟨refl ⟩ + 𝒞 [ R.F₁ (𝒟 [ (coequalize (coeq M) _) ∘ (arr (coeq M)) ]) ∘ adjoint.unit.η (Module.A M) ] ≈⟨ pushˡ R.homomorphism ⟩ + 𝒞 [ R.F₁ (coequalize (coeq M) _) ∘ 𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M) ] ] ∎ + } + where + open 𝒞.HomReasoning + open MR 𝒞 + Adjoint.counit Comparison⁻¹⊣Comparison = ntHelper record + { η = λ X → coequalize (coeq (Comparison.F₀ X)) (adjoint.counit.commute (adjoint.counit.η X)) + ; commute = λ {X} {Y} f → begin + 𝒟 [ coequalize (coeq (Comparison.F₀ Y)) _ ∘ coequalize (coeq (Comparison.F₀ X)) _ ] ≈⟨ unique (coeq (Comparison.F₀ X)) (adjoint.counit.sym-commute f ○ pushˡ (universal (coeq (Comparison.F₀ Y))) ○ pushʳ (universal (coeq (Comparison.F₀ X)))) ⟩ + coequalize (coeq (Comparison.F₀ X)) (extendˡ (adjoint.counit.commute (adjoint.counit.η X))) ≈˘⟨ unique (coeq (Comparison.F₀ X)) (pushʳ (universal (coeq (Comparison.F₀ X)))) ⟩ + 𝒟 [ f ∘ coequalize (coeq (Comparison.F₀ X)) _ ] ∎ + } + where + open 𝒟.HomReasoning + open MR 𝒟 + Adjoint.zig Comparison⁻¹⊣Comparison {X} = begin + 𝒟 [ coequalize (coeq (Comparison.F₀ (Comparison⁻¹.F₀ X))) _ ∘ coequalize (coeq X) _ ] ≈⟨ unique (coeq X) (⟺ adjoint.RLadjunct≈id ○ pushˡ (universal (coeq (Comparison.F₀ (Comparison⁻¹.F₀ X)))) ○ pushʳ (universal (coeq X))) ⟩ + coequalize (coeq X) {h = arr (coeq X)} (equality (coeq X)) ≈˘⟨ unique (coeq X) (⟺ 𝒟.identityˡ) ⟩ + 𝒟.id ∎ + where + open 𝒟.HomReasoning + open MR 𝒟 + Adjoint.zag Comparison⁻¹⊣Comparison {A} = begin + 𝒞 [ R.F₁ (coequalize (coeq (Comparison.F₀ A)) _) ∘ 𝒞 [ R.F₁ (arr (coeq (Comparison.F₀ A))) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩ + 𝒞 [ R.F₁ (𝒟 [ coequalize (coeq (Comparison.F₀ A)) _ ∘ arr (coeq (Comparison.F₀ A)) ]) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ≈˘⟨ R.F-resp-≈ (universal (coeq (Comparison.F₀ A))) ⟩∘⟨refl ⟩ + 𝒞 [ R.F₁ (adjoint.counit.η A) ∘ adjoint.unit.η (R.F₀ A) ] ≈⟨ adjoint.zag ⟩ + 𝒞.id ∎ + where + open 𝒞.HomReasoning + open MR 𝒞 From cce4eae9fdfa6c3280247811c8953d95de6748ca Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Fri, 1 Jan 2021 17:05:33 -0800 Subject: [PATCH 05/11] Define Conservative Functors --- src/Categories/Functor/Properties.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Categories/Functor/Properties.agda b/src/Categories/Functor/Properties.agda index 34c0754d6..8eaf396b4 100644 --- a/src/Categories/Functor/Properties.agda +++ b/src/Categories/Functor/Properties.agda @@ -49,6 +49,12 @@ EssentiallySurjective {C = C} {D = D} F = (d : Category.Obj D) → Σ C.Obj (λ open Morphism D module C = Category C +Conservative : Functor C D → Set _ +Conservative {C = C} {D = D} F = ∀ {A B} → (f : C [ A , B ]) → (g : C [ B , A ]) → Iso D (F₁ f) (F₁ g) → Iso C f g + where + open Functor F + open Morphism + -- a series of [ Functor ]-respects-Thing combinators (with respects -> resp) module _ (F : Functor C D) where From 204685cf5b4e6f326f2603672776308f8a5208fc Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Fri, 1 Jan 2021 18:07:13 -0800 Subject: [PATCH 06/11] Pull out the proof that the comparison functor has an adjoint Luckily, I think we can reuse a huge chunk of this proof for Beck's monadicity theorem. --- src/Categories/Adjoint/Monadic/Crude.agda | 137 ++++++----------- .../Adjoint/Monadic/Properties.agda | 139 ++++++++++++++++++ 2 files changed, 186 insertions(+), 90 deletions(-) create mode 100644 src/Categories/Adjoint/Monadic/Properties.agda diff --git a/src/Categories/Adjoint/Monadic/Crude.agda b/src/Categories/Adjoint/Monadic/Crude.agda index 0f209a4fc..941a4278e 100644 --- a/src/Categories/Adjoint/Monadic/Crude.agda +++ b/src/Categories/Adjoint/Monadic/Crude.agda @@ -2,9 +2,10 @@ open import Categories.Adjoint open import Categories.Category -open import Categories.Functor +open import Categories.Functor renaming (id to idF) --- The crude monadicity theorem. +-- The crude monadicity theorem. This proof is based off of the version +-- provided in "Sheaves In Geometry and Logic" by Maclane and Moerdijk. module Categories.Adjoint.Monadic.Crude {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′} {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) where @@ -13,6 +14,7 @@ open import Function using (_$_) open import Categories.Adjoint.Properties open import Categories.Adjoint.Monadic +open import Categories.Adjoint.Monadic.Properties open import Categories.NaturalTransformation.NaturalIsomorphism open import Categories.NaturalTransformation open import Categories.Monad @@ -48,14 +50,17 @@ private open Coequalizer +-- TODO: I think a _lot_ of this can be factored out into a helper lemma: +-- + -- If 𝒟 has coequalizers of reflexive pairs, then the comparison functor has a left adjoint. module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where -- The key part of the proof. As we have all reflexive coequalizers, we can create the following coequalizer. -- We can think of this as identifying the action of the algebra lifted to a "free" structure -- and the counit of the adjunction, as the unit of the adjunction (also lifted to the "free structure") is a section of both. - coeq : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) - coeq M = has-reflexive-coequalizers record + has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) + has-coequalizer M = has-reflexive-coequalizers record { s = L.F₁ (adjoint.unit.η (Module.A M)) ; isReflexivePair = record { sectionₗ = begin @@ -71,89 +76,41 @@ module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → Refl where open 𝒟.HomReasoning - -- If we have coequalizers of reflexive pairs, then we can define an "inverse" to the comparison functor. - Comparison⁻¹ : Functor 𝒞ᵀ 𝒟 - Comparison⁻¹ = record - { F₀ = λ M → obj (coeq M) - ; F₁ = λ {M} {N} α → coequalize (coeq M) $ begin - 𝒟 [ 𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr α) ] ∘ L.F₁ (Module.action M) ] ≈⟨ pullʳ (⟺ L.homomorphism) ⟩ - 𝒟 [ arr (coeq N) ∘ L.F₁ (𝒞 [ Module⇒.arr α ∘ Module.action M ]) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (Module⇒.commute α) ⟩ - 𝒟 [ arr (coeq N) ∘ L.F₁ (𝒞 [ Module.action N ∘ R.F₁ (L.F₁ (Module⇒.arr α)) ]) ] ≈⟨ refl⟩∘⟨ L.homomorphism ⟩ - 𝒟 [ arr (coeq N) ∘ 𝒟 [ L.F₁ (Module.action N) ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ] ≈⟨ pullˡ (equality (coeq N)) ⟩ - 𝒟 [ 𝒟 [ arr (coeq N) ∘ adjoint.counit.η (L.F₀ (Module.A N)) ] ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ≈⟨ extendˡ (adjoint.counit.commute (L.F₁ (Module⇒.arr α))) ⟩ - 𝒟 [ 𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr α) ] ∘ adjoint.counit.η (L.₀ (Module.A M)) ] ∎ - ; identity = λ {A} → ⟺ $ unique (coeq A) $ begin - 𝒟 [ arr (coeq A) ∘ L.F₁ 𝒞.id ] ≈⟨ refl⟩∘⟨ L.identity ⟩ - 𝒟 [ arr (coeq A) ∘ 𝒟.id ] ≈⟨ id-comm ⟩ - 𝒟 [ 𝒟.id ∘ arr (coeq A) ] ∎ - ; homomorphism = λ {X} {Y} {Z} {f} {g} → ⟺ $ unique (coeq X) $ begin - 𝒟 [ arr (coeq Z) ∘ L.F₁ (𝒞 [ Module⇒.arr g ∘ Module⇒.arr f ]) ] ≈⟨ 𝒟.∘-resp-≈ʳ L.homomorphism ○ 𝒟.sym-assoc ⟩ - 𝒟 [ 𝒟 [ arr (coeq Z) ∘ L.F₁ (Module⇒.arr g) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (coeq Y) ⟩∘⟨refl ⟩ - 𝒟 [ 𝒟 [ coequalize (coeq Y) _ ∘ arr (coeq Y) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ extendˡ (universal (coeq X)) ⟩ - 𝒟 [ 𝒟 [ coequalize (coeq Y) _ ∘ coequalize (coeq X) _ ] ∘ arr (coeq X) ] ∎ - ; F-resp-≈ = λ {A} {B} {f} {g} eq → unique (coeq A) $ begin - 𝒟 [ arr (coeq B) ∘ L.F₁ (Module⇒.arr g) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (𝒞.Equiv.sym eq) ⟩ - 𝒟 [ arr (coeq B) ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (coeq A) ⟩ - 𝒟 [ coequalize (coeq A) _ ∘ arr (coeq A) ] ∎ - } - where - open 𝒟.HomReasoning - open MR 𝒟 - - module Comparison⁻¹ = Functor Comparison⁻¹ - - -- If 𝒟 has reflexive coequalizers, then the "inverse" to the comparison functor is actually adjoint. - Comparison⁻¹⊣Comparison : Comparison⁻¹ ⊣ Comparison - Adjoint.unit Comparison⁻¹⊣Comparison = ntHelper record - { η = λ M → record - { arr = 𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M) ] - ; commute = begin - 𝒞 [ 𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ] ≈⟨ pullʳ (adjoint.unit.commute (Module.action M)) ⟩ - -- It would be nice to have a reasoning combinator doing this "⟺ homomorphism ... homomorphism" pattern - 𝒞 [ R.F₁ (arr (coeq M)) ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩ - 𝒞 [ R.F₁ (𝒟 [ arr (coeq M) ∘ L.F₁ (Module.action M) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.F-resp-≈ (equality (coeq M)) ⟩∘⟨refl) ⟩ - 𝒞 [ R.F₁ (𝒟 [ arr (coeq M) ∘ adjoint.counit.η (L.F₀ (Module.A M)) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.homomorphism ⟩∘⟨refl) ⟩ - 𝒞 [ 𝒞 [ R.F₁ (arr (coeq M)) ∘ R.F₁ (adjoint.counit.η (L.F₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ cancelʳ adjoint.zag ⟩ - -- FIXME Use something like cancel here - R.F₁ (arr (coeq M)) ≈˘⟨ R.F-resp-≈ (𝒟.identityʳ) ⟩ - R.F₁ (𝒟 [ arr (coeq M) ∘ 𝒟.id ]) ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ adjoint.zig) ⟩ - R.F₁ (𝒟 [ arr (coeq M) ∘ 𝒟 [ adjoint.counit.η (L.F₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ]) ≈⟨ R.F-resp-≈ (MR.extendʳ 𝒟 (adjoint.counit.sym-commute (arr (coeq M)))) ⟩ - R.F₁ (𝒟 [ adjoint.counit.η (obj (coeq M)) ∘ 𝒟 [ L.F₁ (R.F₁ (arr (coeq M))) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ]) ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ L.homomorphism) ⟩ - R.F₁ (𝒟 [ adjoint.counit.η (obj (coeq M)) ∘ L.F₁ (𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M)])]) ≈⟨ R.homomorphism ⟩ - 𝒞 [ R.F₁ (adjoint.counit.η (obj (coeq M))) ∘ R.F₁ (L.F₁ (𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M)])) ] ∎ - } - ; commute = λ {M} {N} f → begin - 𝒞 [ 𝒞 [ R.F₁ (arr (coeq N)) ∘ adjoint.unit.η (Module.A N) ] ∘ Module⇒.arr f ] ≈⟨ extendˡ (adjoint.unit.commute (Module⇒.arr f)) ⟩ - 𝒞 [ 𝒞 [ R.F₁ (arr (coeq N)) ∘ R.F₁ (L.F₁ (Module⇒.arr f)) ] ∘ adjoint.unit.η (Module.A M) ] ≈˘⟨ R.homomorphism ⟩∘⟨refl ⟩ - 𝒞 [ R.F₁ (𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr f) ]) ∘ adjoint.unit.η (Module.A M) ] ≈⟨ R.F-resp-≈ (universal (coeq M)) ⟩∘⟨refl ⟩ - 𝒞 [ R.F₁ (𝒟 [ (coequalize (coeq M) _) ∘ (arr (coeq M)) ]) ∘ adjoint.unit.η (Module.A M) ] ≈⟨ pushˡ R.homomorphism ⟩ - 𝒞 [ R.F₁ (coequalize (coeq M) _) ∘ 𝒞 [ R.F₁ (arr (coeq M)) ∘ adjoint.unit.η (Module.A M) ] ] ∎ - } - where - open 𝒞.HomReasoning - open MR 𝒞 - Adjoint.counit Comparison⁻¹⊣Comparison = ntHelper record - { η = λ X → coequalize (coeq (Comparison.F₀ X)) (adjoint.counit.commute (adjoint.counit.η X)) - ; commute = λ {X} {Y} f → begin - 𝒟 [ coequalize (coeq (Comparison.F₀ Y)) _ ∘ coequalize (coeq (Comparison.F₀ X)) _ ] ≈⟨ unique (coeq (Comparison.F₀ X)) (adjoint.counit.sym-commute f ○ pushˡ (universal (coeq (Comparison.F₀ Y))) ○ pushʳ (universal (coeq (Comparison.F₀ X)))) ⟩ - coequalize (coeq (Comparison.F₀ X)) (extendˡ (adjoint.counit.commute (adjoint.counit.η X))) ≈˘⟨ unique (coeq (Comparison.F₀ X)) (pushʳ (universal (coeq (Comparison.F₀ X)))) ⟩ - 𝒟 [ f ∘ coequalize (coeq (Comparison.F₀ X)) _ ] ∎ - } - where - open 𝒟.HomReasoning - open MR 𝒟 - Adjoint.zig Comparison⁻¹⊣Comparison {X} = begin - 𝒟 [ coequalize (coeq (Comparison.F₀ (Comparison⁻¹.F₀ X))) _ ∘ coequalize (coeq X) _ ] ≈⟨ unique (coeq X) (⟺ adjoint.RLadjunct≈id ○ pushˡ (universal (coeq (Comparison.F₀ (Comparison⁻¹.F₀ X)))) ○ pushʳ (universal (coeq X))) ⟩ - coequalize (coeq X) {h = arr (coeq X)} (equality (coeq X)) ≈˘⟨ unique (coeq X) (⟺ 𝒟.identityˡ) ⟩ - 𝒟.id ∎ - where - open 𝒟.HomReasoning - open MR 𝒟 - Adjoint.zag Comparison⁻¹⊣Comparison {A} = begin - 𝒞 [ R.F₁ (coequalize (coeq (Comparison.F₀ A)) _) ∘ 𝒞 [ R.F₁ (arr (coeq (Comparison.F₀ A))) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩ - 𝒞 [ R.F₁ (𝒟 [ coequalize (coeq (Comparison.F₀ A)) _ ∘ arr (coeq (Comparison.F₀ A)) ]) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ≈˘⟨ R.F-resp-≈ (universal (coeq (Comparison.F₀ A))) ⟩∘⟨refl ⟩ - 𝒞 [ R.F₁ (adjoint.counit.η A) ∘ adjoint.unit.η (R.F₀ A) ] ≈⟨ adjoint.zag ⟩ - 𝒞.id ∎ - where - open 𝒞.HomReasoning - open MR 𝒞 + -- -- If we have coequalizers of reflexive pairs, then we can define an "inverse" to the comparison functor. + -- Comparison⁻¹ : Functor 𝒞ᵀ 𝒟 + -- Comparison⁻¹ = record + -- { F₀ = λ M → obj (coeq M) + -- ; F₁ = λ {M} {N} α → coequalize (coeq M) $ begin + -- 𝒟 [ 𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr α) ] ∘ L.F₁ (Module.action M) ] ≈⟨ pullʳ (⟺ L.homomorphism) ⟩ + -- 𝒟 [ arr (coeq N) ∘ L.F₁ (𝒞 [ Module⇒.arr α ∘ Module.action M ]) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (Module⇒.commute α) ⟩ + -- 𝒟 [ arr (coeq N) ∘ L.F₁ (𝒞 [ Module.action N ∘ R.F₁ (L.F₁ (Module⇒.arr α)) ]) ] ≈⟨ refl⟩∘⟨ L.homomorphism ⟩ + -- 𝒟 [ arr (coeq N) ∘ 𝒟 [ L.F₁ (Module.action N) ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ] ≈⟨ pullˡ (equality (coeq N)) ⟩ + -- 𝒟 [ 𝒟 [ arr (coeq N) ∘ adjoint.counit.η (L.F₀ (Module.A N)) ] ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ≈⟨ extendˡ (adjoint.counit.commute (L.F₁ (Module⇒.arr α))) ⟩ + -- 𝒟 [ 𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr α) ] ∘ adjoint.counit.η (L.₀ (Module.A M)) ] ∎ + -- ; identity = λ {A} → ⟺ $ unique (coeq A) $ begin + -- 𝒟 [ arr (coeq A) ∘ L.F₁ 𝒞.id ] ≈⟨ refl⟩∘⟨ L.identity ⟩ + -- 𝒟 [ arr (coeq A) ∘ 𝒟.id ] ≈⟨ id-comm ⟩ + -- 𝒟 [ 𝒟.id ∘ arr (coeq A) ] ∎ + -- ; homomorphism = λ {X} {Y} {Z} {f} {g} → ⟺ $ unique (coeq X) $ begin + -- 𝒟 [ arr (coeq Z) ∘ L.F₁ (𝒞 [ Module⇒.arr g ∘ Module⇒.arr f ]) ] ≈⟨ 𝒟.∘-resp-≈ʳ L.homomorphism ○ 𝒟.sym-assoc ⟩ + -- 𝒟 [ 𝒟 [ arr (coeq Z) ∘ L.F₁ (Module⇒.arr g) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (coeq Y) ⟩∘⟨refl ⟩ + -- 𝒟 [ 𝒟 [ coequalize (coeq Y) _ ∘ arr (coeq Y) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ extendˡ (universal (coeq X)) ⟩ + -- 𝒟 [ 𝒟 [ coequalize (coeq Y) _ ∘ coequalize (coeq X) _ ] ∘ arr (coeq X) ] ∎ + -- ; F-resp-≈ = λ {A} {B} {f} {g} eq → unique (coeq A) $ begin + -- 𝒟 [ arr (coeq B) ∘ L.F₁ (Module⇒.arr g) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (𝒞.Equiv.sym eq) ⟩ + -- 𝒟 [ arr (coeq B) ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (coeq A) ⟩ + -- 𝒟 [ coequalize (coeq A) _ ∘ arr (coeq A) ] ∎ + -- } + -- where + -- open 𝒟.HomReasoning + -- open MR 𝒟 + + -- module Comparison⁻¹ = Functor Comparison⁻¹ + + + + + +-- -- If 𝒟 has coequalizers of reflexive pairs _and_ R preserves these coequalizers, then the unit of the adjunction +-- -- from the previous section is an +-- module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where diff --git a/src/Categories/Adjoint/Monadic/Properties.agda b/src/Categories/Adjoint/Monadic/Properties.agda new file mode 100644 index 000000000..aa3107e65 --- /dev/null +++ b/src/Categories/Adjoint/Monadic/Properties.agda @@ -0,0 +1,139 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Adjoint +open import Categories.Category +open import Categories.Functor renaming (id to idF) + +module Categories.Adjoint.Monadic.Properties {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′} + {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) where + + +open import Level +open import Function using (_$_) + +open import Categories.Adjoint.Properties +open import Categories.Adjoint.Monadic +open import Categories.NaturalTransformation.NaturalIsomorphism +open import Categories.NaturalTransformation +open import Categories.Monad + +open import Categories.Diagram.Coequalizer + +open import Categories.Category.Construction.EilenbergMoore +open import Categories.Category.Construction.Properties.EilenbergMoore + +open import Categories.Morphism +import Categories.Morphism.Reasoning as MR + +private + module L = Functor L + module R = Functor R + + module 𝒞 = Category 𝒞 + module 𝒟 = Category 𝒟 + + module adjoint = Adjoint adjoint + + T : Monad 𝒞 + T = adjoint⇒monad adjoint + + 𝒞ᵀ : Category _ _ _ + 𝒞ᵀ = EilenbergMoore T + + Comparison : Functor 𝒟 𝒞ᵀ + Comparison = ComparisonF adjoint + + module Comparison = Functor Comparison + + +-- If we have a coequalizer of the following diagram, then the comparison functor has a left adjoint. +module _ (has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))) where + + open Coequalizer + + Comparison⁻¹ : Functor 𝒞ᵀ 𝒟 + Comparison⁻¹ = record + { F₀ = λ M → obj (has-coequalizer M) + ; F₁ = λ {M} {N} α → coequalize (has-coequalizer M) $ begin + 𝒟 [ 𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr α) ] ∘ L.F₁ (Module.action M) ] ≈⟨ pullʳ (⟺ L.homomorphism) ⟩ + 𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (𝒞 [ Module⇒.arr α ∘ Module.action M ]) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (Module⇒.commute α) ⟩ + 𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (𝒞 [ Module.action N ∘ R.F₁ (L.F₁ (Module⇒.arr α)) ]) ] ≈⟨ refl⟩∘⟨ L.homomorphism ⟩ + 𝒟 [ arr (has-coequalizer N) ∘ 𝒟 [ L.F₁ (Module.action N) ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ] ≈⟨ pullˡ (equality (has-coequalizer N)) ⟩ + 𝒟 [ 𝒟 [ arr (has-coequalizer N) ∘ adjoint.counit.η (L.F₀ (Module.A N)) ] ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ≈⟨ extendˡ (adjoint.counit.commute (L.F₁ (Module⇒.arr α))) ⟩ + 𝒟 [ 𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr α) ] ∘ adjoint.counit.η (L.₀ (Module.A M)) ] ∎ + ; identity = λ {A} → ⟺ $ unique (has-coequalizer A) $ begin + 𝒟 [ arr (has-coequalizer A) ∘ L.F₁ 𝒞.id ] ≈⟨ refl⟩∘⟨ L.identity ⟩ + 𝒟 [ arr (has-coequalizer A) ∘ 𝒟.id ] ≈⟨ id-comm ⟩ + 𝒟 [ 𝒟.id ∘ arr (has-coequalizer A) ] ∎ + ; homomorphism = λ {X} {Y} {Z} {f} {g} → ⟺ $ unique (has-coequalizer X) $ begin + 𝒟 [ arr (has-coequalizer Z) ∘ L.F₁ (𝒞 [ Module⇒.arr g ∘ Module⇒.arr f ]) ] ≈⟨ 𝒟.∘-resp-≈ʳ L.homomorphism ○ 𝒟.sym-assoc ⟩ + 𝒟 [ 𝒟 [ arr (has-coequalizer Z) ∘ L.F₁ (Module⇒.arr g) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (has-coequalizer Y) ⟩∘⟨refl ⟩ + 𝒟 [ 𝒟 [ coequalize (has-coequalizer Y) _ ∘ arr (has-coequalizer Y) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ extendˡ (universal (has-coequalizer X)) ⟩ + 𝒟 [ 𝒟 [ coequalize (has-coequalizer Y) _ ∘ coequalize (has-coequalizer X) _ ] ∘ arr (has-coequalizer X) ] ∎ + ; F-resp-≈ = λ {A} {B} {f} {g} eq → unique (has-coequalizer A) $ begin + 𝒟 [ arr (has-coequalizer B) ∘ L.F₁ (Module⇒.arr g) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (𝒞.Equiv.sym eq) ⟩ + 𝒟 [ arr (has-coequalizer B) ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (has-coequalizer A) ⟩ + 𝒟 [ coequalize (has-coequalizer A) _ ∘ arr (has-coequalizer A) ] ∎ + } + where + open 𝒟.HomReasoning + open MR 𝒟 + + module Comparison⁻¹ = Functor Comparison⁻¹ + + Comparison⁻¹⊣Comparison : Comparison⁻¹ ⊣ Comparison + Adjoint.unit Comparison⁻¹⊣Comparison = ntHelper record + { η = λ M → record + { arr = 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] + ; commute = begin + 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ] ≈⟨ pullʳ (adjoint.unit.commute (Module.action M)) ⟩ + -- It would be nice to have a reasoning combinator doing this "⟺ homomorphism ... homomorphism" pattern + 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩ + 𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ L.F₁ (Module.action M) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.F-resp-≈ (equality (has-coequalizer M)) ⟩∘⟨refl) ⟩ + 𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ adjoint.counit.η (L.F₀ (Module.A M)) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.homomorphism ⟩∘⟨refl) ⟩ + 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ R.F₁ (adjoint.counit.η (L.F₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ cancelʳ adjoint.zag ⟩ + -- FIXME Use something like cancel here + R.F₁ (arr (has-coequalizer M)) ≈˘⟨ R.F-resp-≈ (𝒟.identityʳ) ⟩ + R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟.id ]) ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ adjoint.zig) ⟩ + R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟 [ adjoint.counit.η (L.F₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ]) ≈⟨ R.F-resp-≈ (MR.extendʳ 𝒟 (adjoint.counit.sym-commute (arr (has-coequalizer M)))) ⟩ + R.F₁ (𝒟 [ adjoint.counit.η (obj (has-coequalizer M)) ∘ 𝒟 [ L.F₁ (R.F₁ (arr (has-coequalizer M))) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ]) ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ L.homomorphism) ⟩ + R.F₁ (𝒟 [ adjoint.counit.η (obj (has-coequalizer M)) ∘ L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M)])]) ≈⟨ R.homomorphism ⟩ + 𝒞 [ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ∘ R.F₁ (L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M)])) ] ∎ + } + ; commute = λ {M} {N} f → begin + 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ adjoint.unit.η (Module.A N) ] ∘ Module⇒.arr f ] ≈⟨ extendˡ (adjoint.unit.commute (Module⇒.arr f)) ⟩ + 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ R.F₁ (L.F₁ (Module⇒.arr f)) ] ∘ adjoint.unit.η (Module.A M) ] ≈˘⟨ R.homomorphism ⟩∘⟨refl ⟩ + 𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr f) ]) ∘ adjoint.unit.η (Module.A M) ] ≈⟨ R.F-resp-≈ (universal (has-coequalizer M)) ⟩∘⟨refl ⟩ + 𝒞 [ R.F₁ (𝒟 [ (coequalize (has-coequalizer M) _) ∘ (arr (has-coequalizer M)) ]) ∘ adjoint.unit.η (Module.A M) ] ≈⟨ pushˡ R.homomorphism ⟩ + 𝒞 [ R.F₁ (coequalize (has-coequalizer M) _) ∘ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ] ∎ + } + where + open 𝒞.HomReasoning + open MR 𝒞 + Adjoint.counit Comparison⁻¹⊣Comparison = ntHelper record + { η = λ X → coequalize (has-coequalizer (Comparison.F₀ X)) (adjoint.counit.commute (adjoint.counit.η X)) + ; commute = λ {X} {Y} f → begin + 𝒟 [ coequalize (has-coequalizer (Comparison.F₀ Y)) _ ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ] ≈⟨ unique (has-coequalizer (Comparison.F₀ X)) (adjoint.counit.sym-commute f ○ pushˡ (universal (has-coequalizer (Comparison.F₀ Y))) ○ pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩ + coequalize (has-coequalizer (Comparison.F₀ X)) (extendˡ (adjoint.counit.commute (adjoint.counit.η X))) ≈˘⟨ unique (has-coequalizer (Comparison.F₀ X)) (pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩ + 𝒟 [ f ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ] ∎ + } + where + open 𝒟.HomReasoning + open MR 𝒟 + Adjoint.zig Comparison⁻¹⊣Comparison {X} = begin + 𝒟 [ coequalize (has-coequalizer (Comparison.F₀ (Comparison⁻¹.F₀ X))) _ ∘ coequalize (has-coequalizer X) _ ] ≈⟨ unique (has-coequalizer X) (⟺ adjoint.RLadjunct≈id ○ pushˡ (universal (has-coequalizer (Comparison.F₀ (Comparison⁻¹.F₀ X)))) ○ pushʳ (universal (has-coequalizer X))) ⟩ + coequalize (has-coequalizer X) {h = arr (has-coequalizer X)} (equality (has-coequalizer X)) ≈˘⟨ unique (has-coequalizer X) (⟺ 𝒟.identityˡ) ⟩ + 𝒟.id ∎ + where + open 𝒟.HomReasoning + open MR 𝒟 + Adjoint.zag Comparison⁻¹⊣Comparison {A} = begin + 𝒞 [ R.F₁ (coequalize (has-coequalizer (Comparison.F₀ A)) _) ∘ 𝒞 [ R.F₁ (arr (has-coequalizer (Comparison.F₀ A))) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩ + 𝒞 [ R.F₁ (𝒟 [ coequalize (has-coequalizer (Comparison.F₀ A)) _ ∘ arr (has-coequalizer (Comparison.F₀ A)) ]) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ≈˘⟨ R.F-resp-≈ (universal (has-coequalizer (Comparison.F₀ A))) ⟩∘⟨refl ⟩ + 𝒞 [ R.F₁ (adjoint.counit.η A) ∘ adjoint.unit.η (R.F₀ A) ] ≈⟨ adjoint.zag ⟩ + 𝒞.id ∎ + where + open 𝒞.HomReasoning + open MR 𝒞 + + module Comparison⁻¹⊣Comparison = Adjoint Comparison⁻¹⊣Comparison From d21f1efb5b158ff5d74d7fc30080852d227b3f02 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Sat, 2 Jan 2021 20:01:00 -0800 Subject: [PATCH 07/11] Split up coequalizer into bundled and predicate form --- src/Categories/Diagram/Coequalizer.agda | 53 +++++++++++++++++++++---- src/Categories/Diagram/Duality.agda | 10 +++-- 2 files changed, 52 insertions(+), 11 deletions(-) diff --git a/src/Categories/Diagram/Coequalizer.agda b/src/Categories/Diagram/Coequalizer.agda index cb63c9339..fbef15478 100644 --- a/src/Categories/Diagram/Coequalizer.agda +++ b/src/Categories/Diagram/Coequalizer.agda @@ -7,6 +7,7 @@ module Categories.Diagram.Coequalizer {o ℓ e} (𝒞 : Category o ℓ e) where open Category 𝒞 open HomReasoning +open import Categories.Morphism 𝒞 open import Categories.Morphism.Reasoning 𝒞 open import Level @@ -15,21 +16,21 @@ open import Function using (_$_) private variable A B C : Obj - f g h i j k : A ⇒ B + h i j k : A ⇒ B -record Coequalizer (f g : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where +record IsCoequalizer {E} (f g : A ⇒ B) (arr : B ⇒ E) : Set (o ⊔ ℓ ⊔ e) where field - {obj} : Obj - arr : B ⇒ obj - equality : arr ∘ f ≈ arr ∘ g - coequalize : {h : B ⇒ C} → h ∘ f ≈ h ∘ g → obj ⇒ C + coequalize : {h : B ⇒ C} → h ∘ f ≈ h ∘ g → E ⇒ C universal : {h : B ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ coequalize eq ∘ arr - unique : {h : B ⇒ C} {i : obj ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ i ∘ arr → i ≈ coequalize eq + unique : {h : B ⇒ C} {i : E ⇒ C} {eq : h ∘ f ≈ h ∘ g} → h ≈ i ∘ arr → i ≈ coequalize eq unique′ : (eq eq′ : h ∘ f ≈ h ∘ g) → coequalize eq ≈ coequalize eq′ unique′ eq eq′ = unique universal + id-coequalize : id ≈ coequalize equality + id-coequalize = unique (⟺ identityˡ) + coequalize-resp-≈ : ∀ {eq : h ∘ f ≈ h ∘ g} {eq′ : i ∘ f ≈ i ∘ g} → h ≈ i → coequalize eq ≈ coequalize eq′ coequalize-resp-≈ {h = h} {i = i} {eq = eq} {eq′ = eq′} h≈i = unique $ begin @@ -44,3 +45,41 @@ record Coequalizer (f g : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where coequalize eq ≈⟨ coequalize-resp-≈ h≈i ⟩ coequalize eq′ ≈˘⟨ eqk ⟩ k ∎ + +record Coequalizer (f g : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where + field + {obj} : Obj + arr : B ⇒ obj + isCoequalizer : IsCoequalizer f g arr + + open IsCoequalizer isCoequalizer public + + +-- Proving this via duality arguments is kind of annoying, as ≅ does not behave nicely in +-- concert with op. +up-to-iso : (coe₁ coe₂ : Coequalizer h i) → Coequalizer.obj coe₁ ≅ Coequalizer.obj coe₂ +up-to-iso coe₁ coe₂ = record + { from = repack coe₁ coe₂ + ; to = repack coe₂ coe₁ + ; iso = record + { isoˡ = repack-cancel coe₂ coe₁ + ; isoʳ = repack-cancel coe₁ coe₂ + } + } + where + open Coequalizer + + repack : (coe₁ coe₂ : Coequalizer h i) → obj coe₁ ⇒ obj coe₂ + repack coe₁ coe₂ = coequalize coe₁ (equality coe₂) + + repack∘ : (coe₁ coe₂ coe₃ : Coequalizer h i) → repack coe₂ coe₃ ∘ repack coe₁ coe₂ ≈ repack coe₁ coe₃ + repack∘ coe₁ coe₂ coe₃ = unique coe₁ (⟺ (glueTrianglesˡ (⟺ (universal coe₂)) (⟺ (universal coe₁)))) -- unique e₃ (⟺ (glueTrianglesʳ (⟺ (universal e₃)) (⟺ (universal e₂)))) + + repack-cancel : (e₁ e₂ : Coequalizer h i) → repack e₁ e₂ ∘ repack e₂ e₁ ≈ id + repack-cancel coe₁ coe₂ = repack∘ coe₂ coe₁ coe₂ ○ ⟺ (id-coequalize coe₂) + +IsCoequalizer⇒Coequalizer : IsCoequalizer h i k → Coequalizer h i +IsCoequalizer⇒Coequalizer {k = k} is-coe = record + { arr = k + ; isCoequalizer = is-coe + } diff --git a/src/Categories/Diagram/Duality.agda b/src/Categories/Diagram/Duality.agda index 628de20b3..fdc79ec0c 100644 --- a/src/Categories/Diagram/Duality.agda +++ b/src/Categories/Diagram/Duality.agda @@ -57,10 +57,12 @@ Coequalizer⇒coEqualizer coe = record coEqualizer⇒Coequalizer : Equalizer f g → Coequalizer f g coEqualizer⇒Coequalizer e = record { arr = arr - ; equality = equality - ; coequalize = equalize - ; universal = universal - ; unique = unique + ; isCoequalizer = record + { equality = equality + ; coequalize = equalize + ; universal = universal + ; unique = unique + } } where open Equalizer e From 81cb5f38b6f012c1abcc22beed835cebb2c657e5 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Sat, 2 Jan 2021 20:01:30 -0800 Subject: [PATCH 08/11] Prove that the unit of the monadicity ajdunction is an iso --- src/Categories/Adjoint/Monadic/Crude.agda | 140 ++++++++++++------ .../Adjoint/Monadic/Properties.agda | 18 +-- 2 files changed, 103 insertions(+), 55 deletions(-) diff --git a/src/Categories/Adjoint/Monadic/Crude.agda b/src/Categories/Adjoint/Monadic/Crude.agda index 941a4278e..c203dad7a 100644 --- a/src/Categories/Adjoint/Monadic/Crude.agda +++ b/src/Categories/Adjoint/Monadic/Crude.agda @@ -15,6 +15,7 @@ open import Function using (_$_) open import Categories.Adjoint.Properties open import Categories.Adjoint.Monadic open import Categories.Adjoint.Monadic.Properties +open import Categories.Functor.Properties open import Categories.NaturalTransformation.NaturalIsomorphism open import Categories.NaturalTransformation open import Categories.Monad @@ -22,10 +23,12 @@ open import Categories.Monad open import Categories.Diagram.Coequalizer open import Categories.Diagram.ReflexivePair +open import Categories.Adjoint.Construction.EilenbergMoore open import Categories.Category.Construction.EilenbergMoore open import Categories.Category.Construction.Properties.EilenbergMoore open import Categories.Morphism +open import Categories.Morphism.Notation import Categories.Morphism.Reasoning as MR private @@ -50,17 +53,17 @@ private open Coequalizer --- TODO: I think a _lot_ of this can be factored out into a helper lemma: --- +-- We could do this with limits, but this is far easier. +PreservesReflexiveCoequalizers : (F : Functor 𝒟 𝒞) → Set _ +PreservesReflexiveCoequalizers F = ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → (coeq : Coequalizer 𝒟 f g) → IsCoequalizer 𝒞 (F.F₁ f) (F.F₁ g) (F.F₁ (arr coeq)) + where + module F = Functor F -- If 𝒟 has coequalizers of reflexive pairs, then the comparison functor has a left adjoint. module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where - -- The key part of the proof. As we have all reflexive coequalizers, we can create the following coequalizer. - -- We can think of this as identifying the action of the algebra lifted to a "free" structure - -- and the counit of the adjunction, as the unit of the adjunction (also lifted to the "free structure") is a section of both. - has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) - has-coequalizer M = has-reflexive-coequalizers record + reflexive-pair : (M : Module T) → ReflexivePair 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) + reflexive-pair M = record { s = L.F₁ (adjoint.unit.η (Module.A M)) ; isReflexivePair = record { sectionₗ = begin @@ -73,44 +76,89 @@ module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → Refl 𝒟.id ∎ } } - where + where open 𝒟.HomReasoning - -- -- If we have coequalizers of reflexive pairs, then we can define an "inverse" to the comparison functor. - -- Comparison⁻¹ : Functor 𝒞ᵀ 𝒟 - -- Comparison⁻¹ = record - -- { F₀ = λ M → obj (coeq M) - -- ; F₁ = λ {M} {N} α → coequalize (coeq M) $ begin - -- 𝒟 [ 𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr α) ] ∘ L.F₁ (Module.action M) ] ≈⟨ pullʳ (⟺ L.homomorphism) ⟩ - -- 𝒟 [ arr (coeq N) ∘ L.F₁ (𝒞 [ Module⇒.arr α ∘ Module.action M ]) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (Module⇒.commute α) ⟩ - -- 𝒟 [ arr (coeq N) ∘ L.F₁ (𝒞 [ Module.action N ∘ R.F₁ (L.F₁ (Module⇒.arr α)) ]) ] ≈⟨ refl⟩∘⟨ L.homomorphism ⟩ - -- 𝒟 [ arr (coeq N) ∘ 𝒟 [ L.F₁ (Module.action N) ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ] ≈⟨ pullˡ (equality (coeq N)) ⟩ - -- 𝒟 [ 𝒟 [ arr (coeq N) ∘ adjoint.counit.η (L.F₀ (Module.A N)) ] ∘ L.F₁ (R.F₁ (L.F₁ (Module⇒.arr α))) ] ≈⟨ extendˡ (adjoint.counit.commute (L.F₁ (Module⇒.arr α))) ⟩ - -- 𝒟 [ 𝒟 [ arr (coeq N) ∘ L.F₁ (Module⇒.arr α) ] ∘ adjoint.counit.η (L.₀ (Module.A M)) ] ∎ - -- ; identity = λ {A} → ⟺ $ unique (coeq A) $ begin - -- 𝒟 [ arr (coeq A) ∘ L.F₁ 𝒞.id ] ≈⟨ refl⟩∘⟨ L.identity ⟩ - -- 𝒟 [ arr (coeq A) ∘ 𝒟.id ] ≈⟨ id-comm ⟩ - -- 𝒟 [ 𝒟.id ∘ arr (coeq A) ] ∎ - -- ; homomorphism = λ {X} {Y} {Z} {f} {g} → ⟺ $ unique (coeq X) $ begin - -- 𝒟 [ arr (coeq Z) ∘ L.F₁ (𝒞 [ Module⇒.arr g ∘ Module⇒.arr f ]) ] ≈⟨ 𝒟.∘-resp-≈ʳ L.homomorphism ○ 𝒟.sym-assoc ⟩ - -- 𝒟 [ 𝒟 [ arr (coeq Z) ∘ L.F₁ (Module⇒.arr g) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (coeq Y) ⟩∘⟨refl ⟩ - -- 𝒟 [ 𝒟 [ coequalize (coeq Y) _ ∘ arr (coeq Y) ] ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ extendˡ (universal (coeq X)) ⟩ - -- 𝒟 [ 𝒟 [ coequalize (coeq Y) _ ∘ coequalize (coeq X) _ ] ∘ arr (coeq X) ] ∎ - -- ; F-resp-≈ = λ {A} {B} {f} {g} eq → unique (coeq A) $ begin - -- 𝒟 [ arr (coeq B) ∘ L.F₁ (Module⇒.arr g) ] ≈⟨ refl⟩∘⟨ L.F-resp-≈ (𝒞.Equiv.sym eq) ⟩ - -- 𝒟 [ arr (coeq B) ∘ L.F₁ (Module⇒.arr f) ] ≈⟨ universal (coeq A) ⟩ - -- 𝒟 [ coequalize (coeq A) _ ∘ arr (coeq A) ] ∎ - -- } - -- where - -- open 𝒟.HomReasoning - -- open MR 𝒟 - - -- module Comparison⁻¹ = Functor Comparison⁻¹ - - - - - --- -- If 𝒟 has coequalizers of reflexive pairs _and_ R preserves these coequalizers, then the unit of the adjunction --- -- from the previous section is an --- module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where + -- The key part of the proof. As we have all reflexive coequalizers, we can create the following coequalizer. + -- We can think of this as identifying the action of the algebra lifted to a "free" structure + -- and the counit of the adjunction, as the unit of the adjunction (also lifted to the "free structure") is a section of both. + has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) + has-coequalizer M = has-reflexive-coequalizers (reflexive-pair M) + + coequalizer : (M : Module T) → Coequalizer 𝒞 (R.F₁ (L.F₁ (Module.action M))) (R.F₁ (adjoint.counit.η (L.₀ (Module.A M)))) + coequalizer M = record + { arr = Module.action M + ; isCoequalizer = record + { equality = Module.commute M + ; coequalize = λ {X} {h} eq → 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] + ; universal = λ {C} {h} {eq} → begin + h ≈⟨ introʳ adjoint.zag ○ 𝒞.sym-assoc ⟩ + 𝒞 [ 𝒞 [ h ∘ R.F₁ (adjoint.counit.η (L.₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ pushˡ (⟺ eq) ⟩ + 𝒞 [ h ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ] ≈⟨ pushʳ (adjoint.unit.sym-commute (Module.action M)) ⟩ + 𝒞 [ 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ] ∎ + ; unique = λ {X} {h} {i} {eq} eq′ → begin + i ≈⟨ introʳ (Module.identity M) ⟩ + 𝒞 [ i ∘ 𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ] ≈⟨ pullˡ (⟺ eq′) ⟩ + 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∎ + } + } + where + open 𝒞.HomReasoning + open MR 𝒞 + + -- FIXME: These proofs are _horrible_ + unit-iso : PreservesReflexiveCoequalizers R → NaturalIsomorphism (Comparison ∘F Comparison⁻¹ adjoint has-coequalizer) idF + unit-iso preserves-reflexive-coeq = record + { F⇒G = ntHelper record + { η = λ M → record + { arr = coequalizer-iso.from M + ; commute = begin + 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ≈⟨ introʳ (R.F-resp-≈ L.identity ○ R.identity) ⟩ + 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ∘ R.F₁ (L.F₁ 𝒞.id) ] ≈⟨ pushʳ (R.F-resp-≈ (L.F-resp-≈ (⟺ (coequalizer-iso.isoˡ M))) ○ (R.F-resp-≈ L.homomorphism) ○ R.homomorphism) ⟩ + 𝒞 [ 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ∘ R.F₁ (L.F₁ (coequalizer-iso.to M)) ] ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ≈⟨ 𝒞.Equiv.refl ⟩ + 𝒞 [ 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ∘ R.F₁ (L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ])) ] ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ≈⟨ (refl⟩∘⟨ (R.F-resp-≈ L.homomorphism ○ R.homomorphism)) ⟩∘⟨refl ⟩ + 𝒞 [ 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ∘ 𝒞 [ R.F₁ (L.F₁ (R.F₁ (arr (has-coequalizer M)))) ∘ R.F₁ (L.F₁ (adjoint.unit.η (Module.A M))) ] ] ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ≈⟨ center ([ R ]-resp-square (adjoint.counit.commute (arr (has-coequalizer M)))) ⟩∘⟨refl ⟩ + 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ R.F₁ (adjoint.counit.η (L.F₀ (Module.A M))) ] ∘ R.F₁ (L.F₁ (adjoint.unit.η (Module.A M))) ] ] ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ≈⟨ ( (refl⟩∘⟨ (cancelʳ (⟺ R.homomorphism ○ R.F-resp-≈ adjoint.zig ○ R.identity))) ⟩∘⟨refl) ⟩ + 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (arr (has-coequalizer M)) ] ∘ R.F₁ (L.F₁ (_≅_.from (coequalizer-iso M))) ] ≈˘⟨ IsCoequalizer.universal (has-coequalizer′ M) ⟩∘⟨refl ⟩ + 𝒞 [ Module.action M ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ∎ + } + ; commute = λ {M} {N} f → begin + 𝒞 [ IsCoequalizer.coequalize (has-coequalizer′ N) _ ∘ R.F₁ (coequalize (has-coequalizer M) _) ] ≈⟨ refl⟩∘⟨ preserves-coequalizer-unique M ⟩ + -- This is _bad. I should have a lemma somewhere that composition of coequalizers is the same as a coequalizer. + 𝒞 [ IsCoequalizer.coequalize (has-coequalizer′ N) _ ∘ IsCoequalizer.coequalize (has-coequalizer′ M) _ ] ≈⟨ IsCoequalizer.unique (has-coequalizer′ M) (Module⇒.commute f ○ pushˡ (IsCoequalizer.universal (has-coequalizer′ N)) ○ 𝒞.∘-resp-≈ʳ (⟺ R.homomorphism) ○ pushʳ (IsCoequalizer.universal (has-coequalizer′ M))) ⟩ + IsCoequalizer.coequalize (has-coequalizer′ M) (extendˡ (Module.commute M)) ≈˘⟨ IsCoequalizer.unique (has-coequalizer′ M) (pushʳ (IsCoequalizer.universal (has-coequalizer′ M))) ⟩ + 𝒞 [ Module⇒.arr f ∘ IsCoequalizer.coequalize (has-coequalizer′ M) _ ] ∎ + } + ; F⇐G = Comparison⁻¹⊣Comparison.unit adjoint has-coequalizer + ; iso = λ M → record + { isoˡ = begin + -- This is _horrible_. Needs to be refactored + 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ∘ IsCoequalizer.coequalize (has-coequalizer′ M) _ ] ≈⟨ IsCoequalizer.unique (has-coequalizer′ M) (pushʳ (IsCoequalizer.universal (has-coequalizer′ M))) ⟩ + -- We should have a helper lemma somewhere for this that isn't as general as coequalize-resp-≈′ + IsCoequalizer.coequalize (has-coequalizer′ M) (extendˡ (Module.commute M)) ≈˘⟨ IsCoequalizer.unique (has-coequalizer′ M) (extendˡ (adjoint.unit.commute (Module.action M)) ○ 𝒞.∘-resp-≈ˡ (IsCoequalizer.equality (has-coequalizer′ M)) ○ pullʳ adjoint.zag ○ id-comm) ⟩ + 𝒞.id ∎ + ; isoʳ = begin + 𝒞 [ IsCoequalizer.coequalize (has-coequalizer′ M) _ ∘ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ] ≈⟨ pullˡ (⟺ (IsCoequalizer.universal (has-coequalizer′ M))) ⟩ + 𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ≈⟨ Module.identity M ⟩ + 𝒞.id ∎ + } + } + where + open 𝒞.HomReasoning + open MR 𝒞 + + coequalizer-iso : (M : Module T) → 𝒞 [ R.F₀ (obj (has-reflexive-coequalizers (reflexive-pair M))) ≅ obj (coequalizer M) ] + coequalizer-iso M = up-to-iso 𝒞 ((IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair M) (has-coequalizer M)))) (coequalizer M) + + -- better name? + has-coequalizer′ : ∀ (M : Module T) → IsCoequalizer 𝒞 (R.F₁ (L.F₁ (Module.action M))) (R.F₁ (adjoint.counit.η (L.₀ (Module.A M)))) (R.F₁ (arr (has-coequalizer M))) + has-coequalizer′ M = (preserves-reflexive-coeq (reflexive-pair M) (has-coequalizer M)) + + -- This should probably live alongside the definition of preserving reflexive coequalizers. + preserves-coequalizer-unique : ∀ (M : Module T) → {Z : 𝒟.Obj} {h : 𝒟 [ L.F₀ (Module.A M) , Z ]} {eq : 𝒟 [ 𝒟 [ h ∘ L.F₁ (Module.action M) ] ≈ 𝒟 [ h ∘ adjoint.counit.η (L.₀ (Module.A M)) ] ]} + → 𝒞 [ R.F₁ (coequalize (has-coequalizer M) eq) ≈ IsCoequalizer.coequalize (has-coequalizer′ M) ([ R ]-resp-square eq) ] + preserves-coequalizer-unique M = begin + R.F₁ (coequalize (has-coequalizer M) _) ≈⟨ IsCoequalizer.unique (has-coequalizer′ M) (R.F-resp-≈ (universal (has-coequalizer M)) ○ R.homomorphism) ⟩ + IsCoequalizer.coequalize (has-coequalizer′ M) ([ R ]-resp-square _) ∎ + + module coequalizer-iso M = _≅_ (coequalizer-iso M) diff --git a/src/Categories/Adjoint/Monadic/Properties.agda b/src/Categories/Adjoint/Monadic/Properties.agda index aa3107e65..9993ea287 100644 --- a/src/Categories/Adjoint/Monadic/Properties.agda +++ b/src/Categories/Adjoint/Monadic/Properties.agda @@ -46,7 +46,7 @@ private module Comparison = Functor Comparison --- If we have a coequalizer of the following diagram, then the comparison functor has a left adjoint. +-- If we have a coequalizer of the following diagram for every T-algabra, then the comparison functor has a left adjoint. module _ (has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M)))) where open Coequalizer @@ -86,16 +86,16 @@ module _ (has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module. { η = λ M → record { arr = 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ; commute = begin - 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ] ≈⟨ pullʳ (adjoint.unit.commute (Module.action M)) ⟩ + 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ] ≈⟨ pullʳ (adjoint.unit.commute (Module.action M)) ⟩ -- It would be nice to have a reasoning combinator doing this "⟺ homomorphism ... homomorphism" pattern - 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩ - 𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ L.F₁ (Module.action M) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.F-resp-≈ (equality (has-coequalizer M)) ⟩∘⟨refl) ⟩ - 𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ adjoint.counit.η (L.F₀ (Module.A M)) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.homomorphism ⟩∘⟨refl) ⟩ - 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ R.F₁ (adjoint.counit.η (L.F₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ cancelʳ adjoint.zag ⟩ + 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩ + 𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ L.F₁ (Module.action M) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.F-resp-≈ (equality (has-coequalizer M)) ⟩∘⟨refl) ⟩ + 𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ adjoint.counit.η (L.F₀ (Module.A M)) ]) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ (R.homomorphism ⟩∘⟨refl) ⟩ + 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ R.F₁ (adjoint.counit.η (L.F₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ cancelʳ adjoint.zag ⟩ -- FIXME Use something like cancel here - R.F₁ (arr (has-coequalizer M)) ≈˘⟨ R.F-resp-≈ (𝒟.identityʳ) ⟩ - R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟.id ]) ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ adjoint.zig) ⟩ - R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟 [ adjoint.counit.η (L.F₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ]) ≈⟨ R.F-resp-≈ (MR.extendʳ 𝒟 (adjoint.counit.sym-commute (arr (has-coequalizer M)))) ⟩ + R.F₁ (arr (has-coequalizer M)) ≈˘⟨ R.F-resp-≈ (𝒟.identityʳ) ⟩ + R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟.id ]) ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ adjoint.zig) ⟩ + R.F₁ (𝒟 [ arr (has-coequalizer M) ∘ 𝒟 [ adjoint.counit.η (L.F₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ]) ≈⟨ R.F-resp-≈ (MR.extendʳ 𝒟 (adjoint.counit.sym-commute (arr (has-coequalizer M)))) ⟩ R.F₁ (𝒟 [ adjoint.counit.η (obj (has-coequalizer M)) ∘ 𝒟 [ L.F₁ (R.F₁ (arr (has-coequalizer M))) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ]) ≈˘⟨ R.F-resp-≈ (𝒟.∘-resp-≈ʳ L.homomorphism) ⟩ R.F₁ (𝒟 [ adjoint.counit.η (obj (has-coequalizer M)) ∘ L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M)])]) ≈⟨ R.homomorphism ⟩ 𝒞 [ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ∘ R.F₁ (L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M)])) ] ∎ From 83ae4b47902568d0b47cb3be6b4cb4b85b6e4a51 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Sun, 3 Jan 2021 01:32:16 -0800 Subject: [PATCH 09/11] Serious refactor of the crude monadicity proof --- src/Categories/Adjoint/Monadic/Crude.agda | 193 +++++++++--------- .../Adjoint/Monadic/Properties.agda | 5 +- src/Categories/Functor/Properties.agda | 3 +- 3 files changed, 99 insertions(+), 102 deletions(-) diff --git a/src/Categories/Adjoint/Monadic/Crude.agda b/src/Categories/Adjoint/Monadic/Crude.agda index c203dad7a..49ac332d6 100644 --- a/src/Categories/Adjoint/Monadic/Crude.agda +++ b/src/Categories/Adjoint/Monadic/Crude.agda @@ -11,12 +11,13 @@ module Categories.Adjoint.Monadic.Crude {o ℓ e o′ ℓ′ e′} {𝒞 : Categ open import Level open import Function using (_$_) +open import Data.Product using (Σ-syntax; _,_) open import Categories.Adjoint.Properties open import Categories.Adjoint.Monadic open import Categories.Adjoint.Monadic.Properties open import Categories.Functor.Properties -open import Categories.NaturalTransformation.NaturalIsomorphism +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism) open import Categories.NaturalTransformation open import Categories.Monad @@ -29,6 +30,7 @@ open import Categories.Category.Construction.Properties.EilenbergMoore open import Categories.Morphism open import Categories.Morphism.Notation +open import Categories.Morphism.Properties import Categories.Morphism.Reasoning as MR private @@ -59,106 +61,101 @@ PreservesReflexiveCoequalizers F = ∀ {A B} {f g : 𝒟 [ A , B ]} → Reflexiv where module F = Functor F --- If 𝒟 has coequalizers of reflexive pairs, then the comparison functor has a left adjoint. -module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where +module _ {F : Functor 𝒟 𝒞} (preserves-reflexive-coeq : PreservesReflexiveCoequalizers F) where + open Functor F - reflexive-pair : (M : Module T) → ReflexivePair 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) - reflexive-pair M = record - { s = L.F₁ (adjoint.unit.η (Module.A M)) - ; isReflexivePair = record - { sectionₗ = begin - 𝒟 [ L.F₁ (Module.action M) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈˘⟨ L.homomorphism ⟩ - L.F₁ (𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ) ≈⟨ L.F-resp-≈ (Module.identity M) ⟩ - L.F₁ 𝒞.id ≈⟨ L.identity ⟩ - 𝒟.id ∎ - ; sectionᵣ = begin - 𝒟 [ adjoint.counit.η (L.₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈⟨ adjoint.zig ⟩ - 𝒟.id ∎ - } - } - where - open 𝒟.HomReasoning - - -- The key part of the proof. As we have all reflexive coequalizers, we can create the following coequalizer. - -- We can think of this as identifying the action of the algebra lifted to a "free" structure - -- and the counit of the adjunction, as the unit of the adjunction (also lifted to the "free structure") is a section of both. - has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) - has-coequalizer M = has-reflexive-coequalizers (reflexive-pair M) - - coequalizer : (M : Module T) → Coequalizer 𝒞 (R.F₁ (L.F₁ (Module.action M))) (R.F₁ (adjoint.counit.η (L.₀ (Module.A M)))) - coequalizer M = record - { arr = Module.action M - ; isCoequalizer = record - { equality = Module.commute M - ; coequalize = λ {X} {h} eq → 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] - ; universal = λ {C} {h} {eq} → begin - h ≈⟨ introʳ adjoint.zag ○ 𝒞.sym-assoc ⟩ - 𝒞 [ 𝒞 [ h ∘ R.F₁ (adjoint.counit.η (L.₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ pushˡ (⟺ eq) ⟩ - 𝒞 [ h ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ] ≈⟨ pushʳ (adjoint.unit.sym-commute (Module.action M)) ⟩ - 𝒞 [ 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ] ∎ - ; unique = λ {X} {h} {i} {eq} eq′ → begin - i ≈⟨ introʳ (Module.identity M) ⟩ - 𝒞 [ i ∘ 𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ] ≈⟨ pullˡ (⟺ eq′) ⟩ - 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∎ - } - } + -- Unfortunately, we need to prove that the 'coequalize' arrows are equal as a lemma + preserves-coequalizer-unique : ∀ {A B C} {f g : 𝒟 [ A , B ]} {h : 𝒟 [ B , C ]} {eq : 𝒟 [ 𝒟 [ h ∘ f ] ≈ 𝒟 [ h ∘ g ] ]} + → (reflexive-pair : ReflexivePair 𝒟 f g) → (coe : Coequalizer 𝒟 f g) + → 𝒞 [ F₁ (coequalize coe eq) ≈ IsCoequalizer.coequalize (preserves-reflexive-coeq reflexive-pair coe) ([ F ]-resp-square eq) ] + preserves-coequalizer-unique reflexive-pair coe = IsCoequalizer.unique (preserves-reflexive-coeq reflexive-pair coe) (F-resp-≈ (universal coe) ○ homomorphism) where open 𝒞.HomReasoning - open MR 𝒞 - - -- FIXME: These proofs are _horrible_ - unit-iso : PreservesReflexiveCoequalizers R → NaturalIsomorphism (Comparison ∘F Comparison⁻¹ adjoint has-coequalizer) idF - unit-iso preserves-reflexive-coeq = record - { F⇒G = ntHelper record - { η = λ M → record - { arr = coequalizer-iso.from M - ; commute = begin - 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ≈⟨ introʳ (R.F-resp-≈ L.identity ○ R.identity) ⟩ - 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ∘ R.F₁ (L.F₁ 𝒞.id) ] ≈⟨ pushʳ (R.F-resp-≈ (L.F-resp-≈ (⟺ (coequalizer-iso.isoˡ M))) ○ (R.F-resp-≈ L.homomorphism) ○ R.homomorphism) ⟩ - 𝒞 [ 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ∘ R.F₁ (L.F₁ (coequalizer-iso.to M)) ] ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ≈⟨ 𝒞.Equiv.refl ⟩ - 𝒞 [ 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ∘ R.F₁ (L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ])) ] ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ≈⟨ (refl⟩∘⟨ (R.F-resp-≈ L.homomorphism ○ R.homomorphism)) ⟩∘⟨refl ⟩ - 𝒞 [ 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ] ∘ 𝒞 [ R.F₁ (L.F₁ (R.F₁ (arr (has-coequalizer M)))) ∘ R.F₁ (L.F₁ (adjoint.unit.η (Module.A M))) ] ] ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ≈⟨ center ([ R ]-resp-square (adjoint.counit.commute (arr (has-coequalizer M)))) ⟩∘⟨refl ⟩ - 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ R.F₁ (adjoint.counit.η (L.F₀ (Module.A M))) ] ∘ R.F₁ (L.F₁ (adjoint.unit.η (Module.A M))) ] ] ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ≈⟨ ( (refl⟩∘⟨ (cancelʳ (⟺ R.homomorphism ○ R.F-resp-≈ adjoint.zig ○ R.identity))) ⟩∘⟨refl) ⟩ - 𝒞 [ 𝒞 [ coequalizer-iso.from M ∘ R.F₁ (arr (has-coequalizer M)) ] ∘ R.F₁ (L.F₁ (_≅_.from (coequalizer-iso M))) ] ≈˘⟨ IsCoequalizer.universal (has-coequalizer′ M) ⟩∘⟨refl ⟩ - 𝒞 [ Module.action M ∘ R.F₁ (L.F₁ (coequalizer-iso.from M)) ] ∎ - } - ; commute = λ {M} {N} f → begin - 𝒞 [ IsCoequalizer.coequalize (has-coequalizer′ N) _ ∘ R.F₁ (coequalize (has-coequalizer M) _) ] ≈⟨ refl⟩∘⟨ preserves-coequalizer-unique M ⟩ - -- This is _bad. I should have a lemma somewhere that composition of coequalizers is the same as a coequalizer. - 𝒞 [ IsCoequalizer.coequalize (has-coequalizer′ N) _ ∘ IsCoequalizer.coequalize (has-coequalizer′ M) _ ] ≈⟨ IsCoequalizer.unique (has-coequalizer′ M) (Module⇒.commute f ○ pushˡ (IsCoequalizer.universal (has-coequalizer′ N)) ○ 𝒞.∘-resp-≈ʳ (⟺ R.homomorphism) ○ pushʳ (IsCoequalizer.universal (has-coequalizer′ M))) ⟩ - IsCoequalizer.coequalize (has-coequalizer′ M) (extendˡ (Module.commute M)) ≈˘⟨ IsCoequalizer.unique (has-coequalizer′ M) (pushʳ (IsCoequalizer.universal (has-coequalizer′ M))) ⟩ - 𝒞 [ Module⇒.arr f ∘ IsCoequalizer.coequalize (has-coequalizer′ M) _ ] ∎ - } - ; F⇐G = Comparison⁻¹⊣Comparison.unit adjoint has-coequalizer - ; iso = λ M → record - { isoˡ = begin - -- This is _horrible_. Needs to be refactored - 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ∘ IsCoequalizer.coequalize (has-coequalizer′ M) _ ] ≈⟨ IsCoequalizer.unique (has-coequalizer′ M) (pushʳ (IsCoequalizer.universal (has-coequalizer′ M))) ⟩ - -- We should have a helper lemma somewhere for this that isn't as general as coequalize-resp-≈′ - IsCoequalizer.coequalize (has-coequalizer′ M) (extendˡ (Module.commute M)) ≈˘⟨ IsCoequalizer.unique (has-coequalizer′ M) (extendˡ (adjoint.unit.commute (Module.action M)) ○ 𝒞.∘-resp-≈ˡ (IsCoequalizer.equality (has-coequalizer′ M)) ○ pullʳ adjoint.zag ○ id-comm) ⟩ - 𝒞.id ∎ - ; isoʳ = begin - 𝒞 [ IsCoequalizer.coequalize (has-coequalizer′ M) _ ∘ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ] ≈⟨ pullˡ (⟺ (IsCoequalizer.universal (has-coequalizer′ M))) ⟩ - 𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ≈⟨ Module.identity M ⟩ - 𝒞.id ∎ - } - } - where - open 𝒞.HomReasoning - open MR 𝒞 - - coequalizer-iso : (M : Module T) → 𝒞 [ R.F₀ (obj (has-reflexive-coequalizers (reflexive-pair M))) ≅ obj (coequalizer M) ] - coequalizer-iso M = up-to-iso 𝒞 ((IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair M) (has-coequalizer M)))) (coequalizer M) - -- better name? - has-coequalizer′ : ∀ (M : Module T) → IsCoequalizer 𝒞 (R.F₁ (L.F₁ (Module.action M))) (R.F₁ (adjoint.counit.η (L.₀ (Module.A M)))) (R.F₁ (arr (has-coequalizer M))) - has-coequalizer′ M = (preserves-reflexive-coeq (reflexive-pair M) (has-coequalizer M)) - -- This should probably live alongside the definition of preserving reflexive coequalizers. - preserves-coequalizer-unique : ∀ (M : Module T) → {Z : 𝒟.Obj} {h : 𝒟 [ L.F₀ (Module.A M) , Z ]} {eq : 𝒟 [ 𝒟 [ h ∘ L.F₁ (Module.action M) ] ≈ 𝒟 [ h ∘ adjoint.counit.η (L.₀ (Module.A M)) ] ]} - → 𝒞 [ R.F₁ (coequalize (has-coequalizer M) eq) ≈ IsCoequalizer.coequalize (has-coequalizer′ M) ([ R ]-resp-square eq) ] - preserves-coequalizer-unique M = begin - R.F₁ (coequalize (has-coequalizer M) _) ≈⟨ IsCoequalizer.unique (has-coequalizer′ M) (R.F-resp-≈ (universal (has-coequalizer M)) ○ R.homomorphism) ⟩ - IsCoequalizer.coequalize (has-coequalizer′ M) ([ R ]-resp-square _) ∎ +-- If 𝒟 has coequalizers of reflexive pairs, then the comparison functor has a left adjoint. +module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → ReflexivePair 𝒟 f g → Coequalizer 𝒟 f g) where - module coequalizer-iso M = _≅_ (coequalizer-iso M) + private + reflexive-pair : (M : Module T) → ReflexivePair 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) + reflexive-pair M = record + { s = L.F₁ (adjoint.unit.η (Module.A M)) + ; isReflexivePair = record + { sectionₗ = begin + 𝒟 [ L.F₁ (Module.action M) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈˘⟨ L.homomorphism ⟩ + L.F₁ (𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ) ≈⟨ L.F-resp-≈ (Module.identity M) ⟩ + L.F₁ 𝒞.id ≈⟨ L.identity ⟩ + 𝒟.id ∎ + ; sectionᵣ = begin + 𝒟 [ adjoint.counit.η (L.₀ (Module.A M)) ∘ L.F₁ (adjoint.unit.η (Module.A M)) ] ≈⟨ adjoint.zig ⟩ + 𝒟.id ∎ + } + } + where + open 𝒟.HomReasoning + + -- The key part of the proof. As we have all reflexive coequalizers, we can create the following coequalizer. + -- We can think of this as identifying the action of the algebra lifted to a "free" structure + -- and the counit of the adjunction, as the unit of the adjunction (also lifted to the "free structure") is a section of both. + has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module.action M)) (adjoint.counit.η (L.₀ (Module.A M))) + has-coequalizer M = has-reflexive-coequalizers (reflexive-pair M) + + module Comparison⁻¹ = Functor (Comparison⁻¹ adjoint has-coequalizer) + module Comparison⁻¹⊣Comparison = Adjoint (Comparison⁻¹⊣Comparison adjoint has-coequalizer) + + -- We have one interesting coequalizer in 𝒞 built out of a T-module's action. + coequalizer-action : (M : Module T) → Coequalizer 𝒞 (R.F₁ (L.F₁ (Module.action M))) (R.F₁ (adjoint.counit.η (L.₀ (Module.A M)))) + coequalizer-action M = record + { arr = Module.action M + ; isCoequalizer = record + { equality = Module.commute M + ; coequalize = λ {X} {h} eq → 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] + ; universal = λ {C} {h} {eq} → begin + h ≈⟨ introʳ adjoint.zag ○ 𝒞.sym-assoc ⟩ + 𝒞 [ 𝒞 [ h ∘ R.F₁ (adjoint.counit.η (L.₀ (Module.A M))) ] ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ≈⟨ pushˡ (⟺ eq) ⟩ + 𝒞 [ h ∘ 𝒞 [ R.F₁ (L.F₁ (Module.action M)) ∘ adjoint.unit.η (R.F₀ (L.F₀ (Module.A M))) ] ] ≈⟨ pushʳ (adjoint.unit.sym-commute (Module.action M)) ⟩ + 𝒞 [ 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∘ Module.action M ] ∎ + ; unique = λ {X} {h} {i} {eq} eq′ → begin + i ≈⟨ introʳ (Module.identity M) ⟩ + 𝒞 [ i ∘ 𝒞 [ Module.action M ∘ adjoint.unit.η (Module.A M) ] ] ≈⟨ pullˡ (⟺ eq′) ⟩ + 𝒞 [ h ∘ adjoint.unit.η (Module.A M) ] ∎ + } + } + where + open 𝒞.HomReasoning + open MR 𝒞 + + -- If 'R' preserves reflexive coequalizers, then the unit of the adjunction is a pointwise isomorphism + unit-iso : PreservesReflexiveCoequalizers R → (X : Module T) → Σ[ h ∈ 𝒞ᵀ [ Comparison.F₀ (Comparison⁻¹.F₀ X) , X ] ] (Iso 𝒞ᵀ (Comparison⁻¹⊣Comparison.unit.η X) h) + unit-iso preserves-reflexive-coeq X = + let + coequalizerˣ = has-coequalizer X + coequalizerᴿˣ = ((IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair X) (has-coequalizer X)))) + coequalizer-iso = up-to-iso 𝒞 (coequalizer-action X) coequalizerᴿˣ + module coequalizer-iso = _≅_ coequalizer-iso + open 𝒞 + open 𝒞.HomReasoning + open MR 𝒞 + α = record + { arr = coequalizer-iso.to + ; commute = begin + coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _) ≈⟨ introʳ (R.F-resp-≈ L.identity ○ R.identity) ⟩ + (coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ 𝒞.id) ≈⟨ pushʳ (R.F-resp-≈ (L.F-resp-≈ (⟺ coequalizer-iso.isoʳ)) ○ R.F-resp-≈ L.homomorphism ○ R.homomorphism) ⟩ + ((coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ (R.F₁ (arr coequalizerˣ) ∘ adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to) ≈⟨ (refl⟩∘⟨ (R.F-resp-≈ L.homomorphism ○ R.homomorphism)) ⟩∘⟨refl ⟩ + ((coequalizer-iso.to ∘ R.F₁ (adjoint.counit.η _)) ∘ R.F₁ (L.F₁ (R.F₁ (arr coequalizerˣ))) ∘ R.F₁ (L.F₁ (adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to) ≈⟨ center ([ R ]-resp-square (adjoint.counit.commute _)) ⟩∘⟨refl ⟩ + ((coequalizer-iso.to ∘ (R.F₁ (arr coequalizerˣ) ∘ R.F₁ (adjoint.counit.η (L.F₀ _))) ∘ R.F₁ (L.F₁ (adjoint.unit.η _))) ∘ R.F₁ (L.F₁ coequalizer-iso.to)) ≈⟨ (refl⟩∘⟨ cancelʳ (⟺ R.homomorphism ○ R.F-resp-≈ adjoint.zig ○ R.identity)) ⟩∘⟨refl ⟩ + (coequalizer-iso.to ∘ R.F₁ (arr coequalizerˣ)) ∘ R.F₁ (L.F₁ coequalizer-iso.to) ≈˘⟨ universal coequalizerᴿˣ ⟩∘⟨refl ⟩ + Module.action X ∘ R.F₁ (L.F₁ coequalizer-iso.to) ∎ + } + in α , record { isoˡ = coequalizer-iso.isoˡ ; isoʳ = coequalizer-iso.isoʳ } + + -- If 'R' preserves reflexive coequalizers and reflects isomorphisms, then the counit of the adjunction is a pointwise isomorphism. + counit-iso : PreservesReflexiveCoequalizers R → Conservative R → (X : 𝒟.Obj) → Σ[ h ∈ 𝒟 [ X , Comparison⁻¹.F₀ (Comparison.F₀ X) ] ] Iso 𝒟 (Comparison⁻¹⊣Comparison.counit.η X) h + counit-iso preserves-reflexive-coeq conservative X = + let coequalizerᴿᴷˣ = IsCoequalizer⇒Coequalizer 𝒞 (preserves-reflexive-coeq (reflexive-pair (Comparison.F₀ X)) (has-coequalizer (Comparison.F₀ X))) + coequalizerᴷˣ = has-coequalizer (Comparison.F₀ X) + coequalizer-iso = up-to-iso 𝒞 coequalizerᴿᴷˣ (coequalizer-action (Comparison.F₀ X)) + module coequalizer-iso = _≅_ coequalizer-iso + open 𝒞.HomReasoning + open 𝒞.Equiv + in conservative (Iso-resp-≈ 𝒞 coequalizer-iso.iso (⟺ (preserves-coequalizer-unique {R} preserves-reflexive-coeq (reflexive-pair (Comparison.F₀ X)) coequalizerᴷˣ)) refl) diff --git a/src/Categories/Adjoint/Monadic/Properties.agda b/src/Categories/Adjoint/Monadic/Properties.agda index 9993ea287..0bc405389 100644 --- a/src/Categories/Adjoint/Monadic/Properties.agda +++ b/src/Categories/Adjoint/Monadic/Properties.agda @@ -79,7 +79,8 @@ module _ (has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module. open 𝒟.HomReasoning open MR 𝒟 - module Comparison⁻¹ = Functor Comparison⁻¹ + private + module Comparison⁻¹ = Functor Comparison⁻¹ Comparison⁻¹⊣Comparison : Comparison⁻¹ ⊣ Comparison Adjoint.unit Comparison⁻¹⊣Comparison = ntHelper record @@ -135,5 +136,3 @@ module _ (has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module. where open 𝒞.HomReasoning open MR 𝒞 - - module Comparison⁻¹⊣Comparison = Adjoint Comparison⁻¹⊣Comparison diff --git a/src/Categories/Functor/Properties.agda b/src/Categories/Functor/Properties.agda index 8eaf396b4..0f9d01f2d 100644 --- a/src/Categories/Functor/Properties.agda +++ b/src/Categories/Functor/Properties.agda @@ -16,6 +16,7 @@ import Categories.Morphism as Morphism import Categories.Morphism.Reasoning as Reas open import Categories.Morphism.IsoEquiv as IsoEquiv open import Categories.Morphism.Isomorphism +open import Categories.Morphism.Notation private variable @@ -50,7 +51,7 @@ EssentiallySurjective {C = C} {D = D} F = (d : Category.Obj D) → Σ C.Obj (λ module C = Category C Conservative : Functor C D → Set _ -Conservative {C = C} {D = D} F = ∀ {A B} → (f : C [ A , B ]) → (g : C [ B , A ]) → Iso D (F₁ f) (F₁ g) → Iso C f g +Conservative {C = C} {D = D} F = ∀ {A B} {f : C [ A , B ]} {g : D [ F₀ B , F₀ A ]} → Iso D (F₁ f) g → Σ (C [ B , A ]) (λ h → Iso C f h) where open Functor F open Morphism From 3ea456841a711218b19d46341685283e4e4b4ebf Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Tue, 19 Jan 2021 16:57:55 -0800 Subject: [PATCH 10/11] Prove the crude monadicity theorem --- src/Categories/Adjoint/Monadic/Crude.agda | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/Categories/Adjoint/Monadic/Crude.agda b/src/Categories/Adjoint/Monadic/Crude.agda index 49ac332d6..490348ea0 100644 --- a/src/Categories/Adjoint/Monadic/Crude.agda +++ b/src/Categories/Adjoint/Monadic/Crude.agda @@ -16,6 +16,8 @@ open import Data.Product using (Σ-syntax; _,_) open import Categories.Adjoint.Properties open import Categories.Adjoint.Monadic open import Categories.Adjoint.Monadic.Properties +open import Categories.Category.Equivalence using (StrongEquivalence) +open import Categories.Category.Equivalence.Properties using (pointwise-iso-equivalence) open import Categories.Functor.Properties open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism) open import Categories.NaturalTransformation @@ -159,3 +161,14 @@ module _ (has-reflexive-coequalizers : ∀ {A B} {f g : 𝒟 [ A , B ]} → Refl open 𝒞.HomReasoning open 𝒞.Equiv in conservative (Iso-resp-≈ 𝒞 coequalizer-iso.iso (⟺ (preserves-coequalizer-unique {R} preserves-reflexive-coeq (reflexive-pair (Comparison.F₀ X)) coequalizerᴷˣ)) refl) + + -- Now, for the final result. Both the unit and counit of the adjunction between the comparison functor and it's inverse are isomorphisms, + -- so therefore they form natural isomorphism. Therfore, we have an equivalence of categories. + crude-monadicity : PreservesReflexiveCoequalizers R → Conservative R → StrongEquivalence 𝒞ᵀ 𝒟 + crude-monadicity preserves-reflexlive-coeq conservative = record + { F = Comparison⁻¹ adjoint has-coequalizer + ; G = Comparison + ; weak-inverse = pointwise-iso-equivalence (Comparison⁻¹⊣Comparison adjoint has-coequalizer) + (counit-iso preserves-reflexlive-coeq conservative) + (unit-iso preserves-reflexlive-coeq) + } From 6022bb97b7f29cdbd58572783f3cabd22748c54f Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Tue, 19 Jan 2021 17:01:22 -0800 Subject: [PATCH 11/11] Minor formatting fixes --- .../Adjoint/Monadic/Properties.agda | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Categories/Adjoint/Monadic/Properties.agda b/src/Categories/Adjoint/Monadic/Properties.agda index 0bc405389..f9ac0128d 100644 --- a/src/Categories/Adjoint/Monadic/Properties.agda +++ b/src/Categories/Adjoint/Monadic/Properties.agda @@ -102,9 +102,9 @@ module _ (has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module. 𝒞 [ R.F₁ (adjoint.counit.η (obj (has-coequalizer M))) ∘ R.F₁ (L.F₁ (𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M)])) ] ∎ } ; commute = λ {M} {N} f → begin - 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ adjoint.unit.η (Module.A N) ] ∘ Module⇒.arr f ] ≈⟨ extendˡ (adjoint.unit.commute (Module⇒.arr f)) ⟩ - 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ R.F₁ (L.F₁ (Module⇒.arr f)) ] ∘ adjoint.unit.η (Module.A M) ] ≈˘⟨ R.homomorphism ⟩∘⟨refl ⟩ - 𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr f) ]) ∘ adjoint.unit.η (Module.A M) ] ≈⟨ R.F-resp-≈ (universal (has-coequalizer M)) ⟩∘⟨refl ⟩ + 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ adjoint.unit.η (Module.A N) ] ∘ Module⇒.arr f ] ≈⟨ extendˡ (adjoint.unit.commute (Module⇒.arr f)) ⟩ + 𝒞 [ 𝒞 [ R.F₁ (arr (has-coequalizer N)) ∘ R.F₁ (L.F₁ (Module⇒.arr f)) ] ∘ adjoint.unit.η (Module.A M) ] ≈˘⟨ R.homomorphism ⟩∘⟨refl ⟩ + 𝒞 [ R.F₁ (𝒟 [ arr (has-coequalizer N) ∘ L.F₁ (Module⇒.arr f) ]) ∘ adjoint.unit.η (Module.A M) ] ≈⟨ R.F-resp-≈ (universal (has-coequalizer M)) ⟩∘⟨refl ⟩ 𝒞 [ R.F₁ (𝒟 [ (coequalize (has-coequalizer M) _) ∘ (arr (has-coequalizer M)) ]) ∘ adjoint.unit.η (Module.A M) ] ≈⟨ pushˡ R.homomorphism ⟩ 𝒞 [ R.F₁ (coequalize (has-coequalizer M) _) ∘ 𝒞 [ R.F₁ (arr (has-coequalizer M)) ∘ adjoint.unit.η (Module.A M) ] ] ∎ } @@ -114,25 +114,25 @@ module _ (has-coequalizer : (M : Module T) → Coequalizer 𝒟 (L.F₁ (Module. Adjoint.counit Comparison⁻¹⊣Comparison = ntHelper record { η = λ X → coequalize (has-coequalizer (Comparison.F₀ X)) (adjoint.counit.commute (adjoint.counit.η X)) ; commute = λ {X} {Y} f → begin - 𝒟 [ coequalize (has-coequalizer (Comparison.F₀ Y)) _ ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ] ≈⟨ unique (has-coequalizer (Comparison.F₀ X)) (adjoint.counit.sym-commute f ○ pushˡ (universal (has-coequalizer (Comparison.F₀ Y))) ○ pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩ - coequalize (has-coequalizer (Comparison.F₀ X)) (extendˡ (adjoint.counit.commute (adjoint.counit.η X))) ≈˘⟨ unique (has-coequalizer (Comparison.F₀ X)) (pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩ - 𝒟 [ f ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ] ∎ + 𝒟 [ coequalize (has-coequalizer (Comparison.F₀ Y)) _ ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ] ≈⟨ unique (has-coequalizer (Comparison.F₀ X)) (adjoint.counit.sym-commute f ○ pushˡ (universal (has-coequalizer (Comparison.F₀ Y))) ○ pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩ + coequalize (has-coequalizer (Comparison.F₀ X)) (extendˡ (adjoint.counit.commute (adjoint.counit.η X))) ≈˘⟨ unique (has-coequalizer (Comparison.F₀ X)) (pushʳ (universal (has-coequalizer (Comparison.F₀ X)))) ⟩ + 𝒟 [ f ∘ coequalize (has-coequalizer (Comparison.F₀ X)) _ ] ∎ } where open 𝒟.HomReasoning open MR 𝒟 Adjoint.zig Comparison⁻¹⊣Comparison {X} = begin 𝒟 [ coequalize (has-coequalizer (Comparison.F₀ (Comparison⁻¹.F₀ X))) _ ∘ coequalize (has-coequalizer X) _ ] ≈⟨ unique (has-coequalizer X) (⟺ adjoint.RLadjunct≈id ○ pushˡ (universal (has-coequalizer (Comparison.F₀ (Comparison⁻¹.F₀ X)))) ○ pushʳ (universal (has-coequalizer X))) ⟩ - coequalize (has-coequalizer X) {h = arr (has-coequalizer X)} (equality (has-coequalizer X)) ≈˘⟨ unique (has-coequalizer X) (⟺ 𝒟.identityˡ) ⟩ - 𝒟.id ∎ + coequalize (has-coequalizer X) {h = arr (has-coequalizer X)} (equality (has-coequalizer X)) ≈˘⟨ unique (has-coequalizer X) (⟺ 𝒟.identityˡ) ⟩ + 𝒟.id ∎ where open 𝒟.HomReasoning open MR 𝒟 Adjoint.zag Comparison⁻¹⊣Comparison {A} = begin 𝒞 [ R.F₁ (coequalize (has-coequalizer (Comparison.F₀ A)) _) ∘ 𝒞 [ R.F₁ (arr (has-coequalizer (Comparison.F₀ A))) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ] ≈⟨ pullˡ (⟺ R.homomorphism) ⟩ 𝒞 [ R.F₁ (𝒟 [ coequalize (has-coequalizer (Comparison.F₀ A)) _ ∘ arr (has-coequalizer (Comparison.F₀ A)) ]) ∘ adjoint.unit.η (Module.A (Comparison.F₀ A)) ] ≈˘⟨ R.F-resp-≈ (universal (has-coequalizer (Comparison.F₀ A))) ⟩∘⟨refl ⟩ - 𝒞 [ R.F₁ (adjoint.counit.η A) ∘ adjoint.unit.η (R.F₀ A) ] ≈⟨ adjoint.zag ⟩ - 𝒞.id ∎ + 𝒞 [ R.F₁ (adjoint.counit.η A) ∘ adjoint.unit.η (R.F₀ A) ] ≈⟨ adjoint.zag ⟩ + 𝒞.id ∎ where open 𝒞.HomReasoning open MR 𝒞