Stream: Miscellaneous

Topic: Lifting Prop to Type without inductive types

Stefan Monnier (Dec 07 2021 at 23:07):

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?

Paolo Giarrusso (Dec 07 2021 at 23:59):

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

Paolo Giarrusso (Dec 07 2021 at 23:59):

``````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.
``````

Paolo Giarrusso (Dec 08 2021 at 00:00):

but is this satisfactory?

Paolo Giarrusso (Dec 08 2021 at 00:01):

I'm only using universe inclusion/Coq subtyping

Stefan Monnier (Dec 08 2021 at 02:34):

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

Yannick Forster (Dec 08 2021 at 16:03):

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).