type-theory/src/2023-05-17-equiv-no-cubical.agda

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

    un-ap-convert : (a b : Bool) → (p : convert a ≡ convert b) → a ≡ b
    un-ap-convert a b p =
      let inner = ap convert-inv p in
      sym (convert-inv-id a) ∙ inner ∙ convert-inv-id b

    cx≡cz : convert x ≡ convert z
    cx≡cz = px ∙ sym pz

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

    x≡z : x ≡ z
    -- x≡z = sym (convert-inv-id x) ∙ eqv4 ∙ convert-inv-id z
    x≡z = un-ap-convert x z cx≡cz

    P : Bool → Type
    P b = convert b ≡ y

    -- Using subst here because that's what Σ-≡,≡→≡ uses
    px≡pz : (subst P x≡z px) ≡ pz
    px≡pz = J
      (λ b p′ →
        let
          x≡b : x ≡ b
          x≡b = ?

          convert-the : convert b ≡ y
          convert-the = ?
        in
        (subst P x≡b px) ≡ convert-the
      ) x≡z refl

    give-me-info = ?
  in
  -- Goal type:
  --  transport (λ cx → convert cx ≡ y)
  --  (
  --    sym (convert-inv-id x)
  --    ∙ ap convert-inv (px ∙ sym pz)
  --    ∙ convert-inv-id z
  --  )
  --  (proj₂ (center-fiber y))  <-- this is just px
  --  ≡ proj₂ fz                <-- this is just pz
  Σ-≡,≡→≡ (x≡z , px≡pz)

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