Cubical.Categories.LocallySmall.Bifunctor.Base

module Cubical.Categories.LocallySmall.Bifunctor.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Sigma.More


open import Cubical.Categories.LocallySmall.Category.Base
open import Cubical.Categories.LocallySmall.Variables
open import Cubical.Categories.LocallySmall.Instances.BinProduct
open import Cubical.Categories.LocallySmall.Functor.Base


open CatIso

record Bifunctor (C : Category Cob CHom-ℓ)
                 (D : Category Dob DHom-ℓ)
                 (E : Category Eob EHom-ℓ)
       : Typeω where
  no-eta-equality
  constructor bifunctor
  private
    module C = CategoryNotation C
    module D = CategoryNotation D
    module E = CategoryNotation E

  field
    Bif-ob : Cob → Dob → Eob
    Bif-hom× : ∀ {c c' d d'} (f : C.Hom[ c , c' ])(g : D.Hom[ d , d' ])
      → E.Hom[ Bif-ob c d , Bif-ob c' d' ]
    Bif-homL : ∀ {c c'} (f : C.Hom[ c , c' ]) d
      → E.Hom[ Bif-ob c d , Bif-ob c' d ]
    Bif-homR : ∀ {d d'} c (g : D.Hom[ d , d' ])
      → E.Hom[ Bif-ob c d , Bif-ob c d' ]
    Bif-×-id : ∀ {c d} → Bif-hom× (C.id {c}) (D.id {d}) ≡ E.id
    Bif-×-seq : ∀ {c c' c'' d d' d''}
      {f : C.Hom[ c , c' ]}{f' : C.Hom[ c' , c'' ]}
      {g : D.Hom[ d , d' ]}{g' : D.Hom[ d' , d'' ]}
      → Bif-hom× (f C.⋆ f') (g D.⋆ g')
        ≡ Bif-hom× f g E.⋆ Bif-hom× f' g'
    Bif-L×-agree : ∀ {c c'} (f : C.Hom[ c , c' ]) d
      → Bif-homL f d ≡ Bif-hom× f D.id
    Bif-R×-agree : ∀ {d d'} c (g : D.Hom[ d , d' ])
      → Bif-homR c g ≡ Bif-hom× C.id g
  Bif-hom×⟨_⟩⟨_⟩ : ∀ {c c' d d'}{f f' g g'}
    (f≡f' : Path C.Hom[ c , c' ] f f')
    (g≡g' : Path D.Hom[ d , d' ] g g')
    → Path E.Hom[ Bif-ob c d , Bif-ob c' d' ] (Bif-hom× f g) (Bif-hom× f' g')
  Bif-hom×⟨ f≡f' ⟩⟨ g≡g' ⟩ = cong₂ Bif-hom× f≡f' g≡g'

  Bif-iso× : ∀ {c c' d d'} (f : C.ISOC.Hom[ c , c' ])(g : D.ISOC.Hom[ d , d' ])
      → E.ISOC.Hom[ Bif-ob c d , Bif-ob c' d' ]
  Bif-iso× f g .fun = Bif-hom× (f .fun) (g .fun)
  Bif-iso× f g .inv = Bif-hom× (f .inv) (g .inv)
  Bif-iso× f g .sec = sym Bif-×-seq ∙ Bif-hom×⟨ f .sec ⟩⟨ g .sec ⟩ ∙ Bif-×-id
  Bif-iso× f g .ret = sym Bif-×-seq ∙ Bif-hom×⟨ f .ret ⟩⟨ g .ret ⟩ ∙ Bif-×-id

open Bifunctor
open Functor

module _
  {C : Category Cob CHom-ℓ}
  {D : Category Dob DHom-ℓ}
  {E : Category Eob EHom-ℓ}
  where
  BifunctorToParFunctor : Bifunctor C D E → Functor (C ×C D) E
  BifunctorToParFunctor F .F-ob = λ z → F .Bif-ob (z .Σω.fst) (z .Σω.snd)
  BifunctorToParFunctor F .F-hom = λ z → F .Bif-hom× (z .fst) (z .snd)
  BifunctorToParFunctor F .F-id = F .Bif-×-id
  BifunctorToParFunctor F .F-seq = λ f g → F .Bif-×-seq

  ParFunctorToBifunctor : Functor (C ×C D) E → Bifunctor C D E
  ParFunctorToBifunctor F .Bif-ob = λ z z₁ → F-ob F (z , z₁)
  ParFunctorToBifunctor F .Bif-hom× = λ f g → F-hom F (f , g)
  ParFunctorToBifunctor F .Bif-homL = λ f d → F-hom F (f , Category.id D)
  ParFunctorToBifunctor F .Bif-homR = λ c g → F-hom F (Category.id C , g)
  ParFunctorToBifunctor F .Bif-×-id = F-id F
  ParFunctorToBifunctor F .Bif-×-seq = F-seq F (_ , _) (_ , _)
  ParFunctorToBifunctor F .Bif-L×-agree f d = refl
  ParFunctorToBifunctor F .Bif-R×-agree g c = refl

  module _ {Cob' CHom-ℓ'}
    {C' : Category Cob' CHom-ℓ'}
    (F : Bifunctor C' D E)
    (G : Functor C C')
    where
    compL : Bifunctor C D E
    compL .Bif-ob = λ z → F .Bif-ob (F-ob G z)
    compL .Bif-hom× = λ f → F .Bif-hom× (F-hom G f)
    compL .Bif-homL = λ f → F .Bif-homL (F-hom G f)
    compL .Bif-homR = λ c → F .Bif-homR (F-ob G c)
    compL .Bif-×-id = cong₂ (F .Bif-hom×) (F-id G) refl ∙ F .Bif-×-id
    compL .Bif-×-seq =
      cong₂ (F .Bif-hom×) (F-seq G _ _) refl
      ∙ F .Bif-×-seq
    compL .Bif-L×-agree = λ f → F .Bif-L×-agree (F-hom G f)
    compL .Bif-R×-agree c g =
      F .Bif-R×-agree (F-ob G c) g
      ∙ cong₂ (F .Bif-hom×) (sym $ F-id G) refl
    infixl 30 compL
    syntax compL F G = F ∘Fl G

  module _ {Dob' DHom-ℓ'}
    {D' : Category Dob' DHom-ℓ'}
    (F : Bifunctor C D' E)
    (G : Functor D D')
    where
    compR : Bifunctor C D E
    compR .Bif-ob = λ z z₁ → F .Bif-ob z (F-ob G z₁)
    compR .Bif-hom× = λ f g → F .Bif-hom× f (F-hom G g)
    compR .Bif-homL = λ f d → F .Bif-homL f (F-ob G d)
    compR .Bif-homR = λ c g → F .Bif-homR c (F-hom G g)
    compR .Bif-×-id = cong₂ (F .Bif-hom×) refl (G .F-id) ∙ F .Bif-×-id
    compR .Bif-×-seq =
      cong₂ (F .Bif-hom×) refl (F-seq G _ _)
      ∙ F .Bif-×-seq
    compR .Bif-L×-agree f d =
      F .Bif-L×-agree f (F-ob G d)
      ∙ cong₂ (F .Bif-hom×) refl (sym $ F-id G)
    compR .Bif-R×-agree = λ c g → F .Bif-R×-agree c (F-hom G g)

    infixl 30 compR
    syntax compR F G = F ∘Fr G

module _
  {C : Category Cob CHom-ℓ}
  {D : Category Dob DHom-ℓ}
  {E : Category Eob EHom-ℓ}
  {Cob' CHom-ℓ'}
  {Dob' DHom-ℓ'}
  {C' : Category Cob' CHom-ℓ'}
  {D' : Category Dob' DHom-ℓ'}
  (F : Bifunctor C' D' E)
  where
  module _ (G : Functor C C') (H : Functor D D') where
    compLR : Bifunctor C D E
    compLR = F ∘Fl G ∘Fr H

  module _ (GH : Σω (Functor C C') λ _ → Functor D D') where
    compLR' : Bifunctor C D E
    compLR' = compLR (GH .Σω.fst) (GH .Σω.snd)

    infixl 30 compLR'
    syntax compLR' F GH = F ∘Flr GH