Stefan Monnier (Dec 07 2021 at 23:07): 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.
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?
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).
About Lift.
About lift.
About unlift.
yes
easy way to check: replace Prop with SProp
Last updated: Oct 12 2024 at 11:01 UTC