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

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