wip 2.13

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

@@ -74,19 +74,17 @@ center-fiber-is-contr y fz =
     P : Bool → Type
     P b = convert b ≡ y
 
+    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
     -- 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
+    px≡pz = J (λ b x≡b → let cb = convert b in (subst P x≡b px) ≡ ?) x≡z ?
 
     give-me-info = ?
   in

src/HottBook/Chapter2Exercises.lagda.md

@@ -1,7 +1,9 @@
 ```
 module HottBook.Chapter2Exercises where
 
-open import Relation.Binary.PropositionalEquality
+import Relation.Binary.PropositionalEquality as Eq
+open Eq
+open Eq.≡-Reasoning
 Type = Set
 transport = subst
 ```
@@ -26,5 +28,70 @@ Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences.
 [2.3.6]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.6
 [2.3.7]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.7
 
-Here is the definition of transportconst from lemma 2.3.5:
+### Exercise 2.13
 
+Show that (2 ≃ 2) ≃ 2.
+
+```
+open import Function.HalfAdjointEquivalence
+open import Data.Bool
+open _≃_
+
+id : {A : Type} → A → A
+id x = x
+
+Bool-id-equiv : Bool ≃ Bool
+Bool-id-equiv = record
+  { to = id
+  ; from = id
+  ; left-inverse-of = λ _ → refl
+  ; right-inverse-of = λ _ → refl
+  ; left-right = λ _ → refl
+  }
+
+Bool-neg : Bool → Bool
+Bool-neg true = false
+Bool-neg false = true
+
+Bool-neg-refl : (x : Bool) → Bool-neg (Bool-neg x) ≡ x
+Bool-neg-refl true = refl
+Bool-neg-refl false = refl
+
+Bool-neg-refl-refl : (x : Bool)
+  → cong Bool-neg (Bool-neg-refl x) ≡ Bool-neg-refl (Bool-neg x)
+Bool-neg-refl-refl true = refl
+Bool-neg-refl-refl false = refl
+
+Bool-neg-equiv : Bool ≃ Bool
+Bool-neg-equiv = record
+  { to = Bool-neg
+  ; from = Bool-neg
+  ; left-inverse-of = Bool-neg-refl
+  ; right-inverse-of = Bool-neg-refl
+  ; left-right = Bool-neg-refl-refl
+  }
+
+Bool-to : (Bool ≃ Bool) → Bool
+Bool-to eqv = eqv .to true
+
+Bool-from : Bool → (Bool ≃ Bool)
+Bool-from true = Bool-id-equiv
+Bool-from false = Bool-neg-equiv
+
+Bool-left-inverse : (eqv : Bool ≃ Bool) → Bool-from (Bool-to eqv) ≡ eqv
+Bool-left-inverse eqv =
+  J (λ the what → Bool-from (Bool-to the) ≡ eqv) refl ?
+
+Bool-right-inverse : (x : Bool) → Bool-to (Bool-from x) ≡ x
+Bool-right-inverse true = refl
+Bool-right-inverse false = refl
+
+Bool≃Bool≃Bool : (Bool ≃ Bool) ≃ Bool
+Bool≃Bool≃Bool = record
+  { to               = Bool-to
+  ; from             = Bool-from
+  ; left-inverse-of  = Bool-left-inverse
+  ; right-inverse-of = Bool-right-inverse
+  ; left-right       = ?
+  }
+```