ETCS

Stream: new members

[David Michael Roberts]

I might have a crack at showing that sets form a category that is a model of ETCS https://ncatlab.org/nlab/show/ETCS

[David Michael Roberts]

Or at least build a model of ETCS in Lean. Not sure quite what the sets of Lean are yet.

[David Michael Roberts]

I mean, I notice that in set_theory.zfc presets are used, but I can't tell if these are the same as Bishop-style presets (https://ncatlab.org/nlab/show/preset) and then sets are what are sometimes called setoids (https://ncatlab.org/nlab/show/equivalence+relation#setoids)

[Simon Hudon]

There are multiple formalizations of sets in Lean, depending on your needs. set_theory.zfc is if you're interested in (untyped) ZFC set theory, data.set formalize sets whose elements have a certain type as predicates on that type and data.finset formalizes finite sets whose elements also have a given type.

[Simon Hudon]

In set_theory.zfc there is pSet but there's also Set which might be more useful

[Mario Carneiro]

I think that pSet is indeed a preset in the nLab sense

[David Michael Roberts]

Yes, I could show that ZFC-sets give a model of ETCS, but it would be more interesting to show that one could build the category of "sets" directly, without knowing a well-founded \in-tree structure on them.

[Mario Carneiro]

although of course there is an equality relation on pSet, since it is a type; this equality is too fine for ZFC and Set is a quotient of this by set extensionality

[David Michael Roberts]

So I guess: is there a way to talk about sets native to Lean, as there is in HoTT, for instance? (where there is the type of hSets)

[Mario Carneiro]

hSet = Type in lean

[David Michael Roberts]

Oh, cool!

[Mario Carneiro]

all types are "sets" in the HoTT sense, because of proof irrelevance

[David Michael Roberts]

So, in principle, one could try to show that Type is (the objects of) a category—perhaps this is done already—and then show it is a term of type ETCS, once that is defined.

[Mario Carneiro]

yes, that should not be difficult

[Simon Hudon]

There is a category of types in category_theory.types

[Scott Morrison]

The category structure on Type is at https://github.com/leanprover/mathlib/blob/master/category_theory/types.lean

[Mario Carneiro]

also ^ that

[Simon Hudon]

@Scott Morrison not fast enough!

[Scott Morrison]

:-)

[Scott Morrison]

I was running a longer race. :-)

[Simon Hudon]

Now you understand why some of my code snippets have small type errors in them :P

[David Michael Roberts]

OK, cool, thanks :-)

[Mario Carneiro]

What's more, I think there is a model of ETCS in Type

[Mario Carneiro]

i.e. a suitably large inductive type can give you all the types you need to interpret the operations of ETCS

[David Michael Roberts]

As an aside: is there a handy chart that details the various unicode autocompletion shortcuts? and/or LaTeX : autocompl shortcut table?

[Mario Carneiro]

If you want the full list you should look at the vscode extension file

[Mario Carneiro]

but it is quite large and likely auto-populated with a bunch of things from LaTeX

[Bryan Gin-ge Chen]

You can also paste in symbols from this page and hover over them to see what the completion is.

[David Michael Roberts]

Which lives...? (thanks, btw)

[David Michael Roberts]

@Bryan Gin-ge Chen cool, thanks

[Mario Carneiro]

https://github.com/leanprover/vscode-lean/blob/master/translations.json

[Bryan Gin-ge Chen]

Here's the vscode file

[David Michael Roberts]

:+1:

[Mario Carneiro]

The maintainer of the extension (Gabriel Ebner) is quite receptive to adding new symbols if you spot one in high unicode that you like

[Jesse Michael Han]

@David Michael Roberts Nice seeing you here!

Type is indeed a model of ETCS; function extensionality should correspond to well-pointedness, working in classical, we have choice, Prop is the subobject classifier, and the NNO is nat.

[David Michael Roberts]

