(** To assume the Univalence axiom outright, import this file.
    (Doing this instead of simply positing Univalence directly
    avoids creating multiple witnesses for the axiom in
    different developments.) *)

Require Import Types.Universe.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Axiom univalence_axiom : Univalence.
Global Existing Instance univalence_axiom.