Skip to content

Commit

Permalink
prose: fix last missing link
Browse files Browse the repository at this point in the history
  • Loading branch information
TOTBWF committed Feb 8, 2025
1 parent f06a23c commit 197ed0e
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions src/Cat/Displayed/Cartesian.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -658,11 +658,10 @@ module Cartesian-fibration (fib : Cartesian-fibration) where
Note that if $\cE$ is a fibration, we can define an operation that
allows us to move vertical morphisms between fibres. This actually
extends to a collection of functors, called [base change functors].
This operation is also definable for [weak fibrations], as it only
This operation is also definable for [[weak cartesian fibrations]], as it only
uses the universal property that yields a vertical morphism.

[base change functors]: Cat.Displayed.Cartesian.Indexing.html
[weak fibrations]: Cat.Displayed.Cartesian.Weak.html#is-weak-cartesian-fibration

```agda
rebase : {x y y' y''} (f : Hom x y)
Expand Down

0 comments on commit 197ed0e

Please sign in to comment.