module 1Lab.Counterexamples.Isovalence where

The failure of “isovalence”🔗

In HoTT, the univalence principle can be equivalently stated as saying that the equivalences form an identity system on the universe; in cubical type theory, this principle is a theorem. But in most cases, we do not construct equivalences directly by hand, instead factoring the construction through exhibiting a quasi-inverse to the function at hand. Seeing this pattern everywhere, one must wonder: could we not have that the isomorphisms are an identity system on the universe?

This alternative principle is sometimes referred to as isovalence for short, and this file will show that it is inconsistent. First, let’s make things clear: there is a natural choice of isomorphism for any type, given by the identity function, where both homotopies are the identity.

id-iso :  {} {A : Type }  Iso A A
id-iso = id , iso id  x  refl)  x  refl)

Quantifying over this is our only choice. But if we’re looking at a specific type like the circle, there are multiple ways to show that the identity map is an isomorphism. This fact will be crucial in the proof below.

We say that isovalence holds if the isomorphisms, equipped with the natural choice of identity, form an identity system on every universe

Isovalence : Typeω
Isovalence =  {}  is-identity-system {A = Type } Iso  a  id-iso)
module _ (isovalent : Isovalence) where

Assuming that isovalence does hold, we can equip the type of isomorphisms with a path induction-like principle: Fixing a type if we have a type family over and then we can construct a section by showing only

    :  { ℓ'} {A : Type } (P : (B : Type ) (f : Iso A B)  Type ℓ')
     P A id-iso
      {B} (f : Iso A B)  P B f
  IsoJ = IdsJ isovalent

Keep in mind that the family being parametrised by an isomorphism can make statements not only about the underlying map but also about the two-sided inverse with which was equipped. In particular, we can formulate the statement “ is a retract of ”, and conclude this about any by showing it at the identity equivalence:

    :  {} {A B : Type }
     (f : A  B)
     (p : is-iso f)
     is-biinv→is-iso (is-iso→is-biinv p)  p
  is-iso-is-preserved {A = A} f f-iso = IsoJ P at-id (f , f-iso) where
    P : (B : Type _) (f : Iso A B)  Type _
    P B (f , wit) = is-biinv→is-iso (is-iso→is-biinv wit)  wit

Showing this at the identity isomorphism is simple, because Agda will automatically chase it around the computation and tell us what we have to show: for the precise implementation here, it boils down to showing that four copies of the identity path are identical to a single copy:

    at-id : P A id-iso
    at-id = ap (iso id  x  refl)) $ funext λ x 
      refl  refl  refl  refl ≡⟨ (∙-idl _ ·· ∙-idl _ ·· ∙-idl _) 

Finally, because is a proposition, under the assumption of isovalence, we can show that is a proposition; since we already know this is false, we conclude that isovalence also fails. This provides the motivation for seeking a more coherent formulation of equivalence.

  is-iso-is-prop :  {} {A B : Type } (f : A  B)  is-prop (is-iso f)
  is-iso-is-prop f = retract→is-prop
    is-biinv→is-iso is-iso→is-biinv (is-iso-is-preserved f) is-biinv-is-prop

  ¬isovalence : 
  ¬isovalence = ¬is-iso-is-prop (is-iso-is-prop _)