C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (𝟙 Y' ⊗ η_ Y Y' ≫ (𝟙 Y ⊗ f)) ≫ (α_ Y' Y Z).inv ≫ (ε_ Y Y' ⊗ 𝟙 Z) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ ↑(tensorLeftHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ (𝟙 Y ⊗ f)) = (ρ_ Y').hom ≫ f
dsimp [tensorLeftHomEquiv]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ ((𝟙 Y' ⊗ η_ Y Y') ≫ (𝟙 Y' ⊗ 𝟙 Y ⊗ f)) ≫ (α_ Y' Y Z).inv ≫ (ε_ Y Y' ⊗ 𝟙 Z) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (𝟙 Y' ⊗ η_ Y Y' ≫ (𝟙 Y ⊗ f)) ≫ (α_ Y' Y Z).inv ≫ (ε_ Y Y' ⊗ 𝟙 Z) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
rw [id_tensor_comp]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (𝟙 Y' ⊗ η_ Y Y') ≫ (((α_ Y' Y Y').inv ≫ ((𝟙 Y' ⊗ 𝟙 Y) ⊗ f)) ≫ (ε_ Y Y' ⊗ 𝟙 Z)) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ ((𝟙 Y' ⊗ η_ Y Y') ≫ (𝟙 Y' ⊗ 𝟙 Y ⊗ f)) ≫ (α_ Y' Y Z).inv ≫ (ε_ Y Y' ⊗ 𝟙 Z) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
slice_lhs 2 3 => rw [associator_inv_naturality]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (𝟙 Y' ⊗ η_ Y Y') ≫ (α_ Y' Y Y').inv ≫ ((ε_ Y Y' ⊗ 𝟙 Y') ≫ (𝟙 (𝟙_ C) ⊗ f)) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (𝟙 Y' ⊗ η_ Y Y') ≫ (((α_ Y' Y Y').inv ≫ ((𝟙 Y' ⊗ 𝟙 Y) ⊗ f)) ≫ (ε_ Y Y' ⊗ 𝟙 Z)) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
slice_lhs 3 4 => rw [tensor_id, id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (((ρ_ Y').hom ≫ (λ_ Y').inv) ≫ (𝟙 (𝟙_ C) ⊗ f)) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (𝟙 Y' ⊗ η_ Y Y') ≫ (α_ Y' Y Y').inv ≫ ((ε_ Y Y' ⊗ 𝟙 Y') ≫ (𝟙 (𝟙_ C) ⊗ f)) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
slice_lhs 1 3 => rw [coevaluation_evaluation]
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (((ρ_ Y').hom ≫ (λ_ Y').inv) ≫ (𝟙 (𝟙_ C) ⊗ f)) ≫ (λ_ Z).hom = (ρ_ Y').hom ≫ f
simp