eq-dec => UIP proof taken from https://sympa.inria.fr/sympa/arc/coq-club/2016-09/msg00064.html

UIP.agda

{-# OPTIONS --without-K #-}

module UIP where

open import Level
open import Relation.Binary.PropositionalEquality

record Canonical {ℓ} {ℓ′} (A : Set ℓ) (B : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  field canonical  : A → B
        constraint : ∀ a a′ →  canonical a ≡ canonical a′
open Canonical

open import Data.Empty
open import Relation.Nullary
open import Relation.Binary

module _ {ℓ} {A : Set ℓ} where

  eqdec-canonical : Decidable {A = A} _≡_ →
    ∀ {x y : A} → Canonical (x ≡ y) (x ≡ y)
  eqdec-canonical dec {x} {y} = record
    { canonical  = canon
    ; constraint = equal } where

    canon : x ≡ y → x ≡ y
    canon eq with dec x y
    ... | yes p = p
    ... | no ¬p = ⊥-elim (¬p eq)

    equal : ∀ a a′ → canon a ≡ canon a′
    equal a a′ with dec x y
    ... | yes p = refl
    ... | no ¬p = ⊥-elim (¬p a)

  quasi-UIP : ∀ {x y : A} (e : x ≡ y) → trans (sym e) e ≡ refl
  quasi-UIP refl = refl

  module _ (c : ∀ {x y : A} → Canonical (x ≡ y) (x ≡ y)) where

    eq-expand : ∀ {x y : A} (e : x ≡ y) →
      trans (sym (canonical c refl)) (canonical c e) ≡ e
    eq-expand e rewrite e = quasi-UIP (canonical c refl)

    UIP : ∀ {x y : A} (e f : x ≡ y) → e ≡ f
    UIP e f rewrite sym (eq-expand e)
                  | sym (eq-expand f)
                  | constraint c e f = refl

  eqdec-UIP : Decidable {A = A} _≡_ →
    ∀ {x y : A} (e f : x ≡ y) → e ≡ f
  eqdec-UIP d = UIP (eqdec-canonical d)