Categories
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.
More …
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.
Overview
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 |
More …
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 …
This was originally posted on cohost.
More …
…probably. To be clear, ECIC refers to Monnier and Bos’
Erasable CIC, with erasable in the sense of erasable pure type systems (EPTS).
I’ll argue that even with erased impredicative fields,
Coquand’s paradox of trees is still typeable.
More …
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.
I’m personally not looking for “experimental” colour films or films that aren’t “true colour”,
so I’ve excluded a number of those here, which are mostly:
- LomoChrome from Lomography
- RETOCOLOR from RETO Project
- Zombie 400 from Mr. Negative × FilmNeverDie
- various from KONO!
- various from Film Photography Project
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.
More …
I’ve wanted to write an informal (but technical!) post about my current research in progress on Stratified Type Theory (StraTT), but we’ve been occupied with writing up a paper draft for submission to CPP 2024, then writing a talk for NJPLS Nov 2023, then being rejected from CPP, then I’ve just been randomly distracted for two weeks but I’m so back now.
That paper draft along with the supplementary material will have all the details, but I’ve decided that what I want to focus on in this post is all the other variations on the system we’ve tried that are either inconsistent or less expressive. This means I won’t cover a lot of motivation or examples (still a work in progress), or mention any metatheory unless where relevant; those can be found in the paper. Admittedly, these are mostly notes for myself, and I go at a pace that sort of assumes enough familiarity with the system to be able to verify well-typedness mentally, but this might be interesting to someone else too.
More …
Overview
Work |
Summary |
Nakano |
STLC + recursive types + guarded types |
Birkdeal, Møgelberg, Schwinghammer, Stovring |
dependent types + recursive types + guarded types |
Atkey and McBride |
STLC + recursive types + guarded types + clocks |
Birkedal and Møgelberg |
dependent types + guarded types |
Møgelberg |
dependent types + guarded types + clocks |
GDTT |
dependent types + guarded types + clocks + delayed substitution |
CloTT |
dependent types + guarded types + ticks + clocks |
GCTT |
cubical type theory + guarded types + delayed substitution |
TCTT |
cubical type theory + guarded types + ticks |
CCTT |
cubical type theory + guarded types + ticks + clocks |
More …
This was originally a two-part post on cohost.
Recently I needed to convert a large TIFF scan of a duochrome page into something reasonable,
i.e. a web-supported image format that was still lossless
since it seemed a shame to ruin such a nice high-definition scan with lossy compression.
In terms of lossless formats, all browsers support
PNG, WEBP, and AVIF, while I really hope JXL support is imminent.
I therefore wanted to see which file format would perform the best in terms of file size
by converting my ~183 MiB TIFF to each of them using ImageMagick.
For PNG, WEBP, and JXL, there’s an effort setting:
lower effort means faster compression but larger size,
while higher effort means slower compression but smaller size.
I used the highest three settings for these, yielding sizes from ~50 MiB to ~20 MiB.
(As a treat, I’ve also converted to JPG, WEBP, AVIF, and JXL at -quality 0
, i.e. lossy with the worst settings.)
More …
This was originally posted on cohost.
On the Market–Frankford trains of SEPTA in Philadelphia,
the designation signs indicating the line and the next stop
are very simple 18-panel 3×5-segment displays.
More …