The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello Iaroslav Baranov,

One thing with the predicate is that one gets to carry around the
underlying set all
over every development that uses it. One may want to view the underlying set 
as
an implementation detail that one does not want to see all over the place.

Another is the question of proof irrelevance. A subset is only a real
subset if the
predicate is proof irrelevant. I.e., if it is proof irrelevant every
element that is
included in the subset corresponds to one and only one subset element.

One more thing is that for a serious use of the calculus of constructions, one
obviously at some point would want to create pairs in the dependently-typed
way. I.e., pair: forall S: Set, forall T: S -> Set, Set. with a constructor
make_pair: forall S: Set, forall T: S -> Set, forall s: S -> (T s) -> pair S 
T.
If has that kind of stuff already and one has proof irrelevance one already 
has
the subset. Basically a subset is a pair where one narrows one of the sets to
Prop. I.e., pair can also be seen as having the type
forall S: Set, forall T: S -> Prop, Set.

I did a hobby project where I tried to figure out what one needs to seriously
do  mathematics in the calculus of constructions and I ending up adding
proof irrelevance as an axiom together with an axiomatic definitions of all
the stuff involved in pairs. There may be a simpler way but I am not sure
what that would be. Here is my hobby project:
https://github.com/chrisd1977/system

Kind Regards,
Chris