nLab typical ambiguity

Contents

Context

Universes

Foundations

Contents

Ideas

In (homotopy) type theory with type universes, by the typical universe ambiguity or just typical ambiguity, for short, one refers to the universe level remaining implicit, as long as a proof assistant is or would be able to deduce it from context.

Both Russell and Tarski style universes can be typically ambiguous or not.

Examples

  • Coq uses Russell style universes with typical ambiguity.

  • Agda uses Russell style universes without typical ambiguity: you always have to explicitly indicate the universe level.

  • The HoTT Book (first edition) uses Russell style universes with (except for a few places) typical ambiguity.

References

  • Solomon Feferman, Typical ambiguity: Trying to have your cake and eat it too

  • Blog Post

Last revised on June 16, 2022 at 08:21:17. See the history of this page for a list of all contributions to it.