{-# 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₂