Skip to content

Commit

Permalink
fix: fix partial rename
Browse files Browse the repository at this point in the history
  • Loading branch information
TOTBWF committed Feb 2, 2023
1 parent cdeba29 commit 017218e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Cat/Displayed/Bifibration.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ module _ (fib : Cartesian-fibration) where
With some repackaging, we can see that this yields a bifibration.

```agda
left-adjoint-reindexing→bifibration
left-adjoint-base-change→bifibration
: (L : {x y} (f : Hom x y) Functor (Fibre ℰ x) (Fibre ℰ y))
( {x y} (f : Hom x y) (L f ⊣ base-change f))
is-bifibration
Expand Down

0 comments on commit 017218e

Please sign in to comment.