<p>The Univalence axiom has various consequences for the identity types, for example:</p>
<ol>
<li>It implies <a href="https://ncatlab.org/nlab/show/function+extensionality#relation_to_the_univalence_axiom" rel="nofollow noreferrer">function extensionality</a>, which governs equality of functions.</li>
<li>It implies that <a href="https://homotopytypetheory.org/2012/06/07/a-simpler-proof-that-%CF%80%E2%82%81s%C2%B9-is-z/" rel="nofollow noreferrer">the circle has a non-trivial identity type</a>.</li>
<li>It implies <a href="https://planetmath.org/98thestructureidentityprinciple" rel="nofollow noreferrer">the identity structure principle</a>.</li>
</ol>
<p><strong>Supplemental:</strong> I may have misunderstood the point of the original question, so let me add a little more.</p>
<p>Suppose in HoTT we construct a type <span class="math-container">$A$</span> <em>without</em> reference to universes and higher-inductive types, that is, just from <span class="math-container">$\mathbb{N}$</span>, <span class="math-container">$\mathbb{1}$</span>, <span class="math-container">$\mathbb{0}$</span>, <span class="math-container">$\times$</span>, <span class="math-container">$+$</span>, <span class="math-container">$\Sigma$</span>, <span class="math-container">$\Pi$</span>, <span class="math-container">$\mathrm{Id}$</span>, and <span class="math-container">$W$</span>-types (inductive types). Because 0-types (sets) are closed under all of these operations, we will get a <span class="math-container">$0$</span>-type. This covers all the examples given in the question and then some.</p>

CC BY-SA 4.0
2021-11-13T15:35:56.760Z
1. I am aware of this, and funext does imply paths between functions are not unique, but what about inductive types (e.g. booleans)?
Guest0x0
CC BY-SA 4.0
2021-11-13T15:37:23.417Z
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?
Guest0x0
CC BY-SA 4.0
2021-11-13T15:41:00.243Z
3. Yes, this applies to types. But I wonder what structural isomorphisms between *terms of inductive types* would be like, if any.
Guest0x0
CC BY-SA 4.0
2021-11-13T19:52:58.773Z
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.)
Andrej Bauer
CC BY-SA 4.0
2021-11-14T00:31:01.740Z
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
Guest0x0
CC BY-SA 4.0
2021-11-14T09:03:15.270Z
"Are paths between sets also sets?" – Your askng this leads me to think the best answer to your question might be "please read the definition of sets in HoTT". That is, a little more background reading seems called for. (Remember, you posted this on a *research-level* forum.)
Andrej Bauer
CC BY-SA 4.0
2021-11-14T12:12:24.093Z
Yep, that's a stupid question. How about internal provability of $isSet(A)$ (and more generally $\mathtt{is(n)Type}(A)$)? btw I'll accept the answer and close the question, but would you mind put a link on h-levels in your answer, for the sake of completeness?
Guest0x0
CC BY-SA 4.0
2021-11-14T14:09:05.677Z
Why do you keep saying "internal provability"? In most cases you can just skip the phrase. In any case, I shall add an explanation about sets.
Andrej Bauer
CC BY-SA 4.0
2021-11-13T14:40:44.057Z
2021-11-14T14:14:40.870Z
2021-11-14T14:14:40.870Z
Andrej Bauer
<p>It is well known that Univalence contradicts Axiom K,
for example there are two ways <span class="math-container">$\mathbf{2} = \mathbf{2}$</span> may be proved using Univalence, via <span class="math-container">$\mathtt{id}_{\mathbf{2}}$</span> or <span class="math-container">$\mathtt{not}$</span>.
But this kind of examples only apply to equality between <em>types</em>. For functions, we have funext in HoTT.
How about equality between terms of inductive types then?</p>
<p>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?</p>
<ul>
<li>The type <span class="math-container">$\mathbf{true} = \mathbf{true}$</span> (similarly <span class="math-container">$\mathbf{false} = \mathbf{false}$</span>) has <span class="math-container">$\mathtt{refl}$</span> as its only close term inhabitant.</li>
<li>The type <span class="math-container">$\Sigma_{x_1 : \mathbf{2}} \Sigma_{x_2 : \mathbf{2}}. x_1 = x_2$</span> has <span class="math-container">$(\mathbf{true}, \mathbf{true}, \mathtt{refl}_{\mathbf{true}})$</span> and <span class="math-container">$(\mathbf{false}, \mathbf{false}, \mathtt{refl}_{\mathbf{false}})$</span> as its only close term inhabitants.</li>
<li>For some <span class="math-container">$a$</span>, <span class="math-container">$\mathtt{refl}_a = \mathtt{refl}_a$</span> has <span class="math-container">$\mathtt{refl}_{\mathtt{refl}_a}$</span> as its only close term inhabitant.</li>
</ul>

