search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
45 stars 12 forks source link

Definition of (co)limits #50

Closed cesarbm03 closed 1 year ago

TashiWalde commented 1 year ago

I don't know if this is the right place to leave these comments, since the branch has already been merged.

Here is another possible definition of limit:

  1. Define cocone not as a single Sigma type, but as a type family cone : (f : A -> B) -> (b : B) -> U.
  2. Define the canonical composition map cone-precomp b x : cone f x -> hom B b x -> cone f b.
  3. Define limit (f : A->B) := Sigma ( x: X, c : cone f x ), (b : B) -> is-equiv (cone-precomp b x c)

Alternatively, if one wants to avoid inputting the composition map (which would require a Segal type), one could directly ask for an equivalence of dependent types (b:B) -> Equiv (hom B b x) (cone f b) and then show that for a Segal type this equivalence needs to be given by composition.

I would argue that this definition is the "morally correct one" because it generalizes well to enriched settings (when the homs of B are not groupoids). In general, it does not suffice to require the universal cone to be terminal; one really needs to insist that it really induces an equivalence between homs and cones.

Of course, in our context one can prove that having a terminal object in the total space of a cartesian fibration identifies that fibration with the representable hom-fibration (side question: is this fact already formalized somewhere?); thus showing that both definitions are equivalent.

jonweinb commented 1 year ago

Of course, in our context one can prove that having a terminal object in the total space of a cartesian fibration identifies that fibration with the representable hom-fibration (side question: is this fact already formalized somewhere?); thus showing that both definitions are equivalent.

Not for the cartesian case, at least, but I'm currently working more on cocartesian fibrations in the Yoneda repository.

TashiWalde commented 1 year ago

Of course, in our context one can prove that having a terminal object in the total space of a cartesian fibration identifies that fibration with the representable hom-fibration (side question: is this fact already formalized somewhere?); thus showing that both definitions are equivalent.

Not for the cartesian case, at least, but I'm currently working more on cocartesian fibrations in the Yoneda repository.

Yeah, I might have gotten cartesian and cocartesian confused :)

jonweinb commented 1 year ago

No worries, I wanted to make the point that the formalization of co-/cartesian (as opposed to discrete co-/contravariant) families isn't quite at that stage yet, but getting there. :)