Joint monomorphisms (#440)

# Description

This PR defines joint monomorphisms, and proves some basic facts about
them.

# Notes

It might be worth comparing joint monos vs. subobjects of products for
things like
[congruences](https://1lab.dev/Cat.Diagram.Congruence.html#4840): I
expect that joint monos might be a bit nicer, but I don't want to do any
refactors in this PR.

## Checklist

Before submitting a merge request, please check the items below:

- [x] I've read [the contributing
guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md).
- [x] The imports of new modules have been sorted with
`support/sort-imports.hs` (or `nix run --experimental-features
nix-command -f . sort-imports`).
- [x] All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content,
and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title
with `chore:`.

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/Functor/Joint.lagda.md

@@ -70,7 +70,7 @@ $f = g$
 
 The canonical example of a family of jointly faithful functors are the
 family of hom-functors $\hat{C}(\yo(A), -)$, indexed by objects of $A$:
-this is a restatment of the [[coyoneda lemma]].
+this is a restatement of the [[coyoneda lemma]].
 
 Note that every functor $F : \cI \to [\cC, \cD]$ induces a family of
 functors via the mapping on objects: this family is jointly faithful
@@ -125,7 +125,7 @@ $F : \cI \to [ \cC, \cD ]$.
 
 ## Jointly full functors
 
-:::{.definition #jointly-full-functors alias="jointy full"}
+:::{.definition #jointly-full-functors alias="jointly full"}
 A diagram of functors $F : \cI \to [\cC, \cD]$ is **jointly full** when
 the functor $\hat{F} : \cC \to [\cI, \cD]$ is full. Explicitly, $F$ is
 jointly full if a family of morphisms $g_i : \cD(F(i)(x), F(i)(y))$ that is
@@ -172,7 +172,7 @@ module _
 :::{.definition #jointly-fully-faithful-functors alias="jointly-fully-faithful"}
 A diagram of functors $F : \cI \to [\cC, \cD]$ is **jointly fully faithful** when
 the functor $\hat{F} : \cC \to [\cI, \cD]$ is fully faithful. Explicitly, $F$ is
-jointly faully faithful if there is an equivalence of natural transformations
+jointly fully faithful if there is an equivalence of natural transformations
 $\hat{F}(x) \to \hat{F}(y)$ and morphisms $\cC(x,y)$.
 :::
 

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