Contents

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