<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><blockquote type="cite"><div><font class="Apple-style-span" color="#000000"><br></font>Clearly, isomorphic implies bijective but the other way around seems<br>not provable constructively, afaik. From surjective you get an iverse <br>g' : B → A such that g ∘ g' = id but not the other way<br>around. Injectivity doesn't give you a function, but even if you<br>assume that it is split (or what is the word) you just get another<br>function g'' : B → A, such that g'' ∘ g = id but I don't see why g'' =<br>g' or how you could in general construct one function which is both<br>left and right inverse to f. Or am I overlooking something obvious?<br></div></blockquote><div><br></div><div><div>As Thierry just pointed out to me, I am. If g ∘ g' = id </div><div>then g ∘ g' ∘ g = g and because g is monic g' ∘ g = id.</div></div><div><br></div><div><br></div><div>Cheers,</div><div>Thorsten</div><div><br></div></div></body></html>