refactor: rename ∥-∥-proj to ∥-∥-proj!

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

@@ -106,8 +106,11 @@ whenever it is a family of propositions, by providing a case for
   → (x : ∥ A ∥) → P
 ∥-∥-rec! {pprop = pprop} = ∥-∥-elim (λ _ → pprop)
 
-∥-∥-proj : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A
-∥-∥-proj {ap = ap} = ∥-∥-rec ap λ x → x
+∥-∥-proj : ∀ {ℓ} {A : Type ℓ} → is-prop A → ∥ A ∥ → A
+∥-∥-proj ap = ∥-∥-rec ap λ x → x
+
+∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A
+∥-∥-proj! {ap = ap} = ∥-∥-proj ap
 ```
 -->
 

src/Cat/Univalent/Rezk/Universal.lagda.md

@@ -86,7 +86,7 @@ eso→pre-faithful
   → is-eso H → (γ δ : F => G)
   → (∀ b → γ .η (H .F₀ b) ≡ δ .η (H .F₀ b)) → γ ≡ δ
 eso→pre-faithful {A = A} {B = B} {C = C} H {F} {G} h-eso γ δ p =
-  Nat-path λ b → ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+  Nat-path λ b → ∥-∥-proj (C.Hom-set _ _ _ _) do
   (b′ , m) ← h-eso b
   ∥_∥.inc $
     γ .η b                                      ≡⟨ C.intror (F-map-iso F m .invl) ⟩
@@ -191,7 +191,7 @@ this file in Agda and poke around the proof.
 ```agda
       lemma : (a : A.Ob) (f : H.₀ a B.≅ b)
             → γ.η a ≡ G.₁ (f .from) C.∘ g C.∘ F.₁ (f .to)
-      lemma a f = ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+      lemma a f = ∥-∥-proj (C.Hom-set _ _ _ _) do
         (k , p)   ← H-full (h.from B.∘ B.to f)
         (k⁻¹ , q) ← H-full (B.from f B.∘ h.to)
         ∥_∥.inc $
@@ -216,7 +216,7 @@ over $b$ is a proposition.
     T-prop : ∀ b → is-prop (T b)
     T-prop b (g , coh) (g′ , coh′) =
       Σ-prop-path (λ x → Π-is-hlevel² 1 λ _ _ → C.Hom-set _ _ _ _) $
-        ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+        ∥-∥-proj (C.Hom-set _ _ _ _) do
         (a₀ , h) ← H-eso b
         pure $ C.iso→epic (F-map-iso F h) _ _
           (C.iso→monic (F-map-iso G (h B.Iso⁻¹)) _ _
@@ -236,7 +236,7 @@ $(a,h)$ pair.
       ∥_∥.inc (Mk.g b a₀ h , Mk.lemma b a₀ h)
 
     mkT : ∀ b → T b
-    mkT b = ∥-∥-proj {ap = T-prop b} (mkT′ b (H-eso b))
+    mkT b = ∥-∥-proj (T-prop b) (mkT′ b (H-eso b))
 ```
 
 Another calculation shows that, since $H$ is full, given any pair of
@@ -260,7 +260,7 @@ the transformation we're defining, too.
         module h = B._≅_ h
 
       naturality : _
-      naturality = ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+      naturality = ∥-∥-proj (C.Hom-set _ _ _ _) do
         (k , p) ← H-full (h′.from B.∘ f B.∘ h.to)
         pure $ C.pullr (C.pullr (F.weave (sym
                   (B.pushl p ∙ ap₂ B._∘_ refl (B.cancelr h.invl)))))
@@ -281,16 +281,16 @@ $- \circ H$ is faithful, and now we've shown it is full, it is fully faithful.
     δ : F => G
     δ .η b = mkT b .fst
     δ .is-natural b b′ f = ∥-∥-elim₂
-      {P = λ α β → ∥-∥-proj {ap = T-prop b′} (mkT′ b′ α) .fst C.∘ F.₁ f
-                 ≡ G.₁ f C.∘ ∥-∥-proj {ap = T-prop b} (mkT′ b β) .fst}
+      {P = λ α β → ∥-∥-proj (T-prop b′) (mkT′ b′ α) .fst C.∘ F.₁ f
+                 ≡ G.₁ f C.∘ ∥-∥-proj (T-prop b) (mkT′ b β) .fst}
       (λ _ _ → C.Hom-set _ _ _ _)
       (λ (a′ , h′) (a , h) → naturality f a a′ h h′) (H-eso b′) (H-eso b)
 
   full : is-full (precompose H)
   full {x = x} {y = y} γ = pure (δ _ _ γ , Nat-path p) where
     p : ∀ b → δ _ _ γ .η (H.₀ b) ≡ γ .η b
     p b = subst
-      (λ e → ∥-∥-proj {ap = T-prop _ _ γ (H.₀ b)} (mkT′ _ _ γ (H.₀ b) e) .fst
+      (λ e → ∥-∥-proj (T-prop _ _ γ (H.₀ b)) (mkT′ _ _ γ (H.₀ b) e) .fst
            ≡ γ .η b)
       (squash (inc (b , B.id-iso)) (H-eso (H.₀ b)))
       (C.eliml (y .F-id) ∙ C.elimr (x .F-id))
@@ -377,7 +377,7 @@ candidate over it.
 <!--
 ```agda
     summon : ∀ {b} → ∥ Essential-fibre H b ∥ → is-contr (Obs b)
-    summon f = ∥-∥-proj {ap = is-contr-is-prop} do
+    summon f = ∥-∥-proj is-contr-is-prop do
       f ← f
       pure $ contr (obj′ f) (Obs-is-prop f)
 
@@ -488,7 +488,7 @@ This proof _really_ isn't commented. I'm sorry.
         (λ _ → compat-prop f) (sym (Homs-prop′ f _ _ _ _ h′)))
 
     Homs-contr : ∀ {b b′} (f : B.Hom b b′) → is-contr (Homs f)
