CategoryTheory.Functor.flipFunctor

Stream: mathlib4

[Edison Xie]

import Mathlib

namespace  CategoryTheory

def Functor.flipFunctor {C D E : Type*} [Category C] [Category D] [Category E] :
    (C ⥤ D ⥤ E) ⥤ (D ⥤ C ⥤ E) where
  obj F := F.flip
  map {X Y} f := {
    app M := {
      app N := (f.app N).app M
      naturality {X' Y'} f' := by
        dsimp
        rw [← NatTrans.comp_app, ← NatTrans.comp_app]
        congr 1
        exact f.naturality _
    }
    naturality {X' Y'} f' := by
      ext M
      dsimp [NatTrans.comp_app]
      exact (f.app M).naturality _
  }

end CategoryTheory

Do we have this in mathlib? It's pretty weird that we have CategoryTheory.Functor.flip₁₃Functor but not this

[Edison Xie]

@Andrew Yang @Joël Riou

[Andrew Yang]

docs#CategoryTheory.flipFunctor

[Edison Xie]

wait but this name is weird, we have Functor.flip, Functor.flip₁₃Functor but suddennly it's CategoryTheory.flipFunctor?

[Andrew Yang]

I would personally say Functor.flip₁₃Functor is the weird one.

[Andrew Yang]

Because it says Functor twice.

[Edison Xie]

hmmmm okay