locating instance definitions

Stream: general

[Kevin Buzzard]

I always have a hard time finding instance definitions. Is there some algorithmic approach?

I am working on Scott's enriched branch of mathlib. He's pointed me to some sorrys and I'm trying to fill them in, but I need to learn the library. For definitions I don't know, I just right click. But for type classes I sometimes get stuck. For example, I realised in a file that Type was a monoidal category. I tried

instance fooz : monoidal_category Type := by apply_instance

and it worked, so he's given Type the structure of a monoidal_category, which is a typeclass whose definition I can see. One of the fields of this typeclass is tensor_unit. So I now want to see the definition of tensor_unit in fooz because I want to know the definition of this field for Type. I try this:

definition fooz: monoidal_category Type := by apply_instance
#print fooz

and I find

def Module.fooz : monoidal_category Type :=
concrete_monoidal_category.to_monoidal_category Type

OK great. So now I discover there is a new class concrete_monoidal_category C. I can find the definition, and see it extends concrete_category C and monoidal_category C. I then try this:

def barz : concrete_monoidal_category Type := by apply_instance

#print barz

and I see

def Module.barz : concrete_monoidal_category Type :=
category_theory.concrete_monoidal_category

and now the trail has basically run dry.

There must be a better way to do this. It is not specifically this question I'm interested in -- this is most definitely not the first time this has happened to me. I'd like to be able to get to the bottom of these things myself instead of having to ask.

[Reid Barton]

I don't understand yet why the trail has run dry. What is category_theory.concrete_monoidal_category? If you #check category_theory.concrete_monoidal_category and use jump to definition on it, where does it take you?

[Kevin Buzzard]

I guess another approach would be this:

#check monoidal_category.tensor_unit Type
-- 𝟙_ Type : Type

(the funny 1 is just notation). I want to know what term this unfolds to, ideally by just looking at the code. I was expecting it to be unit but example : monoidal_category.tensor_unit Type = unit := rfl fails

[Reid Barton]

Well, I would guess punit next

[Reid Barton]

But I know it's not your real question

[Kevin Buzzard]

That was the other thing I tried and it was when that failed that I started on the typeclass woozle-hunt.

[Johan Commelin]

Aaah, that's another thing we can fix in Lean 3.8. unit should be punit : Type

[Reid Barton]

Ah, is the problem somehow that the information you need is in an implicit argument of category_theory.concrete_monoidal_category?
I haven't looked at the code, but so far I am as confused as you

[Kevin Buzzard]

It might be a universe issue but I thought it would be easier to look than to guess.

[Kevin Buzzard]

I don't understand why the code compiles:

instance : concrete_monoidal_category (Type u) :=
{ lax_monoidal := category_theory.lax_monoidal_id }

[Kevin Buzzard]

class concrete_monoidal_category (C : Type (u+1)) extends concrete_category.{u} C, monoidal_category.{u} C :=
(lax_monoidal : lax_monoidal.{u u} (concrete_category.forget C).obj)

I am surprised there is no ..[the stuff I want to see] in the definition

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/monoidal/types.lean

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/monoidal/of_has_finite_products.lean

[Kevin Buzzard]

boggle so it's terminal Type?

[Johan Commelin]

Yup...

[Johan Commelin]

I would hope that is (p)unit

[Chris Hughes]

Isn't terminal Type defined to be punit?

[Kevin Buzzard]

I still don't see why the code compiles.

[Kevin Buzzard]

That instance definition doesn't seem to give enough fields, or any indication as to where the extra fields are coming from.

[Kevin Buzzard]

class concrete_category (C : Type (u+1)) extends category.{u} C :=
(forget : C ⥤ Type u)
[forget_faithful : faithful forget]
end prio

Those fields are all missing in the instance definition.

[Kevin Buzzard]

There is some wizardry going on.

[Chris Hughes]

Or does terminal Type come from some has_limits definition, so I'm guessing pempty -> pempty

[Kevin Buzzard]

Chris do you understand how that instance code can possibly compile when not all fields are defined?

[Johan Commelin]

Fields of the form [foobar X] are filled in by typeclass search. You don't need to give them.

[Kevin Buzzard]

But forget is not marked in that way.

[Johan Commelin]

Fields of the form (foobar X . obviously) are filled in by tidy. You hopefully don't need to give them.

[Kevin Buzzard]

But forget doesn't have the obviously autoparam either.

[Johan Commelin]

Hmmm,... where is this definition that you are talking about?

[Johan Commelin]

Aaah, found it

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/bc36a65c8da72345bdae5af67eec1c11dd62f680/src/category_theory/enriched/examples.lean#L12

[Kevin Buzzard]

I was just playing with this sorry, figuring out what it actually said etc.

[Kevin Buzzard]

and the goal for that first sorry is ⊢ 𝟙_ Type ⟶ (concrete_category.forget (Module ℤ)).obj (𝟙_ (Module ℤ))

[Johan Commelin]

Maybe unification takes care of all the other fields?

[Kevin Buzzard]

and I just got interested in the definition of 𝟙_ Type

[Kevin Buzzard]

I'm very impressed if type class unification can solve faithful ?m_1 and then unification can solve ?m_1!

[Kevin Buzzard]

Oh -- but perhaps unification can solve it first.

[Kevin Buzzard]

Probably this is not even the right question (the actual definition of the term), but I was surprised I couldn't answer it by inspecting the code.

[Kevin Buzzard]

The definition of the map should be done just using the universal properties of the term.

[Kevin Buzzard]

example : monoidal_category.tensor_unit Type = limits.terminal Type := rfl btw

[Kevin Buzzard]

ε := λ _, 0, :tada:

[Kevin Buzzard]

and we will never know the definition of the source :-)