    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An equality postulate which evaluates
    ------------------------------------------------------------------------

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

    module Relation.Binary.PropositionalEquality.TrustMe where

    open import Agda.Builtin.TrustMe using (primTrustMe)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

    -- trustMe {x = x} {y = y} evaluates to refl if x and y are
    -- definitionally equal.

    trustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
    trustMe = primTrustMe

    -- "Erases" a proof. The original proof is not inspected. The
    -- resulting proof reduces to refl if the two sides are definitionally
    -- equal. Note that checking for definitional equality can be slow.

    erase : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y
    erase _ = trustMe

    -- A "postulate with a reduction": postulate[ a ↦ b ] a evaluates to b,
    -- while postulate[ a ↦ b ] a′ gets stuck if a′ is not definitionally
    -- equal to a. This can be used to define a postulate of type (x : A) → B x
    -- by only specifying the behaviour at B t for some t : A. Introduced in
    --
    --   Alan Jeffrey, Univalence via Agda's primTrustMe again
    --   23 January 2015
    --   https://lists.chalmers.se/pipermail/agda/2015/007418.html

    postulate[_↦_] : ∀ {a b} {A : Set a}{B : A → Set b} →
                      (t : A) → B t → (x : A) → B x
    postulate[ a ↦ b ] a′ with trustMe {x = a} {a′}
    postulate[ a ↦ b ] .a | refl = b