3
$\begingroup$

if sup({1,2,3})=3, why can't I use univalence and the fact that {1,2,3}≅{4,5,6} to establish that sup({4,5,6})=3?

$\endgroup$
3
  • $\begingroup$ This is a refinement of a potentially isomorphic question regarding shopping lists and univalence suggested by @DerekElkins in the discussion around the question "isomorphism and the real world" math.stackexchange.com/questions/2494830/… $\endgroup$ Oct 29, 2017 at 14:48
  • $\begingroup$ I don't see why univalence should apply to this kind of sentence. Univalence is a property of a type-theoretic universe; it talks about equivalence and identity of types. $\endgroup$ Oct 29, 2017 at 14:59
  • 1
    $\begingroup$ Though there are already good answers, I'll point out that I phrased the question (in the comment to the other question) as I would expect someone first coming to HoTT/hearing of univalance likely would. If you actually tried to formalize the statement in HoTT, you realize 1) it's not obvious how to translate it, 2) $\{1,2,3\}$ and $\{4,5,6\}$ need to be types to apply univalence, and 3) if they are types then the second expression is a type error if naively translated. $\endgroup$ Oct 30, 2017 at 0:58

4 Answers 4

6
$\begingroup$

You can use univalence like that, but then you have to properly apply it everywhere.

Suppose $e : \{1, 2,3\} \to \{4, 5, 6\}$ is an equivalence. By Univalence axiom there is a path $\mathsf{ua}(e) : \{1, 2,3\} = \{4, 5, 6\}$. There is a path $$p : \sup \{1, 2, 3\} = 3.$$ In order to apply univalence to $\{1, 2, 3\}$ in this sitution, we have to transport $\{1, 2, 3\}$ as well as $\sup$, $p$ and the element $3$ along the path $\mathsf{ua}(e)$. What we get is something like $$\mathsf{ua}(e) \cdot p : (e \circ \mathsf{sup} \circ e^{-1}) \{4, 5, 6\} = e(3).$$ I am not trying to be precise here, because we are already quite sloppy by writing set-theoretic stuff like $\{1, 2, 3\}$ and $\{4, 5, 6\}$, but I hope you get the idea: You have to explicitly transport the entire statement along the equivalence.

Similarly, if your wife sends you to a store to buy $\{\mathrm{bread}, \mathrm{milk}, \mathrm{eggs}\}$ and you brougth back $\{\mathrm{chococalate}, \mathrm{whiskey}, \mathrm{beer}\}$ then in order to make your wife happy, you would have to select an equivalence $e$ between these two sets, and transport the entire statement

Wife ordered $\{\mathrm{bread}, \mathrm{milk}, \mathrm{eggs}\}$.

along $e$. You would end up with something like

$e(\text{Wife})$ ordered $\{\mathrm{chococalate}, \mathrm{whiskey}, \mathrm{beer}\}$.

Are you quite sure you want to transport your wife like that?

$\endgroup$
1
  • $\begingroup$ This also looks like the answer :-) $\endgroup$ Oct 30, 2017 at 11:55
2
$\begingroup$

Univalence is about equivalence of types inhabiting a Universe, but {1,2,3} is not such a type, it is a term of a set inhabiting U.

$\endgroup$
3
  • $\begingroup$ yes, that makes sense, and it echoes now what I now remember reading on the subject. I'll need to look again in more detail again at the notion of Types in HoTT. $\endgroup$ Oct 29, 2017 at 15:13
  • $\begingroup$ There is a longer answer on the HoTT mailing list that goes further it seems that this answer. I am not sure if one can copy and paste answers from mailing lists. I suppose at least one can point them groups.google.com/d/msg/hott-cafe/-ICU_rVEoYY/DeVLZnUYBAAJ $\endgroup$ Oct 29, 2017 at 17:38
  • $\begingroup$ This is not necessarily true, for we can regard $\{ 1, 2, 3 \}$ as a type as well. To put it simply, the OP's observation is not a puzzle because they the objects are identical only up to propositionally equal (as sets) but not definitionally equal. $\endgroup$ Oct 30, 2017 at 3:18
