Homotopy Type Theory family of objects in a concrete precategory > history (Rev #1)

Definition

In a concrete precategory $C$, given an object $A:Ob(C)$ an $A$-indexed family of objects in $C$ is a function $B:El(A) \to Ob(C)$.