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 CC is a concrete category with a function ()(()):Hom(A,B)×El(A)El(B)(-)((-)): Hom(A,B) \times El(A) \to El(B) for objects A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) such that for morphisms f:Hom(A,B)f:Hom(A,B) and g:Hom(B,C)g:Hom(B,C) and elements x:El(A)x:El(A), (gf)(x)=g(f(x))(g \circ f)(x) = g(f(x)).

Examples

  • The category SetSet of sets and functions is an evaluational category.

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

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

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

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

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

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

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

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

  • The category TopTop 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 RelRel of sets and relations is not an evaluational category.

See also

Revision on May 18, 2022 at 13:55:00 by Anonymous?. See the history of this page for a list of all contributions to it.