B-systems

TL;DR

This paper introduces B-systems, algebraic structures closely related to models of dependent type theories, offering a constructively equivalent framework that bridges algebraic models and categorical structures.

Contribution

It defines B-systems as algebraic models aligned with the structures used in dependent type theories, providing a new algebraic perspective closer to contexts and typing judgments.

Findings

B-systems are constructively equivalent to C-systems and contextual categories.

They offer a more algebraic and direct modeling of type-theoretic structures.

The theory of B-systems aligns with the structures used in dependent type theories.

Abstract

B-systems are algebras (models) of an essentially algebraic theory that is expected to be constructively equivalent to the essentially algebraic theory of C-systems which is, in turn, constructively equivalent to the theory of contextual categories. The theory of B-systems is closer in its form to the structures directly modeled by contexts and typing judgements of (dependent) type theories and further away from categories than contextual categories and C-systems.