Documentation Verification Report

PureCoherence

📁 Source: Mathlib/Tactic/CategoryTheory/Coherence/PureCoherence.lean

Statistics

Metric	Count
Definitions `MkEqOfNaturality`, `mkEqOfNaturality`, `MonadNormalizeNaturality`, `mkNaturalityAssociator`, `mkNaturalityComp`, `mkNaturalityHorizontalComp`, `mkNaturalityId`, `mkNaturalityInv`, `mkNaturalityLeftUnitor`, `mkNaturalityRightUnitor`, `mkNaturalityWhiskerLeft`, `mkNaturalityWhiskerRight`, `normalizedHom`, `toNormalize`, `instInhabitedResult`, `default`, `naturality`, `normalize`, `pureCoherence`	19
Theorems	0
Total	19

Mathlib.Tactic.BicategoryLike

Definitions

Name	Category	Theorems
`MkEqOfNaturality` 📖	CompData	—
`MonadNormalizeNaturality` 📖	CompData	—
`naturality` 📖	CompOp	—
`normalize` 📖	CompOp	—
`pureCoherence` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MkEqOfNaturality

Definitions

Name	Category	Theorems
`mkEqOfNaturality` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality

Definitions

Name	Category	Theorems
`mkNaturalityAssociator` 📖	CompOp	—
`mkNaturalityComp` 📖	CompOp	—
`mkNaturalityHorizontalComp` 📖	CompOp	—
`mkNaturalityId` 📖	CompOp	—
`mkNaturalityInv` 📖	CompOp	—
`mkNaturalityLeftUnitor` 📖	CompOp	—
`mkNaturalityRightUnitor` 📖	CompOp	—
`mkNaturalityWhiskerLeft` 📖	CompOp	—
`mkNaturalityWhiskerRight` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.Normalize

Definitions

Name	Category	Theorems
`instInhabitedResult` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.Normalize.Result

Definitions

Name	Category	Theorems
`normalizedHom` 📖	CompOp	—
`toNormalize` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.Normalize.instInhabitedResult

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index