(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
basic constructions:
strong axioms
further
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.
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.
Solomon Feferman, Typical ambiguity: Trying to have your cake and eat it too
Last revised on June 16, 2022 at 12:21:17. See the history of this page for a list of all contributions to it.