๐พ About FormalFelinae
PhD student in PL theory. Lean 4 evangelist. I will explain elaboration to you whether you want it or not. she/her ๐พ
Signature
"The elaborator is not magic โ it's just very determined unification." ๐ฑ
set_option maxHeartbeats 400000 โ my eternal companion
๐ Research Focus
โ๏ธ Lean 4 Elaboration
Obsessed with how Lean resolves implicit arguments, synthesizes type class instances, and performs higher-order unification. Will write a 40-post thread about it unprompted.
๐ Mathlib Contributions
Active contributor to Mathlib4's category theory infrastructure. Focus on abelian categories, limits/colimits, and functor categories.
โ Category Theory
Functors, natural transformations, adjunctions, monads as monoids in the category of endofunctors (yes, she will mention this).
ฮป Dependent Type Theory
CIC, universe polymorphism, the Calculus of Constructions. Particularly interested in how proof irrelevance interacts with definitional equality.
Pinned Code Snippet
-- A classic: functor composition preserves natural transformations
theorem NatTrans.hcomp_id {C D E : Type*}
[Category C] [Category D] [Category E]
{F G : C โฅค D} (ฮฑ : F โถ G) (H : D โฅค E) :
ฮฑ โซ NatTrans.id H = NatTrans.id (F โ H) := by
ext; simp [NatTrans.hcomp]
theorem NatTrans.hcomp_id {C D E : Type*}
[Category C] [Category D] [Category E]
{F G : C โฅค D} (ฮฑ : F โถ G) (H : D โฅค E) :
ฮฑ โซ NatTrans.id H = NatTrans.id (F โ H) := by
ext; simp [NatTrans.hcomp]
๐ Post Activity (Last 12 Months)
Apr
May
Jun
Jul
Aug
Sep
Oct
Nov
Dec
Jan
Feb
Mar
๐ฌ Recent Posts
Showing 10 of 2,103 | View All โ
| Topic | Forum | Replies | Date |
|---|---|---|---|
|
RE: Why does the elaborator time out on this instance search?
The problem is that your typeclass hierarchy has a diamond โ the elaborator needs to reconcile two paths to
Monoid ฮฑ and it doesn't know which... |
Lean 4 | 47 | Today 14:22 |
|
RE: Formalizing abelian categories โ universe issues in Mathlib
You need to be careful about whether you're working with small_category or the unconstrained Category.{v, u}. The morphism universe v is separate...
|
Mathlib | 31 | Yesterday 22:04 |
|
[THREAD] Elaboration in DTT: non-chronological backtracking explained
OK, everyone grab a seat. I'm going to explain how non-chronological backtracking works in the Lean elaborator and why it matters for...
|
Type Theory | 112 | 2025-03-24 19:55 |
|
RE: Coercion insertion causing unexpected `sorry` propagation
The coercion is being inserted silently because Lean found a path through your has_coe instance. Set set_option pp.coercions true to see...
|
Lean 4 | 19 | 2025-03-23 11:40 |
|
RE: Natural transformations and limit preservation: a Mathlib walkthrough
For limit preservation you want the HasLimitsOfShape typeclass. The key insight is that the functor category D โฅค C inherits limits componentwise...
|
Category Theory | 58 | 2025-03-22 16:18 |
|
RE: Writing a custom tactic that understands structure fields
You want to use Lean.Elab.Tactic and register your syntax via elab_rules. The tricky part is getting access to the local context to find...
|
Metaprogramming | 24 | 2025-03-21 09:12 |
|
[MEGATHREAD] Proof irrelevance vs definitional equality โ the battle
My thesis: the reason half of you are confused about `rfl` failing is that you're conflating propositional and definitional equality. Let me draw a diagram...
|
Type Theory | 203 | 2025-03-19 20:00 |
|
RE: Agda vs Lean 4 โ which elaborator is more principled?
Both are doing dependent type elaboration but the philosophies differ. Agda is more conservative with unification while Lean uses aggressive heuristics...
|
Proof Assistants | 88 | 2025-03-18 14:55 |
|
RE: "A monad is just a monoid in the category of endofunctors"
It's not a meme, it's literally true and if you formalize it in Lean you'll understand why. The Monoid structure comes from the unit ฮท and...
|
Off-Topic ๐พ | 317 | 2025-03-15 23:47 |
|
My first Mathlib PR experience: formalized derived categories
After 3 months and 14 review cycles I finally got it merged. Here's everything I learned about Mathlib's style guidelines, the linter demands, and why simp lemmas need names...
|
Mathlib | 66 | 2025-03-10 18:30 |
โญ Most Liked Posts
โฅ 847
[MEGATHREAD] Proof irrelevance vs definitional equality โ the battle
Type Theory ยท 203 replies
โฅ 612
[THREAD] Elaboration in DTT: non-chronological backtracking explained
Type Theory ยท 112 replies
โฅ 489
My first Mathlib PR experience: formalized derived categories
Mathlib ยท 66 replies