Homotopy Type Theory concrete category > history (Rev #8)

Definition

A concrete category $C$ is a concrete precategory such that for all $a,b:A$ , the function $idtoiso_{a,b}$ is an equivalence.