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

module Categories.NaturalTransformation.Properties where

open import Level
open import Data.Product using (Σ; _,_)
open import Function.Bundles using (Func)

open import Categories.Category
open import Categories.Category.Product
open import Categories.Category.Instance.Setoids
open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.Functor.Construction.LiftSetoids
open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.NaturalTransformation.Dinatural hiding (_≃_)

import Categories.Morphism.Reasoning as MR

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

module _ {F G : Functor C D} where
  private
    module C = Category C
    module D = Category D
    open D
    open MR D
    open HomReasoning
    open Functor

    F′ : Bifunctor C.op C D
    F′ = F ∘F πʳ

    G′ : Bifunctor C.op C D
    G′ = G ∘F πʳ

  NT⇒Dinatural : NaturalTransformation F G → DinaturalTransformation F′ G′
  NT⇒Dinatural β = dtHelper record
    { α       = η
    ; commute = λ f → ∘-resp-≈ʳ (elimʳ (identity F)) ○ ⟺ (commute f) ○ introˡ (identity G)
    }
    where open NaturalTransformation β

  Dinatural⇒NT : DinaturalTransformation F′ G′ → NaturalTransformation F G
  Dinatural⇒NT θ = ntHelper record
    { η       = α
    ; commute = λ f → introˡ (identity G) ○ ⟺ (commute f) ○ ∘-resp-≈ʳ (elimʳ (identity F))
    }
    where open DinaturalTransformation θ

  replaceˡ : ∀ {F′} → NaturalTransformation F G → F ≃ F′ → NaturalTransformation F′ G
  replaceˡ {F′} α F≃F′ = ntHelper record
    { η       = λ X → η X ∘ ⇐.η X
    ; commute = λ {X Y} f → begin
      (η Y ∘ ⇐.η Y) ∘ F₁ F′ f ≈⟨ pullʳ (⇐.commute f) ⟩
      η Y ∘ F₁ F f ∘ ⇐.η X    ≈⟨ pullˡ (commute f) ○ assoc ⟩
      F₁ G f ∘ η X ∘ ⇐.η X    ∎
    }
    where open NaturalIsomorphism F≃F′
          open NaturalTransformation α

  replaceʳ : ∀ {G′} → NaturalTransformation F G → G ≃ G′ → NaturalTransformation F G′
  replaceʳ {G′} α G≃G′ = ntHelper record
    { η       = λ X → ⇒.η X ∘ η X
    ; commute = λ {X Y} f → begin
      (⇒.η Y ∘ η Y) ∘ F₁ F f ≈⟨ pullʳ (commute f) ⟩
      ⇒.η Y ∘ F₁ G f ∘ η X   ≈⟨ pullˡ (⇒.commute f) ○ assoc ⟩
      F₁ G′ f ∘ ⇒.η X ∘ η X  ∎
    }
    where open NaturalIsomorphism G≃G′
          open NaturalTransformation α  

module _ (F : Bifunctor C D E) where

  -- there is natural transformation between two partially applied bifunctors.

  appˡ-nat : ∀ {X Y} → (f : Category._⇒_ C X Y) → NaturalTransformation (appˡ F X) (appˡ F Y)
  appˡ-nat f = F ∘ˡ (constNat f ※ⁿ idN)

  appʳ-nat : ∀ {X Y} → (f : Category._⇒_ D X Y) → NaturalTransformation (appʳ F X) (appʳ F Y)
  appʳ-nat f = F ∘ˡ (idN ※ⁿ constNat f)

module _ {F G : Bifunctor C D E} (α : NaturalTransformation F G) where
  private
    module C = Category C
    module D = Category D
    module E = Category E

  appˡ′ : ∀ X → NaturalTransformation (appˡ F X) (appˡ G X)
  appˡ′ X = α ∘ₕ idN

  appʳ′ : ∀ X → NaturalTransformation (appʳ F X) (appʳ G X)
  appʳ′ X = α ∘ₕ idN

-- unlift universe level
module _ {c ℓ ℓ′ e} {F G : Functor C (Setoids c ℓ)} (α : NaturalTransformation (LiftSetoids ℓ′ e ∘F F) (LiftSetoids ℓ′ e ∘F G)) where
  open NaturalTransformation α
  open Func

  unlift-nat : NaturalTransformation F G
  unlift-nat = ntHelper record
    { η       = λ X → record
      { to = λ x → lower (to (η X) (lift x))
      ; cong = λ eq → lower (cong (η X) (lift eq))
      }
    ; commute = λ f → lower (commute f)
    }