tslil clingman
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 am a 5th year graduate student, my
supervisor is Emily
Riehl.
My interests are: formal category theory, higher categories, and
homotopy type theory.
Today's day of the day is -- well, this joke requires
javascript :(.
📧 tslil@jhu.edu
200 Krieger Hall, 3400 N. Charles Street, Baltimore, MD 21218
This website and its content is also available
through IPFS
via DNSLink
at /ipns/tslil.xyz
, or directly
at /ipns/QmeGwomQyT5TtBfYAuA5KHr5XJEuiEvWAdhcapppUftVU5
.
Papers
- (In preparation) On 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.
- (In preparation) Towards proof-relevant category
theory, an exposition of some of the early theory and
notions.
- (In preparation) Graphical Regular Logic, joint with
B. Fong and D. I. Spivak, on the relationship between regular
categories, relational po-cotageries, and the graphical notation
of Fong-Spivak.
- 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.
- 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”.
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. Write-up pending.
- 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).
- (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
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.
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 the Creative
Commons Attribution-ShareAlike 4.0 International License.
Mentor in 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.
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.
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, 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.
Talks
- 2020/11/20
More than merely composition: towards the theory of
proof-relevant categories & algebras
(slides - warning, large
file!)
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 seeMULTIple morphisms
acting weaklyTwo out of the fourHave laws rather
poorBut 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
(slides - warning, large file!)
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
Hobbies
What do i do when i'm not doing maths? A small catalogue of some
of my endeavours
License

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