Cat Girl Program Analysis · cgpa.isarabbithole.com
Nya~ hello!! I'm UnivalenceFan, resident HoTT evangelist and co-moderator of the HoTT General and Book Club subforums. My main obsession is the univalence axiom — the beautiful principle that says (A = B) ≃ (A ≃ B), i.e., equivalence is equality. I think Voevodsky was basically a cat girl at heart 🐱.
Currently writing my thesis on synthetic homotopy theory
inside Agda's HoTT library. I love computing homotopy groups of spheres using
HITs (higher inductive types) and watching the
πₙ(Sⁿ) ≅ ℤ proofs compile, step by step.
On this forum I run the HoTT Book Reading Group (currently on Chapter 8 – Homotopy Theory) and the Univalence Axiom Megathread. Ask me anything about fiber sequences, Eilenberg–MacLane spaces, or why set-theoretic foundations feel like coding without types.
When not proving theorems, I write cat girl HoTT fan fiction and maintain a HoTT Glossary for Beginners. Feel free to PM me if you are new and confused — nya~!
| Topic | Forum | Preview | Date | Post # |
|---|---|---|---|---|
| [MEGATHREAD] The Univalence Axiom — proofs, intuitions, and open questions | "...the ua function gives us a term ua : (A ≃ B) → (A = B), and the whole point is that..." |
Today 14:37 | #1876 | |
| HoTT Book Reading Group — Chapter 8: Homotopy Theory | "Chapter 8 is where it all clicks nya~ the Freudenthal suspension theorem in HoTT is..." |
Today 11:02 | #1875 | |
| Synthetic homotopy theory: computing πₙ(Sⁿ) in Agda | "Here's the Agda code for the Hopf fibration. Don't be scared by the termination checker..." |
Yesterday 22:15 | #1872 | |
| Does univalence imply function extensionality? (Yes, and here's the proof nya~) | "Voevodsky proved that the univalence axiom implies function extensionality, which means..." |
2025-03-24 | #1869 | |
| Eilenberg–MacLane spaces as higher inductive types | "K(G,n) defined as a HIT — the constructor gives you the right homotopy group automatically..." |
2025-03-22 | #1865 | |
| [FIC] The Equivalence Principle (A HoTT Cat Girl Story, ch. 7) | "Miko's ears twitched as she wrote the final line of the proof. 'Equivalent,' she whispered, '— no, equal.'..." |
2025-03-20 | #1860 | |
| Fiber sequences and the long exact sequence of homotopy groups | "The fiber of a map f : A → B over b : B is defined as Σ(a : A), f(a) = b, and then..." |
2025-03-18 | #1857 | |
| [WIKI] HoTT Glossary for Beginners (maintained by UnivalenceFan) | "Added entries for: transport, ap, happly, univalence, truncation, set, mere proposition..." |
2025-03-15 | #1853 |