module 1Lab.Counterexamples.IsIso where

# is-iso is not a propositionπ

We show that if is-iso were a proposition, then (x : A) β x β‘ x would be contractible for any choice of A. Taking A to be SΒΉ, we show that this can not be the case. Suppose that is-iso is a proposition.

module
_ (iso-is-prop : β {β} {A B : Type β} {f : A β B} β is-prop (is-iso f))
where

First we characterise the type is-iso f by showing that, if it is inhabited, then it is equivalent to the centre of A, i.e.Β the loop-assigning maps of A:

lemma : β {β} {A B : Type β} {f : A β B} β is-iso f β is-iso f β ((x : A) β x β‘ x)
lemma {A = A} {B} {f} iiso =
EquivJ (Ξ» _ f β is-iso (f .fst) β ((x : A) β x β‘ x))
(IsoβEquiv helper)
(f , is-isoβis-equiv iiso)
where

By equivalence induction, it suffices to cover the case where f is the identity function. In that case, we can construct an isomorphism quite readily, where the proof uses our assumption iso-is-prop for convenience.

helper : Iso _ _
helper .fst iiso x =
sym (iiso .is-iso.linv x) β iiso .is-iso.rinv x
helper .snd .is-iso.inv x = iso (Ξ» x β x) x (Ξ» _ β refl)
helper .snd .is-iso.rinv p = funext Ξ» x β β-idl _
helper .snd .is-iso.linv x = iso-is-prop _ _

We thus have that is-iso id β ((x : A) β x β‘ x) - since the former is a prop (by assumption), then so is the latter:

is-prop-loops : β {β} {A : Type β} β is-prop ((x : A) β x β‘ x)
is-prop-loops {A = A} = equivβis-hlevel 1 (helper .fst) (helper .snd) iso-is-prop
where helper = lemma {f = Ξ» (x : A) β x}
(iso (Ξ» x β x) (Ξ» x β refl) (Ξ» x β refl))

Thus, it suffices to choose a type for which (x : A) β x β‘ x has two distinct elements. We go with the circle, SΒΉ:

Β¬is-prop-loops : Β¬ is-prop ((x : SΒΉ) β x β‘ x)
Β¬is-prop-loops prop = reflβ loop \$
happly (prop (Ξ» x β refl)
Ξ» { base β loop
; (loop i) j β hcomp (β i β¨ β j) Ξ» where
k (k = i0) β loop (i β¨ j)
k (i = i0) β loop j
k (i = i1) β loop (k β§ j)
k (j = i0) β loop i
k (j = i1) β loop (k β§ i)
})
base