module Equivalence where

open import Relation.Binary.PropositionalEquality
open import Data.Product

J : {A : Set}{a : A}(P : {x : A} → a ≡ x → Set)
    → P refl → {b : A}(p : a ≡ b) → P p
J P m refl = m

contr : Set → Set
contr A = Σ A (λ c → (x : A) → c ≡ x)

fiber : ∀ {A B : Set} → (A → B) → B → Set
fiber f b = Σ _ (λ a → b ≡ f a)

isEquiv :  ∀ {A B : Set} → (f : A → B) → Set
isEquiv f = (b : _) → contr (fiber f b)

wEquiv : Set → Set → Set
wEquiv A B = Σ (A → B) isEquiv

isEquivId : ∀ {A} → isEquiv {A = A} (λ a → a)
isEquivId {A} = λ a → (a , refl) , (λ x → lem a x)
   where lem : (a : A) → (z : Σ A (_≡_ a)) → (a , refl) ≡ z
         lem a (b , ab) = J  (λ {x} ax → _≡_ {A = Σ A (_≡_ a)} (a , refl) (x , ax)) refl ab
--       lem a (.a , refl) = refl


mapEquiv : ∀ {A B : Set} → A ≡ B → wEquiv A B
mapEquiv refl = (λ a → a) , isEquivId

postulate EqAx : ∀ {A B} → isEquiv (mapEquiv {A} {B})

ext : ∀ {A B : Set} → (f g : A → B) → ((a : A) → f a ≡ g a) → f ≡ g
ext f g p = {!!}