#
Homotopy Type Theory
set > history (Rev #5)

## Contents

## Definition

A **set** consists of

### As univalent setoids

A set is a setoid $T$ where the canonical functions

$a:T, b:T \vdash idtoiso(a,b):(a =_T b) \to (a \equiv b)$

are equivalences

$p: \prod_{a:A} \prod_{b:A} (a =_T b) \cong (a \equiv b)$

## Examples

## See also

## References

Revision on April 27, 2022 at 14:47:45 by
Anonymous?.
See the history of this page for a list of all contributions to it.