chore: make level arguments explicit pt 3

Author: anshwad10

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 ℓ

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)

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)

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
 

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}