{-# OPTIONS --without-K --safe #-}
module Categories.NaturalTransformation.Dinatural where

open import Level
open import Data.Product
open import Relation.Binary using (Rel; IsEquivalence; Setoid)

open import Categories.Category
open import Categories.NaturalTransformation as NT hiding (_∘ʳ_)
open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.Functor.Bifunctor
open import Categories.Category.Product
import Categories.Morphism.Reasoning as MR

private
  variable
    o  e : Level
    C D E : Category o  e

record DinaturalTransformation (F G : Bifunctor (Category.op C) C D) : Set (levelOfTerm F) where
  eta-equality
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G

  open D hiding (op)
  open Commutation D

  field
    α          :  X  D [ F.F₀ (X , X) , G.F₀ (X , X) ]
    commute    :  {X Y} (f : C [ X , Y ]) 
                [ F.F₀ (Y , X)  G.F₀ (X , Y) ]⟨
                  F.F₁ (f , C.id)             ⇒⟨ F.F₀ (X , X) 
                  α X                         ⇒⟨ G.F₀ (X , X) 
                  G.F₁ (C.id , f)
                 F.F₁ (C.id , f)             ⇒⟨ F.F₀ (Y , Y) 
                  α Y                         ⇒⟨ G.F₀ (Y , Y) 
                  G.F₁ (f , C.id)
                
    -- We add this extra proof, because, again, we want to ensure the opposite of the
    -- opposite of dinatural transformation is definitionally equal to itself.
    op-commute :  {X Y} (f : C [ X , Y ]) 
                [ F.F₀ (Y , X)  G.F₀ (X , Y) ]⟨
                  F.F₁ (C.id , f)             ⇒⟨ F.F₀ (Y , Y) 
                  (α Y                         ⇒⟨ G.F₀ (Y , Y) 
                  G.F₁ (f , C.id))
                 F.F₁ (f , C.id)             ⇒⟨ F.F₀ (X , X) 
                  (α X                         ⇒⟨ G.F₀ (X , X) 
                  G.F₁ (C.id , f))
                

  op : DinaturalTransformation G.op F.op
  op = record
    { α          = α
    ; commute    = op-commute
    ; op-commute = commute
    }

-- to reduce the burden of constructing a DinaturalTransformation, we introduce
-- another helper.
record DTHelper (F G : Bifunctor (Category.op C) C D) : Set (levelOfTerm F) where
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
  open D hiding (op)
  open Commutation D

  field
    α          :  X  D [ F.F₀ (X , X) , G.F₀ (X , X) ]
    commute    :  {X Y} (f : C [ X , Y ]) 
                [ F.F₀ (Y , X)  G.F₀ (X , Y) ]⟨
                  F.F₁ (f , C.id)             ⇒⟨ F.F₀ (X , X) 
                  α X                         ⇒⟨ G.F₀ (X , X) 
                  G.F₁ (C.id , f)
                 F.F₁ (C.id , f)             ⇒⟨ F.F₀ (Y , Y) 
                  α Y                         ⇒⟨ G.F₀ (Y , Y) 
                  G.F₁ (f , C.id)
                

dtHelper :  {F G : Bifunctor (Category.op C) C D}  DTHelper F G  DinaturalTransformation F G
dtHelper {D = D} θ = record
  { α          = α
  ; commute    = commute
  ; op-commute = λ f  assoc   (commute f)  sym-assoc
  }
  where open DTHelper θ
        open Category D
        open HomReasoning

module _ {F G H : Bifunctor (Category.op C) C D} where
  private
    module C = Category C
  open Category D
  open HomReasoning
  open Functor
  open MR D

  infixr 9 _<∘_
  infixl 9 _∘>_

  _<∘_ : NaturalTransformation G H  DinaturalTransformation F G  DinaturalTransformation F H
  θ <∘ β = dtHelper record
    { α       = λ X  η (X , X)  α X
    ; commute = λ {X Y} f  begin
      F₁ H (C.id , f)  (η (X , X)  α X)  F₁ F (f , C.id)   ≈˘⟨ pushˡ (pushˡ (θ.commute (C.id , f))) 
      ((η (X , Y)  F₁ G (C.id , f))  α X)  F₁ F (f , C.id) ≈⟨ assoc  pullʳ (β.commute f) 
      η (X , Y)  F₁ G (f , C.id)  α Y  F₁ F (C.id , f)     ≈⟨ pullˡ (θ.commute (f , C.id))  pullʳ sym-assoc 
      F₁ H (f , C.id)  (η (Y , Y)  α Y)  F₁ F (C.id , f)   
    }
    where module θ = NaturalTransformation θ
          module β = DinaturalTransformation β
          open θ
          open β

  _∘>_ : DinaturalTransformation G H  NaturalTransformation F G  DinaturalTransformation F H
  β ∘> θ = dtHelper record
    { α       = λ X  α X  η (X , X)
    ; commute = λ {X Y} f  begin
      F₁ H (C.id , f)  (α X  η (X , X))  F₁ F (f , C.id) ≈⟨ refl⟩∘⟨ pullʳ (θ.commute (f , C.id)) 
      F₁ H (C.id , f)  α X  F₁ G (f , C.id)  η (Y , X)   ≈⟨ ∘-resp-≈ʳ sym-assoc  sym-assoc 
      (F₁ H (C.id , f)  α X  F₁ G (f , C.id))  η (Y , X) ≈⟨ β.commute f ⟩∘⟨refl 
      (F₁ H (f , C.id)  α Y  F₁ G (C.id , f))  η (Y , X) ≈˘⟨ pushʳ (assoc  pushʳ (θ.commute (C.id , f))) 
      F₁ H (f , C.id)  (α Y  η (Y , Y))  F₁ F (C.id , f) 
    }
    where module θ = NaturalTransformation θ
          module β = DinaturalTransformation β
          open θ
          open β

module _ {F G : Bifunctor (Category.op C) C D} where
  private
    module C = Category C
  open Category D
  open HomReasoning
  open Functor
  open MR D

  infixl 9 _∘ʳ_

  _∘ʳ_ :  {E : Category o  e} 
           DinaturalTransformation F G  (K : Functor E C)  DinaturalTransformation (F ∘F ((Functor.op K)  K)) (G ∘F ((Functor.op K)  K))
  _∘ʳ_ {E = E} β K = dtHelper record
    { α       = λ X  α (F₀ K X)
    ; commute = λ {X Y} f  begin
      F₁ G (F₁ K E.id , F₁ K f)  α (F₀ K X)  F₁ F (F₁ K f , F₁ K E.id)
        ≈⟨ F-resp-≈ G (identity K , C.Equiv.refl) ⟩∘⟨ Equiv.refl ⟩∘⟨ F-resp-≈ F (C.Equiv.refl , identity K) 
      F₁ G (C.id , F₁ K f)  α (F₀ K X)  F₁ F (F₁ K f , C.id)
        ≈⟨ commute (F₁ K f) 
      F₁ G (F₁ K f , C.id)  α (F₀ K Y)  F₁ F (C.id , F₁ K f)
        ≈˘⟨ F-resp-≈ G (C.Equiv.refl , identity K) ⟩∘⟨ Equiv.refl ⟩∘⟨ F-resp-≈ F (identity K , C.Equiv.refl) 
      F₁ G (F₁ K f , F₁ K E.id)  α (F₀ K Y)  F₁ F (F₁ K E.id , F₁ K f)
        
    }
    where module β = DinaturalTransformation β
          module E = Category E
          open β

  infix 4 _≃_

  _≃_ : Rel (DinaturalTransformation F G) _
  β  δ =  {X}  α β X  α δ X
    where open DinaturalTransformation

  ≃-isEquivalence : IsEquivalence _≃_
  ≃-isEquivalence = record
    { refl  = Equiv.refl
    ; sym   = λ eq  Equiv.sym eq
    ; trans = λ eq eq′  Equiv.trans eq eq′
    }

  ≃-setoid : Setoid _ _
  ≃-setoid = record
    { Carrier       = DinaturalTransformation F G
    ; _≈_           = _≃_
    ; isEquivalence = ≃-isEquivalence
    }


-- for convenience, the following are some helpers for the cases
-- in which the bifunctor on the right is extranatural.
Extranaturalʳ :  {C : Category o  e}  Category.Obj D  (F : Bifunctor (Category.op C) C D)  Set _
Extranaturalʳ A F = DinaturalTransformation (const A) F

Extranaturalˡ :  {C : Category o  e}  (F : Bifunctor (Category.op C) C D)  Category.Obj D  Set _
Extranaturalˡ F A = DinaturalTransformation F (const A)

module _ {F : Bifunctor (Category.op C) C D} where
  open Category D
  private
    module C = Category C
    variable
      A : Obj
      X Y : C.Obj
      f : X C.⇒ Y
  open Functor F
  open HomReasoning
  open MR D

  extranaturalʳ : (a :  X  A  F₀ (X , X)) 
                  (∀ {X X′ f}  F₁ (C.id , f)  a X  F₁ (f , C.id)  a X′) 
                  Extranaturalʳ A F
  extranaturalʳ a comm = dtHelper record
    { α       = a
    ; commute = λ f  ∘-resp-≈ʳ identityʳ  comm  ∘-resp-≈ʳ ( identityʳ)
    }

  open DinaturalTransformation

  extranatural-commʳ : (β : DinaturalTransformation (const A) F) 
                       F₁ (C.id , f)  α β X  F₁ (f , C.id)  α β Y
  extranatural-commʳ {f = f} β = ∘-resp-≈ʳ ( identityʳ)  commute β f  ∘-resp-≈ʳ identityʳ

  -- the dual case, the bifunctor on the left is extranatural.

  extranaturalˡ : (a :  X  F₀ (X , X)  A) 
                  (∀ {X X′ f}  a X  F₁ (f , C.id)  a X′  F₁ (C.id , f)) 
                  Extranaturalˡ F A
  extranaturalˡ a comm = dtHelper record
    { α       = a
    ; commute = λ f  pullˡ identityˡ  comm   (pullˡ identityˡ)
    }

  extranatural-commˡ : (β : DinaturalTransformation F (const A)) 
                       α β X  F₁ (f , C.id)  α β Y  F₁ (C.id , f)
  extranatural-commˡ {f = f} β =  (pullˡ identityˡ)  commute β f  pullˡ identityˡ