Skip to content

Commit

Permalink
formatting: pull module section out of comment
Browse files Browse the repository at this point in the history
This makes the type of `rebase` make sense
  • Loading branch information
TOTBWF committed Feb 8, 2025
1 parent b52720b commit 632648a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Cat/Displayed/Cartesian.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -635,12 +635,12 @@ Thus, we do not dwell on the distinction.
Cartesian-fibration : Type _
Cartesian-fibration = {x y} (f : Hom x y) (y' : Ob[ y ]) Cartesian-lift f y'

module Cartesian-fibration (fib : Cartesian-fibration) where
```
:::

<!--
```agda
module Cartesian-fibration (fib : Cartesian-fibration) where

module _ {x y} (f : Hom x y) (y' : Ob[ y ]) where
open Cartesian-lift (fib f y')
Expand Down

0 comments on commit 632648a

Please sign in to comment.