## Stream: general

### Topic: universes

#### Phiroc (Apr 06 2020 at 11:08):

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 (Apr 06 2020 at 11:14):

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

#### Mario Carneiro (Apr 06 2020 at 11:15):

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 (Oct 20 2020 at 06:30):

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

#### Mario Carneiro (Oct 20 2020 at 06:30):

yes, it increases the axiomatic strength

#### Johan Commelin (Oct 20 2020 at 06:31):

That's the only problem?

#### Johan Commelin (Oct 20 2020 at 06:31):

Sounds like a good thing to me :grinning:

#### Mario Carneiro (Oct 20 2020 at 06:32):

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

#### Johan Commelin (Oct 20 2020 at 06:32):

Well, it might solve my problems

#### Mario Carneiro (Oct 20 2020 at 06:32):

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 (Oct 20 2020 at 06:33):

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

#### Mario Carneiro (Oct 20 2020 at 06:33):

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

#### Johan Commelin (Oct 20 2020 at 06:34):

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 (Oct 20 2020 at 06:35):

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 (Oct 20 2020 at 06:35):

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 (Oct 20 2020 at 06:36):

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

#### Johan Commelin (Oct 20 2020 at 06:36):

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

#### Johan Commelin (Oct 20 2020 at 06:36):

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

#### Mario Carneiro (Oct 20 2020 at 06:36):

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

#### Johan Commelin (Oct 20 2020 at 06:37):

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

#### Mario Carneiro (Oct 20 2020 at 06:38):

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

Why?

#### Mario Carneiro (Oct 20 2020 at 06:39):

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 (Oct 20 2020 at 06:40):

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

#### Mario Carneiro (Oct 20 2020 at 06:40):

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

#### Mario Carneiro (Oct 20 2020 at 06:41):

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

#### Mario Carneiro (Oct 20 2020 at 06:41):

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

#### Mario Carneiro (Oct 20 2020 at 06:42):

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

#### Reid Barton (Oct 20 2020 at 13:50):

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

#### Reid Barton (Oct 20 2020 at 13:51):

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

#### Reid Barton (Oct 20 2020 at 14:01):

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 (Oct 20 2020 at 15:39):

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

#### Mario Carneiro (Oct 20 2020 at 15:41):

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

#### Kevin Buzzard (Oct 20 2020 at 16:58):

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 (Oct 20 2020 at 17:48):

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 (Oct 20 2020 at 17:51):

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 (Oct 20 2020 at 17:52):

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 (Oct 20 2020 at 17:53):

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

#### Reid Barton (Oct 20 2020 at 17:58):

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 (Oct 20 2020 at 17:59):

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 (Oct 20 2020 at 18:01):

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 (Oct 20 2020 at 18:15):

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 (Oct 20 2020 at 18:24):

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 (Oct 20 2020 at 18:30):

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 (Oct 20 2020 at 18:31):

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 (Oct 20 2020 at 18:34):

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 (Oct 20 2020 at 18:34):

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 (Oct 20 2020 at 18:36):

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 (Oct 20 2020 at 18:36):

But still it can be a property, right?

#### Patrick Massot (Oct 20 2020 at 18:37):

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

#### Reid Barton (Oct 20 2020 at 18:39):

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 (Oct 20 2020 at 18:40):

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

#### Reid Barton (Oct 20 2020 at 18:41):

The problem with doing category theory in ZFC?

#### Patrick Massot (Oct 20 2020 at 18:41):

The problem with defining stuff using universal properties

#### Patrick Massot (Oct 20 2020 at 18:43):

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 (Oct 20 2020 at 18:45):

... 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 (Oct 20 2020 at 18:45):

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 (Oct 20 2020 at 18:46):

What do you mean with "any"?

#### Johan Commelin (Oct 20 2020 at 18:46):

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

#### Reid Barton (Oct 20 2020 at 18:46):

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 (Oct 20 2020 at 18:47):

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

#### Reid Barton (Oct 20 2020 at 18:48):

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 (Oct 20 2020 at 18:49):

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

#### Patrick Massot (Oct 20 2020 at 18:49):

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 (Oct 20 2020 at 18:49):

You can state that, and even prove it.

#### Reid Barton (Oct 20 2020 at 18:50):

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 (Oct 20 2020 at 18:52):

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 (Oct 20 2020 at 18:53):

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

#### Patrick Massot (Oct 20 2020 at 18:56):

So what is impossible with ZFC + universes then?

#### Reid Barton (Oct 20 2020 at 19:02):

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 (Oct 20 2020 at 19:03):

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 (Oct 20 2020 at 19:05):

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

#### Patrick Massot (Oct 20 2020 at 19:05):

What is Con(ZFC)?

consistency?

#### Reid Barton (Oct 20 2020 at 19:06):

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

