CS PhD student @ UPenn [he / they]
There are a lot of nice monospaced code-writing fonts that I don’t use. For some of them, there are tiny, specific nitpicks about why I don’t use them. My use case is writing code with a lot of Unicode, like in Lean or Agda, writing Markdown with a lot of Unicode because I can, and having a terminal that looks nice. For reference, I’ll be comparing a snippet of a proof state I have open at the moment, and my default font of choice is currently Fira Code.
More …I’ve now been running my personal server, Thulium, for seven years and four-and-a-half months, and three of those years have elapsed since my previous post. Not much had changed in those intervening years until very recently, so I thought I’d map them out here.
More …This was originally an updating post on types.pl.
Since moving to Philadelphia in 2022, a number of beloved restaurants I’ve discovered have since closed in my mere years here, so I’m keeping this table as a remembrance of restaurants past.
More …This is a table similar to Wikipedia’s zhuyin table, but with slightly different sorting and an example for each possible combination of initials and finals.
More …If you look around for why inductive datatypes need to be strictly positive, you’ll probably end up at Vilhelm Sjöberg’s blog post Why must inductive types be strictly positive?, which gets passed around a lot as an accessible and modernized description of the inconsistency that arises from a certain large, impredicative inductive datatype that is positive but not strictly positive. This example originally comes from Coquand and Paulin-Mohring’s COLOG-88 paper Inductively defined types. A key component of the inconsistency relies on the injectivity of its constructor, but since the inductive is large, even if Rocq were to permit nonstrictly positive inductives, it would still disallow its strong elimination and therefore injectivity!
More …
Part 1: U+237C ⍼ RIGHT ANGLE WITH DOWNWARDS ZIGZAG ARROW
Part 2: update: U+237C ⍼ angzarr;
Part 3: Monotype Mathematical Sorts
This is part 4.
Many thanks to Sallie Morris at the Science Museum Group, Claire Welford-Elkin at St Bride Library, and Brian Corrigan for their help.
This update was originally posted on cohost.
Models of predicative type theory are well-studied and have been mechanized, ranging from proofs of consistency for a minimal type theory with a predicative hierarchy in 1000 lines of Rocq to proofs all the way up to decidability of conversion in 10 000 lines of Agda.
In contrast, the story for impredicative type theory is not so clear. Incorporating different features alongside an impredicative Prop may require substantially different proof methods. This post catalogues these various models, what type theories they model, and what proof technique is used. Most proofs fall into one of three techniques: proof-irrelevant set-theoretic models, reducibility methods, and realizabililty semantics.
| Work | Theory | Proof method | Universes | Inductives | Equality |
|---|---|---|---|---|---|
| Coquand (1985) | CC | ? | Prop, Type | none | untyped |
| Pottinger (1987) | CC | ? | Prop, Type | none | untyped |
| Ehrhard (1988) | CC | ω-Set | Prop, Type | none | none |
| Coquand and Gallier (1990) | CC | reducibility | Prop, Type | none | untyped |
| Luo (1990) | ECC | reducibility; ω-Set | Prop ⊆ Type{i} | dependent pairs | untyped |
| Terlouw (1993) | CC | reducibility | Prop, Type | none | untyped |
| Altenkirch (1993) | CC | Λ-Set | Prop, (Type) | impredicative | typed |
| Goguen (1994) | UTT | set-theoretic | Prop, Type | predicative | typed |
| Geuvers (1995) | CC | reducibility | Prop, Type | none | untyped |
| Melliès and Werner (1998) | PTS | Λ-Set | Prop ⊈ Type{i} | none | untyped |
| Miquel (2001) | CCω | set-theoretic; ω-Set | Prop ⊆ Type{i} | none | untyped |
| Miquel (2001) | ICC | ? | Prop ⊆ Type{i} | none | untyped |
| Miquel and Werner (2003) | CC | set-theoretic | Prop, Type | none | untyped |
| Lee and Werner (2011) | pCIC | set-theoretic | Prop ⊆ Type{i} | predicative | typed |
| Sacchini (2011) | CIC^- | Λ-Set | Prop, Type{i} | predicative, sized | untyped |
| Barras (2012) | CCω | set-theoretic | Prop ⊆ Type{i} | naturals | untyped |
| Barras (2012) | CC | Λ-Set | Prop, Type | naturals | untyped |
| Timany and Sozeau (2018) | pCuIC | set-theoretic | Prop ⊆ Type{i} | predicative | typed |
Get your beans here! This is a list of specialty coffee roasters local to Philly that do single-origin light roasts whose coffeeshops are in or close to Centre City. This list is tailored to my preferences: I make coffee with an Aeropress at home, and I enjoy getting pourover coffee when I’m out.
More ……probably. To be clear, ECIC1 refers to Monnier and Bos’ Erasable CIC2, with erasable in the sense of erasable pure type systems (EPTS)3. I’ll argue that even with erased impredicative fields, Coquand’s paradox of trees4 is still typeable.
Not to be confused with their eCIC, the erasable CIC. ↩
Stefan Monnier; Nathaniel Bos. Is Impredicativity Implicitly Implicit? TYPES 2019. doi:10.4230/LIPIcs.TYPES.2019.9. ↩
Nathan Mishra-Linger; Tim Sheard. Erasure and polymorphism in pure type systems. FOSSACS 2008. doi:10.5555/1792803.1792828. ↩
Thierry Coquand. The paradox of trees in type theory. BIT 32 (1992). doi:10.1007/BF01995104. ↩
This was originally posted on cohost.
While looking up the various colour films my local photo shops carry, I found that a lot of them are actually respools and repackagings of other film (most Kodak), so I’ve tried to compile that information here to keep track of them all.
More …
Part 1: U+237C ⍼ RIGHT ANGLE WITH DOWNWARDS ZIGZAG ARROW
Part 2: update: U+237C ⍼ angzarr;
This is part 3.
Part 4: U+237C ⍼ is (also) S9576 ⍼
Many thanks to Alicia Chilcott and Sophie Hawkey-Edwards at St Bride for their help.
