Elementary proof that Bool is a Set
Here is the encode-decode method that L. Garde suggests (in cubical Agda):

{-# OPTIONS --cubical --safe --postfix-projections #-}

module Hmm where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Empty
open import Cubical.Data.Unit

data ℕ₂ : Type₀ where
  0₂ 1₂ : ℕ₂

Code : ℕ₂ → ℕ₂ → Type₀
Code 0₂ 0₂ = Unit
Code 1₂ 1₂ = Unit
Code m  n  = ⊥

Crefl : ∀{m} → Code m m
Crefl {0₂} = tt
Crefl {1₂} = tt

decode : ∀ m n → Code m n → m ≡ n
decode 0₂ 0₂ c = refl
decode 1₂ 1₂ c = refl

encode : ∀ m n → m ≡ n → Code m n
encode m n p = transport (λ i → Code m (p i)) Crefl

decode-encode : ∀ m n p → decode m n (encode m n p) ≡ p
decode-encode m n p
  = J (λ z q → decode m z (encode m z q) ≡ q) (lemma m) p
  where
  lemma : ∀ m → decode m m (encode m m refl) ≡ refl
  lemma 0₂ = refl
  lemma 1₂ = refl

encode-decode : ∀ m n c → encode m n (decode m n c) ≡ c
encode-decode 0₂ 0₂ c = refl
encode-decode 1₂ 1₂ c = refl

Cprop : ∀ m n → isProp (Code m n)
Cprop 0₂ 0₂ = isPropUnit
Cprop 1₂ 1₂ = isPropUnit

ℕ₂set : isSet ℕ₂
ℕ₂set m n = transport (λ i → isProp (p i)) (Cprop m n)
  where
  p : Code m n ≡ (m ≡ n)
  p = isoToPath (iso (decode m n) (encode m n)
                   (decode-encode m n) (encode-decode m n))