Sure, but is it _proved_ to be a model of ETCS? And, if I use the constructive fragment, do I get a model of the constructive version (a la I guess Mike Shulman's "material and structural set theories" paper)

[David Michael Roberts]

Oh, and thanks, @Jesse Michael Han :-)

[David Michael Roberts]

Also, one could go the whole hog and show without using even Prop that Type is some kind of predicative topos...

[David Michael Roberts]

That said, this is just to get me wet behind the ears and play around with stuff that I care about.

[Mario Carneiro]

Do you know what that should mean?

[David Michael Roberts]

There is a constructive version of well-pointedness, that doesn't force Booleanness. just that "a global element of the subobject classifier is false if and only if it is not true." (from https://ncatlab.org/nlab/show/well-pointed+topos)

[David Michael Roberts]

And as far as predicative stuff, one could show directly that Type is a Pi-W-pretopos satisfying some version of WISC (??? not sure about that one), following eg Benno van den Berg

[David Michael Roberts]

For instance "the category of Bishop sets in Martin-Löf type theory is a predicative topos" (https://ncatlab.org/nlab/show/predicative+topos)

[Mario Carneiro]

I'm not sure about WISC, seems like any version of the axiom of choice is likely to be false without choice, but I checked the proof that epis are surjective in lean:

universe u
theorem epi {α β : Type u} (f : α → β)
  (H : ∀ (γ : Type u) (g h : β → γ), g ∘ f = h ∘ f → g = h) (y : β) : ∃ x, f x = y :=
let g (y : β) : ulift.{u} Prop := ⟨∃ x, f x = y⟩,
    h (y : β) : ulift.{u} Prop := ⟨true⟩ in
have g = h, from H _ g h (funext $ λ x,
  congr_arg ulift.up $ eq_true_intro $ by exact ⟨_, rfl⟩),
by injection congr_fun this y; exact cast eq_true h_1

and it looks like you need Prop and propext essentially (you can't prove it using trunc, and you certainly can't prove it "constructively" i.e. with a sigma)

[Mario Carneiro]

Actually I find this to be an interesting example of a "nonconstructive" constructive exists, in the sense that you can't upgrade the exists to a data type even though the proof does not use choice.

[Mario Carneiro]

I am almost certain that WISC is not provable, although I don't think there is an easy proof of this. I don't think Asaf Karagila's proof https://arxiv.org/pdf/1212.4396.pdf is much affected by the presence of inaccessible cardinals, so it should be independent of lean as well by simulation in ZFC + omega inaccessibles (below the first inaccessible because we are working in Type).

[David Michael Roberts]

Well, I did prove (on paper) that WISC isn't provable from the axioms of an elementary topos, by constructing a topos where it fails :-)

[Mario Carneiro]

I suppose that's also an option... I guess lean has a bit more structure though, so maybe you have to do that with pi-W-toposes? Is that a thing?

[Jesse Michael Han]

@David Michael Roberts I'm not sure if

a global element of the subobject classifier is false if and only if it is not true

holds without invoking classical. Without being able to take a filterquotient of Prop, it's just a massive Heyting algebra, and even with excluded middle, if Lean knows that $\vdash p \vee \neg p$, it does not necessarily decide if $p$ is true or false.

Lean is also not quite a topos over $\mathbf{Set}$, for it lacks externally indexed colimits (while $\Sigma$-types and quotient types give all internally indexed colimits).

[Mario Carneiro]

@Jesse Michael Han Could you unpack what that statement about the subobject classifier should mean? I assume Prop is a subobject classifier for Type even without choice (but assuming propext), because every monomorphism in Type is an injection, and so it factors through the subtype on the range.

Actually, I see another problem: If f : A -> X is a monomorphism and g : X -> Prop is the function g x = \ex a, f x = a, then we want a pullback square with the true : unit -> Prop function. But the subtype is a pullback, and A is not constructively isomorphic to the subtype, so I don't think it holds. That is, Prop isn't even a subobject classifier.

[Jesse Michael Han]

That's interesting. (I assume you mean g x = \ex a, f a = x.) Why is the image of an injection not constructively isomorphic to its domain?

[Mario Carneiro]

There are a few ways to look at it. My favorite is to think in terms of what is "data" vs "erased" stuff, which corresponds to stuff that the computer could actually execute or manipulate. If you have a function f : A -> X where A and X are both data types, then f is a real function, something that transforms one kind of representation into another. There is no guarantee that this transformation is invertible, and in particular assuming that f is injective does not supply you with such an inverse. (This is why equiv contains an explicit inverse function, and bijection is a weaker notion.) So defining a function from A to {x // x \in range f} is easy by restricting the codomain of f, but you don't have enough data for the converse function.

In set theory you would use the exists assumption to give the value, but since this is a Prop, it is "not data" and can't be turned into data. If you use a Type-valued equivalent, like trunc {a // f a = x}, then it would be constructively bijective, but in this case I'm not sure it's a pullback.

[Jesse Michael Han]

If that's the case, when maybe one does need 'classical' to show that Prop (which is then bool) is a subobject classifier after all.

Could you explain why couldn't we do something like, take the collection of pairs $(a, f(a))$ and flip the pairs to get an inverse?

[Mario Carneiro]

Ah, here's another way to show choiceless Type is not a topos:

Corollary 4.2. $\mathbf{C}$ is balanced, i.e., a morphism in $\mathbf{C}$ is an isomorphism iff it is both monic and epic. (https://ncatlab.org/nlab/show/subobject+classifier)

This is not true in Type, since as I said monic means injective and epic means surjective, and the conjunction of these is bijective which is not the same as equiv which is isomorphism.

[Mario Carneiro]

Actually unique choice is enough to prove that a bijection is an equiv

[Mario Carneiro]

so you can still get this property without collapsing Prop = bool

[Mario Carneiro]

Could you explain why couldn't we do something like, take the collection of pairs $(a, f(a))$ and flip the pairs to get an inverse?

because that's not how functions are defined in type theory. In type theory every function is given by a term that has a free variable for the argument

[Mario Carneiro]

That is, "functions" and "functional relations" are not the same

[Mario Carneiro]

a definition like that one would give a functional relation, but proving that a functional relation induces a function requires unique choice

[Mario Carneiro]

By the way, this kind of thing comes up even in "real math". For example, the derivative of a function is a functional relation, not a function

[Mario Carneiro]

You can of course use choice to upgrade it to a function but it's not quite natural and lean will make it feel a little awkward

[Jesse Michael Han]

Right, I see.

Ah, here's another way to show choiceless Type is not a topos:

Corollary 4.2. $\mathbf{C}$ is balanced, i.e., a morphism in $\mathbf{C}$ is an isomorphism iff it is both monic and epic. (https://ncatlab.org/nlab/show/subobject+classifier)

This is not true in Type, since as I said monic means injective and epic means surjective, and the conjunction of these is bijective which is not the same as equiv which is isomorphism.

This is what one usually uses to show that the image of a mono is isomorphic to its domain, so that makes sense.

[David Michael Roberts]

Well, that was the informal explanation. The real definition is Def 4.1 in Shulman's https://arxiv.org/pdf/1808.05204.pdf and is stated in the context of a Heyting category, so no subobject classifier necessary.

[David Michael Roberts]

Also, I wouldn't naively take Prop to be the subobject classifier. What about 1 -> Prop?

[Mario Carneiro]

Prop and 1 -> Prop are isomorphic

[David Michael Roberts]

Ah, well... :-/

[David Michael Roberts]

Looking at

Def 4.1 in Shulman's https://arxiv.org/pdf/1808.05204.pdf

part a) gives me pause. The other parts b)-d) seem ok (Epis are surjective, "every function 1-> U \cup V factors through U or V" and 1->0 is empty).

[Mario Carneiro]

I guess (b) isn't obvious to me, mostly because I'm learning the terminology as I go

[Mario Carneiro]

But (a) does indeed look to be false. If m : A -> X is bijective, then for every x : X (add 1 -> if you like) there exists y : A such that f x = y, but it is not necessarily an isomorphism

[David Michael Roberts]

By Remark 4.2 b) is equiv to epis are surjective, which you proved above.

