# Homotopy Type Theory category (Rev #1)

## Idea

Similarly to the univalence axiom we make two notions of sameness the same. This leads to some nice concequences.

## Definition

A category is a precategory such that for all $a,b:A$, the function $idtoiso_{a,b}$ from Lemma 9.1.4 (see precategory) is an equivalence.

## Properties

### Lemma 9.1.8

In a category, the type of objects is a 1-type.

Proof. It suffices to show that for any $a,b:A$, the type $a=b$ is a set. But $a=b$ is equivalent to $a \cong b$ which is a set. $\square$

## Examples

The univalence axiom implies immediately that $\mathcal{Set}$ is a category. One can also show that any precategory of set-level structures such as groups, rings topologicial spaces, etc. is a category.

Revision on September 4, 2018 at 12:10:24 by Ali Caglayan. See the history of this page for a list of all contributions to it.