The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

The statement as you say it wouldn't even make sense in Coq, because S and B' would be incompatible types.  In Coq I'd say something more like:

forall (S B:Type) (E:S->B), injective E -> exists B':Type, exists M:B -> S + B', bijective M /\ comp M E = inl B'.

(Here " inl B' " is the injection S -> S + B').  The proof would be to set B' to { b:B | forall s:S, E s <> b } and then construct M according to whether b is in the image or not (which would need an application of what I call classic_dec : forall P:Prop, { P } + { ~ P } to construct the function, and probably an application of functional_extensionality to prove the result as well).

But it's starting to sound like the theory you're formalizing is possibly tied tightly enough with ZF-type semantics that using a ZF system would indeed be appropriate.  I think Adam wasn't necessarily saying that using a ZF system would automatically be a bad idea, just that in most of mathematics outside pure set and model theory (and even in quite a bit of set theory), it's more natural to formulate it in type theoretic terms.

And if using a ZF system is appropriate, I'd probably set up a typeclass to encode the ZF[C] theory, use the ZF module to establish the soundness of the theory, then do the development using an abstract ZF base.
-- 
Daniel Schepler

On Wed, Nov 2, 2011 at 5:27 PM, Victor Porton <porton AT narod.ru> wrote:

I want to prove the following statement (or maybe to make it an axiom):

Let S and B are sets and E is an injection from S to B. Then exists a set B' and a bijection M from B to B' such that
M o E = id_S.

Read why I want this axiom and what I do with it at
http://www.mathematics21.org/generalization.html
http://www.mathematics21.org/binaries/gen/generalization.pdf
(In this short article I prove this statement in ZF using the axiom of foundation.)

How to make this statement provable in Coq? At last resort we could make it an axiom. But how we could ensure that consistency of ZF implies consistency of type theory together with axiom? As it is hard to prove I would be resistant to making it just an axiom. But I want it very much.

--
Victor Porton - http://portonvictor.org