C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫
      ((α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫
          (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) ≫
            (𝟙 X₁ ⊗ (β_ X₂ (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫
              (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
        ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom = (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫ tensor_μ C (X₁, X₂) (𝟙_ C, 𝟙_ C) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
dsimp [tensor_μ]
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
this :
  (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C))
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫
      ((α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫
          (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) ≫
            (𝟙 X₁ ⊗ (β_ X₂ (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫
              (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
        ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫
      ((α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫
          (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) ≫
            (𝟙 X₁ ⊗ (β_ X₂ (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫
              (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
        ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
have :
  (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫
      (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C)) :=
  by pure_coherence
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
this :
  (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C))
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (((((α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C))) ≫ (𝟙 X₁ ⊗ (β_ X₂ (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C))) ≫
          (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom)) ≫
        (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
      ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
this :
  (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C))
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫
      ((α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫
          (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) ≫
            (𝟙 X₁ ⊗ (β_ X₂ (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫
              (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
        ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
slice_rhs 1 3 => rw [this]
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (((((α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C))) ≫ (𝟙 X₁ ⊗ (β_ X₂ (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C))) ≫
          (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom)) ≫
        (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
      ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
this :
  (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C))
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (((((α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C))) ≫ (𝟙 X₁ ⊗ (β_ X₂ (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C))) ≫
          (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom)) ≫
        (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
      ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
clear this
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫
      (((𝟙 X₁ ⊗ (λ_ X₂).inv ⊗ 𝟙 (𝟙_ C)) ≫ (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom)) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
        ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (((((α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C))) ≫ (𝟙 X₁ ⊗ (β_ X₂ (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C))) ≫
          (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom)) ≫
        (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
      ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
slice_rhs 2 3 => rw [← tensor_comp, ← tensor_comp, comp_id, comp_id, rightUnitor_inv_braiding]
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫
      (𝟙 X₁ ⊗ (λ_ X₂).inv ⊗ 𝟙 (𝟙_ C)) ≫
        (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫
      (((𝟙 X₁ ⊗ (λ_ X₂).inv ⊗ 𝟙 (𝟙_ C)) ≫ (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom)) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
        ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
simp only [assoc]
no goals
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫
      (𝟙 X₁ ⊗ (λ_ X₂).inv ⊗ 𝟙 (𝟙_ C)) ≫
        (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom) ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)
coherence
no goals
C : Type u₁
inst✝⁸ : Category C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X₁ X₂ : C
⊢ (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).inv) ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫ (𝟙 X₁ ⊗ (ρ_ X₂).inv ⊗ 𝟙 (𝟙_ C))
pure_coherence