3
$\begingroup$

I have seen it claimed several times that axiom K is inconsistent with univalence (e.g. here and here), 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 @L. Garde's example: https://x80.org/collacoq/tebatuheci.coq.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Sep 25, 2021 at 8:43
  • $\begingroup$ 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. $\endgroup$
    – Grant Jurgensen
    Sep 26, 2021 at 0:25
  • $\begingroup$ 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. $\endgroup$
    – Grant Jurgensen
    Sep 26, 2021 at 0:39
  • 1
    $\begingroup$ @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. $\endgroup$
    – L. Garde
    Oct 9, 2021 at 6:22
2
$\begingroup$

For a quick reference, here'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.

Improve this answer
$\endgroup$
12
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Sep 25, 2021 at 8:29
  • $\begingroup$ @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. $\endgroup$
    – ice1000
    Sep 25, 2021 at 8:32
  • $\begingroup$ How do you know what the OP is not aware of? And what has anythhing to do with Coq in this discussion? $\endgroup$
    – Andrej Bauer
    Sep 25, 2021 at 8:41
  • $\begingroup$ > 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. $\endgroup$
    – ice1000
    Sep 25, 2021 at 8:51
  • 1
    $\begingroup$ No problem. Cheers. :-) $\endgroup$
    – Andrej Bauer
    Sep 25, 2021 at 9:03

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.