[Agda] Equivalence axiom => extensionality

[Dan Licata]

Agda agrees, in the sense that the following bit of code shows that
weakly equivalent sets are isomorphic (append it to
http://www.cs.cmu.edu/~drl/tmp/equivax.tgz).  Note that this result does
not use the equivalence axiom.

  module Iso where
    record Iso (A B : Set) : Set where
     field
      l : A -> B
      r : B -> A
      lr : (x : _) -> Id (l (r x)) x
      rl : (x : _) -> Id (r (l x)) x
    
    back : ∀ {A B : Set} -> WEq A B -> (B -> A)
    back (f , by) b = fst (fst (by b))
    
    iso : ∀ {A B : Set} -> WEq A B -> Iso A B
    iso {A} {B} w = record {l = fst w; r = back w; lr = lr w; rl = rl w}
      where lr : (w : WEq A B) (x : B) -> Id (fst w (back w x)) x
            lr (f , by) x with  (by x)
            ... | ((a , b) , c) = b

            rl : (w : WEq A B) (x : A) -> Id (back w (fst w x)) x
            rl (f , by) x with by (f x)
            ... | ((a , b) , c) = IdM.sym (IdM.substeq fst (c (x , Refl)))

-Dan


On Jun23, Thorsten Altenkirch wrote:
> > 
> > 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.
> 
> 

> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda