feat(AlgebraicTopology): the truncated quasicategory induced by a quasicategory

[joelriou]

---

• depends on: feat(AlgebraicTopology/SimplicialSet): more API for SSet.op #38664

[github-actions]

PR summary 99b39ae430

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.Quasicategory.TwoTruncatedQuasicategory (new file)	1092

---

Declarations diff (regex)

+ instance (X : SSet.{u}) [X.Quasicategory] :
+ opEquiv
+ opObjEquiv_symm_yonedaEquiv_const
+ opObjEquiv_yonedaEquiv_const
+ stdSimplex.yonedaEquiv_δ_comp
+ stdSimplex.yonedaEquiv_σ_comp
+ stdSimplex.δ_comp_yonedaEquiv_symm
+ stdSimplex.σ_comp_yonedaEquiv_symm
+ δ_opObjEquiv
+ δ_two_yonedaEquiv_symm
+ σ_opObjEquiv
++ op
++ unop
++ δ_one_yonedaEquiv_symm
++ δ_zero_yonedaEquiv_symm

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 99b39ae).

• +30 new declarations
• −0 removed declarations

+SSet.Edge.CompStruct.δ_one_yonedaEquiv_symm
+SSet.Edge.CompStruct.δ_one_yonedaEquiv_symm_assoc
+SSet.Edge.CompStruct.δ_two_yonedaEquiv_symm
+SSet.Edge.CompStruct.δ_two_yonedaEquiv_symm_assoc
+SSet.Edge.CompStruct.δ_zero_yonedaEquiv_symm
+SSet.Edge.CompStruct.δ_zero_yonedaEquiv_symm_assoc
+SSet.Edge.δ_one_yonedaEquiv_symm
+SSet.Edge.δ_one_yonedaEquiv_symm_assoc
+SSet.Edge.δ_zero_yonedaEquiv_symm
+SSet.Edge.δ_zero_yonedaEquiv_symm_assoc
+SSet.PtSimplex.MulStruct.op
+SSet.PtSimplex.MulStruct.op_map
+SSet.PtSimplex.MulStruct.unop
+SSet.PtSimplex.MulStruct.unop_map
+SSet.PtSimplex.op
+SSet.PtSimplex.opEquiv
+SSet.PtSimplex.opEquiv_apply_map
+SSet.PtSimplex.opEquiv_symm_apply_map
+SSet.PtSimplex.unop
+SSet.RelativeMorphism.mk.congr_simp
+SSet.instQuasicategory₂ObjTruncatedOfNatNatTruncationOfQuasicategory
+SSet.opObjEquiv_symm_yonedaEquiv_const
+SSet.opObjEquiv_yonedaEquiv_const
+SSet.stdSimplex.yonedaEquiv_δ_comp
+SSet.stdSimplex.yonedaEquiv_σ_comp
+SSet.stdSimplex.δ_comp_yonedaEquiv_symm
+SSet.stdSimplex.σ_comp_yonedaEquiv_symm
+SSet.δ_opObjEquiv
+SSet.σ_opObjEquiv
+SimplexCategory.rev_map

---

Decrease in strong tech debt: (relative, absolute) = (7.23, 0.00)

Current number	Change	Type (strong)
4354	-12	backward.defeqAttrib.useBackward
6979	-7	backward.isDefEq.respectTransparency
3984	-3	backward.isDefEq.respectTransparency.types

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
5048	1	exposed public sections

Current commit 99b39ae430
Reference commit 9fb10993c1

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(AlgebraicTopology/SimplicialSet): more API for SSet.op #38664
  By Dependent Issues (🤖). Happy coding!