Skip to content

Commit

Permalink
minor spelling mistake
Browse files Browse the repository at this point in the history
  • Loading branch information
plt-amy committed Aug 2, 2023
1 parent 401512a commit 75f6619
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions src/Cat/Displayed/Instances/Diagrams.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -52,11 +52,11 @@ liftings along a constant functor $\Delta_{x} : \cJ \to \cB$, we get a
diagram in $\cE$ that lies entirely in the fibre $\cE_{x}$: a fibrewise
diagram!

we could concisely define the fibration of fibrewise diagrams
as the base change of $\cE \to \cB$ along the functor $\cB \to [\cJ,
\cB]$ that takes an object to the constant diagram on that object, but
this runs into some annoying issues with transports. Therefore, we
unfold the definition instead.
We could concisely define the fibration of fibrewise diagrams as the
base change of $\cE \to \cB$ along the functor $\cB \to [\cJ, \cB]$ that
takes an object to the constant diagram on that object, but this runs
into some annoying issues with transports. Therefore, we unfold the
definition instead.

[fibration of liftings]: Cat.Displayed.Instances.Lifting.html

Expand Down

0 comments on commit 75f6619

Please sign in to comment.