chore: excise hlevel tactic

src/1Lab/Classical.lagda.md

@@ -46,16 +46,16 @@ We show that these two statements are equivalent propositions.
 
 ```agda
 LEM-is-prop : is-prop LEM
-LEM-is-prop = hlevel!
+LEM-is-prop = hlevel 1
 
 DNE-is-prop : is-prop DNE
-DNE-is-prop = hlevel!
+DNE-is-prop = hlevel 1
 
 LEM→DNE : LEM → DNE
 LEM→DNE lem P = Dec-elim _ (λ p _ → p) (λ ¬p ¬¬p → absurd (¬¬p ¬p)) (lem P)
 
 DNE→LEM : DNE → LEM
-DNE→LEM dne P = dne (el (Dec ∣ P ∣) hlevel!) λ k → k (no λ p → k (yes p))
+DNE→LEM dne P = dne (el (Dec ∣ P ∣) (hlevel 1)) λ k → k (no λ p → k (yes p))
 
 LEM≃DNE : LEM ≃ DNE
 LEM≃DNE = prop-ext LEM-is-prop DNE-is-prop LEM→DNE DNE→LEM
@@ -84,7 +84,7 @@ The weak law of excluded middle is also a proposition.
 
 ```agda
 WLEM-is-prop : is-prop WLEM
-WLEM-is-prop = hlevel!
+WLEM-is-prop = hlevel 1
 ```
 
 ## The axiom of choice {defines="axiom-of-choice"}
@@ -151,7 +151,7 @@ gives us a section $\Sigma P \to 2$.
 ```agda
 module _ (split : Surjections-split) (P : Ω) where
   section : ∥ ((x : Susp ∣ P ∣) → fibre 2→Σ x) ∥
-  section = split Bool-is-set (Susp-prop-is-set hlevel!) 2→Σ 2→Σ-surjective
+  section = split Bool-is-set (Susp-prop-is-set (hlevel 1)) 2→Σ 2→Σ-surjective
 ```
 
 But a section is always injective, and the booleans are [[discrete]], so we can
@@ -160,11 +160,11 @@ is equivalent to $P$, this concludes the proof.
 
 ```agda
   Discrete-ΣP : Discrete (Susp ∣ P ∣)
-  Discrete-ΣP = ∥-∥-rec (Dec-is-hlevel 1 (Susp-prop-is-set hlevel! _ _))
+  Discrete-ΣP = ∥-∥-rec (Dec-is-hlevel 1 (Susp-prop-is-set (hlevel 1) _ _))
     (λ f → Discrete-inj (fst ∘ f) (right-inverse→injective 2→Σ (snd ∘ f))
                         Discrete-Bool)
     section
 
   AC→LEM : Dec ∣ P ∣
-  AC→LEM = Dec-≃ (Susp-prop-path hlevel!) Discrete-ΣP
+  AC→LEM = Dec-≃ (Susp-prop-path (hlevel 1)) Discrete-ΣP
 ```

src/1Lab/Equiv/HalfAdjoint.lagda.md

@@ -7,7 +7,6 @@ description: |
 ---
 <!--
 ```agda
