universes

Stream: general

[Phiroc]

Hello,
in Theorem Proving in Lean, the authors provide the following examples:

#check list -- Type u_1 -> Type u_1
#check prod -- Type u_1 -> Type u_2 -> Type (max u_1 u_2)

Why is the universe the same in the first case, and different in the second?

[Mario Carneiro]

there is one input in the first case and two in the second

[Mario Carneiro]

in general, we want the output type to be determined by the inputs, and the output type will usually be the max of the universes of all the inputs

[Johan Commelin]

Are there foundational problems with allowing mild(?) quantification over universe variables?

[Mario Carneiro]

yes, it increases the axiomatic strength

[Johan Commelin]

That's the only problem?

[Johan Commelin]

Sounds like a good thing to me :grinning:

[Mario Carneiro]

I mean it doesn't really solve any problems, you just get more universes that you aren't allowed to quantify over

[Johan Commelin]

Well, it might solve my problems

[Mario Carneiro]

if you add the ability to quantify over all universes, including the ones you are adding, then you get a second impredicative universe and then it's hello paradox

[Johan Commelin]

I think I only care about rings/modules/schemes that live in Type n for n : nat

[Mario Carneiro]

I think I would prefer the solution Kevin often talks about, where you have less universes, preferably none

[Johan Commelin]

And since most mathematicians still pretend they only work in Type 0, I think it will take some time before we get a profound mathematical construction that genuinely takes a limit construction over Type n (n : nat) to produce something that lives in Type \omega

[Johan Commelin]

Mario Carneiro said:

I think I would prefer the solution Kevin often talks about, where you have less universes, preferably none

But then, why all this trouble of being universe polymorphic?

[Mario Carneiro]

The thing is, once you are doing limit constructions you don't just get to Type \omega, you get to Type (aleph omega) or an even higher cardinal

[Mario Carneiro]

We have to be universe polymorphic because someone had the poor sense to put universes in the type theory

[Johan Commelin]

Right, but my point is that I don't see such constructions happening.

[Johan Commelin]

Whereas I do hope that we might be able to have etale cohomology soonish. The ingredients are slowly dripping into mathlib.

[Mario Carneiro]

so if you want to be generic over things you can construct in lean then you have to be universe polymorphic

[Johan Commelin]

But without universes, you'll have a major pain when you try to define sheaf cohomology

[Mario Carneiro]

I don't think universes actually solve that pain, they just put it somewhere else

[Johan Commelin]

Why?

[Mario Carneiro]

because you can't iterate any universe bumping construction, so inevitably you still have to figure out how to do whatever you are doing without any universe bumps

[Johan Commelin]

Right, but my point is that I don't know of any construction in maths that (even informally) is iterating universe bumps.

[Mario Carneiro]

and at the end of it you realize it all fit in ZFC to begin with

[Mario Carneiro]

I've said it before: what category theorists actually want is Type in Type, not this universe nonsense

[Mario Carneiro]

and if and when you make all the reasoning consistent you find it's just plain old ZFC

[Mario Carneiro]

universes make everything more complicated and don't solve the problem they set out to solve

[Reid Barton]

I totally disagree with the above 3 lines, with the caveat that math universes are not the same as type theory universes

[Reid Barton]

It all fits in ZFC+U--if we're redefining ZFC to mean that then great

[Reid Barton]

It's also probably the case in a given application (in algebraic geometry say) that you can remove the "U" axiom, in the reverse mathematics sense--but this doesn't mean the category theory itself lives in ZFC, any more than the modularity theorem lives in PA

[Mario Carneiro]

I think most real category theory still fits in higher order ZFC, with no actual universes

[Mario Carneiro]

and higher order ZFC fits in ZFC for most concrete arguments if you play enough logical tricks

[Kevin Buzzard]

There are certainly some instances where mathematicians do stuff with universes and then force everything back into ZFC. However it is getting to the point where there are things which some mathematicians (e.g. Scholze) do which cannot be forced back into ZFC, or, at least, nobody is trying to force it back into ZFC right now. We're quite a way away from this in mathlib so whether this will matter to us in practice is unclear to me -- but perhaps Reid knows other areas of maths which are also falling out of ZFC.

I am not looking forward to all this "force everything back into ZFC" issue when we run into etale cohomology. We want to take a limit over a universe and then there's a theorem saying that it's "equal to" a limit over a type. Nowadays I am quite conflicted about to how important this descent is.

[Reid Barton]

Mike Shulman has a paper https://arxiv.org/pdf/0810.1279.pdf discussing size issues in category theory and the possible ways to resolve them (including universes).

[Reid Barton]

Here's a simple example where ZFC is inadequate. Suppose I already have a theory of monoidal categories and monoid objects in them and their modules. Now a friendly Haskell programmer informs me that a monad on a category $C$ is "just a monoid in the category of endofunctors $[C, C]$". Great, now I can apply my existing theory to get a theory of monads and their modules (usually known as algebras).

[Reid Barton]

However, if I try to apply this to a large category (like $C = \mathrm{Set}$ or $C = \mathrm{Mod}_R$) this breaks down, because the "endofunctor category" $[C, C]$ is "too large" to fit in ZFC even as a proper class (basically because its objects are already class-sized).

[Reid Barton]

So, I'm forced to develop a parallel but separate theory of monads on large categories.

[Reid Barton]

For a much fancier example, in algebraic geometry, there's no difficulty in ZFC in defining a stack of small categories on a small site. But, putting aside the issue of the size of the site, it's also very useful to consider stacks of large categories. For example, there is a stack which assigns to $\mathrm{Spec}\,R$ the category $\mathrm{Mod}_R$ of $R$-modules. On a scheme $X$, the "global sections" of this stack is the category of quasicoherent modules on $X$.

[Kevin Buzzard]

