Another proof that reluniv_functor_with_ess_surj issurjective (assuming R is essentially surjective)

[fizruk]

My hypothesis is that we do not need any extra assumptions like AC or univalent C for the functor between RelUniv(J) and RelUniv(J') to be surjective.

Current WIP proof starts with some stronger assumptions which should be relaxed:

• R is split essentially surjective ➞ R is essentially surjective
• S is an equivalence ➞ S is full and reflects pullbacks (however, this might be insufficient);

Now I have an mapping on objects to go from RelUniv(J') to RelUniv(J) which I should document properly. Proving that it is a right inverse directly is cumbersome, so @peterlefanulumsdaine suggested another approach:

• show an isomorphism instead of identity first;
• show that RelUniv(J') is univalent (under some conditions)
• use univalence to get identity and
• complete proof of surjectivity

Finally, I plan to

• clean up the code :)

[fizruk]

I did not figure out how to turn this proof into one that relies of R being merely essentially surjective. In fact I am now convinced that it is not true (although I do not give a counterexample) :)

So I am leaving this simply as another proof (with different assumptions).

[benediktahrens]

Is this used anywhere? If not, I suggest removing this setting.