Searcharxiv⌕ Search

arXiv subjects

Valery Isaev

Publications and source records attributed to Valery Isaev.

10 recordsLinked to original sources
arXiv2024

A Constructive Approach to Complete Spaces

In this paper, we present a constructive generalization of metric and uniform spaces by introducing a new class of spaces, called cover spaces. These spaces form a topological concrete category with a full reflective subcategory of complete spaces. This subcategory is closely related to a particular subcategory of locales, offering an alternative approach to localic completion. Additionally, we demonstrate how this framework provides simple constructive definitions of compact spaces, uniform convergence, and limits of nets.

math.GN↗
arXiv2024

(Co)condition hits the Path

We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax of higher inductive types in homotopy type theory, while coconditions generalize the cubical path type. (Co)conditions are also useful without an interval type. The duality between conditions and coconditions is presented in an interesting way: The elimination principles of inductive types with conditions can be internalized with records with coconditions and vice versa. However, we do not develop the metatheory of conditions and coconditions in this paper. Instead, we only present the type checking.

cs.LO↗
arXiv2018

Contextually indexed contextual categories

In this paper, we define a generalization of indexed categories and contextual categories which we call contextually indexed (contextual) categories. While contextual categories are models of ordinary type theories, contextually indexed (contextual) categories are models of indexed type theories. We also define type-theoretic semi-fibration categories which generalize type-theoretic fibration categories. Every model category in which cofibrations are stable under pullbacks is a type-theoretic semi-fibration category. We show that type-theoretic semi-fibration category gives rise to a contextually indexed contextual category with finite limits. Finally, we prove that the category of simplicial sets with the Joyal model structure gives rise to a locally small Cartesian closed contextually indexed contextual category with indexed limits and colimits.

math.CT↗
arXiv2018

Indexed type theories

In this paper, we define indexed type theories which are related to indexed ($\infty$-)categories in the same way as (homotopy) type theories are related to ($\infty$-)categories. We define several standard constructions for such theories including finite (co)limits, arbitrary (co)products, exponents, object classifiers, and orthogonal factorization systems. We also prove that these constructions are equivalent to their type theoretic counterparts such as $\Sigma$-types, unit types, identity types, finite higher inductive types, $\Pi$-types, univalent universes, and higher modalities.

math.CT↗
arXiv2018

Morita equivalences between algebraic dependent type theories

We define a notion of equivalence between algebraic dependent type theories which we call Morita equivalence. This notion has a simple syntactic description and an equivalent description in terms of models of the theories. The category of models of a type theory often carries a natural structure of a model category. If this holds for the categories of models of two theories, then a map between them is a Morita equivalence if and only if the adjunction generated by it is a Quillen equivalence.

math.CT↗
arXiv2016

Model category of marked objects

For every functor $\mathcal{F} : \mathcal{K} \to \mathbf{C}$, where $\mathcal{K}$ is a small category and $\mathbf{C}$ is a model category which satisfies some mild hypotheses, we define a model category $\mathbf{C}^m$ of $\mathcal{K}$-marked objects of $\mathbf{C}$. We consider an application of this construction to the category of simplicial sets with the Joyal model structure. Marked simplicial sets can be thought of as $(\infty,1)$-categories with some additional structure which depends on $\mathcal{F}$. In particular, we construct a model category of quasi-categories which have limits of all diagrams of any given shape.

math.CT↗
arXiv2016

Model Structures on Categories of Models of Type Theories

Models of dependent type theories are contextual categories with some additional structure. We prove that if a theory $T$ has enough structure, then the category $T\text{-}\mathbf{Mod}$ of its models carries the structure of a model category. We also show that if $T$ has $\Sigma$ types, then weak equivalences can be characterized in terms of homotopy categories of models.

math.CT↗
arXiv2016

Algebraic Presentations of Dependent Type Theories

In this paper, we propose an abstract definition of dependent type theories as essentially algebraic theories. One of the main advantages of this definition is its composability: simple theories can be combined into more complex ones, and different properties of the resulting theory may be deduced from properties of the basic ones. We define a category of algebraic dependent type theories which allows us not only to combine theories but also to consider equivalences between them. We also study models of such theories and show that one can think of them as contextual categories with additional structure.

math.LO↗
arXiv2013

On fibrant objects in model categories

In this paper, we study properties of maps between fibrant objects in model categories. We give a characterization of weak equivalences between fibrant object. If every object of a model category is fibrant, then we give a simple description of a set of generating cofibrations. We show that to construct such model structure it is enough to check some relatively simple conditions.

math.CT↗