category-theoretic triviality

Stream: Is there code for X?

[Kevin Buzzard]

I am at the goal at the sorry below and I want to reduce to commutes. What am I missing?

import category_theory.functor.basic

open category_theory

example {𝒞 : Type} [category 𝒞] {A B C D E P Q R : 𝒞} (f : A ⟶ B) (g : B ⟶ C) (h : C ⟶ D) (i : D ⟶ E)
(φ : A ⟶ P) (ψ : P ⟶ Q) (ρ : Q ⟶ R) (σ : R ⟶ D) (commutes : f ≫ g ≫ h = φ ≫ ψ ≫ ρ ≫ σ) :
f ≫ g ≫ h ≫ i = φ ≫ ψ ≫ ρ ≫ σ ≫ i :=
begin
  sorry
end

I don't want to have to do suffices : f \gg g \gg h \gg blah blah because in reality most of these functions are things like eq_to_hom _ and I don't really want to switch proof terms on because they're full of horner.

[Kevin Buzzard]

The problem with

example {𝒞 : Type} [category 𝒞] {A B C D E P Q R : 𝒞} (f : A ⟶ B) (g : B ⟶ C) (h : C ⟶ D) (i : D ⟶ E)
(φ : A ⟶ P) (ψ : P ⟶ Q) (ρ : Q ⟶ R) (σ : R ⟶ D) (commutes : f ≫ g ≫ h = φ ≫ ψ ≫ ρ ≫ σ) :
f ≫ g ≫ h ≫ i = φ ≫ ψ ≫ ρ ≫ σ ≫ i :=
begin
  simp only [ ← category.assoc] at commutes ⊢,
  rw commutes,
end

is that in practice I don't have commutes to hand, it's what I want to reduce the goal to, and I can't guarantee how many >>s I'll have next time.

[Kevin Buzzard]

Oh I've got it

  simp only [← category.assoc],
  congr' 1,

[Adam Topaz]

@Kevin Buzzard do you know about reassoc_of?

[Adam Topaz]

import category_theory.functor.basic

open category_theory

example {𝒞 : Type} [category 𝒞] {A B C D E P Q R : 𝒞} (f : A ⟶ B) (g : B ⟶ C) (h : C ⟶ D) (i : D ⟶ E)
(φ : A ⟶ P) (ψ : P ⟶ Q) (ρ : Q ⟶ R) (σ : R ⟶ D) (commutes : f ≫ g ≫ h = φ ≫ ψ ≫ ρ ≫ σ) :
f ≫ g ≫ h ≫ i = φ ≫ ψ ≫ ρ ≫ σ ≫ i :=
by simp [reassoc_of commutes]

[Kevin Buzzard]

tactic#category_theory.reassoc_of

[Kevin Buzzard]

Neither a tactic nor a metaprogram!

[Kevin Buzzard]

But I don't want to type simp [reassoc_of _], in my position because _ is horrible.

[Kevin Buzzard]

That's really nice though!

[Adam Topaz]

tactic#slice (and rhs) might also be helpful

[Adam Topaz]

E.g.

example {𝒞 : Type} [category 𝒞] {A B C D E P Q R : 𝒞} (f : A ⟶ B) (g : B ⟶ C) (h : C ⟶ D) (i : D ⟶ E)
(φ : A ⟶ P) (ψ : P ⟶ Q) (ρ : Q ⟶ R) (σ : R ⟶ D) (commutes : f ≫ g ≫ h = φ ≫ ψ ≫ ρ ≫ σ) :
f ≫ g ≫ h ≫ i = φ ≫ ψ ≫ ρ ≫ σ ≫ i :=
begin
  slice_lhs 0 2
  { rw commutes },
  simp,
end