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

open import HottBook.Chapter2

isContr : Type → Type
isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)

fiber : {A B : Type} (f : A → B) (y : B) → Type
fiber {A = A} f y = Σ[ x ∈ A ] f x ≡ y

record isEquiv {A : Type} {B : Type} (f : A → B) : Set where
  no-eta-equality
  field
    equiv-proof : (y : B) → isContr (fiber f y)
open isEquiv

infix 4 _≃_
_≃_ : (A : Set) (B : Set) → Type
A ≃ B = Σ (A → B) \ f → (isEquiv f)

--------------------------------------------------------------------------------

data Other : Type where
  Top : Other
  Bottom : Other

convert : Bool → Other
convert true = Top
convert false = Bottom

convert-inv : Other → Bool
convert-inv Top = true
convert-inv Bottom = false

convert-inv-id : (b : Bool) → convert-inv (convert b) ≡ b
convert-inv-id true = refl
convert-inv-id false = refl

center-fiber : (y : Other) → fiber convert y
center-fiber Top = true , refl
center-fiber Bottom = false , refl

center-fiber-is-contr : (y : Other) → (fz : fiber convert y) → center-fiber y ≡ fz
center-fiber-is-contr y fz =
  let
    fx = center-fiber y
    x = proj₁ fx
    z = proj₁ fz

    px : convert x ≡ y
    px = proj₂ fx

    pz : convert z ≡ y
    pz = proj₂ fz

    eqv3 : convert x ≡ convert z
    eqv3 = px ∙ sym pz

    eqv4 : convert-inv (convert x) ≡ convert-inv (convert z)
    eqv4 = ap convert-inv eqv3

    x≡z : x ≡ z
    x≡z = sym (convert-inv-id x) ∙ eqv4 ∙ convert-inv-id z

    give-me-info = ?
  in
  Σ-≡,≡→≡ (x≡z , ?)

convert-is-equiv : isEquiv convert
convert-is-equiv .equiv-proof y = center-fiber y , center-fiber-is-contr y

convert-equiv : Bool ≃ Other
convert-equiv = convert , convert-is-equiv