Theorems · Theorem · category theory

CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId_inv_app_app

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (X : CategoryTheory.Functor C A) (X_1 : C),
  ((CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId C A).inv.app X).app X_1 =
    CategoryTheory.Limits.Sigma.ι (fun x => X.obj X_1) PUnit.unit

Defined in

Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasCoproducts