6 citations · 14 across the 8 of their papers we have counts for
10 papers
Theorem prover Arend
Fedor Part, Valery Isaev, Sergey Sinchuk
This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the…
A Constructive Approach to Complete Spaces
Valery Isaev
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 conc…
(Co)condition hits the Path
Tesla Zhang, Valery Isaev
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…
Models of Homotopy Type Theory with an Interval Type
Valery Isaev
In this short note, we construct a class of models of an extension of homotopy type theory, which we call homotopy type theory with an interval type.
Contextually indexed contextual categories
Valery Isaev
In this paper, we define a generalization of indexed categories and contextual categories which we call contextually indexed (contextual) categories. While contextual categories ar…
Indexed type theories
Valery Isaev
In this paper, we define indexed type theories which are related to indexed (-)categories in the same way as (homotopy) type theories are related to (-)categories.…
Model category of marked objects
Valery Isaev
For every functor , where is a small category and is a model category which satisfies some mild hypotheses, we…
Model Structures on Categories of Models of Type Theories
Valery Isaev
Models of dependent type theories are contextual categories with some additional structure. We prove that if a theory has enough structure, then the category $T\text{-}\mathbf{…
Algebraic Presentations of Dependent Type Theories
Valery Isaev
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: s…
On fibrant objects in model categories
Valery Isaev
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…