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: community: general

Topic: Workshop on AI proof assistants for ω-categories at ICM 2026

view this post on Zulip Caps (Jul 22 2026 at 14:40):

Today we are announcing:

A series of workshops on AI proof assistants (for ω-categories), as a satellite event of the ICM 2026 Congress of Mathematicians in Philadelphia and of the DubAI AI / MumbAI AI / ShanghAI AI weekly Saturday meetups, held both in-person and live online with 20,000+ professionals within the LastRevision.pro AI-calendar app:

https://LastRevision.pro/r/26202DLGJ19000
https://www.meetup.com/dubai-ai/events/315542036

Registration is not required (but there is an optional USD $500 donation for personalized support) and attendants discuss topics in free-format, as is usual for the Dubai / Mumbai / Shanghai AI weekly meetups.

APPENDIX:

I'll personally want to discuss with reviewers and contributors to these topics at the workshop:

view this post on Zulip Caps (Jul 22 2026 at 14:43):

Chat, what do you think of this claim, purely mathematically only:

https://github.com/hotdocx/emdash/blob/main/emdash2/emdash3_2.lp that the fundamental group of the circle is the integers `π₁(S¹) = ℤ`; more precisely: that the (higher inductive) category/type generated by a directed loop is equivalent to the natural numbers... other examples in the —book include the Eckmann-Hilton argument and that left-adjoints preserve weighted colimits by duality...

I think it means: fundamentals + belief...

APPENDIX:

The basic construction underneath the emdash kernel/book is the ω-categorial/directed dependent hom. For a category-valued family E : K ⊢ Cat where ⊢ denotes a functor category, and for internalized or fixed/external data x : K, u : E[x], emdash declares a displayed/fibred functor

homd_E(x,u) : Π(y : K^op), E[y^-] ⊢_[y] (Hom_K(x,y)^op ⊢ Cat)

Here ⊢_[y] is the mixed-variance displayed version of ⊢, and y^- marks that the E-argument occurs contravariantly. Its value at y, v : E[y], and f : x → y is Hom_{E[y]}(E[f](u),v)...

Thus, for a predicate

E : (Σ(y : Z), Hom_Z(x,y)) ⊢ Cat

and u : E((x,id_x)), fixed-source directed/arrow induction has the expected section

Ind_x(E,u) : Π a, E(a)

Ind_x(E,u)(y,p) = E(p)(u)

view this post on Zulip Kevin Carlson (Jul 22 2026 at 15:17):

It’s a simple and very well known computation. No idea what you might imagine it has to do with “fundamentals + belief.”

view this post on Zulip Caps (Jul 22 2026 at 16:17):

Kevin Carlson said:

It’s a simple and very well known computation. No idea what you might imagine it has to do with “fundamentals + belief.”

you mean "computation" on pencil + paper?

but you are right, my previous message was not clear enough, because I tried to "dumb it down" too much; I have now edited and updated it...

view this post on Zulip fosco (Jul 23 2026 at 07:32):

DubAI AI / MumbAI AI / ShanghAI AI weekly Saturday meetups

...The poor ChennAI AI is now wondering "and why not me?"

view this post on Zulip Caps (Jul 25 2026 at 00:59):

Would expect in this Zulip a "Ask Me/Codex Anything" technical debate, but replies so far are only cynical attempts at drama...

@Evan Patterson literally yesterday apparently had a lot to say on this topic at his Berkeley Seminar

https://youtu.be/mknZxNcn0Ho

except for his paying to my book https://github.com/hotdocx/emdash/blob/main/docs/emdash-book.pdf any review and contribution, lol

Anyway I was looking for an excuse/question to copy-paste this excerpt from the book:

The first concrete higher-inductive calculation declares a global, opaque, one-dimensional directed HIT rather than defining its hom as a word type or as the natural numbers:

constant WalkingEnd : Cat

base : Obj(WalkingEnd)
loop : Hom_WalkingEnd(base,base)

The whole-HIT recursor is then applied to the category universe Cat_cat, choosing the equality-local category ℕ as its base object and the successor endofunctor as its loop:

Code := rec_WalkingEnd(Cat_cat; ℕ, Succ)

Code[base] = ℕ
Code[loop] = Succ : ℕ ⊢ ℕ

These are computation rules for the base and loop constructors of the whole WalkingEnd HIT. Consequently, any based arrow p : Hom_WalkingEnd(base,x) acts through Code, and its action on zero defines the encoder:

encode_x(p) = Code[p](0)

The inverse direction is not obtained by inspecting p as a word. First define the powers of the directed loop and the based representable family:

power(0)   = id_base
power(n+1) = loop ∘ power(n)

