Compare commits

...

2 commits

Author SHA1 Message Date
79e8a2300a it works
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
2024-09-18 06:38:08 -05:00
2f4c87ea1d shortbio 2024-09-18 06:32:18 -05:00
2 changed files with 28 additions and 6 deletions

View file

@ -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 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].
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].
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].

View file

@ -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
open import Data.Bool.Base hiding (_∧_; __)
```
</details>
@ -196,17 +196,39 @@ 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) → leftFace j
(k = i0) → compPath-filler
(λ 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 b = {! !}
gf north = refl
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)
```