open import 1Lab.HLevel.Closure
open import 1Lab.Path.Groupoid
open import 1Lab.Univalence
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Homotopy.Space.Circle

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

Hence, a contradiction:

  contra : βŠ₯
  contra = Β¬is-prop-loops is-prop-loops