src/content/partials/shortBio.md

@@ -1,7 +1,7 @@
 I'm a computer science master's student at the [University of Minnesota][1], advised by [Favonia].
 My current research topic is in cubical type theory and formalization of the Serre spectral sequence.
 
-I've also worked as a researcher for [SIFT], specializing in compilers and binary analysis. Previously I worked as a software engineer at [Swoop Search] and [AWS].
+I also work as a researcher for [SIFT], specializing in compilers and binary analysis. Previously I worked as a software engineer at [Swoop Search] and [AWS].
 
 Before that, I was a CTF hobbyist. I created [EasyCTF], a cybersecurity competition for high schoolers.
 I also briefly played with the CTF team [Project Sekai][pjsk].

src/content/posts/2024-09-18-hcomp/index.lagda.md

@@ -22,7 +22,7 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Core.Primitives
 open import Cubical.HITs.Susp.Base
 open import Cubical.HITs.S1.Base
-open import Data.Bool.Base hiding (_∧_; _∨_)
+open import Data.Bool.Base
 ```
 
 </details>
@@ -196,39 +196,17 @@ Between the second and third steps, I used functoriality of the $\mathsf{ap}$ op
 ```
   fg (loop i) k =
     let
+      leftFace = λ j → compPath-filler (λ i → f (merid false i)) (λ j → f (merid true (~ j))) j i
+
       u = λ j → λ where
         (i = i0) → base
         (i = i1) → f (merid true (~ j))
-        (k = i0) → compPath-filler
+        (k = i0) → leftFace j
-                      (λ i → f (merid false i))
-                      (λ j → f (merid true (~ j))) j i
         (k = i1) → loop i
     in hcomp u (f (merid false i))
 ```
 
 ```
   gf : (b : Susp Bool) → g (f b) ≡ b
-  gf north = refl
+  gf b = {!   !}
-  gf south = merid true
-    -- Both merid true and merid false work here... why pick true?
-  gf (merid true i) j = merid true (i ∧ j)
-```
-
-For the last part, we are trying to prove:
-
-`(merid false ∙ (λ i₁ → merid true (~ i₁))) i ≡ merid false i`
-
-```
-  gf (merid false i) j =
-    let
-      u = λ k → λ where
-        (i = i0) → north
-        (i = i1) → merid true (j ∨ ~ k)
-        (j = i0) →
-          let u = λ k' → λ where
-            (i = i0) → north
-            (i = i1) → merid true (~ k')
-          in hfill u (inS (merid false i)) k
-        (j = i1) → merid false i
-    in hcomp u (merid false i)
 ```