open import Cat.Functor.Naturality
open import Cat.Instances.Product
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cat

open _=>_

module Cat.Functor.Bifunctor where

BifunctorsπŸ”—

private
  variable
    o h o₁ h₁ oβ‚‚ hβ‚‚ o₃ h₃ : Level
    C D E : Precategory o₁ h₁
  module Cat[,] {o h o₁ h₁} {C : Precategory o h} {D : Precategory o₁ h₁} = Cat Cat[ C , D ]

A bifunctor from and to is a functor of two arguments. Traditionally, a bifunctor is defined as having its domain be a product category, so that would have type In those terms, a bifunctor acts on both of its arguments simultaneously, having a single action _β—†_ on morphisms.

For technical reasons, we instead prefer to define bifunctors with a functor category in their codomain, so that In these terms, we can evaluate at an object to get a functor and evaluating this at gives the action of on a pair of objects. The action of on a morphism behaves as a β€œwhiskering” operator, being a map which varies the second parameter, leaving fixed. The action of on a morphism is a natural transformation whose components, having type generate the complementary whiskering operation.

Bifunctor : Precategory o h β†’ Precategory o₁ h₁ β†’ Precategory oβ‚‚ hβ‚‚ β†’ Type _
Bifunctor C D E = Functor C Cat[ D , E ]

