How does one begin a website? What should be the first sentence to meet the reader's eyes? I have elected to circumvent this predicament by, careful readers may note, omitting the first sentence of this website entirely.

I work at Radix Trading B.V. (Amsterdam), and hold a PhD in pure mathematics from JHU (summer 2022) supervised by Emily Riehl.

My interests are: formal category theory, higher categories, homotopy type theory, and computer programming including formalisation.

Today's day of the day is -- well, this joke requires javascript :(.

📧 tslil@posteo.net

Papers

• Towards the theory of proof-relevant categories (dissertation), arXiv version in preparation.
• Regular Calculi I: Graphical Regular Logic, joint with B. Fong and D. I. Spivak, on the novel structure of regular calculi, and their use as an ergonomic and graphical syntax for regular logic and relations. In preparation is the companion, Regular Calculi II: Further Theory
• A misunderstanding of Isbell‘s obstruction to monoidal strictification, a careful look at the now widely disseminated argument about an obstruction to strictifying the associator which shows that, as stated, the argument is not obviously correct and that the truth is more subtle.
• Bi-representations and bi-initial objects are not so different, joint with L. Moser, on 2-categorical and double-categorical theorems characterising when pseudo-functors into Cat are representable, with applications to bi-adjunctions and 2-dimensional limits. (Cahiers de Topologie et Géométrie Différentielle Catégoriques, LXIII-3).
• 2-limits and 2-terminal objects are too different, joint with L. Moser, on the failure of all theorems of the form “a 2-dimensional limit is a 2-dimensional terminal object in a 2-dimensional slice category of cones”. (Appl. Categor. Struct. 2022)

Formalisations

A sample of some of the formalisation work i have done in Homotopy Type Theory.

• (In preparation)Wild globular type theory and globular T-categories, work towards formalising enough of general globular types, dependent globular types, and operations thereupon to state the definition of wild globular T-categories.
• WildCat in HoTT, joint with Ali Caglayan, Morgan Opie, Emily Riehl, Mike Shulman, on formalising the definitions and early theory of “wild” higher categories – those higher categories whose operations are only coherent to a certain level – in Coq-HoTT.
• The Yoneda lemma and dependent path induction are logically equivalent, a formalised proof in UniMath.
• Univalence implies function extensionality, a formalised proof in Agda-HoTT, using Voevodsky's trick but otherwise a novel approach via graphs of functions.

Notes

Here you can find some of the other things i have written up. Usually this is because i thought they were interesting, sometimes the notes were intended to help me better understand things, and sometimes they represent a transcript of my explorations or talks. In no particular order,

• Cocategories, an expository note on and the means through which cocategories give rise to enrichment.
• Polynomials, a degree of generality, an expository note designed as an introduction and motivation for the early theory of polynomial functors.
• enriched base change, mates, and universal algebra, an exploration i did in my first summer before JHU (before i knew about Lawvere theories and really much else).
• there are countably infinitely many one-combinator bases, a hand-out i wrote for an oral presentation as part of my honours degree in mathematics at UCT, in 2014.
• (incomplete) Working notes i compiled as i learnt category theory, beginning from elementary definitions working up to a statement of homology at the level of Ab-categories, and many things besides.
• (more coming soon)

Teaching

William Kelso Morrill Award

In April of 2021 i was honoured to receive from my department the William Kelso Morill Award for Excellence in Mathematics. This award is given to the PhD candidate who “best displays the traits of William Kelso Morrill in his teaching, love of teaching, love of mathematics, and concern for students”.

I was nominated for this award by my students, one of whom wrote “Teaches and simplifies material very well. Takes the time to work with students and gives a lot of feedback on homework and portfolio. Grades within a reasonable timeframe and is easy to reach out to. Reaches out to struggling students. Overall caring person.”

Introduction to Proofs: Course development assistant

In Spring of 2019 Prof. Riehl and i designed and ran an introductory course for mathematics. The course was split into three components: a ‘standard’ introduction to proofs, an enquiry-based learning approach to metric spaces, and a discussion-format section on the notion of proof in mathematics.

The first third of the course used the structure of the book “How to Prove It” by Velleman, and had homework generated by Prof. Riehl and i, as well as some extracted from the book.

During the first third, for a change of perspective and so as to introduce notions of constructive mathematics, i lectured for a week on computer proof assistants. The class re-learnt propositional calculus through the use of the Coq computer proof assistant, as available online at Collacoq, and the goal was a modest reading comprehension of Coq code.

The script for these lectures, containing an introduction to type theory, Coq, and Collacoq – to the extent necessary for, and phrased within the broader of the course – as well as reading exercises, is available here.

• Lectures as HTML file
• Source code for lectures (processed by coqdoc to create the above)

