Stream: Miscellaneous

Topic: Lifting Prop to Type without inductive types


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 08 2021 at 00:00):

but is this satisfactory?

view this post on Zulip Paolo Giarrusso (Dec 08 2021 at 00:01):

I'm only using universe inclusion/Coq subtyping

view this post on Zulip 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.

view this post on Zulip 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).

About Lift.
About lift.
About unlift.

view this post on Zulip Gaëtan Gilbert (Dec 08 2021 at 16:10):

yes
easy way to check: replace Prop with SProp


Last updated: Mar 28 2024 at 09:01 UTC