Tom de Jong

@MartinEscardo and I have been working on injective #types in #constructive #univalent mathematics.

Last week I gave an informal talk in our group's seminar and I wrote a brief blog post with several pointers in case you'd like to know more: https://fplunchnott.wordpress.com/2024/10/25/injective-types/

Injective types

Tom de Jong (University of Nottingham) In this talk I presented some joint work with Martín Escardó on injective types in univalent mathematics. A type D is said to be injective when all maps f : X…

FP Lunch
Nov 8 at 10:23amWeb
Show threadToucanIanNov 8

@de_Jong_Tom @MartinEscardo

That’s awesome!

This encompasses an observation I formalized about apartness on a complete lattice implying WLEM.

Show threadTom de JongNov 8

@ToucanIan @MartinEscardo

Thanks! Indeed, it is also quite close to an argument for directed complete posets (not necessarily having a least element) that I gave in my paper "Apartness, sharp elements, and the Scott topology of domains" https://doi.org/10.1017/S0960129523000282

Apartness, sharp elements, and the Scott topology of domains | Mathematical Structures in Computer Science | Cambridge Core

Apartness, sharp elements, and the Scott topology of domains - Volume 33 Issue 7

Cambridge Core
Show threadToucanIanDec 31

@de_Jong_Tom @MartinEscardo

Just coming back to this… in your recent work are you relaxing that j be an embedding?

Show threadTom de JongDec 31
@ToucanIan @MartinEscardo No, we only consider injectivity w.r.t. embeddings.
Show threadMartin EscardoDec 31

@de_Jong_Tom @ToucanIan

And recently we considered injectivity wrt to *small* embeddings.

And, in the past, independently of type theory, and mostly in 1-topos logic on paper, I wrote several papers about injectivity wrt all sorts of embeddings that arise in several categories of interest, including topological spaces, domains, and locales.