Univalent typoids

TL;DR

This paper introduces univalent typoids, a generalization of setoids in homotopy type theory, establishing their fundamental properties and connections to propositional truncation and weak groupoid structures.

Contribution

It defines univalent typoids, explores their properties, and demonstrates their role as a weak groupoid analogue in homotopy type theory.

Findings

Fundamental properties of univalent typoids established

Interpretation of propositional truncation within typoids

Extension of typoid structures to finite levels

Abstract

A typoid is a type equipped with an equivalence relation, such that the terms of equivalence between the terms of the type satisfy certain conditions, with respect to a given equivalence relation between them, that generalise the properties of the equality terms. The resulting weak 2-groupoid structure can be extended to every finite level. The introduced notions of typoid and typoid function generalise the notions of setoid and setoid function. A univalent typoid is a typoid satisfying a general version of the univalence axiom. We prove some fundamental facts on univalent typoids, their product and exponential. As a corollary, we get an interpretation of propositional truncation within the theory of typoids. The couple typoid and univalent typoid is a weak groupoid-analogue to the couple precategory and category in homotopy type theory.