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
1 vote
1 answer

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
8 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
  • 294
24 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
  • 712