Semi-simplicial Types in Logic-enriched Homotopy Type Theory

TL;DR

This paper introduces a new logic-enriched homotopy type theory that allows defining semi-simplicial types with fibrant types, overcoming previous limitations and enabling implementation in proof assistants.

Contribution

It presents a fibrant, logic-enriched extension of HoTT that supports semi-simplicial types and is suitable for implementation in proof assistants.

Findings

Defined semi-simplicial types in the new system

Outlined an implementation in the proof assistant Plastic

Achieved fibrant types compatible with existing proof tools

Abstract

The problem of defining Semi-Simplicial Types (SSTs) in Homotopy Type Theory (HoTT) has been recognized as important during the Year of Univalent Foundations at the Institute of Advanced Study. According to the interpretation of HoTT in Quillen model categories, SSTs are type-theoretic versions of Reedy fibrant semi-simplicial objects in a model category and simplicial and semi-simplicial objects play a crucial role in many constructions in homotopy theory and higher category theory. Attempts to define SSTs in HoTT lead to some difficulties such as the need of infinitary assumptions which are beyond HoTT with only non-strict equality types. Voevodsky proposed a definition of SSTs in Homotopy Type System (HTS), an extension of HoTT with non-fibrant types, including an extensional strict equality type. However, HTS does not have the desirable computational properties such as decidability of type checking and strong normalization. In this paper, we study a logic-enriched homotopy type theory, an alternative extension of HoTT with equational logic based on the idea of logic-enriched type theories. In contrast to Voevodskys HTS, all types in our system are fibrant and it can be implemented in existing proof assistants. We show how SSTs can be defined in our system and outline an implementation in the proof assistant Plastic.