prose: fix link targets

Author: TOTBWF

src/Cat/Displayed/Cartesian/Joint.lagda.md

@@ -35,7 +35,7 @@ open Displayed E
 :::{.definition #jointly-cartesian-family}
 A family of morphisms $f_{i} : \cE_{u_i}(A', B'_{i})$ over $u_{i} : \cB(A, B_{i})$
 is **jointly cartesian** if it satisfies a familial version of the universal
-property of a [[cartesian]] map.
+property of a [[cartesian|cartesian-morphism]] map.
 :::
 
 ```agda
@@ -369,7 +369,7 @@ jointly-cartesian-vertical-retraction-stable
 
 ## Cancellation properties of jointly cartesian families
 
-Every jointly cartesian family is a [[weakly monic family]].
+Every jointly cartesian family is a [[jointly weak monic family]].
 
 ```agda
 jointly-cartesian→jointly-weak-monic

src/Cat/Displayed/Morphism.lagda.md

@@ -76,7 +76,7 @@ record _↪[_]_
 open _↪[_]_ public
 ```
 
-## Weak monos {defines="weak-monomorphism"}
+## Weak monos {defines="weak-monomorphism weakly-monic"}
 
 When working in a displayed setting, we also have weaker versions of
 the morphism classes we are familiar with, wherein we can only left/right