JMeq.agda

{-# OPTIONS --without-K #-}
open import Agda.Primitive renaming (Set to Type)
open import Agda.Builtin.Equality
module JMeq where

data JMeq {ℓ} {A : Type ℓ} (a : A) : {B : Type ℓ} → B → Type (lsuc ℓ) where
  refl : JMeq a a

JMeq-rec
  : ∀ {ℓ} {A B : Type ℓ} (P : {A : Type ℓ} → A → Type ℓ) {x : A} {y : B}
  → P x → JMeq x y → P y
JMeq-rec P p refl = p

JMeq-refl
  : ∀ {ℓ} {A : Type ℓ} (P : {A : Type ℓ} → A → Type ℓ) {x : A} (p : P x)
  → JMeq-rec P p refl ≡ p
JMeq-refl P p = refl