Bob Atkey @bentnib@types.pl

I often find at work I wish I could say: Just let me write a SELECT query against your backend databases. I can make this problem go away and save several FTEs work faffing around manually with spreadsheets... #Databases #SingleSourceOfTruth #AcademicIT

Went to a rally, got a T-shirt.

Thanks for the design @tomflood

this video is making a lot of things about how conversation work click into place for me for the first time

also, why responding to long emails is hard

https://www.youtube.com/watch?v=LFilYalaF9g

🧵 Thread: Genuine quotes from experts and eyewitnesses on Arthur C. Clarke's Mysterious World (1980), a British television series which looked at unexplained phenomena from around the world.

#supernatural #paranormal #occult #psychic #UFOs #ghosts #yeti #cryptozoology
(originally posted on the bird site)

Our paper on the cumulative hierarchy and ordinals in HoTT got accepted at LICS! 🎉
https://arxiv.org/abs/2301.10696

I'm overjoyed to announce that I will be starting as an Associate Professor in Logical Foundations and Formal Methods at University of Cambridge this fall!

I handed in my thesis!

people.compute.dtu.dk/ahfrom/ahfrom-thesis.pdf

In tribute to Lawvere, here is one of his ideas that is simple enough to explain in one post.
The original paper is "Diagonal arguments and cartesian closed categories" (http://tac.mta.ca/tac/reprints/articles/15/tr15abs.html)

Lawvere's fixed point theorem is the positive constructive content of many diagonalization arguments.
Here I'll show how it unifies Cantor's theorem that there's no surjection from a set to its powerset and the construction of the Y combinator.

Lawvere's fixed point theorem in type theory:
If r : X -> (X -> D) is surjective (forall f: X -> D. exists x. r x = f), then for every function h : D -> D there exists d : D. a fixed point of h , i.e., h d = d.

Proof:
Given h : D -> D, by surjectivity there exists l:X such that r l = λ x. h(r x x).
Then r l l is a fixed point of h:
r l l = (λ x. h(r x x)) l = h (r l l)

Corollary: Cantor's theorem. There is no surjection X -> (X -> Prop).
Proof:
If there were, then every h : Prop -> Prop would have a fixed point, but not : Prop -> Prop does not have a fixed point (exercise).

If we strengthen the hypothesis we can get something which makes sense purely in the equational theory of the lambda calculus (i.e., no existential quantifiers) and therefore interpretable in all Cartesian Closed Categories.

Variant of Lawvere's fixed point theorem in STLC:
if r : X -> (X -> D) is a retract of s : (X -> D) -> X (i.e., (λ x. r(s(x))) = (λ x. x)), then we can construct a fixed point combinator Y : (D -> D) -> D, i.e., Y = λ h. h(Y h).

Note that in the presence of the axiom of choice, this variant is equivalent to the previous, but the most interesting applications are in settings without choice.

Proof:
Y = λ h. r (s (λ x. h(r x x))) (s (λ x. h(r x x)))
Here s (λ x. h(r x x)) is the l in the previous proof, where our strengthened hypothesis gives us a choice of element rather than its mere existence.
Then
Y
= λ h. Y h
= λ h. r (s (λ x. h(r x x))) (s (λ x. h(r x x)))
= λ h. (λ x. h(r x x)) (s (λ x. h(r x x)))
= λ h. h(r (s (λ x. h(r x x))) (s (λ x. h(r x x)))))
= λ h. h(Y h)

Which is the Y combinator in STLC, which more typically is constructed using a recursive type X =~ (X -> D) with r, s the isomorphism, or in untyped lambda calculus which is equivalent to having a single type D where if only β is assumed then D is a retract of (D -> D) and with η then D is isomorphic to (D -> D).

Related expository material:
- https://arxiv.org/abs/math/0305282
- https://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/
- https://www.cs.bham.ac.uk/~mhe/agda-new/LawvereFPT.html

The notion of model of intuitionistic propositional logic (IPL) I'm
most familiar with (being a category theory/PL nerd) is a Heyting
algebra (HA): a poset with finite meets, finite joins and a Heyting
implication. If you add propositional variables, the model includes a
choice of how to interpret them as elements of the HA and if you
include axioms, their interpretation must be true in the HA.

Then you can interpret every proposition of IPL as an element of the
HA where you interpret conjunctions as meets, disjunctions as joins
and implication as the Heyting implication. If G |- A is provable then
/\ [G] |- [A] is true.

If you look up what a model of IPL is though, you'll likely find
Kripke models, and they look at first a bit different: It's a pair of
a poset W, and a "forcing relation" ||- between elements of W and
propositions of IPL satisfying a bunch of properties:

1. for variables x, if w ||- x and v <= w then v ||- x
2. w ||- p /\ q iff w ||- p and w ||- q
3. w ||- true is true
4. w ||- p \/ q iff w ||- p or w ||- q
5. w ||- false is false
6. w ||- p => q iff for any v <= w if v ||- p then v ||- q

Despite the cosmetic difference, Kripke models are instances of the HA
model construction. Given a poset W, the HA in question is
Prop^(W^op), the poset of antitone functions from W to Prop
(classically, Prop is just the boolean order 0 <= 1). This has the
pointwise ordering: f <= g if for every w. f w implies g w.

This is a Heyting Algebra:

top w iff true
(f /\ g) w iff f w and g w
bot w iff false
(f \/ g) w iff f w or g w
(f => g) w iff for any v <= w. if f w then g w

Then an interpretation of the propositional variables in this HA would
be an assignment for each variable X and w a proposition [x] w that is
antitone in w: if [x] w and v <= w then [x] v. Then the model HA
interpretation defines exactly our Kripke forcing semantics. It
defines for each proposition of IPL p a function from W to Prop that
is antitone, i.e., [p] : W^op -> Prop. Then the definition of Kripke
model is just an infix notation for this semantics:

w ||- p := [p] w

And if you unravel the definitions of the HA semantics and the HA
structure of the poset, you reproduce exactly the definition of a
Kripke model.

Bonus: this is all a "de-categorification" of a similar situation for
lambda calculus. The Kripke models are presheaf categories and the HA
are bi-cartesian closed categories.