Homotopy Type Theory family of objects in a concrete precategory > history

< family of objects in a concrete category