[Mario Carneiro]

But, I think we have to be more careful about what the actual category under discussion is. Is all the metatheory being internalized to Lean?

[Mario Carneiro]

That is, if you prove there exists a morphism that may not mean that there is a closed term morphism

[David Michael Roberts]

Hmm, not sure. I was vaguely planning on formalising Mike's definitions and seeing what happened.

[Mario Carneiro]

I can almost imagine that knowing that every x : 1 -> X splits over m in some strong external sense implying that there is an inverse function

[Mario Carneiro]

but that has its own issues

[Mario Carneiro]

If you assume choice, then of course you get all these properties

[Reid Barton]

I just tuned in and I'm not really sure what is going on here, but in the opposite direction it seems that (c) could fail if you interpreted "either A or B must be ..." in a strong external sense, as well

[David Michael Roberts]

I can almost imagine that knowing that every x : 1 -> X splits over m in some strong external sense implying that there is an inverse function

ah, that would be quantifying over 1->X I suppose, leading to a section (?). This is the old problem that with the strong constructive quantifier the axiom of choice is simply true.

[Reid Barton]

Same with (b) if you interpret the statement as a Pi/Sigma rather than a forall/exists

[David Michael Roberts]

I just tuned in and I'm not really sure what is going on here, but in the opposite direction it seems that (c) could fail if you interpreted "either A or B must be ..." in a strong external sense, as well