#### Reid Barton (Oct 20 2020 at 19:07):

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

#### Reid Barton (Oct 20 2020 at 19:10):

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 (Oct 20 2020 at 19:12):

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

#### Adam Topaz (Oct 20 2020 at 20:26):

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 (Oct 21 2020 at 01:11):

@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 (Oct 21 2020 at 01:21):

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 (Oct 21 2020 at 13:29):

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

that's right

#### Mario Carneiro (Oct 21 2020 at 13:33):

you can't apply stone_cech_extend directly

#### Adam Topaz (Oct 21 2020 at 13:33):

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

#### Mario Carneiro (Oct 21 2020 at 13:33):

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

#### Adam Topaz (Oct 21 2020 at 13:34):

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 (Oct 21 2020 at 13:35):

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 (Oct 21 2020 at 13:35):

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

#### Adam Topaz (Oct 21 2020 at 13:37):

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

#### Mario Carneiro (Oct 21 2020 at 13:38):

no, it depends on the universal property

#### Mario Carneiro (Oct 21 2020 at 13:38):

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

#### Adam Topaz (Oct 21 2020 at 13:38):

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

#### Reid Barton (Oct 21 2020 at 13:39):

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 (Oct 21 2020 at 13:39):

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

#### Mario Carneiro (Oct 21 2020 at 13:41):

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

#### Adam Topaz (Oct 21 2020 at 13:41):

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 (Oct 21 2020 at 13:41):

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

#### Reid Barton (Oct 21 2020 at 13:42):

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

#### Adam Topaz (Oct 21 2020 at 13:44):

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 (Oct 21 2020 at 13:44):

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

#### Mario Carneiro (Oct 21 2020 at 13:45):

@_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 (Oct 21 2020 at 13:47):

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

#### Mario Carneiro (Oct 21 2020 at 13:47):

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 (Oct 21 2020 at 13:48):

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

#### Mario Carneiro (Oct 21 2020 at 13:48):

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

#### Reid Barton (Oct 22 2020 at 17:09):

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

#### Reid Barton (Oct 22 2020 at 17:09):

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

#### Mario Carneiro (Oct 22 2020 at 17:10):

I think specifying universal properties?

#### Johan Commelin (Oct 22 2020 at 17:10):

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 (Oct 22 2020 at 17:10):

That's what my motivation was

#### Johan Commelin (Oct 22 2020 at 17:10):

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

#### Mario Carneiro (Oct 22 2020 at 17:11):

what is a bundled hom in this context?

#### Johan Commelin (Oct 22 2020 at 17:11):

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 (Oct 22 2020 at 17:11):

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

#### Mario Carneiro (Oct 22 2020 at 17:11):

equiv is a universe polymorphic bundled hom

#### Johan Commelin (Oct 22 2020 at 17:11):

Mario Carneiro said:

what is a bundled hom in this context?

It is bundled_hom in the sense of docs#bundled_hom

Snap!

#### Reid Barton (Oct 22 2020 at 17:12):

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

#### Adam Topaz (Oct 22 2020 at 17:13):

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

#### Mario Carneiro (Oct 22 2020 at 17:14):

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 (Oct 22 2020 at 17:14):

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 (Oct 22 2020 at 17:14):

You can't even define them with two universe variables

#### Johan Commelin (Oct 22 2020 at 17:14):

Because you need id

#### Mario Carneiro (Oct 22 2020 at 17:14):

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

#### Adam Topaz (Oct 22 2020 at 17:14):

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 (Oct 22 2020 at 17:15):

oh bundled_hom isn't a bundled hom

#### Johan Commelin (Oct 22 2020 at 17:15):

But nevertheless ring_hom.id is a thing

#### Johan Commelin (Oct 22 2020 at 17:15):

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 (Oct 22 2020 at 17:15):

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

type in type

#### Adam Topaz (Oct 22 2020 at 17:16):

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

#### Reid Barton (Oct 22 2020 at 17:16):

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

#### Mario Carneiro (Oct 22 2020 at 17:18):

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

#### Mario Carneiro (Oct 22 2020 at 17:18):

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

#### Reid Barton (Oct 22 2020 at 17:19):

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

#### Mario Carneiro (Oct 22 2020 at 17:20):

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

#### Mario Carneiro (Oct 22 2020 at 17:21):

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

#### Reid Barton (Oct 22 2020 at 17:22):

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 (Oct 22 2020 at 17:22):

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

#### Mario Carneiro (Oct 22 2020 at 17:23):

like perhaps proving theorems generic over different kinds of bundled homs

#### Reid Barton (Oct 22 2020 at 17:23):

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

#### Mario Carneiro (Oct 22 2020 at 17:23):

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

