Skip to content

fix(Topology/Category): make TopCat.Hom constructor private#39005

Open
dagurtomas wants to merge 5 commits intoleanprover-community:masterfrom
dagurtomas:topcat-private
Open

fix(Topology/Category): make TopCat.Hom constructor private#39005
dagurtomas wants to merge 5 commits intoleanprover-community:masterfrom
dagurtomas:topcat-private

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented May 6, 2026

This is the way the ConcreteCategory API is designed, and the private constructor seems to have been commented out by accident. This ensures that morphisms are always constructed using the general API


Open in Gitpod

@dagurtomas dagurtomas added t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters labels May 6, 2026
@dagurtomas dagurtomas changed the title chore(Topology/Category): make TopCat.Hom constructor private fix(Topology/Category): make TopCat.Hom constructor private May 6, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 6, 2026

PR summary ea11ccc0c5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.


No changes to strong technical debt.
No changes to weak technical debt.

@dagurtomas dagurtomas changed the title fix(Topology/Category): make TopCat.Hom constructor private fix(Topology/Category): make TopCat.Hom constructor private May 6, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant