Equivalence

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Equivalence.lean

Statistics

Metric	Count
Definitions Equivalence, Equivalence	2
Theorems hasInitial_iff, hasTerminal_iff, hasInitial_of_equivalence, hasTerminal_of_equivalence	4
Total	6

CategoryTheory

Definitions

Name	Category	Theorems
Equivalence 📖	CompData	48 math math: Equivalence.symmEquivFunctor_obj, Equivalence.comp_asNatTrans, HasCardinalFilteredGenerator.exists_equivalence, Equivalence.mkHom_id_inverse, EssentiallySmall.equiv_smallCategory, Equivalence.inverseFunctor_obj, Equivalence.pow_one, Equivalence.symmEquivInverse_obj_counitIso_hom, Equivalence.inverseFunctor_map, Equivalence.symmEquivFunctor_map, simply_connected_def, Equivalence.inverseFunctorObjIso_inv, SimplyConnectedSpace.equiv_unit, Equivalence.mkIso_hom, Equivalence.congrLeftFunctor_obj, Equivalence.symmEquiv_functor, Equivalence.symmEquivInverse_obj_functor, Equivalence.functorFunctor_obj, Equivalence.symmEquivInverse_obj_counitIso_inv, exists_equivalence_iff_of_locallySmall, Equivalence.inverseFunctorObj'_hom_app, Equivalence.inverseFunctorMapIso_symm_eq_isoInverseOfIsoFunctor, Equivalence.congrLeftFunctor_map, Equivalence.symmEquiv_counitIso, Equivalence.symmEquiv_unitIso, Equivalence.comp_asNatTrans_assoc, simplyConnectedSpace_iff, Equivalence.pow_zero, Equivalence.symmEquiv_inverse, Equivalence.id_asNatTrans, Equivalence.congrRightFunctor_obj, Equivalence.pow_neg_one, Equivalence.mkHom_id_functor, ObjectProperty.exists_equivalence_iff, SmallCategoryCardinalLT.exists_equivalence, Equivalence.functorFunctor_map, Equivalence.inverseFunctorObjIso_hom, Equivalence.inverseFunctorObj'_inv_app, Equivalence.symmEquivInverse_obj_unitIso_inv, Equivalence.mkHom_comp, Equivalence.mkIso_inv, Equivalence.mkHom_comp_assoc, Equivalence.symmEquivInverse_obj_inverse, Equivalence.symmEquivInverse_obj_unitIso_hom, SmallCategoryOfSet.exists_equivalence, Equivalence.congrRightFunctor_map, equiv_punit_iff_unique, Equivalence.symmEquivInverse_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasInitial_of_equivalence 📖	mathematical	—	Limits.HasInitial	—	Adjunction.hasColimitsOfShape_of_equivalence
hasTerminal_of_equivalence 📖	mathematical	—	Limits.HasTerminal	—	Adjunction.hasLimitsOfShape_of_equivalence

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
Equivalence 📖	CompData	—

CategoryTheory.Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasInitial_iff 📖	mathematical	—	CategoryTheory.Limits.HasInitial	—	CategoryTheory.hasInitial_of_equivalence isEquivalence_inverse isEquivalence_functor
hasTerminal_iff 📖	mathematical	—	CategoryTheory.Limits.HasTerminal	—	CategoryTheory.hasTerminal_of_equivalence isEquivalence_inverse isEquivalence_functor

---

← Back to Index