-{-# OPTIONS -vtc.def.fun:10 #-}
 open import 1Lab.Reflection.Marker
 open import 1Lab.HLevel.Closure
 open import 1Lab.Path.Groupoid

src/1Lab/Extensionality.agda

@@ -226,12 +226,12 @@ injection→extensional b-set {f} inj ext =
 
 injection→extensional!
   : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
-  → {@(tactic hlevel-tactic-worker) sb : is-set B}
+  → ⦃ _ : H-Level B 2 ⦄
   → {f : A → B}
   → (∀ {x y} → f x ≡ f y → x ≡ y)
   → Extensional B ℓr
   → Extensional A ℓr
-injection→extensional! {sb = b-set} = injection→extensional b-set
+injection→extensional! = injection→extensional (hlevel 2)
 
 Σ-prop-extensional
   : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Type ℓ'}
@@ -258,12 +258,12 @@ instance
 
   Extensional-tr-map
     : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
-    → {@(tactic hlevel-tactic-worker) bset : is-set B}
-    → ⦃ _ : Extensional (A → B) ℓr ⦄
+    → ⦃ bset : H-Level B 2 ⦄
+    → ⦃ ea : Extensional (A → B) ℓr ⦄
     → Extensional (∥ A ∥ → B) ℓr
-  Extensional-tr-map {bset = bset} ⦃ ea ⦄ =
-    injection→extensional (Π-is-hlevel 2 λ _ → bset) {f = λ f → f ∘ inc}
-      (λ p → funext $ ∥-∥-elim (λ _ → bset _ _) (happly p)) ea
+  Extensional-tr-map ⦃ ea = ea ⦄ =
+    injection→extensional! {f = λ f → f ∘ inc}
+      (λ p → funext $ ∥-∥-elim (λ _ → hlevel 1) (happly p)) ea
 
 private module test where
   variable

src/1Lab/Function/Surjection.lagda.md

@@ -135,11 +135,11 @@ injective-surjective→is-equiv b-set f-inj =
   embedding-surjective→is-equiv (injective→is-embedding b-set _ f-inj)
 
 injective-surjective→is-equiv!
-  : {f : A → B} {@(tactic hlevel-tactic-worker) b-set : is-set B}
+  : {f : A → B} ⦃ b-set : H-Level B 2 ⦄
   → injective f
   → is-surjective f
   → is-equiv f
-injective-surjective→is-equiv! {b-set = b-set} =
-  injective-surjective→is-equiv b-set
+injective-surjective→is-equiv! =
+  injective-surjective→is-equiv (hlevel 2)
 ```
 -->

src/1Lab/HIT/Truncation.lagda.md

@@ -103,14 +103,13 @@ whenever it is a family of propositions, by providing a case for
 ∥-∥-rec₂ pprop = ∥-∥-elim₂ (λ _ _ → pprop)
 
 ∥-∥-rec!
-  : ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'}
-  → {@(tactic hlevel-tactic-worker) pprop : is-prop P}
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'} ⦃ _ : H-Level P 1 ⦄
   → (A → P)
   → (x : ∥ A ∥) → P
-∥-∥-rec! {pprop = pprop} = ∥-∥-elim (λ _ → pprop)
+∥-∥-rec! = ∥-∥-elim (λ _ → hlevel 1)
 
-∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A
-∥-∥-proj! {ap = ap} = ∥-∥-proj ap
+∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} ⦃ _ : H-Level A 1 ⦄ → ∥ A ∥ → A
+∥-∥-proj! = ∥-∥-proj (hlevel 1)
 ```
 -->
 

src/1Lab/HLevel/Closure.lagda.md

@@ -394,6 +394,11 @@ instance opaque
 
   H-Level-is-contr : ∀ {n} {ℓ} {T : Type ℓ} → H-Level (is-contr T) (suc n)
   H-Level-is-contr = prop-instance is-contr-is-prop
+
+  H-Level-is-equiv
+    : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {n}
+    → H-Level (is-equiv f) (suc n)
+  H-Level-is-equiv = prop-instance (is-equiv-is-prop _)
 ```
 
 <!--

src/1Lab/HLevel/Universe.lagda.md

@@ -201,14 +201,5 @@ n-Type-square sq i j .∣_∣ = sq i j
 n-Type-square {p = p} {q} {s} {r} sq i j .is-tr =
   is-prop→squarep (λ i j → is-hlevel-is-prop {A = sq i j} _)
     (ap is-tr p) (ap is-tr q) (ap is-tr s) (ap is-tr r) i j
-
-instance
-  H-Level-nType : ∀ {n k} → H-Level (n-Type ℓ k) (1 + k + n)
-  H-Level-nType {k = k} = basic-instance (1 + k) (n-Type-is-hlevel k)
-
-  H-Level-is-equiv
-    : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {n}
-    → H-Level (is-equiv f) (suc n)
-  H-Level-is-equiv = prop-instance (is-equiv-is-prop _)
 ```
 -->

src/1Lab/Reflection/Deriving/Show.agda

@@ -167,11 +167,11 @@ private
 derive-show : Name → Name → TC ⊤
 derive-show nm dat = do
   is-defined nm >>= λ where
-    false → declare (argI nm) =<< instance-type (quote Show) dat
+    false → declare (argI nm) =<< instance-type (it Show ##_) dat
     true  → pure tt
 
   cons ← get-type-constructors dat
-  (tel , as) ← instance-telescope (quote Show) dat
+  (tel , as) ← instance-telescope (it Show ##_) dat
   let ty = unpi-view tel $ itₙ Fun (it Precedence) (itₙ Fun (def dat as) (it ShowS))
   work ← helper-function nm "go" ty []