Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: mathematics

Topic: Factorials in constructive mathematics

view this post on Zulip John Baez (Sep 17 2025 at 09:34):

@Martín Hötzel Escardó has a nice thread on Mathstodon about factorials in constructive mathematics, generalizing the formula

(n+1)!=n×n! (n+1)! = n \times n!

to homotopy types and indeed an arbitrary (∞,1)(\infty,1)-topos.

It's old, but I just looked at it again and I like it.

view this post on Zulip Joe Moeller (Sep 18 2025 at 00:03):

Surely you mean (n+1)!=(n+1)×n!(n+1)!=(n+1) \times n!

view this post on Zulip Mike Shulman (Sep 18 2025 at 04:25):

Or Γ(n+1)=n×Γ(n)\Gamma(n+1) = n \times \Gamma(n)...

view this post on Zulip John Baez (Sep 18 2025 at 11:07):

Yeah, fixed. It turns out Escardo's constructive analogue is

(X+1)!=(X+1)′×X! (X+1)! = (X+1)' \times X!

where for any set, or space, or homotopy type, A′A' is the set of isolated points of AA.