Homotopy Type Theory
concrete category > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Contents
Definition
A concrete category is a category with a set for every object and a function for objects and .
Without the category structure
A concrete category consists of the following
-
A type , whose elements are called objects. Typically is coerced to in order to write for .
-
For each , a set , whose elements are called elements or terms.
-
For each , a set , whose elements are called arrows or morphisms.
-
For each , a function
called evaluation
-
For each , a morphism called the identity morphism, such that for all , .
-
For each , the function is an equivalence.
See also
Revision on April 25, 2022 at 16:06:06 by
Anonymous?.
See the history of this page for a list of all contributions to it.