Groupoid.toCategory

Stream: mathlib4

[Adam Topaz]

Consider the following:

import Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

open CategoryTheory

variable (X : Type*) [TopologicalSpace X]

#synth (Category X) -- Groupoid.toCategory

This seems like a problem to me!

[Adam Topaz]

It seems to come from docs#FundamentalGroupoid which is reducible for some reason!

[Adam Topaz]

https://github.com/leanprover-community/mathlib4/blob/bd3e369b6f82c874de0f318c71d7e0595f8a3aa4/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean#L278C1-L278C42

[Joël Riou]

I agree that FundamentalGroupoid should not be reducible.

[Eric Wieser]

I think this was a badly ported local attribute [reducible]?

[Adam Topaz]

In mathlib3 it was tagged with local attribute [reducible]. I suppose whoever ported this file gave up when lean4 didn't allow for local reducibility and just made it globally reducuble

[Adam Topaz]

I'll try to PR a fix at some point soon.

[Adam Topaz]

BTW @Jack McKoen this is exactly the issue we came across at the end of lecture from last Thursday.

[Adam Topaz]

#8257