I'd like to "smuggle" a Prop in a Type. The usual notion of universe inclusion should make it safe to do so, but I can't seem to do it without using an inductive type. Am I missing something obvious?

Concretely, I'd like to define

```
Lift : Prop -> Type
lift : t -> Lift t
unlift : Lift t -> t
```

and of course have `(unlift (lift x)) = x`

. With an inductive type, I can have `lift x`

be a pair `(x, Prop)`

and I'm done, but I can't seem to be able to do the same if I restrict myself to functions. Is there some trick I'm missing, or are inductive types indispensable to be able to do that?

```
Definition Lift (P : Prop) : Type := P.
Definition lift {t : Prop} (x : t) : Lift t := x.
Definition unlift {t : Prop} (x : Lift t) : t := x.
```

```
Lemma unlift_lift {t : Prop} (x : t) : unlift (lift x) = x.
Proof. easy. Qed.
Lemma lift_unlift {t : Prop} (x : Lift t) : lift (unlift x) = x.
Proof. easy. Qed.
```

but is this satisfactory?

I'm only using universe inclusion/Coq subtyping

Right, I guess I should have thought to say that I don't want to depend on universe inclusion itself, indeed.

Does this make use of universe inclusion?

```
Definition Lift (P : Prop) : Type :=
forall T : Prop, (P -> Type -> T) -> T.
Definition lift : forall t : Prop, t -> Lift t :=
fun t x T f => f x Prop.
Definition unlift : forall t : Prop, Lift t -> t :=
fun t f => f t (fun x _ => x).
About Lift.
About lift.
About unlift.
```

yes

easy way to check: replace Prop with SProp

Last updated: Nov 29 2023 at 17:01 UTC