[[!redirects concrete categories]] #Contents# * table of contents {:toc} ## 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]]