Greetings, human!

See selected notes below or visit the notes archive. You can find my PGP public key here, and my email is `dan @ this-domain`

.

- A short note on the Frobenius property of a weak factorisation system and its relation to Π-types
- Universes in the groupoid model of type theory
- Category theory in Coq with setoids
- Uniquness of the absurdity proofs
- Jaap van Oosten’s lecture notes on category theory (from the 2016 course)

- Leisure activities
- Modal logic(s)
- Anne Troelstra on Albert Dragalin’s legacy
- Lecture notes on intuitionistic logic by Nick Bezhanishvili and Dick de Jongh

- Petri nets // more Petri nets
- Notes on presheaf approach to concurrency