Dinatural.agda

open import Level
open import Data.Product

open import Categories.Category
open import Categories.NaturalTransformation as NT
open import Categories.Functor
open import Categories.Functor.Bifunctor
open import Categories.Category.Product
import Categories.Square as Square

private
  variable
    o ℓ e : Level
    C D   : Category o ℓ e
    F G H : Bifunctor (Category.op C) C D

record DinaturalTransformation (F G : Bifunctor (Category.op C) C D) : Set (levelOf C ⊔ levelOf D) where
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G

  open D hiding (op)
  open HomReasoning
  open Commutation

  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)
                ⟩

  op : DinaturalTransformation G.op F.op
  op = record
    { α       = α
    ; commute = λ f → assoc ○ ⟺ (commute f) ○ ⟺ assoc
    }

_<∘_ : NaturalTransformation G H → DinaturalTransformation F G → DinaturalTransformation F H
_<∘_ = {!!}