Skip to content

Commit

Permalink
fix: broken link
Browse files Browse the repository at this point in the history
  • Loading branch information
TOTBWF committed Aug 5, 2023
1 parent 2f401b9 commit 2072f15
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/Cat/Restriction/Total.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,8 @@ module _ {o ℓ} {C : Precategory o ℓ} {C↓ : Restriction-category C} where
Furthermore, the injection from $\thecat{Total}(\cC)$ into $\cC$ is
[pseudomonic], as all isomorphisms in $\cC$ are total.

[pseudomonic]: Cat.Functor.Properties.html#pseudomonic-functors

```agda

Forget-total : Functor (Total-maps C↓) C
Expand Down

0 comments on commit 2072f15

Please sign in to comment.