[[!redirects concrete precategories]] #Contents# * table of contents {:toc} ## Definition ## A concrete precategory $C$ is a [[precategory]] with a type $El(A)$ for every object $A:Ob(C)$ and for every object $A:Ob(C)$ and $B:Ob(C)$, there is a [[monic function]] $i_{A,B} \colon Hom(A,B) \to (El(A) \to El(B))$ and an function $(-)((-))\colon Hom(a,b) \times U(a) \to U(b)$ such that for every morphism $f \colon Hom(A,B)$ and $g \colon Hom(B,C)$ and every element $x:U(A)$, $(g \circ f)(x) = g(f(x))$ and $id_A(x) = x$. ## See also ## * [[family of objects in a concrete precategory]] * [[concrete category]] * [[HilbR]] * [[ETCS with elements]]