feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories by sinhp · Pull Request #30366 · leanprover-community/mathlib4

sinhp · 2025-10-09T11:40:50Z

This PR defines the basic preliminaries for defining locally cartesian closed categories (LCCCs).

First, we develop a computable implementation of pullbacks, by introducing a new type-class ChosenPullback. The non-computable HasPullbacksAlong and HasPullbacks predicates yield instances of ChosenPullback using global choice, but interestingly in the category of types every morphism has chosen pullbacks. Also, cartesian monoidal categories, morphisms to the terminal object and the product projections have chosen pullbacks. We prove that ChosenPullback has good closure properties, e.g., isos have chosen pullbacks, and composition of morphisms with chosen pullbacks have chosen pullbacks.

Separately, we prove that pull-push along a morphism with chosen pullbacks gives the (cartesian) binary product of that morphism, seen as an object of a slice category, and any other object of the same slice category. In fact, we also prove the stronger statement, namely that the pull-push composition (Over.ChosenPullback.pullback Z.hom) ⋙ (Over.map Z.hom) is naturally isomorphic to the right tensor product functor _ × Y in Over X. This is going to be crucial in our mate-based approach to LCCCs.

Also, using the calculus of mates we define certain natural isomorphisms involving Over.star and Over.pullback which will be used in defining the right adjoint to the pullback functor in the development of LCCCs.

github-actions · 2025-10-09T11:42:05Z

PR summary 15ee1d2ac7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.LocallyCartesianClosed.Prelim` (new file)	718

Declarations diff

+ ChosenPullback
+ Functor.toOverTerminal
+ Over.pullbackMapNatIsoTensorRight_hom_app
+ binaryFan
+ binaryFanIsBinaryProduct
+ binaryFan_pt
+ binaryFan_pt_hom
+ cartesianMonoidalCategorySnd
+ cartesianMonoidalCategoryToTerminal
+ comp
+ condition
+ counit_app
+ equivOverTerminal
+ fst
+ fst'
+ fst'_left
+ homEquiv
+ homEquiv_symm
+ hom_ext
+ id
+ instance [HasBinaryProducts C] : (forget X).IsLeftAdjoint := ⟨_, ⟨forgetAdjStar X⟩⟩
+ instance [HasBinaryProducts C] : (star X).IsRightAdjoint := ⟨_, ⟨forgetAdjStar X⟩⟩
+ instance _root_.Limits.Types.chosenPullback {X Y : Type u} (f : Y ⟶ X) :
+ isLimitPullbackCone
+ isPullback
+ iteratedSliceBackward_forget
+ lift
+ lift_fst
+ lift_snd
+ mapPullackIsoProd'
+ mapPullbackIsoProd
+ mapPullbackIsoProd_hom_comp_fst
+ mapPullbackIsoProd_hom_comp_snd
+ ofHasPullbacksAlong
+ ofOverMk
+ pullbackMapNatIsoTensorRight
+ pullbackObj
+ snd
+ snd'
+ snd'_left
+ starIsoToOverTerminal
+ starIteratedSliceForwardIsoPullback
+ starPullbackIsoStar
+ star_map
+ unit_app

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

…ndex, pull-push) (Sigma=push, Reindex=pull, pull-push = cartesian product)

joelriou · 2025-10-09T19:59:22Z

Just a few quick remarks for now:

the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;
the assumption HasPullbacks is weakened in PRs by @Jlh18 (see [Merged by Bors] - refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the changes to be made should happen;
I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

sinhp · 2025-10-09T20:44:47Z

Just a few quick remarks for now:

the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;

What about making a new file in the new folder LocallyCartesianClosed named "Prelim.lean"? Otherwise, please suggest a location for this. The effect on Galois/Examples is indeed strange, but I don't think it's gonna be resolved just by changing the file name.
We had a discussion about this on Zulip here:
https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321525.20Locally.20Cartesian.20Closed.20Categories/near/498346104

the assumption HasPullbacks is weakened in PRs by @Jlh18 (see refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the
changes to be made should happen;

@Jlh18 , Is this close to being merged? Seems this is weaker assumption for a couple of theorems in lccc prelim.

I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

We already have cartesian monoidal category structure on slice categories thanks to Andrew's work – incidentally one reason the LCCC work got merge conflict back in February, and had to wait for that work to be done. But, it is nicer to do it that way. I am using this monoidal structure. If I don't misread what you say, then ChosenPullback f for every f also gives a cartesian monoidal structure on slices.

Also, on the semantics side, I think with ChosenPullback f the codomain fibration will be a a cloven fibration, whereas with HasPullbacks you have a general Grothendieck fibration. I think the codomain functor for LCCCs is a general Grothendieck fibration not necessarily a cloven one. So, in a way Π f, ChosenPullback f results in a stricter semantics.

joelriou · 2025-10-10T00:20:44Z

the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;

... The effect on Galois/Examples is indeed strange, but I don't think it's gonna be resolved just by changing the file name.

Well, your additions may have changed the import graph of other files, which may be the reason for the breakage in Galois categories. Putting the new code in a separate file should solve this issue...

the assumption HasPullbacks is weakened in PRs by @Jlh18 (see refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the
changes to be made should happen;

@Jlh18 , Is this close to being merged? Seems this is weaker assumption for a couple of theorems in lccc prelim.

I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

Also, on the semantics side, I think with ChosenPullback f the codomain fibration will be a a cloven fibration, whereas with HasPullbacks you have a general Grothendieck fibration.

I have no idea how what you say answer my suggestion. In your code, it seems that there is data for the right adjoints of the pullback functors on the Over categories, the suggestion is to include also data for the pullback functors themselves, as "chosen" right adjoints of Over.map. How could this make something less general than the definition where the pullback functors would be defined using the limits given by HasPullbacks!?

(Ah, actually, it seems you do not include data for the pushforwards. As a structure on a category, it would make sense to have data for these functors.)

sinhp · 2025-10-10T06:46:25Z

Just a few quick remarks for now:

the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;

What about making a new file in the new folder LocallyCartesianClosed named "Prelim.lean"? Otherwise, please suggest a location for this. The effect on Galois/Examples is indeed strange, but I don't think it's gonna be resolved just by changing the file name. We had a discussion about this on Zulip here: https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321525.20Locally.20Cartesian.20Closed.20Categories/near/498346104

the assumption HasPullbacks is weakened in PRs by @Jlh18 (see refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the
changes to be made should happen;

@Jlh18 , Is this close to being merged? Seems this is weaker assumption for a couple of theorems in lccc prelim.

I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

We already have cartesian monoidal category structure on slice categories thanks to Andrew's work – incidentally one reason the LCCC work got merge conflict back in February, and had to wait for that work to be done. But, it is nicer to do it that way. I am using this monoidal structure. If I don't misread what you say, then ChosenPullback f for every f also gives a cartesian monoidal structure on slices.

Also, on the semantics side, I think with ChosenPullback f the codomain fibration will be a a cloven fibration, whereas with HasPullbacks you have a general Grothendieck fibration. I think the codomain functor for LCCCs is a general Grothendieck fibration not necessarily a cloven one. So, in a way Π f, ChosenPullback f results in a stricter semantics.

the additions to Comma.Over.Pullback should probably go in a separate file, because it is already quite long, and it seems it has strange side effects on an unrelated file Galois/Examples;

... The effect on Galois/Examples is indeed strange, but I don't think it's gonna be resolved just by changing the file name.

Well, your additions may have changed the import graph of other files, which may be the reason for the breakage in Galois categories. Putting the new code in a separate file should solve this issue...

the assumption HasPullbacks is weakened in PRs by @Jlh18 (see refactor: weaken HasPullbacks to HasPullback in Over.Pullback #29795), so that some coordination about the
changes to be made should happen;

@Jlh18 , Is this close to being merged? Seems this is weaker assumption for a couple of theorems in lccc prelim.

I am not sure exactly where/when this remark should be made again, but I think @jcommelin had suggested that at some point we should allow "chosen pullbacks" (which I understand by saying that for a morphism f we could have a ChosenPullback f typeclass with the data of a choice of functor between Over categories that is right adjoint to the obvious functor), I think it is important for future computations.

Also, on the semantics side, I think with ChosenPullback f the codomain fibration will be a a cloven fibration, whereas with HasPullbacks you have a general Grothendieck fibration.

I have no idea how what you say answer my suggestion. In your code, it seems that there is data for the right adjoints of the pullback functors on the Over categories, the suggestion is to include also data for the pullback functors themselves, as "chosen" right adjoints of Over.map. How could this make something less general than the definition where the pullback functors would be defined using the limits given by HasPullbacks!?

(Ah, actually, it seems you do not include data for the pushforwards. As a structure on a category, it would make sense to have data for these functors.)

It seems I was confused about your comment. I thought it is concerning the file Comma.Over.Pullback, but it seems you are actually commenting on #30375 PR and not this PR, correct?

mathlib4-merge-conflict-bot · 2025-10-10T08:25:55Z

This pull request has conflicts, please merge master and resolve them.

…c-prelim

sinhp · 2025-10-10T15:33:33Z

@joelriou

I addressed your first two points in this last commit.

If I understand correctly, your third point applies to a different PR, namely #30375, which I shall address by changes to that PR separately.

joelriou · 2025-10-10T16:16:19Z

Mathlib/CategoryTheory/LocallyCartesianClosed/Prelim.lean

+    (isBinaryProductSigmaReindex Y Z) (Limits.prodIsProd Y Z) ⟨.left⟩
+
+lemma sigmaReindexIsoProd_hom_comp_snd {Y Z : Over X} :
+    (sigmaReindexIsoProd Y Z).hom ≫ (snd Y Z) = (μ_ Y Z) :=


Could you remove unnecessary parentheses in the whole file? (And add simp/reassoc attributes to lemmas when applicable.)

We add stability lemmas for `HasCardinalLT X κ` for sigma types, binary products, etc when `κ` is regular (or at least infinite).

…olimitType (leanprover-community#30779) We obtain a dual result to leanprover-community#30403 for the interaction between final functors and colimits of functors to types. This is phrased using the universe generic `Functor.ColimitType`. (We also improve the proof of leanprover-community#30403)

Multiple build runs from the same PR don't seem to be getting canceled. There's a suspicious line break in the `concurrency` option which might be confusing GitHub and causing this. cf. [#mathlib4 > github action bandwidth @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/github.20action.20bandwidth/near/547550820).

…t` (leanprover-community#30638) + Construct the symmetric monoidal structure on SemimoduleCat, and transport it to the same structure on ModuleCat (in a way preserving pre-existing defeqs) using the equivalence `ModuleCat.equivalenceSemimoduleCat` between the categories. Just a few proofs in the Representation library need to be fixed (in a straightforward way). Public API for ModuleCat is duplicated to SemimoduleCat.

…nity#30749) This is a collection of typo fixes suggested to me by Codex. I decided to split these changes out of leanprover-community#30669, because I feel none of these are completely trivial to review, mostly because they require inspecting the context of the text as opposed to just the text itself. I've manually reviewed all of them to the best of my abilities and I'm reasonably sure they are all correct, and that they represent an improvement over the status quo. However, I am not an expert in Algebra, so please review with care. I suspect that there might still be quite a wide span in the difficulty of reviewing the changes in this PR, but I don't have a strong intuition for which changes herein might still be seen as relatively easy to review. I'm open to splitting this PR further should any reviewer think that is a good idea.

Let `C` be a category and `F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat`. Given `S : C`, and objects `M` and `N` in `F.obj (.mk (op S))`, we define a presheaf of types `F.presheafHom M N` on the category `Over S`: its sections on an object `T : Over S` corresponding to a morphism `p : X ⟶ S` are the type of morphisms `p^* M ⟶ p^* N`. We shall say that `F` satisfies the descent of morphisms for a Grothendieck topology `J` (i.e. `F` is a prestack) if these presheaves are all sheaves. Co-authored-by: Christian Merten [christian@merten.dev](mailto:christian@merten.dev)

…ne (leanprover-community#30996)

leanprover-community#30199) Add simple API lemmas about the support of functions in `ContDiffMapSupportedIn`. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de> Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

…nprover-community#30540) - Define convergence in distribution of random variables: this is the weak convergence of their laws. - Prove the continuous mapping theorem for convergence in distribution and continuous functions. Co-authored-by: Remy Degenne <remydegenne@gmail.com>

…nprover-community#30729) Add several elementary lemmas aiding computations with log⁺. Improve the docstrings a little.

…prover-community#30655) We show that the projection `C × D ⥤ C` is a final (or initial) functor when `D` is connected. (Before this PR, it was proven under the stronger assumption that `D` was (co)filtered.)

…ms (leanprover-community#30693) This category will be relevant in the study of accessible categories. I am making Johan Commelin a co-author as the new file `PartOrdEmb.lean` is essentially a copy-paste of `PartOrd.Lean`. Co-authored-by: Johan Commelin <johan@commelin.net>

Fixes a typo in a docstring.

…nprover-community#31049) Add `enorm` versions of theorems in `OperatorNorm.lean` as it currently has only `norm` and `nnnorm` versions.

leanprover-community#29082) I have not tested if this is usable in practice; perhaps it is not.

…r-community#30335) We obtain various lemmas about adjunctions between functors by computing `conjugateEquiv` in case of associators, unitors, and whiskerings. We deduce a way to obtain compatibilites with respect to composition of functors of left adjoints assuming that we have these compatibilites for right adjoints. In leanprover-community#30318, this shall be applied to the study of the compatibilities with respect to composition of the pullback functors for presheaves of modules.

…unity#31048) It duplicates a lemma above, but having this name is nice for discoverability.

…0662)

…s and derived results on infinite places (leanprover-community#27978) If `w` is an absolute value on `L/K` and `v` is an absolute value of `K` then `w.LiesOver v` is the class defining the property that `v` is the restriction of `w` to `K`. This PR continues the work from leanprover-community#24881. Original PR: leanprover-community#24881

…nprover-community#31052)

…eanprover-community#31035)

…perate growth (leanprover-community#30553) The Schwartz function file reached 1500 lines of code, so it really needs splitting. The only other change is that I added namespaces and moved one lemma into the `MeasureTheory.Measure` namespace to allow for dot-notation.

e.g. `frobenius_add` should be replaced with `map_add _`.

…ver-community#30967) In some cases, add `≠ ∞` versions of existing `< ∞` lemmas, and tag those with finiteness. Use this to golf one proof `by measurability` using finiteness, which is the morally correct proof. Motivated by leanprover-community#30966.

…lccc-prelim

mathlib4-merge-conflict-bot · 2025-11-11T17:39:22Z

This pull request has conflicts, please merge master and resolve them.

github-actions bot added t-category-theory Category theory large-import Automatically added label for PRs with a significant increase in transitive imports labels Oct 9, 2025

sinhp mentioned this pull request Oct 9, 2025

[Merged by Bors] - feat(CategoryTheory): LCCC sections (constructing right adjoint to Over.ChosenPullback.pullback) #30373

Closed

2 tasks

the preliminaries for locally cartesian closed categories (Sigma, Rei…

e360a4a

…ndex, pull-push) (Sigma=push, Reindex=pull, pull-push = cartesian product)

sinhp force-pushed the lccc-prelim branch from aeaef70 to e360a4a Compare October 9, 2025 16:21

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 10, 2025

sinhp closed this Oct 10, 2025

sinhp force-pushed the lccc-prelim branch from e360a4a to 5da8203 Compare October 10, 2025 14:53

Merge remote-tracking branch 'refs/remotes/sina/lccc-prelim' into lcc…

801ce89

…c-prelim

github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Oct 10, 2025

prelims for lcccs

fa5b706

sinhp reopened this Oct 10, 2025

fix for HasPullbacksAlong

1f9de85

joelriou reviewed Oct 10, 2025

View reviewed changes

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 10, 2025

parentheses and simp

75d9799

sinhp removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 11, 2025

sinhp added 5 commits October 11, 2025 13:54

Update Mathlib.lean

6d82809

not needed assumption

012e053

rm simp

97a5a79

correcting attribution

f2618e6

Update Prelim.lean

ad1b0eb

joelriou and others added 26 commits October 29, 2025 00:35

feat(SetTheory): more API for HasCardinalLT (leanprover-community#30633)

7c26ba6

We add stability lemmas for `HasCardinalLT X κ` for sigma types, binary products, etc when `κ` is regular (or at least infinite).

chore: remove some unused variables (leanprover-community#31017)

c0ae1f3

chore(NumberField/Cyclotomic): add statements for the case of power o…

f45bc7a

…ne (leanprover-community#30996)

feat: elementary lemmas aiding computations with log⁺, Mark II (lea…

f531e60

…nprover-community#30729) Add several elementary lemmas aiding computations with log⁺. Improve the docstrings a little.

feat(CategoryTheory/Final): improve assumptions for final_fst (lean…

6f28114

…prover-community#30655) We show that the projection `C × D ⥤ C` is a final (or initial) functor when `D` is connected. (Before this PR, it was proven under the stronger assumption that `D` was (co)filtered.)

doc: fix trivial typo in docstring (leanprover-community#31045)

69f1833

Fixes a typo in a docstring.

feat(Analysis/Complex): enorm versions for OperatorNorm.lean (lea…

c53d34d

…nprover-community#31049) Add `enorm` versions of theorems in `OperatorNorm.lean` as it currently has only `norm` and `nnnorm` versions.

feat: tag IsInducing and Is{Open,Closed,}Embedding with fun_prop (

6a276d1

leanprover-community#29082) I have not tested if this is usable in practice; perhaps it is not.

chore: make MDifferentiableAt.mfderiv_prod an alias. (leanprover-comm…

188562f

…unity#31048) It duplicates a lemma above, but having this name is nice for discoverability.

feat(LocallyFinite): add of_comp_surjective (leanprover-community#3…

3377d31

…0662)

feat(docs/undergrad): add calculus and Schwartz function results (lea…

e29df49

…nprover-community#31052)

feat(Topology/Sets): Singleton instances for (Nonempty)Compacts (l…

737069e

…eanprover-community#31035)

chore: deprecate frobenius_xxx lemmas (leanprover-community#31014)

016f98d

e.g. `frobenius_add` should be replaced with `map_add _`.

Merge branch 'lccc-prelim' of https://github.com/sinhp/mathlib4 into …

a674d3d

…lccc-prelim

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 11, 2025

grunweg changed the title ~~feat (CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories~~ feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories Nov 19, 2025

sinhp mentioned this pull request Dec 3, 2025

[Merged by Bors] - feat(CategoryTheory): Computable cartesian monoidal structure on slices induced by chosen pullbacks #31433

Closed

1 task

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories#30366

feat(CategoryTheory): The Preliminaries for Locally Cartesian Closed Categories#30366
sinhp wants to merge 67 commits intoleanprover-community:masterfrom
sinhp:lccc-prelim

sinhp commented Oct 9, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Oct 9, 2025 •

edited

Loading

Declarations diff

Uh oh!

joelriou commented Oct 9, 2025

Uh oh!

sinhp commented Oct 9, 2025 •

edited

Loading

Uh oh!

joelriou commented Oct 10, 2025 •

edited

Loading

Uh oh!

sinhp commented Oct 10, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Oct 10, 2025

Uh oh!

sinhp commented Oct 10, 2025

Uh oh!

joelriou Oct 10, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

20 participants

Conversation

sinhp commented Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 15ee1d2ac7

Import changes for modified files

Declarations diff

Uh oh!

joelriou commented Oct 9, 2025

Uh oh!

sinhp commented Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

joelriou commented Oct 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sinhp commented Oct 10, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Oct 10, 2025

Uh oh!

sinhp commented Oct 10, 2025

Uh oh!

joelriou Oct 10, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib4-merge-conflict-bot commented Nov 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

20 participants

sinhp commented Oct 9, 2025 •

edited

Loading

github-actions bot commented Oct 9, 2025 •

edited

Loading

sinhp commented Oct 9, 2025 •

edited

Loading

joelriou commented Oct 10, 2025 •

edited

Loading