Skip to content

Commit

Permalink
pre-commit
Browse files Browse the repository at this point in the history
  • Loading branch information
fredrik-bakke committed Nov 9, 2023
1 parent 9a12ea6 commit 94a33e0
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/foundation-core/retractions.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -196,8 +196,8 @@ In a commuting triangle of the form
```

if `r : X → A` is a retraction of the map `g` on the right and `s : B A` is a
retraction of the map `h` on top, then `s ∘ r` is a retraction of the map `f` on the
left.
retraction of the map `h` on top, then `s ∘ r` is a retraction of the map `f` on
the left.

```agda
module _
Expand Down

0 comments on commit 94a33e0

Please sign in to comment.