-- Some definitions which simplify the calculations done elsewhere.

{-# OPTIONS --universe-polymorphism #-}

module Derivation where

open import Data.Product
open import Level
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality

EqualTo : ∀ {ℓ} {A : Set ℓ} (x : A) → Set ℓ
EqualTo x = ∃ (λ y → x ≡ y)

infix 0 ▷_ ▶_

▷_ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → EqualTo x
▷ eq = (_ , eq)

▶_ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≅ y → EqualTo x
▶ eq = (_ , ≅-to-≡ eq)

witness : ∀ {ℓ} {A : Set ℓ} {x : A} → EqualTo x → A
witness = proj₁

proof : ∀ {ℓ} {A : Set ℓ} {x : A} → (eq : EqualTo x) → x ≡ witness eq
proof = proj₂