Univalent typoids
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.
Cite
@article{arxiv.2205.06651,
title = {Univalent typoids},
author = {Iosif Petrakis},
journal= {arXiv preprint arXiv:2205.06651},
year = {2022}
}