#### Reid Barton (Oct 22 2020 at 17:23):

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

#### Mario Carneiro (Oct 22 2020 at 17:25):

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 (Oct 22 2020 at 17:25):

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 (Oct 22 2020 at 17:25):

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 (Oct 22 2020 at 17:26):

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

#### Adam Topaz (Oct 22 2020 at 17:27):

Oh, then I misunderstood what the goal was.

#### Mario Carneiro (Oct 22 2020 at 17:31):

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)


Oh interesting.

#### Adam Topaz (Oct 22 2020 at 17:34):

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

#### Mario Carneiro (Oct 22 2020 at 17:35):

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 (Oct 22 2020 at 17:36):

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 (Oct 22 2020 at 17:37):

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 (Oct 22 2020 at 17:37):

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 (Oct 22 2020 at 17:39):

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 (Oct 22 2020 at 17:39):

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 (Oct 22 2020 at 17:40):

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 (Oct 22 2020 at 17:40):

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 (Oct 22 2020 at 17:41):

so let's automate it

#### Johan Commelin (Oct 22 2020 at 17:41):

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

#### Johan Commelin (Oct 22 2020 at 17:41):

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

#### Johan Commelin (Oct 22 2020 at 17:42):

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

#### Mario Carneiro (Oct 22 2020 at 17:42):

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

#### Johan Commelin (Oct 22 2020 at 17:42):

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

#### Mario Carneiro (Oct 22 2020 at 17:43):

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

#### Reid Barton (Oct 22 2020 at 17:44):

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 (Oct 22 2020 at 17:45):

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

#### Reid Barton (Oct 22 2020 at 17:45):

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

#### Mario Carneiro (Oct 22 2020 at 17:45):

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

#### Mario Carneiro (Oct 22 2020 at 17:46):

even if it's a large/universe polymorphic category

#### Reid Barton (Oct 22 2020 at 17:46):

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 (Oct 22 2020 at 17:47):

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 (Oct 22 2020 at 17:47):

By simultaneously I mean in a single Lean definition

#### Adam Topaz (Oct 22 2020 at 17:47):

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

Yay!

#### Mario Carneiro (Oct 22 2020 at 17:48):

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

#### Adam Topaz (Oct 22 2020 at 17:49):

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

#### Mario Carneiro (Oct 22 2020 at 17:52):

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 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 (Oct 22 2020 at 17:55): 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 (Oct 22 2020 at 17:55): @Cyril Cohen How hard is it to tie your algebra framework into Lean? #### Reid Barton (Oct 22 2020 at 18:00): 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 (Oct 22 2020 at 18:02): I guess stuff like "preserves the algebraic structure" needs to iterate over a variable number of operations (e.g. +, * or both) #### Johan Commelin (Oct 22 2020 at 18:03): 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 (Oct 22 2020 at 18:13): 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 (Oct 22 2020 at 18:14): The list is incomplete, because things like funext and congr_arg are missing. #### Reid Barton (Oct 22 2020 at 18:20): 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 (Oct 22 2020 at 18:21): I'm not really sure, though. #### Eric Wieser (Oct 22 2020 at 18:23): Could those particular lemmas be written in terms of a has_to_fun typeclass? #### Eric Wieser (Oct 22 2020 at 18:24): Which provides has_coe_to_fun in term of the member #### Reid Barton (Oct 22 2020 at 18:25): 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 (Oct 22 2020 at 18:28): 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 (Oct 22 2020 at 18:30): But I'm getting an error at ext saying only constants and Pi types are supported: hom α β. #### Mario Carneiro (Oct 22 2020 at 18:31): 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 (Oct 22 2020 at 18:32): that's definitely one way to make theory templates, just do string replacement in a big code block in quotes #### Mario Carneiro (Oct 22 2020 at 18:34): plus, unlike the tactic approach, it actually lets you write defs that are just as good as the real thing #### Adam Topaz (Oct 22 2020 at 18:35): How do you use it? Can I just write the following? run_cmd emit_code_here "def foo := 1"  #### Johan Commelin (Oct 22 2020 at 18:38): #### Mario Carneiro (Oct 22 2020 at 18:39): huh, I guess we need a run_parser command to make this easier #### Adam Topaz (Oct 22 2020 at 18:40): There must be some tactic unit that takes a parser and runs it no? #### Adam Topaz (Oct 22 2020 at 18:54): 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 (Oct 22 2020 at 18:57):

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 (Oct 22 2020 at 18:57): Oh, the . is necessary? #### Reid Barton (Oct 22 2020 at 18:58): 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 (Oct 22 2020 at 18:58): 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 (Oct 22 2020 at 18:59):

You could also put any other command in between.

#### Adam Topaz (Oct 22 2020 at 18:59):

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 (Oct 22 2020 at 18:59):

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 (Oct 22 2020 at 19:00):

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

