We prove a variant of Läuchli's completeness theorem for intuitionistic predicate calculus. The formulation of the result relies on the observation (due to Lawvere) that Läuchli's theorem is related to the logic of the ...

Strong similarities have been long observed between the Galois (Categories Galoisiennes) and the Tannaka (Categories Tannakiennes) theories of representation of groups. In this paper we construct an explicit (neutral) ...

It is well known that the category of covering projections (that is, locally constant objects) of a locally connected topos is equivalent to the classifying topos of a strict progroupoid (or, equivalently, a localic ...

A topos E is weakly generated by a full subcategory C → E if the extreme subtopos E → E is the smallest subtopos of E containing C → E. If the full subcategory consists of only one object then we say that E is weakly ...

We strengthen a result of Lawvere by proving that every pre-cohesive geometric morphism p: E --> S has a canonical intensive quality s: E --> L. We also discuss examples among bounded pre-cohesive p: E --> S and, in ...

Let be a topos, be the full subcategory of decidable objects, and be the full subcategory of double-negation sheaves. We give sufficient conditions for the existence of a Unity and Identity for the two subcategories of ...

We introduce an apparent strengthening of Sufficient Cohesion that we call Stable Connected Codiscreteness (SCC) and show that if $p: E --> S$ is cohesive and satisfies SCC then the internal axiom of choice holds in $S$. ...

Let E be a topos. If l is a level of E with monic skeleta then it makes sense to consider the objects in E that have l-skeletal boundaries. In particular, if p : E o S is a pre-cohesive geometric morphism then its centre ...

Abstract: Using tools from category theory and 2-category theory, in particular from topos theory, we present the rudiments of a theory of mathematical gestures and hypergestures, including diverse incarnations thereof: ...