Theorems · Definition · category theory
CategoryTheory.Discrete.equivalence
{I : Type u₁} → {J : Type u₂} → I ≃ J → (CategoryTheory.Discrete I ≌ CategoryTheory.Discrete J)We can promote a type-level Equiv to
an equivalence between the corresponding discrete categories.
- Defined in
- Mathlib.CategoryTheory.Discrete.Basic
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Equiv.symmproof · cited by 3,681
- CategoryTheory.Discretestatement and proof · cited by 2,447
- CategoryTheory.Discrete.functorproof · cited by 633
- CategoryTheory.Equivalencestatement · cited by 601
- CategoryTheory.eqToIsoproof · cited by 97
- CategoryTheory.Discrete.natIsoproof · cited by 28
Cited by42
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.AttachCells.reindexproof · cited by 9
- CategoryTheory.SmallObject.hasColimitsOfShape_discreteproof · cited by 7
- CategoryTheory.GradedObject.isColimitCofan₃MapBifunctorBifunctor₂₃MapObjproof · cited by 6
- CategoryTheory.Limits.Sigma.reindexproof · cited by 5
- CategoryTheory.GradedObject.isColimitCofan₃MapBifunctor₁₂BifunctorMapObjproof · cited by 5
- CategoryTheory.Limits.hasCoproducts_shrinkproof · cited by 4
- CategoryTheory.Limits.Pi.reindexproof · cited by 4
- CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initialproof · cited by 3
- CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproductsproof · cited by 3
- CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproductsproof · cited by 3
- CategoryTheory.Limits.hasProductsOfShape_of_smallproof · cited by 2
- CategoryTheory.Limits.Pi.reindex_hom_πproof · cited by 2