Create Adjunctions.agda

src/Categories/Adjoint/Construction/AdjunctionTerminalInitial.agda

@@ -0,0 +1,84 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level
+open import Categories.Category.Core using (Category)
+open import Categories.Category
+open import Categories.Monad
+
+module Categories.Adjoint.Construction.AdjunctionTerminalInitial {o ℓ e} {C : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e} (M : Monad C) where
+
+open import Categories.Adjoint
+open import Categories.Functor
+open import Categories.NaturalTransformation.Core as NT
+open import Categories.NaturalTransformation.NaturalIsomorphism as NI
+open import Categories.Morphism.Reasoning as MR
+
+open import Categories.Adjoint.Construction.Adjunctions M
+
+open import Categories.Object.Terminal (Split M)
+open import Categories.Object.Initial (Split M)
+open import Categories.Category.Construction.EilenbergMoore
+open import Categories.Category.Construction.Kleisli
+open import Categories.Adjoint.Construction.Kleisli M as KL
+open import Categories.Adjoint.Construction.EilenbergMoore M as EM
+
+EM-object : SplitObj
+EM-object = record
+  { D = EilenbergMoore M
+  ; F = EM.Free
+  ; G = EM.Forgetful
+  ; adj = EM.Free⊣Forgetful
+  ; eqM = EM.FF≃F
+  }
+
+EM-terminal : IsTerminal EM-object
+EM-terminal = record
+  { ! = {!!}
+  ; !-unique = {!   !}
+  }
+
+
+Kl-object : SplitObj
+Kl-object = record
+  { D = Kleisli M
+  ; F = KL.Free
+  ; G = KL.Forgetful
+  ; adj = KL.Free⊣Forgetful
+  ; eqM = KL.FF≃F
+  }
+
+Kl-initial : IsInitial Kl-object
+Kl-initial = record
+  { ! = bang
+  ; !-unique = {!   !}
+  }
+  where
+    -- vanno aperte un po' di cose per non diventar matti
+    bang : {A : SplitObj} → Split⇒ Kl-object A
+    bang {splitobj D F G adj eq} = record
+      { H = record
+            { F₀ = λ T → Functor.F₀ F T
+            ; F₁ = λ {A} {B} f → adj.counit.η (F.₀ B) ∘ F.₁ (eq.⇐.η B C.∘ f)
+            ; identity = λ {A} → begin
+              adj.counit.η (F.₀ A) ∘ F.₁ (eq.⇐.η A C.∘ M.η.η A) ≈⟨ refl⟩∘⟨ Functor.F-resp-≈ F lemma ⟩
+              adj.counit.η (F.₀ A) ∘ F.₁ (adj.unit.η A)         ≈⟨ adj.zig ⟩
+              D.id                                              ∎
+            ; homomorphism = λ {X} {Y} {Z} {f} {g} → {!   !}
+            ; F-resp-≈ = λ x → D.∘-resp-≈ʳ (Functor.F-resp-≈ F (C.∘-resp-≈ʳ x))
+            }
+      ; HF≃F' = {!   !}
+      ; G'H≃G = {!   !}
+      }
+      where module adj    = Adjoint adj
+            module F      = Functor F
+            module M      = Monad M
+            module eq     = NaturalIsomorphism eq
+            open module D = Category D
+            open D.HomReasoning
+            module C = Category C
+
+            lemma : ∀ {A} → eq.⇐.η A C.∘ M.η.η A C.≈ adj.unit.η A
+            lemma {A} = C.HomReasoning.begin
+                eq.⇐.η A C.∘ M.η.η A C.HomReasoning.≈⟨ {!   !} ⟩
+                adj.unit.η A         C.HomReasoning.∎
+              where open C.HomReasoning

src/Categories/Adjoint/Construction/Adjunctions.agda

@@ -0,0 +1,73 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level
+open import Categories.Category.Core using (Category)
+open import Categories.Category
+open import Categories.Monad
+
+module Categories.Adjoint.Construction.Adjunctions {o ℓ e} {C : Category o ℓ e} (M : Monad C) where
+
+open Category C
+
+open import Categories.Adjoint
+open import Categories.Functor
+open import Categories.Morphism
+open import Categories.Functor.Properties
+open import Categories.NaturalTransformation.Core
+open import Categories.NaturalTransformation.NaturalIsomorphism
+open import Categories.Morphism.Reasoning as MR
+open import Categories.Tactic.Category
+
+-- three things:
+-- 1. the category of adjunctions splitting a given Monad
+-- 2. the proof that EM(M) is the terminal object here
+-- 3. the proof that KL(M) is the initial object here
+
+record SplitObj : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+  constructor splitobj
+  field
+    D : Category o ℓ e
+    F : Functor C D
+    G : Functor D C
+    adj : F ⊣ G
+    eqM : G ∘F F ≃ Monad.F M
+
+record Split⇒ (X Y : SplitObj) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+  constructor split⇒
+  private
+    module X = SplitObj X
+    module Y = SplitObj Y
+  field
+    H : Functor X.D Y.D
+    HF≃F' : H ∘F X.F ≃ Y.F
+    G'H≃G : Y.G ∘F H ≃ X.G
+
+Split : Monad C → Category _ _ _
+Split M = record
+  { Obj = SplitObj
+  ; _⇒_ = Split⇒
+  ; _≈_ = λ U V → Split⇒.H U ≃ Split⇒.H V
+  ; id = split-id
+  ; _∘_ = comp
+  ; assoc = λ { {f = f} {g = g} {h = h} → associator (Split⇒.H f) (Split⇒.H g) (Split⇒.H h) }
+  ; sym-assoc = λ { {f = f} {g = g} {h = h} → sym-associator (Split⇒.H f) (Split⇒.H g) (Split⇒.H h) }
+  ; identityˡ = unitorˡ
+  ; identityʳ = unitorʳ
+  ; identity² = unitor²
+  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
+  ; ∘-resp-≈ = _ⓘₕ_
+  }
+  where
+  open NaturalTransformation
+  split-id : {A : SplitObj} → Split⇒ A A
+  split-id = record
+    { H = Categories.Functor.id
+    ; HF≃F' = unitorˡ
+    ; G'H≃G = unitorʳ
+    }
+  comp : {A B X : SplitObj} → Split⇒ B X → Split⇒ A B → Split⇒ A X
+  comp {A = A} {B = B} {X = X} (split⇒ Hᵤ HF≃F'ᵤ G'H≃Gᵤ) (split⇒ Hᵥ HF≃F'ᵥ G'H≃Gᵥ) = record
+    { H = Hᵤ ∘F Hᵥ
+    ; HF≃F' = HF≃F'ᵤ ⓘᵥ (Hᵤ ⓘˡ HF≃F'ᵥ) ⓘᵥ associator (SplitObj.F A) Hᵥ Hᵤ
+    ; G'H≃G = G'H≃Gᵥ ⓘᵥ (G'H≃Gᵤ ⓘʳ Hᵥ) ⓘᵥ sym-associator Hᵥ Hᵤ (SplitObj.G X)
+    }