Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Elementary topos nonsense #411

Merged
merged 14 commits into from
Mar 17, 2025
Prev Previous commit
Next Next commit
plt-amy committed Mar 17, 2025
commit e825f94ea118705f3b69e46cfb4943e8dff4d96c
2 changes: 1 addition & 1 deletion src/Cat/Instances/Sheaf/Omega.lagda.md
Original file line number Diff line number Diff line change
@@ -262,7 +262,7 @@ sheaf-name {A} A' = nm module sheaf-name where
We can then compute, in $\psh(\cC)$, the name of $A'$, resulting in a
natural transformation $\name{A'} : A \to \Omega$. It remains to show
that this transformation is actually valued in $\Omega_J$, i.e. that
each of the resulting sieves is closed. To this end, susppose we have
each of the resulting sieves is closed. To this end, suppose we have
some $x : A(U)$ and that the sieve $h^*(\name{A'} x)$ is $J$-covering.
We must show that $\name{A'} x$ contains $h$.