Definition 4.54.

Let \(\phi^*\colon T \to S\) be a morphism of logoi.

  1. We say that \(\phi^*\) provides enough families if, for every family \(v\) in \(S\), there exists a family \(u\) in \(T\) and a morphism \(v \to \phi^*(u)\) in \(\Fam(S)\).

  2. If \(\phi^*\) preserves dependent products, we say that \(\phi^*\) provides enough univalent families if the same condition holds after restricting to univalent families.

  3. We say that \(\phi^*\) is object-generating if the closure of the image of \(\phi^*\) under colimits and finite limits is all of \(S\).