[Agda] Equivalence axiom => extensionality

[Bas Spitters]

Hi Thorsten,

> Actually, I thought this has nothing to do with Type Theory....
>
> Two sets A,B are isomorphic if there are functions f : A → B and f' :
> B → A, which are inverse to each other. A and B are bijective (one
> says equinumerous but this I find misleading) if there is one function
> g : A → B which is both injective and surjective, i.e. both monic and
> epic.
>
> 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?

I am not entirely sure about the context you are working in, but
we have, as you note:
 g (g' b) = b
Hence,
 g (g' (g a)) = g a
By injectivity,
 (g' (g a)) = a

Did I misunderstand what you were saying?

Bas