LocallyDiscrete

Stream: mathlib4

[Calle Sönne]

Currently, LocallyDiscrete is defined as a type synonym rather than a structure:

/-- A type synonym for promoting any type to a category,
with the only morphisms being equalities.
-/
def LocallyDiscrete (C : Type u) :=
  C

Is there a particular reason by this? For example Discrete is defined as a structure, and I feel it should be used in a very similar way. I need to develop some API for LocallyDiscrete anyways, because I need to move between a category C and LocallyDiscrete C a lot when defining the fibered category associated to a pseudofunctor (valued in Cat). Would it be a good idea to also make it a structure then?

[Adam Topaz]

IMO it should be a structure just like Discrete

[Adam Topaz]

I think it's not as commonly used, so no one got around to doing this.

[Calle Sönne]

Adam Topaz said:

I think it's not as commonly used, so no one got around to doing this.

That's what I was suspecting, but I wanted to check before starting to rewrite everything