Theorems · Definition · category theory
Equiv.toIso
{X Y : Type u} → X ≃ Y → (X ≅ Y)Any equivalence between types in the same universe gives a categorical isomorphism between those types.
- Defined in
- Mathlib.CategoryTheory.Types.Basic
- Cited by
- 58 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 and proof · cited by 8,337
- CategoryTheory.Isostatement · cited by 3,963
- Equiv.symmproof · cited by 3,681
- TypeCat.ofHomproof · cited by 389
Cited by136
Results whose statement or proof uses this declaration.
- CategoryTheory.isIso_iff_bijectiveproof · cited by 16
- CategoryTheory.Limits.Types.pullbackIsoPullbackproof · cited by 12
- SSet.Subcomplex.topIsoproof · cited by 8
- CategoryTheory.bijective_iff_isIso_ofHomproof · cited by 8
- Types.monoOverEquivalenceSetproof · cited by 6
- Action.diagonalSuccIsoTensorDiagonalproof · cited by 5
- Action.leftRegularTensorIsoproof · cited by 5
- CategoryTheory.Functor.representableByEquivproof · cited by 5
- SSet.stdSimplex.opIsoproof · cited by 4
- CategoryTheory.equivYonedaproof · cited by 4
- SSet.opFunctorCompOpFunctorIsoproof · cited by 4