Joint monomorphisms

src/Cat/Abelian/Base.lagda.md

@@ -273,7 +273,7 @@ desired equation. Check it out:
       where
         lemma : ⟨ id , 0m ⟩ ∘ π₁ + ⟨ 0m , id ⟩ ∘ π₂
               ≡ id
-        lemma = Prod.unique₂ {pr1 = π₁} {pr2 = π₂}
+        lemma = ⟨⟩-unique₂ {pr1 = π₁} {pr2 = π₂}
           (sym (∘-linear-r _ _ _) ∙ ap₂ _+_ (cancell π₁∘⟨⟩) (pulll π₁∘⟨⟩ ∙ ∘-zero-l) ∙ Hom.elimr refl)
           (sym (∘-linear-r _ _ _) ∙ ap₂ _+_ (pulll π₂∘⟨⟩ ∙ ∘-zero-l) (cancell π₂∘⟨⟩) ∙ Hom.eliml refl)
           (elimr refl)

src/Cat/Diagram/Exponential.lagda.md

@@ -38,7 +38,7 @@ $f : A \to B$, and I have an $x : A$, then application gives me an $f(x)
 
 <!--
 ```agda
-open Binary-products C fp hiding (unique₂)
+open Binary-products C fp
 open Cat.Reasoning C
 open Terminal term
 open Functor

src/Cat/Diagram/Product.lagda.md

@@ -246,7 +246,11 @@ module Binary-products
 
   -- Note: here and below we have to open public the aliases in a module
   -- with parameters so Agda picks up the display forms.
-  module _ {a b} where open Product (all-products a b) renaming (unique to ⟨⟩-unique) hiding (apex) public
+  module _ {a b} where
+    open Product (all-products a b)
+      renaming (unique to ⟨⟩-unique; unique₂ to ⟨⟩-unique₂)
+      hiding (apex)
+      public
   open Functor
 
   infix 50 _⊗₁_
@@ -294,14 +298,14 @@ We also define a handful of common morphisms.
 <!--
 ```agda
   δ-natural : is-natural-transformation Id (×-functor F∘ Cat⟨ Id , Id ⟩) λ _ → δ
-  δ-natural x y f = unique₂
+  δ-natural x y f = ⟨⟩-unique₂
     (cancell π₁∘⟨⟩) (cancell π₂∘⟨⟩)
     (pulll π₁∘⟨⟩ ∙ cancelr π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ cancelr π₂∘⟨⟩)
 
   swap-is-iso : ∀ {a b} → is-invertible (swap {a} {b})
   swap-is-iso = make-invertible swap
-    (unique₂ (pulll π₁∘⟨⟩ ∙ π₂∘⟨⟩) ((pulll π₂∘⟨⟩ ∙ π₁∘⟨⟩)) (idr _) (idr _))
-    (unique₂ (pulll π₁∘⟨⟩ ∙ π₂∘⟨⟩) ((pulll π₂∘⟨⟩ ∙ π₁∘⟨⟩)) (idr _) (idr _))
+    (⟨⟩-unique₂ (pulll π₁∘⟨⟩ ∙ π₂∘⟨⟩) ((pulll π₂∘⟨⟩ ∙ π₁∘⟨⟩)) (idr _) (idr _))
+    (⟨⟩-unique₂ (pulll π₁∘⟨⟩ ∙ π₂∘⟨⟩) ((pulll π₂∘⟨⟩ ∙ π₁∘⟨⟩)) (idr _) (idr _))
 
   swap-natural
     : ∀ {A B C D} ((f , g) : Hom A C × Hom B D)
@@ -317,8 +321,8 @@ We also define a handful of common morphisms.
   swap-δ = ⟨⟩-unique (pulll π₁∘⟨⟩ ∙ π₂∘⟨⟩) (pulll π₂∘⟨⟩ ∙ π₁∘⟨⟩)
 
   assoc-δ : ∀ {a} → ×-assoc ∘ (id ⊗₁ δ {a}) ∘ δ {a} ≡ (δ ⊗₁ id) ∘ δ
-  assoc-δ = unique₂
-    (pulll π₁∘⟨⟩ ∙ unique₂
+  assoc-δ = ⟨⟩-unique₂
+    (pulll π₁∘⟨⟩ ∙ ⟨⟩-unique₂
       (pulll π₁∘⟨⟩ ∙ pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩)
       (pulll π₂∘⟨⟩ ∙ pullr (pulll π₂∘⟨⟩) ∙ pulll (pulll π₁∘⟨⟩) ∙ pullr π₂∘⟨⟩)
       (pulll (pulll π₁∘⟨⟩) ∙ pullr π₁∘⟨⟩)

src/Cat/Displayed/Instances/Subobjects.lagda.md

@@ -30,7 +30,7 @@ open Displayed
 ```
 -->
 
-# The fibration of subobjects {defines="poset-of-subobjects"}
+# The fibration of subobjects {defines="poset-of-subobjects subobject"}
 
 Given a base category $\cB$, we can define the [[displayed category]] of
 _subobjects_ over $\cB$. This is, in essence, a restriction of the

src/Cat/Instances/Slice.lagda.md

@@ -751,15 +751,15 @@ adjunction between dependent sum and base change.
   Forget⊣constant-family : Forget/ ⊣ constant-family
   Forget⊣constant-family .unit .η X .map = ⟨ id , X .map ⟩
   Forget⊣constant-family .unit .η X .commutes = π₂∘⟨⟩
-  Forget⊣constant-family .unit .is-natural _ _ f = ext (unique₂
+  Forget⊣constant-family .unit .is-natural _ _ f = ext (⟨⟩-unique₂
     (pulll π₁∘⟨⟩ ∙ id-comm-sym)
     (pulll π₂∘⟨⟩ ∙ f .commutes)
     (pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩)
     (pulll π₂∘⟨⟩ ∙ π₂∘⟨⟩))
   Forget⊣constant-family .counit .η x = π₁
   Forget⊣constant-family .counit .is-natural _ _ f = π₁∘⟨⟩
   Forget⊣constant-family .zig = π₁∘⟨⟩
-  Forget⊣constant-family .zag = ext (unique₂
+  Forget⊣constant-family .zag = ext (⟨⟩-unique₂
     (pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩)
     (pulll π₂∘⟨⟩ ∙ π₂∘⟨⟩)
     refl