Update Prelude.agda

make refl and lift instances
agda · Jan 12, 2025 · 8daae10 · 8daae10
1 parent 2f085f5
commit 8daae10
Showing 1 changed file with 8 additions and 3 deletions.
diff --git 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