4
$\begingroup$

It is well known that Univalence contradicts Axiom K, for example there are two ways $\mathbf{2} = \mathbf{2}$ may be proved using Univalence, via $\mathtt{id}_{\mathbf{2}}$ or $\mathtt{not}$. But this kind of examples only apply to equality between types. For functions, we have funext in HoTT. How about equality between terms of inductive types then?

To be concrete, consider the following list of statements, which of them hold, and which of them are consistent to be added as axiom, in HoTT with Univalence?

  • The type $\mathbf{true} = \mathbf{true}$ (similarly $\mathbf{false} = \mathbf{false}$) has $\mathtt{refl}$ as its only close term inhabitant.
  • The type $\Sigma_{x_1 : \mathbf{2}} \Sigma_{x_2 : \mathbf{2}}. x_1 = x_2$ has $(\mathbf{true}, \mathbf{true}, \mathtt{refl}_{\mathbf{true}})$ and $(\mathbf{false}, \mathbf{false}, \mathtt{refl}_{\mathbf{false}})$ as its only close term inhabitants.
  • For some $a$, $\mathtt{refl}_a = \mathtt{refl}_a$ has $\mathtt{refl}_{\mathtt{refl}_a}$ as its only close term inhabitant.
$\endgroup$
6
  • 1
    $\begingroup$ The first one is true, since $\bf 2$ is an hSet. The second one is true for the same reason but false if we replace $\bf 2$ with other types, consider some higher inductive types. The last one is false, you can prove this by funExt/univalence, which is definitely unequal (but path-equivalent) to refl. $\endgroup$
    – ice1000
    Nov 13 '21 at 20:26
  • $\begingroup$ @ice1000 For the third one, $\mathtt{refl}_a$ is a term of a path type, which is neither a type nor a function. So I don't see how univalence or funext can be used to prove $\mathtt{refl}_a = \mathtt{refl}_a$, could you elaborate more (and perhaps add an answer)? $\endgroup$
    – Guest0x0
    Nov 14 '21 at 0:35
  • $\begingroup$ $\bf refl$ is a function from a term to its reflexive path. For different input type, there might be various different functions from a term to its reflexive path (consider circle, there are infinitely many such functions). $\endgroup$
    – ice1000
    Nov 14 '21 at 2:36
  • $\begingroup$ @ice1000 What about $\mathtt{refl}$ applied at some fixed point $a$? More concretely when $a$ is a term of a set (e.g $\mathbf{true}$). That is, does statement 1 in the question scales to higher order paths on booleans? $\endgroup$
    – Guest0x0
    Nov 14 '21 at 7:15
  • $\begingroup$ it's inevitable. $\bf refl$ is a constructor, thus injective, what would you expect? You can always extract its argument and do the same thing. Also, make sure you keep HITs in mind when considering paths, because inductive types are mostly sets $\endgroup$
    – ice1000
    Nov 14 '21 at 18:29
3
$\begingroup$

The Univalence axiom has various consequences for the identity types, for example:

  1. It implies function extensionality, which governs equality of functions.
  2. It implies that the circle has a non-trivial identity type.
  3. It implies the identity structure principle.

Supplemental: I may have misunderstood the point of the original question, so let me add a little more.

Suppose in HoTT we construct a type $A$ without reference to universes and higher-inductive types, that is, just from $\mathbb{N}$, $\mathbb{1}$, $\mathbb{0}$, $\times$, $+$, $\Sigma$, $\Pi$, $\mathrm{Id}$, and $W$-types (inductive types). Because 0-types (sets) are closed under all of these operations, we will get a $0$-type. This covers all the examples given in the question and then some.

$\endgroup$
8
  • $\begingroup$ 1. I am aware of this, and funext does imply paths between functions are not unique, but what about inductive types (e.g. booleans)? $\endgroup$
    – Guest0x0
    Nov 13 '21 at 15:35
  • $\begingroup$ 2. I consider this a consequence of Higher Inductive Types, or quotient types in general. Am I missing something here, e.g. some essential connection between Univalence and HIT? $\endgroup$
    – Guest0x0
    Nov 13 '21 at 15:37
  • $\begingroup$ 3. Yes, this applies to types. But I wonder what structural isomorphisms between terms of inductive types would be like, if any. $\endgroup$
    – Guest0x0
    Nov 13 '21 at 15:41
  • 2
    $\begingroup$ Inductive types tend to be sets (0-types) so they won't have interesting identity types. (Also, I would recommend talking about equality of elements or points. The word "term" has a very syntactic connotation. I even wrote a Python script that caught all occurrences of "term" in the HoTT book to get rid of them.) $\endgroup$ Nov 13 '21 at 19:52
  • $\begingroup$ Indeed, the word term is ambiguous. I'll edit the question and rephrase it to "terms of inductive types". So my question reduces to: (1) are paths between sets also sets, and (2) Is "type A is a Set" provable internally $\endgroup$
    – Guest0x0
    Nov 14 '21 at 0:31

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.