In addition i created a written homework sheet, with feedback from Prof. Riehl, on constructive mathematics, available here.

In the second third of the course we switched to an IBL (enquiry-based learning) format and explored some of the early theory of metric spaces. Students completed the appropriate (portion of) the appropriate script before class and took it in turns to present their difficulties or successes with the material to one another. Here are the scripts i designed, with editing and input from Prof. Riehl. These are all made available under the terms of theef Creative Commons Attribution-ShareAlike 4.0 International License.

• Script 1 (PDF)
• Script 2 (PDF)
• Script 3 (PDF)
• Script 4 (PDF)
• Script 5 (PDF)
• Script 6 (PDF)
• Script 7 (PDF)

Mentor in and organiser for the JHU Directed Reading Programme

I have been a mentor in the JHU Directed Reading Programme since its inception. The programme pairs undergraduate students with graduate students for one-on-one independent studies over the course of a semester.

Out of a desire to see the budding programme succeed, through 2018-2019 i helped organise the programme, and represented our then fledgling chapter at the 2018 Directed Reading Programme Network and Workshop at MIT.

I have mentored projects on the following topics: Fundamentals of General Topology, Braid Group Representations and Knot Invariants, Category Theory, and Homotopy Type Theory.

Abstracts of the projects may be found on the programme website.

ODE Autumn 2019/Spring 2021: Portfolios experiment

As head teaching assistant to Prof. Richard Brown – director of undergraduate studies –, in the usually calculation-homework-centric differential equations “service course”, i helped construct and orchestrate an experiment in student evaluation. Despite a class size of 175, we designed the course around semester-long digital portfolios: every week students were charged with creating ‘artefacts’ covering some minimum amount of content, and we were careful to leave this task open-ended.

The goal was to afford students the freedom to express, challenge, and reinforce their understanding in their terms, and in doing so emphasise a fundamental facet of mathematics: creativity. Initially most students produced text-based documents closely matching some of the example artefacts. However, with weekly small-group TA meetings focused solely on crafting these portfolio entries, students gained in confidence throughout the semester. They regularly created artefacts exceeding the minimum requirements, about topics they enjoyed, connections to other courses they had noticed, and work they were proud of. Moreover, the diversity in the style and medium of entries grew noticeably too.

Most importantly, we the TAs spent the semester emphasising the room and need for creativity in engaging with and doing mathematics. Ultimately the course was ranked the highest among all service courses by the students.

Calculus III & ODE: Head T.A. and WeBWorK admin.

In the Autumn of 2018 i was offered the role of Head Teaching Assistant for the Calculus III course at JHU. The instructor, Prof. Riehl, decided that the course should have an online homework component and so we settled on the WeBWorK platform.

During the course i was responsible for managing the online platform, exporting grades, and at times, programming new exercises for the students.

Owing to my experience in this position and my desire to see an online homework platform succeed, i was offered the same role for the course in the Autumn of 2019, though this time the instructor was Prof. Richard Brown, the director of undergraduate studies. I was offered the same role in Autumn of 2020 and Spring 2021, again with Prof. Richard Brown, but this time for the ODE course.

Introduction to Calculus: Sole instructor

In Autumn of 2017 i was offered the chance to run the introductory mathematics course designed to bridge high-school and university level mathematics. Although there was an assigned course text, the syllabus, homework, tests and exams, teaching, and marking were left entirely to me. Thus, i designed and ran the course.

Intersession Course: Primary Instructor

In January of 2017 several colleagues and i applied for, and were granted permission by the university to run an intersession course on recreational mathematics entitled “Recreational Mathematics for All”. We divided up the course into several, related topics and each co-organiser was given a few lectures to develop their topic. I lectured on secret sharing, building on the number theory that had gone before, and paving the way to the group theory that would come after. For evaluation the students submitted an elaboration of a topic that they had met during the course.

Cumulative experience as a teaching assistant

I have served as a Teaching Assistant in courses concerning: Real Analysis, Introductory Abstract Algebra, Linear Algebra, Differential Equations, The Calculus Sequence, and String Theory.

Notable Service

• Primary organiser of the 2019 Category Theory Octoberfest at JHU.
• Co-organiser of the JHU chapter of the Directed Reading Programme (Autumn & Spring 2018, 2019).
• Organiser of Slideshow Karaoke for the Graduate Lunch Seminar at JHU.
• Founder of the Maths Postgraduate Tea Party, Univ. of Cape Town – a biweekly meeting of graduates, comprising peer lectures and discussions over tea.
• Various roles in “Algorithm Circle”, a theoretical comp. sci. club, Univ. of Cape Town, holding free and open lectures, as well as competition preparation. Lecturer (2011-2015), Vice-chairman (2012, 2014), Chairman (2013).
• Organiser of a Haskell programming course, Univ. of Cape Town, 2011 & 2012 – a free and open Haskell language programming course.

