{-# OPTIONS --without-K --safe #-}
 
-- Bifunctor, aka a Functor from C × D to E
module Categories.Functor.Bifunctor where
 
open import Level
open import Data.Product using (_,_)
 
open import Categories.Category
open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.Category.Product
 
private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ o⁗ ℓ⁗ e⁗ : Level
    C D E A B : Category o ℓ e
 
Bifunctor : Category o ℓ e → Category o′ ℓ′ e′ → Category o″ ℓ″ e″ → Set _
Bifunctor C D E = Functor (Product C D) E
 
module Bifunctor (H : Bifunctor C D E) where
  open Functor H public
 
  overlap-× : ∀ (F : Functor A C) (G : Functor A D) → Functor A E
  overlap-× F G = H ∘F (F ※ G)
 
  reduce-× : ∀ (F : Functor A C) (G : Functor B D) → Bifunctor A B E
  reduce-× F G = H ∘F (F ⁂ G)
 
  flip : Bifunctor D C E
  flip = H ∘F Swap
 
  appˡ : Category.Obj C → Functor D E
  appˡ c = H ∘F constˡ c
 
  appʳ : Category.Obj D → Functor C E
  appʳ d = H ∘F constʳ d
 
  ₁ˡ : ∀ {A B d} (f : C [ A , B ]) → E [ F₀ (A , d) , F₀ (B , d) ]
  ₁ˡ f = ₁ (f , Category.id D)
 
  ₁ʳ : ∀ {A B c} (f : D [ A , B ]) → E [ F₀ (c , A) , F₀ (c , B) ]
  ₁ʳ f = ₁ (Category.id C , f)
 
  homomorphismˡ : ∀ {X Y Z d} {f : C [ X , Y ]} {g : C [ Y , Z ]} →
                     E [ ₁ˡ {d = d} (C [ g ∘ f ]) ≈ E [ ₁ˡ g ∘ ₁ˡ f ] ]
  homomorphismˡ = trans E
      (F-resp-≈ (refl C , sym D (Category.identity² D)))
      homomorphism
    where open Category.Equiv
 
  homomorphismʳ : ∀ {X Y Z c} {f : D [ X , Y ]} {g : D [ Y , Z ]} →
                     E [ ₁ʳ {c = c} (D [ g ∘ f ]) ≈ E [ ₁ʳ g ∘ ₁ʳ f ] ]
  homomorphismʳ = trans E
      (F-resp-≈ (sym C (Category.identity² C) , refl D))
      homomorphism
    where open Category.Equiv
 
  resp-≈ˡ : ∀ {A B d} {f g : C [ A , B ]} → C [ f ≈ g ] →
               E [ ₁ˡ {d = d} f ≈ ₁ˡ g ]
  resp-≈ˡ f≈g = F-resp-≈ (f≈g , Category.Equiv.refl D)
 
  resp-≈ʳ : ∀ {A B c} {f g : D [ A , B ]} → D [ f ≈ g ] →
               E [ ₁ʳ {c = c} f ≈ ₁ʳ g ]
  resp-≈ʳ f≈g = F-resp-≈ (Category.Equiv.refl C , f≈g)
 
open Bifunctor public using (appˡ; appʳ) renaming (flip to flip-bifunctor)
 
overlap-× : ∀ (H : Bifunctor C D E) (F : Functor A C) (G : Functor A D) → Functor A E
overlap-× H = Bifunctor.overlap-× H
 
reduce-× : ∀ (H : Bifunctor C D E) (F : Functor A C) (G : Functor B D) -> Bifunctor A B E
reduce-× H = Bifunctor.reduce-× H