Enabling rewriting in Agda allows proving funext and K

Rewriting.agda

{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
import Agda.Builtin.Equality.Rewrite

private module _ {a} {A : Set a} where
  Path⇒≡ : (p : .Bool → A) → p false ≡ p true
  Path⇒≡ _ = refl

  module _ {x y} where
    ≡⇒Path : x ≡ y → .Bool → A
    ≡⇒Path refl _ = x

    ≡⇒Path-false : ∀ eq → ≡⇒Path eq false ≡ x
    ≡⇒Path-false refl = refl

    ≡⇒Path-true : ∀ eq → ≡⇒Path eq true ≡ y
    ≡⇒Path-true refl = refl

{-# REWRITE ≡⇒Path-false ≡⇒Path-true #-}

funext : ∀ {a b} {A : Set a} {B : A → Set b} {f g : ∀ x → B x} → (∀ x → f x ≡ g x) → f ≡ g
funext eqv = Path⇒≡ λ i x → ≡⇒Path (eqv x) i

K : ∀ {a} {A : Set a} {x : A} (x≡x : x ≡ x) → refl ≡ x≡x
K {x = x} x≡x = Path⇒≡ (≡⇒Path (K′ x≡x))
  where
    K′ : ∀ {y} (x≡y : x ≡ y) → Path⇒≡ (≡⇒Path x≡y) ≡ x≡y
    K′ refl = refl

Rewriting2.agda

{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

open import Agda.Primitive.Cubical
open import Agda.Builtin.Equality
import Agda.Builtin.Equality.Rewrite

data 𝕀 : Set where
  𝟘 𝟙 : 𝕀
  𝟘≡𝟙 : PathP _ 𝟘 𝟙

module _ {a} {A : Set a} where
  private module _ {x y} where
    ≡⇒Path : x ≡ y → 𝕀 → A
    ≡⇒Path refl _ = x

    ≡⇒Path-𝟘 : ∀ x≡y → ≡⇒Path x≡y 𝟘 ≡ x
    ≡⇒Path-𝟘 refl = refl

    ≡⇒Path-𝟘≡𝟙 : ∀ x≡y i → ≡⇒Path x≡y (𝟘≡𝟙 i) ≡ y
    ≡⇒Path-𝟘≡𝟙 refl _ = refl

    {-# REWRITE ≡⇒Path-𝟘 ≡⇒Path-𝟘≡𝟙 #-}

    ≡⇒Path-𝟘≡𝟙′ : ∀ x≡y i → ≡⇒Path x≡y (𝟘≡𝟙 i) ≡ y
    ≡⇒Path-𝟘≡𝟙′ x≡y i = refl

    K′ : ∀ x≡y → ≡⇒Path-𝟘≡𝟙′ x≡y i0 ≡ x≡y
    K′ refl = refl

  K : ∀ {x} (x≡x : x ≡ x) → refl ≡ x≡x
  K x≡x = K′ x≡x

Rewriting3.agda

{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

open import Agda.Builtin.Equality
import Agda.Builtin.Equality.Rewrite

private
  data Unit : Set where
    * : Unit

  opaque
    ∗ : Unit
    ∗ = *

module _ {a} {A : Set a} {x} where
  private module _ {y} where
    ≡⇒Path : x ≡ y → Unit → A
    ≡⇒Path refl _ = x

    ≡⇒Path-* : ∀ x≡y → ≡⇒Path x≡y * ≡ x
    ≡⇒Path-* refl = refl

    ≡⇒Path-∗ : ∀ x≡y → ≡⇒Path x≡y ∗ ≡ y
    ≡⇒Path-∗ refl = refl

    {-# REWRITE ≡⇒Path-* ≡⇒Path-∗ #-}

    opaque
      unfolding ∗

      ≡⇒Path-∗′ : ∀ x≡y → x ≡ ≡⇒Path x≡y ∗
      ≡⇒Path-∗′ x≡y = refl

      K′ : ∀ x≡y → ≡⇒Path-∗′ x≡y ≡ x≡y
      K′ refl = refl

  opaque
    unfolding ≡⇒Path-∗′

    K : (x≡x : x ≡ x) → refl ≡ x≡x
    K = K′