6
$\begingroup$

The operations of adding and removing a point (where removing is a consideration of a subset of elements x such that $(x = *) \to 0$) implements the equivalence of these 1-types, as far as I can see. Then, by univalence, it comes from equality.

My intuition tells me that this should not be the case because these are different concepts. But is the reasoning correct?

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ The result (and the argument) sounds reasonable and it is true in the simplicial model, so I see no reason to doubt it if you believe you have a proof. $\endgroup$
    – Simon Henry
    Commented Oct 14, 2023 at 2:37
  • $\begingroup$ Would it ease your discomfort to notice that this equivalence doesn't commute with the maps that takes underlying sets? So as abstract types, they can be identified, but not as types together with a notion of underlying set? $\endgroup$
    – Ulrik Buchholtz
    Commented Oct 14, 2023 at 6:19
  • $\begingroup$ Yes, I thought about this too. But no, with category equivalences we often significantly change the base set (if we are talking about such a thing at all), the main thing is that all data and axioms are rearranged in two directions. In this case, the concepts are equivalent, regardless of what happens to the base sets. Here we have more data on one side than on the other. To think that a point set and a bare set are the same concept seems strange to me. $\endgroup$
    – Arshak Aivazian
    Commented Oct 14, 2023 at 6:34
  • 1
    $\begingroup$ The natural categories corresponding to them are not actually equivalent. Although I still don’t know how exactly mathematics is supposed to guess which definition of morphisms is correct for any type :) $\endgroup$
    – Arshak Aivazian
    Commented Oct 14, 2023 at 6:34
  • $\begingroup$ What is the "LEM for sets" mentioned in the title? $\endgroup$
    – Dan Doel
    Commented Oct 15, 2023 at 20:53

1 Answer 1

Reset to default
5
$\begingroup$

I will give a somewhat philosophical answer, which is no, in HoTT with LEM, pointed sets and sets are not the same thing. That is when you are working in HoTT, you always know when you are working with a set and when you are working with a pointed set and no confusion can ever arise from this situation.

What is true is that pointed sets and sets may be identified by an equivalence $e : \textrm{Set}_* \simeq \textrm{Set}$, which due to univalence gives us a path/identification $p : \textrm{Set}_* \equiv \textrm{Set}$. But paths/identifications in HoTT do not force us to treat the two sides of the path as indistinguishable, it says something more like "any construction we do with with pointed sets can be transported without loss of information to a corresponding construction on sets (and vice-versa)." If you work in a proof assistant for HoTT you will see that if you try to give a Set and say it's a pointed set, you will just get a type error, you would need to explicitly invoke the path.

If it makes you more comfortable to think in terms of models, we should think of these types as (infinity)-groupoids, in which case $\textrm{Set}_*$ is the 1-groupoid of pointed sets and base-point preserving isomorphisms and $\textrm{Set}$ is the 1-groupoid of sets and isomorphisms, and these groupoids are equivalent.

Edit: Also, you can remove the global assumption of LEM by replacing pointed sets with "sets equipped with a detachable point", i.e., pointed sets such that equality with the point is decidable.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .