{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Core using (Category)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Categories.Category.Monoidal.CounitalCopy using (CounitalCopy)
open import Categories.Category.Restriction using (Restriction)
open import Data.Product using (_,_)

import Categories.Morphism.Reasoning as MR
import Categories.Morphism as M

-- Counital copy categories admit a non trivial restriction structure.

module Categories.Category.Monoidal.CounitalCopy.Restriction {o β„“ e} {π’ž : Category o β„“ e} {monoidal : Monoidal π’ž} {symmetric : Symmetric monoidal} (counitalCopy : CounitalCopy symmetric) where
  open Category π’ž
  open Symmetric symmetric
  open CounitalCopy counitalCopy
  open Equiv
  open M π’ž
  open MR π’ž
  open HomReasoning
  open import Categories.Category.Monoidal.Utilities monoidal
  open Shorthands
  open import Categories.Category.Monoidal.Properties monoidal
  open import Categories.Category.Monoidal.Braided.Properties braided using (braiding-coherence) renaming (module Shorthands to BraidedShorthands)
  open BraidedShorthands using (Οƒβ‡’)

  restriction : Restriction π’ž
  restriction = record
    { _↓ = _↓
    ; pidΚ³ = pidΚ³'
    ; ↓-comm = ↓-comm''
    ; ↓-denestΚ³ = ↓-denestΚ³'
    ; ↓-skew-comm = ↓-skew-comm'
    ; ↓-cong = Ξ» fβ‰ˆg β†’ refl⟩∘⟨ refl⟩∘⟨ βŠ—.F-resp-β‰ˆ (fβ‰ˆg , refl) ⟩∘⟨refl
    }
    where
      _↓ : βˆ€ {A B} β†’ A β‡’ B β†’ A β‡’ A
      _↓ {A} {B} f = Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ”
      pidΚ³' : βˆ€ {A B} {f : A β‡’ B} β†’ f ∘ f ↓ β‰ˆ f
      pidΚ³' {f = f} = begin 
        f ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ”         β‰ˆβŸ¨ extendΚ³ (sym unitorΛ‘-commute-from) ⟩ 
        Ξ»β‡’ ∘ (id βŠ—β‚ f) ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ (extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (id-comm-sym , id-comm) β—‹ βŠ—.homomorphism)) ⟩ 
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (id βŠ—β‚ f) ∘ (f βŠ—β‚ id) ∘ Ξ” β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ pullΛ‘ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (identityΛ‘ , identityΚ³)) ⟩ 
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ f) ∘ Ξ”              β‰ˆΛ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ natural f ⟩
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ Ξ” ∘ f                     β‰ˆβŸ¨ refl⟩∘⟨ (pullΛ‘ (sym Ξ΄-identityΛ‘)) ⟩ 
        Ξ»β‡’ ∘ λ⇐ ∘ f                                β‰ˆβŸ¨ cancelΛ‘ unitorΛ‘.isoΚ³ ⟩ 
        f                                          ∎
      ↓-comm' : βˆ€ {A B C} (f : A β‡’ B) (g : A β‡’ C) β†’ f ↓ ∘ g ↓ β‰ˆ Ξ»β‡’ ∘ (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ Ξ΄) βŠ—β‚ id) ∘ ((g βŠ—β‚ f) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
      ↓-comm' f g = begin 
        (Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ”) ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ pullΚ³ (pullΚ³ (pullΚ³ (extendΚ³ (sym unitorΛ‘-commute-from)))) ⟩ 
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ»β‡’ ∘ (id βŠ—β‚ Ξ”) ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (id-comm-sym , id-comm) β—‹ βŠ—.homomorphism) ⟩
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ (g βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (id-comm-sym , id-comm) β—‹ βŠ—.homomorphism) ⟩
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ extendΚ³ (sym unitorΛ‘-commute-from) ⟩
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ Ξ»β‡’ ∘ (id βŠ—β‚ (f βŠ—β‚ id)) ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ extendΚ³ (sym unitorΛ‘-commute-from) ⟩
        Ξ»β‡’ ∘ Ξ»β‡’ ∘ (id βŠ—β‚ (Ξ΄ βŠ—β‚ id)) ∘ (id βŠ—β‚ (f βŠ—β‚ id)) ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ helper ⟩
        Ξ»β‡’ ∘ Ξ»β‡’ ∘ (id βŠ—β‚ (Ξ΄ βŠ—β‚ id)) ∘ (Ξ΄ βŠ—β‚ id) ∘ Ξ±β‡’ ∘ ((id βŠ—β‚ f) βŠ—β‚ id) ∘ ((g βŠ—β‚ id) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ (pullΛ‘ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (identityΛ‘ , identityΚ³)) β—‹ extendΚ³ (sym assoc-commute-from)) ⟩ 
        Ξ»β‡’ ∘ Ξ»β‡’ ∘ Ξ±β‡’ ∘ ((Ξ΄ βŠ—β‚ Ξ΄) βŠ—β‚ id) ∘ ((id βŠ—β‚ f) βŠ—β‚ id) ∘ ((g βŠ—β‚ id) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullΛ‘ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ ((sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (identityΛ‘ , identityΚ³)) , identityΒ²)) ⟩
        Ξ»β‡’ ∘ Ξ»β‡’ ∘ Ξ±β‡’ ∘ ((Ξ΄ βŠ—β‚ Ξ΄) βŠ—β‚ id) ∘ ((g βŠ—β‚ f) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ” 
          β‰ˆβŸ¨ refl⟩∘⟨ (pullΛ‘ coherence₁) ⟩
        Ξ»β‡’ ∘ (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ Ξ΄) βŠ—β‚ id) ∘ ((g βŠ—β‚ f) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          ∎
          where
          helper : (id βŠ—β‚ (f βŠ—β‚ id)) ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ” β‰ˆ (Ξ΄ βŠ—β‚ id) ∘ Ξ±β‡’ ∘ ((id βŠ—β‚ f) βŠ—β‚ id) ∘ ((g βŠ—β‚ id) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          helper = begin 
            (id βŠ—β‚ (f βŠ—β‚ id)) ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
              β‰ˆβŸ¨ extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (id-comm-sym , id-comm) β—‹ βŠ—.homomorphism) ⟩
            (Ξ΄ βŠ—β‚ id) ∘ (id βŠ—β‚ (f βŠ—β‚ id)) ∘ (g βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
              β‰ˆΛ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ cancelΛ‘ associator.isoΚ³ ⟩
            (Ξ΄ βŠ—β‚ id) ∘ (id βŠ—β‚ (f βŠ—β‚ id)) ∘ (g βŠ—β‚ id) ∘ Ξ±β‡’ ∘ α⇐ ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
              β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc β—‹ sym Ξ”-assoc) ⟩
            (Ξ΄ βŠ—β‚ id) ∘ (id βŠ—β‚ (f βŠ—β‚ id)) ∘ (g βŠ—β‚ id) ∘ Ξ±β‡’ ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
              β‰ˆΛ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ extendΚ³ (assoc-commute-from β—‹ ∘-resp-β‰ˆΛ‘ (βŠ—.F-resp-β‰ˆ (refl , βŠ—.identity))) ⟩
            (Ξ΄ βŠ—β‚ id) ∘ (id βŠ—β‚ (f βŠ—β‚ id)) ∘ Ξ±β‡’ ∘ ((g βŠ—β‚ id) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
              β‰ˆβŸ¨ refl⟩∘⟨ extendΚ³ (sym assoc-commute-from) ⟩
            (Ξ΄ βŠ—β‚ id) ∘ Ξ±β‡’ ∘ ((id βŠ—β‚ f) βŠ—β‚ id) ∘ ((g βŠ—β‚ id) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
              ∎
      ↓-comm'' : βˆ€ {A B C} {f : A β‡’ B} {g : A β‡’ C} β†’ f ↓ ∘ g ↓ β‰ˆ g ↓ ∘ f ↓
      ↓-comm'' {f = f} {g} = begin 
        (Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ”) ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ ↓-comm' f g ⟩
        Ξ»β‡’ ∘ (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ Ξ΄) βŠ—β‚ id) ∘ ((g βŠ—β‚ f) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          β‰ˆΛ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullΛ‘ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (cocommutative , identityΒ²)) ⟩
        Ξ»β‡’ ∘ (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ Ξ΄) βŠ—β‚ id) ∘ ((g βŠ—β‚ f) βŠ—β‚ id) ∘ (Οƒβ‡’ βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ ((sym (braiding.β‡’.commute _)) , refl) β—‹ βŠ—.homomorphism) ⟩
        Ξ»β‡’ ∘ (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ Ξ΄) βŠ—β‚ id) ∘ (Οƒβ‡’ βŠ—β‚ id) ∘ ((f βŠ—β‚ g) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ ((sym (braiding.β‡’.commute _)) , refl) β—‹ βŠ—.homomorphism) ⟩
        Ξ»β‡’ ∘ (Ξ»β‡’ βŠ—β‚ id) ∘ (Οƒβ‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ Ξ΄) βŠ—β‚ id) ∘ ((f βŠ—β‚ g) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ (pullΛ‘ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ ((braiding-coherence β—‹ sym coherence₃) , identityΒ²))) ⟩
        Ξ»β‡’ ∘ (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ Ξ΄) βŠ—β‚ id) ∘ ((f βŠ—β‚ g) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          β‰ˆΛ˜βŸ¨ ↓-comm' g f ⟩
        (Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ Ξ”) ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ” 
          ∎
      ↓-denestΚ³' : βˆ€ {A B C} {f : A β‡’ B} {g : A β‡’ C} β†’ (g ∘ f ↓) ↓ β‰ˆ g ↓ ∘ f ↓
      ↓-denestΚ³' {f = f} {g} = begin
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ ((g ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ”) βŠ—β‚ id) ∘ Ξ”
          β‰ˆΛ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ ∘-resp-β‰ˆΛ‘ (βŠ—.F-resp-β‰ˆ ((assoc β—‹ assoc β—‹ assoc) , elimΛ‘ (elimΛ‘ (elimΛ‘ identityΒ²)))) ⟩
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (((((g ∘ Ξ»β‡’) ∘ (Ξ΄ βŠ—β‚ id)) ∘ (f βŠ—β‚ id)) ∘ Ξ”) βŠ—β‚ ((((id ∘ id) ∘ id) ∘ id) ∘ id)) ∘ Ξ”
          β‰ˆΛ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ (pullΛ‘ (sym βŠ—.homomorphism) β—‹ pullΛ‘ (sym βŠ—.homomorphism) β—‹ pullΛ‘ (sym βŠ—.homomorphism) β—‹ pullΛ‘ (sym βŠ—.homomorphism)) ⟩
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ id) βŠ—β‚ id) ∘ ((f βŠ—β‚ id) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ helper ⟩ 
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ Ξ»β‡’ ∘ (id βŠ—β‚ Ξ”) ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ”
          β‰ˆΛ˜βŸ¨ pullΚ³ (pullΚ³ (pullΚ³ (extendΚ³ (sym unitorΛ‘-commute-from)))) ⟩ 
        (Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ Ξ”) ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ” 
          ∎
          where
          helper : (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ id) βŠ—β‚ id) ∘ ((f βŠ—β‚ id) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ” β‰ˆ Ξ»β‡’ ∘ (id βŠ—β‚ Ξ”) ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ”
          helper = begin 
            (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ id) βŠ—β‚ id) ∘ ((f βŠ—β‚ id) βŠ—β‚ id) ∘ (Ξ” βŠ—β‚ id) ∘ Ξ”
              β‰ˆΛ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc β—‹ sym Ξ”-assoc) ⟩ 
            (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ id) βŠ—β‚ id) ∘ ((f βŠ—β‚ id) βŠ—β‚ id) ∘ α⇐ ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
              β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ extendΚ³ (sym assoc-commute-to β—‹ ∘-resp-β‰ˆΚ³ (βŠ—.F-resp-β‰ˆ (refl , βŠ—.identity))) ⟩ 
            (Ξ»β‡’ βŠ—β‚ id) ∘ ((Ξ΄ βŠ—β‚ id) βŠ—β‚ id) ∘ α⇐ ∘ (f βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
              β‰ˆβŸ¨ refl⟩∘⟨ extendΚ³ (sym assoc-commute-to β—‹ ∘-resp-β‰ˆΚ³ (βŠ—.F-resp-β‰ˆ (refl , βŠ—.identity))) ⟩ 
            (Ξ»β‡’ βŠ—β‚ id) ∘ α⇐ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
              β‰ˆΛ˜βŸ¨ pullΛ‘ coherence₁ ⟩ 
            Ξ»β‡’ ∘ Ξ±β‡’ ∘ α⇐ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
              β‰ˆβŸ¨ refl⟩∘⟨ cancelΛ‘ associator.isoΚ³ ⟩
            Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ Ξ”
              β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (id-comm , id-comm-sym) β—‹ βŠ—.homomorphism) ⟩ 
            Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (id βŠ—β‚ Ξ”) ∘ (f βŠ—β‚ id) ∘ Ξ”
              β‰ˆβŸ¨ refl⟩∘⟨ extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (id-comm , id-comm-sym) β—‹ βŠ—.homomorphism) ⟩ 
            Ξ»β‡’ ∘ (id βŠ—β‚ Ξ”) ∘ (Ξ΄ βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ” 
              ∎
      ↓-skew-comm' : βˆ€ {A B C} {f : A β‡’ B} {g : B β‡’ C} β†’ g ↓ ∘ f β‰ˆ f ∘ (g ∘ f) ↓
      ↓-skew-comm' {f = f} {g} = begin 
        (Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ Ξ”) ∘ f                   
          β‰ˆβŸ¨ pullΚ³ (pullΚ³ (pullΚ³ (natural f))) ⟩ 
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (f βŠ—β‚ f) ∘ Ξ”              
          β‰ˆΛ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullΛ‘ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (identityΛ‘ , identityΚ³)) ⟩ 
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (id βŠ—β‚ f) ∘ (f βŠ—β‚ id) ∘ Ξ” 
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ (extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (id-comm , id-comm-sym) β—‹ βŠ—.homomorphism)) ⟩ 
        Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (id βŠ—β‚ f) ∘ (g βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ” 
          β‰ˆβŸ¨ refl⟩∘⟨ (extendΚ³ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (id-comm , id-comm-sym) β—‹ βŠ—.homomorphism)) ⟩  
        Ξ»β‡’ ∘ (id βŠ—β‚ f) ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ” 
          β‰ˆβŸ¨ extendΚ³ unitorΛ‘-commute-from ⟩ 
        f ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ (g βŠ—β‚ id) ∘ (f βŠ—β‚ id) ∘ Ξ”         
          β‰ˆβŸ¨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullΛ‘ (sym βŠ—.homomorphism β—‹ βŠ—.F-resp-β‰ˆ (refl , identityΒ²)) ⟩ 
        f ∘ Ξ»β‡’ ∘ (Ξ΄ βŠ—β‚ id) ∘ ((g ∘ f) βŠ—β‚ id) ∘ Ξ”               
          ∎