Andy Pitts on Intensional Setoids

From the description:

Roughly speaking, Martin-Löf's dependent type theory comes in two flavours, intensional and extensional. Compared with the second flavour, the first one lacks logical principles such as function extensionality that are taken for granted in mathematics; but it has very good computational properties and (therefore) underlies the various theorem-proving systems implementing dependent type theory. Since Martin Hofmann's PhD work in the late 1990s, we have known that some type-theoretic version of the notion of "setoid" (= set equipped with an equivalence relation) can be used to regain some version of extensional type theory in some version of intensional type theory; but to be more precise, one has to explain the three "some"s in that sentence. I have long avoided thinking about setoids, because the topic is said to be hellish; but one can grow to love most things if one tries! In this talk I will tell you some things I have learned (peering over the shoulders of Hofmann, Altenkirch and Palmgren) about setoids and families of setoids in the simplest form of intensional type theory with universes; and will sketch precisely how they can be used to give a semantics of extensional type theory.

Intensional setoids sound like the kind of condition you could expect to get after passing a three-legged stool. See https://amp12.github.io/IntensionalSetoids/

52:36 This was Andy Pitts' homework, I think: See this talk from six years ago: Maria Emilia Maietti - Quotient completions for topos-like structures

See the paper Elementary quotient completion Maria Emilia Maietti and Giuseppe Rosolini.

She is a colleague of Giovanni Sambin at Padua:




See About Logic interview with Giovanni Sambin.

Subscribe to Topos Institute.

Comments

Post a Comment

Popular posts from this blog

John Searle's Chinese Room Argument

Image
He's fed up with talking about this. I used to have a copy of the little book he wrote called Minds, Brains & Science. Apparently the AI at Google has read it too and gets it completely: How does stuff like this happen? Most people won't even notice what I'm saying even if I point out that the Google search changed the title. The book was really called Minds, Brains & Science , not Minds, Brains & Programs . (But maybe that was a later edition or something?) I asked Google and it said: John Searle's book Minds, Brains and Science did not become "Minds, Brains & Programs"—rather, they are two separate, distinct works published a few years apart: "Minds, Brains, and Programs" (1980): A landmark academic paper published in the journal Behavioral and Brain Sciences. This is where Searle first introduced his famous Chinese Room Argument to challenge the concept of "strong AI". "Minds, Brains and Science" (1984): A shor...
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more

FUTO FUBS

Image
I think this is the first time they've actually publicly announced anything about this project. See these posts: Eron Woolf on Why Open Source is Failing Matt Mikhailov and Vincent McKibbon on The Problem with Open Hardware Jason Kridner talking About BeagleBoard.org and Software Development .  See these places:  https://danielc.dev/rk/ https://github.com/petabyt/rk https://github.com/futo-org/ret See also  https://pine64.org/devices/pinebook_pro/ . Subscribe to  FUTO .  See  https://github.com/nir9/low-level-learning-resources/tree/master/setups/debian . Subscribe to  Nir Lichtman .  If you're looking for a cool init process, try  https://ctx.graphics/terminal/ . See  Artful Bytes - When to Use a RTOS  and  How to Create a Successful Open Source Project . 
Read more