Skip to content

Commit

Permalink
fix: change link type in Mono.Strong
Browse files Browse the repository at this point in the history
  • Loading branch information
TOTBWF committed Nov 3, 2024
1 parent 1cfb69b commit ca06d24
Showing 1 changed file with 8 additions and 4 deletions.
12 changes: 8 additions & 4 deletions src/Cat/Morphism/Strong/Mono.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,10 @@ invertible→strong-mono f-inv =
```
Next, let's show that strong monos compose. This is completely dual
to the proof that `strong epis compose`{.Agda ident=strong-epi-∘}, so
we direct the reader there for exposition.
to the proof that [strong epis compose], so we direct the reader there
for exposition.
[strong epis compose]: Cat.Morphism.StrongEpi.html#properties
```agda
strong-mono-∘
Expand All @@ -125,8 +127,10 @@ strong-mono-∘ f g (f-mono , f-str) (g-mono , g-str) =
```
Like their non-strong counterparts, strong monomorphisms satisfy a
left cancellation property. This is dual to the proof that `strong epis
cancel`{.Agda ident=strong-epi-cancelr}, so we omit the details.
left cancellation property. This is dual to the proof that [strong epis
cancel], so we omit the details.
[strong epis cancel]: Cat.Morphism.StrongEpi.html#properties
```agda
strong-mono-cancell
Expand Down

0 comments on commit ca06d24

Please sign in to comment.