Opposite category Identity

Stream: mathlib4

[Nicolas Rolland]

Here's a little brain puzzle :

import Mathlib.CategoryTheory.Category.Cat
namespace CategoryTheory
universe v u
variable (B: Cat.{v,u})

def one_Bop_asfctr  := (𝟙 (Bᵒᵖ) : Bᵒᵖ ⥤ Bᵒᵖ )

yields the error

type mismatch
𝟙 (↑B)ᵒᵖ
has type
(↑B)ᵒᵖ ⟶ (↑B)ᵒᵖ : Type ?u.347
but is expected to have type
(↑B)ᵒᵖ ⥤ (↑B)ᵒᵖ : Type (max v u)

---

What are we looking at in the definition ?

𝟙 (Bᵒᵖ) is the identity in Cat, the category of categories, for the object Bᵒᵖ ∈ Cat .
This is 𝟙 with some white in the middle which stands for CategoryStruct.id field in Mathlib/CategoryTheory/Category/Basic.lean

So this is really an arrow of Cat and indeed, this term yields no error

def one_Bop := (𝟙 (Bᵒᵖ) : Bᵒᵖ ⟶ Bᵒᵖ )

Of course the identity in the category Cat is defined to be equal to the identity functor defined by 𝟭 (Bᵒᵖ) and which yields a functor. This is bold 𝟭 with no white in the middle, which stand for Functor.id
in Mathlib/CategoryTheory/Functor/Basic.lean

def id_Bop    := (𝟭 (Bᵒᵖ) : Bᵒᵖ ⥤ Bᵒᵖ )

But for some reason, the identity arrow in Cat for Bᵒᵖ is not the identity functor for Bᵒᵖ, because of this universe thingy.

And of course if we don't op, everything works, the 𝟙 is the 𝟭

def one_B_asfctr := (𝟙 B : B ⥤ B )

[Nicolas Rolland]

PS : is there a way to opt-out of the universe discipline for some section ? the rest of the code would have to trust that the inside of the section has not any paradoxical stuff.

most of the time, universe error message hide some real issue in the code, which has nothing to do with universe.

[Eric Wieser]

You can prove the universes are a distraction by using the same one everywhere:

import Mathlib.CategoryTheory.Category.Cat
namespace CategoryTheory
universe v u
variable (B: Cat.{u,u})

def one_Bop_asfctr  := ((𝟙 (Bᵒᵖ) : Bᵒᵖ ⟶ Bᵒᵖ) : CategoryTheory.Functor.{u,u,u,u} Bᵒᵖ Bᵒᵖ )

[Nicolas Rolland]

Oh good tip. I thought universe were the pb here (!)

So now this boils down to

type mismatch
𝟙 (↑B)ᵒᵖ
has type
(↑B)ᵒᵖ ⟶ (↑B)ᵒᵖ : Type u
but is expected to have type
(↑B)ᵒᵖ ⥤ (↑B)ᵒᵖ : Type u

[Mario Carneiro]

The issue is that the first arrow is an arrow in Type, whereas the functor arrow is defeq to an arrow in Cat

[Mario Carneiro]

This is because Bᵒᵖ is a type, not a category

[Mario Carneiro]

this works:

def one_Bop_asfctr  :=
  ((𝟙 (Cat.of Bᵒᵖ) : Cat.of Bᵒᵖ ⟶ Cat.of Bᵒᵖ) : CategoryTheory.Functor.{u,u,u,u} Bᵒᵖ Bᵒᵖ )