-    Homs-contr f = ∥-∥-proj (Homs-contr′ f)
+    Homs-contr f = ∥-∥-proj! (Homs-contr′ f)
 
     G₁ : ∀ {b b′} → B.Hom b b′ → C.Hom (G₀ b) (G₀ b′)
     G₁ f = Homs-contr f .centre .fst
@@ -552,7 +552,7 @@ a set --- a proposition --- these choices don't matter, so we can use
 essential surjectivity of $H$.
 
 ```agda
-    G .F-∘ {x} {y} {z} f g = ∥-∥-proj do
+    G .F-∘ {x} {y} {z} f g = ∥-∥-proj! do
       (ax , hx) ← H-eso x
       (ay , hy) ← H-eso y
       (az , hz) ← H-eso z

src/Data/Fin/Finite.lagda.md

@@ -93,11 +93,11 @@ open Finite ⦃ ... ⦄ public
 instance
   H-Level-Finite : ∀ {ℓ} {A : Type ℓ} {n : Nat} → H-Level (Finite A) (suc n)
   H-Level-Finite = prop-instance {T = Finite _} λ where
-    x y i .Finite.cardinality → ∥-∥-proj
+    x y i .Finite.cardinality → ∥-∥-proj!
       ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈
       i
     x y i .Finite.enumeration → is-prop→pathp
-      {B = λ i → ∥ _ ≃ Fin (∥-∥-proj ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈ i) ∥}
+      {B = λ i → ∥ _ ≃ Fin (∥-∥-proj! ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈ i) ∥}
       (λ _ → squash)
       (x .enumeration) (y .enumeration) i
 
@@ -146,7 +146,7 @@ private
     .snd .is-iso.rinv fzero → refl
     .snd .is-iso.linv x → funext λ { () }
 
-  finite-pi-fin (suc sz) {B} fam = ∥-∥-proj $ do
+  finite-pi-fin (suc sz) {B} fam = ∥-∥-proj! $ do
     e ← finite-choice (suc sz) λ x → fam x .enumeration
     let rest = finite-pi-fin sz (λ x → fam (fsuc x))
     cont ← rest .Finite.enumeration
@@ -167,13 +167,13 @@ Finite-⊎ {A = A} {B = B} = fin $ do
   beq ← enumeration {T = B}
   pure (⊎-ap aeq beq ∙e Finite-coproduct)
 
-Finite-Π {A = A} {P = P} ⦃ fin {sz} en ⦄ ⦃ fam ⦄ = ∥-∥-proj $ do
+Finite-Π {A = A} {P = P} ⦃ fin {sz} en ⦄ ⦃ fam ⦄ = ∥-∥-proj! $ do
   eqv ← en
   let count = finite-pi-fin sz λ x → fam $ equiv→inverse (eqv .snd) x
   eqv′ ← count .Finite.enumeration
   pure $ fin $ pure $ Π-dom≃ (eqv e⁻¹) ∙e eqv′
 
-Finite-Σ {A = A} {P = P} ⦃ afin ⦄ ⦃ fam ⦄ = ∥-∥-proj $ do
+Finite-Σ {A = A} {P = P} ⦃ afin ⦄ ⦃ fam ⦄ = ∥-∥-proj! $ do
   aeq ← afin .Finite.enumeration
   let
     module aeq = Equiv aeq

src/Data/Set/Material.lagda.md

@@ -285,8 +285,8 @@ Presentation-is-prop {ℓ} {A} f P1 P2 = done where
 
   eqv : ∀ x → fibre g x ≃ fibre h x
   eqv x = prop-ext (gm x) (hm x)
-    (λ fib → ∥-∥-proj {ap = hm x} (v' .fst x (u' .snd x (inc fib))))
-    (λ fib → ∥-∥-proj {ap = gm x} (u' .fst x (v' .snd x (inc fib))))
+    (λ fib → ∥-∥-proj (hm x) (v' .fst x (u' .snd x (inc fib))))
+    (λ fib → ∥-∥-proj (gm x) (u' .fst x (v' .snd x (inc fib))))
 ```
 
 This pointwise equivalence between fibres extends to an equivalence
