Theorems · Definition · category theory
CategoryTheory.Limits.PushoutCocone.eta
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
{X Y Z : C} →
{f : X ⟶ Y} →
{g : X ⟶ Z} →
(t : CategoryTheory.Limits.PushoutCocone f g) → t ≅ CategoryTheory.Limits.PushoutCocone.mk t.inl t.inr ⋯The natural isomorphism between a pushout cocone and the corresponding pushout cocone
reconstructed using PushoutCocone.mk.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Isostatement · cited by 3,963
- CategoryTheory.Limits.Cocone.ptstatement and proof · cited by 1,354
- CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
- CategoryTheory.Iso.reflproof · cited by 727
- CategoryTheory.Limits.WalkingSpanstatement · cited by 300
- CategoryTheory.Limits.spanstatement · cited by 294
- CategoryTheory.Limits.PushoutCocone.mkstatement · cited by 89
- CategoryTheory.Limits.PushoutCoconestatement and proof · cited by 66
- CategoryTheory.Limits.PushoutCocone.inlstatement · cited by 58
- CategoryTheory.Limits.PushoutCocone.inrstatement · cited by 58
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.pushoutCoconeEquivBinaryCofanproof · cited by 7
- CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIsostatement · cited by 0
- CategoryTheory.Limits.PushoutCocone.mkSelfIsColimitproof · cited by 0
- CategoryTheory.Limits.PushoutCocone.eta_hom_homstatement and proof · cited by 0
- CategoryTheory.Limits.PushoutCocone.eta_inv_homstatement and proof · cited by 0