Updates

src/2023-05-06-equiv.lagda.md

@@ -58,7 +58,6 @@ we can just give $y$ again, and use the `refl` function above for the equality
 proof
 
 ```
-Bool-id-is-equiv .equiv-proof y .fst = y , Bool-id-refl y
 ```
 
 The next step is to prove that it's contractible. Using the same derivation for
@@ -74,25 +73,66 @@ when $i = i0$, and something that equals the fiber $y_1$'s preimage $x_1$ when
 $i = i1$, aka $y \equiv proj_1\ y_1$.
 
 ```
+
+-- 2023-05-13: Favonia's hint is to compute "ap g p", and then concatenate
+-- it with a proof that g is the left-inverse of f
+-- ok i'm pretty sure this should be the g = f^-1
+Bool-id-inv : Bool → Bool
+Bool-id-inv b = (((Bool-id-is-equiv .equiv-proof) b) .fst) .fst
+
+Bool-id-inv-is-inv : (b : Bool) → Bool-id-inv (Bool-id b) ≡ b
+Bool-id-inv-is-inv true =
+    Bool-id-inv (Bool-id true)
+  ≡⟨ refl ⟩
+    Bool-id-inv true
+  ≡⟨ refl ⟩
+    -- This isn't trivially true?
+    (Bool-id-is-equiv .equiv-proof true .fst) .fst
+  ≡⟨ ? ⟩
+    true
+  ∎
+Bool-id-inv-is-inv false = ?
+
+Bool-id-is-equiv .equiv-proof y .fst = y , Bool-id-refl y
+
 Bool-id-is-equiv .equiv-proof y .snd y₁ i .fst =
   let
     eqv = snd y₁
     -- eqv : Bool-id (fst y₁) ≡ y
+    -- this is the second pieece of the other fiber passed in
 
     eqv2 = eqv ∙ sym (Bool-id-refl y)
     -- eqv2 : Bool-id (fst y₁) ≡ Bool-id y
+    -- concat the fiber (Bool-id (fst y₁) ≡ y) with (y ≡ Bool-id y) to get the
+    -- path from (Bool-id (fst y₁) ≡ Bool-id y)
 
     -- Ok, unap doesn't actually exist unless f is known to have an inverse.
     -- Fortunately, because we're proving an equivalence, we know that f has an
-    -- inverse, in particular going from y to x, which in thise case is also y.
+    -- inverse, in particular going from y to x, which in this case is also y.
     eqv3 = unap Bool-id eqv2
 
-    Bool-id-inv : Bool → Bool
-    Bool-id-inv b = (((Bool-id-is-equiv .equiv-proof) b) .fst) .fst
+    -- Then, ap g p should be like:
+    ap-g-p : Bool-id-inv (Bool-id (fst y₁)) ≡ Bool-id-inv (Bool-id y)
+    ap-g-p = cong Bool-id-inv eqv2
+
+    -- OHHHHH now we just need to find that Bool-id-inv (Bool-id y) ≡ y, and
+    -- then we can apply it to both sides to simplify
+    -- So something like this:
+
+    -- left-id : Bool-id-inv ∙ Bool-id ≡ ?
+    -- left-id = ?
 
     eqv3′ = cong Bool-id-inv eqv2
     give-me-info = ?
     -- eqv3 : fst y₁ ≡ y
+
+    -- Use the equational reasoning shitter
+    final : y ≡ fst y₁
+    final =
+        y
+      ≡⟨ ? ⟩
+        fst y₁
+      ∎
 ```
 
 Blocked on this issue: https://git.mzhang.io/school/cubical/issues/1
@@ -124,11 +164,11 @@ Bool-id-is-equiv .equiv-proof y .snd y₁ i .snd j =
     a-b = Bool-id-refl y
     c-d = y₁ .snd
   in
+  ?
   ```
 
 Blocked on this issue: https://git.mzhang.io/school/cubical/issues/2
   ```
