Zulip Chat Archive

Stream: new members

Topic: ETCS


view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:32):

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:33):

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:35):

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)

view this post on Zulip Simon Hudon (Oct 10 2018 at 05:36):

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.

view this post on Zulip Simon Hudon (Oct 10 2018 at 05:37):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:42):

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:42):

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.

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:43):

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:43):

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)

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:43):

hSet = Type in lean

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:43):

Oh, cool!

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:43):

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:44):

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.

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:45):

yes, that should not be difficult

view this post on Zulip Simon Hudon (Oct 10 2018 at 05:45):

There is a category of types in category_theory.types

view this post on Zulip Scott Morrison (Oct 10 2018 at 05:45):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:45):

also ^ that

view this post on Zulip Simon Hudon (Oct 10 2018 at 05:46):

@Scott Morrison not fast enough!

view this post on Zulip Scott Morrison (Oct 10 2018 at 05:46):

:-)

view this post on Zulip Scott Morrison (Oct 10 2018 at 05:46):

I was running a longer race. :-)

view this post on Zulip Simon Hudon (Oct 10 2018 at 05:47):

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:50):

OK, cool, thanks :-)

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:50):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:51):

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:51):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:51):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:52):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2018 at 05:52):

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

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:52):

Which lives...? (thanks, btw)

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:52):

@Bryan Gin-ge Chen cool, thanks

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:52):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2018 at 05:52):

Here's the vscode file

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:54):

:+1:

view this post on Zulip Mario Carneiro (Oct 10 2018 at 05:55):

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

view this post on Zulip Jesse Michael Han (Oct 13 2018 at 04:14):

@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.

view this post on Zulip David Michael Roberts (Oct 13 2018 at 04:22):

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)

view this post on Zulip David Michael Roberts (Oct 13 2018 at 04:22):

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

view this post on Zulip David Michael Roberts (Oct 13 2018 at 04:23):

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

view this post on Zulip David Michael Roberts (Oct 13 2018 at 04:24):

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

view this post on Zulip Mario Carneiro (Oct 13 2018 at 04:24):

Do you know what that should mean?

view this post on Zulip David Michael Roberts (Oct 13 2018 at 04:26):

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)

view this post on Zulip David Michael Roberts (Oct 13 2018 at 04:27):

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

view this post on Zulip David Michael Roberts (Oct 13 2018 at 04:29):

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

view this post on Zulip Mario Carneiro (Oct 13 2018 at 05:12):

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)

view this post on Zulip Mario Carneiro (Oct 13 2018 at 05:24):

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.

view this post on Zulip Mario Carneiro (Oct 13 2018 at 06:02):

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).

view this post on Zulip David Michael Roberts (Oct 13 2018 at 07:11):

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 :-)

view this post on Zulip Mario Carneiro (Oct 13 2018 at 07:13):

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?

view this post on Zulip Jesse Michael Han (Oct 13 2018 at 19:19):

@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 p¬p \vdash p \vee \neg p, it does not necessarily decide if pp is true or false.

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

view this post on Zulip Mario Carneiro (Oct 13 2018 at 23:40):

@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.

view this post on Zulip Jesse Michael Han (Oct 14 2018 at 00:56):

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?

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:16):

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.

view this post on Zulip Jesse Michael Han (Oct 14 2018 at 01:25):

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))(a, f(a)) and flip the pairs to get an inverse?

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:26):

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

Corollary 4.2. C\mathbf{C} is balanced, i.e., a morphism in C\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.

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:27):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:27):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:29):

Could you explain why couldn't we do something like, take the collection of pairs (a,f(a))(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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:29):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:30):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:31):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:32):

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

view this post on Zulip Jesse Michael Han (Oct 14 2018 at 01:34):

Right, I see.

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

Corollary 4.2. C\mathbf{C} is balanced, i.e., a morphism in C\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.

view this post on Zulip David Michael Roberts (Oct 14 2018 at 01:51):

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.

view this post on Zulip David Michael Roberts (Oct 14 2018 at 01:52):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:54):

Prop and 1 -> Prop are isomorphic

view this post on Zulip David Michael Roberts (Oct 14 2018 at 01:55):

Ah, well... :-/

view this post on Zulip David Michael Roberts (Oct 14 2018 at 01:57):

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).

view this post on Zulip Mario Carneiro (Oct 14 2018 at 01:59):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:02):

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

view this post on Zulip David Michael Roberts (Oct 14 2018 at 02:03):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:03):

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?

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:04):

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

view this post on Zulip David Michael Roberts (Oct 14 2018 at 02:04):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:05):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:05):

but that has its own issues

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:06):

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

view this post on Zulip Reid Barton (Oct 14 2018 at 02:06):

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

view this post on Zulip David Michael Roberts (Oct 14 2018 at 02:07):

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.

view this post on Zulip Reid Barton (Oct 14 2018 at 02:08):

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

view this post on Zulip David Michael Roberts (Oct 14 2018 at 02:08):

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.

view this post on Zulip Reid Barton (Oct 14 2018 at 02:08):

I mean that you could interpret it as a sum type

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:08):

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

view this post on Zulip David Michael Roberts (Oct 14 2018 at 02:08):

@Reid Barton yes, I imagine so.

view this post on Zulip Reid Barton (Oct 14 2018 at 02:08):

rather than the propositional truncation thereof

view this post on Zulip David Michael Roberts (Oct 14 2018 at 02:09):

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

view this post on Zulip Reid Barton (Oct 14 2018 at 02:09):

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.

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:10):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:11):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:13):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:13):

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

view this post on Zulip David Michael Roberts (Oct 14 2018 at 02:14):

Fair enough. Gotta run now, though

view this post on Zulip Reid Barton (Oct 14 2018 at 02:16):

BTW, are you allowing funext?

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:17):

I was assuming the other two axioms

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:17):

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

view this post on Zulip Reid Barton (Oct 14 2018 at 02:17):

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

view this post on Zulip Mario Carneiro (Oct 14 2018 at 02:18):

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

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 10:15):

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

view this post on Zulip David Michael Roberts (Oct 14 2018 at 10:45):

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

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 13:23):

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.

view this post on Zulip Jesse Michael Han (Oct 14 2018 at 17:55):

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).


Last updated: May 14 2021 at 13:24 UTC