Jointly Cartesian Families (#481)

# Description

This PR defines jointly cartesian families, which paves the way for the
correct way to handle #424. Right now the prose
is a bit sparse, as many of the good examples require us to develop
point-set topology, which is exactly what I added this to do! Some of
the names for the cancellation lemmas are also a bit brutal; suggestions
are very much appreciated!

I've also done a bit of cleanup on some proofs in
`Cat.Displayed.Cartesian`; I needed to generalize a bunch of these, so
figured now would be a good of a time as any.

## 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:`.

Author: TOTBWF

src/Cat/Displayed/Cartesian.lagda.md

@@ -148,7 +148,7 @@ base along a composite.
   : ∀ {a b c} {f : Hom b c} {g : Hom a b} {x y : Ob[ c ]} (f' : Hom[ id ] x y)
   → rebase g (rebase f f') Fib.∘ ^*-comp-to ≡ ^*-comp-to Fib.∘ rebase (f ∘ g) f'
 ^*-comp-to-natural {f = f} {g = g} f' =
-  ap hom[] $ cartesian→weak-monic E (π*.cartesian) _ _ $ cast[] $
+  ap hom[] $ cartesian→weak-monic E (π*.cartesian) _ _ _ $ cast[] $
     pulll[] _ (π*.commutesp id-comm _)
     ∙[] pullr[] _ (π*.commutesv _)
     ∙[] π*.uniquep₂ _ id-comm-sym _ _ _