From 8daae10575316c0b97e54868c7ba262bb1ef1e98 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 12 Jan 2025 15:47:14 +0530
Subject: [PATCH] Update Prelude.agda

make refl and lift instances
---
 Cubical/Foundations/Prelude.agda | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda
index 5559b748b..75ff805f7 100644
--- a/Cubical/Foundations/Prelude.agda
+++ b/Cubical/Foundations/Prelude.agda
@@ -43,9 +43,10 @@ private
     B : A → Type ℓ
     x y z w : A
 
-refl : x ≡ x
-refl {x = x} _ = x
-{-# INLINE refl #-}
+instance
+  refl : x ≡ x
+  refl {x = x} _ = x
+  {-# INLINE refl #-}
 
 sym : x ≡ y → y ≡ x
 sym p i = p (~ i)
@@ -638,3 +639,7 @@ liftExt x i = lift (x i)
 liftFun : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'}
   (f : A → B) → Lift {j = ℓ''} A → Lift {j = ℓ'''} B
 liftFun f (lift a) = lift (f a)
+
+instance
+  liftInstance : ⦃ A ⦄ → Lift A
+  liftInstance ⦃ a ⦄ = lift a