  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.
