Don't match on Set

bad.agda

module foo where 
    data ⊘ : Set where
    data ⊤ : Set where tt : ⊤
    open import Cubical.Data.Bool
    open import Cubical.Foundations.Isomorphism  
    open import Cubical.Foundations.Prelude 
 
    postulate 
        f : Set → Bool
        reduction₁ : f (⊤ × ⊤) ≡ true
        reduction₂ : f (⊤) ≡ false

        f' : Set → Set 
        reduction₃ : f' (⊤ × ⊤) ≡ ⊤ 
        reduciton₄ : f' (⊤) ≡ ⊘

    ⊤≡⊤×⊤ : ⊤ ≡ ⊤ × ⊤ 
    ⊤≡⊤×⊤ = isoToPath (iso (λ _ → tt , tt) (λ x → tt) (λ{ (tt , tt) → refl}) λ{tt → refl})

    oops : true ≡ false
    oops = true         ≡⟨ sym reduction₁ ⟩ 
           f (⊤ × ⊤)    ≡⟨ cong f (sym ⊤≡⊤×⊤) ⟩ 
           f ⊤          ≡⟨ reduction₂ ⟩ 
           false        ∎

    oops' : ⊤ ≡ ⊘ 
    oops' = ⊤           ≡⟨ sym reduction₃ ⟩ 
            f' (⊤ × ⊤)  ≡⟨ cong f' (sym  ⊤≡⊤×⊤) ⟩
            f' ⊤        ≡⟨ reduciton₄ ⟩ 
            ⊘           ∎