The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 08/13/2013 05:09 PM, Victor Porton wrote:
> [[[
> Definition A := { x:nat | x>  1 }.
>
> Record B := {
>               x: nat;
>               c: x>  1
> }.
> ]]]
>
> A and B are essentially the same thing.
>
> But for proofs of equality of objects of type B proof irrelevance is 
> required, while for proofs of equality of objects of type A proof irrelevance 
> is not required. Right?
>    

No.  These types are isomorphic at quite a shallow level.  The first one 
just uses an "abbreviation" via the library type family [sig].