Documentation

Mathlib.CategoryTheory.ChosenFiniteProducts.Over

ChosenFiniteProducts for Over X #

We provide a ChosenFiniteProducts (Over X) instance via pullbacks, and provide simp lemmas for the induced MonoidalCategory (Over X) instance.

source
@[reducible]
noncomputable def CategoryTheory.Over.chosenFiniteProducts {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] (X : C) :
ChosenFiniteProducts (Over X)

A choice of finite products of Over X given by Limits.pullback.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.Over.tensorObj_ext {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X R : C} {S T : Over X} (f₁ f₂ : R ⟶ (MonoidalCategoryStruct.tensorObj S T).left) (e₁ : CategoryStruct.comp f₁ (Limits.pullback.fst S.hom T.hom) = CategoryStruct.comp f₂ (Limits.pullback.fst S.hom T.hom)) (e₂ : CategoryStruct.comp f₁ (Limits.pullback.snd S.hom T.hom) = CategoryStruct.comp f₂ (Limits.pullback.snd S.hom T.hom)) :
    f₁ = f₂
    source
    theorem CategoryTheory.Over.tensorObj_ext_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X R : C} {S T : Over X} {f₁ f₂ : R ⟶ (MonoidalCategoryStruct.tensorObj S T).left} :
    f₁ = f₂ ↔ CategoryStruct.comp f₁ (Limits.pullback.fst S.hom T.hom) = CategoryStruct.comp f₂ (Limits.pullback.fst S.hom T.hom) ∧ CategoryStruct.comp f₁ (Limits.pullback.snd S.hom T.hom) = CategoryStruct.comp f₂ (Limits.pullback.snd S.hom T.hom)
    source
    @[simp]
    theorem CategoryTheory.Over.tensorObj_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S : Over X) :
    (MonoidalCategoryStruct.tensorObj R S).left = Limits.pullback R.hom S.hom
    source
    @[simp]
    theorem CategoryTheory.Over.tensorObj_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S : Over X) :
    (MonoidalCategoryStruct.tensorObj R S).hom = CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom
    source
    @[simp]
    theorem CategoryTheory.Over.tensorUnit_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} :
    (MonoidalCategoryStruct.tensorUnit (Over X)).left = X
    source
    @[simp]
    theorem CategoryTheory.Over.tensorUnit_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} :
    (MonoidalCategoryStruct.tensorUnit (Over X)).hom = CategoryStruct.id X
    source
    @[simp]
    theorem CategoryTheory.Over.lift_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : R ⟶ S) (g : R ⟶ T) :
    (ChosenFiniteProducts.lift f g).left = Limits.pullback.lift f.left g.left ⋯
    source
    @[simp]
    theorem CategoryTheory.Over.toUnit_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R : Over X} :
    (ChosenFiniteProducts.toUnit R).left = R.hom
    source
    @[simp]
    theorem CategoryTheory.Over.associator_hom_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (Limits.pullback.fst R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) = CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (Limits.pullback.fst R.hom S.hom)
    source
    @[simp]
    theorem CategoryTheory.Over.associator_hom_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : R.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (Limits.pullback.fst R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) h) = CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) h)
    source
    @[simp]
    theorem CategoryTheory.Over.associator_hom_left_snd_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (Limits.pullback.snd R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) (Limits.pullback.fst S.hom T.hom)) = CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (Limits.pullback.snd R.hom S.hom)
    source
    @[simp]
    theorem CategoryTheory.Over.associator_hom_left_snd_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : S.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (Limits.pullback.snd R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) h)) = CategoryStruct.comp (Limits.pullback.fst (MonoidalCategoryStruct.tensorObj R S).hom T.hom) (CategoryStruct.comp (Limits.pullback.snd R.hom S.hom) h)
    source
    @[simp]
    theorem CategoryTheory.Over.associator_hom_left_snd_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (Limits.pullback.snd R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) (Limits.pullback.snd S.hom T.hom)) = Limits.pullback.snd (MonoidalCategoryStruct.tensorObj R S).hom T.hom
    source
    @[simp]
    theorem CategoryTheory.Over.associator_hom_left_snd_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : T.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).hom.left (CategoryStruct.comp (Limits.pullback.snd R.hom (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) S.hom)) (CategoryStruct.comp (Limits.pullback.snd S.hom T.hom) h)) = CategoryStruct.comp (Limits.pullback.snd (MonoidalCategoryStruct.tensorObj R S).hom T.hom) h
    source
    @[simp]
    theorem CategoryTheory.Over.associator_inv_left_fst_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) (Limits.pullback.fst R.hom S.hom)) = Limits.pullback.fst R.hom (MonoidalCategoryStruct.tensorObj S T).hom
    source
    @[simp]
    theorem CategoryTheory.Over.associator_inv_left_fst_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : R.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) h)) = CategoryStruct.comp (Limits.pullback.fst R.hom (MonoidalCategoryStruct.tensorObj S T).hom) h
    source
    @[simp]
    theorem CategoryTheory.Over.associator_inv_left_fst_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) (Limits.pullback.snd R.hom S.hom)) = CategoryStruct.comp (Limits.pullback.snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (Limits.pullback.fst S.hom T.hom)
    source
    @[simp]
    theorem CategoryTheory.Over.associator_inv_left_fst_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : S.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) (CategoryStruct.comp (Limits.pullback.snd R.hom S.hom) h)) = CategoryStruct.comp (Limits.pullback.snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (CategoryStruct.comp (Limits.pullback.fst S.hom T.hom) h)
    source
    @[simp]
    theorem CategoryTheory.Over.associator_inv_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (Limits.pullback.snd (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) = CategoryStruct.comp (Limits.pullback.snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (Limits.pullback.snd S.hom T.hom)
    source
    @[simp]
    theorem CategoryTheory.Over.associator_inv_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (R S T : Over X) {Z : C} (h : T.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.associator R S T).inv.left (CategoryStruct.comp (Limits.pullback.snd (CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) R.hom) T.hom) h) = CategoryStruct.comp (Limits.pullback.snd R.hom (MonoidalCategoryStruct.tensorObj S T).hom) (CategoryStruct.comp (Limits.pullback.snd S.hom T.hom) h)
    source
    @[simp]
    theorem CategoryTheory.Over.leftUnitor_hom_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
    (MonoidalCategoryStruct.leftUnitor Y).hom.left = Limits.pullback.snd (MonoidalCategoryStruct.tensorUnit (Over X)).hom Y.hom
    source
    @[simp]
    theorem CategoryTheory.Over.leftUnitor_inv_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (Limits.pullback.fst (CategoryStruct.id X) Y.hom) = Y.hom
    source
    @[simp]
    theorem CategoryTheory.Over.leftUnitor_inv_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) {Z : C} (h : X ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (CategoryStruct.comp (Limits.pullback.fst (CategoryStruct.id X) Y.hom) h) = CategoryStruct.comp Y.hom h
    source
    @[simp]
    theorem CategoryTheory.Over.leftUnitor_inv_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (Limits.pullback.snd (CategoryStruct.id X) Y.hom) = CategoryStruct.id Y.left
    source
    @[simp]
    theorem CategoryTheory.Over.leftUnitor_inv_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) {Z : C} (h : Y.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv.left (CategoryStruct.comp (Limits.pullback.snd (CategoryStruct.id X) Y.hom) h) = h
    source
    @[simp]
    theorem CategoryTheory.Over.rightUnitor_hom_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
    (MonoidalCategoryStruct.rightUnitor Y).hom.left = Limits.pullback.fst Y.hom (CategoryStruct.id X)
    source
    @[simp]
    theorem CategoryTheory.Over.rightUnitor_inv_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (Limits.pullback.fst Y.hom (CategoryStruct.id X)) = CategoryStruct.id Y.left
    source
    @[simp]
    theorem CategoryTheory.Over.rightUnitor_inv_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) {Z : C} (h : Y.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (CategoryStruct.comp (Limits.pullback.fst Y.hom (CategoryStruct.id X)) h) = h
    source
    @[simp]
    theorem CategoryTheory.Over.rightUnitor_inv_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) :
    CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (Limits.pullback.snd Y.hom (CategoryStruct.id X)) = Y.hom
    source
    @[simp]
    theorem CategoryTheory.Over.rightUnitor_inv_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} (Y : Over X) {Z : C} (h : X ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).inv.left (CategoryStruct.comp (Limits.pullback.snd Y.hom (CategoryStruct.id X)) h) = CategoryStruct.comp Y.hom h
    source
    theorem CategoryTheory.Over.whiskerLeft_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
    (MonoidalCategoryStruct.whiskerLeft R f).left = Limits.pullback.map R.hom S.hom R.hom T.hom (CategoryStruct.id ((Functor.id C).obj R.left)) f.left (CategoryStruct.id ((Functor.fromPUnit X).obj R.right)) ⋯ ⋯
    source
    @[simp]
    theorem CategoryTheory.Over.whiskerLeft_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (Limits.pullback.fst R.hom T.hom) = Limits.pullback.fst R.hom S.hom
    source
    @[simp]
    theorem CategoryTheory.Over.whiskerLeft_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) {Z : C} (h : R.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (CategoryStruct.comp (Limits.pullback.fst R.hom T.hom) h) = CategoryStruct.comp (Limits.pullback.fst R.hom S.hom) h
    source
    @[simp]
    theorem CategoryTheory.Over.whiskerLeft_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (Limits.pullback.snd R.hom T.hom) = CategoryStruct.comp (Limits.pullback.snd R.hom S.hom) f.left
    source
    @[simp]
    theorem CategoryTheory.Over.whiskerLeft_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) {Z : C} (h : T.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R f).left (CategoryStruct.comp (Limits.pullback.snd R.hom T.hom) h) = CategoryStruct.comp (Limits.pullback.snd R.hom S.hom) (CategoryStruct.comp f.left h)
    source
    theorem CategoryTheory.Over.whiskerRight_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
    (MonoidalCategoryStruct.whiskerRight f R).left = Limits.pullback.map S.hom R.hom T.hom R.hom f.left (CategoryStruct.id ((Functor.id C).obj R.left)) (CategoryStruct.id ((Functor.fromPUnit X).obj S.right)) ⋯ ⋯
    source
    @[simp]
    theorem CategoryTheory.Over.whiskerRight_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (Limits.pullback.fst T.hom R.hom) = CategoryStruct.comp (Limits.pullback.fst S.hom R.hom) f.left
    source
    @[simp]
    theorem CategoryTheory.Over.whiskerRight_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) {Z : C} (h : T.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (CategoryStruct.comp (Limits.pullback.fst T.hom R.hom) h) = CategoryStruct.comp (Limits.pullback.fst S.hom R.hom) (CategoryStruct.comp f.left h)
    source
    @[simp]
    theorem CategoryTheory.Over.whiskerRight_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (Limits.pullback.snd T.hom R.hom) = Limits.pullback.snd S.hom R.hom
    source
    @[simp]
    theorem CategoryTheory.Over.whiskerRight_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T : Over X} (f : S ⟶ T) {Z : C} (h : R.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f R).left (CategoryStruct.comp (Limits.pullback.snd T.hom R.hom) h) = CategoryStruct.comp (Limits.pullback.snd S.hom R.hom) h
    source
    theorem CategoryTheory.Over.tensorHom_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) :
    (MonoidalCategoryStruct.tensorHom f g).left = Limits.pullback.map R.hom T.hom S.hom U.hom f.left g.left (CategoryStruct.id ((Functor.fromPUnit X).obj R.right)) ⋯ ⋯
    source
    @[simp]
    theorem CategoryTheory.Over.tensorHom_left_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) :
    CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (Limits.pullback.fst S.hom U.hom) = CategoryStruct.comp (Limits.pullback.fst R.hom T.hom) f.left
    source
    @[simp]
    theorem CategoryTheory.Over.tensorHom_left_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) {Z : C} (h : S.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (CategoryStruct.comp (Limits.pullback.fst S.hom U.hom) h) = CategoryStruct.comp (Limits.pullback.fst R.hom T.hom) (CategoryStruct.comp f.left h)
    source
    @[simp]
    theorem CategoryTheory.Over.tensorHom_left_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) :
    CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (Limits.pullback.snd S.hom U.hom) = CategoryStruct.comp (Limits.pullback.snd R.hom T.hom) g.left
    source
    @[simp]
    theorem CategoryTheory.Over.tensorHom_left_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S T U : Over X} (f : R ⟶ S) (g : T ⟶ U) {Z : C} (h : U.left ⟶ Z) :
    CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g).left (CategoryStruct.comp (Limits.pullback.snd S.hom U.hom) h) = CategoryStruct.comp (Limits.pullback.snd R.hom T.hom) (CategoryStruct.comp g.left h)
    source
    @[simp]
    theorem CategoryTheory.Over.braiding_hom_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S : Over X} :
    (β_ R S).hom.left = (Limits.pullbackSymmetry R.hom S.hom).hom
    source
    @[simp]
    theorem CategoryTheory.Over.braiding_inv_left {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {X : C} {R S : Over X} :
    (β_ R S).inv.left = (Limits.pullbackSymmetry S.hom R.hom).hom