<p>For a quick reference, <a href="https://jesper.sikanda.be/files/pattern-matching-without-K.pdf" rel="nofollow noreferrer">here</a>'s (equation 8) a proof sketched in Agda. But I guess you're asking for the idea, and I think the reference is kinda technical.</p>
<p>When you say 'univalence', you not only mean an axiom, but also its relevant computation rules. However, in HoTT, the existence of univalence is postulated, so you have to use the model to compute it. It's the computation rules that are incompatible with K. Here's how.</p>
<p>Imagine univalence as an operator (I wish you can understand the notation, it's quite standard in the literature of dependent type theory), taking an isomorphism and gives you a type-level identity: <code>ua : (f : A -&gt; B) (g : B -&gt; A) (sec : f . g = id) (ret : g . f = id) -&gt; A = B</code>, where <code>.</code> is function composition and <code>id</code> is the identity function. You have another operation <code>transport : A = B -&gt; (A -&gt; B)</code>, which has the following β reduction:</p>
<ul>
<li><code>transport (ua f _ _ _)</code> reduces to <code>f</code> (aka uaβ in some literature)</li>
<li><code>transport refl</code> reduces to <code>id</code> (aka regularity in some literature)</li>
</ul>
<p>OTOH, UIP claims that all identities (including type-level ones) are <code>refl</code>, so <code>ua a b c d</code> for any <code>a</code>, <code>b</code>, <code>c</code>, <code>d</code> should give you <code>refl</code> by UIP. Here you may already see a contradiction, but let's put it further. The following proof is the same as the referenced paper in the beginning of this answerr.</p>
<p>Consider <code>not : Bool -&gt; Bool</code> defined in the obvious way, and <code>notEq : not . not = id</code> proved in the obvious way. <code>transport (ua not not notEq notEq) true = not true = false</code> by ua's β rule, while by UIP it's equivalent to <code>transport refl true = id true = true</code>. See? Same term reduces in two ways. That's a contradiction.</p>
<blockquote>
<p>Is UIP also inconsistent with univalence?</p>
</blockquote>
<p>Yes.</p>

CC BY-SA 4.0
2021-09-25T08:29:21.573Z
If my memory serves me right, one does not need any special computation rules. Simply assuming that $\mathrm{idtoeq} : (A \simeq A) \to (A = A)$ is an equivalence is enough to derive the relevant computation rule (in propositional form), which is certainly enough to show that UIP fails.
Andrej Bauer
CC BY-SA 4.0
2021-09-25T08:32:21.497Z
@AndrejBauer Surely there are many ways, but the fact that $\text{idtoeq}$ is an equivalence is also an extra condition that the OP isn't aware of. Also, you need to define equivalence, which may use contractibility and fiber, which I guess is unfriendly to a Coq-backgrounded person.
ice1000
CC BY-SA 4.0
2021-09-25T08:41:37.993Z
How do you know what the OP is not aware of? And what has anythhing to do with Coq in this discussion?
Andrej Bauer
CC BY-SA 4.0
2021-09-25T08:51:23.510Z
> I understand the univalence axiom only in non-homotopic terms, as a map from an isomorphism on types to an equality of the same types.
ice1000
CC BY-SA 4.0
2021-09-25T08:51:36.420Z
I think "map" does not mean "equivalence".
ice1000
CC BY-SA 4.0
2021-09-25T08:53:54.637Z
I think you need to give people some credit. Also, if I may do so, a word of advice: explicitly telling a person that their knowledge is lacking (especially based on scant evidence) is likely less productive that augmenting their knowledge with an explanation that weaves in the missing bits and lets them absorb it.
Andrej Bauer
CC BY-SA 4.0
2021-09-25T08:55:07.847Z
Yes, I totally agree! That's what I did at the beginning of the second paragraph.
ice1000
CC BY-SA 4.0
2021-09-25T08:56:03.000Z
Yes, I'd do it more gently. Out of curiosity, are you trying to start a Coq vs. Agda religious war?
Andrej Bauer
CC BY-SA 4.0
2021-09-25T08:57:42.500Z
No, I mentioned Coq out of no good reason (I probably shouldn't mention it). Also, speaking of credit, when I pressed enter after the quotation and was going to add some texts (including credits), the message was sent. So it should be an error.
ice1000
CC BY-SA 4.0
2021-09-25T09:03:38.877Z
No problem. Cheers. :-)
Andrej Bauer
CC BY-SA 4.0
2021-09-25T10:10:11.117Z
@AndrejBauer Well, Coq is explicitly mentioned in the question !
L. Garde
CC BY-SA 4.0
2021-09-25T10:35:50.890Z
Oops, I missed that. Answer: Coq is agonistic about both Axiom K and Univalence.
Andrej Bauer
CC BY-SA 4.0
2021-09-25T05:08:36.867Z
2021-09-25T05:08:36.867Z
ice1000
<p>You will certainly find it natural that most types, like structures, admit <em>different</em> isomorphisms. Just take the type <span class="math-container">$\textbf{2}$</span>, with inhabitants <span class="math-container">$0_\textbf{2}$</span> and <span class="math-container">$1_\textbf{2}$</span>. It admits 2 obvious different isomorphisms (<em>id</em> and <em>swap</em>), and therefore, by the univalence axiom, the identity type <span class="math-container">$\textbf{2}=_\textit{U}\textbf{2}$</span> admits 2 different inhabitants.</p>
<p>This is in contradiction with UIP, and with axiom K which is a special case of it.</p>
<p>See Example 3.1.9, and Theorem 7.2.1 of the HoTT book.</p>

CC BY-SA 4.0
2021-09-25T08:43:43.917Z
The OP explicitly asked whether Axiom K and UIP are equivalent. Your answer is a bit misleading in that regard, so it is better to clarify: Axiom K is indeed an *instance* of UIP, but from that instance we can derive the rest of UIP.
Andrej Bauer
CC BY-SA 4.0
2021-09-26T00:25:48.273Z
Oh, I see now. It was not immediately clear to me how we could construct a contradiction from the different isomorphisms, but I worked it out. For anyone else as slow as me:

Let `x, y: A ≃ B`, where `x ≠ y`, and `ϕ: (A ≃ B) ≃ (A = B)` the isomorphism obtained by specializing the univalence axiom to types `A` and `B`. By UIP, we have `ϕ x = ϕ y`, which cancels to `x = y`, a contradiction.
Grant Jurgensen
CC BY-SA 4.0
2021-09-26T00:39:18.667Z
It's also worth noting that I originally referred to univalence as a "a map from an isomorphism on types to an equality of the same types", i.e. a term of type `Π A B: Type, A ≃ B -> A = B`. This was perhaps a mistake; I believe univalence typically refers to the stronger claim `Π A B: Type, (A ≃ B) ≃ (A = B)`, which I used to finish the above proof.
Grant Jurgensen
CC BY-SA 4.0
2021-10-09T06:22:12.457Z
@GrantJurgensen Your are right, my answer is elliptic on that point.
The univalence axiom says more precisely that the map from identity to isomorphism is an equivalence (HoTT book A.3.1), that is to say it postulates a map from isomorphism to identity which is an inverse of the natural map from identity to isomorphism.
L. Garde
CC BY-SA 4.0
2021-09-25T08:23:02.513Z
2021-09-25T08:23:02.513Z
L. Garde
<p>I have seen it claimed several times that axiom K is inconsistent with univalence (e.g. <a href="https://coq.discourse.group/t/what-do-you-think-of-axioms/231" rel="nofollow noreferrer">here</a> and <a href="https://ncatlab.org/nlab/show/axiom+K+%28type+theory%29" rel="nofollow noreferrer">here</a>), but I have never seen a proof sketch. Specifically, I'm curious about how this manifests in the Coq theorem prover.</p>
<p>Also, I thought axiom K was equivalent to UIP. Is UIP also inconsistent with univalence?</p>
<p>For what its worth, I am not well versed in homotopy theory. I understand the univalence axiom only in non-homotopic terms, as a map from an isomorphism on types to an equality of the same types.</p>
<p>Edit: Here is a Coq proof based on @L. Garde's example: <a href="https://x80.org/collacoq/tebatuheci.coq" rel="nofollow noreferrer">https://x80.org/collacoq/tebatuheci.coq</a>.</p>

<type-theory><coq><homotopy-type-theory>
How does axiom K contradict univalence?
Grant Jurgensen
# How does axiom K contradict univalence?

(Asked by: username_0 on 2021-09-24)

I have seen it claimed several times that axiom K is inconsistent with univalence (e.g. [here](https://coq.discourse.group/t/what-do-you-think-of-axioms/231) and [here](https://ncatlab.org/nlab/show/axiom+K+%28type+theory%29)), but I have never seen a proof sketch. Specifically, I'm curious about how this manifests in the Coq theorem prover.

Also, I thought axiom K was equivalent to UIP. Is UIP also inconsistent with univalence?

For what its worth, I am not well versed in homotopy theory. I understand the univalence axiom only in non-homotopic terms, as a map from an isomorphism on types to an equality of the same types.

Edit: Here is a Coq proof based on @username_3's example: <https://x80.org/collacoq/tebatuheci.coq>.

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


---

## 2 answers

### Answer by username_3 on 2021-09-25. Score: 6 | Accepted answer

You will certainly find it natural that most types, like structures, admit *different* isomorphisms. Just take the type $\textbf{2}$, with inhabitants $0\_\textbf{2}$ and $1\_\textbf{2}$. It admits 2 obvious different isomorphisms (*id* and *swap*), and therefore, by the univalence axiom, the identity type $\textbf{2}=\_\textit{U}\textbf{2}$ admits 2 different inhabitants.

This is in contradiction with UIP, and with axiom K which is a special case of it.

See Example 3.1.9, and Theorem 7.2.1 of the HoTT book.

> **Comments:**
> **username_2**: The OP explicitly asked whether Axiom K and UIP are equivalent. Your answer is a bit misleading in that regard, so it is better to clarify: Axiom K is indeed an *instance* of UIP, but from that instance we can derive the rest of UIP.  
> **username_0**: Oh, I see now. It was not immediately clear to me how we could construct a contradiction from the different isomorphisms, but I worked it out. For anyone else as slow as me:  Let `x, y: A ≃ B`, where `x ≠ y`, and `ϕ: (A ≃ B) ≃ (A = B)` the isomorphism obtained by specializing the univalence axiom to types `A` and `B`. By UIP, we have `ϕ x = ϕ y`, which cancels to `x = y`, a contradiction.  
> **username_0**: It's also worth noting that I originally referred to univalence as a "a map from an isomorphism on types to an equality of the same types", i.e. a term of type `Π A B: Type, A ≃ B -> A = B`. This was perhaps a mistake; I believe univalence typically refers to the stronger claim `Π A B: Type, (A ≃ B) ≃ (A = B)`, which I used to finish the above proof.  
> **username_3**: @GrantJurgensen Your are right, my answer is elliptic on that point. The univalence axiom says more precisely that the map from identity to isomorphism is an equivalence (HoTT book A.3.1), that is to say it postulates a map from isomorphism to identity which is an inverse of the natural map from identity to isomorphism.  

---

### Answer by username_1 on 2021-09-25. Score: 2

For a quick reference, [here](https://jesper.sikanda.be/files/pattern-matching-without-K.pdf)'s (equation 8) a proof sketched in Agda. But I guess you're asking for the idea, and I think the reference is kinda technical.

When you say 'univalence', you not only mean an axiom, but also its relevant computation rules. However, in HoTT, the existence of univalence is postulated, so you have to use the model to compute it. It's the computation rules that are incompatible with K. Here's how.

Imagine univalence as an operator (I wish you can understand the notation, it's quite standard in the literature of dependent type theory), taking an isomorphism and gives you a type-level identity: `ua : (f : A -> B) (g : B -> A) (sec : f . g = id) (ret : g . f = id) -> A = B`, where `.` is function composition and `id` is the identity function. You have another operation `transport : A = B -> (A -> B)`, which has the following β reduction:

* `transport (ua f _ _ _)` reduces to `f` (aka uaβ in some literature)
* `transport refl` reduces to `id` (aka regularity in some literature)

OTOH, UIP claims that all identities (including type-level ones) are `refl`, so `ua a b c d` for any `a`, `b`, `c`, `d` should give you `refl` by UIP. Here you may already see a contradiction, but let's put it further. The following proof is the same as the referenced paper in the beginning of this answerr.

Consider `not : Bool -> Bool` defined in the obvious way, and `notEq : not . not = id` proved in the obvious way. `transport (ua not not notEq notEq) true = not true = false` by ua's β rule, while by UIP it's equivalent to `transport refl true = id true = true`. See? Same term reduces in two ways. That's a contradiction.

> Is UIP also inconsistent with univalence?

Yes.

> **Comments:**
> **username_2**: If my memory serves me right, one does not need any special computation rules. Simply assuming that $\mathrm{idtoeq} : (A \simeq A) \to (A = A)$ is an equivalence is enough to derive the relevant computation rule (in propositional form), which is certainly enough to show that UIP fails.  
> **username_1**: @AndrejBauer Surely there are many ways, but the fact that $\text{idtoeq}$ is an equivalence is also an extra condition that the OP isn't aware of. Also, you need to define equivalence, which may use contractibility and fiber, which I guess is unfriendly to a Coq-backgrounded person.  
> **username_2**: How do you know what the OP is not aware of? And what has anythhing to do with Coq in this discussion?  
> **username_1**: > I understand the univalence axiom only in non-homotopic terms, as a map from an isomorphism on types to an equality of the same types.  
> **username_1**: I think "map" does not mean "equivalence".  
> **username_2**: I think you need to give people some credit. Also, if I may do so, a word of advice: explicitly telling a person that their knowledge is lacking (especially based on scant evidence) is likely less productive that augmenting their knowledge with an explanation that weaves in the missing bits and lets them absorb it.  
> **username_1**: Yes, I totally agree! That's what I did at the beginning of the second paragraph.  
> **username_2**: Yes, I'd do it more gently. Out of curiosity, are you trying to start a Coq vs. Agda religious war?  
> **username_1**: No, I mentioned Coq out of no good reason (I probably shouldn't mention it). Also, speaking of credit, when I pressed enter after the quotation and was going to add some texts (including credits), the message was sent. So it should be an error.  
> **username_2**: No problem. Cheers. :-)  
> **username_3**: @AndrejBauer Well, Coq is explicitly mentioned in the question !  
> **username_2**: Oops, I missed that. Answer: Coq is agonistic about both Axiom K and Univalence.  

---

