# Zulip Chat Archive

## Stream: maths

### Topic: weird type class issue

#### Johan Commelin (Oct 18 2018 at 07:44):

Consider this code:

import category_theory.category open category_theory universes u u₁ u₂ v v₁ v₂ w w₁ w₂ variables {C : Type u₁} [𝒞 : category.{u₁ u₂} C] --[@has_limits.{u₁ u₂} C 𝒞] include 𝒞 -- todo should this be done as a subfunctor? structure covering_family (U : C) := (I : Type u₂) (obj : I → C) (hom : Π {i : I}, obj i ⟶ U) #print covering_family structure coverage := (covers : Π {U : C}, set (covering_family U)) -- red squiggles under "covering_family"

I get the following error:

failed to synthesize type class instance for C : Type u₁, 𝒞 : category C, C : Type u₁, 𝒞 : category C, U : C ⊢ category C

#### Johan Commelin (Oct 18 2018 at 07:45):

Why are `C`

and the category structure duplicated there? And why can't it resolve the type class issue?

#### Johannes Hölzl (Oct 18 2018 at 07:46):

what happens if you remove the `include`

and write the variables directly as parameters for `coverage`

?

#### Johan Commelin (Oct 18 2018 at 07:47):

These includes are all over the place in Scott's library. If you remove it you get red squiggles under the `⟶`

in `obj i ⟶ U`

.

#### Johan Commelin (Oct 18 2018 at 07:49):

def coverage := Π {U : C}, set (covering_family U)

gives the error

failed to synthesize type class instance for C : Type u₁, 𝒞 : category C, U : C ⊢ category C

So now the duplication is gone. But it still can't resolve the type class...

#### Johan Commelin (Oct 18 2018 at 07:50):

The following works but is very ugly.

def coverage := Π {U : C}, set (@covering_family _ 𝒞 U)

#### Johan Commelin (Oct 18 2018 at 11:20):

In general I think the fact that we need `include 𝒞`

all the time is a sign that something is wrong. But I have no clue what is wrong and how to fix it.

#### Reid Barton (Oct 18 2018 at 12:45):

I usually include the universe parameters when I run into this kind of issue, like `covering_family.{u\1 u\2}`

. (BTW, usually we use a `v`

-type letter for the morphism universe.)

I have no idea about the duplicate display in the error message though.

#### Johan Commelin (Oct 18 2018 at 12:56):

I currently have

