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.
3
questions
1
vote
1
answer
158
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
8
votes
3
answers
240
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 ...
- 294
24
votes
2
answers
331
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 ...
- 712