Shea Levy (Oct 27 2020 at 10:55): Shea Levy (Oct 27 2020 at 10:55):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?
Bas Spitters (Oct 27 2020 at 11:29):It would be fine with me to rename the stream and just use descriptive topics, analysis/algebra/...
Do you have specific topics in mind?
Shea Levy (Oct 27 2020 at 11:33):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.
Bas Spitters (Oct 27 2020 at 11:41):Have a look at the HoTT book
Karl Palmskog (Oct 27 2020 at 12:49):All the math in the "regular" mathcomp library is constructive, and in particular they recently added work on order theory
Karl Palmskog (Oct 27 2020 at 12:57):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.
Enrico Tassi (Oct 27 2020 at 13:05):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.
Enrico Tassi (Oct 27 2020 at 13:07):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.
Shea Levy (Oct 27 2020 at 14:00):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 least upper bound) and not be able to prove o₁ ≺ o₂?
Would that be appropriate on any stream here? If so, which?
Karl Palmskog (Oct 27 2020 at 14:01):since you are not mentioning Coq, and this is not directly related to constructive analysis, it falls in this stream (Miscellaneous)
Karl Palmskog (Oct 27 2020 at 14:03):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/
Théo Zimmermann (Oct 27 2020 at 14:09):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).
Théo Zimmermann (Oct 27 2020 at 14:09):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.
Karl Palmskog (Oct 27 2020 at 14:11):arguably we already have too many streams, e.g., I would consolidate UI and VsCoq
Théo Zimmermann (Oct 27 2020 at 14:13):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: Apr 19 2024 at 23:02 UTC