{-# OPTIONS --without-K #-}
open import Equality
module Adjunction
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where
open import Prelude hiding (id)
open import Category eq
open Derived-definitions-and-properties eq
open import Functor eq
private
Is-left-adjoint-of :
∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
{ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
Extensionality (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) →
C ⇨ D → D ⇨ C → Set _
Is-left-adjoint-of {ℓ₁} {ℓ₂} {C} {ℓ₃} {ℓ₄} {D} ext F G =
∃ λ (η : id⇨ ⇾ G ∙⇨ F) →
∃ λ (ε : F ∙⇨ G ⇾ id⇨) →
subst ((F ∙⇨ G) ∙⇨ F ⇾_) (id⇨∙⇨ ext₁) (ε ⇾∙⇨ F) ∙⇾
subst (_⇾ (F ∙⇨ G) ∙⇨ F) (∙⇨id⇨ ext₁)
(subst (F ∙⇨ id⇨ ⇾_) (∙⇨-assoc ext₁ F G) (F ⇨∙⇾ η))
≡
id⇾ F
×
subst (G ∙⇨ F ∙⇨ G ⇾_) (∙⇨id⇨ ext₂) (G ⇨∙⇾ ε) ∙⇾
subst (_⇾ G ∙⇨ F ∙⇨ G) (id⇨∙⇨ ext₂)
(subst (id⇨ ∙⇨ G ⇾_) (sym $ ∙⇨-assoc ext₂ G F) (η ⇾∙⇨ G))
≡
id⇾ G
where
ext₁ : Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄)
ext₁ = lower-extensionality (ℓ₃ ⊔ ℓ₄) ℓ₃ ext
ext₂ : Extensionality (ℓ₃ ⊔ ℓ₄) (ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
ext₂ = lower-extensionality (ℓ₁ ⊔ ℓ₂) ℓ₁ ext
_⊣_ :
∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
{ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
C ⇨ D → D ⇨ C → Set _
_⊣_ {ℓ₁} {ℓ₂} {C} {ℓ₃} {ℓ₄} {D} F G =
∃ λ (η : id⇨ ⇾ G ∙⇨ F) →
∃ λ (ε : F ∙⇨ G ⇾ id⇨) →
(∀ {X} → transformation ε D.∙ (F ⊙ transformation η {X = X}) ≡ D.id)
×
(∀ {X} → (G ⊙ transformation ε {X = X}) C.∙ transformation η ≡ C.id)
where
open _⇾_
module C = Precategory C
module D = Precategory D
Adjunction :
∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
Precategory ℓ₁ ℓ₂ → Precategory ℓ₃ ℓ₄ → Set _
Adjunction C D = ∃ λ (F : C ⇨ D) → ∃ λ (G : D ⇨ C) → F ⊣ G
Monad : ∀ {ℓ₁ ℓ₂} (C : Precategory ℓ₁ ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
Monad C =
∃ λ (F : C ⇨ C) →
∃ λ (η : id⇨ ⇾ F) →
∃ λ (μ : F ∙⇨ F ⇾ F) →
(∀ {X} → transformation μ ∙ (F ⊙ transformation μ {X = X})
≡
transformation μ ∙ transformation μ {X = F ⊚ X})
×
(∀ {X} → transformation μ ∙ (F ⊙ transformation η {X = X}) ≡ id)
×
(∀ {X} → transformation μ ∙ transformation η {X = F ⊚ X} ≡ id)
where
open _⇾_
open Precategory C
adjunction→monad :
∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
{ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
Adjunction C D → Monad C
adjunction→monad {C = C} {D = D} (F , G , η , ε , εFFη≡1 , GεηG≡1) =
G ∙⇨ F
, η
, GεF
, lemma₁
, lemma₂
, lemma₃
where
open _⇾_
module C = Precategory C
module D = Precategory D
GεF : (G ∙⇨ F) ∙⇨ (G ∙⇨ F) ⇾ G ∙⇨ F
natural-transformation GεF =
G ⊙ transformation ε
, nat
where
abstract
nat :
∀ {X Y} {f : C.Hom X Y} →
((G ∙⇨ F) ⊙ f) C.∙ (G ⊙ transformation ε) ≡
(G ⊙ transformation ε) C.∙ (((G ∙⇨ F) ∙⇨ (G ∙⇨ F)) ⊙ f)
nat {f = f} =
((G ∙⇨ F) ⊙ f) C.∙ (G ⊙ transformation ε) ≡⟨⟩
(G ⊙ F ⊙ f) C.∙ (G ⊙ transformation ε) ≡⟨ sym (⊙-∙ G) ⟩
G ⊙ ((F ⊙ f) D.∙ transformation ε) ≡⟨ cong (G ⊙_) (natural ε) ⟩
G ⊙ (transformation ε D.∙ (F ⊙ G ⊙ F ⊙ f)) ≡⟨ ⊙-∙ G ⟩
(G ⊙ transformation ε) C.∙ (G ⊙ F ⊙ G ⊙ F ⊙ f) ≡⟨⟩
(G ⊙ transformation ε) C.∙ (((G ∙⇨ F) ∙⇨ (G ∙⇨ F)) ⊙ f) ∎
abstract
lemma₁ :
∀ {X} →
transformation GεF {X = X} C.∙ ((G ∙⇨ F) ⊙ transformation GεF) ≡
transformation GεF C.∙ transformation GεF
lemma₁ =
(G ⊙ transformation ε) C.∙ (G ⊙ F ⊙ G ⊙ transformation ε) ≡⟨ sym (⊙-∙ G) ⟩
G ⊙ (transformation ε D.∙ (F ⊙ G ⊙ transformation ε)) ≡⟨ cong (G ⊙_) (sym $ natural ε) ⟩
G ⊙ (transformation ε D.∙ transformation ε) ≡⟨ ⊙-∙ G ⟩∎
(G ⊙ transformation ε) C.∙ (G ⊙ transformation ε) ∎
lemma₂ :
∀ {X} →
transformation GεF {X = X} C.∙ ((G ∙⇨ F) ⊙ transformation η) ≡
C.id
lemma₂ =
(G ⊙ transformation ε) C.∙ (G ⊙ F ⊙ transformation η) ≡⟨ sym (⊙-∙ G) ⟩
G ⊙ (transformation ε D.∙ (F ⊙ transformation η)) ≡⟨ cong (G ⊙_) εFFη≡1 ⟩
G ⊙ D.id ≡⟨ ⊙-id G ⟩∎
C.id ∎
lemma₃ :
∀ {X} →
transformation GεF {X = X} C.∙ transformation η ≡ C.id
lemma₃ =
(G ⊙ transformation ε) C.∙ transformation η ≡⟨ GεηG≡1 ⟩∎
C.id ∎