Why is `is_limit` data?

Stream: maths

[Ken Lee]

The definition of a cone being a limit is as follows in mathlib :

structure is_limit (t : cone F) :=
(lift  : Π (s : cone F), s.X ⟶ t.X)
(fac'  : ∀ (s : cone F) (j : J), lift s ≫ t.π.app j = s.π.app j . obviously)
(uniq' : ∀ (s : cone F) (m : s.X ⟶ t.X) (w : ∀ j : J, m ≫ t.π.app j = s.π.app j),
  m = lift s . obviously)

It contains the data of lifts from other cones as part of the definition, even though the these lifts should be uniquely determined by the universal property. So why keep the data?

I came across this issue because I am trying to define the full subcategory of discrete fibrations in over C where C : Cat.{v u}. Specifically, I want discrete fibrations to be X -> C such that Arrow X is the (1-categorical) pullback of X and Arrow C over C, where Arrow X -> X and Arrow C -> Ctakes target, Arrow X -> Arrow C is induced from X -> C.

[Markus Himmel]

Sometimes it's nice to have the data around because it makes proofs cleaner since you don't have to invoke uniqueness whenever you want to use the specific construction of the limit.

Can you work around the issue by using nonempty (is_limit t) in your application?

[Ken Lee]

Yes, I guess I can try that.

[Johan Commelin]

I think the idea is that has_limits(_of_shape) is a Prop, but the library supports explicit limit constructions with good definitional properties. So to some extent, we need to record data.

[Reid Barton]

You can also use \Sigma (X : over C), is_limit [...] as the objects of your category, even if it's not literally a subtype of anything--this is what docs#category_theory.induced_category is about