Self-introduction + Subobject classifier in mathlib

Stream: new members

[Pablo Donato]

Hi everyone! :hello:

I'm Pablo Donato, a post-doctoral researcher at the Grothendieck Institute under the supervision of Olivia Caramello since July. Previously I did a PhD where I tried to design better graphical user interfaces for proof assistants, taking inspiration from recent developments in deep inference proof theory. I know some folks here have done great work on GUIs, e.g.
ProofWidgets for interacting with goals and Paperproof for visualizing proofs. I would definitely be excited to collaborate on these subjects in the future :big_smile:

---

Now I have just started learning both topos theory and Lean 4, with the goal of formalizing the former into the latter (joint project with @Anthony Bordg, see #new members > Topoi in Mathlib). I am currently going through the first chapter of the classic Sheaves in Geometry and Logic, and would like to do some hands-on practice by formalizing basic notions and results in Lean. In particular, it has been suggested by @Adam Topaz that subobject classifiers are an easy target for formalization that have not made their way to mathlib yet.

Thus I was wondering if I could obtain write access to non-master branches to start working on subobject classifiers? I would basically implement definitions and theorems from Sheaves in Geometry and Logic in a module Mathlib.CategoryTheory.Subobject.Classifier.

[Yaël Dillies]

Welcome! What's your GitHub username? We need it to give you access

[Yaël Dillies]

You're also more likely to get a quick invitation if you send your message in #mathlib4:github permission

[Pablo Donato]

Ah yes I forgot! My username is Champitoad

[Luigi Massacci]

Hey Pablo:wave: