Coherence

Statistics

Metric	Count
Definitions `LiftHom`, `LiftHom_associator_hom`, `LiftHom_associator_inv`, `LiftHom_comp`, `LiftHom_id`, `LiftHom_left_unitor_hom`, `LiftHom_left_unitor_inv`, `LiftHom_right_unitor_hom`, `LiftHom_right_unitor_inv`, `LiftHom_tensor`, `LiftObj`, `LiftObj_of`, `LiftObj_tensor`, `LiftObj_unit`, `coherence`, `coherence_loop`, `exception`, `exception'`, `insertTrailingIds`, `liftHom_WhiskerLeft`, `liftHom_WhiskerRight`, `liftable_prefixes`, `mkProjectMapExpr`, `monoidal_coherence`, `monoidal_simps`, `pure_coherence`, `tacticMonoidal_coherence`	27
Theorems `assoc_liftHom`, `insert_id_lhs`, `insert_id_rhs`	3
Total	30

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc_liftHom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Category.assoc`
`insert_id_lhs` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.id`	—	—	`CategoryTheory.Category.comp_id`
`insert_id_rhs` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.id`	—	—	`CategoryTheory.Category.comp_id`

---