Hobbies

What do i do when i'm not doing maths? A small catalogue of some of my endeavours

• 3D printing & electronics
• Exploring cellular automata
• Coding, computer generated art, and playing and creating music

I maintain a Gemini capsule with various entries about computing and my hobbies. Of particular interest is the ability to play the game of Tak against a bot of mine served over CGI over Gemini.

gemini://l-3.space

It's quite possible that your browser doesn't (yet!) support the Gemini protocol; l-3.space is compiled to bare-bones HTML automatically and available at https://l-3.space.

Talks

• 2021/11/11
  Structures for witnessed composition, an approach to higher categories
  UVA Topology Seminar
• September 2021
  Representation presentation: to present a representative, 2-representative theorem
  CT 20→21, video talk.
• 2021/08/10
  Invitation to the next dimension: 2D doesn't mean double the work, only twice as much
  Topos Institute, Berkeley.
• 2021/07/16
  Graphical Regular Logic: the complete 2D picture
  (slides)
  Applied Category Theory 2021, University of Cambridge.
• 2020/11/20
  More than merely composition: towards the theory of proof-relevant categories & algebras
  Carnegie Mellon University HoTT Seminar
• 2020/10/14
  2-lessons from Australian Category Theory: Mates and Doctrinal Adjunction
  (slides - warning, large file!)
  Johns Hopkins Category Theory Seminar
• 2020/09/16
  BI DOUBLing categories we'll see
  MULTIple morphisms acting weakly
  Two out of the four
  Have laws rather poor
  But the last is coherent VIRTUALLY!
  (slides - warning, large file!)
  Johns Hopkins Category Theory Seminar
• 2019/11/05 & 2019/11/12
  Within and not without: an apology for internal languages
  Johns Hopkins Category Theory Seminar
• 2019/09/17
  Induction and construction: the pointless theory of localic topox
  Johns Hopkins Category Theory Seminar
• 2019/06/15
  Towards proof relevant category theory, as modelled by globular T-categories
  HoTT-UF workshop at Types 2019,
  Oslo
• 2019/06/06
  What is proof relevant category theory?
  HoTT-UF project,
  CAS, Oslo
• 2019/04/02
  The univalence axiom, a brief & incomplete tour
  (slides)
  School and Workshop on Univalent Mathematics,
  University of Birmingham
• 2019/02/19
  Polynomial functors, a degree of generality
  Johns Hopkins Category Theory Seminar
• 2019/02/10
  Audience of high-school students, Fractions: ratio of two integers or universal machine?
  Johns Hopkins Mathematics Tournament
• 2018/11/30
  Homotopy Type Theory, the confluence of logic
  and space (slides)
  University Seminar: Logic Across Disciplines,
  George Washington University
• 2018/11/08
  What is an LCC?
  Johns Hopkins Category Theory Seminar
• 2018/09/20
  Type Theory and Categories, the unbearable likeness of being
  (slides)
  Oral Speciality Exam,
  Johns Hopkins University
• 2017/11/15 and 2017/12/05
  What do we mean when we say spectra?   and
  ‘Rings, Modules and Algebras in Infinite Loop Space Theory’ at a glance
  Graduate Course: Topics in Algebraic Topology,
  Johns Hopkins University
• 2017/11/30
  An Intuitive Description of Toposes, Toposes as a Description of Intuitionism
  University Seminar: Logic Across Disciplines,
  George Washington University
• 2017/10/12
  All good things must come to an end
  Johns Hopkins Category Theory Seminar
• 2017/04/09
  The calculus of fractions and homotopy theory
  Graduate Course: Algebraic Topology II,
  Johns Hopkins University
• 2016/12/12
  A monad is just … (with an eye to universal algebra)
  Johns Hopkins Category Theory Seminar

Conferences

• Programme Associate, Higher Categories & Categorification, Spring 2020, MSRI, USA
• Category Theory Octoberfest 2019, JHU, USA
• Homotopy Type Theory 2019, CMU, USA
• Category Theory 2019, University of Edinburgh, UK
• Types 2019, Oslo, Norway
• HoTT-UF Project, CAS Oslo, Norway
• Summer School on Higher Topos Theory and Univalent Foundations, 2019, University of Leeds, UK
• School and Workshop on Univalent Mathematics, 2019, University of Birmingham, UK
• Vladimir Voevodsky Memorial Conference, IAS, USA
• Category Theory Octoberfest 2018, CUNY, USA
• Directed Reading Programme Network and Workshop 2018, MIT, USA
• Category Theory Octoberfest 2017, CMU, USA
• Category Theory 2017, UBC, Canada

License

Except where otherwise noted, content on this website is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.