How to prove in Agda that every equivalence in the type 𝟚 is either id or a permutation?

Question

I would like to prove in Agda that every equivalence of the type 𝟚 is either the identity, or the permutation of two elements.

  𝟚-equivalences-characterization: ∀ (f : 𝟚 ≃ 𝟚) → ((proj₁ f) ≡ id) ⊎ ((proj₁ f) ≡ permut-𝟚)

My idea was to use with-clause, to split into cases the result of applying (proj₁ f) to inj₁ * and inj₂ *. The problem is that I can't make something like this work:

  𝟚-equivalences-characterization f with (proj₁ f) (inj₁ *) | (proj₁ f) (inj₂ *)
  ...                                            | (inj₁ *) | (inj₂ *) = inj₁ (funext (proj₁ f) id T) where
                                                                      T : ∀ (u : 𝟚-type) → (proj₁ f) u ≡ u
                                                                      T (inj₁ *) = refl
                                                                      T (inj₂ *) = refl

It seems that refl is not a proof that (proj₁ f) (inj₁ *) ≡ (inj₁ *), even though that is literally the case I am at. I am not sure how to approach this proof. Mathematically it seems evident that but I can't make it work in agda.

Answer 1

I think I got a solution, but it doesn't involve using a with-clause, rather is a different approach. (I still dont know if its possible to solve using only with). The idea is to carry the value of (proj₁ f) x next to the proof that (proj₁ f) x ≡ (proj₁ f) x along the way.

  𝟚-equivalences-characterization: ∀ (f : 𝟚-type ≃ 𝟚-type) 
                                    → ((proj₁ f) ≡ id) ⊎ ((proj₁ f) ≡ permut-𝟚)

  𝟚-equivalences-characterizationf = (with ∘ decompose) f where
    decompose : 𝟚-type ≃ 𝟚-type
        → (Σ[ (⟨ f , f-isEquiv ⟩) ∈ (𝟚-type ≃ 𝟚-type) ] 
            ((Σ[ x ∈ 𝟚-type ] (f (inj₁ *) ≡ x)) × (Σ[ x ∈ 𝟚-type ] (f (inj₂ *) ≡ x)))) 
    decompose f = ⟨ f , ⟨ ⟨ (proj₁ f) (inj₁ *) , refl ⟩ , ⟨ ((proj₁ f) (inj₂ *)) , refl ⟩ ⟩ ⟩

    with : (h : Σ[ (⟨ f , f-isEquiv ⟩) ∈ (𝟚-type ≃ 𝟚-type) ]
            ((Σ[ x ∈ 𝟚-type ] (f (inj₁ *) ≡ x)) × (Σ[ x ∈ 𝟚-type ] (f (inj₂ *) ≡ x)))) 
        → ((proj₁ (proj₁ h)) ≡ id) ⊎ ((proj₁ (proj₁ h)) ≡ permut-𝟚)

decompose acts explicitly adding the information of (proj₁ f) (inj_x *) ≡ (inj_x *) with the corresponding proof, which is what I was missing using a "with" clause.

And "with" acts like the with cause, except now we actually have a proof that f (inj₁ *) ≡ (inj₁ *) (for example).

And now you can split with in cases, for example:

with ⟨ ⟨ f , f-isEquiv ⟩ , ⟨ ⟨ inj₁ * , f∘inj₁≡inj₁ ⟩ , 
                          ⟨ inj₂ * , f∘inj₂≡inj₂ ⟩ ⟩ ⟩ 
                             = inj₁ (funext f id (λ {(inj₁ *) → f∘inj₁≡inj₁ ; 
                                                     (inj₂ *) → f∘inj₂≡inj₂}))