Documentation Verification Report

TwoTruncated

📁 Source: Mathlib/AlgebraicTopology/Quasicategory/TwoTruncated.lean

Statistics

Metric	Count
Definitions `ofHomotopyCategory₂Fac`, `comp`, `compStruct`, `HomotopicL`, `HomotopicR`, `HomotopyCategory₂`, `homMk`, `instCategoryStruct`, `pt`, `Quasicategory₂`, `instCategoryHomotopyCategory₂`, `instSetoidEdge`	12
Theorems `comp_unique`, `homotopyCategory₂_fac`, `nonempty_iff`, `congr_homotopyCategory₂HomMk`, `homotopicR`, `refl`, `trans`, `congr_homotopyCategory₂HomMk`, `homotopicL`, `refl`, `trans`, `homMk_id`, `homMk_surjective`, `mk_surjective`, `fill21`, `fill31`, `fill32`, `homotopicL_iff_homotopicR`	18
Total	30

SSet.Truncated

Definitions

Name	Category	Theorems
`HomotopicL` 📖	MathDef	6 math math: `HomotopicL.refl`, `Edge.CompStruct.comp_unique`, `homotopicL_iff_homotopicR`, `HomotopicL.symm`, `HomotopicR.homotopicL`, `HomotopicL.trans`
`HomotopicR` 📖	MathDef	5 math math: `HomotopicR.trans`, `HomotopicL.homotopicR`, `homotopicL_iff_homotopicR`, `HomotopicR.symm`, `HomotopicR.refl`
`HomotopyCategory₂` 📖	CompData	5 math math: `HomotopyCategory₂.mk_surjective`, `Edge.CompStruct.nonempty_iff`, `HomotopyCategory₂.homMk_surjective`, `HomotopyCategory₂.homMk_id`, `Edge.CompStruct.homotopyCategory₂_fac`
`Quasicategory₂` 📖	CompData	—
`instCategoryHomotopyCategory₂` 📖	CompOp	—
`instSetoidEdge` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homotopicL_iff_homotopicR` 📖	mathematical	—	`HomotopicL` `HomotopicR`	—	`HomotopicL.homotopicR` `HomotopicR.homotopicL`

SSet.Truncated.Edge

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	—
`compStruct` 📖	CompOp	—

SSet.Truncated.Edge.CompStruct

Definitions

Name	Category	Theorems
`ofHomotopyCategory₂Fac` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_unique` 📖	mathematical	—	`SSet.Truncated.HomotopicL`	—	`SSet.Truncated.HomotopicL.homotopicR` `SSet.Truncated.Quasicategory₂.fill32` `SSet.Truncated.Quasicategory₂.fill31`
`homotopyCategory₂_fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SSet.Truncated.HomotopyCategory₂` `SSet.Truncated.HomotopyCategory₂.instCategoryStruct` `SSet.Truncated.HomotopyCategory₂.homMk`	—	`SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk` `comp_unique` `SSet.Truncated.HomotopicL.refl`
`nonempty_iff` 📖	mathematical	—	`SSet.Truncated.Edge.CompStruct` `CategoryTheory.CategoryStruct.comp` `SSet.Truncated.HomotopyCategory₂` `SSet.Truncated.HomotopyCategory₂.instCategoryStruct` `SSet.Truncated.HomotopyCategory₂.homMk`	—	`homotopyCategory₂_fac`

SSet.Truncated.HomotopicL

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_homotopyCategory₂HomMk` 📖	mathematical	—	`SSet.Truncated.HomotopyCategory₂.homMk`	—	—
`homotopicR` 📖	mathematical	—	`SSet.Truncated.HomotopicR`	—	`SSet.Truncated.Quasicategory₂.fill32`
`refl` 📖	mathematical	—	`SSet.Truncated.HomotopicL`	—	—
`trans` 📖	mathematical	—	`SSet.Truncated.HomotopicL`	—	`SSet.Truncated.Quasicategory₂.fill32`

SSet.Truncated.HomotopicR

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_homotopyCategory₂HomMk` 📖	mathematical	—	`SSet.Truncated.HomotopyCategory₂.homMk`	—	`homotopicL`
`homotopicL` 📖	mathematical	—	`SSet.Truncated.HomotopicL`	—	`SSet.Truncated.Quasicategory₂.fill31`
`refl` 📖	mathematical	—	`SSet.Truncated.HomotopicR`	—	—
`trans` 📖	mathematical	—	`SSet.Truncated.HomotopicR`	—	`SSet.Truncated.Quasicategory₂.fill31`

SSet.Truncated.HomotopyCategory₂

Definitions

Name	Category	Theorems
`homMk` 📖	CompOp	6 math math: `SSet.Truncated.HomotopicR.congr_homotopyCategory₂HomMk`, `SSet.Truncated.Edge.CompStruct.nonempty_iff`, `homMk_surjective`, `homMk_id`, `SSet.Truncated.HomotopicL.congr_homotopyCategory₂HomMk`, `SSet.Truncated.Edge.CompStruct.homotopyCategory₂_fac`
`instCategoryStruct` 📖	CompOp	4 math math: `SSet.Truncated.Edge.CompStruct.nonempty_iff`, `homMk_surjective`, `homMk_id`, `SSet.Truncated.Edge.CompStruct.homotopyCategory₂_fac`
`pt` 📖	CompOp	1 math math: `homMk_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homMk_id` 📖	mathematical	—	`homMk` `pt` `SSet.Truncated.Edge.id` `CategoryTheory.CategoryStruct.id` `SSet.Truncated.HomotopyCategory₂` `instCategoryStruct`	—	—
`homMk_surjective` 📖	mathematical	—	`SSet.Truncated.Edge` `Quiver.Hom` `SSet.Truncated.HomotopyCategory₂` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStruct` `homMk`	—	`Quotient.mk_surjective`
`mk_surjective` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `Opposite.op` `SSet.Truncated.HomotopyCategory₂`	—	—

SSet.Truncated.Quasicategory₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fill21` 📖	mathematical	—	`SSet.Truncated.Edge` `SSet.Truncated.Edge.CompStruct`	—	—
`fill31` 📖	mathematical	—	`SSet.Truncated.Edge.CompStruct`	—	—
`fill32` 📖	mathematical	—	`SSet.Truncated.Edge.CompStruct`	—	—

---

← Back to Index