Stream: Coq users

Topic: dependent sum subtypes

view this post on Zulip Raul (Apr 20 2023 at 17:56):

Hi!

I have a dependent sum type and a subtype of the first component (not necessarily a decidable) type.
Is the type of pairs with first component in the subtype a subtype of the sum?
How would it be called?
How can this be formalized in Coq (I'm working with sigT)?

view this post on Zulip Guillaume Melquiond (Apr 20 2023 at 19:29):

I am not sure to fully grasp the question. Are you wondering if there is a trivial isomorphism between {y: {x:A & P x} & Q (projT1 y)} and {x:A & prod (P x) (Q x)}? Then yes. But if you are wondering whether they are convertible types, then no.

Last updated: Oct 04 2023 at 21:01 UTC