open import 1Lab.Counterexamples.IsIso renaming (contra to ¬is-iso-is-prop)
open import 1Lab.Equiv.Biinv
open import 1Lab.Prelude

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

  IsoJ
: ∀ {ℓ ℓ'} {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:

  is-iso-is-preserved
: ∀ {ℓ} {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 _) ⟩≡
refl                      ∎


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 _)