Update to cubical HEAD

* Cubical.Core.Everything was removed upstream * isFullyFaithfulLiftF got proved upstream agda/cubical@b046b02 --------- Co-authored-by: Johnson He <[email protected]>
maxsnew · May 16, 2024 · 8b99d63 · 8b99d63
1 parent 2297acf
commit 8b99d63
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 8 deletions.
diff --git 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
@@ -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
@@ -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