BicategoryCoherence

Statistics

Metric	Count
Definitions `LiftHom`, `LiftHom₂`, `bicategory_coherence`, `exception`, `exception'`, `liftHomComp`, `liftHomId`, `liftHomOf`, `liftHom₂AssociatorHom`, `liftHom₂AssociatorInv`, `liftHom₂Comp`, `liftHom₂Id`, `liftHom₂LeftUnitorHom`, `liftHom₂LeftUnitorInv`, `liftHom₂RightUnitorHom`, `liftHom₂RightUnitorInv`, `liftHom₂WhiskerLeft`, `liftHom₂WhiskerRight`, `mkLiftMap₂LiftExpr`, `tacticBicategory_coherence`, `whisker_simps`	21
Theorems `assoc_liftHom₂`	1
Total	22

Name	Category	Theorems
`LiftHom` 📖	CompData	—
`LiftHom₂` 📖	CompData	—
`bicategory_coherence` 📖	CompOp	—
`exception` 📖	CompOp	—
`exception'` 📖	CompOp	—
`liftHomComp` 📖	CompOp	—
`liftHomId` 📖	CompOp	—
`liftHomOf` 📖	CompOp	—
`liftHom₂AssociatorHom` 📖	CompOp	—
`liftHom₂AssociatorInv` 📖	CompOp	—
`liftHom₂Comp` 📖	CompOp	—
`liftHom₂Id` 📖	CompOp	—
`liftHom₂LeftUnitorHom` 📖	CompOp	—
`liftHom₂LeftUnitorInv` 📖	CompOp	—
`liftHom₂RightUnitorHom` 📖	CompOp	—
`liftHom₂RightUnitorInv` 📖	CompOp	—
`liftHom₂WhiskerLeft` 📖	CompOp	—
`liftHom₂WhiskerRight` 📖	CompOp	—
`mkLiftMap₂LiftExpr` 📖	CompOp	—
`tacticBicategory_coherence` 📖	CompOp	—
`whisker_simps` 📖	CompOp	—

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc_liftHom₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory`	—	`CategoryTheory.Category.assoc`

---