From d842be9c52a06067c1e5ad4dbccdfda4b6cc50f8 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Thu, 6 Nov 2014 13:38:59 -0500
Subject: [PATCH] feat(library/hott) add univalence axiom

---
 library/hott/axioms/ua.lean | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 library/hott/axioms/ua.lean

diff --git a/library/hott/axioms/ua.lean b/library/hott/axioms/ua.lean
new file mode 100644
index 000000000..aadaefd92
--- /dev/null
+++ b/library/hott/axioms/ua.lean
@@ -0,0 +1,8 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jeremy Avigad, Jakob von Raumer
+-- Ported from Coq HoTT
+import hott.path hott.equiv
+open path Equiv
+
+axiom ua {A B : Type} [H : A ≃ B] : A ≈ B