From 793017b1908138ca1dd09d2e46048aaa6338d7b4 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 7 Mar 2017 13:33:37 -0500 Subject: [PATCH] feat(library/init/logic.lean): add Sort -> Prop universe lift --- library/init/logic.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/library/init/logic.lean b/library/init/logic.lean index f92e78dc61..82d5d4b917 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -947,7 +947,7 @@ structure {r s} ulift (α : Type s) : Type (max s r) := up :: (down : α) namespace ulift -/- βijection between α and ulift.{v} α -/ +/- Bijection between α and ulift.{v} α -/ lemma up_down {α : Type u} : ∀ (b : ulift.{v} α), up (down b) = b | (up a) := rfl @@ -955,6 +955,19 @@ lemma down_up {α : Type u} (a : α) : down (up.{v} a) = a := rfl end ulift +/- Universe lifting operation from Sort to Type -/ +structure plift (α : Sort u) : Type u := +up :: (down : α) + +namespace plift +/- Bijection between α and slift α -/ +lemma up_down {α : Sort u} : ∀ (b : plift α), up (down b) = b +| (up a) := rfl + +lemma down_up {α : Sort u} (a : α) : down (up a) = a := +rfl +end plift + /- Equalities for rewriting let-expressions -/ lemma let_value_eq {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β) : a₁ = a₂ → (let x : α := a₁ in b x) = (let x : α := a₂ in b x) :=