It would not surprise me if some mathematicians thought that we were in some kind of second foundational crisis -- ZFC worked fine for 100 years but now people really want to do stuff which pushes it to the limits and possibly beyond. However there are many areas of mathematics for which ZFC is completely adequate; I was talking to Hairer about this and he seemed absolutely convinced that he didn't even need full AC, and that ZF + countable dependent choice could get him a Fields Medal in the kind of analysis he did.

[Kevin Buzzard]

I've never thought about precisely how much AC I need, but I have this uncomfortable feeling that the ZFC crisis I had in my 20s, when I carefully checked that a bunch of stuff I wanted/needed could be done in ZFC, is now going to be repeated if I ever want to dive into condensed mathematics, and this time I'm not entirely sure what the answer will be.

[Reid Barton]

With my category theorist hat on, I want to make two points:

1. It really is important to make some size distinctions, at least to the extent of "small" and "large" , because you can't do very much category theory without talking about Set and other large categories, and here we already find for example that Set has (co)limits indexed by small categories but not large ones. The beginning of Shulman's paper gives more examples of this kind.
2. It's useful at least for conceptual reasons to talk about "very large" categories like $[\mathrm{Set}, \mathrm{Set}]$ or the 2-category of all stacks of locally presentable categories on a scheme (or whatever). These objects are too big to exist in ZFC(at least if we interpret $\mathrm{Set}$ as referring to the category of all sets, and similarly for locally presentable categories).

[Reid Barton]

Now,

• In the end, one might be interested in a specific theorem about monads or quasicoherent modules or whatever, and then one could ask whether or not this theorem is provable in ZFC. In my view, this is basically a question of reverse mathematics, and those who aren't interested in such questions shouldn't feel obliged to care about them.
• A lot of category theory can be presented in a way which is agnostic to the specific foundations, while still making the basic small/large distinction. In this case, the reader can choose whether to interpret "small/large" as "set/class" or "element of $\mathcal{U}$/non-element of $\mathcal{U}$" or in some other way.

Personally, I find the interpretation using Grothendieck universes convenient because it allows me to make sense of all category theory using ordinary sets, and doesn't need classes or fancy logic. However, it does have the disadvantages that the interpretation is relative to a fixed inaccessible cardinal and that, for example, a group constructed to have a certain universal property a priori only has this universal property with respect to other groups that are small with respect to the reference cardinal, and not with respect to all groups.

[Patrick Massot]

Reid, since you are in this foundational mood, and I don't know anything about all this, do you have a definitive answer to the question: if I have a set S, can I define free groups over $S$ as groups $F$ equipped with a map from $i : S \to F$ such that, for all groups $G$ and $f : S \to G$ there is a unique morphism $\varphi : F \to G$ such that $\varphi \circ i = f$? Or is it forbidden because there is no set of groups? If it's forbidden, what can be done?

[Patrick Massot]

I have the vague impression this is forbidden as a definition but somewhat allowed as a theorem about a given $F$, but this doesn't seem to make any sense.

[Johan Commelin]

At least in Lean the answer seems to be that you cannot make it the definition, but you can make it a theorem.

[Patrick Massot]

Yes, this is my impression, but it's weird and I'd like to understand this one day (or at least have the feeling to understand a bit and get a reference I can read from times to times)

[Kevin Buzzard]

Yes that's no definition. You can only quantify over all G in some universe, so really you end up with infinitely many universal properties in some sense.

[Patrick Massot]

But still it can be a property, right?

[Patrick Massot]

Because if I define $F$ using reduced words etc. then certainly it satisfies the universal property for all groups, right?

[Reid Barton]

In ZFC the predicate "$f : S \to F$ exhibits $F$ as the free group on $S$" defined in this way (for all groups $G$ and maps $S \to G$ there exists ...) is totally fine. For example, it could be a hypothesis to a theorem. (Of course you need to do something else to prove that there actually exists such an $F$ and $f$, but I don't think that's what you were asking about.)

[Patrick Massot]

Then where is the problem? Is it that we want more than ZFC for other purposes and this breaks this definition?

[Reid Barton]

The problem with doing category theory in ZFC?

[Patrick Massot]

The problem with defining stuff using universal properties

[Patrick Massot]

If I have several universes, I can still prove that my favorite free groups satisfies the universal property for all groups in any universe but this cannot be an assumption in a theorem, right?

[Eric Wieser]

... which means you can end up writing essentially the same proof over and over again for each of your favorite free groups, right?

[Patrick Massot]

And if I have a low-tech definition of free groups (something like $i(S)$ generates $F$ and there is no relation between elements of $i(S)$, which can be defined properly), I cannot state something like "$(F, i)$ is a free group on $S$ iff it satisfies the universal property for every group in every universe" right?

[Johan Commelin]

What do you mean with "any"?

[Johan Commelin]

If it means "all", then you indeed cannot,
if it means "there exists a universe", then you can

[Reid Barton]

If you're doing category theory in ZFC+U with the "all categories implicitly relativized to a universe $\mathcal{U}$" convention, then it is still meaningful to talk about whether a morphism $f : S \to UF$ ($U : \mathrm{Set} \to \mathrm{Grp}$ the forgetful functor) has the universal property of making $F$ a free group with respect to all groups. It just isn't the condition that falls out from the category theory, because $\mathrm{Grp}$ now means "all $\mathcal{U}$-small groups" (and likewise for $\mathrm{Set}$).

[Patrick Massot]

English is a really awful language, but hopefully I disambiguated.

[Reid Barton]

At least not by definition--of course in this case the two conditions really are equivalent, but the easiest way to see that might be to note that you can construct the free group in a way that does not depend upon the reference universe $\mathcal{U}$.

[Reid Barton]

Johan's answer is right for Lean, but not for ZFC+U, I think.

[Patrick Massot]

But why is there this assymetry that I can state this as a property of a given concrete $(F, i)$ but not as an assumption of a theorem?

