Skip to main content

Questions tagged [topos]

A topos, in the context of logic, refers to an elementary topos. It is a cartesian-closed category with finite limits and subobject classifiers.

Filter by
Sorted by
Tagged with
4 votes
1 answer

Does "unique mere existence" imply "existence"?

Hopefully this question fits in well here. I'm hoping that more people who know the answer will see it here than on somwehere like mse, but please let me know if you'd rather I move it there! Say you'...
Chris Grossack's user avatar
1 vote
2 answers

Formalization of a model of ∞-category in a proof assistant

I am aware of similar question in MO whose comment nicely lists zoo of possible models and only such models can be formalized. But I have not found any implementation so far which I could use or ...
TomR's user avatar
  • 133
9 votes
3 answers

When is hProp equivalent to the subobject classifier?

In the definition of an elementary topos, the "object of propositions" $\Omega$ is axiomatized by the universal property of a subobject classifier. In homotopy type theory, we instead start ...
Max New's user avatar
  • 314
25 votes
2 answers

How to use a proof assistant to reason in a topos?

I would like to use a proof assistant to reason in the internal language of a topos. More specifically, I would like to (be able to) formalise informal arguments such as in Ingo Blechschmidt's PhD ...
Nico's user avatar
  • 722