Rep_base[x] = Hom_WalkingEnd(base,x)

The power functor and successor action are related by a directed loop-coherence transformation—the spiral:

spiral :
  Rep_base[loop] ∘ power
    ⇒
  power ∘ Succ

The contextual elimination rule for the whole HIT consumes Code, Rep_base, power, and spiral, producing one coherent decoder over every endpoint:

decodeᵈ :=
  indᵈ_WalkingEnd(Code, Rep_base, power, spiral)

decode_x : Obj(Code[x]) → Hom_WalkingEnd(base,x)
decode_base = power

norm_p :
  p → decode_x(encode_x(p))
  inside Hom_WalkingEnd(base,x)

Only after this directed normalization cell has been constructed does one-dimensionality turn it into equality. At the base, the two inverse calculations are:

power(encode_base(p)) = p
encode_base(power(n)) = n

Hom_WalkingEnd(base,base) ≃ ℕ
    (equivalence of underlying carriers)

Thus every based directed endomorphism is exactly one finite, nonnegative power of loop. The answer is ℕ rather than ℤ because direction matters: loop has no right inverse. The equivalence is obtained through whole-HIT elimination and its base/loop computation—not by installing ℕ as the hom. It compares the underlying endomorphism type/carrier; it does not identify all of WalkingEnd with ℕ or claim a packaged monoid/hom-category equivalence.

At the next hom level, the Eckmann-Hilton argument concerns 2-endomorphisms of an identity 1-cell:

2End_B(x) = Hom_{Hom_B(x,x)}(id_x,id_x)

α, β : 2End_B(x)
β · α = β * α = α · β

Here · is vertical composition, while * is horizontal composition derived from whiskering/postcomposition. They have the same unit, and interchange gives the shared middle term β * α; hence 2-endomorphisms of id_x commute.

At the universal-construction level, let W : J ⇸ J′ be a weight/profunctor, F : J → A a diagram, and C : J′ → A a selected W-weighted colimit. For an adjunction S ⊣ R, with S : A → B and R : B → A, the preservation statement is:

W-Colim_A(F,C)
    ⇒
W-Colim_B(S ∘ F, S ∘ C)

The proof is the same right-adjoint theorem viewed in opposite categories:

W-colimit in A
  ↔ W^op-limit in A^op
  → S^op preserves that limit, since R^op ⊣ S^op
  → W^op-limit in B^op

  ↔ W-colimit in B

Thus a left adjoint preserves every selected weighted colimit for which the input comparison/witness is supplied; the statement does not assert that every such colimit exists.

view this post on Zulip Caps (Jul 25 2026 at 01:01):

Reminder: A good time to participate in person / live online (with DubAI AI / MumbAI AI / ShanghAI AI folks) at this series of (informal) Workshop on AI proof assistants (for ω-categories) is at:

I'll personally want to discuss with reviewers and contributors (in person and/or live online) to this community book project:

And yes, we are trying to get this emdash —book published by Quanta Books! It's story contains more juicy drama than Kevin Hartnett's The Proof in the Code...

view this post on Zulip Kevin Carlson (Jul 25 2026 at 02:30):

Technical debate about…what, exactly? You’re just spamming us with slop. And people are rarely aware of, let alone cite, slop books by anons on random GitHubs.

view this post on Zulip Caps (Jul 25 2026 at 03:38):

Kevin Carlson said:

Technical debate about…what, exactly? You’re just spamming us with slop. And people are rarely aware of, let alone cite, slop books by anons on random GitHubs.

Dear Kevin Carlson, thanks for your prolific contributions in virtually every threads in this Zulip. But you might be an unfortunate victim of what is called "SLOP COPE"; instead of paying me $500 to show you how to upgrade your AI MathOps, you'd rather cope with delusional one-liners...

e.g. you'll rather cope with quiver.app which has not been upgraded for years (despite the promises by @Nathanael Arkor since last CT2025) than use my OpenAI-verified Codex-plugin ArrowGram to edit your commutative diagrams and research papers and 100x your productivity:

- https://github.com/hotdocx/arrowgram
- https://LastRevision.pro/marketing/blog/lean-lambdapi-ai-workspaces-in-browser

getpaidx-workspace-arrowgram-vertical.png

getpaidx-workspace-lambdapi.png

view this post on Zulip Nathanael Arkor (Jul 25 2026 at 06:12):

Caps said:

quiver.app which has not been upgraded for years

image.png

view this post on Zulip fosco (Jul 25 2026 at 08:58):

The signal-to-noise ratio in this thread is approaching zero...

view this post on Zulip Tom de Jong (Jul 25 2026 at 15:45):

FWIW: Over on the TYPES Zulip this user was recently banned.