feat(hott/init): add lift to initialization

hott/init/datatypes.hlean

@@ -22,6 +22,9 @@ inductive empty : Type
 inductive eq.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
 refl : eq a a
 
+structure lift.{l₁ l₂} (A : Type.{l₁}) : Type.{max l₁ l₂} :=
+up :: (down : A)
+
 structure prod (A B : Type) :=
 mk :: (pr1 : A) (pr2 : B)
 

hott/init/logic.hlean

@@ -66,6 +66,14 @@ calc_refl  eq.refl
 calc_trans eq.trans
 calc_symm  eq.symm
 
+namespace lift
+  definition down_up.{l₁ l₂} {A : Type.{l₁}} (a : A) : down (up.{l₁ l₂} a) = a :=
+  rfl
+
+  definition up_down.{l₁ l₂} {A : Type.{l₁}} (a : lift.{l₁ l₂} A) : up (down a) = a :=
+  lift.rec_on a (λ d, rfl)
+end lift
+
 -- ne
 -- --