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