#### Adam Topaz (Oct 22 2020 at 19:00):

It's not highlighting in vscode

#### Reid Barton (Oct 22 2020 at 19:01):

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

#### Mario Carneiro (Oct 22 2020 at 19:01):

it also doesn't work with newlines apparently

#### Reid Barton (Oct 22 2020 at 19:01):

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

#### Mario Carneiro (Oct 22 2020 at 19:01):

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


#### Reid Barton (Oct 22 2020 at 19:03):

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

#### Mario Carneiro (Oct 22 2020 at 19:03):

this also doesn't seem to work:

run_parser emit_code_here "
def foo := 1
"


something funny happens when the last " is not indented

there is

#### Mario Carneiro (Oct 22 2020 at 19:03):

command_like

#### Reid Barton (Oct 22 2020 at 19:03):

can you get the source string out?

#### Reid Barton (Oct 22 2020 at 19:04):

meta constant command_like : parser unit

#### Mario Carneiro (Oct 22 2020 at 19:04):

no, it executes on the spot

ah, I see

#### Mario Carneiro (Oct 22 2020 at 19:04):

it's actually the way emit_code_here works

#### Mario Carneiro (Oct 22 2020 at 19:05):

it's just with_input command_like

#### Reid Barton (Oct 22 2020 at 19:05):

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

#### Eric Wieser (Oct 22 2020 at 19:05):

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 (Oct 22 2020 at 19:06):

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 (Oct 22 2020 at 19:06):

Do you mean the error about ext?

#### Reid Barton (Oct 22 2020 at 19:06):

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

#### Mario Carneiro (Oct 22 2020 at 19:07):

hom is a variable, not a constant

#### Eric Wieser (Oct 22 2020 at 19:08):

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

#### Reid Barton (Oct 22 2020 at 19:08):

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

#### Mario Carneiro (Oct 22 2020 at 19:10):

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 (Oct 22 2020 at 19:10):

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

#### Mario Carneiro (Oct 22 2020 at 19:10):

which I don't find enough uses for

#### Mario Carneiro (Oct 22 2020 at 19:12):

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

#print bar


#### Adam Topaz (Oct 22 2020 at 19:18):

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

#### Adam Topaz (Oct 22 2020 at 19:19):

Or can I just write multiline strings with "?

#### Adam Topaz (Oct 22 2020 at 19:19):

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

#### Adam Topaz (Oct 22 2020 at 19:21):

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 (Oct 22 2020 at 19:21):

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 (Oct 22 2020 at 19:25):

run_parser PR'd in #4745

#### Mario Carneiro (Oct 22 2020 at 19:26):

run_parser emit_code_here "\n" -- loops


#### Mario Carneiro (Oct 22 2020 at 19:27):

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


#### Adam Topaz (Oct 22 2020 at 19:27):

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

#### Mario Carneiro (Oct 22 2020 at 19:28):

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 (Oct 22 2020 at 19:29):

It should check that left.length < str.length

#4746

#### Mario Carneiro (Oct 22 2020 at 19:47):

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

-- Mario's shirt

#### Mario Carneiro (Oct 22 2020 at 20:28):

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 (Oct 22 2020 at 20:30):

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

#### Adam Topaz (Oct 22 2020 at 20:57):

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 (Oct 22 2020 at 21:11):

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

#### Adam Topaz (Oct 22 2020 at 21:12):

$3679$-ary operations are okay though

#### Reid Barton (Oct 22 2020 at 21:13):

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

#### Mario Carneiro (Oct 22 2020 at 21:32):

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 (Oct 22 2020 at 21:34):

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 (Oct 22 2020 at 21:34):

This arity type is in mathlib somewhere...

#### Mario Carneiro (Oct 22 2020 at 21:35):

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

Oh ok

docs#arity

#### Mario Carneiro (Oct 22 2020 at 21:35):

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

#### Mario Carneiro (Oct 22 2020 at 21:37):

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

#### Mario Carneiro (Oct 22 2020 at 21:48):

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 (Oct 22 2020 at 21:49):

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

#### Mario Carneiro (Oct 22 2020 at 21:52):

it's a metametametaprogram

#### Adam Topaz (Oct 22 2020 at 21:53):

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

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


#### Mario Carneiro (Oct 22 2020 at 21:54):

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

#### Mario Carneiro (Oct 22 2020 at 21:55):

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

#### Adam Topaz (Oct 22 2020 at 21:57):

def foo := by arity (ℕ) 24525


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

#### Mario Carneiro (Oct 22 2020 at 21:59):

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

#### Adam Topaz (Oct 22 2020 at 23:36):

Ping @Colter MacDonald

Last updated: May 15 2021 at 23:13 UTC