From 8b99d636b5d126ffc4acf5cdb02f6923e26adb25 Mon Sep 17 00:00:00 2001 From: Johnson He <40815177+hejohns@users.noreply.github.com> Date: Thu, 16 May 2024 10:25:41 -0400 Subject: [PATCH] Update to cubical HEAD * Cubical.Core.Everything was removed upstream * isFullyFaithfulLiftF got proved upstream https://github.com/agda/cubical/commit/b046b02b4277f3326daa2be2ba9faa4791f18392 --------- Co-authored-by: Johnson He --- Cubical/Categories/Instances/Sets/More.agda | 4 ---- Cubical/Data/Sigma/More.agda | 2 -- Cubical/Foundations/Isomorphism/More.agda | 2 -- 3 files changed, 8 deletions(-) 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