## Stream: new members

### Topic: ETCS

#### 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

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

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

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

#### 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

#### Mario Carneiro (Oct 10 2018 at 05:42):

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

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

#### 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

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

#### Mario Carneiro (Oct 10 2018 at 05:43):

hSet = Type in lean

Oh, cool!

#### Mario Carneiro (Oct 10 2018 at 05:43):

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

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

#### Mario Carneiro (Oct 10 2018 at 05:45):

yes, that should not be difficult

#### Simon Hudon (Oct 10 2018 at 05:45):

There is a category of types in category_theory.types

#### 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

also ^ that

#### Simon Hudon (Oct 10 2018 at 05:46):

@Scott Morrison not fast enough!

:-)

#### Scott Morrison (Oct 10 2018 at 05:46):

I was running a longer race. :-)

#### Simon Hudon (Oct 10 2018 at 05:47):

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

#### David Michael Roberts (Oct 10 2018 at 05:50):

OK, cool, thanks :-)

#### Mario Carneiro (Oct 10 2018 at 05:50):

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

#### 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

#### 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?

#### Mario Carneiro (Oct 10 2018 at 05:51):

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

#### Mario Carneiro (Oct 10 2018 at 05:52):

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

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

#### David Michael Roberts (Oct 10 2018 at 05:52):

Which lives...? (thanks, btw)

#### David Michael Roberts (Oct 10 2018 at 05:52):

@Bryan Gin-ge Chen cool, thanks

#### Mario Carneiro (Oct 10 2018 at 05:52):

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

#### Bryan Gin-ge Chen (Oct 10 2018 at 05:52):

Here's the vscode file

:+1:

#### 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

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

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

#### David Michael Roberts (Oct 13 2018 at 04:22):

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

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

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

#### Mario Carneiro (Oct 13 2018 at 04:24):

Do you know what that should mean?

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

#### 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

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

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

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

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

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

#### 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?

#### 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 $\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 (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.

#### 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?

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

#### 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))$ and flip the pairs to get an inverse?

#### Mario Carneiro (Oct 14 2018 at 01:26):

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 (Oct 14 2018 at 01:27):

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

#### Mario Carneiro (Oct 14 2018 at 01:27):

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

#### 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))$ 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 (Oct 14 2018 at 01:29):

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

#### 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

#### 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

#### 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

#### 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. $\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 (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.

#### 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?

#### Mario Carneiro (Oct 14 2018 at 01:54):

Prop and 1 -> Prop are isomorphic

Ah, well... :-/

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

#### 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

#### 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

#### David Michael Roberts (Oct 14 2018 at 02:03):

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

#### 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?

#### 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

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

#### 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

#### Mario Carneiro (Oct 14 2018 at 02:05):

but that has its own issues

#### Mario Carneiro (Oct 14 2018 at 02:06):

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

#### 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

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

#### 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

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

#### Reid Barton (Oct 14 2018 at 02:08):

I mean that you could interpret it as a sum type

#### Mario Carneiro (Oct 14 2018 at 02:08):

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

#### David Michael Roberts (Oct 14 2018 at 02:08):

@Reid Barton yes, I imagine so.

#### Reid Barton (Oct 14 2018 at 02:08):

rather than the propositional truncation thereof

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

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

#### 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

#### 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

#### 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

#### 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

#### David Michael Roberts (Oct 14 2018 at 02:14):

Fair enough. Gotta run now, though

#### Reid Barton (Oct 14 2018 at 02:16):

BTW, are you allowing funext?

#### Mario Carneiro (Oct 14 2018 at 02:17):

I was assuming the other two axioms

#### Mario Carneiro (Oct 14 2018 at 02:17):

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

#### Reid Barton (Oct 14 2018 at 02:17):

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

#### 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

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

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

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

#### 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