Final

Statistics

Metric	Count
Definitions	0
Theorems `final_of_final_costructuredArrowToOver`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`final_of_final_costructuredArrowToOver` 📖	—	`Final` `CategoryTheory.CostructuredArrow` `obj` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.CostructuredArrow.toOver`	—	—	`final_of_natIso` `final_comp` `final_of_isRightAdjoint` `isRightAdjoint_of_isEquivalence` `CategoryTheory.CostructuredArrow.isEquivalenceMap₂` `CategoryTheory.Equivalence.isEquivalence_inverse` `CategoryTheory.Equivalence.faithful_inverse` `CategoryTheory.Equivalence.full_inverse` `isIso_whiskerLeft` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.IsIso.id` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Equivalence.faithful_functor` `CategoryTheory.Equivalence.full_functor` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `map_comp` `CategoryTheory.Equivalence.fun_inv_map` `CategoryTheory.Equivalence.functor_unit_comp_assoc`

---