custom syntax extension for categories

Stream: mathlib4

[Nicolas Rolland]

Very often, most of what is written in category is low level operation which some syntax transformers could apply.

We enjoy added smart in the language for function : we have automatic currying when we partially apply a function, we define function pointwise without thinking etc...

The following example is super readable with "smart syntax", but hard to read after all the explicit symbol pushing.

Can similar smarts be applied for categories, say with lean metaprogramming facilities ?

import Mathlib.CategoryTheory.Functor.Currying
import Mathlib.CategoryTheory.Functor.Hom

namespace CategoryTheory.Distributors
abbrev Dist.{u, v₂, u₂, v₁, u₁} (A : Type u₁) [Category.{v₁} A] (B : Type u₂ ) [Category.{v₂} B] := Bᵒᵖ × A ⥤ Type u
universe u
variable {A : Type u } [Category.{u} A]
variable {B : Type u } [Category.{u} B]
variable {C : Type u } [Category.{u} C]
variable {D : Type u } [Category.{u} D]

def opFunctor  :  (A ⥤ B)ᵒᵖ ⥤ (Aᵒᵖ ⥤ Bᵒᵖ)  where -- utility
  obj f := Functor.op (Opposite.unop f)
  map {fop gop : (A ⥤ B)ᵒᵖ} (nop : fop ⟶ gop) := {
    app := fun ao =>  Opposite.op ((Opposite.unop nop).app (Opposite.unop ao))
    naturality := fun _ _ uo => congrArg Quiver.Hom.op ((nop.unop.naturality uo.unop).symm) }

def prodFunctor : (A ⥤ B) × (C ⥤ D) ⥤ A × C ⥤ B × D where -- utility
  obj FG := FG.1.prod FG.2
  map nm :=  NatTrans.prod nm.1 nm.2


-- What I have to write

def phi_ : (A ⥤ B) ⥤ Dist A B  :=
  (curry.obj prodFunctor).obj (𝟭 Bᵒᵖ) ⋙ (whiskeringRight _ _ _ ).obj (Functor.hom B)

def _phi : (A ⥤ B)ᵒᵖ ⥤  Dist B A :=
  opFunctor ⋙ (curry.obj (Prod.swap _ _ ⋙ prodFunctor )).obj (𝟭 B) ⋙
    (whiskeringRight _ _ _ ).obj (Functor.hom B)


-- What I want to write

def phi_' : (A ⥤ B) ⥤ Dist A B    :=
  prodFunctor ((𝟭 Bᵒᵖ), (·)) ⋙ Functor.hom B

def _phi' : (A ⥤ B)ᵒᵖ ⥤  Dist B A :=
  opFunctor ⋙ prodFunctor ((·), (𝟭 B))  ⋙ Functor.hom B


end CategoryTheory.Distributors

[Kim Morrison]

There is src#CategoryTheory.Functorial.

[Kim Morrison]

And in particular Functor.of. It's possible that with some additional instances you could get what you want.

[Kim Morrison]

You would have to write Functor.of (... object level function...), but we could add some syntax sugar to help with that.

[Kim Morrison]

(Adding @Nicolas Rolland since it is an old thread.)