2023-05-17 08:20:08 +00:00
|
|
|
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
|
|
|
|
|
2023-05-17 08:57:06 +00:00
|
|
|
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
|
2023-05-17 08:20:08 +00:00
|
|
|
|
2023-05-17 08:57:06 +00:00
|
|
|
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
|
2023-05-17 08:20:08 +00:00
|
|
|
|
|
|
|
x≡z : x ≡ z
|
2023-05-17 08:57:06 +00:00
|
|
|
-- 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
|
|
|
|
|
2023-05-17 09:53:06 +00:00
|
|
|
inner : (subst P refl px) ≡ ?
|
|
|
|
inner = ?
|
|
|
|
|
|
|
|
-- J : {A : Set a} {x : A}
|
|
|
|
-- → (B : (y : A) → x ≡ y → Set b) → {y : A}
|
|
|
|
-- → (p : x ≡ y)
|
|
|
|
-- → (b-refl : B x refl)
|
|
|
|
-- → B y p
|
2023-05-17 08:57:06 +00:00
|
|
|
-- Using subst here because that's what Σ-≡,≡→≡ uses
|
|
|
|
px≡pz : (subst P x≡z px) ≡ pz
|
2023-05-17 09:53:06 +00:00
|
|
|
px≡pz = J (λ b x≡b → let cb = convert b in (subst P x≡b px) ≡ ?) x≡z ?
|
2023-05-17 08:20:08 +00:00
|
|
|
|
|
|
|
give-me-info = ?
|
|
|
|
in
|
2023-05-17 08:57:06 +00:00
|
|
|
-- 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)
|
2023-05-17 08:20:08 +00:00
|
|
|
|
|
|
|
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
|