August Update 2
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...
Work log for my M.Eng (Part III) project.
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...
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...
This week I spent more time bashing my head against UniMath’s bicategories.
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...
The most recent draft of my dissertation is now uploaded at https://notes.eutro.dev/cs/diss/output/writeup-2026-05-22.pdf.
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...
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...
I have written the bulk of the background chapter of my dissertation, these past few days spent writing the section titled “Mixed Evaluation Order.”
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...
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
This week my most critical obligation is to organise my writings into a more dissertation-like format than this blog.
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...
This week I proved univalence for the single-sorted duploid arising from a (fully equalizing) adjunction between univalent categories, however I struggled ...
This week I spent a little time looking at and proving some of the last few theorems from Guillaume’s thesis.
This week I had a stab at stating the univalence condition for duploids, and seeing what I can do with it.
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...
These past two weeks I developed some theory about unital magmoids, and (separately) returned to the adjunctions of a duploid’s shift functors.
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...
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...
Today I submitted my “phase 2” project proposal, for approval by the examiners. The text of the proposal is presented below.
I will be working with Jon Sterling on the denotational semantics of effectful languages with mixed evaluation-order (CBV/CBN).