diff --git a/Cubical/Axiom/UniquenessOfIdentity.agda b/Cubical/Axiom/UniquenessOfIdentity.agda index f7a735cb35..66055179ca 100644 --- a/Cubical/Axiom/UniquenessOfIdentity.agda +++ b/Cubical/Axiom/UniquenessOfIdentity.agda @@ -50,8 +50,8 @@ module _ {A : Type ℓ} where ¬UIPType {ℓ} uip = false≢true (cong lower (transport-uip p (lift true))) where - B = Lift {j = ℓ} Bool - p = cong (Lift {j = ℓ}) (ua notEquiv) + B = Bool* + p = cong (Lift ℓ) (ua notEquiv) transport-uip : (p : B ≡ B) → ∀ b → transport p b ≡ b transport-uip = UIP→AxiomK uip _ B _ transportRefl diff --git a/Cubical/CW/Connected.agda b/Cubical/CW/Connected.agda index c85d2c85fb..a848e3c37b 100644 --- a/Cubical/CW/Connected.agda +++ b/Cubical/CW/Connected.agda @@ -583,38 +583,27 @@ module _ (A : ℕ → Type ℓ) (sk+c : yieldsCombinatorialConnectedCWskel A 0) collapse₁card (suc (suc x)) = AC.card (suc (suc x)) collapse₁CWskel : ℕ → Type _ - collapse₁CWskel zero = Lift ⊥ - collapse₁CWskel (suc zero) = Lift (Fin 1) + collapse₁CWskel zero = ⊥* + collapse₁CWskel (suc zero) = Unit* collapse₁CWskel (suc (suc n)) = A (suc (suc n)) collapse₁α : (n : ℕ) → Fin (collapse₁card n) × S⁻ n → collapse₁CWskel n - collapse₁α (suc zero) (x , p) = lift fzero + collapse₁α (suc zero) (x , p) = tt* collapse₁α (suc (suc n)) = AC.α (2 +ℕ n) connectedCWskel→ : yieldsConnectedCWskel collapse₁CWskel 0 - fst (fst connectedCWskel→) = collapse₁card - fst (snd (fst connectedCWskel→)) = collapse₁α - fst (snd (snd (fst connectedCWskel→))) = λ() - snd (snd (snd (fst connectedCWskel→))) zero = - isContr→Equiv (isOfHLevelLift 0 (inhProp→isContr fzero isPropFin1)) - ((inr fzero) - , (λ { (inr x) j → inr (isPropFin1 fzero x j) })) - snd (snd (snd (fst connectedCWskel→))) (suc zero) = - compEquiv (invEquiv (isoToEquiv e₁)) - (compEquiv (isoToEquiv (snd liftStr)) - (isoToEquiv (pushoutIso _ _ _ _ - (idEquiv _) LiftEquiv (idEquiv _) - (funExt cohₗ) (funExt cohᵣ)))) - where - -- Agda complains if these proofs are inlined... - cohₗ : (x : _) → collapse₁α 1 x ≡ collapse₁α 1 x - cohₗ (x , p) = refl - - cohᵣ : (x : Fin (fst liftStr) × Bool) → fst x ≡ fst x - cohᵣ x = refl - snd (snd (snd (fst connectedCWskel→))) (suc (suc n)) = AC.e (suc (suc n)) - snd connectedCWskel→ = refl , (λ _ → λ ()) + connectedCWskel→ .fst .fst = collapse₁card + connectedCWskel→ .fst .snd .fst = collapse₁α + connectedCWskel→ .fst .snd .snd .fst () + connectedCWskel→ .fst .snd .snd .snd zero = isContr→Equiv isContrUnit* (inr fzero , λ { (inr x) → cong inr (isPropFin1 fzero x) }) + connectedCWskel→ .fst .snd .snd .snd (suc zero) = isoToEquiv $ + A 2 Iso⟨ invIso e₁ ⟩ + Pushout (CW₁-discrete (A , sk) .fst ∘ AC.α 1) fst Iso⟨ liftStr .snd ⟩ + Pushout (λ _ → fzero) fst Iso⟨ pushoutIso _ _ _ _ (idEquiv _) (isContr→≃Unit* isContrFin1) (idEquiv _) refl refl ⟩ + Pushout (collapse₁α 1) fst ∎Iso + connectedCWskel→ .fst .snd .snd .snd (suc (suc n)) = AC.e (suc (suc n)) + connectedCWskel→ .snd = refl , λ _ () collapse₁Equiv : (n : ℕ) → realise (_ , sk) ≃ realise (_ , connectedCWskel→ .fst) @@ -1221,7 +1210,7 @@ makeConnectedCW {ℓ = ℓ} (suc n) {C = C} (cwsk , eqv) cA with C' zero (lt x) = ⊥* C' (suc m) (lt x) = Unit* C' m (eq x) = - Lift (SphereBouquet 2+n (A 2+n)) + Lift _ (SphereBouquet 2+n (A 2+n)) C' m (gt x) = C* m -- Basepoints (not needed, but useful) @@ -1364,7 +1353,7 @@ connectedCWContr : {ℓ : Level} (n m : ℕ) (l : m <ᵗ suc n) (X : Type ℓ) (cwX : isConnectedCW n X) → isContr (fst (fst cwX) (suc m)) connectedCWContr n zero l X cwX = subst isContr - (cong (Lift ∘ Fin) (sym ((snd (fst cwX)) .snd .fst)) + (cong (Lift _ ∘ Fin) (sym ((snd (fst cwX)) .snd .fst)) ∙ sym (ua (compEquiv (CW₁-discrete (connectedCWskel→CWskel (fst cwX))) LiftEquiv))) (isOfHLevelLift 0 (inhProp→isContr fzero isPropFin1)) @@ -1515,7 +1504,7 @@ module isFinitelyPresented-π'connectedCW-lemmas {ℓ : Level} lem : (α : FinSphereBouquetMap∙ (card Xˢᵏᵉˡ (suc (suc (suc n)))) (card Xˢᵏᵉˡ (suc (suc n))) (suc n)) - (e : fst X₄₊ₙ∙ ≡ Lift (cofib (fst α))) + (e : fst X₄₊ₙ∙ ≡ Lift _ (cofib (fst α))) → ∥ PathP (λ i → e (~ i)) (lift (inl tt)) x ∥₁ lem α e = TR.rec squash₁ ∣_∣₁ (isConnectedPathP _ isConX' _ _ .fst) diff --git a/Cubical/CW/HurewiczTheorem.agda b/Cubical/CW/HurewiczTheorem.agda index 031468afa5..adc63dc0f7 100644 --- a/Cubical/CW/HurewiczTheorem.agda +++ b/Cubical/CW/HurewiczTheorem.agda @@ -1249,7 +1249,7 @@ HurewiczTheorem n = Xᶜʷ = X , cw Xᶜʷ' = X , Xˢᵏᵉˡ' , (invEquiv (snd cw')) - liftLem : (A : CW ℓ-zero) (a : fst A) (e : isConnected 2 (Lift (fst A))) + liftLem : (A : CW ℓ-zero) (a : fst A) (e : isConnected 2 (Lift _ (fst A))) → Path (Σ[ A ∈ CW ℓ-zero ] (Σ[ a ∈ fst A ] isConnected 2 (fst A))) (A , a , subst (isConnected 2) (ua (invEquiv LiftEquiv)) e) ((CWLift ℓ-zero A) , (lift a , e)) diff --git a/Cubical/CW/Instances/Lift.agda b/Cubical/CW/Instances/Lift.agda index b009b478ef..8c6b9b5206 100644 --- a/Cubical/CW/Instances/Lift.agda +++ b/Cubical/CW/Instances/Lift.agda @@ -21,7 +21,7 @@ private module _ (ℓ : Level) where CWskelLift : CWskel ℓA → CWskel (ℓ-max ℓA ℓ) - fst (CWskelLift sk) n = Lift {j = ℓ} (fst sk n) + fst (CWskelLift sk) n = Lift ℓ (fst sk n) fst (snd (CWskelLift sk)) = CWskel-fields.card sk fst (snd (snd (CWskelLift sk))) n (x , a) = lift (CWskel-fields.α sk n (x , a)) @@ -33,7 +33,7 @@ module _ (ℓ : Level) where (pushoutEquiv _ _ _ _ (idEquiv _) LiftEquiv (idEquiv _) refl refl)) - hasCWskelLift : {A : Type ℓA} → hasCWskel A → hasCWskel (Lift {j = ℓ} A) + hasCWskelLift : {A : Type ℓA} → hasCWskel A → hasCWskel (Lift ℓ A) fst (hasCWskelLift (sk , e)) = CWskelLift sk snd (hasCWskelLift (sk , e)) = compEquiv (invEquiv LiftEquiv) @@ -41,7 +41,7 @@ module _ (ℓ : Level) where (invEquiv (isoToEquiv (SeqColimLift {ℓ = ℓ} _)))) CWLift : CW ℓA → CW (ℓ-max ℓA ℓ) - fst (CWLift (A , sk)) = Lift {j = ℓ} A + fst (CWLift (A , sk)) = Lift ℓ A snd (CWLift (A , sk)) = PT.map hasCWskelLift sk finCWskelLift : ∀ {n} → finCWskel ℓA n → finCWskel (ℓ-max ℓA ℓ) n @@ -52,12 +52,12 @@ module _ (ℓ : Level) where (compEquiv (_ , snd (snd sk) k) LiftEquiv) .snd hasFinCWskelLift : {A : Type ℓA} - → hasFinCWskel A → hasFinCWskel (Lift {j = ℓ} A) + → hasFinCWskel A → hasFinCWskel (Lift ℓ A) fst (hasFinCWskelLift (dim , sk , e)) = dim fst (snd (hasFinCWskelLift (dim , sk , e))) = finCWskelLift sk snd (snd (hasFinCWskelLift c)) = hasCWskelLift (hasFinCWskel→hasCWskel _ c) .snd finCWLift : finCW ℓA → finCW (ℓ-max ℓA ℓ) - fst (finCWLift (A , sk)) = Lift {j = ℓ} A + fst (finCWLift (A , sk)) = Lift ℓ A snd (finCWLift (A , sk)) = PT.map hasFinCWskelLift sk diff --git a/Cubical/CW/Instances/Pushout.agda b/Cubical/CW/Instances/Pushout.agda index 0a0005680b..4a7164a937 100644 --- a/Cubical/CW/Instances/Pushout.agda +++ b/Cubical/CW/Instances/Pushout.agda @@ -756,8 +756,11 @@ module _ {ℓ ℓ' : Level} (P : Type ℓ → Type ℓ') (P1 : P Unit*) (P0 : P (Ppush : (A B C : Type ℓ) (f : A → B) (g : A → C) → P A → P B → P C → P (Pushout f g)) where private - PFin1 : P (Lift (Fin 1)) - PFin1 = subst P (cong Lift (isoToPath Iso-Unit-Fin1)) P1 + L : Type → Type ℓ + L = Lift ℓ + + PFin1 : P (L (Fin 1)) + PFin1 = subst P (cong L (isoToPath Iso-Unit-Fin1)) P1 P⊎ : {B C : Type ℓ} → P B → P C → P (B ⊎ C) P⊎ {B = B} {C} pB pC = @@ -767,35 +770,35 @@ module _ {ℓ ℓ' : Level} (P : Type ℓ → Type ℓ') (P1 : P Unit*) (P0 : P PushoutEmptyDomainIso)) (Ppush ⊥* B C (λ ()) (λ ()) P0 pB pC) - PFin : (n : ℕ) → P (Lift (Fin n)) + PFin : (n : ℕ) → P (Lift _ (Fin n)) PFin zero = subst P - (cong Lift + (cong L (ua (propBiimpl→Equiv isProp⊥ (λ x → ⊥.rec (¬Fin0 x)) (λ()) ¬Fin0))) P0 PFin (suc n) = - subst P (cong Lift (sym (isoToPath Iso-Fin-Unit⊎Fin))) + subst P (cong (Lift _) (sym (isoToPath Iso-Fin-Unit⊎Fin))) (subst P (isoToPath (Lift⊎Iso ℓ)) (P⊎ P1 (PFin n))) - PS : (n : ℕ) → P (Lift (S⁻ n)) + PS : (n : ℕ) → P (L (S⁻ n)) PS zero = P0 - PS (suc zero) = subst P (cong Lift (isoToPath (invIso Iso-Bool-Fin2))) (PFin 2) + PS (suc zero) = subst P (cong L (isoToPath (invIso Iso-Bool-Fin2))) (PFin 2) PS (suc (suc n)) = subst P - (cong Lift (isoToPath (compIso PushoutSuspIsoSusp (invIso (IsoSucSphereSusp n))))) + (cong L (isoToPath (compIso PushoutSuspIsoSusp (invIso (IsoSucSphereSusp n))))) (subst P (isoToPath (LiftPushoutIso ℓ)) - (Ppush (Lift (S₊ n)) Unit* Unit* (λ _ → tt*) (λ _ → tt*) + (Ppush (L (S₊ n)) Unit* Unit* (λ _ → tt*) (λ _ → tt*) (PS (suc n)) P1 P1)) - PFin×S : (n m : ℕ) → P (Lift (Fin n × S⁻ m)) + PFin×S : (n m : ℕ) → P (L (Fin n × S⁻ m)) PFin×S zero m = - subst P (ua (compEquiv (uninhabEquiv (λ()) λ()) LiftEquiv)) P0 + subst P (ua (uninhabEquiv lower λ ())) P0 PFin×S (suc n) m = subst P (isoToPath is) (P⊎ (PS m) (PFin×S n m)) where - is : Iso (Lift (S⁻ m) ⊎ Lift (Fin n × S⁻ m)) - (Lift (Fin (suc n) × S⁻ m)) + is : Iso (L (S⁻ m) ⊎ L (Fin n × S⁻ m)) + (L (Fin (suc n) × S⁻ m)) is = compIso (Lift⊎Iso ℓ) (compIso (invIso LiftIso) @@ -815,7 +818,7 @@ module _ {ℓ ℓ' : Level} (P : Type ℓ → Type ℓ') (P1 : P Unit*) (P0 : P refl refl) (invEquiv (B .snd .snd .snd .snd n)))) (Ppush _ _ _ - (λ { (lift r) → CWskel-fields.α B n r}) (liftFun fst) + (λ { (lift r) → CWskel-fields.α B n r}) (liftMap fst) (PFin×S (CWskel-fields.card B n) n) (PCWskel B n) (PFin (CWskel-fields.card B n))) diff --git a/Cubical/Categories/Constructions/Lift.agda b/Cubical/Categories/Constructions/Lift.agda index 98611d424c..11463ae7c4 100644 --- a/Cubical/Categories/Constructions/Lift.agda +++ b/Cubical/Categories/Constructions/Lift.agda @@ -15,7 +15,7 @@ open Category module _ (C : Category ℓ ℓ') (ℓ'' : Level) where LiftHoms : Category ℓ (ℓ-max ℓ' ℓ'') LiftHoms .ob = C .ob - LiftHoms .Hom[_,_] A B = Lift {j = ℓ''} (C [ A , B ]) + LiftHoms .Hom[_,_] A B = Lift ℓ'' (C [ A , B ]) LiftHoms .id = lift (C .id) LiftHoms ._⋆_ f g = lift (f .lower ⋆⟨ C ⟩ g .lower) LiftHoms .⋆IdL f = cong lift (C .⋆IdL (f .lower)) diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index aab7f9b501..45213f2f1f 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -48,20 +48,20 @@ _[_,-] : (C : Category ℓ ℓ') → (c : C .ob)→ Functor C (SET ℓ') (C [ c ,-]) .F-seq _ _ = funExt λ _ → sym (C .⋆Assoc _ _ _) -- Lift functor -LiftF : Functor (SET ℓ) (SET (ℓ-max ℓ ℓ')) -LiftF {ℓ}{ℓ'} .F-ob A = (Lift {ℓ}{ℓ'} (A .fst)) , isOfHLevelLift 2 (A .snd) -LiftF .F-hom f x = lift (f (x .lower)) -LiftF .F-id = refl -LiftF .F-seq f g = funExt λ x → refl +LiftF : ∀ ℓ' → Functor (SET ℓ) (SET (ℓ-max ℓ ℓ')) +LiftF ℓ' .F-ob A = (Lift ℓ' (A .fst)) , isOfHLevelLift 2 (A .snd) +LiftF ℓ' .F-hom f x = lift (f (x .lower)) +LiftF ℓ' .F-id = refl +LiftF ℓ' .F-seq f g = funExt λ x → refl module _ {ℓ ℓ' : Level} where - isFullyFaithfulLiftF : isFullyFaithful (LiftF {ℓ} {ℓ'}) + isFullyFaithfulLiftF : isFullyFaithful (LiftF {ℓ} ℓ') isFullyFaithfulLiftF X Y = isoToIsEquiv LiftFIso where open Iso LiftFIso : Iso (X .fst → Y .fst) - (Lift {ℓ}{ℓ'} (X .fst) → Lift {ℓ}{ℓ'} (Y .fst)) - fun LiftFIso = LiftF .F-hom {X} {Y} + (Lift ℓ' (X .fst) → Lift ℓ' (Y .fst)) + fun LiftFIso = LiftF ℓ' .F-hom {X} {Y} inv LiftFIso = λ f x → f (lift x) .lower rightInv LiftFIso = λ _ → funExt λ _ → refl leftInv LiftFIso = λ _ → funExt λ _ → refl @@ -189,7 +189,7 @@ module _ {ℓ} where -- LiftF : SET ℓ → SET (ℓ-suc ℓ) preserves "small" limits -- i.e. limits over diagram shapes J : Category ℓ ℓ module _ {ℓ : Level} where - preservesLimitsLiftF : preservesLimits {ℓJ = ℓ} {ℓJ' = ℓ} (LiftF {ℓ} {ℓ-suc ℓ}) + preservesLimitsLiftF : preservesLimits {ℓJ = ℓ} {ℓJ' = ℓ} (LiftF {ℓ} (ℓ-suc ℓ)) preservesLimitsLiftF = preservesLimitsChar _ completeSET completeSETSuc @@ -209,7 +209,7 @@ module _ {ℓ : Level} where (λ x hx → funExt (λ d → cone≡ λ u → funExt (λ _ → sym (funExt⁻ (hx u) d)))) lowerCone : ∀ J D - → Cone (LiftF ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit) + → Cone (LiftF _ ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit) → Cone D (Unit* , isOfHLevelLift 2 isSetUnit) coneOut (lowerCone J D cc) v tt* = cc .coneOut v tt* .lower coneOutCommutes (lowerCone J D cc) e = @@ -217,14 +217,14 @@ module _ {ℓ : Level} where liftCone : ∀ J D → Cone D (Unit* , isOfHLevelLift 2 isSetUnit) - → Cone (LiftF ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit) + → Cone (LiftF _ ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit) coneOut (liftCone J D cc) v tt* = lift (cc .coneOut v tt*) coneOutCommutes (liftCone J D cc) e = funExt λ { tt* → cong lift (funExt⁻ (cc .coneOutCommutes e) tt*) } limSetIso : ∀ J D → CatIso (SET (ℓ-suc ℓ)) - (completeSETSuc J (LiftF ∘F D) .lim) - (LiftF .F-ob (completeSET J D .lim)) + (completeSETSuc J (LiftF _ ∘F D) .lim) + (LiftF _ .F-ob (completeSET J D .lim)) fst (limSetIso J D) cc = lift (lowerCone J D cc) cInv (snd (limSetIso J D)) cc = liftCone J D (cc .lower) sec (snd (limSetIso J D)) = funExt (λ _ → liftExt (cone≡ λ _ → refl)) diff --git a/Cubical/Categories/Presheaf/Morphism.agda b/Cubical/Categories/Presheaf/Morphism.agda index 425dc17680..387e25029e 100644 --- a/Cubical/Categories/Presheaf/Morphism.agda +++ b/Cubical/Categories/Presheaf/Morphism.agda @@ -48,7 +48,7 @@ module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'} PshHom : Type (ℓ-max (ℓ-max (ℓ-max ℓc ℓc') ℓp) ℓq) PshHom = PresheafCategory C (ℓ-max ℓp ℓq) - [ LiftF {ℓp}{ℓq} ∘F P , LiftF {ℓq}{ℓp} ∘F Q ∘F (F ^opF) ] + [ LiftF ℓq ∘F P , LiftF ℓp ∘F Q ∘F (F ^opF) ] module _ (h : PshHom) where -- This should define a functor on the category of elements diff --git a/Cubical/Categories/Presheaf/Properties.agda b/Cubical/Categories/Presheaf/Properties.agda index 221a844b79..306242bfcb 100644 --- a/Cubical/Categories/Presheaf/Properties.agda +++ b/Cubical/Categories/Presheaf/Properties.agda @@ -394,5 +394,5 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) -- Isomorphism between presheaves of different levels PshIso : (C : Category ℓ ℓ') (P : Presheaf C ℓS) (Q : Presheaf C ℓS') → Type _ -PshIso {ℓS = ℓS}{ℓS' = ℓS'} C P Q = - NatIso (LiftF {ℓ = ℓS}{ℓ' = ℓS'} ∘F P) (LiftF {ℓ = ℓS'}{ℓ' = ℓS} ∘F Q) +PshIso {ℓS = ℓS} {ℓS' = ℓS'} C P Q = + NatIso (LiftF ℓS' ∘F P) (LiftF ℓS ∘F Q) diff --git a/Cubical/Categories/Yoneda.agda b/Cubical/Categories/Yoneda.agda index a32f3849ca..f4915434a2 100644 --- a/Cubical/Categories/Yoneda.agda +++ b/Cubical/Categories/Yoneda.agda @@ -153,27 +153,27 @@ module _ {C : Category ℓ ℓ'} where -- A more universe-polymorphic Yoneda lemma yoneda* : {C : Category ℓ ℓ'}(F : Functor C (SET ℓ'')) → (c : Category.ob C) - → Iso ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-]) - , LiftF {ℓ''}{ℓ'} ∘F F ]) + → Iso ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF ℓ'' ∘F (C [ c ,-]) + , LiftF ℓ' ∘F F ]) (fst (F ⟅ c ⟆)) yoneda* {ℓ}{ℓ'}{ℓ''}{C} F c = - ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-]) - , LiftF {ℓ''}{ℓ'} ∘F F ]) + ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF ℓ'' ∘F (C [ c ,-]) + , LiftF ℓ' ∘F F ]) Iso⟨ the-iso ⟩ ((FUNCTOR (LiftHoms C ℓ'') (SET (ℓ-max ℓ' ℓ''))) [ (LiftHoms C ℓ'' [ c ,-]) - , LiftF {ℓ''}{ℓ'} ∘F (F ∘F lowerHoms C ℓ'') ]) - Iso⟨ yoneda (LiftF {ℓ''}{ℓ'} ∘F (F ∘F lowerHoms C ℓ'')) c ⟩ - Lift {ℓ''}{ℓ'} (fst (F ⟅ c ⟆)) + , LiftF ℓ' ∘F (F ∘F lowerHoms C ℓ'') ]) + Iso⟨ yoneda (LiftF ℓ' ∘F (F ∘F lowerHoms C ℓ'')) c ⟩ + Lift ℓ' (fst (F ⟅ c ⟆)) Iso⟨ invIso LiftIso ⟩ (fst (F ⟅ c ⟆)) ∎Iso where the-iso : Iso ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) - [ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-]) - , LiftF {ℓ''}{ℓ'} ∘F F ]) + [ LiftF ℓ'' ∘F (C [ c ,-]) + , LiftF ℓ' ∘F F ]) ((FUNCTOR (LiftHoms C ℓ'') (SET (ℓ-max ℓ' ℓ''))) [ (LiftHoms C ℓ'' [ c ,-]) - , LiftF {ℓ''}{ℓ'} ∘F (F ∘F lowerHoms C ℓ'') ]) + , LiftF ℓ' ∘F (F ∘F lowerHoms C ℓ'') ]) the-iso .fun α .N-ob d f = α .N-ob d f the-iso .fun α .N-hom g = α .N-hom (g .lower) the-iso .inv β .N-ob d f = β .N-ob d f @@ -184,22 +184,22 @@ yoneda* {ℓ}{ℓ'}{ℓ''}{C} F c = yonedaᴾ* : {C : Category ℓ ℓ'}(F : Functor (C ^op) (SET ℓ'')) → (c : Category.ob C) → Iso (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) - [ LiftF {ℓ'}{ℓ''} ∘F (C [-, c ]) - , LiftF {ℓ''}{ℓ'} ∘F F ]) + [ LiftF ℓ'' ∘F (C [-, c ]) + , LiftF ℓ' ∘F F ]) (fst (F ⟅ c ⟆)) yonedaᴾ* {ℓ}{ℓ'}{ℓ''}{C} F c = (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) - [ LiftF {ℓ'}{ℓ''} ∘F (C [-, c ]) , LiftF {ℓ''}{ℓ'} ∘F F ]) Iso⟨ the-iso ⟩ + [ LiftF ℓ'' ∘F (C [-, c ]) , LiftF ℓ' ∘F F ]) Iso⟨ the-iso ⟩ (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) - [ LiftF {ℓ'}{ℓ''} ∘F ((C ^op) [ c ,-]) - , LiftF {ℓ''}{ℓ'} ∘F F ]) Iso⟨ yoneda* F c ⟩ + [ LiftF ℓ'' ∘F ((C ^op) [ c ,-]) + , LiftF ℓ' ∘F F ]) Iso⟨ yoneda* F c ⟩ fst (F ⟅ c ⟆) ∎Iso where the-iso : Iso (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) - [ LiftF {ℓ'}{ℓ''} ∘F (C [-, c ]) , LiftF {ℓ''}{ℓ'} ∘F F ]) + [ LiftF ℓ'' ∘F (C [-, c ]) , LiftF ℓ' ∘F F ]) (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) - [ LiftF {ℓ'}{ℓ''} ∘F ((C ^op) [ c ,-]) , LiftF {ℓ''}{ℓ'} ∘F F ]) + [ LiftF ℓ'' ∘F ((C ^op) [ c ,-]) , LiftF ℓ' ∘F F ]) the-iso .fun α .N-ob = α .N-ob the-iso .fun α .N-hom = α .N-hom the-iso .inv β .N-ob = β .N-ob diff --git a/Cubical/Codata/M/Container.agda b/Cubical/Codata/M/Container.agda index 4dc647b50d..7afa22cf90 100644 --- a/Cubical/Codata/M/Container.agda +++ b/Cubical/Codata/M/Container.agda @@ -64,11 +64,11 @@ shift-chain = λ X,π -> ((λ x → X X,π (suc x)) ,, λ {n} → π X,π {suc n ------------------------------------------------------ Wₙ : ∀ {ℓ} -> Container ℓ -> ℕ -> Type ℓ -Wₙ S 0 = Lift Unit +Wₙ S 0 = Unit* Wₙ S (suc n) = P₀ S (Wₙ S n) πₙ : ∀ {ℓ} -> (S : Container ℓ) -> {n : ℕ} -> Wₙ S (suc n) -> Wₙ S n -πₙ {ℓ} S {0} _ = lift tt +πₙ {ℓ} S {0} _ = tt* πₙ S {suc n} = P₁ (πₙ S {n}) sequence : ∀ {ℓ} -> Container ℓ -> Chain ℓ diff --git a/Cubical/Codata/M/helper.agda b/Cubical/Codata/M/helper.agda index c71103771c..787879ee44 100644 --- a/Cubical/Codata/M/helper.agda +++ b/Cubical/Codata/M/helper.agda @@ -81,9 +81,9 @@ iso→fun-Injection-Iso-x isom {x} {y} = (λ x₁ → x₁ (lift tt)) (λ x → refl) (λ x → refl) ⟩ - (∀ (t : Lift Unit) -> (((fun isom) ∘ tempx) t ≡ ((fun isom) ∘ tempy) t)) + (∀ (t : Unit*) -> (((fun isom) ∘ tempx) t ≡ ((fun isom) ∘ tempy) t)) Iso⟨ iso→Pi-fun-Injection isom ⟩ - (∀ (t : Lift Unit) -> tempx t ≡ tempy t) + (∀ (t : Unit*) -> tempx t ≡ tempy t) Iso⟨ iso (λ x₁ → x₁ (lift tt)) (λ x₁ t → x₁) (λ x → refl) diff --git a/Cubical/Codata/M/itree.agda b/Cubical/Codata/M/itree.agda index 68c25c3680..6e9f4cee6c 100644 --- a/Cubical/Codata/M/itree.agda +++ b/Cubical/Codata/M/itree.agda @@ -29,12 +29,9 @@ delay-ret r = in-fun (inr r , λ ()) delay-tau : {R : Type₀} -> delay R -> delay R delay-tau S = in-fun (inl tt , λ x → S) --- Bottom element raised -data ⊥₁ : Type₁ where - -- TREES tree-S : (E : Type₀ -> Type₁) (R : Type₀) -> Container (ℓ-suc ℓ-zero) -tree-S E R = (R ⊎ (Σ[ A ∈ Type₀ ] (E A))) , (λ { (inl _) -> ⊥₁ ; (inr (A , e)) -> Lift A } ) +tree-S E R = (R ⊎ (Σ[ A ∈ Type₀ ] (E A))) , (λ { (inl _) -> ⊥* ; (inr (A , e)) -> Lift _ A } ) tree : (E : Type₀ -> Type₁) (R : Type₀) -> Type₁ tree E R = M (tree-S E R) @@ -51,7 +48,7 @@ tree-vis {A = A} e k = in-fun (inr (A , e) , λ { (lift x) -> k x } ) -- Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic itree-S : ∀ (E : Type₀ -> Type₁) (R : Type₀) -> Container (ℓ-suc ℓ-zero) -itree-S E R = ((Unit ⊎ R) ⊎ (Σ[ A ∈ Type₀ ] (E A))) , (λ { (inl (inl _)) -> Lift Unit ; (inl (inr _)) -> ⊥₁ ; (inr (A , e)) -> Lift A } ) +itree-S E R = ((Unit ⊎ R) ⊎ (Σ[ A ∈ Type₀ ] (E A))) , (λ { (inl (inl _)) -> Unit* ; (inl (inr _)) -> ⊥* ; (inr (A , e)) -> Lift _ A } ) itree : ∀ (E : Type₀ -> Type₁) (R : Type₀) -> Type₁ itree E R = M (itree-S E R) diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda index 315fb97694..7c1539a1eb 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda @@ -127,13 +127,13 @@ module _ (G : AbGroup ℓ) where HⁿSⁿ↓ n = ST.map λ f x → ΩEM+1→EM-gen (suc n) _ (cong f (toSusp (S₊∙ (suc n)) x)) private - liftMap : (n : ℕ) (f : S₊ (suc n) → EM G (suc n)) + liftMapEM : (n : ℕ) (f : S₊ (suc n) → EM G (suc n)) → S₊ (suc (suc n)) → EM G (suc (suc n)) - liftMap n f = SⁿFun n (0ₖ _) (EM→ΩEM+1 (suc n) ∘ f) + liftMapEM n f = SⁿFun n (0ₖ _) (EM→ΩEM+1 (suc n) ∘ f) HⁿSⁿ↑ : (n : ℕ) → coHom (suc n) G (S₊ (suc n)) → coHom (suc (suc n)) G (S₊ (suc (suc n))) - HⁿSⁿ↑ n = ST.map (liftMap n) + HⁿSⁿ↑ n = ST.map (liftMapEM n) Hⁿ[Sⁿ,G]≅Hⁿ⁺¹[Sⁿ⁺¹,G] : (n : ℕ) → AbGroupEquiv (coHomGr (suc n) G (S₊ (suc n))) @@ -168,8 +168,8 @@ module _ (G : AbGroup ℓ) where λ f → TR.rec (isProp→isOfHLevelSuc n (squash₂ _ _)) (λ q → cong ∣_∣₂ (funExt λ x → cong (ΩEM+1→EM (suc n)) - (cong-∙ (liftMap n f) (merid x) (sym (merid (ptSn _))) - ∙ cong (cong (liftMap n f) (merid x) ∙_) + (cong-∙ (liftMapEM n f) (merid x) (sym (merid (ptSn _))) + ∙ cong (cong (liftMapEM n f) (merid x) ∙_) (cong sym (cong (EM→ΩEM+1 (suc n)) q ∙ EM→ΩEM+1-0ₖ (suc n))) ∙ sym (rUnit _)) diff --git a/Cubical/Data/Bool/Base.agda b/Cubical/Data/Bool/Base.agda index 8200c8d1b1..a76fb2af20 100644 --- a/Cubical/Data/Bool/Base.agda +++ b/Cubical/Data/Bool/Base.agda @@ -86,15 +86,14 @@ dichotomyBoolSym true = inr refl -- Universe lifted booleans Bool* : ∀ {ℓ} → Type ℓ -Bool* = Lift Bool +Bool* {ℓ} = Lift _ Bool -true* : ∀ {ℓ} → Bool* {ℓ} +true* : Bool* {ℓ} true* = lift true -false* : ∀ {ℓ} → Bool* {ℓ} +false* : Bool* {ℓ} false* = lift false -- Pointed version Bool*∙ : ∀ {ℓ} → Σ[ X ∈ Type ℓ ] X -fst Bool*∙ = Bool* -snd Bool*∙ = true* +Bool*∙ = Bool* , true* diff --git a/Cubical/Data/Bool/Properties.agda b/Cubical/Data/Bool/Properties.agda index f31da973f3..42bccbd36d 100644 --- a/Cubical/Data/Bool/Properties.agda +++ b/Cubical/Data/Bool/Properties.agda @@ -66,11 +66,11 @@ K-Bool : (P : {b : Bool} → b ≡ b → Type ℓ) → (∀{b} → P {b} refl) → ∀{b} → (q : b ≡ b) → P q -K-Bool P Pr {false} = J (λ{ false q → P q ; true _ → Lift ⊥ }) Pr -K-Bool P Pr {true} = J (λ{ true q → P q ; false _ → Lift ⊥ }) Pr +K-Bool P Pr {false} = J (λ{ false q → P q ; true _ → ⊥* }) Pr +K-Bool P Pr {true} = J (λ{ true q → P q ; false _ → ⊥* }) Pr isSetBool : isSet Bool -isSetBool a b = J (λ _ p → ∀ q → p ≡ q) (K-Bool (refl ≡_) refl) +isSetBool a = J> K-Bool (refl ≡_) refl true≢false : ¬ true ≡ false true≢false p = subst (λ b → if b then Bool else ⊥) p true diff --git a/Cubical/Data/Empty/Base.agda b/Cubical/Data/Empty/Base.agda index 1a259eb27e..55a4a2ce7c 100644 --- a/Cubical/Data/Empty/Base.agda +++ b/Cubical/Data/Empty/Base.agda @@ -8,17 +8,17 @@ private data ⊥ : Type₀ where -⊥* : Type ℓ -⊥* = Lift ⊥ +⊥* : ∀ {ℓ} → Type ℓ +⊥* = Lift _ ⊥ rec : {A : Type ℓ} → ⊥ → A rec () -rec* : {A : Type ℓ} → ⊥* {ℓ = ℓ'} → A +rec* : {A : Type ℓ} → ⊥* {ℓ'} → A rec* () elim : {A : ⊥ → Type ℓ} → (x : ⊥) → A x elim () -elim* : {A : ⊥* {ℓ'} → Type ℓ} → (x : ⊥* {ℓ'}) → A x +elim* : {A : ⊥* {ℓ'} → Type ℓ} → (x : ⊥*) → A x elim* () diff --git a/Cubical/Data/Empty/Properties.agda b/Cubical/Data/Empty/Properties.agda index 2ff52f19fe..dc81d2710b 100644 --- a/Cubical/Data/Empty/Properties.agda +++ b/Cubical/Data/Empty/Properties.agda @@ -9,7 +9,7 @@ open import Cubical.Data.Empty.Base isProp⊥ : isProp ⊥ isProp⊥ () -isProp⊥* : ∀ {ℓ} → isProp {ℓ} ⊥* +isProp⊥* : ∀ {ℓ} → isProp (⊥* {ℓ}) isProp⊥* _ () isContr⊥→A : ∀ {ℓ} {A : Type ℓ} → isContr (⊥ → A) diff --git a/Cubical/Data/Fin/Inductive/Properties.agda b/Cubical/Data/Fin/Inductive/Properties.agda index badbaf1ba1..8ce2c63f28 100644 --- a/Cubical/Data/Fin/Inductive/Properties.agda +++ b/Cubical/Data/Fin/Inductive/Properties.agda @@ -19,7 +19,7 @@ open import Cubical.Data.Nat.Order.Inductive open import Cubical.Data.Fin.Base as FinOld hiding (Fin ; injectSuc ; fsuc ; fzero ; flast ; ¬Fin0 ; sumFinGen) open import Cubical.Data.Fin.Properties as FinOldProps - hiding (sumFinGen0 ; isSetFin ; sumFin-choose ; sumFinGenHom ; sumFinGenId) + hiding (sumFinGen0 ; isSetFin ; isContrFin1 ; sumFin-choose ; sumFinGenHom ; sumFinGenId) open import Cubical.Relation.Nullary @@ -146,6 +146,9 @@ isSetFin {n = n} = isPropFin1 : isProp (Fin 1) isPropFin1 (zero , tt) (zero , tt) = refl +isContrFin1 : isContr (Fin 1) +isContrFin1 = inhProp→isContr fzero isPropFin1 + DiscreteFin : ∀ {n} → Discrete (Fin n) DiscreteFin x y with discreteℕ (fst x) (fst y) ... | yes p = yes (Σ≡Prop (λ _ → isProp<ᵗ) p) diff --git a/Cubical/Data/FinSet/Binary/Small/Properties.agda b/Cubical/Data/FinSet/Binary/Small/Properties.agda index 7de1fc05c0..cdf616c615 100644 --- a/Cubical/Data/FinSet/Binary/Small/Properties.agda +++ b/Cubical/Data/FinSet/Binary/Small/Properties.agda @@ -38,12 +38,12 @@ isBinaryEl (un b c e i) (transp (λ j → ∥ Bool ≃ ua e (i ∨ ~ j) ∥₁) i (isBinaryEl c)) i -isBinaryEl' : ∀ ℓ b → isBinary (Lift {j = ℓ} (El b)) +isBinaryEl' : ∀ ℓ b → isBinary (Lift ℓ (El b)) isBinaryEl' ℓ ℕ₂ = ∣ LiftEquiv ∣₁ isBinaryEl' ℓ (un b c e i) = squash₁ - (transp (λ j → ∥ Bool ≃ Lift {j = ℓ} (ua e (i ∧ j)) ∥₁) (~ i) (isBinaryEl' ℓ b)) - (transp (λ j → ∥ Bool ≃ Lift {j = ℓ} (ua e (i ∨ ~ j)) ∥₁) i (isBinaryEl' ℓ c)) + (transp (λ j → ∥ Bool ≃ Lift ℓ (ua e (i ∧ j)) ∥₁) (~ i) (isBinaryEl' ℓ b)) + (transp (λ j → ∥ Bool ≃ Lift ℓ (ua e (i ∨ ~ j)) ∥₁) i (isBinaryEl' ℓ c)) i isPropIsSetEl : isOfHLevelDep 1 (λ b → isSet (El b)) @@ -108,8 +108,8 @@ structureᵤ = λ where where open FS.BinStructure - path : Lift Binary ≡ FS.Binary _ + path : Lift _ Binary ≡ FS.Binary _ path = ua (compEquiv (invEquiv LiftEquiv) reflect) - bs : FS.BinStructure (Lift Binary) + bs : FS.BinStructure (Lift _ Binary) bs = subst⁻ FS.BinStructure path FS.structure₀ diff --git a/Cubical/Data/FinSet/Properties.agda b/Cubical/Data/FinSet/Properties.agda index 169e9747aa..f10e7d432b 100644 --- a/Cubical/Data/FinSet/Properties.agda +++ b/Cubical/Data/FinSet/Properties.agda @@ -107,11 +107,11 @@ isFinSet⊥ = isFinSetFin isFinSetLift : {L L' : Level} → {A : Type L} → - isFinSet A → isFinSet (Lift {L}{L'} A) + isFinSet A → isFinSet (Lift L' A) fst (isFinSetLift {A = A} isFinSetA) = isFinSetA .fst snd (isFinSetLift {A = A} isFinSetA) = Prop.elim - {P = λ _ → ∥ Lift A ≃ Fin (isFinSetA .fst) ∥₁} + {P = λ _ → ∥ Lift _ A ≃ Fin (isFinSetA .fst) ∥₁} (λ [a] → isPropPropTrunc ) (λ A≅Fin → ∣ compEquiv (invEquiv (LiftEquiv {A = A})) A≅Fin ∣₁) (isFinSetA .snd) diff --git a/Cubical/Data/Graph/Examples.agda b/Cubical/Data/Graph/Examples.agda index 1d8670828e..927251b6b3 100644 --- a/Cubical/Data/Graph/Examples.agda +++ b/Cubical/Data/Graph/Examples.agda @@ -111,9 +111,9 @@ module _ {ℓv ℓe ℓv' ℓe'} where _⊎Gr_ : ∀ (G : Graph ℓv ℓe) (G' : Graph ℓv' ℓe') → Graph (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe') Node (G ⊎Gr G') = Node G ⊎ Node G' - Edge (G ⊎Gr G') (inl x) (inl y) = Lift {j = ℓe'} (Edge G x y) - Edge (G ⊎Gr G') (inr x) (inr y) = Lift {j = ℓe } (Edge G' x y) - Edge (G ⊎Gr G') _ _ = Lift ⊥ + Edge (G ⊎Gr G') (inl x) (inl y) = Lift ℓe' (Edge G x y) + Edge (G ⊎Gr G') (inr x) (inr y) = Lift ℓe (Edge G' x y) + Edge (G ⊎Gr G') _ _ = ⊥* record ⊎Diag ℓ (G : Graph ℓv ℓe) (G' : Graph ℓv' ℓe') : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe'))) where @@ -140,9 +140,9 @@ module _ {ℓv ℓe ℓv' ℓe'} where Node (G ×Gr G') = Node (fst G) × Node (fst G') Edge (G ×Gr G') (x , x') (y , y') with snd G x y | snd G' x' y' ... | yes _ | yes _ = Edge (fst G) x y ⊎ Edge (fst G') x' y' - ... | yes _ | no _ = Lift {j = ℓe } (Edge (fst G') x' y') - ... | no _ | yes _ = Lift {j = ℓe'} (Edge (fst G) x y) - ... | no _ | no _ = Lift ⊥ + ... | yes _ | no _ = Lift ℓe (Edge (fst G') x' y') + ... | no _ | yes _ = Lift ℓe' (Edge (fst G) x y) + ... | no _ | no _ = ⊥* record ×Diag ℓ (G : DecGraph ℓv ℓe) (G' : DecGraph ℓv' ℓe') : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max (ℓ-max ℓv ℓv') (ℓ-max ℓe ℓe'))) where diff --git a/Cubical/Data/Graph/Path.agda b/Cubical/Data/Graph/Path.agda index 17963c38a0..30845b55e4 100644 --- a/Cubical/Data/Graph/Path.agda +++ b/Cubical/Data/Graph/Path.agda @@ -57,7 +57,7 @@ module _ {G : Graph ℓv ℓe} where -- This is called ̂W (W-hat) in the paper PathWithLen : ℕ → Node G → Node G → Type (ℓ-max ℓv ℓe) - PathWithLen 0 v w = Lift {j = ℓe} (v ≡ w) + PathWithLen 0 v w = Lift ℓe (v ≡ w) PathWithLen (suc n) v w = Σ[ x ∈ Node G ] (Edge G v x × PathWithLen n x w) isSetPathWithLen : ∀ n v w → isSet (PathWithLen n v w) diff --git a/Cubical/Data/List/Dependent.agda b/Cubical/Data/List/Dependent.agda index a01333bde8..78691d298b 100644 --- a/Cubical/Data/List/Dependent.agda +++ b/Cubical/Data/List/Dependent.agda @@ -28,7 +28,7 @@ infixr 5 _∷_ -- Represent ListP via known operations in order to derive properties more easily. RepListP : ∀ {ℓA ℓB} {A : Type ℓA} (B : A → Type ℓB) (as : List A) → Type (ℓ-max ℓA ℓB) -RepListP B [] = Lift Unit +RepListP B [] = Unit* RepListP B (a ∷ as) = B a × RepListP B as isoRepListP : ∀ {ℓA ℓB} {A : Type ℓA} (B : A → Type ℓB) (as : List A) → ListP B as ≅ RepListP B as diff --git a/Cubical/Data/List/Properties.agda b/Cubical/Data/List/Properties.agda index 7a9e74119c..2b8f6d6451 100644 --- a/Cubical/Data/List/Properties.agda +++ b/Cubical/Data/List/Properties.agda @@ -66,9 +66,9 @@ module _ {ℓ} {A : Type ℓ} where module ListPath {ℓ} {A : Type ℓ} where Cover : List A → List A → Type ℓ - Cover [] [] = Lift Unit - Cover [] (_ ∷ _) = Lift ⊥ - Cover (_ ∷ _) [] = Lift ⊥ + Cover [] [] = Unit* + Cover [] (_ ∷ _) = ⊥* + Cover (_ ∷ _) [] = ⊥* Cover (x ∷ xs) (y ∷ ys) = (x ≡ y) × Cover xs ys reflCode : ∀ xs → Cover xs xs @@ -124,17 +124,17 @@ private x y : A xs ys : List A - caseList : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (n c : B) → List A → B - caseList n _ [] = n - caseList _ c (_ ∷ _) = c +caseList : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (n c : B) → List A → B +caseList n _ [] = n +caseList _ c (_ ∷ _) = c - safe-head : A → List A → A - safe-head x [] = x - safe-head _ (x ∷ _) = x +safe-head : A → List A → A +safe-head x [] = x +safe-head _ (x ∷ _) = x - safe-tail : List A → List A - safe-tail [] = [] - safe-tail (_ ∷ xs) = xs +safe-tail : List A → List A +safe-tail [] = [] +safe-tail (_ ∷ xs) = xs cons-inj₁ : x ∷ xs ≡ y ∷ ys → x ≡ y cons-inj₁ {x = x} p = cong (safe-head x) p @@ -152,10 +152,10 @@ snoc-inj₁ {xs = xs} {ys = ys} p = ∙∙ rev-rev _ ¬cons≡nil : ¬ (x ∷ xs ≡ []) -¬cons≡nil {_} {A} p = lower (subst (caseList (Lift ⊥) (List A)) p []) +¬cons≡nil p = lower (ListPath.encode _ _ p) ¬nil≡cons : ¬ ([] ≡ x ∷ xs) -¬nil≡cons {_} {A} p = lower (subst (caseList (List A) (Lift ⊥)) p []) +¬nil≡cons p = lower (ListPath.encode _ _ p) ¬snoc≡nil : ¬ (xs ∷ʳ x ≡ []) ¬snoc≡nil {xs = []} contra = ¬cons≡nil contra diff --git a/Cubical/Data/Maybe/Properties.agda b/Cubical/Data/Maybe/Properties.agda index 981d2852fb..2fb60d4fcc 100644 --- a/Cubical/Data/Maybe/Properties.agda +++ b/Cubical/Data/Maybe/Properties.agda @@ -10,7 +10,7 @@ open import Cubical.Foundations.Structure using (⟨_⟩) open import Cubical.Functions.Embedding using (isEmbedding) -open import Cubical.Data.Empty as ⊥ using (⊥; isProp⊥) +open import Cubical.Data.Empty as ⊥ using (⊥*; isProp⊥*) open import Cubical.Data.Unit open import Cubical.Data.Nat using (suc) open import Cubical.Data.Sum using (_⊎_; inl; inr) @@ -44,9 +44,9 @@ map-Maybe-id (just _) = refl -- Path space of Maybe type module MaybePath {ℓ} {A : Type ℓ} where Cover : Maybe A → Maybe A → Type ℓ - Cover nothing nothing = Lift Unit - Cover nothing (just _) = Lift ⊥ - Cover (just _) nothing = Lift ⊥ + Cover nothing nothing = Unit* + Cover nothing (just _) = ⊥* + Cover (just _) nothing = ⊥* Cover (just a) (just a') = a ≡ a' reflCode : (c : Maybe A) → Cover c c @@ -88,9 +88,9 @@ module MaybePath {ℓ} {A : Type ℓ} where isOfHLevelCover : (n : HLevel) → isOfHLevel (suc (suc n)) A → ∀ c c' → isOfHLevel (suc n) (Cover c c') - isOfHLevelCover n p nothing nothing = isOfHLevelLift (suc n) (isOfHLevelUnit (suc n)) - isOfHLevelCover n p nothing (just a') = isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isProp⊥) - isOfHLevelCover n p (just a) nothing = isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isProp⊥) + isOfHLevelCover n p nothing nothing = isOfHLevelUnit* (suc n) + isOfHLevelCover n p nothing (just a') = isProp→isOfHLevelSuc n isProp⊥* + isOfHLevelCover n p (just a) nothing = isProp→isOfHLevelSuc n isProp⊥* isOfHLevelCover n p (just a) (just a') = p a a' isOfHLevelMaybe : ∀ {ℓ} (n : HLevel) {A : Type ℓ} @@ -113,16 +113,16 @@ fromJust-def a nothing = a fromJust-def _ (just a) = a just-inj : (x y : A) → just x ≡ just y → x ≡ y -just-inj x _ eq = cong (fromJust-def x) eq +just-inj x y = MaybePath.encode _ _ isEmbedding-just : isEmbedding (just {A = A}) isEmbedding-just w z = MaybePath.Cover≃Path (just w) (just z) .snd ¬nothing≡just : ∀ {x : A} → ¬ (nothing ≡ just x) -¬nothing≡just {A = A} {x = x} p = lower (subst (caseMaybe (Maybe A) (Lift ⊥)) p (just x)) +¬nothing≡just p = lower (MaybePath.encode _ _ p) ¬just≡nothing : ∀ {x : A} → ¬ (just x ≡ nothing) -¬just≡nothing {A = A} {x = x} p = lower (subst (caseMaybe (Lift ⊥) (Maybe A)) p (just x)) +¬just≡nothing p = lower (MaybePath.encode _ _ p) isProp-x≡nothing : (x : Maybe A) → isProp (x ≡ nothing) isProp-x≡nothing nothing x w = diff --git a/Cubical/Data/Nat/Algebra.agda b/Cubical/Data/Nat/Algebra.agda index b69d75002f..70dfa091c5 100644 --- a/Cubical/Data/Nat/Algebra.agda +++ b/Cubical/Data/Nat/Algebra.agda @@ -136,7 +136,7 @@ module AlgebraHInit→Ind (N : NatAlgebra ℓ') ℓ (hinit : isNatHInitial N ( -- the fact that we have to lift the Carrier obstructs readability a bit -- this is the same algebra as N, but lifted into the correct universe LiftN : NatAlgebra (ℓ-max ℓ' ℓ) - Carrier LiftN = Lift {_} {ℓ} (N .Carrier) + Carrier LiftN = Lift ℓ (N .Carrier) alg-zero LiftN = lift (N .alg-zero) alg-suc LiftN = lift ∘ N .alg-suc ∘ lower diff --git a/Cubical/Data/Sigma/Properties.agda b/Cubical/Data/Sigma/Properties.agda index b07c203650..fa86e1ff6a 100644 --- a/Cubical/Data/Sigma/Properties.agda +++ b/Cubical/Data/Sigma/Properties.agda @@ -137,7 +137,7 @@ inv lUnit×Iso = tt ,_ rightInv lUnit×Iso _ = refl leftInv lUnit×Iso _ = refl -lUnit*×Iso : ∀{ℓ} → Iso (Unit* {ℓ} × A) A +lUnit*×Iso : Iso (Unit* {ℓ} × A) A fun lUnit*×Iso = snd inv lUnit*×Iso = tt* ,_ rightInv lUnit*×Iso _ = refl @@ -149,7 +149,7 @@ inv rUnit×Iso = _, tt rightInv rUnit×Iso _ = refl leftInv rUnit×Iso _ = refl -rUnit*×Iso : ∀{ℓ} → Iso (A × Unit* {ℓ}) A +rUnit*×Iso : Iso (A × Unit* {ℓ}) A fun rUnit*×Iso = fst inv rUnit*×Iso = _, tt* rightInv rUnit*×Iso _ = refl diff --git a/Cubical/Data/Sum/Properties.agda b/Cubical/Data/Sum/Properties.agda index 8ce0928e77..763c6b1d10 100644 --- a/Cubical/Data/Sum/Properties.agda +++ b/Cubical/Data/Sum/Properties.agda @@ -32,10 +32,10 @@ private module ⊎Path {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where Cover : A ⊎ B → A ⊎ B → Type (ℓ-max ℓ ℓ') - Cover (inl a) (inl a') = Lift {j = ℓ-max ℓ ℓ'} (a ≡ a') - Cover (inl _) (inr _) = Lift ⊥ - Cover (inr _) (inl _) = Lift ⊥ - Cover (inr b) (inr b') = Lift {j = ℓ-max ℓ ℓ'} (b ≡ b') + Cover (inl a) (inl a') = Lift ℓ' (a ≡ a') + Cover (inl _) (inr _) = ⊥* + Cover (inr _) (inl _) = ⊥* + Cover (inr b) (inr b') = Lift ℓ (b ≡ b') reflCode : (c : A ⊎ B) → Cover c c reflCode (inl a) = lift refl @@ -178,13 +178,13 @@ inv ⊎-IdL-⊥-Iso x = inr x rightInv ⊎-IdL-⊥-Iso _ = refl leftInv ⊎-IdL-⊥-Iso (inr _) = refl -⊎-IdL-⊥*-Iso : ∀{ℓ} → Iso (⊥* {ℓ} ⊎ A) A +⊎-IdL-⊥*-Iso : ∀ {ℓ} → Iso (⊥* {ℓ} ⊎ A) A fun ⊎-IdL-⊥*-Iso (inr x) = x inv ⊎-IdL-⊥*-Iso x = inr x rightInv ⊎-IdL-⊥*-Iso _ = refl leftInv ⊎-IdL-⊥*-Iso (inr _) = refl -⊎-IdR-⊥*-Iso : ∀{ℓ} → Iso (A ⊎ ⊥* {ℓ}) A +⊎-IdR-⊥*-Iso : ∀ {ℓ} → Iso (A ⊎ ⊥* {ℓ}) A fun ⊎-IdR-⊥*-Iso (inl x) = x inv ⊎-IdR-⊥*-Iso x = inl x rightInv ⊎-IdR-⊥*-Iso _ = refl @@ -196,10 +196,10 @@ leftInv ⊎-IdR-⊥*-Iso (inl _) = refl ⊎-IdL-⊥-≃ : ⊥ ⊎ A ≃ A ⊎-IdL-⊥-≃ = isoToEquiv ⊎-IdL-⊥-Iso -⊎-IdR-⊥*-≃ : ∀{ℓ} → A ⊎ ⊥* {ℓ} ≃ A +⊎-IdR-⊥*-≃ : ∀ {ℓ} → A ⊎ ⊥* {ℓ} ≃ A ⊎-IdR-⊥*-≃ = isoToEquiv ⊎-IdR-⊥*-Iso -⊎-IdL-⊥*-≃ : ∀{ℓ} → ⊥* {ℓ} ⊎ A ≃ A +⊎-IdL-⊥*-≃ : ∀ {ℓ} → ⊥* {ℓ} ⊎ A ≃ A ⊎-IdL-⊥*-≃ = isoToEquiv ⊎-IdL-⊥*-Iso Π⊎Iso : Iso ((x : A ⊎ B) → E x) (((a : A) → E (inl a)) × ((b : B) → E (inr b))) @@ -358,10 +358,10 @@ Iso⊎→Iso {A = A} {C = C} {B = B} {D = D} f e p = Iso' Iso.leftInv Iso' x = lem1 x (_ , refl) (_ , refl) Lift⊎Iso : ∀ (ℓ : Level) - → Iso (Lift {j = ℓ} A ⊎ Lift {j = ℓ} B) - (Lift {j = ℓ} (A ⊎ B)) -fun (Lift⊎Iso ℓD) (inl x) = liftFun inl x -fun (Lift⊎Iso ℓD) (inr x) = liftFun inr x + → Iso (Lift ℓ A ⊎ Lift ℓ B) + (Lift ℓ (A ⊎ B)) +fun (Lift⊎Iso ℓD) (inl x) = liftMap inl x +fun (Lift⊎Iso ℓD) (inr x) = liftMap inr x inv (Lift⊎Iso ℓD) (lift (inl x)) = inl (lift x) inv (Lift⊎Iso ℓD) (lift (inr x)) = inr (lift x) rightInv (Lift⊎Iso ℓD) (lift (inl x)) = refl diff --git a/Cubical/Data/Unit/Base.agda b/Cubical/Data/Unit/Base.agda index 8c1849acf0..4dca11655d 100644 --- a/Cubical/Data/Unit/Base.agda +++ b/Cubical/Data/Unit/Base.agda @@ -7,15 +7,14 @@ open import Agda.Builtin.Unit public renaming ( ⊤ to Unit ) -- Universe polymorphic version -Unit* : {ℓ : Level} → Type ℓ -Unit* = Lift Unit +Unit* : ∀ {ℓ} → Type ℓ +Unit* = Lift _ Unit pattern tt* = lift tt -- Pointed version Unit*∙ : ∀ {ℓ} → Σ[ X ∈ Type ℓ ] X -fst Unit*∙ = Unit* -snd Unit*∙ = tt* +Unit*∙ = Unit* , tt* -- Universe polymorphic version without definitional equality -- Allows us to "lock" proofs. See "Locking, unlocking" in diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 0c78a79647..25d33e4aba 100644 --- a/Cubical/Foundations/Equiv.agda +++ b/Cubical/Foundations/Equiv.agda @@ -173,11 +173,11 @@ compEquiv-assoc : (f : A ≃ B) (g : B ≃ C) (h : C ≃ D) → compEquiv f (compEquiv g h) ≡ compEquiv (compEquiv f g) h compEquiv-assoc f g h = equivEq refl -LiftEquiv : A ≃ Lift {i = ℓ} {j = ℓ'} A +LiftEquiv : A ≃ Lift ℓ' A LiftEquiv .fst a .lower = a LiftEquiv .snd .equiv-proof = strictContrFibers lower -Lift≃Lift : (e : A ≃ B) → Lift {j = ℓ'} A ≃ Lift {j = ℓ''} B +Lift≃Lift : (e : A ≃ B) → Lift ℓ' A ≃ Lift ℓ'' B Lift≃Lift e .fst a .lower = e .fst (a .lower) Lift≃Lift e .snd .equiv-proof b .fst .fst .lower = invEq e (b .lower) Lift≃Lift e .snd .equiv-proof b .fst .snd i .lower = diff --git a/Cubical/Foundations/HLevels.agda b/Cubical/Foundations/HLevels.agda index ab77a66d6b..e688d69da6 100644 --- a/Cubical/Foundations/HLevels.agda +++ b/Cubical/Foundations/HLevels.agda @@ -601,10 +601,10 @@ isGroupoidHSet = isOfHLevelTypeOfHLevel 2 -- h-level of lifted type -isOfHLevelLift : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} → isOfHLevel n A → isOfHLevel n (Lift {j = ℓ'} A) +isOfHLevelLift : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} → isOfHLevel n A → isOfHLevel n (Lift ℓ' A) isOfHLevelLift n = isOfHLevelRetract n lower lift λ _ → refl -isOfHLevelLower : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} → isOfHLevel n (Lift {j = ℓ'} A) → isOfHLevel n A +isOfHLevelLower : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} → isOfHLevel n (Lift ℓ' A) → isOfHLevel n A isOfHLevelLower n = isOfHLevelRetract n lift lower λ _ → refl ---------------------------- diff --git a/Cubical/Foundations/Isomorphism.agda b/Cubical/Foundations/Isomorphism.agda index e44bb1c41f..f7a0be42c1 100644 --- a/Cubical/Foundations/Isomorphism.agda +++ b/Cubical/Foundations/Isomorphism.agda @@ -161,7 +161,7 @@ inv (compIsoIdR isom i) = inv isom rightInv (compIsoIdR isom i) b = rUnit (isom .rightInv b) (~ i) leftInv (compIsoIdR isom i) a = lUnit (isom .leftInv a) (~ i) -LiftIso : Iso A (Lift {i = ℓ} {j = ℓ'} A) +LiftIso : Iso A (Lift ℓ' A) fun LiftIso = lift inv LiftIso = lower rightInv LiftIso _ = refl diff --git a/Cubical/Foundations/Pointed/Base.agda b/Cubical/Foundations/Pointed/Base.agda index 91a7f020af..4fdd2ef244 100644 --- a/Cubical/Foundations/Pointed/Base.agda +++ b/Cubical/Foundations/Pointed/Base.agda @@ -22,9 +22,8 @@ pt = str Pointed₀ = Pointed ℓ-zero -Lift∙ : ∀ {i j} → (A : Pointed i) → Pointed (ℓ-max i j) -fst (Lift∙ {j = j} A) = Lift {j = j} (typ A) -snd (Lift∙ A) = lift (pt A) +Lift∙ : ∀ ℓ' → (A : Pointed ℓ) → Pointed (ℓ-max ℓ ℓ') +Lift∙ ℓ' A = Lift ℓ' (typ A) , lift (pt A) {- Pointed functions -} _→∙_ : (A : Pointed ℓ) (B : Pointed ℓ') → Type (ℓ-max ℓ ℓ') @@ -59,6 +58,10 @@ compEquiv∙ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Po fst (compEquiv∙ e1 e2) = compEquiv (fst e1) (fst e2) snd (compEquiv∙ e1 e2) = cong (fst (fst e2)) (snd e1) ∙ snd e2 +Lift∙≃Lift∙ : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Pointed ℓ} {B : Pointed ℓ'} + → A ≃∙ B → Lift∙ ℓ'' A ≃∙ Lift∙ ℓ''' B +Lift∙≃Lift∙ (e , p) = Lift≃Lift e , liftExt p + Equiv∙J : {B : Pointed ℓ} (C : (A : Pointed ℓ) → A ≃∙ B → Type ℓ') → C B (idEquiv (fst B) , refl) → {A : _} (e : A ≃∙ B) → C A e diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda index 260be6bfb9..8e8dba1faf 100644 --- a/Cubical/Foundations/Prelude.agda +++ b/Cubical/Foundations/Prelude.agda @@ -638,16 +638,16 @@ isPropSinglP = isContr→isProp (isContrSinglP _ _) -- Universe lifting -record Lift {i j} (A : Type i) : Type (ℓ-max i j) where +record Lift ℓ' (A : Type ℓ) : Type (ℓ-max ℓ ℓ') where constructor lift field lower : A open Lift public -liftExt : ∀ {A : Type ℓ} {a b : Lift {ℓ} {ℓ'} A} → (lower a ≡ lower b) → a ≡ b -liftExt x i = lift (x i) +liftExt : ∀ {A : Type ℓ} {a b : Lift ℓ' A} → lower a ≡ lower b → a ≡ b +liftExt p i = lift (p i) -liftFun : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} - (f : A → B) → Lift {j = ℓ''} A → Lift {j = ℓ'''} B -liftFun f (lift a) = lift (f a) +liftMap : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} + (f : A → B) → Lift ℓ'' A → Lift ℓ''' B +liftMap f (lift a) = lift (f a) diff --git a/Cubical/Foundations/Univalence.agda b/Cubical/Foundations/Univalence.agda index 8802e7d32b..fbd7b57cbe 100644 --- a/Cubical/Foundations/Univalence.agda +++ b/Cubical/Foundations/Univalence.agda @@ -275,7 +275,7 @@ univalenceStatement = Univalence.thm eqweqmap eqweqmapid univalenceUAH : {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B) univalenceUAH = ( _ , univalenceStatement ) -univalencePath : {A B : Type ℓ} → (A ≡ B) ≡ Lift (A ≃ B) +univalencePath : {A B : Type ℓ} → (A ≡ B) ≡ Lift _ (A ≃ B) univalencePath = ua (compEquiv univalence LiftEquiv) -- Lemmas for constructing and destructing dependent paths in a function type where the domain is ua. diff --git a/Cubical/Functions/Embedding.agda b/Cubical/Functions/Embedding.agda index 27b7a26d32..0a19d81a56 100644 --- a/Cubical/Functions/Embedding.agda +++ b/Cubical/Functions/Embedding.agda @@ -317,8 +317,8 @@ universeEmbedding F liftingEquiv = hasPropFibersOfImage→isEmbedding propFibers propFibersF X = Embedding-into-isProp→isProp (Equiv→Embedding (fiberSingl X)) isPropSingl liftEmbedding : (ℓ ℓ' : Level) - → isEmbedding (Lift {i = ℓ} {j = ℓ'}) -liftEmbedding ℓ ℓ' = universeEmbedding (Lift {j = ℓ'}) (λ _ → invEquiv LiftEquiv) + → isEmbedding (Lift ℓ' :> (Type ℓ → Type (ℓ-max ℓ ℓ'))) +liftEmbedding ℓ ℓ' = universeEmbedding (Lift ℓ') (λ _ → invEquiv LiftEquiv) module FibrationIdentityPrinciple {B : Type ℓ} {ℓ'} where -- note that fibrationEquiv (for good reason) uses ℓ' = ℓ-max ℓ ℓ', so we have to work @@ -343,8 +343,8 @@ module FibrationIdentityPrinciple {B : Type ℓ} {ℓ'} where ■ -- Then embed into the above case by lifting the type - L : Type _ → Type _ -- local synonym fixing the levels of Lift - L = Lift {i = ℓ'} {j = ℓ} + L : Type ℓ' → Type _ -- local synonym fixing the levels of Lift + L = Lift ℓ liftFibration : Fibration B ℓ' → Fibration′ liftFibration (A , f) = L A , f ∘ lower @@ -366,10 +366,8 @@ module FibrationIdentityPrinciple {B : Type ℓ} {ℓ'} where ≃⟨ Σ-cong-equiv-snd (λ _ → Σ-cong-equiv-snd λ _ → pathToEquiv (PathP≡Path⁻ _ _ _)) ⟩ (Σ[ (E , eq) ∈ fiber L A ] fiber (_∘ lower) (transport⁻ (λ i → eq i → B) f)) ■ where - unquoteDecl boringSwap = - declStrictEquiv boringSwap - (λ ((E , g) , (eq , p)) → ((E , eq) , (g , p))) - (λ ((E , g) , (eq , p)) → ((E , eq) , (g , p))) + boringSwap = strictEquiv (λ ((E , g) , (eq , p)) → ((E , eq) , (g , p))) + (λ ((E , g) , (eq , p)) → ((E , eq) , (g , p))) isEmbeddingLiftFibration : isEmbedding liftFibration isEmbeddingLiftFibration = hasPropFibers→isEmbedding hasPropFibersLiftFibration diff --git a/Cubical/HITs/Colimit/Examples.agda b/Cubical/HITs/Colimit/Examples.agda index 17a6aaaac1..0a9e2947ef 100644 --- a/Cubical/HITs/Colimit/Examples.agda +++ b/Cubical/HITs/Colimit/Examples.agda @@ -17,9 +17,9 @@ open import Cubical.HITs.Pushout module _ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} where PushoutDiag : (A → B) → (A → C) → Diag (ℓ-max ℓ (ℓ-max ℓ' ℓ'')) ⇐⇒ - (PushoutDiag f g) $g fzero = Lift {j = ℓ-max ℓ ℓ'' } B - (PushoutDiag f g) $g fsuc fzero = Lift {j = ℓ-max ℓ' ℓ'' } A - (PushoutDiag f g) $g fsuc (fsuc fzero) = Lift {j = ℓ-max ℓ ℓ' } C + (PushoutDiag f g) $g fzero = Lift (ℓ-max ℓ ℓ'') B + (PushoutDiag f g) $g fsuc fzero = Lift (ℓ-max ℓ' ℓ'') A + (PushoutDiag f g) $g fsuc (fsuc fzero) = Lift (ℓ-max ℓ ℓ' ) C _<$g>_ (PushoutDiag f g) {fsuc fzero} {fzero} tt (lift a) = lift (f a) _<$g>_ (PushoutDiag f g) {fsuc fzero} {fsuc (fsuc fzero)} tt (lift a) = lift (g a) diff --git a/Cubical/HITs/CumulativeHierarchy/Constructions.agda b/Cubical/HITs/CumulativeHierarchy/Constructions.agda index fcf41a8ef5..a577961ad6 100644 --- a/Cubical/HITs/CumulativeHierarchy/Constructions.agda +++ b/Cubical/HITs/CumulativeHierarchy/Constructions.agda @@ -71,7 +71,7 @@ open SetPackage using (structure; ∈-rep; unpack; repack) module EmptySet where EmptyStructure : SetStructure ℓ - SetStructure.X EmptyStructure = Lift E.⊥ + SetStructure.X EmptyStructure = E.⊥* SetStructure.ix EmptyStructure () EmptyPackage : SetPackage ℓ ℓ-zero @@ -114,7 +114,7 @@ open UnionSet renaming (UNION to infixr 9 ⋃_) using (union-ax) public module PairingSet (a b : V ℓ) where PairingStructure : SetStructure ℓ - SetStructure.X PairingStructure = Lift Bool + SetStructure.X PairingStructure = Bool* SetStructure.ix PairingStructure (lift false) = a SetStructure.ix PairingStructure (lift true) = b @@ -139,8 +139,8 @@ open PairingSet renaming (PAIR to infix 12 ⁅_,_⁆) using (pairing-ax) public module SingletonSet (a : V ℓ) where SingletonStructure : SetStructure ℓ - SetStructure.X SingletonStructure = Lift Unit - SetStructure.ix SingletonStructure (lift tt) = a + SetStructure.X SingletonStructure = Unit* + SetStructure.ix SingletonStructure tt* = a SingletonPackage : SetPackage _ (ℓ-suc ℓ) structure SingletonPackage = SingletonStructure @@ -165,7 +165,7 @@ module InfinitySet {ℓ} where # suc n = sucV (# n) ωStructure : SetStructure ℓ - SetStructure.X ωStructure = Lift ℕ + SetStructure.X ωStructure = Lift ℓ ℕ SetStructure.ix ωStructure = #_ ∘ lower ω : V ℓ diff --git a/Cubical/HITs/James/Stable.agda b/Cubical/HITs/James/Stable.agda index 7749e464ba..b7b0cfa0f0 100644 --- a/Cubical/HITs/James/Stable.agda +++ b/Cubical/HITs/James/Stable.agda @@ -73,7 +73,7 @@ LoopSuspPushoutSquare : PushoutSquare LoopSuspPushoutSquare = (LoopSuspSquare , isContr→≃Unit* isContrPushout .snd) open PushoutPasteLeft LoopSuspPushoutSquare - (λ _ → lift {j = ℓ} tt) _ _ (funExt merid) + (λ _ → _ :> Unit* {ℓ}) _ _ (funExt merid) cofib-snd-James : cofib (λ (r : X × ΩΣX) → snd r) ≃ Susp ΩΣX cofib-snd-James = pushoutSwitchEquiv diff --git a/Cubical/HITs/ListedFiniteSet/Base.agda b/Cubical/HITs/ListedFiniteSet/Base.agda index 33cc0d13b7..ed1744d1fc 100644 --- a/Cubical/HITs/ListedFiniteSet/Base.agda +++ b/Cubical/HITs/ListedFiniteSet/Base.agda @@ -29,7 +29,7 @@ data LFSet (A : Type ℓ) : Type ℓ where -- at the end. -- We might want to avoid it, or come up with a more clever equational reasoning. _∈_ : {A : Type ℓ} → A → LFSet A → hProp ℓ -z ∈ [] = Lift ⊥.⊥ , isOfHLevelLift 1 isProp⊥ +z ∈ [] = ⊥.⊥* , isOfHLevelLift 1 isProp⊥ z ∈ (y ∷ xs) = (z ≡ₚ y) ⊔ (z ∈ xs) z ∈ dup x xs i = proof i where diff --git a/Cubical/HITs/Pushout/Properties.agda b/Cubical/HITs/Pushout/Properties.agda index 62f4d99d0d..f29157dea4 100644 --- a/Cubical/HITs/Pushout/Properties.agda +++ b/Cubical/HITs/Pushout/Properties.agda @@ -557,11 +557,11 @@ module _ {ℓ ℓ' ℓ'' : Level} (ℓ''' : Level) PushoutLevel = ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ'' ℓ''')) PushoutLift : Type PushoutLevel - PushoutLift = Pushout {A = Lift {j = ℓ-max ℓ' (ℓ-max ℓ'' ℓ''')} A} - {B = Lift {j = ℓ-max ℓ (ℓ-max ℓ'' ℓ''')} B} - {C = Lift {j = ℓ-max ℓ (ℓ-max ℓ' ℓ''')} C} - (liftFun f) - (liftFun g) + PushoutLift = Pushout {A = Lift (ℓ-max ℓ' (ℓ-max ℓ'' ℓ''')) A} + {B = Lift (ℓ-max ℓ (ℓ-max ℓ'' ℓ''')) B} + {C = Lift (ℓ-max ℓ (ℓ-max ℓ' ℓ''')) C} + (liftMap f) + (liftMap g) PushoutLiftIso : Iso (Pushout f g) PushoutLift Iso.fun PushoutLiftIso (inl x) = inl (lift x) @@ -744,14 +744,14 @@ PushoutCompEquivIso : ∀ {ℓA ℓA' ℓB ℓB' ℓC} PushoutCompEquivIso {ℓA = ℓA} {ℓA'} {ℓB} {ℓB'} {ℓC} e1 e2 f g = compIso (pushoutIso _ _ _ _ LiftEquiv LiftEquiv LiftEquiv refl refl) (compIso (PushoutCompEquivIso' {ℓ = ℓ*} {ℓ*} {ℓ*} - (liftEq ℓ* e1) (liftEq ℓ* e2) (liftFun f) (liftFun g)) + (liftEq ℓ* e1) (liftEq ℓ* e2) (liftMap f) (liftMap g)) (invIso (pushoutIso _ _ _ _ LiftEquiv LiftEquiv (LiftEquiv {ℓ' = ℓ*}) refl refl))) where ℓ* = ℓ-maxList (ℓA ∷ ℓA' ∷ ℓB ∷ ℓB' ∷ ℓC ∷ []) liftEq : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (ℓ* : Level) - → A ≃ B → Lift {j = ℓ*} A ≃ Lift {j = ℓ*} B + → A ≃ B → Lift ℓ* A ≃ Lift ℓ* B liftEq ℓ* e = compEquiv (invEquiv LiftEquiv) (compEquiv e LiftEquiv) PushoutCompEquivIso' : ∀ {ℓ ℓ' ℓ''} {A A' : Type ℓ} {B B' : Type ℓ'} {C : Type ℓ''} @@ -1185,9 +1185,9 @@ module PushoutPasteLeft {ℓ₀ ℓ₂ ℓ₄ ℓP ℓA ℓB : Level} help = M.isPushoutTotSquare→isPushoutBottomSquare (rotatePushoutSquare (_ , e) .snd) LiftPushoutIso : (ℓP : Level) {f : A → B} {g : A → C} - → Iso (Pushout (liftFun {ℓ'' = ℓP} {ℓ''' = ℓP} f) - (liftFun {ℓ'' = ℓP} {ℓ''' = ℓP} g)) - (Lift {j = ℓP} (Pushout f g)) + → Iso (Pushout (liftMap f :> (Lift ℓP A → Lift ℓP B)) + (liftMap g :> (Lift ℓP A → Lift ℓP C))) + (Lift ℓP (Pushout f g)) fun (LiftPushoutIso ℓP) (inl (lift x)) = lift (inl x) fun (LiftPushoutIso ℓP) (inr (lift x)) = lift (inr x) fun (LiftPushoutIso ℓP) (push (lift a) i) = lift (push a i) diff --git a/Cubical/HITs/SequentialColimit/Base.agda b/Cubical/HITs/SequentialColimit/Base.agda index 303b3edd7c..de5920c935 100644 --- a/Cubical/HITs/SequentialColimit/Base.agda +++ b/Cubical/HITs/SequentialColimit/Base.agda @@ -37,5 +37,5 @@ realiseSequenceMap (sequencemap map comm) (push {n = n} x i) = LiftSequence : ∀ {ℓA} (ℓ↑ : Level) (S : Sequence ℓA) → Sequence (ℓ-max ℓA ℓ↑) -obj (LiftSequence ℓ↑ S) n = Lift {j = ℓ↑} (obj S n) -map (LiftSequence ℓ↑ S) = liftFun (map S) +obj (LiftSequence ℓ↑ S) n = Lift ℓ↑ (obj S n) +map (LiftSequence ℓ↑ S) = liftMap (map S) diff --git a/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda b/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda index c83c327d38..d80da6d1fb 100644 --- a/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda +++ b/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda @@ -236,12 +236,12 @@ Iso.leftInv (⋀lIdIso {A = A}) = ⋀-fun≡ _ _ (sym (push (inl false*))) h hₗ λ x → compPath-filler (sym (push (inl false*))) (push (inr x)) where - h : (x : (Lift Bool) × fst A) → + h : (x : Bool* × fst A) → inr (false* , Bool⋀→ (inr x)) ≡ inr x h (lift false , a) = refl h (lift true , a) = sym (push (inl false*)) ∙ push (inr a) - hₗ : (x : Lift Bool) → + hₗ : (x : Bool*) → PathP (λ i → inr (false* , Bool⋀→ (push (inl x) i)) ≡ push (inl x) i) (λ i → push (inl false*) (~ i)) (h (x , pt A)) @@ -264,12 +264,12 @@ snd ⋀lIdEquiv∙ = refl , (sym (rUnit refl) ◁ (λ i j → snd f (~ i ∨ j)) ▷ lUnit (snd f))) where - h : (x : Lift Bool) (a : fst A) + h : (x : Bool*) (a : fst A) → Bool⋀→ (inr (x , fst f a)) ≡ fst f (Bool⋀→ (inr (x , a))) h (lift false) a = refl h (lift true) a = sym (snd f) - hₗ : (x : Lift Bool) + hₗ : (x : Bool*) → PathP (λ i → Bool⋀→ ((idfun∙ Bool*∙ ⋀→ f) (push (inl x) i)) ≡ fst f (Bool⋀→ (push (inl x) i))) (sym (snd f)) (h x (pt A)) @@ -308,17 +308,17 @@ snd ⋀lIdEquiv∙ = refl , (sym (rUnit refl) ◁ flipSquare (sym (rUnit refl)))) where - l₁ : (x : Lift Bool) → inl tt ≡ Bool⋀→ (inr (x , inl tt)) + l₁ : (x : Bool*) → inl tt ≡ Bool⋀→ (inr (x , inl tt)) l₁ (lift true) = refl l₁ (lift false) = refl - l₂ : (x : Lift Bool) (y : fst A × fst B) + l₂ : (x : Bool*) (y : fst A × fst B) → inr (Bool⋀→ (inr (x , fst y)) , snd y) ≡ Bool⋀→ (inr (x , inr y)) l₂ (lift true) y = sym (push (inr (snd y))) l₂ (lift false) y = refl - l₁≡l₂-left : (x : Lift Bool) (y : fst A) → + l₁≡l₂-left : (x : Bool*) (y : fst A) → PathP (λ i → l₁ x i ≡ l₂ x (y , pt B) i) (push (inl (Bool⋀→ (inr (x , y))))) λ i → Bool⋀→ {ℓ} {A = A ⋀∙ B} (inr (x , push (inl y) i)) @@ -326,7 +326,7 @@ snd ⋀lIdEquiv∙ = refl ◁ λ i j → push (inr (pt B)) (~ i ∧ j) l₁≡l₂-left (lift false) y = refl - l₁≡l₂-right : (x : Lift Bool) (y : fst B) + l₁≡l₂-right : (x : Bool*) (y : fst B) → PathP (λ i → l₁ x i ≡ l₂ x ((pt A) , y) i) (push (inr y) ∙ (λ i → inr (Bool⋀→ {A = A} (push (inl x) i) , y))) (λ i → Bool⋀→ {A = A ⋀∙ B} (inr (x , push (inr y) i))) @@ -334,7 +334,7 @@ snd ⋀lIdEquiv∙ = refl l₁≡l₂-right (lift true) y = sym (rUnit (push (inr y))) ◁ λ i j → push (inr y) (j ∧ ~ i) - mainᵣ : (x : Lift Bool) (y : A ⋀ B) + mainᵣ : (x : Bool*) (y : A ⋀ B) → (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B) (SmashAssocIso .Iso.fun (inr (x , y))) ≡ Bool⋀→ {ℓ} (inr (x , y)) @@ -353,7 +353,7 @@ snd ⋀lIdEquiv∙ = refl refl ◁ l₁≡l₂-right x y)) - mainᵣ-pt-coh : (x : Lift Bool) + mainᵣ-pt-coh : (x : Bool*) → PathP (λ i → inl tt ≡ Bool⋀→ (push (inl x) i)) refl (mainᵣ x (inl tt)) mainᵣ-pt-coh (lift false) = refl @@ -486,7 +486,7 @@ snd ⋀lIdEquiv∙ = refl ∙ (λ i → push (inr y) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , y))) ∙ sym (rUnit _))) - Fₗ≡refl : (x : Lift Bool) (y : fst B) → Fₗ .fst (inr (x , y)) ≡ refl + Fₗ≡refl : (x : Bool*) (y : fst B) → Fₗ .fst (inr (x , y)) ≡ refl Fₗ≡refl (lift false) y = (λ i → Fₗ-false y i ∙∙ refl ∙∙ sym (rUnit (push (inr y)) (~ i))) ∙ ∙∙lCancel _ @@ -501,7 +501,7 @@ snd ⋀lIdEquiv∙ = refl ∙ cong (_∙ sym (push (inr (pt B)))) (sym (lUnit (push (inr (pt B))))) ∙ rCancel _ - Fᵣ≡refl : (x : Lift Bool) (y : fst B) → Fᵣ .fst (inr (x , y)) ≡ refl + Fᵣ≡refl : (x : Bool*) (y : fst B) → Fᵣ .fst (inr (x , y)) ≡ refl Fᵣ≡refl x y = cong (push (inl (snd A)) ∙_) (sym (rUnit _) ∙ (λ i j → push (push tt (~ i)) (~ j))) diff --git a/Cubical/Homotopy/EilenbergSteenrod.agda b/Cubical/Homotopy/EilenbergSteenrod.agda index 89024834b8..cbe1bdd9c3 100644 --- a/Cubical/Homotopy/EilenbergSteenrod.agda +++ b/Cubical/Homotopy/EilenbergSteenrod.agda @@ -36,8 +36,7 @@ open import Cubical.Axiom.Choice record coHomTheory {ℓ ℓ' : Level} (H : (n : ℤ) → Pointed ℓ → AbGroup ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) where - Boolℓ : Pointed ℓ - Boolℓ = Lift Bool , lift true + field Hmap : (n : ℤ) → {A B : Pointed ℓ} (f : A →∙ B) → AbGroupHom (H n B) (H n A) HMapComp : (n : ℤ) → {A B C : Pointed ℓ} (g : B →∙ C) (f : A →∙ B) @@ -50,13 +49,12 @@ record coHomTheory {ℓ ℓ' : Level} (H : (n : ℤ) → Pointed ℓ → AbGroup Exactness : {A B : Pointed ℓ} (f : A →∙ B) (n : ℤ) → Ker (Hmap n f) ≡ Im (Hmap n {B = _ , inr (pt B)} (cfcod (fst f) , refl)) - Dimension : (n : ℤ) → ¬ n ≡ 0 → isContr (fst (H n Boolℓ)) + Dimension : (n : ℤ) → ¬ n ≡ 0 → isContr (fst (H n Bool*∙)) BinaryWedge : (n : ℤ) {A B : Pointed ℓ} → AbGroupEquiv (H n (A ⋁ B , (inl (pt A)))) (dirProdAb (H n A) (H n B)) record coHomTheoryGen {ℓ ℓ' : Level} (H : (n : ℤ) → Pointed ℓ → AbGroup ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) where - Boolℓ : Pointed ℓ - Boolℓ = Lift Bool , lift true + field Hmap : (n : ℤ) → {A B : Pointed ℓ} (f : A →∙ B) → AbGroupHom (H n B) (H n A) HMapComp : (n : ℤ) → {A B C : Pointed ℓ} (g : B →∙ C) (f : A →∙ B) @@ -70,7 +68,7 @@ record coHomTheoryGen {ℓ ℓ' : Level} (H : (n : ℤ) → Pointed ℓ → AbGr Exactness : {A B : Pointed ℓ} (f : A →∙ B) (n : ℤ) → Ker (Hmap n f) ≡ Im (Hmap n {B = _ , inr (pt B)} (cfcod (fst f) , refl)) - Dimension : (n : ℤ) → ¬ n ≡ 0 → isContr (fst (H n Boolℓ)) + Dimension : (n : ℤ) → ¬ n ≡ 0 → isContr (fst (H n Bool*∙)) Wedge : (n : ℤ) {I : Type ℓ} (satAC : satAC (ℓ-max ℓ ℓ') 2 I) {A : I → Pointed ℓ} → isEquiv {A = H n (⋁gen∙ I A) .fst} {B = ΠAbGroup (λ i → H n (A i)) .fst} diff --git a/Cubical/Homotopy/Group/Base.agda b/Cubical/Homotopy/Group/Base.agda index ab2cd2092c..732c4d8b06 100644 --- a/Cubical/Homotopy/Group/Base.agda +++ b/Cubical/Homotopy/Group/Base.agda @@ -644,7 +644,7 @@ snd (π'Gr≅πGr n A) = -- Proof that π'Gr preserves universe lifts π'GrLiftIso : ∀ {ℓ} (ℓ' : Level) {A : Pointed ℓ} (n : ℕ) - → GroupIso (π'Gr n (Lift∙ {j = ℓ'} A)) (π'Gr n A) + → GroupIso (π'Gr n (Lift∙ ℓ' A)) (π'Gr n A) fun (fst (π'GrLiftIso ℓ' n)) = sMap λ f → (λ x → lower (fst f x)) , (cong lower (snd f)) @@ -1080,10 +1080,8 @@ invEquiv∙idEquiv∙≡idEquiv = ΣPathP ((Σ≡Prop (λ _ → isPropIsEquiv _) , (cong-∙ lower (cong (lift ∘ (fst (fst e))) (snd f)) _)))))) (πA≃πB .snd) where - e' : Lift∙ {j = ℓ'} A ≃∙ Lift∙ {j = ℓ} B - fst e' = - compEquiv (invEquiv LiftEquiv) (compEquiv (fst e) LiftEquiv) - snd e' = cong lift (snd e) + e' : Lift∙ ℓ' A ≃∙ Lift∙ ℓ B + e' = Lift∙≃Lift∙ e main : ∀ {ℓ} {A B : Pointed ℓ} (n : ℕ) → (e : A ≃∙ B) @@ -1115,10 +1113,8 @@ invEquiv∙idEquiv∙≡idEquiv = ΣPathP ((Σ≡Prop (λ _ → isPropIsEquiv _) (compGroupHom (_ , main n e') (GroupIso→GroupHom (π'GrLiftIso _ n))) .snd) where - e' : Lift∙ {j = ℓ'} A ≃∙ Lift∙ {j = ℓ} B - fst e' = - compEquiv (invEquiv LiftEquiv) (compEquiv (fst e) LiftEquiv) - snd e' = cong lift (snd e) + e' : Lift∙ ℓ' A ≃∙ Lift∙ ℓ B + e' = Lift∙≃Lift∙ e main : ∀ {ℓ} {A B : Pointed ℓ} (n : ℕ) → (e : A ≃∙ B) diff --git a/Cubical/Structures/Maybe.agda b/Cubical/Structures/Maybe.agda index f375148a92..7bbac9833f 100644 --- a/Cubical/Structures/Maybe.agda +++ b/Cubical/Structures/Maybe.agda @@ -23,9 +23,9 @@ private ℓ ℓ₁ ℓ₁' : Level MaybeRel : {A B : Type ℓ} (R : A → B → Type ℓ₁) → Maybe A → Maybe B → Type ℓ₁ -MaybeRel R nothing nothing = Lift Unit -MaybeRel R nothing (just _) = Lift ⊥ -MaybeRel R (just _) nothing = Lift ⊥ +MaybeRel R nothing nothing = Unit* +MaybeRel R nothing (just _) = ⊥* +MaybeRel R (just _) nothing = ⊥* MaybeRel R (just x) (just y) = R x y congMaybeRel : {A B : Type ℓ} {R : A → B → Type ℓ₁} {S : A → B → Type ℓ₁'}