module AdjointResults where

open import Cubical.Foundations.Prelude

open import Cubical.Categories.Adjoint
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation

open import Cubical.Data.Sigma

private
  variable
    ℓC ℓC' ℓD ℓD' : Level

open Category
open Functor
open UnitCounit
open NatTrans

module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
  record MakeLeftAdjoint (R : Functor D C) : Type (ℓ-max (ℓ-max (ℓ-max ℓC ℓC') ℓD) ℓD') where
    field
      L₀ : C .ob → D .ob
      η : ∀ x → C [ x , R ⟅ L₀ x ⟆ ]
      universal : ∀ {x y} (f : C [ x , R ⟅ y ⟆ ]) → D [ L₀ x , y ]
      commutes  : ∀ {x y} (f : C [ x , R ⟅ y ⟆ ]) → R ⟪ universal f ⟫ ∘⟨ C ⟩ η x ≡ f
      unique    : ∀ {x y} {f : C [ x , R ⟅ y ⟆ ]} {g : D [ L₀ x , y ]}
                → R ⟪ g ⟫ ∘⟨ C ⟩ η x ≡ f
                → universal f ≡ g

    unique' : ∀ {x y} {g₁ g₂ : D [ L₀ x , y ]}
            → R ⟪ g₁ ⟫ ∘⟨ C ⟩ η x ≡ R ⟪ g₂ ⟫ ∘⟨ C ⟩ η x
            → g₁ ≡ g₂
    unique' p = sym (unique p) ∙ unique refl

    toFunctor : Functor C D
    F-ob toFunctor = L₀
    F-hom toFunctor f = universal (η _ ∘⟨ C ⟩ f)
    F-id toFunctor = unique
      (R ⟪ D .id ⟫ ∘⟨ C ⟩ η _ ≡⟨ cong (λ - → - ∘⟨ C ⟩ η _) (F-id R) ⟩
       C .id ∘⟨ C ⟩ η _       ≡⟨ C .⋆IdR _ ⟩
       η _                    ≡⟨ sym (C .⋆IdL _) ⟩
       η _ ∘⟨ C ⟩ C. id ∎)
    F-seq toFunctor f g = unique
      (R ⟪ universal (η _ ∘⟨ C ⟩ g) ∘⟨ D ⟩ universal (η _ ∘⟨ C ⟩ f) ⟫ ∘⟨ C ⟩ η _         ≡⟨ cong (seq' C (η _)) (F-seq R _ _) ⟩
       (R ⟪ universal (η _ ∘⟨ C ⟩ g) ⟫ ∘⟨ C ⟩ R ⟪ universal (η _ ∘⟨ C ⟩ f) ⟫) ∘⟨ C ⟩ η _ ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
       R ⟪ universal (η _ ∘⟨ C ⟩ g) ⟫ ∘⟨ C ⟩ R ⟪ universal (η _ ∘⟨ C ⟩ f) ⟫ ∘⟨ C ⟩ η _   ≡⟨ cong (comp' C (R ⟪ universal (comp' C (η _) g) ⟫)) (commutes (η _ ∘⟨ C ⟩ f)) ⟩
       R ⟪ universal (η _ ∘⟨ C ⟩ g) ⟫ ∘⟨ C ⟩ η _ ∘⟨ C ⟩ f                                ≡⟨ C .⋆Assoc _ _ _ ⟩
       (R ⟪ universal (η _ ∘⟨ C ⟩ g) ⟫ ∘⟨ C ⟩ η _) ∘⟨ C ⟩ f                              ≡⟨ cong (seq' C f) (commutes (η _ ∘⟨ C ⟩ g)) ⟩
       (η _ ∘⟨ C ⟩ g) ∘⟨ C ⟩ f                                                           ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
       η _ ∘⟨ C ⟩ g ∘⟨ C ⟩ f ∎)

    open TriangleIdentities

    toAdjoint : toFunctor ⊣ R
    toAdjoint ._⊣_.η .N-ob = η
    toAdjoint ._⊣_.η .N-hom {x} {y} f = sym (commutes (η y ∘⟨ C ⟩ f))
    toAdjoint ._⊣_.ε .N-ob y = universal (C .id)
    toAdjoint ._⊣_.ε .N-hom {x} {y} f =
      unique' (R ⟪ universal (C .id) ∘⟨ D ⟩ universal (η (R ⟅ y ⟆) ∘⟨ C ⟩ R ⟪ f ⟫) ⟫ ∘⟨ C ⟩ η (R ⟅ x ⟆)         ≡⟨ cong (seq' C (η (R ⟅ x ⟆))) (F-seq R _ _) ⟩
               (R ⟪ universal (C .id) ⟫ ∘⟨ C ⟩ R ⟪ universal (η (R ⟅ y ⟆) ∘⟨ C ⟩ R ⟪ f ⟫) ⟫) ∘⟨ C ⟩ η (R ⟅ x ⟆) ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
               R ⟪ universal (C .id) ⟫ ∘⟨ C ⟩ R ⟪ universal (η (R ⟅ y ⟆) ∘⟨ C ⟩ R ⟪ f ⟫) ⟫ ∘⟨ C ⟩ η (R ⟅ x ⟆)   ≡⟨ cong (comp' C (R ⟪ universal (C .id) ⟫)) (commutes (η (R ⟅ y ⟆) ∘⟨ C ⟩ R ⟪ f ⟫)) ⟩
               R ⟪ universal (C .id) ⟫ ∘⟨ C ⟩ η (R ⟅ y ⟆) ∘⟨ C ⟩ R ⟪ f ⟫                                        ≡⟨ C .⋆Assoc _ _ _ ⟩
               (R ⟪ universal (C .id) ⟫ ∘⟨ C ⟩ η (R ⟅ y ⟆)) ∘⟨ C ⟩ R ⟪ f ⟫                                      ≡⟨ cong (seq' C (R ⟪ f ⟫)) (commutes (C .id)) ⟩
               C .id ∘⟨ C ⟩ R ⟪ f ⟫                                                                             ≡⟨ C .⋆IdR _ ⟩
               R ⟪ f ⟫                                                                                          ≡⟨ sym (C .⋆IdL _) ⟩
               R ⟪ f ⟫ ∘⟨ C ⟩ C .id                                                                             ≡⟨ cong (comp' C (R ⟪ f ⟫)) (sym (commutes (C .id))) ⟩
               R ⟪ f ⟫ ∘⟨ C ⟩ (R ⟪ universal (C. id) ⟫ ∘⟨ C ⟩ η (R ⟅ x ⟆))                                      ≡⟨ C .⋆Assoc _ _ _ ⟩
               (R ⟪ f ⟫ ∘⟨ C ⟩ R ⟪ universal (C. id) ⟫) ∘⟨ C ⟩ η (R ⟅ x ⟆)                                      ≡⟨ cong (seq' C (η (R ⟅ x ⟆))) (sym (F-seq R _ _)) ⟩
               R ⟪ f ∘⟨ D ⟩ universal (C. id) ⟫ ∘⟨ C ⟩ η (R ⟅ x ⟆) ∎)
    toAdjoint ._⊣_.triangleIdentities .Δ₁ x =
      unique' (R ⟪ universal (C .id) ∘⟨ D ⟩ universal (η (R ⟅ L₀ x ⟆) ∘⟨ C ⟩ η x) ⟫ ∘⟨ C ⟩ η x         ≡⟨ cong (seq' C (η x)) (F-seq R _ _) ⟩
               (R ⟪ universal (C .id) ⟫ ∘⟨ C ⟩ R ⟪ universal (η (R ⟅ L₀ x ⟆) ∘⟨ C ⟩ η x) ⟫) ∘⟨ C ⟩ η x ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
               R ⟪ universal (C .id) ⟫ ∘⟨ C ⟩ R ⟪ universal (η (R ⟅ L₀ x ⟆) ∘⟨ C ⟩ η x) ⟫ ∘⟨ C ⟩ η x   ≡⟨ cong (comp' C (R ⟪ universal (C .id) ⟫)) (commutes (η (R ⟅ L₀ x ⟆) ∘⟨ C ⟩ η x)) ⟩
               R ⟪ universal (C .id) ⟫ ∘⟨ C ⟩ η (R ⟅ L₀ x ⟆) ∘⟨ C ⟩ η x                                ≡⟨ C .⋆Assoc _ _ _ ⟩
               (R ⟪ universal (C .id) ⟫ ∘⟨ C ⟩ η (R ⟅ L₀ x ⟆)) ∘⟨ C ⟩ η x                              ≡⟨ cong (seq' C (η x)) (commutes (C .id)) ⟩
               C .id ∘⟨ C ⟩ η x                                                                        ≡⟨ cong (seq' C (η x)) (sym (F-id R)) ⟩
               R ⟪ D .id ⟫ ∘⟨ C ⟩ η x ∎)
    toAdjoint ._⊣_.triangleIdentities .Δ₂ y = commutes (C .id)