The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Nov 2, 2011, at 8:27 PM, Victor Porton 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.

As far as I understand this statement makes sense in 

1. ZF and its versions ( either by themselves or simulated in some other 
deduction system ) 

2. possibly type systems with syntactic sub-typing (see below)

It does not make any obvious sense in the standard type systems for the 
following reason. The composition M o E maps S to B' . You want to choose B' 
such that this functions is "identity on S" which makes no sense in the usual 
type theory since identity there can only be from S to S and not from S to 
B'. 

If there was a syntactically distinguished class of "inclusions" in the type 
system ( which actually can make sense for another reason - the theory of 
cofibrations ) then your construction would  start from an inclusion E : S -> 
B and create a new type B' and ( let me use M^{-1} instead of M ) a 
decomposition S -> B' -> B of E where the first function is a "syntactic 
inclusion" and the second is a bijection.

Vladimir.