Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
10 lines (7 sloc) 327 Bytes
(** 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.
Axiom univalence_axiom : Univalence.
Global Existing Instance univalence_axiom.
You can’t perform that action at this time.