I see we have a stream here about constructive reals/analysis. Would it be appropriate for a general stream about constructive math as it can be implemented in coq?

It would be fine with me to rename the stream and just use descriptive topics, analysis/algebra/...

Do you have specific topics in mind?

Working on putting together an ordinal type as equivalence classes of well-ordered types, have some questions about how to define the well-order on the ordinals themselves and what we can prove about the ordinals.

Have a look at the HoTT book

All the math in the "regular" mathcomp library is constructive, and in particular they recently added work on order theory

non-constructive libraries generally flag up their axiom use clearly (and live in separate streams, in some cases). Hence, I don't think we need a general constructive math stream. But with more mathematical interest, there could indeed be dedicated streams to algebra, topology, etc.

My personal preference would be to just have streams about a topic, not to commit to an axiom. Sure, you may find in there ideas/proofs that don't work for you, but I have the feeling we have more to gain in keeping things together rather than separating them.

I know that some topics are very different if you tie your hands w.r.t. an axiom (eg Analysis) but it is not clear what you gain by the split. If you have a thousands messages per day, maybe it becomes a necessity... until then, I would suggest just keep things mixed.

Sorry, I'm confused. If I wanted to ask something like:

Suppose we defined o₁ ≺ o₂ on the ordinals to be inhabited whenever there is some x : o₂ such that o₁ is order-isomorphic to the initial segment of o₂ directly preceding x (this is, I believe, equivalent to the definition in the HoTT book). Am I right in thinking that I could in principle prove o₁ isomorphic to some initial segment of o₂ that has some upper bound (but not necessarily a known

leastupper bound) and not be able to prove o₁ ≺ o₂?

Would that be appropriate on any stream here? If so, which?

since you are not mentioning Coq, and this is not directly related to constructive analysis, it falls in this stream (Miscellaneous)

we have many mathematically inclined users here, but most discussions are focused on Coq and/or its theory and libraries. There is a whole HoTT Zulip for pure theory (and also implementation) related to HoTT: https://hott.zulipchat.com/

It's fine to create new streams, but only if you have sufficiently many people interested to join it, otherwise you will just get a ghost town (since people are not subscribed to new streams by default).

And it's also always fine to ask any question anywhere since if it is not in the right place, it is easy to move it.

arguably we already have too many streams, e.g., I would consolidate UI and VsCoq

UI was an attempt at making UI devs talk to each other and to Coq devs. It didn't work. However, it would be a problem IMHO to have a stream dedicated to all user interfaces and overcrowded by users of one specific UI.

Last updated: Jun 01 2023 at 12:01 UTC