```------------------------------------------------------------------------
------------------------------------------------------------------------

-- The code is based on the presentation in the HoTT book (but might

{-# OPTIONS --without-K #-}

open import Equality

{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 ext F G means that F is a left adjoint of G.
-- This definition tries to follow the HoTT book closely.

∀ {ℓ₁ ℓ₂} {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

-- F ⊣ G means that F is a left adjoint of G.
--
-- This definition avoids the use of subst in the previous definition
-- by making use of the equality characterisation for natural
-- transformations (equality-characterisation⇾). I (NAD) took the idea
-- for this definition from the HoTT-Agda library
--
-- TODO: Prove that the two definitions are equivalent.

_⊣_ :
∀ {ℓ₁ ℓ₂} {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

∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
Precategory ℓ₁ ℓ₂ → Precategory ℓ₃ ℓ₄ → Set _
Adjunction C D = ∃ λ (F : C ⇨ D) → ∃ λ (G : D ⇨ C) → F ⊣ G

------------------------------------------------------------------------

-- A monad on a precategory.
--
-- This definition is taken from Wikipedia

Monad : ∀ {ℓ₁ ℓ₂} (C : Precategory ℓ₁ ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
∃ λ (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

--
-- This definition is taken from Wikipedia

∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
{ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
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

-- This natural transformation is defined directly, rather than by
-- using composition, to avoid the use of casts.

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                                         ∎
```