K-rule enunciation and proof

K-rule.agda

module K-rule where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

-- Enunciation of K-rule
K-rule : Set₁
K-rule = {A : Set}{x : A}(P : x ≡ x → Set)(p : P refl)(e : x ≡ x) → P e

-- Proof of K-rule
-- by pattern matching on x ≡ x (Coquand, 1992)
.K-rule-proof : {A : Set}{x : A}(P : x ≡ x → Set)(p : P refl)(e : x ≡ x) → P e
K-rule-proof P p refl = p