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.
4
questions
4
votes
1
answer
420
views
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'...
- 329
1
vote
2
answers
285
views
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 ...
- 133
9
votes
3
answers
320
views
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 ...
- 314
25
votes
2
answers
387
views
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 ...
- 722