From 978f1d1bea44b520789a8eb9d2bc2c3c0e8554be Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 28 Sep 2016 11:37:05 -0700
Subject: [PATCH] feat(library/init/logic): add universe lifting operation

---
 library/init/logic.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/library/init/logic.lean b/library/init/logic.lean
index 3771f08d95..e8157fe5eb 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -952,3 +952,16 @@ match h₁, h₂ with
 | (is_true h_c),  h₂ := h_c
 | (is_false h_c), h₂ := false.elim h₂
 end
+
+/- Universe lifting operation -/
+structure {r s} ulift (A : Type s) : Type (max 1 s r) :=
+up :: (down : A)
+
+namespace ulift
+/- Bijection between A and ulift.{v} A -/
+lemma up_down {A : Type u} : ∀ (b : ulift.{v} A), up (down b) = b
+| (up a) := rfl
+
+lemma down_up {A : Type u} (a : A) : down (up.{v} a) = a :=
+rfl
+end ulift