CC BY-SA 4.0
2021-11-13T20:26:56.697Z
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`.
ice1000
CC BY-SA 4.0
2021-11-14T00:35:56.693Z
@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)?
Guest0x0
CC BY-SA 4.0
2021-11-14T02:36:28.050Z
$\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).
ice1000
CC BY-SA 4.0
2021-11-14T07:15:08.157Z
@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?
Guest0x0
CC BY-SA 4.0
2021-11-14T18:29:44.343Z
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
ice1000
CC BY-SA 4.0
2021-11-14T18:32:06.323Z
Btw, in cubical type theory, `transport` preserves the path information, so transportation over the `notPath : Bool = Bool` will give you `p : PathP (\i => notPath i) true false` a path between `true` and `false`, but its type is different from reflexive paths on booleans. This fact is good for intuition.
ice1000
<type-theory><dependent-type><homotopy-type-theory>
Effect of HoTT/Univalence Axiom on equality between terms of inductive types?
Guest0x0
# Effect of HoTT/Univalence Axiom on equality between terms of inductive types?

(Asked by: username_0 on 2021-11-13)

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.

**Tags:** type-theory, dependent-type, homotopy-type-theory

> **Comments:**
> **username_1**: 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`.  
> **username_0**: @username_1 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)?  
> **username_1**: $\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).  
> **username_0**: @username_1 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?  
> **username_1**: 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  
> **username_1**: Btw, in cubical type theory, `transport` preserves the path information, so transportation over the `notPath : Bool = Bool` will give you `p : PathP (\i => notPath i) true false` a path between `true` and `false`, but its type is different from reflexive paths on booleans. This fact is good for intuition.  

---

## 1 answers

### Answer by username_2 on 2021-11-13. Score: 3 | Accepted answer

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

1. It implies [function extensionality](https://ncatlab.org/nlab/show/function+extensionality#relation_to_the_univalence_axiom), which governs equality of functions.
2. It implies that [the circle has a non-trivial identity type](https://homotopytypetheory.org/2012/06/07/a-simpler-proof-that-%CF%80%E2%82%81s%C2%B9-is-z/).
3. It implies [the identity structure principle](https://planetmath.org/98thestructureidentityprinciple).

**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.

> **Comments:**
> **username_0**: 1. I am aware of this, and funext does imply paths between functions are not unique, but what about inductive types (e.g. booleans)?  
> **username_0**: 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?  
> **username_0**: 3. Yes, this applies to types. But I wonder what structural isomorphisms between *terms of inductive types* would be like, if any.  
> **username_2**: 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.)  
> **username_0**: 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  
> **username_2**: "Are paths between sets also sets?" – Your askng this leads me to think the best answer to your question might be "please read the definition of sets in HoTT". That is, a little more background reading seems called for. (Remember, you posted this on a *research-level* forum.)  
> **username_0**: Yep, that's a stupid question. How about internal provability of $isSet(A)$ (and more generally $\mathtt{is(n)Type}(A)$)? btw I'll accept the answer and close the question, but would you mind put a link on h-levels in your answer, for the sake of completeness?  
> **username_2**: Why do you keep saying "internal provability"? In most cases you can just skip the phrase. In any case, I shall add an explanation about sets.  

---

