{-# OPTIONS --safe #-}

{-
This file contians a proof that the smash product turns the universe
of pointed types into a symmetric monoidal precategory. The pentagon
and hexagon are proved in separate files due to the length of the
proofs. The remaining identities and the main result are proved here.
-}

module Cubical.HITs.SmashProduct.SymmetricMonoidal where

open import Cubical.HITs.SmashProduct.Base
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.Pushout.Base
open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.HITs.Wedge
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.Path
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.HITs.SmashProduct.Base
open import Cubical.HITs.SmashProduct.Pentagon
open import Cubical.HITs.SmashProduct.Hexagon
open import Cubical.Categories.Category.Precategory
  renaming (_×_ to _×'_)
open import Cubical.Data.Bool

open Precategory hiding (_∘_)
open Prefunctor
open isSymmetricPrecategory
open isMonoidalPrecategory
open PreNatIso
open PreNatTrans
open preIsIso


private
  variable
    ℓ ℓ' : Level
    A B : Pointed ℓ

⋀→∙-idfun : {A : Pointed ℓ} {B : Pointed ℓ'}
  → (_⋀→∙_ (idfun∙ A) (idfun∙ B)) ≡ idfun∙ (A ⋀∙ B)
⋀→∙-idfun =
  ΣPathP (funExt
    (⋀-fun≡ _ _ refl (λ _ → refl)
      (λ x → flipSquare (sym (rUnit (push (inl x)))))
      λ x → flipSquare (sym (rUnit (push (inr x)))))
                   , refl)

⋀→∙-comp : {A A' A'' B B' B'' : Pointed ℓ}
  (f : A →∙ A') (f' : A' →∙ A'')
  (g : B →∙ B') (g' : B' →∙ B'')
  → ((f' ∘∙ f) ⋀→∙ (g' ∘∙ g)) ≡ ((f' ⋀→∙ g') ∘∙ (f ⋀→∙ g))
⋀→∙-comp f f' g g' =
  ΣPathP ((funExt
   (⋀-fun≡ _ _ refl (λ _ → refl)
     (λ x → flipSquare
       (cong (push (inl (fst f' (fst f x))) ∙_)
         ((λ i j → cong-∙ (λ y → inr (fst f' (fst f x) , y))
                        (cong (fst g') (snd g)) (snd g') i (~ j))
        ∙ symDistr (cong (λ y → inr (fst f' (fst f x) , y))
                          (λ i → fst g' (snd g i)))
                    (cong (λ y → inr (fst f' (fst f x) , y)) (snd g')))
       ∙ assoc _ _ _
       ∙∙ (λ j → (push (inl (fst f' (fst f x)))
           ∙ (λ j → inr (fst f' (fst f x) , snd g' (~ j))))
           ∙ λ j → inr (fst f' (f .fst x) , fst g' (snd g (~ j))))
       ∙∙ sym (cong-∙ (f' ⋀→ g') (push (inl (fst f x)))
         λ i → inr (fst f x , g .snd (~ i)))))
     λ x → flipSquare
       (cong (push (inr (fst g' (fst g x))) ∙_)
         ((λ i j → cong-∙ (λ y → inr (y , fst g' (fst g x)))
                        (cong (fst f') (snd f)) (snd f') i (~ j))
        ∙ symDistr (cong (λ y → inr (y , fst g' (fst g x)))
                          (λ i → fst f' (snd f i)))
                    (cong (λ y → inr (y , fst g' (fst g x))) (snd f')))
       ∙ assoc _ _ _
       ∙∙ (λ j → (push (inr (fst g' (fst g x)))
           ∙ (λ j → inr (snd f' (~ j) , fst g' (fst g x))))
           ∙ λ j → inr (fst f' (snd f (~ j)) , fst g' (g .fst x)))
       ∙∙ sym (cong-∙ (f' ⋀→ g') (push (inr (fst g x)))
                  λ i → inr ((snd f (~ i)) , fst g x)))))
        , (rUnit refl))

⋀assoc-⋀→∙ : {A A' B B' C C' : Pointed ℓ}
  (f : A →∙ A') (g : B →∙ B') (h : C →∙ C') →
      ≃∙map SmashAssocEquiv∙ ∘∙ (f ⋀→∙ (g ⋀→∙ h))
    ≡ ((f ⋀→∙ g) ⋀→∙ h) ∘∙ ≃∙map SmashAssocEquiv∙
⋀assoc-⋀→∙ {A = A} {A' = A'} {B = B} {B' = B'} {C = C} {C' = C'} f g h =
  ΣPathP
   ((funExt (⋀-fun≡'.main _ _
     (λ x → mainᵣ (fst x) (snd x))
     (λ x → p≡refl ◁ flipSquare
       (cong (cong (SmashAssocIso .Iso.fun))
         (sym (rUnit (push (inl (fst f x))))))
         ▷ λ _ → refl)
     (⋀→∙Homogeneous≡ (isHomogeneousPath _ _)
       λ y z → (λ i → push-lem y z (~ i)
                    ∙∙ refl
                    ∙∙ sym (push-lem y z i0))
           ∙ ∙∙lCancel (sym (push-lem y z i0))
           ∙ sym p≡refl)))
  , λ i j → pt-lem-main i j)
  where
  mainᵣ : (x : fst A) (y : B ⋀ C)
    → SmashAssocIso .Iso.fun (inr (fst f x , (g ⋀→ h) y))
     ≡ ((f ⋀→∙ g) ⋀→ h) (SmashAssocIso .Iso.fun (inr (x , y)))
  mainᵣ x =
    ⋀-fun≡ _ _ refl (λ _ → refl)
      (λ b → flipSquare
        (cong-∙ (λ z → SmashAssocIso .Iso.fun (inr (fst f x , z)))
                (push (inl (fst g b)))
                (λ i₁ → inr (fst g b , snd h (~ i₁)))))
      λ b → flipSquare
        (cong-∙ (λ z → SmashAssocIso .Iso.fun (inr (fst f x , z)))
                (push (inr (fst h b)))
                (λ i₁ → inr (snd g (~ i₁) , fst h b))
       ∙∙ cong₂ _∙_ ((λ j i → ⋀CommIso .Iso.fun
                   (compPath≡compPath'
                     (push (inl (fst h b)))
                     (λ i → inr (fst h b , push (inl (fst f x)) i)) (~ j) i))
                    ∙ cong-∙ (⋀CommIso .Iso.fun)
                        (push (inl (fst h b)))
                        λ i → inr (fst h b , push (inl (fst f x)) i))
                    refl
        ∙ sym (assoc _ _ _)
        ∙ cong₂ _∙_ refl (sym (cong-∙ (λ y → (inr (y , fst h b)))
                                (push (inl (fst f x)))
                                (λ i₁ → inr (fst f x , snd g (~ i₁)))))
       ∙∙ sym (lem b))
     where
     lem : (b : _) → cong ((f ⋀→∙ g) ⋀→ h)
             (cong (SmashAssocIso .Iso.fun) λ i → inr (x , push (inr b) i))
          ≡ (push (inr (fst h b)))
          ∙ λ i → inr (((push (inl (fst f x))
          ∙ λ i₁ → inr (fst f x , snd g (~ i₁))) i) , (fst h b))
     lem b = (λ j i → ((f ⋀→∙ g) ⋀→ h)
                 (⋀CommIso .Iso.fun
                   (compPath≡compPath' (push (inl b))
                     (λ i → inr (b , push (inl x) i)) (~ j) i)))
           ∙∙ cong-∙ (((f ⋀→∙ g) ⋀→ h) ∘ ⋀CommIso .Iso.fun)
                (push (inl b)) (λ i → inr (b , push (inl x) i))
           ∙∙ cong₂ _∙_
               (sym (rUnit _))
               refl

  push-lem : (y : _) (z : _)
    → cong (((f ⋀→∙ g) ⋀→ h) ∘ (fst (fst SmashAssocEquiv∙)))
            (push (inr (inr (y , z))))
     ≡ cong (fst (≃∙map SmashAssocEquiv∙ ∘∙ (f ⋀→∙ (g ⋀→∙ h))))
            (push (inr (inr (y , z))))
  push-lem y z =
      cong (cong ((f ⋀→∙ g) ⋀→ h))
           (cong-∙∙ ⋀comm→ (push (inl z))
                            (λ i → inr (z , push (inr y) i))
                            refl
         ∙ sym (compPath≡compPath' (push (inr z)) _))
   ∙∙ cong-∙ ((f ⋀→∙ g) ⋀→ h)
        (push (inr z)) (λ i → inr (push (inr y) i , z))
   ∙∙ (cong₂ _∙_ (sym (rUnit (push (inr (fst h z)))))
                 (cong-∙ (λ x → inr (x , fst h z))
                         (push (inr (fst g y)))
                         (λ i → inr (snd f (~ i) , fst g y)))
     ∙ sym (cong-∙ (SmashAssocIso .Iso.fun)
             (push (inr (inr (fst g y , fst h z))))
             (λ i → inr (snd f (~ i)
                        , inr (fst g y , fst h z)))
        ∙∙ cong (_∙ (λ i → inr (inr (snd f (~ i) , fst g y) , fst h z)))
                (cong-∙∙ ⋀comm→
                         (push (inl (fst h z)))
                         (λ i → inr (fst h z , push (inr (fst g y)) i))
                         refl
             ∙ sym (compPath≡compPath' (push (inr (fst h z))) _))
        ∙∙ sym (assoc _ _ _)))

  module N = ⋀-fun≡'
      (λ z → SmashAssocIso .Iso.fun ((f ⋀→ (g ⋀→∙ h)) z))
      (λ z → ((f ⋀→∙ g) ⋀→ h) (SmashAssocIso .Iso.fun z))
      (λ x₁ → mainᵣ (fst x₁) (snd x₁))

  p≡refl : N.p ≡ refl
  p≡refl = (λ j → cong (SmashAssocIso .Iso.fun
                       ∘ ((f ⋀→ (g ⋀→∙ h))))
                         (push (inr (inl tt)))
                 ∙∙ refl
                 ∙∙ cong (((f ⋀→∙ g) ⋀→ h)
                         ∘ (SmashAssocIso .Iso.fun))
                         (sym (push (push tt j))))
          ∙ cong (λ x → x ∙∙ refl ∙∙ refl)
                  (cong-∙ (SmashAssocIso .Iso.fun)
                          (push (inr (inl tt)))
                          (λ i → inr (snd f (~ i) , inl tt))
                 ∙ sym (rUnit refl))
          ∙ sym (rUnit refl)

  pt-lem : cong (fst (≃∙map SmashAssocEquiv∙ ∘∙ (f ⋀→∙ (g ⋀→∙ h))))
             (push (inr (inl tt)))
         ≡ cong (fst (((f ⋀→∙ g) ⋀→∙ h) ∘∙ ≃∙map SmashAssocEquiv∙))
             (push (inr (inl tt)))
  pt-lem i j =
    fst (≃∙map SmashAssocEquiv∙) (rUnit (push (inr (inl tt))) (~ i) j)

  pt-lem-main : I → I → _
  pt-lem-main i j =
    hcomp (λ k → λ {(i = i0) → rUnit (refl {x = inl tt}) k j
                   ; (i = i1) → rUnit (refl {x = inl tt}) k j
                   ; (j = i0) → (pt-lem i0 ∙∙ refl ∙∙ sym (pt-lem k)) i
                   ; (j = i1) → inl tt})
          (∙∙lCancel (sym (pt-lem i0)) j i)

⋀comm-sq : {A A' B B' : Pointed ℓ}
  (f : A →∙ A') (g : B →∙ B')
  → (⋀comm→∙ ∘∙ (f ⋀→∙ g)) ≡ ((g ⋀→∙ f) ∘∙ ⋀comm→∙)
⋀comm-sq f g =
  ΣPathP ((funExt
    (⋀-fun≡ _ _ refl (λ _ → refl)
      (λ x → flipSquare
        (cong-∙ ⋀comm→
          (push (inl (fst f x))) (λ i → inr (fst f x , snd g (~ i)))))
      λ b → flipSquare (cong-∙ ⋀comm→
                         (push (inr (fst g b)))
                         (λ i → inr (snd f (~ i) , fst g b)))))
    , refl)

⋀comm-sq' : {A A' B B' : Pointed ℓ}
  (f : A →∙ A') (g : B →∙ B')
  → (f ⋀→∙ g) ≡ (⋀comm→∙ ∘∙ ((g ⋀→∙ f) ∘∙ ⋀comm→∙))
⋀comm-sq' f g =
     sym (∘∙-idʳ (f ⋀→∙ g))
  ∙∙ cong (_∘∙ (f ⋀→∙ g)) (sym lem)
  ∙∙ ∘∙-assoc ⋀comm→∙ ⋀comm→∙ (f ⋀→∙ g)
   ∙ cong (λ w → ⋀comm→∙ ∘∙ w) (⋀comm-sq f g)
  where
  lem : ⋀comm→∙ ∘∙ ⋀comm→∙ ≡ idfun∙ _
  lem = ΣPathP ((funExt (Iso.rightInv ⋀CommIso)) , (sym (rUnit refl)))

Bool⋀→ : Bool*∙ {ℓ} ⋀ A → typ A
Bool⋀→ {A = A} (inl x) = pt A
Bool⋀→ (inr (lift false , a)) = a
Bool⋀→ {A = A} (inr (lift true , a)) = pt A
Bool⋀→ {A = A} (push (inl (lift false)) i) = pt A
Bool⋀→ {A = A} (push (inl (lift true)) i) = pt A
Bool⋀→ {A = A} (push (inr x) i) = pt A
Bool⋀→ {A = A} (push (push a i₁) i) = pt A

⋀lIdIso : Iso (Bool*∙ {ℓ} ⋀ A) (typ A)
Iso.fun (⋀lIdIso {A = A}) (inl x) = pt A
Iso.fun ⋀lIdIso = Bool⋀→
Iso.inv ⋀lIdIso a = inr (false* , a)
Iso.rightInv ⋀lIdIso a = refl
Iso.leftInv (⋀lIdIso {A = A}) =
  ⋀-fun≡ _ _ (sym (push (inl false*))) h hₗ
    λ x → compPath-filler (sym (push (inl false*))) (push (inr x))
  where
  h : (x : (Lift Bool) × fst A) →
      inr (false* , Bool⋀→ (inr x)) ≡ inr x
  h (lift false , a) = refl
  h (lift true , a) = sym (push (inl false*)) ∙ push (inr a)

  hₗ : (x : Lift Bool) →
      PathP
      (λ i → inr (false* , Bool⋀→ (push (inl x) i)) ≡ push (inl x) i)
      (λ i → push (inl false*) (~ i)) (h (x , pt A))
  hₗ (lift false) i j = push (inl false*) (~ j ∨ i)
  hₗ (lift true) =
      compPath-filler (sym (push (inl false*))) (push (inl true*))
    ▷ (cong (sym (push (inl false*)) ∙_)
       λ j i → push (push tt j) i)

⋀lIdEquiv∙ : Bool*∙ {ℓ} ⋀∙ A ≃∙ A
fst ⋀lIdEquiv∙ = isoToEquiv ⋀lIdIso
snd ⋀lIdEquiv∙ = refl

⋀lId-sq : (f : A →∙ B) →
      (≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ (idfun∙ Bool*∙ ⋀→∙ f))
    ≡ (f ∘∙ ≃∙map ⋀lIdEquiv∙)
⋀lId-sq {ℓ} {A = A} {B = B} f =
  ΣPathP ((funExt
    (⋀-fun≡ _ _ (sym (snd f)) (λ x → h (fst x) (snd x)) hₗ hᵣ))
  , (sym (rUnit refl) ◁ (λ i j → snd f (~ i ∨ j))
    ▷ lUnit (snd f)))
  where
  h : (x : Lift Bool) (a : fst A)
    → Bool⋀→ (inr (x , fst f a)) ≡ fst f (Bool⋀→ (inr (x , a)))
  h (lift false) a = refl
  h (lift true) a = sym (snd f)

  hₗ : (x : Lift Bool)
    → PathP (λ i → Bool⋀→ ((idfun∙ Bool*∙ ⋀→ f) (push (inl x) i))
                   ≡ fst f (Bool⋀→ (push (inl x) i)))
             (sym (snd f)) (h x (pt A))
  hₗ (lift false) =
    flipSquare ((cong-∙ (Bool⋀→ {ℓ})
                  (push (inl false*))
                  (λ i → inr (lift false , snd f (~ i)))
              ∙ sym (lUnit (sym (snd f))))
             ◁ λ i j → snd f (~ i ∧ ~ j))
  hₗ (lift true) =
    flipSquare
       ((cong-∙ (Bool⋀→ {ℓ})
         (push (inl true*)) (λ i → inr (lift true , snd f (~ i)))
       ∙ sym (rUnit refl))
      ◁ λ i _ → snd f (~ i))

  hᵣ : (x : fst A)
    → PathP (λ i → Bool⋀→ {ℓ} ((idfun∙ Bool*∙ ⋀→ f) (push (inr x) i))
                   ≡ fst f (snd A))
             (sym (snd f)) (h true* x)
  hᵣ x = flipSquare ((cong-∙ (Bool⋀→ {ℓ})
                      (push (inr (fst f x)))
                      (λ i → inr (true* , fst f x))
                    ∙ sym (rUnit refl))
      ◁ λ i _ → snd f (~ i))

⋀lId-assoc : ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→∙ idfun∙ B)
             ∘∙ ≃∙map SmashAssocEquiv∙)
            ≡ ≃∙map ⋀lIdEquiv∙
⋀lId-assoc {ℓ} {A = A} {B = B} =
  ΣPathP (funExt
          (⋀-fun≡'.main _ _
            (λ xy → mainᵣ (fst xy) (snd xy))
            (λ x → sym (rUnit refl) ◁ mainᵣ-pt-coh x)
            (⋀→∙Homogeneous≡ (isHomogeneousPath _ _) mainᵣ-coh))
        , (sym (rUnit refl)
          ◁ flipSquare (sym (rUnit refl))))
  where
  l₁ : (x : Lift Bool) → inl tt ≡ Bool⋀→ (inr (x , inl tt))
  l₁ (lift true) = refl
  l₁ (lift false) = refl

  l₂ : (x : Lift Bool) (y : fst A × fst B)
    → inr (Bool⋀→ (inr (x , fst y)) , snd y)
    ≡ Bool⋀→ (inr (x , inr y))
  l₂ (lift true) y = sym (push (inr (snd y)))
  l₂ (lift false) y = refl

  l₁≡l₂-left : (x : Lift Bool) (y : fst A) →
    PathP (λ i → l₁ x i ≡ l₂ x (y , pt B) i)
          (push (inl (Bool⋀→ (inr (x , y)))))
          λ i → Bool⋀→ {ℓ} {A = A ⋀∙ B} (inr (x , push (inl y) i))
  l₁≡l₂-left (lift true) y = (λ i → push (push tt i))
                   ◁ λ i j → push (inr (pt B)) (~ i ∧ j)
  l₁≡l₂-left (lift false) y = refl

  l₁≡l₂-right : (x : Lift Bool) (y : fst B)
    → PathP (λ i → l₁ x i ≡ l₂ x ((pt A) , y) i)
            (push (inr y) ∙ (λ i → inr (Bool⋀→ {A = A} (push (inl x) i) , y)))
            (λ i → Bool⋀→ {A = A ⋀∙ B} (inr (x , push (inr y) i)))
  l₁≡l₂-right (lift false) y = sym (rUnit (push (inr y)))
  l₁≡l₂-right (lift true) y = sym (rUnit (push (inr y)))
                   ◁ λ i j → push (inr y) (j ∧ ~ i)

  mainᵣ : (x : Lift Bool) (y : A ⋀ B)
    → (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B)
        (SmashAssocIso .Iso.fun (inr (x , y)))
     ≡ Bool⋀→ {ℓ} (inr (x , y))
  mainᵣ x = ⋀-fun≡ _ _ (l₁ x) (l₂ x)
    (λ y → flipSquare (sym (rUnit (push (inl (Bool⋀→ (inr (x , y))))))
          ◁ l₁≡l₂-left x y))
    λ y → flipSquare (
      (cong (cong (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B))
            (cong-∙∙ ⋀comm→
              (push (inl y)) (λ i → inr (y , push (inl x) i)) refl
          ∙ sym (compPath≡compPath'
                  (push (inr y)) (λ i → inr (push (inl x) i , y))))
        ∙ cong-∙ (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B)
            (push (inr y)) λ i → inr (push (inl x) i , y))
        ◁ (cong₂ _∙_ (sym (rUnit (push (inr y))))
                     refl
                   ◁ l₁≡l₂-right x y))

  mainᵣ-pt-coh : (x : Lift Bool)
    → PathP (λ i → inl tt ≡ Bool⋀→ (push (inl x) i))
             refl (mainᵣ x (inl tt))
  mainᵣ-pt-coh (lift false) = refl
  mainᵣ-pt-coh (lift true) = refl

  module N = ⋀-fun≡'
    (λ z → (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B) (SmashAssocIso .Iso.fun z))
    (λ z → ⋀lIdIso .Iso.fun z)
    (λ xy → mainᵣ (fst xy) (snd xy))
  open N

  lem : (x : fst A) (y : fst B)
    → cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→ idfun∙ B)
            ∘ SmashAssocIso .Iso.fun)
             (push (inr (inr (x , y))))
    ≡ push (inr y)
  lem x y =
      cong (cong (≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→ idfun∙ B))
            (cong-∙∙ ⋀comm→
              (push (inl y)) (λ i → inr (y , push (inr x) i)) refl
           ∙ sym (compPath≡compPath'
                  (push (inr y)) λ i → inr (push (inr x) i , y)))
    ∙∙ cong-∙ (≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→ idfun∙ B)
              (push (inr y))
              (λ i → inr (push (inr x) i , y))
    ∙∙ (sym (rUnit _)
     ∙ sym (rUnit _))

  mainᵣ-coh : (x : fst A) (y : fst B)
    → Fₗ .fst (inr (x , y)) ≡ Fᵣ .fst (inr (x , y))
  mainᵣ-coh x y =
      (λ i → lem x y i ∙∙ sym (lem x y i1) ∙∙ refl)
    ∙ sym (compPath≡compPath'
           (push (inr y)) (sym (push (inr y))))
    ∙ rCancel (push (inr y))
    ∙ rUnit refl

-- Triangle equality
⋀triang : ∀ {ℓ} {A B : Pointed ℓ}
  → (((≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ ⋀comm→∙) ⋀→∙ idfun∙ B)
    ∘∙ ≃∙map SmashAssocEquiv∙)
    ≡ idfun∙ A ⋀→∙ ≃∙map (⋀lIdEquiv∙ {ℓ} {A = B})
⋀triang {ℓ = ℓ} {A = A} {B = B} =
  ΣPathP ((funExt (⋀-fun≡'.main _ _
    (λ x → mainᵣ (fst x) (snd x))
    (λ x → p≡refl
         ◁ flipSquare ((λ i j → push (inl x) (i ∧ j))
         ▷ rUnit (push (inl x))))
    (⋀→∙Homogeneous≡ (isHomogeneousPath _ _)
      λ x y → Fₗ≡refl x y ∙ sym (Fᵣ≡refl x y))))
    , (sym (rUnit refl) ◁ flipSquare p≡refl))
  where
  mainᵣ-hom : (x : fst A) (y : Bool* {ℓ}) (z : fst B)
    → Path (A ⋀ B) (inr (Bool⋀→ (inr (y , x)) , z))
                    (inr (x , Bool⋀→ (inr (y , z))))
  mainᵣ-hom x (lift false) z = refl
  mainᵣ-hom x (lift true) z = sym (push (inr z)) ∙ push (inl x)

  mainᵣ : (x : fst A) (y : Bool*∙ {ℓ} ⋀ B) →
    ((≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ ⋀comm→∙) ⋀→ (idfun∙ B))
      (Iso.fun (SmashAssocIso {A = A} {B = Bool*∙ {ℓ}} {C = B}) (inr (x , y)))
    ≡ inr (x , ⋀lIdIso .Iso.fun y)
  mainᵣ x = ⋀-fun≡ _ _ (push (inl x))
    (λ y → mainᵣ-hom x (fst y) (snd y))
    (λ { (lift false) → flipSquare (sym (rUnit (push (inl x)))
                       ◁ λ i j → push (inl x) (j ∨ i))
       ; (lift true) → flipSquare ((sym (rUnit (push (inl (pt A))))
                                   ∙ λ j i → push (push tt j) i)
                     ◁ λ i j → compPath-filler'
                                 (sym (push (inr (pt B)))) (push (inl x)) j i)})
     λ b → flipSquare
       ((cong (cong (((≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)))
         (cong-∙∙ ⋀comm→ (push (inl b)) (λ i → inr (b , push (inl x) i)) refl
         ∙ sym (compPath≡compPath'
                 (push (inr b)) (λ i → inr (push (inl x) i , b))))
       ∙ cong-∙ (((≃∙map (⋀lIdEquiv∙ {ℓ})  ∘∙ ⋀comm→∙) ⋀→ idfun∙ B))
                (push (inr b)) (λ i → inr (push (inl x) i , b))
       ∙ sym (rUnit _)
       ∙ (λ i → (push (inr b) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , b))))
       ∙ sym (rUnit (push (inr b))))
       ◁ λ i j → compPath-filler' (sym (push (inr b))) (push (inl x)) j i)

  lemₗ : cong (idfun∙ A ⋀→ ≃∙map (⋀lIdEquiv∙ {ℓ} {A = B}))
             (push (inr (inl tt)))
      ≡ (push (inl (snd A)))
  lemₗ = sym (rUnit _) ∙ λ i → push (push tt (~ i))

  module K = ⋀-fun≡' (λ z →
          ((≃∙map ⋀lIdEquiv∙ ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
          (SmashAssocIso .Iso.fun z))
       (λ z → (idfun∙ A ⋀→ ≃∙map ⋀lIdEquiv∙) z)
       (λ x₁ → mainᵣ (fst x₁) (snd x₁))
  open K

  p≡refl : p ≡ refl
  p≡refl = cong (push (inl (snd A)) ∙_) (cong sym lemₗ)
         ∙ rCancel (push (inl (pt A)))

  Fₗ-false : (y : fst B)
    → cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
        (cong ⋀comm→ (push (inl y)
                   ∙' (λ i → inr (y , push (inr (lift false)) i))))
      ≡ push (inr y)
  Fₗ-false y =
      cong (cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B))
         (cong (cong ⋀comm→)
           (sym (compPath≡compPath'
             (push (inl y)) (λ i → inr (y , push (inr (lift false)) i))))
       ∙ cong-∙ ⋀comm→ (push (inl y))
                        (λ i → inr (y , push (inr (lift false)) i)))
    ∙∙ cong-∙ ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
              (push (inr y)) (λ i → inr (push (inr (lift false)) i , y))
    ∙∙ (sym (rUnit _)
     ∙ (λ i → push (inr y) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , y)))
     ∙ sym (rUnit _))

  Fₗ-true : (y : fst B)
    → cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
        (cong (SmashAssocIso .Iso.fun) (push (inr (inr (lift true , y)))))
      ≡ push (inr y)
  Fₗ-true y =
      cong (cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B))
        (cong-∙∙ ⋀comm→ (push (inl y)) (λ i → inr (y , push (inr true*) i)) refl
        ∙ sym (compPath≡compPath' (push (inr y))
                                  λ i → inr (push (inr true*) i , y)))
    ∙∙ cong-∙ ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
              (push (inr y))
              (λ i → inr (push (inr true*) i , y))
    ∙∙ ((sym (rUnit _)
     ∙ (λ i → push (inr y) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , y)))
     ∙ sym (rUnit _)))

  Fₗ≡refl : (x : Lift Bool) (y : fst B) → Fₗ .fst (inr (x , y)) ≡ refl
  Fₗ≡refl (lift false) y =
     (λ i → Fₗ-false y i ∙∙ refl ∙∙ sym (rUnit (push (inr y)) (~ i)))
    ∙ ∙∙lCancel _
  Fₗ≡refl (lift true) y =
      (λ j → Fₗ-true y j
          ∙∙ (sym (push (inr y)) ∙ push (push tt j))
          ∙∙ sym (rUnit (push (inr (pt B))) (~ j)))
    ∙ (λ j → (λ i → push (inr y) (i ∧ ~ j))
           ∙∙ (λ i → push (inr y) (~ j ∧ ~ i))
            ∙ push (inr (pt B))
           ∙∙ sym (push (inr (pt B))))
    ∙ cong (_∙ sym (push (inr (pt B)))) (sym (lUnit (push (inr (pt B)))))
    ∙ rCancel _

  Fᵣ≡refl : (x : Lift Bool) (y : fst B) → Fᵣ .fst (inr (x , y)) ≡ refl
  Fᵣ≡refl x y =
    cong (push (inl (snd A)) ∙_)
      (sym (rUnit _) ∙ (λ i j → push (push tt (~ i)) (~ j)))
    ∙ rCancel _


-- ⋀ as a functor
⋀F : ∀ {ℓ} → Prefunctor (PointedCat ℓ ×' PointedCat ℓ) (PointedCat ℓ)
F-ob ⋀F (A , B) = A ⋀∙ B
F-hom ⋀F (f , g) = f ⋀→∙ g
F-id ⋀F = ⋀→∙-idfun
F-seq ⋀F (f , g) (f' , g') = ⋀→∙-comp f f' g g'

⋀lUnitNatIso : PreNatIso (PointedCat ℓ) (PointedCat ℓ)
      (restrFunctorₗ ⋀F Bool*∙) (idPrefunctor (PointedCat ℓ))
N-ob (trans ⋀lUnitNatIso) X = ≃∙map ⋀lIdEquiv∙
N-hom (trans ⋀lUnitNatIso) f = ⋀lId-sq f
inv' (isIs ⋀lUnitNatIso c) = ≃∙map (invEquiv∙ ⋀lIdEquiv∙)
sect (isIs (⋀lUnitNatIso {ℓ = ℓ}) c) =
  ≃∙→ret/sec∙ (⋀lIdEquiv∙ {ℓ = ℓ} {A = c}) .snd
retr (isIs ⋀lUnitNatIso c) =
  ≃∙→ret/sec∙ ⋀lIdEquiv∙ .fst

makeIsIso-Pointed : ∀ {ℓ} {A B : Pointed ℓ} {f : A →∙ B}
  → isEquiv (fst f) → preIsIso {C = PointedCat ℓ} f
inv' (makeIsIso-Pointed {f = f} eq) = ≃∙map (invEquiv∙ ((fst f , eq) , snd f))
sect (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f)  .snd
retr (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f)  .fst

restrₗᵣ : PreNatIso (PointedCat ℓ) (PointedCat ℓ)
      (restrFunctorᵣ ⋀F Bool*∙) (restrFunctorₗ ⋀F Bool*∙)
N-ob (trans restrₗᵣ) X = ⋀comm→∙
N-hom (trans restrₗᵣ) f = ⋀comm-sq f (idfun∙ Bool*∙)
isIs restrₗᵣ c = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso)

-- main result
⋀Symm : ∀ {ℓ} → isSymmetricPrecategory (PointedCat ℓ)
_⊗_ (isMonoidal ⋀Symm) = ⋀F
𝟙 (isMonoidal ⋀Symm) = Bool*∙
N-ob (trans (⊗assoc (isMonoidal ⋀Symm))) (A , B , C) = ≃∙map SmashAssocEquiv∙
N-hom (trans (⊗assoc (isMonoidal ⋀Symm))) (f , g , h) = ⋀assoc-⋀→∙ f g h
inv' (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) =
  ≃∙map (invEquiv∙ SmashAssocEquiv∙)
sect (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) =
  ≃∙→ret/sec∙ SmashAssocEquiv∙ .snd
retr (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) =
  ≃∙→ret/sec∙ SmashAssocEquiv∙ .fst
⊗lUnit (isMonoidal ⋀Symm) = ⋀lUnitNatIso
⊗rUnit (isMonoidal ⋀Symm) = compPreNatIso _ _ _ restrₗᵣ ⋀lUnitNatIso
triang (isMonoidal (⋀Symm {ℓ})) X Y = ⋀triang
⊗pentagon (isMonoidal ⋀Symm) X Y Z W =
  (∘∙-assoc assc₅∙ assc₄∙ assc₃∙) ∙ pentagon∙
N-ob (trans (Braid ⋀Symm)) X = ⋀comm→∙
N-hom (trans (Braid ⋀Symm)) (f , g) = ⋀comm-sq f g
isIs (Braid ⋀Symm) _ = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso)
isSymmetricPrecategory.hexagon ⋀Symm a b c = hexagon∙
symBraiding ⋀Symm X Y =
  ΣPathP ((funExt (Iso.rightInv ⋀CommIso)) , (sym (rUnit refl)))