Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
Require Import Types.Universe.Require Import Types.Universe.
(** 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.) *)
Axiom univalence_axiom : Univalence.
Existing Instance univalence_axiom.