Zulip Chat Archive

Stream: maths

Topic: Category Type

Mathieu Chanavat (Sep 23 2022 at 19:38):

Hi there,
(this is my first message, please be nice :))

So I'm having trouble with pullbacks in the category Type. Say I have two maps in Type u: m,m′:X→Ym, m' : X \to Y. Then I can consider their pullback cone via limit.cone (cospan m m') without any problem. However, when I take m=m′ m = m', Lean gives an error "maximum class-instance resolution depth has been reached". I found a workaround, but it's not very pretty and I'd like to understand what's going on (I'm not very familiar with the notation .{u} for the universes and all this stuff). Did I miss something?
Minimal code (lean:3.48.0):

import category_theory.limits.types
import category_theory.functor
import category_theory.limits.shapes.functor_category

open category_theory category_theory.limits functor

universes u
noncomputable theory

-- set_option trace.class_instances true

def one_map_Type {X Y : Type u} (m : X ⟶ Y) :=
  limit.cone (cospan m m)

def two_maps_Type {X Y : Type u} (m m' : X ⟶ Y) : cone (cospan m m') :=
  limit.cone (cospan m m')

-- A workaround
def Types_inst := category_theory.types.{u}

def one_map_Type' {X Y : Type u} (m : X ⟶ Y) : cone (cospan m m) :=
  @limit.cone _ _ _ Types_inst.{u} (cospan m m) _

-- A non-workaround
def one_map_Type'' {X Y : Type u} (m : X ⟶ Y) : cone (cospan m m) :=
  @limit.cone _ _ _ category_theory.types.{u} (cospan m m) _

Adam Topaz (Sep 23 2022 at 19:51):

here is a minimal example for anyone reading this:

import category_theory.limits.types

open category_theory category_theory.limits functor

universes u

set_option trace.class_instances true

example {X Y : Type u} (m : X ⟶ Y) : has_pullback m m := infer_instance

Adam Topaz (Sep 23 2022 at 19:52):

typeclass inference cannot deduce a has_pullback m m instance.

Adam Topaz (Sep 23 2022 at 19:52):

this isn't good.

Adam Topaz (Sep 23 2022 at 19:55):

from the class instance trace it seems that lean REALLY wants to show that m satisfies is_iso...

Adam Topaz (Sep 23 2022 at 19:56):

And it looks like there is a loop...

Adam Topaz (Sep 23 2022 at 19:57):

Adam Topaz (Sep 23 2022 at 20:03):

Just in case it helps diagnosing the issue:

import category_theory.limits.types

open category_theory category_theory.limits functor

universes u

local attribute [-instance]
  limits.has_kernel_pair_of_mono
  limits.has_pullback_of_left_factors_mono
  limits.has_pullback_of_right_factors_mono
  limits.has_pullback_of_comp_mono

example {X Y : Type u} (m : X ⟶ Y) : has_pullback m m := infer_instance

this works fine

Andrew Yang (Sep 23 2022 at 20:09):

I think the situation is kind of like the one mentioned here, where Lean somehow finds (λ x, x) ≫ f defeq to f and it then goes in some loop.

Adam Topaz (Sep 23 2022 at 20:10):

yeah you're probably right.

Last updated: Dec 20 2023 at 11:08 UTC