C-systems defined by universe categories: presheaves

TL;DR

This paper constructs 'almost representations' for canonical presheaves in C-systems derived from universe categories, analyzing their behavior under functors and exploring related presheaf constructions.

Contribution

It introduces a method to construct 'almost representations' for presheaves on C-systems from universe categories, advancing understanding of their functorial properties.

Findings

Construction of 'almost representations' for presheaves

Analysis of presheaf behavior under universe category functors

Development of presheaf constructions with broader applications

Abstract

The main result of this paper may be stated as a construction of "almost representations" for the canonical presheaves of object extensions of length n on the C-systems defined by locally cartesian closed universe categories with binary product structures and the study of the behavior of these "almost representations" with respect to the universe category functors. In addition, we study a number of constructions on presheaves on C-systems and on universe categories that are used in the proofs of our main results, but are expected to have other applications as well.