I would imagine it's not meant to be exclusive or.

[Reid Barton]

I mean that you could interpret it as a sum type

[Mario Carneiro]

it's certainly exclusive or, but that's not the hard part

[David Michael Roberts]

@Reid Barton yes, I imagine so.

[Reid Barton]

rather than the propositional truncation thereof

[David Michael Roberts]

@Mario Carneiro but what if A=B as subobjects of X? (here I'm using Remark 4.2 again)

[Reid Barton]

I haven't read the preceding part of the paper so I'm not sure whether the metatheory is intended to be classical or what.

[Mario Carneiro]

If A = B then 1 = A \cup A, and then by pushing the unique element of 1 around you find A = 1 and hence 1 has two distinct elements, which is false

[Mario Carneiro]

Actually I'm not even sure why that is an axiom, seems like it should be true in the base theory

[Mario Carneiro]

If 1 = A \cup B then you get a distinguished element of A \cup B, and by following it you find which one is isomorphic to 1

[Mario Carneiro]

then again that relies on elementwise reasoning so it probably isn't true in the base theory

[David Michael Roberts]

Fair enough. Gotta run now, though

[Reid Barton]

BTW, are you allowing funext?

[Mario Carneiro]

I was assuming the other two axioms

[Mario Carneiro]

It is true that without quot.sound you have to worry about funext

[Reid Barton]

Okay good, otherwise I was confused about some earlier stuff.

[Mario Carneiro]

and in that case I'm not sure there is a good theory at all, since the category is all about equalities of morphisms which are functions

[Kevin Buzzard]

I love that #new users has all these questions about how @ works etc and then a huge thread about topos theory :-)

[David Michael Roberts]

Tbh I barely know how @ works, too, but I am coming at this top-down, which is probably the wrong way to do it.

[Kevin Buzzard]

I don't think there are right and wrong ways to do it. I think we're still figuring out the best ways to learn and to direct growth of Lean. I think the best way to do it is to try all the ways we can think of.

[Jesse Michael Han]

Re: the preceding discussion, I think one again needs unique choice to show (besides ruling out things like uninvertible bijections) that any epimorphism satisfies the universal property with respect to its kernel relation on its domain (i.e. is regular).