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

module Categories.Adjoint.Instance.Core where

-- The adjunction between the forgetful functor from Cats to Groupoids
-- and the Core functor.

open import Level using (_⊔_)
import Function

open import Categories.Adjoint using (_⊣_)
open import Categories.Category using (Category)
import Categories.Category.Construction.Core as C
open import Categories.Category.Groupoid using (Groupoid)
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Instance.Groupoids using (Groupoids)
open import Categories.Functor using (Functor; _∘F_; id)
open import Categories.Functor.Instance.Core using (Core)
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as MR
open import Categories.Morphism.IsoEquiv using (⌞_⌟)
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (refl; _≃_)

-- The forgetful functor from Groupoids to Cats

Forgetful :  {o  e}  Functor (Groupoids o  e) (Cats o  e)
Forgetful = record
  { F₀ = category
  ; F₁ = Function.id
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = Function.id
  }
  where open Groupoid

-- Core is right-adjoint to the forgetful functor from Groupoids to
-- Cats

CoreAdj :  {o  e}  Forgetful {o} {  e} {e}  Core
CoreAdj = record
  { unit   = ntHelper record { η = unit   ; commute = λ {G} {H} F  unit-commute {G} {H} F }
  ; counit = ntHelper record { η = counit ; commute = counit-commute }
  ; zig    = λ {G}  zig {G}
  ; zag    = zag
  }
  where
    open Groupoid using (category)
    module Core = Functor Core

    unit :  G  Functor (category G) (C.Core (category G))
    unit G = record
      { F₀ = Function.id
      ; F₁ = λ f  record { from = f ; to = f ⁻¹ ; iso = iso }
      ; identity     =  Equiv.refl 
      ; homomorphism =  Equiv.refl 
      ; F-resp-≈     = λ eq   eq 
      }
      where open Groupoid G

    unit-commute :  {G H} (F : Functor (category G) (category H)) 
                   unit H ∘F F  Core.F₁ F ∘F unit G
    unit-commute {G} {H} F = record
      { F⇒G = record { η = λ _  ≅.refl ; commute = λ _   MR.id-comm-sym (category H)  ; sym-commute = λ _   MR.id-comm (category H)  }
      ; F⇐G = record { η = λ _  ≅.refl ; commute = λ _   MR.id-comm-sym (category H)  ; sym-commute = λ _   MR.id-comm (category H)   }
      ; iso = λ _  record { isoˡ =  identityˡ  ; isoʳ =  identityˡ  }
      }
      where
        open Category (category H)
        open Morphism (category H)

    counit :  C  Functor (C.Core C) C
    counit C = record
      { F₀ = Function.id
      ; F₁ = _≅_.from
      ; identity     = Equiv.refl
      ; homomorphism = Equiv.refl
      ; F-resp-≈     = λ where  eq   eq
      }
      where
        open Category C
        open Morphism C

    counit-commute :  {C D} (F : Functor C D) 
                     counit D ∘F Core.F₁ F  F ∘F counit C
    counit-commute {C} {D} F = record
      { F⇒G = record { η = λ _  D.id ; commute = λ _  MR.id-comm-sym D ; sym-commute = λ _  MR.id-comm D }
      ; F⇐G = record { η = λ _  D.id ; commute = λ _  MR.id-comm-sym D ; sym-commute = λ _  MR.id-comm D }
      ; iso = λ _  _≅_.iso ≅.refl
      }
      where
        module D = Category D
        open Morphism D

    zig :  {G}  counit (category G) ∘F unit G  id
    zig {G} = record
      { F⇒G = record { η = λ _  G.id ; commute = λ _  MR.id-comm-sym (category G) ; sym-commute = λ _  MR.id-comm (category G) }
      ; F⇐G = record { η = λ _  G.id ; commute = λ _  MR.id-comm-sym (category G) ; sym-commute = λ _  MR.id-comm (category G) }
      ; iso = λ _  _≅_.iso ≅.refl
      }
      where
        module G = Groupoid G
        open Morphism G.category

    zag :  {B}  Core.F₁ (counit B) ∘F unit (Core.F₀ B)  id
    zag {B} = record
      { F⇒G = record { η = λ _  ≅.refl ; commute = λ _   MR.id-comm-sym B  ; sym-commute = λ _   MR.id-comm B  }
      ; F⇐G = record { η = λ _  ≅.refl ; commute = λ _   MR.id-comm-sym B  ; sym-commute = λ _   MR.id-comm B  }
      ; iso = λ _  record { isoˡ =  identityˡ  ; isoʳ =  identityˡ  }
      }
      where
        open Category B
        open Morphism B