open import Data.Product
open import Agda.Primitive 
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

_≡ₗ_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set (lsuc ℓ)
_≡ₗ_ {ℓ} {A} a a' = ∀ (P : A → Set ℓ) → ((P a → P a') × (P a' → P a)  )

lemma : ∀ {A : Set} (a : A) (a' : A) → a ≡ a' → a ≡ₗ a'
lemma a b refl _ = (λ Pa → Pa) , λ Pa' → Pa'

ammel : ∀ {A : Set} (a : A) (a' : A) → a ≡ₗ a' → a ≡ a'
ammel a a' a≡ₗa' with a≡ₗa' (λ x → a ≡ x)
... | a≡a→a≡a' , _ = a≡a→a≡a' refl