Binary (co)products of type-valued functors

Defines an explicit construction of binary products and coproducts of type-valued functors.

Also defines isomorphisms to the categorical product and coproduct, respectively.

def CategoryTheory.FunctorToTypes.prod {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Functor C (Type w)

prod F G is the explicit binary product of type-valued functors F and G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.prod_obj {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (prod F G).obj a = (F.obj a × G.obj a)

@[simp]

theorem CategoryTheory.FunctorToTypes.prod_map {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (prod F G).map f = TypeCat.ofHom fun (a : F.obj X✝ × G.obj X✝) => ((ConcreteCategory.hom (F.map f)) a.1, (ConcreteCategory.hom (G.map f)) a.2)

def CategoryTheory.FunctorToTypes.prod.fst {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} : prod F G ⟶ F

The first projection of prod F G, onto F.

Equations

• CategoryTheory.FunctorToTypes.prod.fst = { app := fun (x : C) => TypeCat.ofHom fun (a : (CategoryTheory.FunctorToTypes.prod F G).obj x) => a.1, naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.fst_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (x✝ : C) : fst.app x✝ = TypeCat.ofHom fun (a : (prod F G).obj x✝) => a.1

def CategoryTheory.FunctorToTypes.prod.snd {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} : prod F G ⟶ G

The second projection of prod F G, onto G.

Equations

• CategoryTheory.FunctorToTypes.prod.snd = { app := fun (x : C) => TypeCat.ofHom fun (a : (CategoryTheory.FunctorToTypes.prod F G).obj x) => a.2, naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.snd_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (x✝ : C) : snd.app x✝ = TypeCat.ofHom fun (a : (prod F G).obj x✝) => a.2

def CategoryTheory.FunctorToTypes.prod.lift {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) : F ⟶ prod F₁ F₂

Given natural transformations F ⟶ F₁ and F ⟶ F₂, construct a natural transformation F ⟶ prod F₁ F₂.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.lift_app {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) (x : C) : (lift τ₁ τ₂).app x = TypeCat.ofHom fun (y : F.obj x) => ((ConcreteCategory.hom (τ₁.app x)) y, (ConcreteCategory.hom (τ₂.app x)) y)

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.lift_fst {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) : CategoryStruct.comp (lift τ₁ τ₂) fst = τ₁

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.lift_snd {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) : CategoryStruct.comp (lift τ₁ τ₂) snd = τ₂

def CategoryTheory.FunctorToTypes.binaryProductCone {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.BinaryFan F G

The binary fan whose point is prod F G.

Equations

• CategoryTheory.FunctorToTypes.binaryProductCone F G = CategoryTheory.Limits.BinaryFan.mk CategoryTheory.FunctorToTypes.prod.fst CategoryTheory.FunctorToTypes.prod.snd

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductCone_pt_map_hom_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (a : F.obj X✝ × G.obj X✝) : (ConcreteCategory.hom ((binaryProductCone F G).pt.map f)) a = ((ConcreteCategory.hom (F.map f)) a.1, (ConcreteCategory.hom (G.map f)) a.2)

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductCone_π_app {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (x✝ : Discrete Limits.WalkingPair) : (binaryProductCone F G).π.app x✝ = match x✝.as with | Limits.WalkingPair.left => prod.fst | Limits.WalkingPair.right => prod.snd

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductCone_pt_obj {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (binaryProductCone F G).pt.obj a = (F.obj a × G.obj a)

def CategoryTheory.FunctorToTypes.binaryProductLimit {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.IsLimit (binaryProductCone F G)

prod F G is a limit cone.

Equations

• CategoryTheory.FunctorToTypes.binaryProductLimit F G = { lift := fun (s : CategoryTheory.Limits.BinaryFan F G) => CategoryTheory.FunctorToTypes.prod.lift s.fst s.snd, fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductLimit_lift {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (s : Limits.BinaryFan F G) : (binaryProductLimit F G).lift s = prod.lift s.fst s.snd

def CategoryTheory.FunctorToTypes.binaryProductLimitCone {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.LimitCone (Limits.pair F G)

prod F G is a binary product for F and G.

Equations

• CategoryTheory.FunctorToTypes.binaryProductLimitCone F G = { cone := CategoryTheory.FunctorToTypes.binaryProductCone F G, isLimit := CategoryTheory.FunctorToTypes.binaryProductLimit F G }

noncomputable def CategoryTheory.FunctorToTypes.binaryProductIso {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : F ⨯ G ≅ prod F G

The categorical binary product of type-valued functors is prod F G.

Equations

• CategoryTheory.FunctorToTypes.binaryProductIso F G = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.FunctorToTypes.binaryProductLimitCone F G)

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_hom_comp_fst {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp (binaryProductIso F G).hom prod.fst = Limits.prod.fst

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_hom_comp_snd {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp (binaryProductIso F G).hom prod.snd = Limits.prod.snd

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_fst {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp (binaryProductIso F G).inv Limits.prod.fst = prod.fst

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_fst_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : (prod F G).obj a) : (ConcreteCategory.hom (Limits.prod.fst.app a)) ((ConcreteCategory.hom ((binaryProductIso F G).inv.app a)) z) = z.1

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_snd {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp (binaryProductIso F G).inv Limits.prod.snd = prod.snd

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_snd_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : (prod F G).obj a) : (ConcreteCategory.hom (Limits.prod.snd.app a)) ((ConcreteCategory.hom ((binaryProductIso F G).inv.app a)) z) = z.2

noncomputable def CategoryTheory.FunctorToTypes.prodMk {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) : (F ⨯ G).obj a

Construct an element of (F ⨯ G).obj a from an element of F.obj a and an element of G.obj a.

Equations

• CategoryTheory.FunctorToTypes.prodMk x y = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryProductIso F G).inv.app a)) (x, y)

@[simp]

theorem CategoryTheory.FunctorToTypes.prodMk_fst {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) : (ConcreteCategory.hom (Limits.prod.fst.app a)) (prodMk x y) = x

@[simp]

theorem CategoryTheory.FunctorToTypes.prodMk_snd {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) : (ConcreteCategory.hom (Limits.prod.snd.app a)) (prodMk x y) = y

theorem CategoryTheory.FunctorToTypes.prod_ext {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (z w : (prod F G).obj a) (h1 : z.1 = w.1) (h2 : z.2 = w.2) : z = w

theorem CategoryTheory.FunctorToTypes.prod_ext_iff {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} {z w : (prod F G).obj a} : z = w ↔ z.1 = w.1 ∧ z.2 = w.2

noncomputable def CategoryTheory.FunctorToTypes.binaryProductEquiv {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (F ⨯ G).obj a ≃ F.obj a × G.obj a

(F ⨯ G).obj a is in bijection with the product of F.obj a and G.obj a.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductEquiv_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : (F ⨯ G).obj a) : (binaryProductEquiv F G a) z = (((ConcreteCategory.hom ((binaryProductIso F G).hom.app a)) z).1, ((ConcreteCategory.hom ((binaryProductIso F G).hom.app a)) z).2)

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductEquiv_symm_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : F.obj a × G.obj a) : (binaryProductEquiv F G a).symm z = prodMk z.1 z.2

theorem CategoryTheory.FunctorToTypes.prod_ext' {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z w : (F ⨯ G).obj a) (h1 : (ConcreteCategory.hom (Limits.prod.fst.app a)) z = (ConcreteCategory.hom (Limits.prod.fst.app a)) w) (h2 : (ConcreteCategory.hom (Limits.prod.snd.app a)) z = (ConcreteCategory.hom (Limits.prod.snd.app a)) w) : z = w

theorem CategoryTheory.FunctorToTypes.prod_ext'_iff {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} {z w : (F ⨯ G).obj a} : z = w ↔ (ConcreteCategory.hom (Limits.prod.fst.app a)) z = (ConcreteCategory.hom (Limits.prod.fst.app a)) w ∧ (ConcreteCategory.hom (Limits.prod.snd.app a)) z = (ConcreteCategory.hom (Limits.prod.snd.app a)) w

def CategoryTheory.FunctorToTypes.coprod {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Functor C (Type w)

coprod F G is the explicit binary coproduct of type-valued functors F and G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod_map {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (coprod F G).map f = TypeCat.ofHom (Sum.map ⇑(ConcreteCategory.hom (F.map f)) ⇑(ConcreteCategory.hom (G.map f)))

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod_obj {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (coprod F G).obj a = (F.obj a ⊕ G.obj a)

def CategoryTheory.FunctorToTypes.coprod.inl {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} : F ⟶ coprod F G

The left inclusion of F into coprod F G.

Equations

• CategoryTheory.FunctorToTypes.coprod.inl = { app := fun (x : C) => TypeCat.ofHom fun (x_1 : F.obj x) => Sum.inl x_1, naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.inl_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (x✝ : C) : inl.app x✝ = TypeCat.ofHom fun (x : F.obj x✝) => Sum.inl x

def CategoryTheory.FunctorToTypes.coprod.inr {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} : G ⟶ coprod F G

The right inclusion of G into coprod F G.

Equations

• CategoryTheory.FunctorToTypes.coprod.inr = { app := fun (x : C) => TypeCat.ofHom fun (x_1 : G.obj x) => Sum.inr x_1, naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.inr_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (x✝ : C) : inr.app x✝ = TypeCat.ofHom fun (x : G.obj x✝) => Sum.inr x

def CategoryTheory.FunctorToTypes.coprod.desc {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) : coprod F₁ F₂ ⟶ F

Given natural transformations F₁ ⟶ F and F₂ ⟶ F, construct a natural transformation coprod F₁ F₂ ⟶ F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.desc_app {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) (a : C) : (desc τ₁ τ₂).app a = TypeCat.ofHom (Sum.elim ⇑(ConcreteCategory.hom (τ₁.app a)) ⇑(ConcreteCategory.hom (τ₂.app a)))

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.desc_inl {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) : CategoryStruct.comp inl (desc τ₁ τ₂) = τ₁

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.desc_inr {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) : CategoryStruct.comp inr (desc τ₁ τ₂) = τ₂

def CategoryTheory.FunctorToTypes.binaryCoproductCocone {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.BinaryCofan F G

The binary cofan whose point is coprod F G.

Equations

• CategoryTheory.FunctorToTypes.binaryCoproductCocone F G = CategoryTheory.Limits.BinaryCofan.mk CategoryTheory.FunctorToTypes.coprod.inl CategoryTheory.FunctorToTypes.coprod.inr

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_map_hom_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (a✝ : F.obj X✝ ⊕ G.obj X✝) : (ConcreteCategory.hom ((binaryCoproductCocone F G).pt.map f)) a✝ = Sum.map (⇑(ConcreteCategory.hom (F.map f))) (⇑(ConcreteCategory.hom (G.map f))) a✝

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductCocone_ι_app {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (x✝ : Discrete Limits.WalkingPair) : (binaryCoproductCocone F G).ι.app x✝ = match x✝.as with | Limits.WalkingPair.left => coprod.inl | Limits.WalkingPair.right => coprod.inr

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_obj {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (binaryCoproductCocone F G).pt.obj a = (F.obj a ⊕ G.obj a)

def CategoryTheory.FunctorToTypes.binaryCoproductColimit {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.IsColimit (binaryCoproductCocone F G)

coprod F G is a colimit cocone.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductColimit_desc {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (s : Limits.BinaryCofan F G) : (binaryCoproductColimit F G).desc s = coprod.desc s.inl s.inr

def CategoryTheory.FunctorToTypes.binaryCoproductColimitCocone {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.ColimitCocone (Limits.pair F G)

coprod F G is a binary coproduct for F and G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.FunctorToTypes.binaryCoproductIso {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : F ⨿ G ≅ coprod F G

The categorical binary coproduct of type-valued functors is coprod F G.

Equations

• CategoryTheory.FunctorToTypes.binaryCoproductIso F G = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.FunctorToTypes.binaryCoproductColimitCocone F G)

@[simp]

theorem CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_hom {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp Limits.coprod.inl (binaryCoproductIso F G).hom = coprod.inl

@[simp]

theorem CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_hom_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (x : F.obj a) : (ConcreteCategory.hom ((binaryCoproductIso F G).hom.app a)) ((ConcreteCategory.hom (Limits.coprod.inl.app a)) x) = Sum.inl x

@[simp]

theorem CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_hom {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp Limits.coprod.inr (binaryCoproductIso F G).hom = coprod.inr

@[simp]

theorem CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_hom_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (x : G.obj a) : (ConcreteCategory.hom ((binaryCoproductIso F G).hom.app a)) ((ConcreteCategory.hom (Limits.coprod.inr.app a)) x) = Sum.inr x

@[simp]

theorem CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_inv {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp coprod.inl (binaryCoproductIso F G).inv = Limits.coprod.inl

@[simp]

theorem CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_inv_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (x : F.obj a) : (ConcreteCategory.hom ((binaryCoproductIso F G).inv.app a)) (Sum.inl x) = (ConcreteCategory.hom (Limits.coprod.inl.app a)) x

@[simp]

theorem CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_inv {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp coprod.inr (binaryCoproductIso F G).inv = Limits.coprod.inr

@[simp]

theorem CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_inv_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (x : G.obj a) : (ConcreteCategory.hom ((binaryCoproductIso F G).inv.app a)) (Sum.inr x) = (ConcreteCategory.hom (Limits.coprod.inr.app a)) x

@[reducible, inline]

noncomputable abbrev CategoryTheory.FunctorToTypes.coprodInl {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : F.obj a) : (F ⨿ G).obj a

Construct an element of (F ⨿ G).obj a from an element of F.obj a

Equations

• CategoryTheory.FunctorToTypes.coprodInl x = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a)) (Sum.inl x)

@[reducible, inline]

noncomputable abbrev CategoryTheory.FunctorToTypes.coprodInr {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : G.obj a) : (F ⨿ G).obj a

Construct an element of (F ⨿ G).obj a from an element of G.obj a

Equations

• CategoryTheory.FunctorToTypes.coprodInr x = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a)) (Sum.inr x)

noncomputable def CategoryTheory.FunctorToTypes.binaryCoproductEquiv {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (F ⨿ G).obj a ≃ F.obj a ⊕ G.obj a

(F ⨿ G).obj a is in bijection with disjoint union of F.obj a and G.obj a.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductEquiv_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : (F ⨿ G).obj a) : (binaryCoproductEquiv F G a) z = (ConcreteCategory.hom ((binaryCoproductIso F G).hom.app a)) z

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductEquiv_symm_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : F.obj a ⊕ G.obj a) : (binaryCoproductEquiv F G a).symm z = (ConcreteCategory.hom ((binaryCoproductIso F G).inv.app a)) z