------------------------------------------------------------------------
-- The Agda standard library
--
-- Results concerning uniqueness of identity proofs, with axiom K
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Axiom.UniquenessOfIdentityProofs.WithK where

open import Axiom.UniquenessOfIdentityProofs using (UIP)
open import Relation.Binary.PropositionalEquality.Core using (refl)

-- Axiom K implies UIP.

uip : ∀ {a} {A : Set a} → UIP A
uip refl refl = refl