Contents

Definition

A concrete category $C$ is a category with a set $El(A)$ for every object $A:Ob(C)$ and a function $(-)((-)): Hom(A,B) \times El(A) \to El(B)$ for objects $A:Ob(C)$ and $B:Ob(C)$.

Without the category structure

A concrete category $A$ consists of the following

• A type $A_0$, whose elements are called objects. Typically $A$ is coerced to $A_0$ in order to write $x:A$ for $x:A_0$.

• For each $a:A$, a set $el_A(a)$, whose elements are called elements or terms.

• For each $a,b:A$, a set $hom_A(a,b)$, whose elements are called arrows or morphisms.

• For each $a,b:A$, a function

  $$(-)((-)): hom_A(a,b) \times el_A(a) \to el_A(b)$$

  called evaluation

• For each $a:A$, a morphism $1_a:hom_A(a,a)$ called the identity morphism, such that for all $x:el_A(a)$, $1_a(x) = x$.

• For each $a,b:A$, the function $idtoiso_{a,b}$ is an equivalence.

See also

• concrete dagger 2-poset?
• concrete precategory
• HilbR
• ETCS?