crazy idea: "Type" → "Space", "term" → "point"

Stream: general

[Alex Kontorovich]

It just occurred to me: one of the pieces of friction when mathematicians start playing with formalization is that they have to change from their familiar "elements" in a "Set" to "terms" of a "Type". They get over it pretty quickly, but it's a papercut (and an important one to go through, e.g., Set X means functions X → Bool, so we don't want to confuse things by calling X itself a Set). But mathematicians already have vocabulary for "Type" and "term", they just call them "Space" and "point"! I came to this realization when I was considering in my lecture today to call a TopologicalSpace a TopologicalType (it's a Type, with a topology on it). But why not meet people where they are? We already use "Space" in exactly the same way as "Type" is used in type theory. VectorSpace (ok, Module) is a Type with the structure of a vector space. FunctionSpace is the Type of f : X → Y. MeasureSpace, MetricSpace. The dependent type Π(x : A), B(x) could be thought of as a "function space from space A to the B-family of spaces," and Σ(x : A), B(x) as a "bundle space over A with fibers B(x)." Even higher-order constructions like universes could be "spaces of spaces." Etc etc. Mathematicians can also easily understand the "Space of all proofs of proposition P" and a "point" in this space corresponding to a proof of P. How impossible would it be to start talking about abstract points x : X of a Space X and dropping the "term : Type" vocabulary? I'm sure this suggestion will get immediately shot down, but thought I'd just throw it out there.

[Yaël Dillies]

Isn't this, in fact, precisely the point of view that HoTT pushes you towards?

[Michael Rothgang]

Interesting! Here's my quick opinion. (I've used Lean a fair bit, but not yet taught a Lean course.)
Switching all talk about Lean to this vocabulary is probably not good (as it will, for example, confuse computer scientist or type theorists) --- but for a project more focused on teaching, this could be worthwhile.

[Alex Kontorovich]

I'm not trying to do anything to computer scientists or type theorists. I just have in mind that we mathematicians can tell each other: other people call "points" "terms" and "Spaces" "Types", so if you hear those funny words, that's what they mean. Maybe we can have an abbrev that Space is the same thing as Type? That would allow me to write:

class topologicalSpace (X : Space) where
  isOpen : Set X → Prop
  isOpen_univ : isOpen (Set.univ : Set X)
  finiteInter : ∀ s t : Set X, isOpen s → isOpen t → isOpen (s ∩ t)
  arbUnion : ∀ (ι : Set (Set X)), (∀ s ∈ ι, isOpen s) → isOpen (⋃ s ∈ ι, s)

(Ok, I have to be more careful about universes, but some version of that?) So X is some abstract Space, and I'll put on top of it the structure of a topology, so it makes sense to now call it a TopologicalSpace...

[Kenny Lau]

I think category theory might also be useful in explaining type theory. Afterall, in Category Theory, it is not a well-formed question to ask about equality, which translates to the fact that we also don't talk about equality of types.

[Shreyas Srinivas]

I have to second what Yael is saying, but extend it by pointing out that your intuition is guiding you towards models of type theory. Hoffman and Steicher’s groupoid interpretation might be your cup of tea as a mathematician.

[Chase Norman]

The example could be even more idiomatic if Set X was 𝒫 X for the powerset and if ∈ was an alias for :.

[Terence Tao]

I get the sense that Mathlib tends to avoid having multiple names for the same concept (this would complicate lemma search, for instance). But for downstream projects I think it would be fine.