[Reid Barton]

You can state that, and even prove it.

[Reid Barton]

In Lean, it works differently because you can only quantify over types in a specific universe, and quantifiers over universes can only occur at the outside of a top-level definition.

[Reid Barton]

In ZFC I think that statements which use bounded quantification, i.e., only have quantifiers like $\forall X, X \in S \to \ldots$ is a notion which is useful, but you're not restricted to only making such statements.

[Reid Barton]

(Sorry, that was a poorly-constructed sentence but I hope it makes sense.)

[Patrick Massot]

So what is impossible with ZFC + universes then?

[Reid Barton]

The drawback of this approach isn't that anything is impossible, but rather that if you really care about (let's say) "Universal" properties that quantify over all groups, or whatever, you will have to do some extra work to know that you have one.

[Reid Barton]

Whereas if you really did category theory with the category of all groups in the first place, then universal properties in category theory would be true Universal properties.

[Reid Barton]

(Plus of course you might be concerned about accepting the universe axiom, which does prove additional arithmetic statements like Con(ZFC).)

[Patrick Massot]

What is Con(ZFC)?

[Patrick Massot]

consistency?

[Reid Barton]

Yes, or more precisely, some encoding of it in terms of natural numbers.

[Reid Barton]

Some particular, rather large polynomial in a few variables has no integer solution.

[Reid Barton]

The later parts of Shulman's paper go into ways to systematically turn universe-relative universal properties into true Universal properties, and ways you might be able to talk about "very large" categories without increasing the consistency strength of the background theory.

[Patrick Massot]

Ok, thanks for all you explanations! I'll try to think about all that.

[Adam Topaz]

I have a question related to this issue about defining things in terms of their universal properties. I know of one example in mathlib which does (more-or-less) exactly this: src#stone_cech_setoid
Does this mean that mathlib only has the universal property of the Stone-Cech compactification for topological spaces which live in the same universe? Is there any way around this (without changing the definition of stone_cech)?

[Mario Carneiro]

@Adam Topaz It is a curious consequence of "internal definitions" (for example, a free group is a certain quotient of lists) that they imply and are implied by the "external definition" (a free group is one that maps in an appropriate way to all groups) at every universe. This fact means that even a definition using an external definition at Type u is equivalent to the external definition at all types, so stone_cech's universal property applies even to larger universes even though you can't apply it directly

[Mario Carneiro]

Patrick Massot said:

But why is there this assymetry that I can state this as a property of a given concrete $(F, i)$ but not as an assumption of a theorem?

The key to this ability for us to prove external properties that we didn't quantify over to start with at the foundational level is the extra universe argument in T.rec:

