An Equational Logical Framework for Type Theories

TL;DR

This paper introduces a logical framework for type theories that incorporates an extensional equality type, enabling the representation of various type-theoretic concepts within a unified equational approach.

Contribution

It extends existing frameworks by including an extensional equality type, allowing type theories to be specified via signatures of constants.

Findings

Framework supports identity and equality types

Includes a hierarchy of universes

Demonstrates examples of type-theoretic concepts

Abstract

A wide range of intuitionistic type theories may be presented as equational theories within a logical framework. This method was formulated by Per Martin-L\"{o}f in the mid-1980's and further developed by Uemura, who used it to prove an initiality result for a class of models. Herein is presented a logical framework for type theories that includes an extensional equality type so that a type theory may be given by a signature of constants. The framework is illustrated by a number of examples of type-theoretic concepts, including identity and equality types, and a hierarchy of universes.