chore: make level arguments explicit pt 1

Author: anshwad10

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,15 +33,15 @@ 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)
       (compEquiv e
        (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

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,22 +209,22 @@ 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 =
       funExt λ { tt* → cong lower (funExt⁻ (cc .coneOutCommutes e) tt*) }
 
     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))

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*

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

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* ()

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)

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

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 =

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

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