Recently I formalized a ZFC-type set theory (with atoms) in Lean in https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_3_1.lean . With some judicious exports and variables, I can hide the usual laundry list of types and inferences one would ordinarily need in Lean, and pretend that I have some pre-existing types (or spaces, if you wish) Set and Object that obey all the axioms of ZFC (well, actually just ZF, as this section doesn't introduce choice yet). This allows for clean statements such as

theorem SetTheory.Set.compl_union {A B X:Set} (hAX: A ⊆ X) (hBX: B ⊆ X) : X \ (A ∪ B) = (X \ A) ∩ (X \ B)

Types then barely show up (except at one annoying remaining technicality, in that an element x:A of A:Set is not an Object but rather belongs to the subtype { x // x ∈ A} of Object corresponding to that Set). At the end of the Lean file I provide some API to convert things back to Mathlib's more type-theoretic A: Set X formalism.

Similarly, for other sections of my book, I have found it relatively easy to introduce custom notation that aligns quite well with the spirit of my original text, and only at the end of the formalization do I provide the API to convert it back to the Mathlib analogues of the same concepts. So one could do something similar here with files downstream from Mathlib that use your custom abbreviations such as Space.

[Kevin Buzzard]

Back in the lean 3 days I once gave a department colloquium where I started by saying "a type in lean is just another word for a collection of stuff, the same way that a set is" and I then defined Set to mean Type (can't do this in lean 4 because Set is taken) and then just wrote X : Set all the way through my demo rather than X : Type.

[Terence Tao]

In the lean file I shared above, I was able to use namespace, export, and variable to override the Mathlib Set X (which now becomes _root_.Set X) and introduce my own type Set to be whatever I wanted (in particular, automatically obeying the axioms I wanted, which in this case were Zermelo-Frankel set theory with atoms). (There is one line of code, variable [SetTheory], that introduces all these axioms "by fiat". But I never need to show that SetTheory is actually an inhabited type; Lean supports purely axiomatic reasoning just fine while hiding the type theory.)

[Kenny Lau]

@Terence Tao You might know this already, but Mathlib has a model of ZFC called ZFSet, and it might be a fun exercise for someone (maybe me) to show that Mathlib's ZFSet is an instance of your SetTheory. Not sure if I might run into universe issues though, I might only be able to prove it if I change your Type to Type 1 :melt:
https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_3_1.lean#L38-L39

  Set : Type -- Axiom 3.1
  Object : Type -- Axiom 3.1

[Kenny Lau]

It might as well be independent of Lean whether SetTheory is consistent, since it might be independent of Lean whether a universe exists in Type (there's no axiom saying that Type has to be the smallest universe)

[Terence Tao]

Nice question. My guess is that there will be some computability issues: my axioms permit replacement and substitution by arbitrary predicates, not just ones that are computable, or internally definable within the theory. This may introduce some subtle issues (hopefully not Russell paradox-level issues though).

[Kenny Lau]

Using Prop might indeed be problematic in a classical setting (with a very liberal use of the word "classical"), but I suspect it wouldn't be a problem here because ZFSet also uses arbitrary predicates:
PSet.powerset

/-- The pre-set powerset operator -/
def powerset (x : PSet) : PSet :=
  ⟨Set x.Type, fun p => ⟨{ a // p a }, fun y => x.Func y.1⟩⟩

A lot of things wouldn't be "computable", but it doesn't really matter in classical mathematics, at least in this context. We can't have computable models of ZFC in paper-mathematics either (assuming, well, ZFC is consistent).

[Edward van de Meent]

i'm trying this right now (because it's a good excuse to get aquainted with ZFSet and its quircs), and curiously, replace seems to be somewhat annoying... In particular, the closest thing in the ZFSet api is ZFSet.image which does not take functional relation, but instead an actual function... As a result, i think proving this version requires mathlib's choice axiom...

[Kenny Lau]

@Edward van de Meent did you have to change Type to Type 1?

[Edward van de Meent]

yes

[Kenny Lau]

Edward van de Meent said:

i'm trying this right now (because it's a good excuse to get aquainted with ZFSet and its quircs), and curiously, replace seems to be somewhat annoying... In particular, the closest thing in the ZFSet api is ZFSet.image which does not take functional relation, but instead an actual function... As a result, i think proving this version requires mathlib's choice axiom...

Yeah I wouldn't be surprised if you need choice everywhere

[Edward van de Meent]

yea, most of these probably already use choice, it was just unexpected that i'd have to use it explicitly instead of the API being in such a way you don't notice it.

[Kenny Lau]

I feel like if Tao's P: Subtype (mem . A) → Object → Prop had Object instead of Subtype (mem . A), it might not even be possible to prove

[Kenny Lau]

since the ZFC thing seems to need some Definable instance

[Kenny Lau]

never mind, I guess in that case we would still be able to restrict the predicate to A

[Edward van de Meent]

I feel like this Definable thing can likely be created via choice

[Kenny Lau]

yeah, probably

[Terence Tao]

Yeah, I found to my annoyance that even when I did not explicitly assume choice in ZF set theory, I needed to work with "unique choice" in which any predicate P x y that had a unique solution y for each given x could be assigned a choice function. This is much weaker than full choice, but I don't think it follows from constructive logic, so with Lean's standard axiom set I had no option other than to use choice. I guess one could introduce a custom unique_choice axiom but I don't know how interesting it would be to anyone else to do so.

[Kenny Lau]

You could write down the axiom as:

axiom uniqueChoice : (α : Type u) → Nonempty α → Subsingleton α → α

But yeah, I don't know if people would be interested in this, especially when choice is already so integrated with everything we do

[Kevin Buzzard]

Occasionally we get set theorists here who are well aware what AC is and are surprised that it's needed in lean to prove unique choice, which apparently is a theorem in ZFCZF (I'm not an expert but this is my understanding; it's definitely not provable constructively in Lean's type theory though because AC in lean can be thought of as "breaking out of Prop into Type" which this is doing)

[Kenny Lau]

yeah, ZFC doesn't really have the concept of "data", so every theorem is just Lean's Prop, so to prove unique choice you just write down the set

as an analogy, to show that's it's more "constructive", the "algorithm" is to just take the intersection of the whole set, that will give you the unique element that is in a given set

[Kenny Lau]

(which is equivalent to taking the union of the whole set!)

[Edward van de Meent]

constructing an equivalence between ZFSet.omega and Nat is surprisingly annoying

[Edward van de Meent]

i would have expected more API

[Edward van de Meent]

i suspect the map ZFSet.omega -> Nat will require choice?

[Kevin Buzzard]

I've not used set theory at all in Lean but isn't this just some straightforward recursion to define the map (from Nat to omega) and induction to prove it's injective and surjective?

[Terence Tao]

Can you use Nat.rec or just inductive matching
to build a map from Nat to ZFSet.omega and then later figure out how to prove that it is injective and surjective?

[Edward van de Meent]

silly me, i thought i'd need to define cardinality of ZFSets first :upside_down:

[Yaël Dillies]

Kevin Buzzard said:

Occasionally we get set theorists here who are well aware what AC is and are surprised that it's needed in lean to prove unique choice, which apparently is a theorem in ZFC

"a theorem in ZF" is what you meant, I assume

[Arthur Paulino]

[I'm not a mathematician]
My mental model is that we're using a digital system with types that are expressive enough to encode mathematical concepts. I actually like the grounded terminology of terms and types because that's what is actually happening in the system. A different terminology would make me more confused as a learner (as it did in my early Lean days).

[suhr]

By the way, is it possible to restrict choice in such a way, so non-constructive content is encapsulated in Prop (you can state the existence but can't get a standalone value in Type)? So you have calculus of propositions and calculus of problems in the spirit of https://arxiv.org/pdf/2307.09202.

[Kevin Buzzard]

The issue with mathematicians is that they have typically literally never even heard of type theory, and whilst many of them have not done a formal course in set theory they are told on day 1 that a set is "a collection of stuff, like the naturals or reals or $\{37,x,\mathrm{bus\ stop}\}$" (and given no further information) and then later on that "a group is a set equipped with...", "a manifold is a set equipped with...", "a metric space is a set equipped with...", "a perfectoid space is a set equipped with...". So the language is ubiquitous even though many mathematicians never see a formal exposition of any foundational system.

[Kenny Lau]

Edward van de Meent said:

constructing an equivalence between ZFSet.omega and Nat is surprisingly annoying

Everything is defined explicitly using PSet, so I would just do explicit functions using those

[Kevin Buzzard]

Edward van de Meent said:

i suspect the map ZFSet.omega -> Nat will require choice?

The way Terry and I suggested to do it, yes (because you'll need the inverse of a bijection, which needs unique choice). I've not looked at the definition but the big question is whether the recursor needs AC. Because Nat is defined as an inductive type, you get its recursor for free in a computable way. But my guess is that omega will be defined in a far more obscure way so the question will be whether its eliminator can be made constructive.

[Kevin Buzzard]

docs#ZFSet.omega

[Kevin Buzzard]

Oh this looks like it might have a constructive recursor -- it's just Nat in disguise? Hmm it's Nat wrapped in a Quotient.mk and a ULift so the question is whether these are sufficiently constructive. It wouldn't surprise me...

[Kenny Lau]

According to me, a constructive map should be possible.

[Aaron Liu]

Kevin Buzzard said:

Oh this looks like it might have a constructive recursor -- it's just Nat in disguise? Hmm it's Nat wrapped in a Quotient.mk and a ULift so the question is whether these are sufficiently constructive. It wouldn't surprise me...

At a glance, this will need choice because you don't get enough out of "equivalent to something in the image of PSet.ofNat" to be able to invert the map. You would need something like an explicit equivalence.

[Kenny Lau]

But I don't need to invert any map, I'm defining both functions in both directions

[Aaron Liu]

I think it's not computable, since if it were you could decide any proposition (assuming this is what you meant):

import Mathlib

instance : IsEmpty PSet.empty.Type := ⟨PEmpty.elim⟩

example (f : { x : ZFSet // x ∈ ZFSet.omega } → Nat)
    (hf : Function.LeftInverse f
      fun x => ⟨ZFSet.mk (PSet.ofNat x), .up x, .rfl⟩) :
    ∀ P : Prop, Decidable P := fun P =>
  let s : PSet := .mk (ULift (PLift P)) fun _ => .empty
  have h0 (hnP : ¬P) : s.Equiv .empty :=
    have : IsEmpty s.Type := ⟨fun hP => absurd hP.down.down hnP⟩
    PSet.equiv_of_isEmpty _ .empty
  have h1 (hP : P) : s.Equiv (insert .empty .empty) := ⟨
    fun _ => ⟨none, .rfl⟩,
    fun x => x.rec ⟨.up (.up hP), .rfl⟩ PEmpty.rec⟩
  have h : s ∈ PSet.omega := Classical.byCases
    (fun hP => ⟨.up 1, h1 hP⟩)
    (fun hnP => ⟨.up 0, h0 hnP⟩)
  have h₀ (hnP : ¬P) : f ⟨ZFSet.mk s, h⟩ = 0 :=
    (congrArg f (Subtype.ext (ZFSet.sound (h0 hnP)))).trans (hf 0)
  have h₁ (hP : P) : f ⟨ZFSet.mk s, h⟩ = 1 :=
    (congrArg f (Subtype.ext (ZFSet.sound (h1 hP)))).trans (hf 1)
  decidable_of_iff (f ⟨ZFSet.mk s, h⟩ = 1) (Classical.byCases
    (fun hP => ⟨fun _ => hP, fun _ => h₁ hP⟩)
    (fun hnP =>
      ⟨fun h => absurd ((h₀ hnP).symm.trans h) Nat.zero_ne_one,
        fun hP => absurd hP hnP⟩))

[Kenny Lau]

@Aaron Liu hmm, it does seem to be not as simple as I thought. It might also depend on the definition of "function". I was hoping that I could just define a PSet explicitly and then interpret it as a function.

It also seems like this latter approach might still work if we change the definition of function to use ZFSet.funs.

(But then of course this would have nothing to do with the axioms stated by Tao)

[Jz Pan]

Kevin Buzzard said:

yes (because you'll need the inverse of a bijection, which needs unique choice)

You can also define the inverse map using Nat.find (but it requires DecidableEq).

[Mario Carneiro]

These details BTW are exactly why Definable exists; they give some conditions under which you can construct such a function without choice. In practice it didn't really work out, and there is a classical instance making everything Definable

[Edward van de Meent]

indeed, docs#Classical.allZFSetDefinable

[Alex J. Best]

Personally I try and teach and use the pair (element, Type) as it is consistent with the type theory literature, but one less new word for people to learn

[James E Hanson]

Alex Kontorovich said:

We already use "Space" in exactly the same way as "Type" is used in type theory.

I don't think this is actually true, or at the very least depends heavily on what part of math someone is from. The use of the word space in math is almost always either historical/idiomatic (as in 'vector space') or somehow related to some topological notion.

If you start telling a typical mathematician about a group $G$ and then casually mention the 'underlying space of $G$', they will assume that the group in question is a topological group or at least something very similar, rather than an abstract group. Imagine trying to clarify this: 'no, the elements of $G$ don't live in a topological space, they just live in a space'. This just isn't how mathematicians talk.

The identification of types with spaces in HoTT is also pretty narrow relative to the general sense of the word 'space' in mathematics.

[James E Hanson]

Terence Tao said:

This is much weaker than full choice, but I don't think it follows from constructive logic,

To some extent this depends on which 'brand' of constructive mathematics you're talking about. Unique choice is provable in the context of topos theory and constructive set theory. As far as I know it really wasn't until the advent of modern type theory that people starting thinking about systems that don't prove unique choice. Also, for what it's worth, I believe that there are systems with classical logic in which it isn't provable, so it is in some sense orthogonal to constructivity.

[Max New]

Unique choice and function extensionality are both provable in cubical type theory as well, which is another flavor of constructive type theory. This is the main reason in my opinion that cubical type theory despite all of the higher homotopy stuff turns out to be the most "normal" constructive type theory that has a usable implementation currently (cubical Agda).

[Max New]

but there the definition of Prop is different: a Prop is a Type all of whose elements are equal

[Shreyas Srinivas]

Max New said:

but there the definition of Prop is different: a Prop is a Type all of whose elements are equal

I am confused by this statement. How is that different from this:

example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl

[Jireh Loreaux]

Max New said:

all of whose elements are equal

provably or judgementally?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Provably, afaik. That is the difference to Lean

[Max New]

Shreyas Srinivas said:

Max New said:

but there the definition of Prop is different: a Prop is a Type all of whose elements are equal

I am confused by this statement. How is that different from this:

example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl

In lean, all Props satisfy this definition, but in cubical type theory you define a new type hProp to be a pair of a P : Type and a proof that forall p1 p2 : P. p1 = p2. But you don't get definitional proof irrelevance which is a big difference from Lean

[Max New]

On mastodon I've been pointed to these slides from an expert on this stuff that suggests they think this is the major sticking point, the principle of unique choice and definitional proof irrelevance seem irreconcilable constructively: https://pujet.fr/pdf/uniquechoice_slides.pdf