import category_theory.examples.topological_spaces import category_theory.opposites import category_theory.yoneda import category_theory.limits.equalizers import category_theory.limits.products open category_theory universes u u₁ u₂ v v₁ v₂ w w₁ w₂ namespace category_theory.limits variables {C : Type u₁} [𝒞 : category.{u₁ u₂} C] include 𝒞 variables [has_coequalizers.{u₁ u₂} C] {Y Z : C} (f g : Y ⟶ Z) def coequalizer.cofork := has_coequalizers.coequalizer.{u₁ u₂} f g def coequalizer := (coequalizer.cofork f g).X def coequalizer.π : Z ⟶ (coequalizer f g) := (coequalizer.cofork f g).π @[search] def coequalizer.w : f ≫ (coequalizer.π f g) = g ≫ (coequalizer.π f g) := (coequalizer.cofork f g).w def coequalizer.universal_property : is_coequalizer (coequalizer.cofork f g) := has_coequalizers.is_coequalizer.{u₁ u₂} C f g def coequalizer.desc (P : C) (h : Z ⟶ P) (w : f ≫ h = g ≫ h) : coequalizer f g ⟶ P := (coequalizer.universal_property f g).desc { X := P, π := h, w := w } @[extensionality] lemma coequalizer.hom_ext {Y Z : C} {f g : Y ⟶ Z} {X : C} (h k : coequalizer f g ⟶ X) (w : coequalizer.π f g ≫ h = coequalizer.π f g ≫ k) : h = k := begin let s : cofork f g := ⟨ ⟨ X ⟩, coequalizer.π f g ≫ h ⟩, have q := (coequalizer.universal_property f g).uniq s h, have p := (coequalizer.universal_property f g).uniq s k, rw [q, ←p], solve_by_elim, refl end end category_theory.limits section presheaf open category_theory.limits variables (X : Type u₁) [𝒳 : category.{u₁ v₁} X] (C : Type u₂) [𝒞 : category.{u₂ v₂} C] include 𝒳 𝒞 def presheaf := Xᵒᵖ ⥤ C variables {X} {C} instance : category (presheaf X C) := by unfold presheaf; apply_instance omit 𝒞 instance : has_coproducts (presheaf X (Type v₂)) := sorry #print presheaf.category_theory.category end presheaf -- todo should this be done as a subfunctor? structure covering_family {X : Type u₁} [category.{u₁ v₁} X] (U : X) := (index : Type v₁) (obj : index → X) (hom : Π (i : index), obj i ⟶ U) namespace covering_family open category_theory.limits variables {X : Type u₁} [𝒳 : category.{u₁ v₁} X] include 𝒳 variables {U : X} def sieve (f : covering_family U) : presheaf X (Type v₁) := @coequalizer _ _ (sorry) (@Sigma _ _ _ (f.index × f.index) (λ p, _)) (@Sigma _ _ _ f.index (((yoneda X) : X → presheaf X (Type v₁)) ∘ f.obj)) _ _ def sheaf_condition (f : (covering_family U)) {C : Type u₂} [category.{u₂ v₂} C] (F : presheaf X C) : Prop := sorry end covering_family structure coverage {X : Type u₁} [category.{u₁ u₂} X] := (covers : Π (U : X), set (covering_family U)) (property : ∀ {U V : X} (g : V ⟶ U) (f : (covering_family U)), ∃ h : (covering_family V), ∀ j : h.index, ∃ {i : f.index} {k : h.obj j ⟶ f.obj i}, h.hom j ≫ g = k ≫ f.hom i) class site (X : Type u₁) extends category.{u₁ u₂} X := (coverage : @coverage X (by assumption)) section sheaf variables (X : Type u₁) [𝒳 : site.{u₁ v₁} X] (C : Type u₂) [𝒞 : category.{u₂ v₂} C] include 𝒳 𝒞 structure sheaf := (presheaf : presheaf X C) (sheaf_condition : ∀ {U : X} (f : (@covering_family _ 𝒳.to_category U)), f.sheaf_condition presheaf) end sheaf namespace topological_space variables {X : Type u} [topological_space X] instance : site (opens X) := { coverage := { covers := λ U, λ Us, begin sorry -- the union of the Ui should be U end, property := sorry } } end topological_space

Lean is especially unhappy about the part where I try to define the `sieve`

.

#### Johan Commelin (Oct 18 2018 at 12:56):

Currently I'm just going to wait till some PR's get merged.

#### Reid Barton (Oct 18 2018 at 13:05):

Lots of those `_`

s in sieve still need to be filled in, right?

#### Reid Barton (Oct 18 2018 at 13:05):

Or at least... 3 I guess?

#### Johan Commelin (Oct 18 2018 at 13:14):

Yes, that is right. But I need fibre products for the for the `_`

in the first `Sigma`

. :sad:

#### Reid Barton (Oct 18 2018 at 13:36):

In general I think the fact that we need

`include 𝒞`

all the time is a sign that something is wrong. But I have no clue what is wrong and how to fix it.

So there are two issues which come up a lot due to the way category theory uses universe variables.

1. The `include 𝒞`

thing is a workaround for a specific elaborator bug where it doesn't correctly account for universe parameters of variables that have been included by the "square bracket rule". If you hit this bug then you will see an error about something like "bad tactic or buggy elaborator".

2. It also often happens that you have to help Lean out with some explicit universe parameters. I think what is going on is that one of the parameters is not constrained by anything (usually the `v`

), and so Lean is looking for a `category.{u ?u_1} C`

instance. Apparently it's unwilling to take an instance `category.{u v} C`

for some specific `v`

and specialize `?u_1`

to `v`

. I'm not sure whether this is a bug or just something where the system doesn't work in the way we would usually prefer.

#### Johan Commelin (Oct 18 2018 at 13:37):

I see. I wouldn't mind if universe unification was slightly more greedy in this case.

#### Reid Barton (Oct 18 2018 at 13:38):

Your `covering_family`

thing is the second issue.

#### Reid Barton (Oct 18 2018 at 13:43):

Maybe we would like to have something like `out_param`

on the universe parameter `v`

, but that's not currently possible

#### Reid Barton (Oct 18 2018 at 13:44):

Also I don't really understand how `out_param`

works, so I could be way off-base.

#### Reid Barton (Oct 18 2018 at 13:52):

