    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Propositional (intensional) equality
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Relation.Binary.PropositionalEquality where

    open import Axiom.UniquenessOfIdentityProofs
    open import Function.Base using (id; _∘_)
    import Function.Dependent.Bundles as Dependent using (Func)
    open import Function.Indexed.Relation.Binary.Equality using (≡-setoid)
    open import Level using (Level; _⊔_)
    open import Relation.Nullary.Irrelevant using (Irrelevant)
    open import Relation.Nullary.Decidable using (yes; no; dec-yes-irr; dec-no)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Definitions using (DecidableEquality)
    open import Relation.Binary.Indexed.Heterogeneous
      using (IndexedSetoid)
    import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
      as Trivial using (indexedSetoid)

    private
      variable
        a b c ℓ p : Level
        A B C : Set a

    ------------------------------------------------------------------------
    -- Re-export contents modules that make up the parts

    open import Relation.Binary.PropositionalEquality.Core public
    open import Relation.Binary.PropositionalEquality.Properties public
    open import Relation.Binary.PropositionalEquality.Algebra public

    ------------------------------------------------------------------------
    -- Pointwise equality

    _→-setoid_ : ∀ (A : Set a) (B : Set b) → Setoid _ _
    A →-setoid B = ≡-setoid A (Trivial.indexedSetoid (setoid B))

    :→-to-Π : ∀ {A : Set a} {B : IndexedSetoid A b ℓ} →
              ((x : A) → IndexedSetoid.Carrier B x) →
              Dependent.Func (setoid A) B
    :→-to-Π {B = B} f = record
      { to = f
      ; cong = λ { refl → IndexedSetoid.refl B }
      }

    →-to-⟶ : ∀ {A : Set a} {B : Setoid b ℓ} →
             (A → Setoid.Carrier B) →
             Dependent.Func (setoid A) (Trivial.indexedSetoid B)
    →-to-⟶ = :→-to-Π

    ------------------------------------------------------------------------
    -- More complex rearrangement lemmas

    -- A lemma that is very similar to Lemma 2.4.3 from the HoTT book.

    naturality : ∀ {x y} {x≡y : x ≡ y} {f g : A → B}
                 (f≡g : ∀ x → f x ≡ g x) →
                 trans (cong f x≡y) (f≡g y) ≡ trans (f≡g x) (cong g x≡y)
    naturality {x = x} {x≡y = refl} f≡g =
      f≡g x               ≡⟨ sym (trans-reflʳ _) ⟩
      trans (f≡g x) refl  ∎
      where open ≡-Reasoning

    -- A lemma that is very similar to Corollary 2.4.4 from the HoTT book.

    cong-≡id : ∀ {f : A → A} {x : A} (f≡id : ∀ x → f x ≡ x) →
               cong f (f≡id x) ≡ f≡id (f x)
    cong-≡id {f = f} {x} f≡id = begin
      cong f fx≡x                                    ≡⟨ sym (trans-reflʳ _) ⟩
      trans (cong f fx≡x) refl                       ≡⟨ cong (trans _) (sym (trans-symʳ fx≡x)) ⟩
      trans (cong f fx≡x) (trans fx≡x (sym fx≡x))    ≡⟨ sym (trans-assoc (cong f fx≡x)) ⟩
      trans (trans (cong f fx≡x) fx≡x) (sym fx≡x)    ≡⟨ cong (λ p → trans p (sym _)) (naturality f≡id) ⟩
      trans (trans f²x≡x (cong id fx≡x)) (sym fx≡x)  ≡⟨ cong (λ p → trans (trans f²x≡x p) (sym fx≡x)) (cong-id _) ⟩
      trans (trans f²x≡x fx≡x) (sym fx≡x)            ≡⟨ trans-assoc f²x≡x ⟩
      trans f²x≡x (trans fx≡x (sym fx≡x))            ≡⟨ cong (trans _) (trans-symʳ fx≡x) ⟩
      trans f²x≡x refl                               ≡⟨ trans-reflʳ _ ⟩
      f≡id (f x)                                     ∎
      where open ≡-Reasoning; fx≡x = f≡id x; f²x≡x = f≡id (f x)

    module _ (_≟_ : DecidableEquality A) {x y : A} where

      ≡-≟-identity : (eq : x ≡ y) → x ≟ y ≡ yes eq
      ≡-≟-identity eq = dec-yes-irr (x ≟ y) (Decidable⇒UIP.≡-irrelevant _≟_) eq

      ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y
      ≢-≟-identity = dec-no (x ≟ y)

    ------------------------------------------------------------------------
    -- Inspect

    -- Inspect can be used when you want to pattern match on the result r
    -- of some expression e, and you also need to "remember" that r ≡ e.

    -- See README.Inspect for an explanation of how/why to use this.

    -- Normally (but not always) the new `with ... in` syntax described at
    -- https://agda.readthedocs.io/en/v2.6.4/language/with-abstraction.html#with-abstraction-equality
    -- can be used instead."

    record Reveal_·_is_ {A : Set a} {B : A → Set b}
                        (f : (x : A) → B x) (x : A) (y : B x) :
                        Set (a ⊔ b) where
      constructor [_]
      field eq : f x ≡ y

    inspect : ∀ {A : Set a} {B : A → Set b}
              (f : (x : A) → B x) (x : A) → Reveal f · x is f x
    inspect f x = [ refl ]

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.0

    isPropositional : Set a → Set a
    isPropositional = Irrelevant

    {-# WARNING_ON_USAGE isPropositional
    "Warning: isPropositional was deprecated in v2.0.
    Please use Relation.Nullary.Irrelevant instead. "
    #-}