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.

$\endgroup$
5
$\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.

$\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$ Sep 25 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$ Sep 26 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$ Sep 26 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 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.

$\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$ Sep 25 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 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$ Sep 25 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 at 8:51
  • 1
    $\begingroup$ No problem. Cheers. :-) $\endgroup$ Sep 25 at 9:03

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.