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

Definition

In a concrete homotopy 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)$.

See also

• concrete homotopy precategory?
• family