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 =
    ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫
      ((α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫
          (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) ≫
            (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X₁).hom ⊗ 𝟙 X₂) ≫
              (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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 = ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ tensor_μ C (𝟙_ C, 𝟙_ C) (X₁, X₂) ≫ ((λ_ 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 :
  ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) =
    𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂
⊢ (λ_ (X₁ ⊗ X₂)).hom =
    ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫
      ((α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫
          (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) ≫
            (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X₁).hom ⊗ 𝟙 X₂) ≫
              (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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 =
    ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫
      ((α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫
          (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) ≫
            (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X₁).hom ⊗ 𝟙 X₂) ≫
              (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫
        ((λ_ X₁).hom ⊗ (λ_ X₂).hom)
have :
  ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫
      (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) =
    𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂ :=
  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 :
  ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) =
    𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂
⊢ (λ_ (X₁ ⊗ X₂)).hom =
    ((((𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂) ≫ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X₁).hom ⊗ 𝟙 X₂)) ≫ (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom)) ≫
        (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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 :
  ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) =
    𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂
⊢ (λ_ (X₁ ⊗ X₂)).hom =
    ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫
      ((α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫
          (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) ≫
            (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X₁).hom ⊗ 𝟙 X₂) ≫
              (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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 =
    ((((𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂) ≫ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X₁).hom ⊗ 𝟙 X₂)) ≫ (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom)) ≫
        (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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 :
  ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) =
    𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂
⊢ (λ_ (X₁ ⊗ X₂)).hom =
    ((((𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂) ≫ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X₁).hom ⊗ 𝟙 X₂)) ≫ (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom)) ≫
        (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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 =
    (((𝟙 (𝟙_ C) ⊗ (ρ_ X₁).inv ⊗ 𝟙 X₂) ≫ (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom)) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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 =
    ((((𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂) ≫ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X₁).hom ⊗ 𝟙 X₂)) ≫ (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom)) ≫
        (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫
      ((λ_ X₁).hom ⊗ (λ_ X₂).hom)
slice_rhs 1 2 => rw [← tensor_comp, ← tensor_comp, comp_id, comp_id, leftUnitor_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 =
    (𝟙 (𝟙_ C) ⊗ (ρ_ X₁).inv ⊗ 𝟙 X₂) ≫
      (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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 =
    (((𝟙 (𝟙_ C) ⊗ (ρ_ X₁).inv ⊗ 𝟙 X₂) ≫ (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom)) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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 =
    (𝟙 (𝟙_ C) ⊗ (ρ_ X₁).inv ⊗ 𝟙 X₂) ≫
      (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).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
⊢ ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ (𝟙 (𝟙_ C) ⊗ (α_ (𝟙_ C) X₁ X₂).inv) =
    𝟙 (𝟙_ C) ⊗ (λ_ X₁).inv ⊗ 𝟙 X₂
pure_coherence