# nLab univalent setoid

Contents

## In higher category theory

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

## Idea

There are two ways to show that two objects of a presetoid are identified with each other: by way of the identity type, and by way of the type of isomorphisms in the core pregroupoid of a presetoid. Univalent setoids are precisely the presetoids which the two notions of identifying objects with each other coincide.

## Definition

For each object $a:Ob(A)$ and $b:Ob(A)$ of a presetoid $A$, there is a function

$\mathrm{idtoiso}(a, b):(a =_A b) \to (a \cong_A b)$

from the identity type to the type of isomorphisms in the core pregroupoid $\mathrm{Core}(A)$ of $A$. A presetoid is a univalent setoid or a saturated setoid if for each object $a:Ob(A)$ and $b:Ob(A)$ the function

$\mathrm{idtoiso}(a, b):(a =_A b) \simeq (a \cong_A b)$

is an equivalence of types.

Since every type of morphisms in the core of the presetoid is a h-set, this means that every univalent setoid is a h-groupoid.