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