Commit 2020-12-15 10:30 407d1386
View on Github →chore(category_theory/equivalence): weaken essential surjectivity (#3821) Weaken essential surjectivity to be a Prop, rather than the data of the inverse.
chore(category_theory/equivalence): weaken essential surjectivity (#3821) Weaken essential surjectivity to be a Prop, rather than the data of the inverse.