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))$.

See also

• family of objects in a concrete precategory
• concrete category
• HilbR
• ETCS?