diff --git a/Cubical/Categories/Instances/Sets/More.agda b/Cubical/Categories/Instances/Sets/More.agda
index 8253ad58..151800f3 100644
--- a/Cubical/Categories/Instances/Sets/More.agda
+++ b/Cubical/Categories/Instances/Sets/More.agda
@@ -47,7 +47,3 @@ module _ {A}{B} (f : CatIso (SET ℓ) A B) a where
     ∙ transportRefl _
     ∙ transportRefl _
     ∙ cong (f .fst) (transportRefl _ ∙ transportRefl _ ))
-
-isFullyFaithfulLiftF : ∀ {ℓ ℓ'} → isFullyFaithful (LiftF {ℓ}{ℓ'})
-isFullyFaithfulLiftF x y =
-  isoToIsEquiv (iso _ (λ f x → f (lift x) .lower) (λ b → refl) λ _ → refl)
diff --git a/Cubical/Data/Sigma/More.agda b/Cubical/Data/Sigma/More.agda
index 7ae83feb..80edf8d2 100644
--- a/Cubical/Data/Sigma/More.agda
+++ b/Cubical/Data/Sigma/More.agda
@@ -6,8 +6,6 @@ module Cubical.Data.Sigma.More where
 
 open import Cubical.Data.Sigma.Base
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
diff --git a/Cubical/Foundations/Isomorphism/More.agda b/Cubical/Foundations/Isomorphism/More.agda
index 172ebb20..058388ce 100644
--- a/Cubical/Foundations/Isomorphism/More.agda
+++ b/Cubical/Foundations/Isomorphism/More.agda
@@ -1,8 +1,6 @@
 {-# OPTIONS --safe #-}
 module Cubical.Foundations.Isomorphism.More where
 
-open import Cubical.Core.Everything
-
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv.Base
 open import Cubical.Foundations.Isomorphism