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

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

# Contents

## Idea

A concrete category with a good notion of evaluation of morphisms and elements.

## Definition

An evaluational category $C$ is a concrete category with a function $(-)((-)): Hom(A,B) \times El(A) \to El(B)$ for objects $A:Ob(C)$ and $B:Ob(C)$ such that for morphisms $f:Hom(A,B)$ and $g:Hom(B,C)$ and elements $x:El(A)$, $(g \circ f)(x) = g(f(x))$.

## Examples

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

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

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

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

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

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

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

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

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

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

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

## Non-examples

• The category $Rel$ of sets and relations is not an evaluational category.