Masters worklog

Work log for my M.Eng (Part III) project.

Recent Posts

August Update 2

1 minute read

I have been writing and thinking and writing and thinking. Here are some thoughts. Cutting Down I have reduced the body by one (1) more page since last t...

August Update 1

1 minute read

In the past few weeks I prodded a little more at bicategorical proofs about left universal arrows. However, in the interest of time, I’m turning my attenti...

July Update 2

1 minute read

This week I spent more time bashing my head against UniMath’s bicategories.

July Update 1

3 minute read

These past few weeks I have spent some time working on the Rezk completion for duploids. Otherwise, I would like to collect my thoughts on what I wish to d...

May Update 3

less than 1 minute read

The most recent draft of my dissertation is now uploaded at https://notes.eutro.dev/cs/diss/output/writeup-2026-05-22.pdf.

May Update 3

less than 1 minute read

The most recent draft of my dissertation is now uploaded at https://notes.eutro.dev/cs/diss/output/writeup-2026-05-15.pdf. In the past couple of days I ha...

May Update 2

1 minute read

This past week I made a great deal of progress on writing. The new version is up on my notes site. Notably, I reorganized the Unital Magmoids chapter to i...

May Update 1

3 minute read

I have written the bulk of the background chapter of my dissertation, these past few days spent writing the section titled “Mixed Evaluation Order.”

April Update 2

6 minute read

I have continued to write this week. I do not have much to say on this, except that I have now made it so that I can keep multiple dated versions of the re...

April Update 1

1 minute read

I have been writing the text of my dissertation and made the rendered draft available at https://notes.eutro.dev/cs/diss/output/writeup.pdf.1

March Update 2

9 minute read

This week my most critical obligation is to organise my writings into a more dissertation-like format than this blog.

March Update 1

9 minute read

This week we resolved my issues from last week about the equalizing requirement for the upshift-downshift adjunction of a duploid. I briefly considered how...

February Update 4

5 minute read

This week I proved univalence for the single-sorted duploid arising from a (fully equalizing) adjunction between univalent categories, however I struggled ...

February Update 3

8 minute read

This week I spent a little time looking at and proving some of the last few theorems from Guillaume’s thesis.

February Update 2

10 minute read

This week I had a stab at stating the univalence condition for duploids, and seeing what I can do with it.

February Update 1

9 minute read

This week I made some progress on defining a truly single-sorted duploid from an adjunction, which does not need use a coproduct for the structure of the o...

January Update 2

8 minute read

These past two weeks I developed some theory about unital magmoids, and (separately) returned to the adjunctions of a duploid’s shift functors.

January Update 1

3 minute read

Although I did not spend a huge amount of time on the project this week, I thankfully discovered my mistake from last week about \(\mathrm{delay}\)’s lineari...

December Update

9 minute read

This update will be long, as I have struggled to sit down and actually write one of these. Hopefully over the course of the project I manage to get into a be...

Project Proposal Phase 2

3 minute read

Today I submitted my “phase 2” project proposal, for approval by the examiners. The text of the proposal is presented below.

Project Proposal Phase 1

less than 1 minute read

I will be working with Jon Sterling on the denotational semantics of effectful languages with mixed evaluation-order (CBV/CBN).