-  ?
 ```
 
 ## Other Equivalences

src/2023-05-14-biinv-equiv.agda

@@ -0,0 +1,86 @@
+{-# OPTIONS --cubical #-}
+
+open import Agda.Primitive.Cubical
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Prelude hiding (Σ-syntax)
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Equiv.BiInvertible
+open import Data.Bool
+open import Data.Product.Base
+
+id : ∀ {ℓ} {A : Type ℓ} → A → A
+id x = x
+
+linv : {A B : Type} (f : A → B) → Type
+linv {A} {B} f = Σ[ g ∈ (B → A) ] (g ∘ f ≡ id)
+
+rinv : {A B : Type} (f : A → B) → Type
+rinv {A} {B} f = Σ[ g ∈ (B → A) ] (f ∘ g ≡ id)
+
+biinv : {A B : Type} (f : A → B) → Type
+biinv f = linv f × rinv f
+
+--------------------------------------------------------------------------------
+
+Bool-id : Bool → Bool
+Bool-id true = true
+Bool-id false = false
+
+Bool-id-pointwise : (b : Bool) → Bool-id (Bool-id b) ≡ b
+Bool-id-pointwise true = refl
+Bool-id-pointwise false = refl
+
+Bool-id-equiv : Bool-id ∘ Bool-id ≡ id
+Bool-id-equiv = funExt Bool-id-pointwise
+
+Bool-linv : linv Bool-id
+Bool-linv .fst = Bool-id
+Bool-linv .snd = funExt Bool-id-pointwise
+
+Bool-rinv : rinv Bool-id
+Bool-rinv .fst = Bool-id
+Bool-rinv .snd = funExt Bool-id-pointwise
+
+Bool-id-biinv : BiInvEquiv Bool Bool
+Bool-id-biinv = biInvEquiv
+  Bool-id
+  Bool-id Bool-id-pointwise
+  Bool-id Bool-id-pointwise
+
+Bool-id-iso : Iso Bool Bool
+Bool-id-iso = iso
+  Bool-id
+  Bool-id
+  Bool-id-pointwise
+  Bool-id-pointwise
+
+Bool-id-biinv-equiv : Bool ≃ Bool
+Bool-id-biinv-equiv = Bool-id , isoToIsEquiv Bool-id-iso
+
+Bool-id-path : Bool ≡ Bool
+Bool-id-path = ua Bool-id-biinv-equiv
+
+--------------------------------------------------------------------------------
+
+Bool-neg : Bool → Bool
+Bool-neg true = false
+Bool-neg false = true
+
+Bool-neg-pointwise : (b : Bool) → Bool-neg (Bool-neg b) ≡ b
+Bool-neg-pointwise true = refl
+Bool-neg-pointwise false = refl
+
+Bool-neg-iso : Iso Bool Bool
+Bool-neg-iso = iso
+  Bool-neg
+  Bool-neg
+  Bool-neg-pointwise
+  Bool-neg-pointwise
+
+Bool-neg-equiv : Bool ≃ Bool
+Bool-neg-equiv = isoToEquiv Bool-neg-iso
+
+Bool-neg-path : Bool ≡ Bool
+Bool-neg-path = ua Bool-neg-equiv

src/2023-05-15-equiv-try-again.agda

@@ -0,0 +1,84 @@
+{-# OPTIONS --cubical #-}
+
+open import Agda.Primitive.Cubical
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Prelude
+open import Data.Bool
+open import Data.Fin
+
+--------------------------------------------------------------------------------
+
+ap : {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
+ap f p i = f (p i)
+
+--------------------------------------------------------------------------------
+
+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
+
+convert-fiber : (y : Other) → fiber convert y
+convert-fiber Top = true , refl
+convert-fiber Bottom = false , refl
+
+convert-fiber-is-contr : (y : Other) → (fz : fiber convert y) → convert-fiber y ≡ fz
+convert-fiber-is-contr y fz i =
+  let
+    fx : fiber convert y
+    fx = convert-fiber y
+
+    x : Bool
+    x = fst fx
+
+    z : Bool
+    z = fst fz
+
+    eqv : convert z ≡ y
+    eqv = snd fz
+
+    eqv2 : convert x ≡ y
+    eqv2 = snd fx
+
+    eqv3 : y ≡ convert x
+    eqv3 = sym eqv2
+
+    eqv4 : convert z ≡ convert x
+    eqv4 = eqv ∙ eqv3
+
+    -- This is the `ap g p`
+    eqv5 : convert-inv (convert z) ≡ convert-inv (convert x)
+    eqv5 = ap convert-inv eqv4
+
+    eqv6 : z ≡ x
+    eqv6 = sym (convert-inv-id z) ∙ eqv5 ∙ convert-inv-id x
+
+    eqv7 : x ≡ z
+    eqv7 = sym eqv6
+
+    -- y ≡ convert x
+    ouais = fz
+  in
+  -- z = fst fz
+  -- convert-fiber y ≡ fz
+  -- (x , x₁ ≡ y) ≡ (z , z₁ ≡ y)
+  --  - x ≡ z
+  --  - (x₁ ≡ y) ≡ (z₁ ≡ y)
+  eqv7 i , ?
+
+convert-is-equiv : isEquiv convert
+convert-is-equiv .equiv-proof y = convert-fiber y , convert-fiber-is-contr y
+
+convert-equiv : Bool ≃ Other
+convert-equiv = convert , convert-is-equiv