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.
Improve this question
$\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, 2021 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, 2021 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, 2021 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, 2021 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, 2021 at 18:29

1 Answer 1

Reset to default
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.

Improve this answer
$\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, 2021 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, 2021 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, 2021 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$
    – Andrej Bauer
    Nov 13, 2021 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, 2021 at 0:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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