# Homotopy Type Theory extensional category > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

# Contents

## Idea

An evaluational concrete category where morphisms satisfy the axiom of extensionality.

## Definition

An extensional category $C$ is a evaluational concrete category such that for morphisms $f:Hom(A,B)$ and $g:Hom(A,B)$, if $f(x) = g(x)$ for all elements $x:El(A)$, then $f = g$.

## Examples

• The category $Set$ of sets and functions is an extensional category.

• The category $Mon$ of monoids and monoid homomorphisms is an extensional category.

• The category $\mathbb{Z}Mod$ of $\mathbb{Z}$-modules and $\mathbb{Z}$-module homomorphisms is an extensional category.

• The category $\mathbb{Z}Alg$ of $\mathbb{Z}$-algebras and $\mathbb{Z}$-algebra homomorphisms is an extensional category.

• The category $CRing$ of commutative rings and commutative ring homomorphisms is an extensional category.

• The category $Field$ of fields and field homomorphisms is an extensional category.

• The category $HeytAlg$ of Heyting algebras and Heyting algebra homomorphisms is an extensional category.

• The category $Frm$ of frames and frame homomorphisms is an extensional category.

• The category $Conv$ of set-truncated convergence spaces and continuous functions is an extensional category.

• The category $Top$ of set-truncated topological spaces and continuous functions is an extensional category.

• The category of empty sets and functions is an extensional category.