There is one way to equat Unit, and two ways to equat Bool. Counting isomorphisms is fun.

BoolBoolBool.agda

{-# OPTIONS --safe --cubical #-}
module BoolBoolBool where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Bool

module M1 where
  -- there are four Bool → Bool functions
  data EndoBool : Set where
    EB-id    : EndoBool
    EB-true  : EndoBool
    EB-false : EndoBool
    EB-not   : EndoBool

  to : EndoBool → (Bool → Bool)
  to EB-id    = λ x → x
  to EB-true  = λ _ → true
  to EB-false = λ _ → false
  to EB-not   = not

  from' : Bool → Bool → EndoBool
  from' false false = EB-false
  from' false true  = EB-not
  from' true  false = EB-id
  from' true  true  = EB-true

  from : (Bool → Bool) → EndoBool
  from f = from' (f true) (f false)

  from∘to : (f : EndoBool) → from (to f) ≡ f
  from∘to EB-id    = refl
  from∘to EB-true  = refl
  from∘to EB-false = refl
  from∘to EB-not   = refl

  to∘from' : (f : Bool → Bool) → (x : Bool) → to (from' (f true) (f false)) x ≡ f x
  to∘from' f true with f true | f false
  ... | true  | true  = refl
  ... | true  | false = refl
  ... | false | true  = refl
  ... | false | false = refl
  to∘from' f false with f true | f false
  ... | true  | true  = refl
  ... | true  | false = refl
  ... | false | true  = refl
  ... | false | false = refl

  to∘from : (f : Bool → Bool) → to (from f) ≡ f
  to∘from f = funExt (to∘from' f)

  EndoBool≡Bool→Bool : EndoBool ≡ (Bool → Bool)
  EndoBool≡Bool→Bool = isoToPath (iso to from to∘from from∘to)

module M2 where
  boolId : Bool → Bool
  boolId x = x

  isEquivId : isEquiv boolId
  isEquivId = isoToIsEquiv (iso boolId boolId (λ _ → refl) (λ _ → refl))

  isEquivNot : isEquiv not
  isEquivNot = notIsEquiv

  to : Bool → Bool ≃ Bool
  to true  = boolId , isEquivId
  to false = not , notIsEquiv

  from : Bool ≃ Bool → Bool
  from f = fst f true

  from∘to : (b : Bool) → from (to b) ≡ b
  from∘to false = refl
  from∘to true  = refl

  split-bool : ∀ b → (b ≡ false) ⊎ (b ≡ true)
  split-bool false = inl refl
  split-bool true  = inr refl

  lemma1not' : ∀ (f : Bool → Bool) b → f true ≡ false → f false ≡ false → f b ≡ true → ⊥
  lemma1not' _ false ft ff fb = true≢false (sym fb ∙ ff)
  lemma1not' _ true  ft ff fb = true≢false (sym fb ∙ ft)

  lemma1id' : ∀ (f : Bool → Bool) b → f true ≡ true → f false ≡ true → f b ≡ false → ⊥
  lemma1id' _ false ft ff fb = false≢true (sym fb ∙ ff)
  lemma1id' _ true  ft ff fb = false≢true (sym fb ∙ ft)

  lemma1not : ∀ f → f true ≡ false → isEquiv f → ∀ b → not b ≡ f b
  lemma1not f ftrue eq true  = sym ftrue
  lemma1not f ftrue eq false with split-bool (f false)
  ... | inr p = sym p
  ... | inl p with equiv-proof eq true
  ... | (b , q) , _ = ⊥-elim (lemma1not' f b ftrue p q)

  lemma1id : ∀ f → f true ≡ true → isEquiv f → ∀ b → boolId b ≡ f b
  lemma1id f ftrue eq true = sym ftrue
  lemma1id f ftrue eq false with split-bool (f false)
  ... | inl p = sym p
  ... | inr p with equiv-proof eq false
  ... | (b , q) , _ = ⊥-elim (lemma1id' f b ftrue p q)

  lemma1 : (f : Bool → Bool) → isEquiv f → fst (to (f true)) ≡ f
  lemma1 f p with split-bool (f true)
  ... | inl q = funExt λ b → cong (λ z → fst (to z) b) q ∙ lemma1not f q p b
  ... | inr q = funExt λ b → cong (λ z → fst (to z) b) q ∙ lemma1id f q p b
  
  to∘from : (b : Bool ≃ Bool) → to (from b) ≡ b
  to∘from (f , p) = cong₂ _,_
    (lemma1 f p)
    (isProp→PathP {B = isEquiv} isPropIsEquiv (lemma1 f p) (snd (to (f true))) p)
  
  Bool≡Bool≃Bool : Bool ≡ (Bool ≃ Bool)
  Bool≡Bool≃Bool = isoToPath (iso to from to∘from from∘to)

  Bool≡Bool≡Bool : Lift Bool ≡ (Bool ≡ Bool)
  Bool≡Bool≡Bool = subst (λ T → Lift Bool ≡ T) refl (cong Lift Bool≡Bool≃Bool ∙ sym univalencePath)

UnitUnitUnit.agda

{-# OPTIONS --safe --cubical #-}
module UnitUnitUnit where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Unit

module Mx where
  isContrEndoUnit : isContr (Unit → Unit)
  isContrEndoUnit = (λ _ → tt) , λ _ → funExt (λ _ → refl)

  isPropEndoUnit : isProp (Unit → Unit)
  isPropEndoUnit = isContr→isProp isContrEndoUnit

  lemma : ∀ {A B : Set} → isContr A → isContr B → A ≡ B
  lemma (a , p) (b , q) = isoToPath (iso (λ _ → b) (λ _ → a) q p)

  lemma' : ∀ {A : Set} {B : Set₁} → isContr A → isContr B → Lift A ≡ B
  lemma' (a , p) (b , q) = isoToPath (iso (λ _ → b) (λ _ → lift a) q (λ { (lift x) → cong lift (p x) } ) )

  Unit≡Unit→Unit : Unit ≡ (Unit → Unit)
  Unit≡Unit→Unit = lemma isContrUnit isContrEndoUnit

  lemma2 : (i j : Iso Unit Unit) → i ≡ j
  lemma2 (iso f g p q) (iso f' g' p q') i
    = iso (isPropEndoUnit f f' i) (isPropEndoUnit g g' i)
      (λ r → isPropUnit _ _) (λ r → isPropUnit _ _)

  isContrUnitIso : isContr (Iso Unit Unit)
  isContrUnitIso = iso (λ x → x) (λ x → x) (λ _ → refl) (λ _ → refl) , lemma2 _

  idBool : Unit → Unit
  idBool x = x

  idTT : Unit → Unit
  idTT _ = tt

  isEquiv-idBool : isEquiv idBool
  isEquiv-idBool = record { equiv-proof = λ _ → (tt , isPropUnit _ _) , λ { (tt , f) i → refl i , isPropUnit _ _ } }

  isEquiv-idTT : isEquiv (λ _ → tt)
  isEquiv-idTT = record { equiv-proof = λ _ → (tt , isPropUnit _ _) , λ { (tt , f) i → refl i , isPropUnit _ _ } }

  isContrUnitEquiv : isContr (Unit ≃ Unit)
  isContrUnitEquiv
    = (idBool , isEquiv-idBool )
    , λ { (f , eq)  → cong₂ _,_ idTT' (isProp→PathP {B = isEquiv} (λ _ → isPropIsEquiv _) idTT' _ _)  }
    where
      idTT' : idTT ≡ idTT
      idTT' = refl

  module L {ℓ : Level} where
    LiftUnitEquiv : Type ℓ
    LiftUnitEquiv = Lift (Unit ≃ Unit)
    
    isContrLiftUnitEquiv : isContr LiftUnitEquiv
    isContrLiftUnitEquiv = isOfHLevelLift 0 isContrUnitEquiv

  isContrUnit≡ : isContr (Unit ≡ Unit)
  isContrUnit≡ = subst isContr (sym univalencePath) L.isContrLiftUnitEquiv

  Unit≡Unit≡Unit : Lift Unit ≡ (Unit ≡ Unit)
  Unit≡Unit≡Unit = lemma' isContrUnit isContrUnit≡