Theorems · Definition · category theory
CategoryTheory.Limits.Types.colimitEquivColimitType
{J : Type v} →
[inst : CategoryTheory.Category.{w, v} J] →
(F : CategoryTheory.Functor J (Type u)) →
[inst_1 : CategoryTheory.Limits.HasColimit F] → CategoryTheory.Limits.colimit F ≃ F.ColimitTypeThe equivalence between the abstract colimit of F in TypeCat u
and the "concrete" definition as a quotient.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement and proof · cited by 16,252
- Equivstatement · cited by 8,337
- Equiv.symmproof · cited by 3,681
- CategoryTheory.Limits.colimitstatement · cited by 453
- Equiv.transproof · cited by 337
- CategoryTheory.Limits.HasColimitstatement and proof · cited by 307
- CategoryTheory.Limits.colimit.isColimitproof · cited by 193
- equivShrinkproof · cited by 118
- CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIsoproof · cited by 67
- CategoryTheory.Functor.ColimitTypestatement and proof · cited by 37
- CategoryTheory.Iso.toEquivproof · cited by 32
Cited by7
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotientproof · cited by 2
- CategoryTheory.Limits.Types.colimit_eqproof · cited by 2
- CategoryTheory.Limits.Types.colimitEquivColimitType_applystatement and proof · cited by 1
- CategoryTheory.Limits.Types.colimitEquivColimitType_symm_applystatement · cited by 1
- CategoryTheory.Limits.Types.nonempty_of_nonempty_colimitproof · cited by 1
- CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_applystatement · cited by 0
- CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_symm_applystatement · cited by 0