Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

14 lines (10 sloc) 0.587 kb
Require Import Paths Univalence Funext.
(** This file asserts univalence as a global axiom, along with its
basic consequences. If you want function extensionality as well,
use [ExtensionalityAxiom]. *)
Axiom univalence : univalence_statement.
Definition equiv_to_path := @equiv_to_path univalence.
Definition equiv_to_path_section := @equiv_to_path_section univalence.
Definition equiv_to_path_retraction := @equiv_to_path_retraction univalence.
Definition equiv_to_path_triangle := @equiv_to_path_triangle univalence.
Definition equiv_induction := @equiv_induction univalence.
Jump to Line
Something went wrong with that request. Please try again.