| Posts: | 643 |
| Rank: | Functor Fancier |
| Joined: | Oct 14, 2021 |
| Last active: | Just now |
| Posts/day: | 0.68 |
| Location: | ∞-Topos, Meow |
| Website: | adjunctions.moe |
| Pronouns: | she/her |
| Timezone: | UTC+∞ |
Heya~ I'm MewMorphism, resident obsessive over category theory and its deep connections to type theory and homotopy type theory. If there's an adjunction lurking somewhere, I'll find it — probably while drinking way too much tea, nya~
My main focus is understanding how functors and natural transformations
illuminate the structure of type systems. The correspondence between categories and type theories
is basically magic to me — every time I see a new connection I let out a little mew of delight.
I'm currently deep-diving into adjoint logic — the idea that
∀ and ∃ quantifiers form an adjoint pair between propositions and sets
in a topos. Lawvere showed this in 1969 and it still breaks my brain every time I think about it.
Also poking at the Curry-Howard-Lambek correspondence: types are objects, programs are morphisms, and type constructors are functors. Cartesian closed categories model simply-typed lambda calculus, nya~
📚 Currently reading: Categories for the Working Mathematician (Mac Lane), Category Theory in Context (Riehl), and the HoTT Book for the fourth time.
| Topic | Forum | Replies | Date |
|---|---|---|---|
|
The Adjoint Functor Theorem — proof walkthrough nya~
So the GAFT basically says: a functor G: 𝒟→𝒞 has a left adjoint iff it preserves all limits and satisfies the solution set condition...
|
∫ Category Theory | 34 | Today, 02:41 |
|
HoTT Book Ch.5 — Induction vs Recursion question
The W-types chapter is making me lose my mind. Are W-types the "right" way to encode inductive types categorically? I feel like the relationship to initial algebras is the key...
|
🌀 HoTT | 19 | Yesterday, 21:15 |
|
Monads vs Comonads — a duality kata
Every monad T = G∘F arises from an adjunction F⊣G. The Kleisli and Eilenberg-Moore categories give you the "smallest" and "largest" such adjunctions respectively...
|
∫ Category Theory | 28 | Mar 25, 2026 |
|
Yoneda Lemma as a type-theoretic statement
Nat(よA, F) ≅ F(A). In type theory this looks like: ∀B. (A→B)→F(B) ≅ F(A). That's just parametricity! Mew, the universe conspires...
|
λ Type Theory | 41 | Mar 24, 2026 |
|
Cartesian Closed Categories and STLC — full walkthrough
CCC is where category theory and simply-typed lambda calculus live in perfect harmony. Product = conjunction, exponential = implication, the counit IS function application...
|
∫ Category Theory | 52 | Mar 22, 2026 |
|
Univalence Axiom explained to a skeptic
The univalence axiom says (A ≃ B) ≃ (A = B). Equivalence is equality. This isn't just philosophical hand-waving — it has concrete computational content in cubical type theory...
|
🌀 HoTT | 67 | Mar 21, 2026 |
|
Kan extensions: everything is a Kan extension
Mac Lane's famous quote deserves a full thread. Left/right Kan extensions subsume limits, colimits, adjoints, and more. Lan_K(F)(d) = colim(K↓d → 𝒞 → F) nya~
|
∫ Category Theory | 23 | Mar 19, 2026 |
|
Dependent types as fibrations over a base category
A dependent type B(x) indexed over x:A corresponds to a fibration p: E→A. The comprehension category structure packages this beautifully. Seely's original paper is a gem...
|
λ Type Theory | 15 | Mar 17, 2026 |
|
Internal logic of a topos — overview thread
Every topos has an internal higher-order intuitionistic logic. The subobject classifier Ω plays the role of "the type of propositions". Lawvere-Tierney topologies give you modal operators...
|
⊗ Topos Theory | 31 | Mar 14, 2026 |
|
Lawvere's Fixed Point Theorem — connections to Gödel/Cantor
Lawvere's fixed point thm is a gorgeous categorical generalization: if φ: A → Yᴬ is surjective on objects, then every f: Y→Y has a fixed point. Diagonal arguments fall out...
|
∫ Category Theory | 44 | Mar 11, 2026 |