inductive nat'
| zero : nat'
| succ : nat' → nat'
#print nat'.rec
-- protected eliminator nat'.rec : Π {C : nat' → Sort l},
--  C nat'.zero → (Π (a : nat'), C a → C a.succ) → Π (n : nat'), C n

Note that nat' has no universe parameters but it has a recursor that quantifies over a universe parameter l. If recursors didn't do this, for example if nat'.rec only quantified over C : nat' -> Type, then we wouldn't need the inductive axioms at all; we could use church encodings to do everything. But this universe lifting property is truly magical, as it allows you to prove that a universal property at one type implies a universal property for one specifically crafted inductive type, which then implies the universal property at a higher universe using that inductive type's recursor.

[Adam Topaz]

@Mario Carneiro As a concrete example, is it possible to make the second example in the following code work?

import topology.stone_cech

noncomputable theory

universes u v
variables {α : Type u} {β : Type v} [topological_space α] [topological_space β]
  [compact_space β] [t2_space β]
variables {γ : Type u} [topological_space γ] [compact_space γ] [t2_space γ]

example (f : α → γ) (cont : continuous f) : stone_cech α → γ := stone_cech_extend cont -- works

example (f : α → β) (cont : continuous f) : stone_cech α → β := stone_cech_extend cont -- doesn't work

I understand that it's possible to prove that the stone cech compactification of a topological space in Type u, which is defined so that it satisfies the universal property with respect to every topological space of Type u, also satisfies the universal property for every topological space of Type v. But it seems to me that doing this is essentially equivalent to redefining the stone cech compactification, or more specifically in this case, the equivalence relation stone_cech_setoid, so that it doesn't quantify over types in the first place.

[Mario Carneiro]

that's right

[Mario Carneiro]

you can't apply stone_cech_extend directly

[Adam Topaz]

Okay, so life isn't as easy as I would have hoped.

[Mario Carneiro]

but you can hide this construction inside a proof, for example, if you wanted to keep the definition "clean"

[Adam Topaz]

Mario Carneiro said:

but you can hide this construction inside a proof, for example, if you wanted to keep the definition "clean"

What do you mean by this?

[Mario Carneiro]

you can construct an inductive type with the requisite properties in order to prove that the universal property at u implies the universal property at v

[Mario Carneiro]

and then that is the theorem you would be applying instead of stone_cech_extend

[Adam Topaz]

Oh, I'm not sure what such an inductive type would like like. You mean something similar to ulift?

[Mario Carneiro]

no, it depends on the universal property

[Mario Carneiro]

for free groups it's lists on the basic elements

[Mario Carneiro]

in a lot of categorical proofs this is where we show that the presheaf is representable

[Adam Topaz]

Ah okay. So this would just redefine the object altogether then.

[Reid Barton]

When I wrote the stone_cech stuff I think I just followed some notes I found online--if there's a way to describe the required topology directly, without quantifying over Type u, then that's probably a better definition.

[Adam Topaz]

I think there is a way to do it, using the monadic properties of ultrafilters, but of course it's more complicated.

[Mario Carneiro]

I think the internal definition of stone cech uses the set of ultrafilters

[Adam Topaz]

Actually, maybe it's not too bad with what's in this file:
https://github.com/leanprover-community/mathlib/blob/master/src/topology/category/Compactum.lean

[Reid Barton]

For example maybe it's enough to consider all quotients of ultrafilter α itself

[Reid Barton]

or maybe you don't even need to allow a quotient

[Adam Topaz]

Isn't the stone cech compactification the largest quotient of ultrafilter \a which is an algebra for the ultrafilter monad, and for which the canonical map from \a is continuous?

[Adam Topaz]

This would be a description that says nothing about any type other than \a itself.

[Mario Carneiro]

@_Wikipedia said:

There are several ways to modify this idea to make it work; for example, one can restrict the compact Hausdorff spaces K to have underlying set P(P(X)) (the power set of the power set of X), which is sufficiently large that it has cardinality at least equal to that of every compact Hausdorff set to which X can be mapped with dense image.

[Adam Topaz]

The constructions in terms of maps to the unit interval (from wiki) would also work, I guess.

[Mario Carneiro]

This reminds me that hausdorff sets have an interesting cardinality bound: they are at most the double powerset of any dense subset A because you can uniquely pick out every element of X by a filter in A

[Mario Carneiro]

I think this proof would be easiest (I've done it in metamath before, it follows from the axioms pretty easily)

[Mario Carneiro]

the unit interval requires partitions of unity, which I think are more complicated

[Reid Barton]

By the way, what was the original point of this thread? :upside_down:

[Reid Barton]

What was quantifying over universe levels intended to be used for?

[Mario Carneiro]

I think specifying universal properties?

[Johan Commelin]

Johan Commelin said:

Are there foundational problems with allowing mild(?) quantification over universe variables?

Why can't I write a bundled_hom class that is universe polymorphic...

[Johan Commelin]

That's what my motivation was

[Johan Commelin]

Because I want bundled_hom.funext and bundled_hom.congr_arg and bundled_hom.congr_fun, etc...

[Mario Carneiro]

what is a bundled hom in this context?

[Johan Commelin]

Instead of having to reprove them for mul_hom, zero_hom, monoid_hom, one_hom, ring_hom, alg_hom, the list goes on...

[Adam Topaz]

E.g. a group homomorphism from a group of Type u to a group of Type v.

[Mario Carneiro]

equiv is a universe polymorphic bundled hom

[Johan Commelin]

Mario Carneiro said:

what is a bundled hom in this context?

It is bundled_hom in the sense of docs#bundled_hom

[Johan Commelin]

Snap!

[Reid Barton]

It's not clear to me why this needs more universe quantification than Lean provides

[Adam Topaz]

I think it's because of bundled as in docs#category_theory.bundled

[Mario Carneiro]

docs#category_theory.bundled_hom is a predicate on homs from Type u to Type u. It could be a predicate on homs from Type u to Type v but then you couldn't compose them

[Johan Commelin]

variables {c : Type u → Type u} (hom : Π ⦃α β : Type u⦄ (Iα : c α) (Iβ : c β), Type u)

/-- Class for bundled homs. Note that the arguments order follows that of lemmas for `monoid_hom`.
This way we can use `⟨@monoid_hom.to_fun, @monoid_hom.id ...⟩` in an instance. -/
structure bundled_hom :=
(to_fun : Π {α β : Type u} (Iα : c α) (Iβ : c β), hom Iα Iβ → α → β)
(id : Π {α : Type u} (I : c α), hom I I)
(comp : Π {α β γ : Type u} (Iα : c α) (Iβ : c β) (Iγ : c γ),
  hom Iβ Iγ → hom Iα Iβ → hom Iα Iγ)
(hom_ext : ∀ {α β : Type u} (Iα : c α) (Iβ : c β), function.injective (to_fun Iα Iβ) . obviously)
(id_to_fun : ∀ {α : Type u} (I : c α), to_fun I I (id I) = _root_.id . obviously)
(comp_to_fun : ∀ {α β γ : Type u} (Iα : c α) (Iβ : c β) (Iγ : c γ)
  (f : hom Iα Iβ) (g : hom Iβ Iγ),
  to_fun Iα Iγ (comp Iα Iβ Iγ g f) = (to_fun Iβ Iγ g) ∘ (to_fun Iα Iβ f) . obviously)

[Johan Commelin]

You can't even define them with two universe variables

[Johan Commelin]

Because you need id

[Mario Carneiro]

Actually I think c could be Type u -> Type v

[Adam Topaz]

It would be cool to define the "category" of groups as having underlying object type \Sigma {u : universe} (G : Type u) (is_group : group G)

[Reid Barton]

oh bundled_hom isn't a bundled hom

[Johan Commelin]

But nevertheless ring_hom.id is a thing

[Johan Commelin]

Adam Topaz said:

It would be cool to define the "category" of groups as having underlying object type \Sigma {u : universe} (G : Type u) (is_group : group G)

Is that an example of a \HUGE category?

[Reid Barton]

I'm trying to understand what the end goal is though

[Mario Carneiro]

type in type

[Adam Topaz]

So that the universal property of the free group is actually the left adjoint to the forgetful functor for example.

[Reid Barton]

But bundled_hom.funext and so on sounds a lot simpler than talking about universal properties

[Mario Carneiro]

also don't forget the "metatheorem" approach: write a tactic to generate all instantiations of a schematic theorem

[Mario Carneiro]

you can quite often write higher order theorems than the logic actually supports this way

[Reid Barton]

This was on my mind too but I wanted to understand what those theorems are first.

[Mario Carneiro]

I think a tactic that writes the theory of foo_homs would be more useful than literal category theory

[Mario Carneiro]

and as long as everything is in meta-land the high consistency strength requirements of general category theory is no problem

[Reid Barton]

Well, I think Johan's intention was also not to literally do category theory but just be able to abstract over what it means to be a "foo hom" when multiple universes are involved

[Mario Carneiro]

sure, but I assume this is going to be used for something

[Mario Carneiro]

like perhaps proving theorems generic over different kinds of bundled homs

[Reid Barton]

For ext this problem is already solved by @[ext], right?

[Mario Carneiro]

I think the interesting problem is explicating the actual set of theorems we'd like to generate for foo homs

[Reid Barton]

What's an example of a theorem in mathlib which would be a special case of one of these generalized theorems?

[Mario Carneiro]

I am still stuck at the stage where everything category theory appears to deliver is utterly trivial results about associativity pentagons that are one line proofs in the concrete case, which is why I have a poor opinion of the subject

[Reid Barton]

In particular, it's not clear to me that we couldn't solve whatever the problem is by just having a class like class has_hom (foo : Type*) (bar : Type*) without it knowing that we're always going to set e.g. foo = ring.{u} and bar = ring.{v}.

[Adam Topaz]

I would like to be able to write the following, for example:

class is_free_group (G : Type u) (S : Type u) [group G] :=
(incl : S → G)
(lift {v : universe} {H : Type v} [group H] (f : S → H) : G →* H)
(lift_comp_incl {v : universe} {H : Type v} [group H] {f : S → H} : (lift f) ∘ incl = f)
(lift_unique {v : universe} {H : Type v} [group H] {f : S → H} {g : G →* H} :
  g ∘ incl = f → g = lift f)

[Reid Barton]

No, this universal property example I understand and it seems hard but it sounded like the things Johan wanted might be easy.

[Adam Topaz]

Oh, then I misunderstood what the goal was.

[Mario Carneiro]

you can get reasonably close to a general theory using

class is_free_group_lift (G : Type u) (S : Type u) [group G] (incl : S → G)
  {H : Type v} [group H] (f : S → H) :=
(lift : G →* H)
(lift_comp_incl : lift ∘ incl = f)
(lift_unique {g : G →* H} : g ∘ incl = f → g = lift)

[Adam Topaz]

Oh interesting.

[Adam Topaz]

But of course this wouldn't give a specification of the free group.

[Mario Carneiro]

no but I'm not trying to do that, I'm trying to do everything a specification of the free group would do

[Mario Carneiro]

anyway we know how to specify free groups, you can just restrict to universe u and that works because free groups have some presentability property

[Mario Carneiro]

you can always say "I wish my foundations were more expressive than they are, because they miss <use case X>", that's godel incompleteness

[Reid Barton]

Right, the fact that you can't directly state what I called the "Universal property" is kind of annoying, but in specific cases you can find alternative definitions (e.g., by restricting the universe to an appropriate one) and then prove an "improved" eliminator which removes the universe restriction.

[Mario Carneiro]

My contention above is actually that you can use is_free_group_lift to work with the unreduced is_free_group predicate by referring to it obliquely

[Reid Barton]

For example in your original is_free_group, if we replace v by u (since we know the free group construction doesn't increase the universe level, this should be fine), then the type of is_free_group.lift is something like Pi (G : Type u) (S : Type u) [group G] [is_free_group G S] {H : Type u} [group H] (f : S -> H) : G ->* H, but we can define a better projection with the type Pi (G : Type u) (S : Type u) [group G] [is_free_group G S] {H : Type v} [group H] (f : S -> H) : G ->* H.

[Reid Barton]

And for the construction side, obviously it's fine to only have to pass the fields in in the special case v = u.

[Johan Commelin]

I think for every foo in one, mul, monoid, ring, we have about 100 lines of quasi-consistent api for foo_hom (and linear_map and alg_hom maybe, although they depend on R), and then another 100 lines for foo_equiv.

[Mario Carneiro]

so let's automate it

[Johan Commelin]

But these APIs are currently not all homogeneous, there are gaps all over the place.

[Johan Commelin]

Our only hope is that Yury will refactor them....

[Johan Commelin]

We want ext, ext_iff, coe, coe_injective, funext, congr_arg, congr_fun, coe_mk, and another 10 common lemmas

[Mario Carneiro]

It would be nice to have a framework for writing entire theory templates that will be multiply instantiated

[Johan Commelin]

id, comp, id_comp, comp_id, comp_assoc, id_apply, comp_apply

[Mario Carneiro]

those lemmas are all inputs to the category theory though, you get no help in proving them

[Reid Barton]

I don't think abstracting over the category is really viable anyways when using the style of unbundled objects and arrows that specify which structure they preserve

[Johan Commelin]

Not all of them are input, and some of them the automation should be able to guess

[Reid Barton]

I mean, I guess it might be but it's not the way the category theory library is set up at least

[Mario Carneiro]

it's certainly viable for meta code to abstract over the category

[Mario Carneiro]

even if it's a large/universe polymorphic category

[Reid Barton]

Right, I meant trying to prove the theorems like comp_assoc for all the variants like ->* simultaneously (or even making them all instances of the same type class or whatever).

[Mario Carneiro]

it does seem like a good idea to focus on the concrete category case though, because almost all our examples are of that form

[Reid Barton]

By simultaneously I mean in a single Lean definition

[Adam Topaz]

I feel like we're going back to all those discussions about universal algebra ;)

[Reid Barton]

Yay!

[Mario Carneiro]

didn't someone write a program that would do some of this? Subgroups and submonoids and other subthings?

[Adam Topaz]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Free.20stuff/near/209873309

[Mario Carneiro]

Clearly a framework for doing this in a more ergonomic way would be good

meta def homomorphism_comp (struct_name : name) : tactic declaration :=
do (params, fields) ← get_parameters_and_data_fields struct_name,
   let base_type := params.head,
   let struct_u : expr :=  expr.const struct_name [level.param `u],
   let struct_v : expr :=  expr.const struct_name [level.param `v],
   let struct_w : expr :=  expr.const struct_name [level.param `w],
   α ← mk_local' `α binder_info.implicit (sort (level.succ (level.param `u))),
   ia ← mk_local' `ia binder_info.inst_implicit (struct_u α),
   β ← mk_local' `β binder_info.implicit (sort (level.succ (level.param `v))),
   ib ← mk_local' `ib binder_info.inst_implicit (struct_v β),
   γ ← mk_local' `γ binder_info.implicit (sort (level.succ (level.param `w))),
   ic ← mk_local' `ic binder_info.inst_implicit (struct_w γ),
   f ← mk_local' `f binder_info.implicit (pi `_x binder_info.default α β),
   g ← mk_local' `g binder_info.implicit (pi `_x binder_info.default β γ),
   let hom_name := mk_simple_name (string.append struct_name.to_string "_homomorphism"),
   let hom_constr_name := hom_name <.> "mk",
   hom_f ← mk_app hom_name [α, β, ia, ib, f],
   hom_g ← mk_app hom_name [β, γ, ib, ic, g],
   hf ← mk_local' `hf binder_info.default hom_f,
   hg ← mk_local' `hg binder_info.default hom_g,
   compos ← mk_mapp `function.comp [none, none, none, g, f],
   stmt ← mk_app hom_name [α, γ, ia, ic, compos],
   let field_numbers := list.range fields.length,
   let fields_enum := list.zip fields field_numbers,
   compatibilities ← fields_enum.mmap
    (λ field_enum, homomorphism_comp_part struct_name base_type α β γ ia ib ic f g hf hg
                    field_enum.fst field_enum.snd fields_enum.length),
   constr ← mk_mapp hom_constr_name [some α, some γ, some ia, some ic, some compos],
   let body := expr.app_of_list constr compatibilities,
   let decl_body := expr.lambdas [α, β, γ, ia, ib, ic, f, g, hf, hg] body,
   let decl_type := expr.pis [α, β, γ, ia, ib, ic, f, g, hf, hg] stmt,
   let decl_name := mk_simple_name (string.append struct_name.to_string "_homomorphism_comp"),
   return $ declaration.thm decl_name (collect_univ_params decl_type) decl_type (task.pure decl_body)
-- for any transitive target? eq, if, iff, ...

[Mario Carneiro]

One possibility, similar to to_additive, would be to write a sort of "sample definition" and extract the template to instantiate from it, changing the names of constants and possibly applying a substitution but otherwise keeping things as is

[Johan Commelin]

@Cyril Cohen How hard is it to tie your algebra framework into Lean?

[Reid Barton]

Mario Carneiro said:

One possibility, similar to to_additive, would be to write a sort of "sample definition" and extract the template to instantiate from it, changing the names of constants and possibly applying a substitution but otherwise keeping things as is

I believe you'll find that such a tool already exists and is known as "the C preprocessor" :upside_down:

[Reid Barton]

I guess stuff like "preserves the algebraic structure" needs to iterate over a variable number of operations (e.g. +, * or both)

[Johan Commelin]

But the proof of ext_iff doesn't care about algebraic structure. And neither does comp_assoc, nor does comp_id or id_apply.

[Johan Commelin]

lemma one_hom.to_fun_eq_coe
lemma one_hom.coe_mk
lemma one_hom.coe_inj
lemma one_hom.ext
lemma one_hom.ext_iff
lemma one_hom.id_apply
lemma one_hom.comp_apply
lemma one_hom.comp_assoc
lemma one_hom.cancel_right
lemma one_hom.cancel_left
lemma one_hom.comp_id
lemma one_hom.id_comp

this is what I extracted about one_homs

The proofs don't use any properties of one_hom, except that it behaves like a function.
It's all rfl or cases, cases, congr or some generic logic lemmas.

[Johan Commelin]

The list is incomplete, because things like funext and congr_arg are missing.

[Reid Barton]

Right, so while I think it's probably better to autogenerate these lemmas at the same time as we autogenerate the rest of the theory of has_ones and sub_has_ones and so on, I claim you don't need any fancy universe polymorphism to implement one_hom.comp_assoc, say, in terms of ingredients that say that "taking the underlying function" is injective and commutes with composition.

[Reid Barton]

I'm not really sure, though.

[Eric Wieser]

Could those particular lemmas be written in terms of a has_to_fun typeclass?

[Eric Wieser]

Which provides has_coe_to_fun in term of the member

[Reid Barton]

Right, I would just start with things like class has_comp (a b : Type) (c : out_param Type) and compatibility classes and see whether that's good enough

[Adam Topaz]

So I'm trying something like this:

import tactic

variables (hom : Π (α : Type*) (β : Type*), Type*)

class has_faithful_coe_to_fun :=
(coe {α β} : hom α β → α → β)
(is_faithful {α β} {f g : hom α β} : coe f = coe g → f = g)

namespace has_faithful_coe_to_fun

variable [has_faithful_coe_to_fun hom]

instance {α β} : has_coe_to_fun (hom α β) := ⟨λ f, α → β,λ f, coe f⟩

@[ext]
lemma ext {α β} (f g : hom α β) : ⇑f = g → f = g := λ h, is_faithful h

end has_faithful_coe_to_fun

[Adam Topaz]

But I'm getting an error at ext saying only constants and Pi types are supported: hom α β.

[Mario Carneiro]

Reid Barton said:

Mario Carneiro said:

One possibility, similar to to_additive, would be to write a sort of "sample definition" and extract the template to instantiate from it, changing the names of constants and possibly applying a substitution but otherwise keeping things as is

I believe you'll find that such a tool already exists and is known as "the C preprocessor" :upside_down:

You know, we have something that is just as flexible/hackish as the C preprocessor: emit_code_here

[Mario Carneiro]

that's definitely one way to make theory templates, just do string replacement in a big code block in quotes

[Mario Carneiro]

plus, unlike the tactic approach, it actually lets you write defs that are just as good as the real thing

[Adam Topaz]

How do you use it? Can I just write the following?

run_cmd emit_code_here "def foo := 1"

[Johan Commelin]

Can we use this: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Generate.20homomorphism.20types.20for.20algebraic.20structures/ ?

[Mario Carneiro]

huh, I guess we need a run_parser command to make this easier

[Adam Topaz]

There must be some tactic unit that takes a parser and runs it no?

[Adam Topaz]

I have absolutely no idea what I'm doing... Can I make this work?

@[user_command]
meta def add_thing (_ : interactive.parse $ lean.parser.tk "add_thing") : lean.parser unit :=
do s ← lean.parser.ident,
  lean.parser.emit_code_here (to_string s)

[Reid Barton]

import tactic.core

@[user_command]
meta def add_thing (_ : interactive.parse $ lean.parser.tk "add_thing") : lean.parser unit :=
do s ← lean.parser.ident,
  lean.parser.emit_code_here (to_string s)
.

add_thing «#check 5»

[Adam Topaz]

Oh, the . is necessary?

[Reid Barton]

Well add_thing isn't a user command until the declaration ends, and if add_thing is not a user command then writing it will not end the declaration.

[Mario Carneiro]

import tactic.basic

open tactic lean.parser interactive interactive.types
@[user_command] meta def run_parser_cmd (_ : parse $ tk "run_parser") : lean.parser unit :=
do e ← lean.parser.pexpr 0,
  e ← tactic.to_expr e,
  p ← eval_expr (lean.parser unit) e,
  p.

run_parser emit_code_here "def foo := 1"

#print foo

[Reid Barton]

You could also put any other command in between.

[Adam Topaz]

Like I said, I really had no idea what I was doing. That's the first piece of meta code I've even tried to write.

[Reid Barton]

I don't know if it's what you intended but I'm amused at the idea of writing entire Lean definitions inside «...».

[Mario Carneiro]

oh, you are using ident quoting? That's an interesting way to get highlighting

[Adam Topaz]

It's not highlighting in vscode

[Reid Barton]

it doesn't give the correct highlighting in emacs though, does it work well in ...

[Mario Carneiro]

it also doesn't work with newlines apparently

[Reid Barton]

ok well at least it works in Zulip! :octopus:

[Reid Barton]

oh, no newlines is bad

[Mario Carneiro]

run_parser emit_code_here «
  def foo := 1
»
-- error: illegal character in escaped identifier

[Reid Barton]

I don't suppose there's a parser for an entire top-level command?

[Mario Carneiro]

this also doesn't seem to work:

run_parser emit_code_here "
  def foo := 1
"

something funny happens when the last " is not indented

[Mario Carneiro]

there is

[Mario Carneiro]

command_like

[Reid Barton]

can you get the source string out?

[Reid Barton]

meta constant command_like : parser unit

[Mario Carneiro]

no, it executes on the spot

[Reid Barton]

doesn't seem entirely helpful

[Reid Barton]

ah, I see

[Mario Carneiro]

it's actually the way emit_code_here works

[Mario Carneiro]

it's just with_input command_like

[Reid Barton]

It would be slick if instead of doing any quoting at all like foo "def ...", you could just write foo def ...

[Eric Wieser]

Anyone have any idea why the faithful_has_coe_to_fun a little ways above didn't work? It seems unfortunate to have to resort to code generation to define basic stuff about morphisms, where we don't have to do so for structures

[Adam Topaz]

Eric Wieser said:

Anyone have any idea why the faithful_has_coe_to_fun a little ways above didn't work? It seems unfortunate to have to resort to code generation to define basic stuff about morphisms, where we don't have to do so for structures

I think it has to do with the @[ext] attribute itself.

[Reid Barton]

Do you mean the error about ext?

[Reid Barton]

ext expects the lemmas to have a certain form, kind of like simp

[Mario Carneiro]

hom is a variable, not a constant

[Eric Wieser]

Ah, so we'd need code generation at least for populating ext attributes

[Reid Barton]

Or we could change how ext works. But I think doing code generation is preferable anyways.

[Mario Carneiro]

yeah, right now this string interpolation approach seems better than alternatives, even for the more complex use cases with a variable number of operations

[Mario Carneiro]

in fact it might not even be horrible looking if you use format!

[Mario Carneiro]

which I don't find enough uses for

[Mario Carneiro]

run_parser do
  let foo := "bar",
  emit_code_here (format!"
    def {foo} := 1
    ").to_string

#print bar

[Adam Topaz]

Does lean have something like python's multiline strings with """?

[Adam Topaz]

Or can I just write multiline strings with "?

[Adam Topaz]

Cool. It's strange about the indentation of ", in Mario's comment above.

[Adam Topaz]

Looks like it's about the final newline.
E.g. this works

def str : string :=
"
def foo := 1
def bar := 2"

run_parser emit_code_here str

[Adam Topaz]

But this doesn't (or at least it looks like run_parser loops forever)

def str : string :=
"
def foo := 1
def bar := 2
"

run_parser emit_code_here str

[Mario Carneiro]

run_parser PR'd in #4745

[Mario Carneiro]

run_parser emit_code_here "\n" -- loops

[Mario Carneiro]

run_parser do with_input command_like "\n", pure () -- no loop

[Adam Topaz]

I guess we could make a new function emit_code_here' which removes trailing newlines

[Mario Carneiro]

Oh I see:

meta def emit_code_here : string → lean.parser unit
| str := do left ← emit_command_here str,
            if left.length = 0 then return ()
            else emit_code_here left

this has no termination condition

[Mario Carneiro]

It should check that left.length < str.length

[Mario Carneiro]

#4746

[Patrick Massot]

Already failing CI...

[Mario Carneiro]

I don't always test my code, but when I do, I do it in production.

-- Mario's shirt

[Mario Carneiro]

Hm, I wasn't really planning on using run_parser to actually parse something in the source, but it is possible:

run_parser do -- 4
  tk ".",
  e ← texpr,
  ↑(to_expr e >>= eval_expr ℕ >>= trace)
.
2 + 2

[Mario Carneiro]

unfortunately parsers can't parse command keywords like def so this isn't quite what reid was looking for

[Adam Topaz]

This is fun!

def monoid_stuff : list (string × nat) := [("mul",2),("one",0)]

def mk_op_str_aux (s : string) : nat → string
| nat.zero := s
| (nat.succ n) := s ++ " → " ++ (mk_op_str_aux n)

def mk_op_str (nn : string) (s : string) (n : nat) : string := nn ++ " : " ++ mk_op_str_aux s n

def mk_class_str_aux (nn : string) : list (string × nat) → string
| list.nil := ""
| (list.cons hd tl) := "\n( " ++ mk_op_str hd.1 nn hd.2 ++ " )" ++ mk_class_str_aux tl

def mk_class_str (class_name : string) : list (string × nat) → string :=
λ ls, "class " ++ class_name ++ " (α : Type*) :=" ++ mk_class_str_aux "α" ls

run_parser emit_code_here (mk_class_str "raw_monoid" monoid_stuff)

#print raw_monoid

[Adam Topaz]

Ah, but I get a "deep recursion" error if I try to define a typeclass with a $10000$-ary operation.

[Adam Topaz]

$3679$-ary operations are okay though

[Reid Barton]

Well, hopefully Lean 4 will let us supoport 3680-ary operations

[Mario Carneiro]

It's a bit slow for some reason, but this works:

def monoid_stuff : list (string × nat) := [("mul",10000),("one",0)]

def arity (α : Type*) : nat → Type*
| nat.zero := α
| (nat.succ n) := α → arity n

meta def mk_class_str_aux (s : string) : list (string × nat) → string
| list.nil := ""
| (list.cons (nn, n) tl) :=
  (format!"\n({nn} : arity {s} {to_string n})").to_string ++ mk_class_str_aux tl

meta def mk_class_str (class_name : string) : list (string × nat) → string :=
λ ls, "class " ++ class_name ++ " (α : Type*) :=" ++ mk_class_str_aux "α" ls

run_parser emit_code_here (mk_class_str "raw_monoid" monoid_stuff)

#print raw_monoid

[Adam Topaz]

Oh interesting. So the the deep recursion is only a problem when you generate a large string, and not when you generate a long type expression

[Adam Topaz]

This arity type is in mathlib somewhere...

[Mario Carneiro]

no, the deep recursion isn't for the string, it's for the parsing of the notation A -> A -> A -> ... -> A

[Adam Topaz]

Oh ok

[Adam Topaz]

docs#arity

[Mario Carneiro]

although I think that you can also get into deep recursion trouble when constructing the strings too

[Mario Carneiro]

or at least quadratic behavior

[Mario Carneiro]

you should probably stick to the iterated arrows instead of arity though, since it requires unfolding at point of use

[Mario Carneiro]

Ooh, I had another idea...

[Mario Carneiro]

def monoid_stuff : list (string × nat) := [("mul",10000),("one",0)]

meta def arity (α : pexpr) (n : nat) : tactic unit :=
do α ← to_expr α,
  tactic.exact $ (expr.pi `_x binder_info.default α)^[n] α

meta def mk_class_str_aux (s : string) : list (string × nat) → string
| list.nil := ""
| (list.cons (nn, n) tl) :=
  "\n(" ++ nn ++ " : by arity ```(" ++ s ++ ") " ++ to_string n ++ ")" ++ mk_class_str_aux tl

meta def mk_class_str (class_name : string) : list (string × nat) → string :=
λ ls, "class " ++ class_name ++ " (α : Type*) :=" ++ mk_class_str_aux "α" ls

run_parser emit_code_here (mk_class_str "raw_monoid" monoid_stuff)

#print raw_monoid

[Mario Carneiro]

it times out, unfortunately. I think it's getting stuck somewhere in the aux defs of the structure

[Mario Carneiro]

it's a metametametaprogram

[Adam Topaz]

That's cool, even just to be able to write

def foo := by arity ```(ℕ) 3
#print fo

[Mario Carneiro]

it makes the parser's job easier here, since there are no long chains in the source text

[Mario Carneiro]

I think lean still has to go through them all when dealing with the exprs later in elaboration and typechecking

[Adam Topaz]

def foo := by arity ```(ℕ) 24525

Lean is happy with that, but not with $24526$.

[Mario Carneiro]

to be fair, if you have a structure with a 24526-ary operation then perhaps you would rather generalize to n-ary

[Adam Topaz]

Ping @Colter MacDonald

[Johan Commelin]

Type theory/logic noob here. We currently cannot state universe restrictions. And I understand that this is a box of pandora. We want equality of expressions of universe levels to be decidable. However, since the theory of linearly ordered abelian groups is decidable, I was wondering whether it is possible to add u < v constraints to the theory of universe levels and still have a system that works well in practice.
I guess this would mean that the kernel might need to run some version of omega during typechecking, which is maybe not very performant/practical. On the other hand, 99% of the time, we would be inside the current fragment of universe logic. So maybe it can be made to work.

Being able to write u < v or u ≤ v constraints would be really useful for statements in category theory.

[Floris van Doorn]

We basically can already write u ≤ v and u < v because u ≤ max u w and u < max (u+1) w so you can let v = max u w or v = max (u+1) w.

[Johan Commelin]

Yes, that's a very good point. But these expressions can potentially get quite complicated, right? This is the approach that we recently started using in the category theory library. We'll have to find out how far we can push it in practice.

[Kevin Buzzard]

Didn't we already see this failing earlier this week? Lean failed to unify max u v = max v ?m_1