1
$\begingroup$

The question may reveal a confusion between univalence on one hand and transporting along an identity on the other hand. I will try to disentangle them.

Start with two sets, $\textit{i.e}$ two elements of the type hSet, let say $\lbrace 1,2,3\rbrace$, $\lbrace 4, 5, 6\rbrace$ : hSet, then recall that the type hSet is the dependent sum type $\sum X: U, \text{isaset}\,X$ (where $U$ is a type-theoretic universe and $\text{isaset}\,X$ is the proposition that the type $X$ is a set), one can prove that the type $\lbrace 1, 2, 3\rbrace =_{hSet} \lbrace 4,5,6\rbrace$ is equivalent to the type

$\sum p : \text{pr1} \lbrace 1,2,3\rbrace =_U \text{pr1} \lbrace 4,5,6\rbrace, \text{transport}\,p\,(\text{pr2} \lbrace 1,2,3\rbrace) = \text{pr2}\lbrace 4,5,6\rbrace$.

But $\text{isaset}(\text{pr1}\lbrace 4,5,6\rbrace)$ being a proposition, an element of the sum type above amounts to just an element of the type $\text{pr1} \lbrace 1,2,3\rbrace =_U \text{pr1} \lbrace 4,5,6\rbrace$. It is where the univalence comes into play, telling you that it's enough (in order to get an identity between our given sets) to have an equivalence between the first projections, namely an element of the type $\text{pr1}\lbrace 1,2,3\rbrace \cong \text{pr1} \lbrace 4,5,6\rbrace$.

Once you have an equality between $\lbrace 1,2,3\rbrace$ and $\lbrace 4,5,6\rbrace$ (and we have seen above what such an equality means), you can use this equality to transport any property from $\lbrace 1,2,3\rbrace$ to $\lbrace 4,5,6\rbrace$. Indeed, given a family of small types $B(X)$, with $X:hSet$, one has an element $\text{transport}_B$ of type

$B(\lbrace 1,2,3\rbrace)\times (\lbrace 1,2,3\rbrace =_{hSet} \lbrace 4,5,6\rbrace) \rightarrow B(\lbrace 4,5,6\rbrace)$.

Take for instance "$X$ has a sup" for $B(X)$, then from your equality (possibly resulting from the use of the univalence axiom as sketched above) and the fact that $\lbrace 1,2,3\rbrace$ has a sup one concludes, using $\text{transport}_B$, that $\lbrace 4,5,6\rbrace$ has a sup. You could take $B(X,x) := (\text{sup} X =_{\text{pr1}X} x)$ as a family of types indexed by the type ($\sum X: hSet, \text{pr1}\,X$) and try to transport along an adequate equality, but this family of types is not even well defined since the element $\text{sup}\,X$ does not always exist. I hope it illustrates how one can use, or misuse for that matter, transport along an identity. So you really need to be careful and work out the details .

$\endgroup$
1
  • $\begingroup$ I'll set this one as the answer, though of course I am not the right person to be able to judge that at this point. But this is certainly enough for me to study. $\endgroup$ Oct 29, 2017 at 20:10
1
$\begingroup$

Since this is tagged as category-theory, a resolution in terms of category theory may be informative.

If we use $\{ 1, 2, 3 \}$ and $\{ 4, 5, 6\}$ to denote objects of the category Set, then they are indeed isomorphic.

If we use $\{ 1, 2, 3 \}$ and $\{ 4, 5, 6\}$ to denote subsets of $\mathbb{N}$ (i.e. objects of the category $\mathrm{Sub}(\mathbb{N})$), then they are not isomorphic.

$\sup$ is a (partial) operation on $\mathrm{Sub}(\mathbb{N})$, so it is the latter notion of isomorphism that is relevant, not the former.

$\endgroup$
1
  • $\begingroup$ Thanks, that is also very helpful. Because it would be odd if HoTT did not mesh with Category Theory. I'll keep this in mind as I go along in my research.... $\endgroup$ Feb 9, 2018 at 8:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.