no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
coherence
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (𝟙 ((𝟙_ C ⊗ X) ⊗ 𝟙_ C) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫
        ((β_ (𝟙_ C) X).hom ⊗ 𝟙 (𝟙_ C)) ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
(slice_rhs 3 4 => rw [← comp_tensor_id, Iso.hom_inv_id, tensor_id])
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (𝟙 ((𝟙_ C ⊗ X) ⊗ 𝟙_ C) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
rw [id_comp]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (𝟙 ((𝟙_ C ⊗ X) ⊗ 𝟙_ C) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫
        ((β_ (𝟙_ C) X).hom ⊗ 𝟙 (𝟙_ C)) ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
slice_rhs 3 4 => rw [← comp_tensor_id, Iso.hom_inv_id, tensor_id]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((((α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C))) ≫
        (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫
      (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫
      (β_ (𝟙_ C ⊗ tensorUnit') X).hom ≫
        (α_ X (𝟙_ C) tensorUnit').inv ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 tensorUnit') ≫ (α_ (𝟙_ C) X tensorUnit').hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫
        ((β_ (𝟙_ C) X).hom ⊗ 𝟙 (𝟙_ C)) ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫
      (β_ (𝟙_ C ⊗ tensorUnit') X).hom ≫
        (α_ X (𝟙_ C) tensorUnit').inv ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 tensorUnit') ≫ (α_ (𝟙_ C) X tensorUnit').hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
(slice_lhs 1 3 => rw [← hexagon_reverse])
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((((α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C))) ≫
        (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫
      (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫
      (β_ (𝟙_ C ⊗ tensorUnit') X).hom ≫
        (α_ X (𝟙_ C) tensorUnit').inv ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 tensorUnit') ≫ (α_ (𝟙_ C) X tensorUnit').hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
simp only [assoc]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((((α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C))) ≫
        (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫
      (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫
      (β_ (𝟙_ C ⊗ tensorUnit') X).hom ≫
        (α_ X (𝟙_ C) tensorUnit').inv ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 tensorUnit') ≫ (α_ (𝟙_ C) X tensorUnit').hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (𝟙 (𝟙_ C) ⊗ (β_ (𝟙_ C) X).hom) ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫
        ((β_ (𝟙_ C) X).hom ⊗ 𝟙 (𝟙_ C)) ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫
      (β_ (𝟙_ C ⊗ tensorUnit') X).hom ≫
        (α_ X (𝟙_ C) tensorUnit').inv ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 tensorUnit') ≫ (α_ (𝟙_ C) X tensorUnit').hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom)
slice_lhs 1 3 => rw [← hexagon_reverse]
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) tensorUnit' X).inv ≫
      (β_ (𝟙_ C ⊗ tensorUnit') X).hom ≫
        (α_ X (𝟙_ C) tensorUnit').inv ≫
          ((β_ (𝟙_ C) X).inv ⊗ 𝟙 tensorUnit') ≫ (α_ (𝟙_ C) X tensorUnit').hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫ (β_ (𝟙_ C ⊗ tensorUnit') X).hom ≫ (𝟙 X ⊗ (ρ_ (𝟙_ C)).hom) ≫ (β_ (𝟙_ C) X).inv
rw [braiding_rightUnitor_aux₁]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) tensorUnit' X).inv ≫ (((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ (𝟙_ C) X).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫ ((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) tensorUnit' X).inv ≫ (β_ (𝟙_ C ⊗ tensorUnit') X).hom ≫ (𝟙 X ⊗ (ρ_ (𝟙_ C)).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫ ((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv
(slice_lhs 2 3 => rw [← braiding_naturality])
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) tensorUnit' X).inv ≫ (((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ (𝟙_ C) X).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫ ((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv
simp only [assoc]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) tensorUnit' X).inv ≫ (((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ (𝟙_ C) X).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫ ((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) tensorUnit' X).inv ≫ (β_ (𝟙_ C ⊗ tensorUnit') X).hom ≫ (𝟙 X ⊗ (ρ_ (𝟙_ C)).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫ ((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv
slice_lhs 2 3 => rw [← braiding_naturality]
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) tensorUnit' X).inv ≫ ((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) tensorUnit' X).inv ≫ ((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X)
rw [Iso.hom_inv_id, comp_id]
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) tensorUnit' X).inv ≫ ((ρ_ (𝟙_ C)).hom ⊗ 𝟙 X) = 𝟙 (𝟙_ C) ⊗ (λ_ X).hom
rw [triangle_assoc_comp_right]