[Agda] Equivalence axiom => extensionality

[Thorsten Altenkirch]

> 
> Clearly, isomorphic implies bijective but the other way around seems
> not provable constructively, afaik. From surjective you get an iverse 
> g' : B → A such that g ∘ g' = id but not the other way
> around. Injectivity doesn't give you a function, but even if you
> assume that it is split (or what is the word) you just get another
> function g'' : B → A, such that g'' ∘ g = id but I don't see why g'' =
> g' or how you could in general construct one function which is both
> left and right inverse to f. Or am I overlooking something obvious?

As Thierry just pointed out to me, I am. If g ∘ g' = id 
then g ∘ g' ∘ g = g and because g is monic g' ∘ g = id.


Cheers,
Thorsten

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100623/1f6bdc86/attachment.html