Maybe the clearest example of this is something like `terminal_object (C : Type u) [category.{u v} C] [has_terminal_object.{u v} C] : C`

where you could have a type `C : Type u`

equipped with two totally different `category.{u v}`

and `category.{u w}`

structures with different terminal objects. The type of `terminal_object C`

is just `C`

which has `Type u`

so there is no way you could ever constrain the `v`

parameter.

#### Johan Commelin (Oct 19 2018 at 12:21):

The issues aren't gone, but my definition of `sieve`

is converging onto something far more readable then I had before:

import category_theory.examples.topological_spaces import category_theory.opposites import category_theory.yoneda import category_theory.limits open category_theory universes u u₁ u₂ v v₁ v₂ w w₁ w₂ namespace category_theory.limits variables {C : Type u₁} [𝒞 : category.{u₁ u₂} C] include 𝒞 variables [has_coequalizers.{u₁ u₂} C] {Y Z : C} (f g : Y ⟶ Z) def coequalizer.cofork := has_coequalizers.coequalizer.{u₁ u₂} f g def coequalizer := (coequalizer.cofork f g).X def coequalizer.π : Z ⟶ (coequalizer f g) := (coequalizer.cofork f g).π @[search] def coequalizer.w : f ≫ (coequalizer.π f g) = g ≫ (coequalizer.π f g) := (coequalizer.cofork f g).w def coequalizer.universal_property : is_coequalizer (coequalizer.cofork f g) := has_coequalizers.is_coequalizer.{u₁ u₂} C f g def coequalizer.desc (P : C) (h : Z ⟶ P) (w : f ≫ h = g ≫ h) : coequalizer f g ⟶ P := (coequalizer.universal_property f g).desc { X := P, π := h, w := w } @[extensionality] lemma coequalizer.hom_ext {Y Z : C} {f g : Y ⟶ Z} {X : C} (h k : coequalizer f g ⟶ X) (w : coequalizer.π f g ≫ h = coequalizer.π f g ≫ k) : h = k := begin let s : cofork f g := ⟨ ⟨ X ⟩, coequalizer.π f g ≫ h ⟩, have q := (coequalizer.universal_property f g).uniq s h, have p := (coequalizer.universal_property f g).uniq s k, rw [q, ←p], solve_by_elim, refl end end category_theory.limits section presheaf open category_theory.limits variables (X : Type u₁) [𝒳 : category.{u₁ v₁} X] (C : Type u₂) [𝒞 : category.{u₂ v₂} C] include 𝒳 𝒞 def presheaf := Xᵒᵖ ⥤ C variables {X} {C} instance : category (presheaf X C) := by unfold presheaf; apply_instance omit 𝒞 instance presheaf.has_coequalizers : @has_coequalizers (presheaf X (Type v₁)) presheaf.category_theory.category := sorry instance presheaf.has_coproducts : @has_coproducts (presheaf X (Type v₁)) presheaf.category_theory.category := sorry instance presheaf.has_pullbacks : @has_pullbacks (presheaf X (Type v₁)) presheaf.category_theory.category := sorry end presheaf -- todo should this be done as a subfunctor? structure covering_family {X : Type u₁} [category.{u₁ v₁} X] (U : X) := (index : Type v₁) (obj : index → X) (map : Π (i : index), obj i ⟶ U) namespace covering_family open category_theory.limits variables {X : Type u₁} [𝒳 : category.{u₁ v₁} X] include 𝒳 variables {U : X} def sieve (f : covering_family U) : presheaf X (Type v₁) := let CP := (((yoneda X) : X → presheaf X (Type v₁)) ∘ f.obj) in coequalizer (Sigma.desc (λ p : (f.index × f.index), (Sigma.ι CP p.1) ∘ (pullback.π₁ ((yoneda X).map (f.map p.1)) ((yoneda X).map (f.map p.2))))) (Sigma.desc (λ p : (f.index × f.index), (Sigma.ι CP p.2) ∘ (pullback.π₂ ((yoneda X).map (f.map p.1)) ((yoneda X).map (f.map p.2))))) def sheaf_condition (f : (covering_family U)) {C : Type u₂} [category.{u₂ v₂} C] (F : presheaf X C) : Prop := sorry end covering_family

#### Johan Commelin (Oct 19 2018 at 12:22):

But there are still a lot of typeclass issues.

Last updated: May 12 2021 at 06:14 UTC