Erik Palmgren: A setoid model in a flexible framework for formalized models of type theory

Abstract: The standard frameworks for models of type theory, categories with families (cwfs), and categories with attributes (cwas), rely on a type functor into the category of sets, T : C^op → Sets. When formalizing such models in type theory the question arises how the categories of sets should be understood? We propose a flexible variant of the cwa notion suitable for such formalizations, and exemplify its use by a setoid model for dependent type theory with Π-types. The category of sets is replaced by Fr(B), the category comprised of subsetoids of a fixed setoid B, and functions between such subsetoids. The setoid B is the *bounding setoid* of the cwa, and thus we name the new notion a *bounded cwa*. In the case of the setoid model we chose B to be (V, =_V), the setoid of iterative sets, used in Aczel’s type-theoretic model of constructive set theory.

We give details of a Coq formalization of the setoid model. The formalization is made in the context of a general toolbox for formalized models of type theories, currently in development together with Peter LeFanu Lumsdaine, and also using some previous work with Olov Wilander.