Naïm Camille Favier

Hi!

My name is Naïm Camille Favier (/na'im ka.mij fa.vje/, na-EEM, نعیم).
My pronouns are he, they, or anything else.
My native language is French. Here's an actual picture of me.

Since 2024, I am a PhD student in the Logic and Types unit at Chalmers University of Technology, in Gothenburg, Sweden, working on formalising cubical type theory. My supervisor is Nils Anders Danielsson.

My scientific interests revolve around the computational trilogy: the profound interplay between the seemingly distant fields of computer science, logic and geometry. More specifically, I am interested in:

dependent type theory, particularly homotopy type theory and the univalent foundations of mathematics
category theory and ∞-analogues
constructive mathematics
formalised mathematics, especially in the Agda proof assistant
pure functional programming

Here are some other places you can find me on the Internet:

by email at n@monade.li (personal) or naimf@chalmers.se (academic)
on the Fediverse: @ncf@types.pl
on IRC: ncf at libera.chat (#agda, ##dependent, #categorytheory, …)
on various Zulip servers (Agda, HoTT, Category Theory)
on GitHub: ncfavier
on StackExchange
my ORCID is 0000-0001-9708-624X and my academic web page is here

My PGP key has fingerprint F3EB 4BBB 4E71 99BC 299C D4E9 95AF CE82 1190 8325.

Stuff I did

I have been a contributor to the 1Lab 🧊, a discoverable library of formalised (univalent) mathematics written in Cubical Agda, an implementation of cubical type theory.
My formalisation whims that are too silly for the 1Lab are in cubical-experiments.
Previously, I wrote a type-checker and evaluator for a polymorphic version of the guarded λ-calculus, during a research internship supervised by Guilhem Jaber.
I wrote a toy implementation of the jq language using a monadic variation on van Laarhoven traversals.

Music

My main non-scientific interest is music. I play the piano and I have a classical background, but I mostly listen to jazz/fusion and progressive rock.

Some musicians and bands I like

Classical. Sergei Rachmaninoff. Frédéric Chopin. César Franck. Johann Sebastian Bach. Igor Stravinsky. Edvard Grieg.

Jazz-ish. Tigran Hamasyan. Hiromi Uehara. Jesús Molina. Eldar Djangirov. Avishai Cohen. Əzizə Mustafazadə. KNOWER. mouse on the keys. Rafa Rodriguez. Les Doigts de l'Homme. DOMi & JD Beck. Valeriy Stepanov. Varra. Michel Camilo. Snarky Puppy. Farmers Market. Guy Bernfeld.

Prog-ish. Aviations. CHON. Animals as Leaders. Arch Echo. Native Construct. GEM. Dream Theater. Loam. Owane. Seda. The Fall of Troy. The Helix Nebula. DEZOLVE. The Omnific. The Resonance Project. Polyphia. Stephen Taranto. Cö shu Nie.

Other. Streetlight Manifesto (ska punk). Jamie Paige (electro pop). Jacob Collier (everything). Anything with konnakol.

Film

My favourite films are Hayao Miyazaki's Princess Mononoke and Nausicaä of the Valley of the Wind.

Links

Knowledge. Wikipedia. Sci-Hub and Library Genesis (watch out for changing domains). Library of Babel.

Mathematics. nLab. 1Lab. agda-unimath. Kerodon. The Clowder Project. The HoTT Game (may not work with recent versions of Agda, see this pull request).

Nonsense mathematics. mLab. The Art of Baskerville. Unintentional type theory. Mustard watches. halloweenmath. Falso. Locus Solum, appendix B.

Tools. quiver. Detexify.

Web comics. xkcd. Existential comics. My infinity is bigger than yours.

Misc. Zen. 無. Jabberwocky. ???.

Cool people

Friends, acquaintances, or people I generally like or admire (non-exhaustive list).

Commitments

I strongly support open access to research, and have pledged to review only for conferences and journals with open access proceedings.

I Will Fucking Piledrive You If You Mention AI Again.