Theorems · Definition · category theory
CategoryTheory.Iso.toEquiv
{X Y : Type u} → (X ≅ Y) → X ≃ YAny isomorphism between types gives an equivalence.
- Defined in
- Mathlib.CategoryTheory.Types.Basic
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Equivstatement · cited by 8,337
- CategoryTheory.Iso.homproof · cited by 7,684
- CategoryTheory.Iso.invproof · cited by 6,514
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- CategoryTheory.Isostatement and proof · cited by 3,963
Cited by56
Results whose statement or proof uses this declaration.
- CategoryTheory.isIso_iff_bijectiveproof · cited by 16
- CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iffproof · cited by 9
- CategoryTheory.bijective_iff_isIso_ofHomproof · cited by 8
- CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObjproof · cited by 7
- equivEquivIsoproof · cited by 7
- CategoryTheory.Limits.Types.colimitEquivColimitTypeproof · cited by 6
- CategoryTheory.Limits.Concrete.prodEquivproof · cited by 5
- CategoryTheory.Functor.representableByEquivproof · cited by 5
- CategoryTheory.Functor.CorepresentableBy.ofIsoproof · cited by 4
- CategoryTheory.Limits.Cone.isLimitEquivIsTerminalproof · cited by 4
- CategoryTheory.Functor.RepresentableBy.ofIsoproof · cited by 3
- CategoryTheory.Functor.final_of_colimit_comp_coyoneda_iso_pUnitproof · cited by 3