{-# DISPLAY Functor {o} {β„“} {_} {_} C (Cat[_,_] {o₁} {ℓ₁} {oβ‚‚} {β„“β‚‚} D E) = Bifunctor {o} {β„“} {o₁} {ℓ₁} {oβ‚‚} {β„“β‚‚} C D E #-}

module Bifunctor (F : Bifunctor C D E) where
  private
    module C = Precategory C
    module D = Precategory D
    module E = Cat E
    variable
      a b c d : ⌞ C ⌟
      w x y z : ⌞ D ⌟
More on the technical reasons.

The mechanism Mikan uses for reifying normal forms for display to the user favours definitions that can be written entirely in terms of the module system. If we defined bifunctors with a product argument, the joint action on morphisms would be disqualified from being written infix, since the module system provides no facility for currying a function.

  private
    open module rβ‚€ X = Functor (F .Functor.Fβ‚€ X) public
      renaming (F₁ to infix 35 _β–Ά_) using (Fβ‚€)

    open module r₁ {a b} (f : C.Hom a b) = _=>_ (F .Functor.F₁ f) public
      renaming (Ξ· to infix 35 _β—€_) using ()

Publicly opening private module aliases ensures that only the symbols Fβ‚€, _β—€_, and _β–Ά_ are in scope, but not the intermediate modules rβ‚€ and r₁, ensuring that a term like f β—€ A will not be recovered as f r₁.β—€ A.

The rest of this module contains helpers for working with the two functorial actions. First, we write two little helper functions that allow eliding the β€œunchanging” argument of the whiskerings. The names lmap and rmap are named left and right after the direction of the triangles _β—€_ and _β–Ά_.

  lmap : C.Hom a b β†’ E.Hom (Fβ‚€ a x) (Fβ‚€ b x)
  lmap f = f β—€ _

  rmap : D.Hom x y β†’ E.Hom (Fβ‚€ a x) (Fβ‚€ a y)
  rmap f = _ β–Ά f

These operations are both functorial by themselves. For rmap, we show this by projecting from the functor For lmap, functoriality of gives us a path of natural transformations, so we must project the identity between the underlying maps as an additional step.

  rmap-id : a β–Ά D.id {x} ≑ E.id
  rmap-∘  : (f : D.Hom y z) (g : D.Hom x y) β†’ a β–Ά (f D.∘ g) ≑ (a β–Ά f) E.∘ (a β–Ά g)

  rmap-id = F .Functor.Fβ‚€ _ .Functor.F-id
  rmap-∘  = F .Functor.Fβ‚€ _ .Functor.F-∘

  lmap-id : C.id {a} β—€ x ≑ E.id
  lmap-∘  : (f : C.Hom b c) (g : C.Hom a b) β†’ (f C.∘ g) β—€ x ≑ (f β—€ x) E.∘ (g β—€ x)

  lmap-id    = F .Functor.F-id     Β·β‚š _
  lmap-∘ f g = F .Functor.F-∘  f g Β·β‚š _

Finally, the naturality squares for each pictured below, show that lmap and rmap commute past eachother.

  lrmap : βˆ€ f g β†’ (f β—€ y) E.∘ (a β–Ά g) ≑ (b β–Ά g) E.∘ (f β—€ x)
  lrmap f g = F .Functor.F₁ f .is-natural _ _ g

  rlmap : βˆ€ g f β†’ (b β–Ά g) E.∘ (f β—€ x) ≑ (f β—€ y) E.∘ (a β–Ά g)
  rlmap f g = sym (lrmap g f)

Horizontal compositionπŸ”—

A bifunctor provides two identical, but not definitionally equal, ways of acting on both coordinates. For definiteness, we define the horizontal composition operation to be the left-hand-side of lrmap.

  _β—†_ : βˆ€ {a b x y} β†’ C.Hom a b β†’ D.Hom x y β†’ E.Hom (F Β· a Β· x) (F Β· b Β· y)
  _β—†_ Ξ² Ξ± = (Ξ² β—€ _) E.∘ (_ β–Ά Ξ±)

A pair of short calculations shows that this operation is β€œfunctorial in both variables”.

  β—†-id : βˆ€ {a x} β†’ C.id {a} β—† D.id {x} ≑ E.id
  β—†-id =
    C.id β—† D.id               β‰‘βŸ¨βŸ©
    (C.id β—€ _) E.∘ (_ β–Ά D.id) β‰‘βŸ¨ E.eliml lmap-id βŸ©β‰‘
    _ β–Ά D.id                  β‰‘βŸ¨ rmap-id βŸ©β‰‘
    E.id                      ∎

  β—†-∘
    : βˆ€ {a b c x y z}
    β†’ {f : C.Hom b c} {g : C.Hom a b} {f' : D.Hom y z} {g' : D.Hom x y}
    β†’ (f C.∘ g) β—† (f' D.∘ g') ≑ (f β—† f') E.∘ (g β—† g')
  β—†-∘ {f = f} {g} {f'} {g'} =
    (f C.∘ g) β—† (f' D.∘ g')                         β‰‘βŸ¨βŸ©
    (f C.∘ g β—€ _) E.∘ (_ β–Ά f' D.∘ g')               β‰‘βŸ¨ apβ‚‚ E._∘_ (lmap-∘ _ _) (rmap-∘ _ _) βŸ©β‰‘
    ((f β—€ _) E.∘ (g β—€ _)) E.∘ (_ β–Ά f') E.∘ (_ β–Ά g') β‰‘βŸ¨ E.extendr (E.extendl (lrmap _ _)) βŸ©β‰‘
    ((f β—€ _) E.∘ (_ β–Ά f')) E.∘ (g β—€ _) E.∘ (_ β–Ά g') β‰‘βŸ¨βŸ©
    (f β—† f') E.∘ (g β—† g')                           ∎

As special cases of functoriality, we recover the whiskerings as a special case of horizontal composition.

  lmap-β—† : βˆ€ {a b x} (f : C.Hom a b) β†’ f β—€ x ≑ f β—† D.id
  lmap-β—† f = E.intror rmap-id

  rmap-β—† : βˆ€ {x y a} (f : D.Hom x y) β†’ a β–Ά f ≑ C.id β—† f
  rmap-β—† f = E.introl lmap-id

Associated functorsπŸ”—

Evaluating at an object gives a functor by definition. Since this functor acts by rmap, we call this the functor associated to on the Right.

  Right : C.Ob β†’ Functor D E
  Right A = F .Functor.Fβ‚€ A

In the other direction, we must write out the functor associated to on the Left, given an object in components.

  Left : D.Ob β†’ Functor C E
  Left X .Functor.Fβ‚€ A = Fβ‚€ A X
  Left X .Functor.F₁ f = f β—€ X
  Left X .Functor.F-id = lmap-id
  Left X .Functor.F-∘  = lmap-∘

  module β–Ά {A} = Fr (Right A) hiding (Fβ‚€ ; F₁)
  module β—€ {A} = Fr (Left A)  hiding (Fβ‚€ ; F₁)

By swapping the positions of lmap and rmap, we can turn a bifunctor of and to into a bifunctor of and to 

module _ {C : Precategory o h} {D : Precategory o₁ h₁} {E : Precategory oβ‚‚ hβ‚‚} where
  private
    module C = Precategory C
    module D = Precategory D
    module E = Precategory E

  record Make-bifunctor : Type (o βŠ” o₁ βŠ” oβ‚‚ βŠ” h βŠ” h₁ βŠ” hβ‚‚) where
    field
      Fβ‚€   : ⌞ C ⌟ β†’ ⌞ D ⌟ β†’ ⌞ E ⌟
      lmap : βˆ€ {a b x} β†’ C.Hom a b β†’ E.Hom (Fβ‚€ a x) (Fβ‚€ b x)
      rmap : βˆ€ {x y a} β†’ D.Hom x y β†’ E.Hom (Fβ‚€ a x) (Fβ‚€ a y)

      lmap-id : βˆ€ {a x} β†’ lmap {a} {x = x} C.id ≑ E.id
      rmap-id : βˆ€ {x a} β†’ rmap {x} {a = a} D.id ≑ E.id

      lmap-∘
        : βˆ€ {a b c x} (f : C.Hom b c) (g : C.Hom a b)
        β†’ lmap {x = x} (f C.∘ g) ≑ lmap f E.∘ lmap g

      rmap-∘
        : βˆ€ {x y z a} (f : D.Hom y z) (g : D.Hom x y)
        β†’ rmap {a = a} (f D.∘ g) ≑ rmap f E.∘ rmap g

      lrmap
        : βˆ€ {a b x y} (f : C.Hom a b) (g : D.Hom x y)
        β†’ lmap f E.∘ rmap g ≑ rmap g E.∘ lmap f

  make-bifunctor : Make-bifunctor β†’ Bifunctor C D E
  {-# INLINE make-bifunctor #-}
  make-bifunctor mm =
    record
      { Fβ‚€   = Ξ» x β†’ record
        { Fβ‚€   = mm.Fβ‚€ x
        ; F₁   = mm.rmap
        ; F-id = mm.rmap-id
        ; F-∘  = mm.rmap-∘
        }
      ; F₁   = Ξ» x β†’ record
        { Ξ·          = Ξ» _     β†’ mm.lmap x
        ; is-natural = Ξ» x y z β†’ mm.lrmap _ _
        }
      ; F-id = ext Ξ» _ β†’ mm.lmap-id
      ; F-∘  = Ξ» f g β†’ ext Ξ» _ β†’ mm.lmap-∘ _ _
      }
    where module mm = Make-bifunctor mm

module _ (F : Bifunctor C D E) where
  private open module F = Bifunctor F
  open Functor

  -- Defining Flip in components instead of using make-bifunctor avoids
  -- introducing a new "Flip.Right" which is distinct from Left.
  --
  -- This is basically the only avoidable case of generativity.

  Flip : Bifunctor D C E
  Flip .Fβ‚€ = Left

  Flip .F₁ f .Ξ· A              = A β–Ά f
  Flip .F₁ f .is-natural x y g = rlmap _ _

  Flip .F-id    = ext Ξ» _ β†’ rmap-id
  Flip .F-∘ f g = ext Ξ» _ β†’ rmap-∘ _ _

Finally, we can Uncurry into a functor using the horizontal composition defined above.

  Uncurry : Functor (C Γ—αΆœ D) E
  Uncurry .Fβ‚€      = uncurry F.Fβ‚€
  Uncurry .F₁      = uncurry _β—†_
  Uncurry .F-id    = β—†-id
  Uncurry .F-∘ _ _ = β—†-∘

module
  _ {o₁ h₁ oβ‚‚ hβ‚‚ o₃ h₃ : _}
  {C : Precategory o₁ h₁}
  {D : Precategory oβ‚‚ hβ‚‚}
  {E : Precategory o₃ h₃}
  {F G : Bifunctor C D E}
  where

  private
    module C = Precategory C
    module D = Precategory D
    module E = Cat E
    variable
      a b c d : ⌞ C ⌟
      w x y z : ⌞ D ⌟
    module F = Bifunctor F
    module G = Bifunctor G

    open _=>_

  module Binatural (eta : F => G) where
    abstract
      natural-β—€ : βˆ€ {f : C.Hom a b} {x} β†’ eta Β· _ Β· _ E.∘ (f F.β—€ x) ≑ (f G.β—€ x) E.∘ eta Β· _ Β· _
      natural-β—€ = eta .is-natural _ _ _ Ξ·β‚š _

      natural-β–Ά : βˆ€ {a} {f : D.Hom x y} β†’ eta Β· _ Β· _ E.∘ (a F.β–Ά f) ≑ (a G.β–Ά f) E.∘ eta Β· _ Β· _
      natural-β–Ά = eta .Ξ· _ .is-natural _ _ _

      natural-β—†
        : βˆ€ {f : C.Hom a b} {g : D.Hom x y}
        β†’ eta Β· _ Β· _ E.∘ (f F.β—† g) ≑ (f G.β—† g) E.∘ eta Β· _ Β· _
      natural-β—† = E.pulll natural-β—€ βˆ™ E.extendr natural-β–Ά

    private
      open module eta₁ a = _=>_ (eta .Ξ· a) public

    right : βˆ€ {x} β†’ F.Right x => G.Right x
    right = eta .Ξ· _

    left : βˆ€ {x} β†’ F.Left x => G.Left x
    left .Ξ·              x = eta .Ξ· _ .Ξ· _
    left .is-natural x y f = natural-β—€

  open Binatural using (natural-β—€ ; natural-β–Ά ; natural-β—†) public

  biisoβ†’isoⁿ
    : (i : βˆ€ x y β†’ F Β· x Β· y E.β‰… G Β· x Β· y)
    β†’ (βˆ€ {x y z} (f : C.Hom x y) β†’ (f G.β—€ z) E.∘ i x z .E.to ≑ i y z .E.to E.∘ (f F.β—€ z))
    β†’ (βˆ€ {x y z} (f : D.Hom x y) β†’ (z G.β–Ά f) E.∘ i z x .E.to ≑ i z y .E.to E.∘ (z F.β–Ά f))
    β†’ F Cat[,].β‰… G
  {-# INLINE biisoβ†’isoⁿ #-}
  biisoβ†’isoⁿ i n1 n2 = isoβ†’isoⁿ
    (Ξ» x β†’ isoβ†’isoⁿ (i x) Ξ» {x y} f β†’ n2 f)
    Ξ» {x y} f β†’ ext (Ξ» z β†’ n1 f)

  record Make-binatural : Type (o₁ βŠ” oβ‚‚ βŠ” h₁ βŠ” hβ‚‚ βŠ” h₃) where
    field
      Ξ· : (c : C.Ob) β†’ (d : D.Ob) β†’ E.Hom (F.Fβ‚€ c d) (G.Fβ‚€ c d)
      is-natural-β—€
        : βˆ€ {c1 c2 : C.Ob} (f : C.Hom c1 c2) (d : D.Ob)
        β†’ Ξ· c2 d E.∘ (f F.β—€ d) ≑ (f G.β—€ d) E.∘ Ξ· c1 d
      is-natural-β–Ά
        : βˆ€ (c : C.Ob) {d1 d2 : D.Ob} (f : D.Hom d1 d2)
        β†’ Ξ· c d2 E.∘ (c F.β–Ά f) ≑ (c G.β–Ά f) E.∘ Ξ· c d1

  make-binatural : Make-binatural β†’ F => G
  {-# INLINE make-binatural #-}
  make-binatural mk =
    record
    { Ξ· = Ξ» x β†’ record
      { Ξ· = Ξ» y β†’ mk.Ξ· x y
      ; is-natural = Ξ» y z f β†’ mk.is-natural-β–Ά x f
      }
    ; is-natural = Ξ» x y f β†’ ext Ξ» z β†’ mk.is-natural-β—€ f z
    }
    where module mk = Make-binatural mk