@@ -386,7 +386,7 @@ module Members {ℓ} (X : V ℓ) where
 
   memb : ∀ {x} → x ∈ₛ X ≃ fibre elem x
   memb {x = x} = prop-ext (is-member _ X .is-tr) (embeds _)
-    (λ a → ∥-∥-proj {ap = embeds _} (subst (x ∈ₛ_) presents a))
+    (λ a → ∥-∥-proj (embeds _) (subst (x ∈ₛ_) presents a))
     (λ a → subst (x ∈ₛ_) (sym presents) (inc a))
 
   module memb {x} = Equiv (memb {x})

src/Order/Semilattice/Free.lagda.md

@@ -194,7 +194,7 @@ $K$-finiteness condition, but it will be very useful!
       .glb≤fam i →
         K-fin-lt {P , P-fin} {ηₛₗ (cover i .fst)} λ j i=j →
           subst (λ e → ∣ P e ∣) (out! i=j) (cover i .snd)
-      .greatest lb′ wit → K-fin-lt {lb′} {P , P-fin} λ i i∈p → ∥-∥-proj do
+      .greatest lb′ wit → K-fin-lt {lb′} {P , P-fin} λ i i∈p → ∥-∥-proj! do
         (idx , path) ← surj (i , i∈p)
         pure (K-fin-lt′ {lb′} {ηₛₗ (cover idx .fst)} (wit idx) i (inc (ap fst path)))
 ```
@@ -267,7 +267,7 @@ make-free-slat .universal {x} {y} f = total-hom go pres where
   pres .pres-⋆ (A , af) (B , bf) =
     ap fst $
       glb-unique y.po (go.ε′ (_∪_ x (A , af) (B , bf) .fst) (_∪_ x (A , af) (B , bf) .snd)) $ _ , λ where
-        .glb≤fam (x , w) → ∥-∥-proj $ w >>= λ where
+        .glb≤fam (x , w) → ∥-∥-proj! $ w >>= λ where
           (inl w) → pure $
             g1 .fst y.∩ g2 .fst y.≤⟨ y.∩≤l ⟩
             g1 .fst             y.≤⟨ g1.glb≤fam (x , w) ⟩
@@ -287,7 +287,7 @@ make-free-slat .universal {x} {y} f = total-hom go pres where
 make-free-slat .commutes {y = y} f = funext λ x → sym y.∩-idr
   where module y = Semilattice y
 make-free-slat .unique {x = x} {y = y} {f = f} {g = g} w =
-  Homomorphism-path λ arg → ∥-∥-proj {ap = y.has-is-set _ _} do
+  Homomorphism-path λ arg → ∥-∥-proj (y.has-is-set _ _) do
     (card , diagram , glb) ← K-reduce x arg
     let
       path : arg ≡ KA.⋂ λ i → ηₛₗ x (diagram i)