Zulip Chat Archive

Stream: Infinity-Cosmos

Topics:

synchronous meeting Monday November 24 (13 messages, latest: Dec 02 2025 at 23:18)
need help removing an erw (5 messages, latest: Nov 19 2025 at 16:00)
2-truncated quasicategories (63 messages, latest: Nov 19 2025 at 12:13)
time for the formal category theory of quasicategories! (9 messages, latest: Oct 31 2025 at 17:26)
help fixing broken files after mathlib bump (8 messages, latest: Oct 21 2025 at 20:19)
challenge: eight sorries away from product-preserving (62 messages, latest: Oct 10 2025 at 21:53)
Functor quasi-categories are formalized (20 messages, latest: Sep 19 2025 at 17:10)
pseudofunctors on EnrichedCat (1 message, latest: Sep 16 2025 at 14:02)
transport enrichment for enriched ordinary categories (14 messages, latest: Aug 16 2025 at 05:29)
Bicategory of enriched categories (40 messages, latest: Aug 11 2025 at 00:58)
equivalences of quasi-categories (24 messages, latest: Jul 29 2025 at 04:30)
remaining facts about the simplex category (42 messages, latest: Jul 06 2025 at 09:04)
Universe issues: relating across universes (5 messages, latest: Jun 29 2025 at 14:16)
Universe issues: ulifting from low-u data (1 message, latest: Jun 24 2025 at 23:27)
alternate (defeq) nerve definition (8 messages, latest: Jun 01 2025 at 23:08)
infinity-cosmos project synchronous meeting! (19 messages, latest: May 29 2025 at 02:45)
towards the homotopy category of a quasi-category (84 messages, latest: May 20 2025 at 10:21)
broken symmetric instance on simplicial sets (4 messages, latest: May 10 2025 at 18:42)
challenge: constructively generate nerve data (4 messages, latest: May 10 2025 at 17:53)
Model categories (9 messages, latest: Apr 17 2025 at 16:55)
Constructing morphism from inner 2-horn (3 messages, latest: Apr 09 2025 at 15:21)
infinity cosmos project at the "AI for Mathematics" workshop (5 messages, latest: Apr 07 2025 at 20:31)
the homotopy category functor and the nerve adjunction (93 messages, latest: Apr 02 2025 at 15:46)
do we need Quillen model categories? (31 messages, latest: Apr 01 2025 at 14:54)
new task list (2 messages, latest: Mar 21 2025 at 17:39)
standardSimplex → stdSimplex (13 messages, latest: Mar 18 2025 at 21:17)
preserves limits (3 messages, latest: Mar 14 2025 at 09:30)
(new) simplicial notations (96 messages, latest: Mar 13 2025 at 21:07)
new task list incoming (5 messages, latest: Mar 09 2025 at 01:08)
Learning Mathlib's category theory (16 messages, latest: Feb 14 2025 at 23:12)
Model of Isomorphism (36 messages, latest: Feb 09 2025 at 21:53)
mathlib bump (4 messages, latest: Feb 02 2025 at 17:13)
infinity-cosmos PR feed (87 messages, latest: Feb 02 2025 at 16:22)
conical simplicial limits (84 messages, latest: Jan 23 2025 at 14:42)
isofibration API (10 messages, latest: Jan 22 2025 at 20:54)
truncated simplicial notations (19 messages, latest: Jan 17 2025 at 23:43)
contributions to the infinity-cosmos project? (4 messages, latest: Jan 14 2025 at 00:05)
aesop failure (11 messages, latest: Jan 07 2025 at 17:37)
Integration with CW-Complexes (1 message, latest: Jan 06 2025 at 22:21)
conical terminal object (9 messages, latest: Dec 13 2024 at 21:19)
Simplicial (homotopy coherent) nerve (2 messages, latest: Dec 10 2024 at 17:26)
enriched cotensors (18 messages, latest: Dec 03 2024 at 15:48)
Quasicategory (nerve C) (47 messages, latest: Nov 26 2024 at 19:29)
warning: mathlib reorganization (5 messages, latest: Nov 26 2024 at 18:11)
what permissions do we need for PRs? (31 messages, latest: Nov 22 2024 at 20:07)
towards a correct definition of an infinity-cosmos (15 messages, latest: Nov 22 2024 at 18:58)
llp/rlp PR (1 message, latest: Nov 16 2024 at 23:50)
Mathlib Bump (1 message, latest: Nov 12 2024 at 21:03)
capitalization of morphism properties? (16 messages, latest: Nov 12 2024 at 06:55)
MorphismProperty for Morphisms between Classes of Objects (4 messages, latest: Nov 11 2024 at 19:16)
homotopies and equivalences for both qCats and Kan (16 messages, latest: Nov 09 2024 at 16:33)
welcome! (53 messages, latest: Nov 08 2024 at 22:19)
warning: repository reorganization (3 messages, latest: Oct 31 2024 at 21:31)
warning: small refactor of simplicial categories (2 messages, latest: Oct 25 2024 at 15:50)
warning: new PR will move some simplicial sets files (2 messages, latest: Oct 11 2024 at 16:11)
Closed Monoidal cats are self-enriched (8 messages, latest: Oct 01 2024 at 21:14)
terminology for co/skeleton functors (25 messages, latest: Sep 30 2024 at 16:14)
should we shutdown the local "mathlib" folder? (4 messages, latest: Sep 29 2024 at 21:42)
the coherent isomorphism (27 messages, latest: Sep 26 2024 at 20:35)
Cartesian/monoidal closed structure on SSet (31 messages, latest: Sep 23 2024 at 22:06)
lake exe cache get not working (21 messages, latest: Sep 10 2024 at 13:09)
Axioms (3 messages, latest: Sep 10 2024 at 07:44)
help with Kerodon tags (11 messages, latest: Sep 10 2024 at 05:02)
channel events (2 messages, latest: Sep 10 2024 at 02:44)
repository protocols? (5 messages, latest: Sep 09 2024 at 22:04)
related golfing work (1 message, latest: Sep 09 2024 at 16:57)

Last updated: Dec 20 2025 at 21:32 UTC