Theorems · Theorem · category theory

CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C),
  CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl F =
    CategoryTheory.Limits.pushout.inr
      (CategoryTheory.Limits.coprod.desc
        (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.one))
        (F.map CategoryTheory.Limits.WalkingParallelPairHom.left))
      (CategoryTheory.Limits.coprod.desc
        (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.one))
        (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))

Defined in

Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasBinaryCoproductsCategoryTheory.Limits.HasPushouts