text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.RingStructure.GradedCommutativity where

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.GroupoidLaws hiding (assoc)
open import Cubical.Foundations.Path

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat
open import Cubical.Data.Int
  renaming (_+_ to _ℤ+_ ; _·_ to _ℤ∙_ ; +Comm to +ℤ-comm ; ·Comm to ∙-comm ; +Assoc to ℤ+-assoc ; -_ to -ℤ_)
  hiding (_+'_ ; +'≡+)
open import Cubical.Data.Sigma
open import Cubical.Data.Sum

open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.Truncation as T
open import Cubical.HITs.S1 hiding (_·_)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp

open import Cubical.Homotopy.Loopspace

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.Properties

private
  variable
    ℓ : Level

open PlusBis

natTranspLem : ∀ {ℓ} {A B : ℕ → Type ℓ} {n m : ℕ} (a : A n)
  (f : (n : ℕ) → (a : A n) → B n) (p : n ≡ m)
  → f m (subst A p a) ≡ subst B p (f n a)
natTranspLem {A = A} {B = B} a f p = sym (substCommSlice A B f p a)

transp0₁ : (n : ℕ) → subst coHomK (+'-comm 1 (suc n)) (0ₖ _) ≡ 0ₖ _
transp0₁ zero = refl
transp0₁ (suc n) = refl

transp0₂ : (n m : ℕ) → subst coHomK (+'-comm (suc (suc n)) (suc m)) (0ₖ _) ≡ 0ₖ _
transp0₂ n zero = refl
transp0₂ n (suc m) = refl

-- Recurring expressions
private
  ΩKn+1→Ω²Kn+2 : {k : ℕ} → typ (Ω (coHomK-ptd k)) → typ ((Ω^ 2) (coHomK-ptd (suc k)))
  ΩKn+1→Ω²Kn+2 x = sym (Kn→ΩKn+10ₖ _) ∙∙ cong (Kn→ΩKn+1 _) x ∙∙ Kn→ΩKn+10ₖ _

  ΩKn+1→Ω²Kn+2' : {k : ℕ} → Kn→ΩKn+1 k (0ₖ k) ≡ Kn→ΩKn+1 k (0ₖ k) → typ ((Ω^ 2) (coHomK-ptd (suc k)))
  ΩKn+1→Ω²Kn+2' p = sym (Kn→ΩKn+10ₖ _) ∙∙ p ∙∙ Kn→ΩKn+10ₖ _

  Kn→Ω²Kn+2 : {k : ℕ} → coHomK k → typ ((Ω^ 2) (coHomK-ptd (2 + k)))
  Kn→Ω²Kn+2 x = ΩKn+1→Ω²Kn+2 (Kn→ΩKn+1 _ x)

-- Definition of of -ₖ'ⁿ̇*ᵐ
-- This definition is introduced to facilite the proofs
-ₖ'-helper : {k : ℕ} (n m : ℕ)
  → isEvenT n ⊎ isOddT n → isEvenT m ⊎ isOddT m
  → coHomKType k → coHomKType k
-ₖ'-helper {k = zero} n m (inl x₁) q x = x
-ₖ'-helper {k = zero} n m (inr x₁) (inl x₂) x = x
-ₖ'-helper {k = zero} n m (inr x₁) (inr x₂) x = 0 - x
-ₖ'-helper {k = suc zero} n m p q base = base
-ₖ'-helper {k = suc zero} n m (inl x) q (loop i) = loop i
-ₖ'-helper {k = suc zero} n m (inr x) (inl x₁) (loop i) = loop i
-ₖ'-helper {k = suc zero} n m (inr x) (inr x₁) (loop i) = loop (~ i)
-ₖ'-helper {k = suc (suc k)} n m p q north = north
-ₖ'-helper {k = suc (suc k)} n m p q south = north
-ₖ'-helper {k = suc (suc k)} n m (inl x) q (merid a i) =
  (merid a ∙ sym (merid (ptSn (suc k)))) i
-ₖ'-helper {k = suc (suc k)} n m (inr x) (inl x₁) (merid a i) =
  (merid a ∙ sym (merid (ptSn (suc k)))) i
-ₖ'-helper {k = suc (suc k)} n m (inr x) (inr x₁) (merid a i) =
  (merid a ∙ sym (merid (ptSn (suc k)))) (~ i)

-ₖ'-gen : {k : ℕ} (n m : ℕ)
         (p : isEvenT n ⊎ isOddT n)
         (q : isEvenT m ⊎ isOddT m)
       → coHomK k → coHomK k
-ₖ'-gen {k = zero} = -ₖ'-helper {k = zero}
-ₖ'-gen {k = suc k} n m p q = T.map (-ₖ'-helper {k = suc k} n m p q)

-- -ₖ'ⁿ̇*ᵐ
-ₖ'^_·_ : {k : ℕ} (n m : ℕ) → coHomK k → coHomK k
-ₖ'^_·_ {k = k} n m = -ₖ'-gen n m (evenOrOdd n) (evenOrOdd m)

-- cohomology version
-ₕ'^_·_ : {k : ℕ} {A : Type ℓ} (n m : ℕ) → coHom k A → coHom k A
-ₕ'^_·_ n m = ST.map λ f x → (-ₖ'^ n · m) (f x)

-- -ₖ'ⁿ̇*ᵐ = -ₖ' for n m odd
-ₖ'-gen-inr≡-ₖ' : {k : ℕ} (n m : ℕ) (p : _) (q : _) (x : coHomK k)
  → -ₖ'-gen n m (inr p) (inr q) x ≡ (-ₖ x)
-ₖ'-gen-inr≡-ₖ' {k = zero} n m p q _ = refl
-ₖ'-gen-inr≡-ₖ' {k = suc zero} n m p q =
  T.elim ((λ _ → isOfHLevelTruncPath))
         λ { base → refl
          ; (loop i) → refl}
-ₖ'-gen-inr≡-ₖ' {k = suc (suc k)} n m p q =
  T.elim ((λ _ → isOfHLevelTruncPath))
         λ { north → refl
           ; south → refl
           ; (merid a i) k → ∣ symDistr (merid (ptSn _)) (sym (merid a)) (~ k) (~ i) ∣ₕ}

-- -ₖ'ⁿ̇*ᵐ x = x for n even
-ₖ'-gen-inl-left : {k : ℕ} (n m : ℕ) (p : _) (q : _) (x : coHomK k)
  → -ₖ'-gen n m (inl p) q x ≡ x
-ₖ'-gen-inl-left {k = zero} n m p q x = refl
-ₖ'-gen-inl-left {k = suc zero} n m p q =
  T.elim (λ _ → isOfHLevelTruncPath)
         λ { base → refl ; (loop i) → refl}
-ₖ'-gen-inl-left {k = suc (suc k)} n m p q =
  T.elim (λ _ → isOfHLevelPath (4 + k) (isOfHLevelTrunc (4 + k)) _ _)
         λ { north → refl
           ; south → cong ∣_∣ₕ (merid (ptSn _))
           ; (merid a i) k → ∣ compPath-filler (merid a) (sym (merid (ptSn _))) (~ k) i ∣ₕ}

-- -ₖ'ⁿ̇*ᵐ x = x for m even
-ₖ'-gen-inl-right : {k : ℕ} (n m : ℕ) (p : _) (q : _) (x : coHomK k)
  → -ₖ'-gen n m p (inl q) x ≡ x
-ₖ'-gen-inl-right {k = zero} n m (inl x₁) q x = refl
-ₖ'-gen-inl-right {k = zero} n m (inr x₁) q x = refl
-ₖ'-gen-inl-right {k = suc zero} n m (inl x₁) q =
  T.elim (λ _ → isOfHLevelTruncPath)
         λ { base → refl ; (loop i) → refl}
-ₖ'-gen-inl-right {k = suc zero} n m (inr x₁) q =
  T.elim (λ _ → isOfHLevelTruncPath)
         λ { base → refl ; (loop i) → refl}
-ₖ'-gen-inl-right {k = suc (suc k)} n m (inl x₁) q =
  T.elim (λ _ → isOfHLevelTruncPath)
         λ { north → refl
           ; south → cong ∣_∣ₕ (merid (ptSn _))
           ; (merid a i) k → ∣ compPath-filler (merid a) (sym (merid (ptSn _))) (~ k) i  ∣ₕ}
-ₖ'-gen-inl-right {k = suc (suc k)} n m (inr x₁) q =
  T.elim (λ _ → isOfHLevelTruncPath)
         λ { north → refl
           ; south → cong ∣_∣ₕ (merid (ptSn _))
           ; (merid a i) k → ∣ compPath-filler (merid a) (sym (merid (ptSn _))) (~ k) i  ∣ₕ}

-ₖ'-gen² : {k : ℕ} (n m : ℕ)
         (p : isEvenT n ⊎ isOddT n)
         (q : isEvenT m ⊎ isOddT m)
         → (x : coHomK k) → -ₖ'-gen n m p q (-ₖ'-gen n m p q x) ≡ x
-ₖ'-gen² {k = zero} n m (inl x₁) q x = refl
-ₖ'-gen² {k = zero} n m (inr x₁) (inl x₂) x = refl
-ₖ'-gen² {k = zero} n m (inr x₁) (inr x₂) x =
     cong (pos 0 -_) (-AntiComm (pos 0) x)
  ∙∙ -AntiComm (pos 0) (-ℤ (x - pos 0))
  ∙∙ h x
  where
  h : (x : _) →  -ℤ (-ℤ (x - pos 0) - pos 0) ≡ x
  h (pos zero) = refl
  h (pos (suc n)) = refl
  h (negsuc n) = refl
-ₖ'-gen² {k = suc k} n m (inl x₁) q x i =
  -ₖ'-gen-inl-left n m x₁ q (-ₖ'-gen-inl-left n m x₁ q x i) i
-ₖ'-gen² {k = suc k} n m (inr x₁) (inl x₂) x i =
  -ₖ'-gen-inl-right n m (inr x₁) x₂ (-ₖ'-gen-inl-right n m (inr x₁) x₂ x i) i
-ₖ'-gen² {k = suc k} n m (inr x₁) (inr x₂) x =
  (λ i → -ₖ'-gen-inr≡-ₖ' n m x₁ x₂ (-ₖ'-gen-inr≡-ₖ' n m x₁ x₂ x i) i) ∙ -ₖ^2 x

-ₖ'-genIso : {k : ℕ} (n m : ℕ)
         (p : isEvenT n ⊎ isOddT n)
         (q : isEvenT m ⊎ isOddT m)
       → Iso (coHomK k) (coHomK k)
Iso.fun (-ₖ'-genIso {k = k} n m p q) = -ₖ'-gen n m p q
Iso.inv (-ₖ'-genIso {k = k} n m p q) = -ₖ'-gen n m p q
Iso.rightInv (-ₖ'-genIso {k = k} n m p q) = -ₖ'-gen² n m p q
Iso.leftInv (-ₖ'-genIso {k = k} n m p q) = -ₖ'-gen² n m p q

-- action of cong on -ₖ'ⁿ̇*ᵐ
cong-ₖ'-gen-inr : {k : ℕ} (n m : ℕ)  (p : _) (q : _) (P : Path (coHomK (2 + k)) (0ₖ _) (0ₖ _))
     → cong (-ₖ'-gen n m (inr p) (inr q)) P ≡ sym P
cong-ₖ'-gen-inr {k = k} n m p q P = code≡sym (0ₖ _) P
  where
  code : (x : coHomK (2 + k)) → 0ₖ _ ≡ x → x ≡ 0ₖ _
  code = T.elim (λ _ → isOfHLevelΠ (4 + k) λ _ → isOfHLevelTruncPath)
                λ { north → cong (-ₖ'-gen n m (inr p) (inr q))
                  ; south P → cong ∣_∣ₕ (sym (merid (ptSn _))) ∙ (cong (-ₖ'-gen n m (inr p) (inr q)) P)
                  ; (merid a i) → t a i}
    where
    t : (a : S₊ (suc k)) → PathP (λ i → 0ₖ (2 + k) ≡ ∣ merid a i ∣ₕ → ∣ merid a i ∣ₕ ≡ 0ₖ (2 + k))
                                  (cong (-ₖ'-gen n m (inr p) (inr q)))
                                  (λ P → cong ∣_∣ₕ (sym (merid (ptSn _))) ∙ (cong (-ₖ'-gen n m (inr p) (inr q)) P))
    t a = toPathP (funExt λ P → cong (transport (λ i → ∣ merid a i ∣ ≡ 0ₖ (suc (suc k))))
                   (cong (cong (-ₖ'-gen n m (inr p) (inr q))) (λ i → (transp (λ j → 0ₖ (suc (suc k)) ≡ ∣ merid a (~ j ∧ ~ i) ∣) i
                         (compPath-filler P (λ j → ∣ merid a (~ j) ∣ₕ) i))))
        ∙∙ cong (transport (λ i → ∣ merid a i ∣ ≡ 0ₖ (suc (suc k)))) (congFunct (-ₖ'-gen n m (inr p) (inr q)) P (sym (cong ∣_∣ₕ (merid a))))
        ∙∙ (λ j → transp (λ i → ∣ merid a (i ∨ j) ∣ ≡ 0ₖ (suc (suc k))) j
                  (compPath-filler' (cong ∣_∣ₕ (sym (merid a)))
                    (cong (-ₖ'-gen n m (inr p) (inr q)) P
                    ∙ cong (-ₖ'-gen n m (inr p) (inr q)) (sym (cong ∣_∣ₕ (merid a)))) j))
        ∙∙ (λ i → sym (cong ∣_∣ₕ (merid a))
                 ∙ isCommΩK (2 + k) (cong (-ₖ'-gen n m (inr p) (inr q)) P)
                                    (cong (-ₖ'-gen n m (inr p) (inr q)) (sym (cong ∣_∣ₕ (merid a)))) i)
        ∙∙ (λ j → (λ i → ∣ merid a (~ i ∨ j) ∣)
                 ∙ (cong ∣_∣ₕ (compPath-filler' (merid a) (sym (merid (ptSn _))) (~ j)) ∙ (λ i → -ₖ'-gen n m (inr p) (inr q) (P i))))
        ∙ sym (lUnit _))

  code≡sym : (x : coHomK (2 + k)) → (p : 0ₖ _ ≡ x) → code x p ≡ sym p
  code≡sym x = J (λ x p → code x p ≡ sym p) refl

cong-cong-ₖ'-gen-inr : {k : ℕ} (n m : ℕ) (p : _) (q : _)
    (P : Square (refl {x = 0ₖ (suc (suc k))}) refl refl refl)
  → cong (cong (-ₖ'-gen n m (inr p) (inr q))) P ≡ sym P
cong-cong-ₖ'-gen-inr n m p q P =
     rUnit _
  ∙∙ (λ k → (λ i → cong-ₖ'-gen-inr n m p q refl (i ∧ k))
          ∙∙ (λ i → cong-ₖ'-gen-inr n m p q (P i) k)
          ∙∙ λ i → cong-ₖ'-gen-inr n m p q refl (~ i ∧ k))
  ∙∙ (λ k → transportRefl refl k
          ∙∙ cong sym P
          ∙∙ transportRefl refl k)
  ∙∙ sym (rUnit (cong sym P))
  ∙∙ sym (sym≡cong-sym P)

Kn→ΩKn+1-ₖ'' : {k : ℕ} (n m : ℕ) (p : _) (q : _) (x : coHomK k)
  → Kn→ΩKn+1 k (-ₖ'-gen n m (inr p) (inr q) x) ≡ sym (Kn→ΩKn+1 k x)
Kn→ΩKn+1-ₖ'' n m p q x = cong (Kn→ΩKn+1 _) (-ₖ'-gen-inr≡-ₖ' n m p q x) ∙ Kn→ΩKn+1-ₖ _ x

transpΩ² : {n m : ℕ} (p q : n ≡ m) → (P : _)
        → transport (λ i → refl {x = 0ₖ (p i)} ≡ refl {x = 0ₖ (p i)}) P
        ≡ transport (λ i → refl {x = 0ₖ (q i)} ≡ refl {x = 0ₖ (q i)}) P
transpΩ² p q P k = subst (λ n → refl {x = 0ₖ n} ≡ refl {x = 0ₖ n}) (isSetℕ _ _ p q k) P

-- Some technical lemmas about Kn→Ω²Kn+2 and its interaction with -ₖ'ⁿ̇*ᵐ and transports
-- TODO : Check if this can be cleaned up more by having more general lemmas
private
  lem₁ : (n : ℕ) (a : _)
    → (cong (cong (subst coHomK (+'-comm (suc zero) (suc (suc n)))))
          (Kn→Ω²Kn+2 ∣ a ∣ₕ))
     ≡ ΩKn+1→Ω²Kn+2
       (sym (transp0₁ n) ∙∙ cong (subst coHomK (+'-comm (suc zero) (suc n))) (Kn→ΩKn+1 (suc n) ∣ a ∣ₕ) ∙∙ transp0₁ n)
  lem₁ zero a =
       (λ k i j → transportRefl (Kn→Ω²Kn+2 ∣ a ∣ₕ i j) k)
     ∙ cong ΩKn+1→Ω²Kn+2 λ k → rUnit (λ i → transportRefl (Kn→ΩKn+1 1 ∣ a ∣ i) (~ k)) k
  lem₁ (suc n) a =
       (λ k → transp (λ i → refl {x = 0ₖ (+'-comm 1 (suc (suc (suc n))) (i ∨ ~ k))}
                            ≡ refl {x = 0ₖ (+'-comm 1 (suc (suc (suc n))) (i ∨ ~ k))}) (~ k)
                (λ i j → transp (λ i → coHomK (+'-comm 1 (suc (suc (suc n))) (i ∧ ~ k))) k
                (Kn→Ω²Kn+2 ∣ a ∣ₕ i j)))
    ∙∙ transpΩ² (+'-comm 1 (suc (suc (suc n))))
                (cong suc (+'-comm (suc zero) (suc (suc n))))
                (Kn→Ω²Kn+2 ∣ a ∣ₕ)
    ∙∙ sym (natTranspLem {A = λ n → 0ₖ n ≡ 0ₖ n}
             (Kn→ΩKn+1 (suc (suc n)) ∣ a ∣)
              (λ _ → ΩKn+1→Ω²Kn+2)
              (+'-comm 1 (suc (suc n))))
    ∙∙ cong ΩKn+1→Ω²Kn+2
         (λ k → transp (λ i → 0ₖ (+'-comm (suc zero) (suc (suc n)) (i ∨ k))
                              ≡ 0ₖ (+'-comm (suc zero) (suc (suc n)) (i ∨ k))) k
          (λ i → transp (λ i → coHomK (+'-comm (suc zero) (suc (suc n)) (i ∧ k))) (~ k)
           (Kn→ΩKn+1 _ ∣ a ∣ₕ i)))
    ∙∙ cong ΩKn+1→Ω²Kn+2 (rUnit (cong (subst coHomK (+'-comm (suc zero) (suc (suc n))))
                                   (Kn→ΩKn+1 (suc (suc n)) ∣ a ∣ₕ)))

  lem₂ : (n : ℕ) (a : _) (p : _) (q : _)
    → (cong (cong (-ₖ'-gen (suc (suc n)) (suc zero) p q
                  ∘ (subst coHomK (+'-comm 1 (suc (suc n))))))
             (Kn→Ω²Kn+2 (∣ a ∣ₕ)))
     ≡ ΩKn+1→Ω²Kn+2
         (sym (transp0₁ n)
       ∙∙ cong (subst coHomK (+'-comm (suc zero) (suc n)))
                (cong (-ₖ'-gen (suc (suc n)) (suc zero) p q)
                 (Kn→ΩKn+1 (suc n) ∣ a ∣ₕ))
       ∙∙ transp0₁ n)
  lem₂ n a (inl x) (inr y) =
       (λ k i j → (-ₖ'-gen-inl-left (suc (suc n)) 1 x (inr y) (
                    subst coHomK (+'-comm 1 (suc (suc n)))
                  (Kn→Ω²Kn+2 ∣ a ∣ₕ i j))) k)
    ∙∙ lem₁ n a
    ∙∙ cong ΩKn+1→Ω²Kn+2 (cong (sym (transp0₁ n) ∙∙_∙∙ transp0₁ n)
      λ k i → subst coHomK (+'-comm 1 (suc n))
              (-ₖ'-gen-inl-left (suc (suc n)) 1 x (inr y) (Kn→ΩKn+1 (suc n) ∣ a ∣ i) (~ k)))
  lem₂ n a (inr x) (inr y) =
       cong-cong-ₖ'-gen-inr (suc (suc n)) 1 x y
         (cong
        (cong
         (subst coHomK (+'-comm 1 (suc (suc n)))))
        (Kn→Ω²Kn+2 ∣ a ∣ₕ))
    ∙∙ cong sym (lem₁ n a)
    ∙∙ λ k → ΩKn+1→Ω²Kn+2
                (sym (transp0₁ n) ∙∙
                 cong (subst coHomK (+'-comm 1 (suc n)))
                 (cong-ₖ'-gen-inr (suc (suc n)) 1 x y
                  (Kn→ΩKn+1 (suc n) ∣ a ∣) (~ k))
                 ∙∙ transp0₁ n)

  lem₃ : (n m : ℕ) (q : _) (p : isEvenT (suc (suc n)) ⊎ isOddT (suc (suc n))) (x : _)
    → (((sym (cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (transp0₂ m n))
                                 ∙∙ (λ j → -ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q
                                (subst coHomK (+'-comm (suc (suc m)) (suc n)) (Kn→ΩKn+1 _ x j)))
                    ∙∙ cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (transp0₂ m n))))
     ≡ (Kn→ΩKn+1 _ (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q
                      (subst coHomK (cong suc (+-comm (suc m) n)) x)))
  lem₃ n m q p x =
    sym (cong-∙∙ (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (sym (transp0₂ m n))
        (λ j → subst coHomK (+'-comm (suc (suc m)) (suc n)) (Kn→ΩKn+1 _ x j))
        (transp0₂ m n))
          ∙ h n m p q x
    where
    help : (n m : ℕ) (x : _)
      → ((sym (transp0₂ m n))
         ∙∙ (λ j → subst coHomK (+'-comm (suc (suc m)) (suc n))
                     (Kn→ΩKn+1 (suc (suc (m + n))) x j))
         ∙∙ transp0₂ m n)
         ≡ Kn→ΩKn+1 (suc (n + suc m))
                  (subst coHomK (cong suc (+-comm (suc m) n)) x)
    help zero m x =
         sym (rUnit _)
      ∙∙ (λ k i → transp (λ i → coHomK (+'-comm (suc (suc m)) 1 (i ∨ k))) k
            (Kn→ΩKn+1 _
              (transp (λ i → coHomK (predℕ (+'-comm (suc (suc m)) 1 (i ∧ k)))) (~ k) x) i))
      ∙∙ cong (Kn→ΩKn+1 _)
           λ k → subst coHomK (isSetℕ _ _ (cong predℕ (+'-comm (suc (suc m)) 1))
                   (cong suc (+-comm (suc m) zero)) k) x
    help (suc n) m x =
      sym (rUnit _)
      ∙∙ ((λ k i → transp (λ i → coHomK (+'-comm (suc (suc m)) (suc (suc n)) (i ∨ k))) k
            (Kn→ΩKn+1 _
             (transp (λ i → coHomK (predℕ (+'-comm (suc (suc m)) (suc (suc n)) (i ∧ k)))) (~ k) x) i)))
      ∙∙ cong (Kn→ΩKn+1 _)
          (λ k → subst coHomK (isSetℕ _ _ (cong predℕ (+'-comm (suc (suc m)) (suc (suc n))))
                                            (cong suc (+-comm (suc m) (suc n))) k) x)

    h : (n m : ℕ) (p : isEvenT (suc (suc n)) ⊎ isOddT (suc (suc n))) (q : _) (x : _)
      →  cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q)
           (sym (transp0₂ m n)
            ∙∙ (λ j → subst coHomK (+'-comm (suc (suc m)) (suc n))
                       (Kn→ΩKn+1 (suc (suc (m + n))) x j))
            ∙∙ transp0₂ m n)
        ≡  Kn→ΩKn+1 (suc (n + suc m))
            (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q
             (subst coHomK (cong suc (+-comm (suc m) n)) x))
    h n m (inl p) (inl q) x =
         (λ k → cong (-ₖ'-gen (suc n) (suc (suc m))
                  (isPropEvenOrOdd (suc n) (evenOrOdd (suc n)) (inr p) k) (inl q))
                    (help n m x k))
      ∙∙ ((λ k i → -ₖ'-gen-inl-right (suc n) (suc (suc m)) (inr p) q (help n m x i1 i) k))
      ∙∙ λ i → Kn→ΩKn+1 (suc (n + suc m))
                 (-ₖ'-gen-inl-right (suc n) (suc (suc m)) (isPropEvenOrOdd (suc n) (inr p) (evenOrOdd (suc n)) i) q
                  (subst coHomK (cong suc (+-comm (suc m) n)) x) (~ i))
    h n m (inl p) (inr q) x =
       (λ k → cong (-ₖ'-gen (suc n) (suc (suc m)) (isPropEvenOrOdd (suc n) (evenOrOdd (suc n)) (inr p) k) (inr q))
           (help n m x k))
     ∙∙ cong-ₖ'-gen-inr (suc n) (suc (suc m)) p q (help n m x i1)
     ∙∙ sym (Kn→ΩKn+1-ₖ'' (suc n) (suc (suc m)) p q
          (subst coHomK (λ i → suc (+-comm (suc m) n i)) x))
      ∙ λ k → Kn→ΩKn+1 (suc (n + suc m))
        (-ₖ'-gen (suc n) (suc (suc m)) (isPropEvenOrOdd (suc n) (inr p) (evenOrOdd (suc n)) k) (inr q)
         (subst coHomK (cong suc (+-comm (suc m) n)) x))
    h n m (inr p) (inl q) x =
         (λ k → cong (-ₖ'-gen (suc n) (suc (suc m)) (isPropEvenOrOdd (suc n) (evenOrOdd (suc n)) (inl p) k) (inl q))
                   (help n m x k))
      ∙∙ (λ k i → -ₖ'-gen-inl-left (suc n) (suc (suc m)) p (inl q) (help n m x i1 i) k)
      ∙∙ λ k → Kn→ΩKn+1 (suc (n + suc m))
                 (-ₖ'-gen-inl-right (suc n) (suc (suc m)) (evenOrOdd (suc n)) q
                  (subst coHomK (cong suc (+-comm (suc m) n)) x) (~ k))
    h n m (inr p) (inr q) x =
         (λ k → cong (-ₖ'-gen (suc n) (suc (suc m)) (isPropEvenOrOdd (suc n) (evenOrOdd (suc n)) (inl p) k) (inr q))
                    (help n m x k))
      ∙∙ (λ k i → -ₖ'-gen-inl-left (suc n) (suc (suc m)) p (inr q) (help n m x i1 i) k)
      ∙∙ cong (Kn→ΩKn+1 (suc (n + suc m)))
           (sym (-ₖ'-gen-inl-left (suc n) (suc (suc m)) p (inr q)
             (subst coHomK (λ i → suc (+-comm (suc m) n i)) x)))
       ∙ λ k → Kn→ΩKn+1 (suc (n + suc m))
        (-ₖ'-gen (suc n) (suc (suc m)) (isPropEvenOrOdd (suc n) (inl p) (evenOrOdd (suc n)) k) (inr q)
         (subst coHomK (cong suc (+-comm (suc m) n)) x))

  lem₄ : (n m : ℕ) (q : _) (p : isEvenT (suc (suc n)) ⊎ isOddT (suc (suc n))) (a : _) (b : _)
          → cong (Kn→ΩKn+1 _) (((sym (cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (transp0₂ m n))
                                 ∙∙ (λ j → -ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q
                                (subst coHomK (+'-comm (suc (suc m)) (suc n))
                                  (_⌣ₖ_ {n = suc (suc m)} {m = (suc n)} ∣ merid b j ∣ₕ ∣ a ∣)))
                    ∙∙ cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (transp0₂ m n))))
           ≡ cong (Kn→ΩKn+1 _) (Kn→ΩKn+1 _ (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q
                                               (subst coHomK (cong suc (+-comm (suc m) n))
                                               (_⌣ₖ_ {n = suc m} {m = (suc n)} ∣ b ∣ₕ ∣ a ∣))))
  lem₄ n m q p a b = cong (cong (Kn→ΩKn+1 _)) (lem₃ n m q p (_⌣ₖ_ {n = suc m} {m = (suc n)} ∣ b ∣ₕ ∣ a ∣))

  lem₅ : (n m : ℕ) (p : _) (q : _) (a : _) (b : _)
    → cong (cong (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                   ∘ (subst coHomK (+'-comm (suc (suc m)) (suc (suc n))))))
         (ΩKn+1→Ω²Kn+2 (sym (cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (transp0₂ n m))
                     ∙∙ (λ i → -ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
                                   (subst coHomK (+'-comm (suc (suc n)) (suc m))
                                     (_⌣ₖ_ {n = suc (suc n)} {m = suc m} ∣ merid a i ∣ₕ ∣ b ∣ₕ)))
                     ∙∙ cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (transp0₂ n m)))
        ≡ Kn→Ω²Kn+2 (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                       (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
                         (subst coHomK (cong suc (sym (+-suc n m))) (_⌣ₖ_ {n = suc n} {m = suc m} ∣ a ∣ₕ ∣ b ∣ₕ))))
  lem₅ n m p q a b =
       cong (cong (cong (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                        ∘ (subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))))))
            (cong (sym (Kn→ΩKn+10ₖ _) ∙∙_∙∙ Kn→ΩKn+10ₖ _)
              (lem₄ m n p q b a))
     ∙ help p q (_⌣ₖ_ {n = suc n} {m = suc m} ∣ a ∣ ∣ b ∣)
    where
    annoying : (x : _)
      → cong (cong (subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))))
          (Kn→Ω²Kn+2 (subst coHomK (cong suc (+-comm (suc n) m)) x))
         ≡ Kn→Ω²Kn+2 (subst coHomK (cong suc (sym (+-suc n m))) x)
    annoying x =
        ((λ k → transp (λ i → refl {x = 0ₖ ((+'-comm (suc (suc m)) (suc (suc n))) (i ∨  ~ k))}
                              ≡ refl {x = 0ₖ ((+'-comm (suc (suc m)) (suc (suc n))) (i ∨ ~ k))}) (~ k)

                  λ i j → transp (λ i → coHomK (+'-comm (suc (suc m)) (suc (suc n)) (i ∧ ~ k))) k
                    (Kn→Ω²Kn+2 (subst coHomK (cong suc (+-comm (suc n) m)) x) i j)))
      ∙∙ cong (transport (λ i → refl {x = 0ₖ ((+'-comm (suc (suc m)) (suc (suc n))) i)}
                              ≡ refl {x = 0ₖ ((+'-comm (suc (suc m)) (suc (suc n))) i)}))
              (natTranspLem {A = coHomK} x (λ _ → Kn→Ω²Kn+2) (cong suc (+-comm (suc n) m)))
      ∙∙ sym (substComposite (λ n → refl {x = 0ₖ n} ≡ refl {x = 0ₖ n})
             (cong (suc ∘ suc ∘ suc) (+-comm (suc n) m)) (+'-comm (suc (suc m)) (suc (suc n)))
             (Kn→Ω²Kn+2 x))
      ∙∙ (λ k → subst (λ n → refl {x = 0ₖ n} ≡ refl {x = 0ₖ n})
                       (isSetℕ _ _
                         (cong (suc ∘ suc ∘ suc) (+-comm (suc n) m) ∙ (+'-comm (suc (suc m)) (suc (suc n))))
                         (cong (suc ∘ suc ∘ suc) (sym (+-suc n m))) k)
                 (Kn→Ω²Kn+2 x))
      ∙∙ sym (natTranspLem {A = coHomK} x (λ _ → Kn→Ω²Kn+2) (cong suc (sym (+-suc n m))))

    help : (p : _) (q : _) (x : _) →
      cong (cong (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                ∘ subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))))
           (Kn→Ω²Kn+2 (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
                (subst coHomK (cong suc (+-comm (suc n) m)) x)))
        ≡ Kn→Ω²Kn+2
             (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
              (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
               (subst coHomK (cong suc (sym (+-suc n m))) x)))
    help (inl x) (inl y) z =
         (λ k i j →
           -ₖ'-gen-inl-right (suc (suc n)) (suc (suc m)) (inl x) y
             (subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))
               ((ΩKn+1→Ω²Kn+2
                 (Kn→ΩKn+1 _ (-ₖ'-gen-inl-right (suc m) (suc (suc n)) (evenOrOdd (suc m)) x
                  (subst coHomK (cong suc (+-comm (suc n) m)) z) k))) i j)) k)
      ∙∙ annoying z
      ∙∙ cong Kn→Ω²Kn+2
          λ k → (-ₖ'-gen-inl-right (suc (suc n)) (suc (suc m)) (inl x) y
                   (-ₖ'-gen-inl-right (suc m) (suc (suc n)) (evenOrOdd (suc m)) x
                    (subst coHomK (cong suc (sym (+-suc n m))) z) (~ k)) (~ k))
    help (inl x) (inr y) z =
         (λ k i j →
           -ₖ'-gen-inl-left (suc (suc n)) (suc (suc m)) x (inr y)
            (subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))
              (Kn→Ω²Kn+2 (-ₖ'-gen-inl-right (suc m) (suc (suc n)) (evenOrOdd (suc m)) x
                           (subst coHomK (cong suc (+-comm (suc n) m)) z) k) i j)) k)
      ∙∙ annoying z
      ∙∙ cong Kn→Ω²Kn+2
               (λ k → (-ₖ'-gen-inl-left (suc (suc n)) (suc (suc m)) x (inr y)
                 (-ₖ'-gen-inl-right (suc m) (suc (suc n)) (evenOrOdd (suc m)) x
                  (subst coHomK (cong suc (sym (+-suc n m))) z) (~ k)) (~ k)))
    help (inr x) (inl y) z =
         (λ k i j → -ₖ'-gen-inl-right (suc (suc n)) (suc (suc m)) (inr x) y
                      (subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))
                        (Kn→Ω²Kn+2
                          (-ₖ'-gen (suc m) (suc (suc n)) (isPropEvenOrOdd (suc m) (evenOrOdd (suc m)) (inr y) k) (inr x)
                             (subst coHomK (cong suc (+-comm (suc n) m)) z)) i j)) k)
      ∙∙ cong (cong (cong (subst coHomK (+'-comm (suc (suc m)) (suc (suc n))))) ∘  ΩKn+1→Ω²Kn+2)
            (Kn→ΩKn+1-ₖ'' (suc m) (suc (suc n)) y x
                     (subst coHomK (cong suc (+-comm (suc n) m)) z))
      ∙∙ cong sym (annoying z)
      ∙∙ cong ΩKn+1→Ω²Kn+2 (sym (Kn→ΩKn+1-ₖ'' (suc m) (suc (suc n)) y x
                             (subst coHomK (cong suc (sym (+-suc n m))) z)))
      ∙∙ cong Kn→Ω²Kn+2 λ k → (-ₖ'-gen-inl-right (suc (suc n)) (suc (suc m)) (inr x) y
                                  (-ₖ'-gen (suc m) (suc (suc n)) (isPropEvenOrOdd (suc m) (evenOrOdd (suc m)) (inr y) (~ k)) (inr x)
                                   (subst coHomK (cong suc (sym (+-suc n m))) z)) (~ k))
    help (inr x) (inr y) z =
         (λ k → cong-cong-ₖ'-gen-inr (suc (suc n)) (suc (suc m)) x y
                  (λ i j → subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))
                     (Kn→Ω²Kn+2
                       (-ₖ'-gen (suc m) (suc (suc n))
                         (isPropEvenOrOdd (suc m) (evenOrOdd (suc m)) (inl y) k) (inr x)
                          (subst coHomK (cong suc (+-comm (suc n) m)) z)) i j)) k)
      ∙∙ cong (sym ∘ cong (cong (subst coHomK (+'-comm (suc (suc m)) (suc (suc n))))) ∘  Kn→Ω²Kn+2)
               (-ₖ'-gen-inl-left (suc m) (suc (suc n)) y (inr x)
                (subst coHomK (cong suc (+-comm (suc n) m)) z))
      ∙∙ cong sym (annoying z)
      ∙∙ cong (sym ∘ Kn→Ω²Kn+2)
                (sym (-ₖ'-gen-inl-left (suc m) (suc (suc n)) y (inr x)
                      (subst coHomK (cong suc (sym (+-suc n m))) z)))
      ∙∙ cong ΩKn+1→Ω²Kn+2
              λ k → (Kn→ΩKn+1-ₖ'' (suc (suc n)) (suc (suc m)) x y
                      (-ₖ'-gen (suc m) (suc (suc n)) (
                         isPropEvenOrOdd (suc m) (evenOrOdd (suc m)) (inl y) (~ k)) (inr x)
                       (subst coHomK (cong suc (sym (+-suc n m))) z))) (~ k)

  lem₆ : (n m : ℕ) (p : _) (q : _) (a : _) (b : _)
    → flipSquare
        (Kn→Ω²Kn+2 (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q
                     (subst coHomK (cong suc (+-comm (suc m) n))
                     (_⌣ₖ_ {n = suc m} {m = (suc n)} ∣ b ∣ₕ ∣ a ∣))))
       ≡ Kn→Ω²Kn+2
         (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
           (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
             (subst coHomK (cong suc (sym (+-suc n m)))
               (-ₖ'-gen (suc n) (suc m) (evenOrOdd (suc n)) (evenOrOdd (suc m))
                 (subst coHomK (+'-comm (suc m) (suc n)) (∣ b ∣ₕ ⌣ₖ ∣ a ∣ₕ))))))
  lem₆ n m p q a b =
      sym (sym≡flipSquare (Kn→Ω²Kn+2 (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q
                     (subst coHomK (cong suc (+-comm (suc m) n))
                     (_⌣ₖ_ {n = suc m} {m = (suc n)} ∣ b ∣ₕ ∣ a ∣)))))
     ∙ cong ΩKn+1→Ω²Kn+2
           (help₁
             (subst coHomK (cong suc (+-comm (suc m) n))
               (_⌣ₖ_ {n = suc m} {m = (suc n)} ∣ b ∣ ∣ a ∣)) p q
          ∙ cong (Kn→ΩKn+1 _) (sym (help₂ (∣ b ∣ ⌣ₖ ∣ a ∣))))
    where
    help₁ : (x : _) (p : _) (q : _)
      → sym (Kn→ΩKn+1 (suc (n + suc m)) (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q x))
       ≡ Kn→ΩKn+1 (suc (n + suc m)) ((-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
          (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
           (-ₖ'-gen (suc n) (suc m) (evenOrOdd (suc n)) (evenOrOdd (suc m)) x))))
    help₁ z (inl x) (inl y) =
         cong (λ x → sym (Kn→ΩKn+1 (suc (n + suc m)) x))
           (-ₖ'-gen-inl-right (suc n) (suc (suc m)) (evenOrOdd (suc n)) y z)
      ∙∙ sym (Kn→ΩKn+1-ₖ'' (suc n) (suc m) x y z)
      ∙∙ λ k → Kn→ΩKn+1 (suc (n + suc m))
        (-ₖ'-gen-inl-right (suc (suc n)) (suc (suc m)) (inl x) y
         (-ₖ'-gen-inl-right (suc m) (suc (suc n)) (evenOrOdd (suc m)) x
          (-ₖ'-gen (suc n) (suc m)
            (isPropEvenOrOdd (suc n) (inr x) (evenOrOdd (suc n)) k)
            (isPropEvenOrOdd (suc m) (inr y) (evenOrOdd (suc m)) k) z) (~ k)) (~ k))
    help₁ z (inl x) (inr y) =
         (λ k → sym (Kn→ΩKn+1 (suc (n + suc m))
                      (-ₖ'-gen (suc n) (suc (suc m))
                        (isPropEvenOrOdd (suc n) (evenOrOdd (suc n)) (inr x) k) (inr y) z)))
      ∙∙ cong sym (Kn→ΩKn+1-ₖ'' (suc n) (suc (suc m)) x y z)
      ∙∙ cong (Kn→ΩKn+1 (suc (n + suc m))) (sym (-ₖ'-gen-inl-right (suc n) (suc m) (inr x) y z))
       ∙ λ k → Kn→ΩKn+1 (suc (n + suc m))
        (-ₖ'-gen-inl-left (suc (suc n)) (suc (suc m)) x (inr y)
         (-ₖ'-gen-inl-right (suc m) (suc (suc n)) (evenOrOdd (suc m)) x
          (-ₖ'-gen (suc n) (suc m)
            (isPropEvenOrOdd (suc n) (inr x) (evenOrOdd (suc n)) k)
            (isPropEvenOrOdd (suc m) (inl y) (evenOrOdd (suc m)) k) z) (~ k)) (~ k))
    help₁ z (inr x) (inl y) =
         cong (λ x → sym (Kn→ΩKn+1 (suc (n + suc m)) x))
           (-ₖ'-gen-inl-right (suc n) (suc (suc m)) (evenOrOdd (suc n)) y z)
      ∙∙ (λ k → Kn→ΩKn+1-ₖ'' (suc m) (suc (suc n)) y x
                  (-ₖ'-gen-inl-left (suc n) (suc m) x (inr y) z (~ k)) (~ k))
      ∙∙ λ k → Kn→ΩKn+1 (suc (n + suc m))
                 (-ₖ'-gen-inl-right (suc (suc n)) (suc (suc m)) (inr x) y
                  (-ₖ'-gen (suc m) (suc (suc n))
                    (isPropEvenOrOdd (suc m) (inr y) (evenOrOdd (suc m)) k) (inr x)
                   (-ₖ'-gen (suc n) (suc m)
                     (isPropEvenOrOdd (suc n) (inl x) (evenOrOdd (suc n)) k)
                     (isPropEvenOrOdd (suc m) (inr y) (evenOrOdd (suc m)) k) z)) (~ k))
    help₁ z (inr x) (inr y) =
         ((λ k → sym (Kn→ΩKn+1 (suc (n + suc m))
                      (-ₖ'-gen (suc n) (suc (suc m))
                        (isPropEvenOrOdd (suc n) (evenOrOdd (suc n)) (inl x) k) (inr y) z))))
      ∙∙ cong sym (cong (Kn→ΩKn+1 (suc (n + suc m))) (-ₖ'-gen-inl-left (suc n) (suc (suc m)) x (inr y) z))
      ∙∙ (λ k → sym (Kn→ΩKn+1 (suc (n + suc m))
                     (-ₖ'-gen-inl-left (suc m) (suc (suc n)) y (inr x)
                       (-ₖ'-gen-inl-right (suc n) (suc m) (inl x) y z (~ k)) (~ k))))
       ∙ λ k → Kn→ΩKn+1-ₖ'' (suc (suc n)) (suc (suc m)) x y
                  (-ₖ'-gen (suc m) (suc (suc n)) (isPropEvenOrOdd (suc m) (inl y) (evenOrOdd (suc m)) k) (inr x)
                   (-ₖ'-gen (suc n) (suc m)
                     (isPropEvenOrOdd (suc n) (inl x) (evenOrOdd (suc n)) k)
                     (isPropEvenOrOdd (suc m) (inl y) (evenOrOdd (suc m)) k)  z)) (~ k)

    help₂ : (x : _) →
       (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
         (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
           (subst coHomK (cong suc (sym (+-suc n m)))
             (-ₖ'-gen (suc n) (suc m) (evenOrOdd (suc n)) (evenOrOdd (suc m))
               (subst coHomK (+'-comm (suc m) (suc n)) x)))))
     ≡ -ₖ'-gen (suc (suc n)) (suc (suc m)) p q
        (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
          (-ₖ'-gen (suc n) (suc m) (evenOrOdd (suc n)) (evenOrOdd (suc m))
            (subst coHomK (cong suc (+-comm (suc m) n)) x)))
    help₂ x =
         (λ k → -ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                  (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
                    (transp (λ i → coHomK ((cong suc (sym (+-suc n m))) (i ∨ k))) k
                     (-ₖ'-gen (suc n) (suc m) (evenOrOdd (suc n)) (evenOrOdd (suc m))
                       (transp (λ i → coHomK ((cong suc (sym (+-suc n m))) (i ∧ k))) (~ k)
                         (subst coHomK (+'-comm (suc m) (suc n)) x))))))
       ∙ cong (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                 ∘ -ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
                 ∘ -ₖ'-gen (suc n) (suc m) (evenOrOdd (suc n)) (evenOrOdd (suc m)))
              (sym (substComposite coHomK (+'-comm (suc m) (suc n)) ((cong suc (sym (+-suc n m)))) x)
              ∙ λ k → subst coHomK (isSetℕ _ _ (+'-comm (suc m) (suc n) ∙ cong suc (sym (+-suc n m)))
                        ((cong suc (+-comm (suc m) n))) k) x)

  lem₇ : (n : ℕ) (a : _) (p : _) (q : _)
    → ((λ i → Kn→ΩKn+1 _ (-ₖ'-gen (suc n) (suc zero) (evenOrOdd (suc n)) (inr tt)
                          (transp0₁ n (~ i))))
    ∙∙ (λ i j → Kn→ΩKn+1 _ (-ₖ'-gen (suc n) (suc zero) (evenOrOdd (suc n)) (inr tt)
                              (subst coHomK (+'-comm (suc zero) (suc n)) (Kn→ΩKn+1 (suc n) ∣ a ∣ₕ i))) j)
    ∙∙ (λ i → Kn→ΩKn+1 _ (-ₖ'-gen (suc n) (suc zero) (evenOrOdd (suc n)) (inr tt)
                          (transp0₁ n i))))
       ≡ (cong (Kn→ΩKn+1 (suc (suc (n + zero))))
           (sym (transp0₁ n)
         ∙∙ sym (cong (subst coHomK (+'-comm (suc zero) (suc n)))
                 (cong (-ₖ'-gen (suc (suc n)) (suc zero) p q) (Kn→ΩKn+1 (suc n) ∣ a ∣ₕ)))
         ∙∙ transp0₁ n))
  lem₇ zero a (inl x) (inr tt) =
      (λ k → rUnit ((cong (Kn→ΩKn+1 _) (cong-ₖ'-gen-inr (suc zero) (suc zero) tt tt
                      (λ i → (subst coHomK (+'-comm (suc zero) (suc zero))
                       (Kn→ΩKn+1 (suc zero) ∣ a ∣ₕ i))) k))) (~ k))
    ∙ λ k → ((cong (Kn→ΩKn+1 (suc (suc zero)))
               (rUnit (λ i → subst coHomK (+'-comm (suc zero) (suc zero))
                 (-ₖ'-gen-inl-left (suc (suc zero)) (suc zero) tt (inr tt)
                  (Kn→ΩKn+1 (suc zero) ∣ a ∣ₕ (~ i)) (~ k))) k)))
  lem₇ (suc n) a (inl x) (inr tt) =
      ((λ k → rUnit (cong (Kn→ΩKn+1 _)
        (λ i → -ₖ'-gen (suc (suc n)) (suc zero)
                 (isPropEvenOrOdd n (evenOrOdd (suc (suc n))) (inr x) k) (inr tt)
                   (subst coHomK (+'-comm (suc zero) (suc (suc n)))
                    (Kn→ΩKn+1 (suc (suc n)) ∣ a ∣ₕ i)))) (~ k)))
    ∙∙ (((λ k → ((cong (Kn→ΩKn+1 _) (cong-ₖ'-gen-inr (suc (suc n)) (suc zero) x tt
           (λ i → (subst coHomK (+'-comm (suc zero) (suc (suc n)))
                     (Kn→ΩKn+1 (suc (suc n)) ∣ a ∣ₕ i))) k))))))
    ∙∙ λ k → ((cong (Kn→ΩKn+1 (suc (suc (suc n + zero))))
               (rUnit (λ i → subst coHomK (+'-comm (suc zero) (suc (suc n)))
                 (-ₖ'-gen-inl-left (suc (suc (suc n))) (suc zero) x (inr tt)
                   (Kn→ΩKn+1 (suc (suc n)) ∣ a ∣ₕ (~ i)) (~ k))) k)))
  lem₇ (suc n) a (inr x) (inr tt) =
       (λ k → rUnit (λ i j → Kn→ΩKn+1 _
                  (-ₖ'-gen (suc (suc n)) (suc zero)
                          (isPropEvenOrOdd (suc (suc n)) (evenOrOdd (suc (suc n))) (inl x) k) (inr tt)
                     (subst coHomK (+'-comm (suc zero) (suc (suc n)))
                       (Kn→ΩKn+1 (suc (suc n)) ∣ a ∣ₕ i))) j) (~ k))
    ∙∙ (λ k i j → Kn→ΩKn+1 _ (-ₖ'-gen-inl-left (suc (suc n)) (suc zero) x (inr tt)
                                (subst coHomK (+'-comm (suc zero) (suc (suc n)))
                                  (Kn→ΩKn+1 (suc (suc n)) ∣ a ∣ₕ i)) k) j)
    ∙∙ λ k → cong (Kn→ΩKn+1 _)
              (rUnit (sym (cong (subst coHomK (+'-comm (suc zero) (suc (suc n))))
                (cong-ₖ'-gen-inr (suc (suc (suc n))) (suc zero) x tt (Kn→ΩKn+1 (suc (suc n)) ∣ a ∣ₕ) (~ k)))) k)

-- ∣ a ∣ ⌣ₖ ∣ b ∣ ≡ -ₖ'ⁿ*ᵐ (∣ b ∣ ⌣ₖ ∣ a ∣) for n ≥ 1, m = 1
gradedComm'-elimCase-left : (n : ℕ) (p : _) (q : _) (a : S₊ (suc n)) (b : S¹) →
      (_⌣ₖ_  {n = suc n} {m = (suc zero)} ∣ a ∣ₕ ∣ b ∣ₕ)
    ≡ (-ₖ'-gen (suc n) (suc zero) p q)
       (subst coHomK (+'-comm (suc zero) (suc n))
        (_⌣ₖ_  {n = suc zero} {m = suc n} ∣ b ∣ₕ ∣ a ∣ₕ))
gradedComm'-elimCase-left zero (inr tt) (inr tt) a b =
    proof a b
  ∙ cong (-ₖ'-gen 1 1 (inr tt) (inr tt))
         (sym (transportRefl ((_⌣ₖ_ {n = suc zero} {m = suc zero} ∣ b ∣ ∣ a ∣))))
  where
  help : flipSquare (ΩKn+1→Ω²Kn+2' (λ j i → _⌣ₖ_ {n = suc zero} {m = suc zero} ∣ loop i ∣ₕ ∣ loop j ∣ₕ)) ≡
                    cong (cong (-ₖ'-gen 1 1 (inr tt) (inr tt)))
                      (ΩKn+1→Ω²Kn+2' (λ i j → _⌣ₖ_ {n = suc zero} {m = suc zero} ∣ loop j ∣ₕ ∣ loop i ∣ₕ))
  help = sym (sym≡flipSquare _)
       ∙ sym (cong-cong-ₖ'-gen-inr 1 1 tt tt
              (ΩKn+1→Ω²Kn+2' (λ i j → _⌣ₖ_ {n = suc zero} {m = suc zero} ∣ loop j ∣ ∣ loop i ∣)))

  proof : (a b : S¹) → _⌣ₖ_ {n = suc zero} {m = suc zero} ∣ a ∣ₕ ∣ b ∣ₕ ≡
      -ₖ'-gen 1 1 (inr tt) (inr tt) (_⌣ₖ_ {n = suc zero} {m = suc zero} ∣ b ∣ ∣ a ∣)
  proof base base = refl
  proof base (loop i) k = -ₖ'-gen 1 1 (inr tt) (inr tt) (Kn→ΩKn+10ₖ _ (~ k) i)
  proof (loop i) base k = Kn→ΩKn+10ₖ _ k i
  proof (loop i) (loop j) k =
    hcomp (λ r →  λ { (i = i0) → -ₖ'-gen 1 1 (inr tt) (inr tt) (Kn→ΩKn+10ₖ _ (~ k ∨ ~ r) j)
                     ; (i = i1) → -ₖ'-gen 1 1 (inr tt) (inr tt) (Kn→ΩKn+10ₖ _ (~ k ∨ ~ r) j)
                     ; (j = i0) → Kn→ΩKn+10ₖ _ (k ∨ ~ r) i
                     ; (j = i1) → Kn→ΩKn+10ₖ _ (k ∨ ~ r) i
                     ; (k = i0) → doubleCompPath-filler
                                    (sym (Kn→ΩKn+10ₖ _))
                                    (λ j i → _⌣ₖ_ {n = suc zero} {m = suc zero} ∣ loop i ∣ₕ ∣ loop j ∣ₕ)
                                    (Kn→ΩKn+10ₖ _) (~ r) j i
                     ; (k = i1) → (-ₖ'-gen 1 1 (inr tt) (inr tt)
                                    (doubleCompPath-filler
                                     (sym (Kn→ΩKn+10ₖ _))
                                     (λ i j → _⌣ₖ_ {n = suc zero} {m = suc zero} ∣ loop j ∣ₕ ∣ loop i ∣ₕ)
                                     (Kn→ΩKn+10ₖ _) (~ r) i j))})
          (help k i j)
gradedComm'-elimCase-left (suc n) p q north b =
  cong (-ₖ'-gen (suc (suc n)) 1 p q ∘
            (subst coHomK (+'-comm 1 (suc (suc n)))))
              (sym (⌣ₖ-0ₖ _ (suc (suc n)) ∣ b ∣ₕ))
gradedComm'-elimCase-left (suc n) p q south b =
  cong (-ₖ'-gen (suc (suc n)) 1 p q ∘
            (subst coHomK (+'-comm 1 (suc (suc n)))))
              ((sym (⌣ₖ-0ₖ _ (suc (suc n)) ∣ b ∣ₕ)) ∙ λ i → ∣ b ∣ ⌣ₖ ∣ merid (ptSn (suc n)) i ∣ₕ)
gradedComm'-elimCase-left (suc n) p q (merid a i) base k =
  hcomp (λ j → λ {(i = i0) → (-ₖ'-gen (suc (suc n)) 1 p q ∘
                                  (subst coHomK (+'-comm 1 (suc (suc n)))))
                                    (0ₖ _)
                 ; (i = i1) → (-ₖ'-gen (suc (suc n)) 1 p q ∘
                                  (subst coHomK (+'-comm 1 (suc (suc n)))))
                                    (compPath-filler (sym (⌣ₖ-0ₖ _ (suc (suc n)) ∣ base ∣ₕ))
                                                     (λ i → ∣ base ∣ ⌣ₖ ∣ merid a i ∣ₕ) j k)
                 ; (k = i0) → _⌣ₖ_ {n = suc (suc n)} {m = suc zero} ∣ merid a i ∣ₕ ∣ base ∣ₕ
                 ; (k = i1) → -ₖ'-gen (suc (suc n)) 1 p q
                                (subst coHomK (+'-comm 1 (suc (suc n)))
                                 (∣ base ∣ₕ ⌣ₖ ∣ merid a i ∣ₕ))})
        (hcomp (λ j → λ {(i = i0) → ∣ north ∣
                        ; (i = i1) → ∣ north ∣
                        ; (k = i0) → (sym (Kn→ΩKn+10ₖ _)
                                    ∙ (λ j → Kn→ΩKn+1 _
                                         (sym (gradedComm'-elimCase-left n (evenOrOdd (suc n)) (inr tt) a base
                                        ∙ cong (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt)) (transp0₁ n)) j))) j i
                        ; (k = i1) → ∣ north ∣})
               ∣ north ∣)
gradedComm'-elimCase-left (suc n) p q (merid a i) (loop j) k =
  hcomp (λ r →
    λ { (i = i0) → (-ₖ'-gen (suc (suc n)) 1 p q ∘
                      (subst coHomK (+'-comm 1 (suc (suc n)))))
                        (sym (⌣ₖ-0ₖ _ (suc (suc n)) ∣ (loop j) ∣ₕ) k)
      ; (i = i1) → (-ₖ'-gen (suc (suc n)) 1 p q ∘
                      (subst coHomK (+'-comm 1 (suc (suc n)))))
                        (compPath-filler (sym (⌣ₖ-0ₖ _ (suc (suc n)) ∣ (loop j) ∣ₕ))
                          (λ i → ∣ loop j ∣ ⌣ₖ ∣ merid (ptSn (suc n)) i ∣ₕ) r k)
      ; (k = i0) → _⌣ₖ_ {n = suc (suc n)} {m = suc zero} ∣ merid a i ∣ₕ ∣ loop j ∣ₕ
      ; (k = i1) → -ₖ'-gen (suc (suc n)) 1 p q
                     (subst coHomK (+'-comm 1 (suc (suc n)))
                      (_⌣ₖ_ {n = suc zero} {m = suc (suc n)} ∣ loop j ∣ₕ
                        ∣ compPath-filler (merid a) (sym (merid (ptSn (suc n)))) (~ r) i ∣ₕ))})
        (hcomp (λ r →
          λ { (i = i0) → (-ₖ'-gen (suc (suc n)) 1 p q ∘
                            (subst coHomK (+'-comm 1 (suc (suc n)))))
                              ∣ rCancel (merid (ptSn (suc (suc n)))) (~ k ∧ r) j ∣
            ; (i = i1) → (-ₖ'-gen (suc (suc n)) 1 p q ∘
                            (subst coHomK (+'-comm 1 (suc (suc n)))))
                              ∣ rCancel (merid (ptSn (suc (suc n)))) (~ k ∧ r) j ∣
            ; (k = i0) → help₂ r i j
            ; (k = i1) → -ₖ'-gen (suc (suc n)) 1 p q
                           (subst coHomK (+'-comm 1 (suc (suc n)))
                            (_⌣ₖ_ {n = suc zero} {m = suc (suc n)} ∣ loop j ∣ₕ
                              (Kn→ΩKn+1 _ ∣ a ∣ₕ i)))})
   (-ₖ'-gen (suc (suc n)) 1 p q
                           (subst coHomK (+'-comm 1 (suc (suc n)))
                            (_⌣ₖ_ {n = suc zero} {m = suc (suc n)} ∣ loop j ∣ₕ
                              (Kn→ΩKn+1 _ ∣ a ∣ₕ i)))))
    where
    P : Path _ (Kn→ΩKn+1 (suc (suc (n + 0))) (0ₖ _))
               (Kn→ΩKn+1 (suc (suc (n + 0))) (_⌣ₖ_ {n = (suc n)} {m = suc zero} ∣ a ∣ ∣ base ∣))
    P i = Kn→ΩKn+1 (suc (suc (n + 0)))
            ((sym (gradedComm'-elimCase-left n (evenOrOdd (suc n)) (inr tt) a base
              ∙ cong (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt)) (transp0₁ n)) i))

    help₁ : (P ∙∙ ((λ i j → _⌣ₖ_ {n = suc (suc n)} {m = suc zero} ∣ merid a j ∣ₕ ∣ loop i ∣ₕ)) ∙∙ sym P)
         ≡ ((λ i → Kn→ΩKn+1 _ (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt)
                                   (transp0₁ n (~ i))))
        ∙∙ (λ i j → Kn→ΩKn+1 _ (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt)
                                  (subst coHomK (+'-comm 1 (suc n)) (∣ loop i ∣ₕ ⌣ₖ ∣ a ∣ₕ))) j)
        ∙∙ (λ i → Kn→ΩKn+1 _ (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt)
                                   (transp0₁ n i))))
    help₁ k i j =
        ((λ i → (Kn→ΩKn+1 (suc (suc (n + 0))))
                  (compPath-filler'
                    ((gradedComm'-elimCase-left n (evenOrOdd (suc n)) (inr tt) a base))
                   (cong (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt))
                    (transp0₁ n)) (~ k) (~ i)))
       ∙∙ (λ i j → (Kn→ΩKn+1 _
                     (gradedComm'-elimCase-left n (evenOrOdd (suc n)) (inr tt) a (loop i) k) j))
       ∙∙ λ i → (Kn→ΩKn+1 (suc (suc (n + 0))))
                   (compPath-filler'
                     ((gradedComm'-elimCase-left n (evenOrOdd (suc n)) (inr tt) a base))
                    (cong (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt))
                     (transp0₁ n)) (~ k) i)) i j

    help₂ : I → I → I → coHomK _
    help₂ r i j =
      hcomp (λ k →
        λ { (i = i0) → (-ₖ'-gen (suc (suc n)) 1 p q ∘
                           subst coHomK (+'-comm 1 (suc (suc n))))
                          ∣ rCancel (merid (ptSn (suc (suc n)))) (~ k ∨ r) j ∣
          ; (i = i1) → (-ₖ'-gen (suc (suc n)) 1 p q ∘
                           subst coHomK (+'-comm 1 (suc (suc n))))
                          ∣ rCancel (merid (ptSn (suc (suc n)))) (~ k ∨ r) j ∣
          ; (j = i0) → compPath-filler (sym (Kn→ΩKn+10ₖ (suc (suc (n + 0)))))
                          P k r i
          ; (j = i1) → compPath-filler (sym (Kn→ΩKn+10ₖ (suc (suc (n + 0)))))
                          P k r i
          ; (r = i0) → -ₖ'-gen (suc (suc n)) 1 p q
                         (subst coHomK (+'-comm 1 (suc (suc n)))
                           (doubleCompPath-filler (sym (Kn→ΩKn+10ₖ _))
                             (λ i j → _⌣ₖ_ {n = suc zero} {m = suc (suc n)} ∣ loop j ∣ₕ
                                         (Kn→ΩKn+1 (suc n) ∣ a ∣ₕ i)) (Kn→ΩKn+10ₖ _) (~ k) i j))
          ; (r = i1) → doubleCompPath-filler P
                         (λ i j → _⌣ₖ_ {n = suc (suc n)} {m = suc zero} ∣ merid a j ∣ₕ ∣ loop i ∣ₕ)
                         (sym P) (~ k) j i})
             (hcomp (λ k →
               λ { (i = i0) → ∣ north ∣
                 ; (i = i1) → ∣ north ∣
                 ; (j = i0) → (Kn→ΩKn+10ₖ (suc (suc (n + 0)))) (~ r) i
                 ; (j = i1) → (Kn→ΩKn+10ₖ (suc (suc (n + 0)))) (~ r) i
                 ; (r = i0) → lem₂ n a p q (~ k) i j
                 ; (r = i1) → help₁ (~ k) j i})
                    (hcomp (λ k →
                      λ { (i = i0) → ∣ north ∣
                        ; (i = i1) → ∣ north ∣
                        ; (j = i0) → Kn→ΩKn+10ₖ (suc (suc (n + 0))) (~ r) i
                        ; (j = i1) → Kn→ΩKn+10ₖ (suc (suc (n + 0))) (~ r) i
                        ; (r = i0) → flipSquare≡cong-sym (flipSquare (ΩKn+1→Ω²Kn+2
                                                (sym (transp0₁ n)
                                              ∙∙ cong (subst coHomK (+'-comm 1 (suc n)))
                                                  (cong (-ₖ'-gen (suc (suc n)) 1 p q)
                                                   (Kn→ΩKn+1 (suc n) ∣ a ∣ₕ))
                                              ∙∙ transp0₁ n))) (~ k) i j
                        ; (r = i1) → ((λ i → Kn→ΩKn+1 _ (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt)
                                                 (transp0₁ n (~ i))))
                                    ∙∙ (λ i j → Kn→ΩKn+1 _ (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt)
                                                  (subst coHomK (+'-comm 1 (suc n)) (Kn→ΩKn+1 (suc n) ∣ a ∣ₕ i))) j)
                                    ∙∙ (λ i → Kn→ΩKn+1 _ (-ₖ'-gen (suc n) 1 (evenOrOdd (suc n)) (inr tt)
                                                  (transp0₁ n i)))) j i})
                              (hcomp (λ k →
                                λ { (i = i0) → ∣ north ∣
                                  ; (i = i1) → ∣ north ∣
                                  ; (j = i0) → Kn→ΩKn+10ₖ (suc (suc (n + 0))) (~ r ∧ k) i
                                  ; (j = i1) → Kn→ΩKn+10ₖ (suc (suc (n + 0))) (~ r ∧ k) i
                                  ; (r = i0) → doubleCompPath-filler
                                                  (sym (Kn→ΩKn+10ₖ _))
                                                  (cong (Kn→ΩKn+1 (suc (suc (n + 0))))
                                                      (sym (transp0₁ n)
                                                    ∙∙ sym (cong (subst coHomK (+'-comm 1 (suc n)))
                                                             (cong (-ₖ'-gen (suc (suc n)) 1 p q)
                                                               (Kn→ΩKn+1 (suc n) ∣ a ∣ₕ)))
                                                    ∙∙ transp0₁ n))
                                                (Kn→ΩKn+10ₖ _) k j i
                                  ; (r = i1) → lem₇ n a p q (~ k) j i})
                                         (lem₇ n a p q i1 j i))))

-- ∣ a ∣ ⌣ₖ ∣ b ∣ ≡ -ₖ'ⁿ*ᵐ (∣ b ∣ ⌣ₖ ∣ a ∣) for all n, m ≥ 1
gradedComm'-elimCase : (k n m : ℕ) (term : n + m ≡ k) (p : _) (q : _) (a : _) (b : _) →
      (_⌣ₖ_  {n = suc n} {m = (suc m)} ∣ a ∣ₕ ∣ b ∣ₕ)
    ≡ (-ₖ'-gen (suc n) (suc m) p q)
       (subst coHomK (+'-comm (suc m) (suc n))
        (_⌣ₖ_  {n = suc m} {m = suc n} ∣ b ∣ₕ ∣ a ∣ₕ))
gradedComm'-elimCase k zero zero term p q a b = gradedComm'-elimCase-left zero p q a b
gradedComm'-elimCase k zero (suc m) term (inr tt) q a b =
    help q
  ∙ sym (cong (-ₖ'-gen 1 (suc (suc m)) (inr tt) q
             ∘ (subst coHomK (+'-comm (suc (suc m)) 1)))
        (gradedComm'-elimCase-left (suc m) q (inr tt) b a))
  where
  help : (q : _) → ∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ ≡
            -ₖ'-gen 1 (suc (suc m)) (inr tt) q
            (subst coHomK (+'-comm (suc (suc m)) 1)
             (-ₖ'-gen (suc (suc m)) 1 q (inr tt)
              (subst coHomK (+'-comm 1 (suc (suc m))) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ))))
  help (inl x) =
      (sym (transportRefl _)
     ∙ (λ i → subst coHomK (isSetℕ _ _ refl (+'-comm 1 (suc (suc m)) ∙ +'-comm (suc (suc m)) 1) i)
               (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ)))
    ∙∙ substComposite coHomK
         (+'-comm 1 (suc (suc m)))
          (+'-comm (suc (suc m)) 1)
           ((∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ))
    ∙∙ λ i → -ₖ'-gen-inl-right (suc zero) (suc (suc m)) (inr tt) x
            ((subst coHomK (+'-comm (suc (suc m)) 1)
             (-ₖ'-gen-inl-left (suc (suc m)) 1 x (inr tt)
              (subst coHomK (+'-comm 1 (suc (suc m))) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ)) (~ i)))) (~ i)
  help (inr x) =
       (sym (transportRefl _)
    ∙∙ (λ k → subst coHomK (isSetℕ _ _ refl (+'-comm 1 (suc (suc m)) ∙ +'-comm (suc (suc m)) 1) k) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ))
    ∙∙ sym (-ₖ^2 (subst coHomK (+'-comm 1 (suc (suc m)) ∙ +'-comm (suc (suc m)) 1) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ))))
    ∙∙ (λ i → -ₖ'-gen-inr≡-ₖ' 1 (suc (suc m)) tt x
                (-ₖ'-gen-inr≡-ₖ' (suc (suc m)) 1 x tt
                  (substComposite coHomK (+'-comm 1 (suc (suc m))) (+'-comm (suc (suc m)) 1) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ) i)
                  (~ i)) (~ i))
    ∙∙ λ i → (-ₖ'-gen 1 (suc (suc m)) (inr tt) (inr x)
                  (transp (λ j → coHomK ((+'-comm (suc (suc m)) 1) (j ∨ ~ i))) (~ i)
                    (-ₖ'-gen (suc (suc m)) 1 (inr x) (inr tt)
                      (transp (λ j → coHomK ((+'-comm (suc (suc m)) 1) (j ∧ ~ i))) i
                              ((subst coHomK (+'-comm 1 (suc (suc m))) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ)))))))
gradedComm'-elimCase k (suc n) zero term p q a b =
  gradedComm'-elimCase-left (suc n) p q a b
gradedComm'-elimCase zero (suc n) (suc m) term p q a b =
  ⊥.rec (snotz (sym (+-suc n m) ∙ cong predℕ term))
gradedComm'-elimCase (suc zero) (suc n) (suc m) term p q a b =
  ⊥.rec (snotz (sym (+-suc n m) ∙ cong predℕ term))
gradedComm'-elimCase (suc (suc k)) (suc n) (suc m) term p q north north = refl
gradedComm'-elimCase (suc (suc k)) (suc n) (suc m) term p q north south = refl
gradedComm'-elimCase (suc (suc k)) (suc n) (suc m) term p q north (merid a i) r =
  -ₖ'-gen (suc (suc n)) (suc (suc m)) p q (
    (subst coHomK (+'-comm (suc (suc m)) (suc (suc n))))
      ((sym (Kn→ΩKn+10ₖ _)
      ∙ cong (Kn→ΩKn+1 _)
          (cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (sym (transp0₂ n m))
                 ∙ sym (gradedComm'-elimCase (suc k) m (suc n) (+-suc m n ∙ +-comm (suc m) n ∙ cong predℕ term)
             (evenOrOdd (suc m)) p a north))) r i))
gradedComm'-elimCase (suc (suc k)) (suc n) (suc m) term p q south north = refl
gradedComm'-elimCase (suc (suc k)) (suc n) (suc m) term p q south south = refl
gradedComm'-elimCase (suc (suc k)) (suc n) (suc m) term p q south (merid a i) r =
  -ₖ'-gen (suc (suc n)) (suc (suc m)) p q (
    (subst coHomK (+'-comm (suc (suc m)) (suc (suc n))))
      ((sym (Kn→ΩKn+10ₖ _)
      ∙ cong (Kn→ΩKn+1 _)
          (cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (sym (transp0₂ n m))
                  ∙ sym (gradedComm'-elimCase (suc k) m (suc n) (+-suc m n ∙ +-comm (suc m) n ∙ cong predℕ term)
             (evenOrOdd (suc m)) p a south))) r i))
gradedComm'-elimCase (suc (suc k)) (suc n) (suc m) term p q (merid a i) north r =
    (cong (Kn→ΩKn+1 (suc (suc (n + suc m))))
      (gradedComm'-elimCase (suc k) n (suc m) (cong predℕ term) (evenOrOdd (suc n)) q a north
       ∙ cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (transp0₂ m n))
   ∙' Kn→ΩKn+10ₖ _) r i
gradedComm'-elimCase (suc (suc k)) (suc n) (suc m) term p q (merid a i) south r =
    (cong (Kn→ΩKn+1 (suc (suc (n + suc m))))
      (gradedComm'-elimCase (suc k) n (suc m) (cong predℕ term) (evenOrOdd (suc n)) q a south
       ∙ cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (transp0₂ m n))
   ∙' Kn→ΩKn+10ₖ _) r i
gradedComm'-elimCase (suc (suc k)) (suc n) (suc m) term p q (merid a i) (merid b j) r =
  hcomp (λ l →
    λ { (i = i0) → -ₖ'-gen (suc (suc n)) (suc (suc m)) p q (
                     (subst coHomK (+'-comm (suc (suc m)) (suc (suc n))))
                       ((compPath-filler (sym (Kn→ΩKn+10ₖ _))
                        (cong (Kn→ΩKn+1 _)
                          (cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (sym (transp0₂ n m))
                                   ∙ sym (gradedComm'-elimCase (suc k) m (suc n) (+-suc m n ∙ +-comm (suc m) n ∙ cong predℕ term)
                               (evenOrOdd (suc m)) p b north))) l r j)))
       ; (i = i1) → -ₖ'-gen (suc (suc n)) (suc (suc m)) p q (
                     (subst coHomK (+'-comm (suc (suc m)) (suc (suc n))))
                       ((compPath-filler (sym (Kn→ΩKn+10ₖ _))
                        (cong (Kn→ΩKn+1 _)
                          (cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (sym (transp0₂ n m))
                                  ∙ sym (gradedComm'-elimCase (suc k) m (suc n) (+-suc m n ∙ +-comm (suc m) n ∙ cong predℕ term)
                              (evenOrOdd (suc m)) p b south))) l r j)))
       ; (r = i0) → help₂ l i j
       ; (r = i1) → -ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                       (subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))
                        (help₁ l i j))})
   (hcomp (λ l →
     λ { (i = i0) → -ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                      (subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))
                        (Kn→ΩKn+10ₖ _ (~ r ∨ ~ l) j))
       ; (i = i1) → -ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                      (subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))
                        (Kn→ΩKn+10ₖ _ (~ r ∨ ~ l) j))
       ; (j = i0) → Kn→ΩKn+10ₖ _ r i
       ; (j = i1) → Kn→ΩKn+10ₖ _ r i
       ; (r = i0) → lem₄ n m q p a b (~ l) j i
       ; (r = i1) → -ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                      (subst coHomK (+'-comm (suc (suc m)) (suc (suc n)))
                        (doubleCompPath-filler
                         (sym (Kn→ΩKn+10ₖ _))
                          (λ i j → Kn→ΩKn+1 _ ((sym (cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (transp0₂ n m))
                                             ∙∙ (λ i → -ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
                                                           (subst coHomK (+'-comm (suc (suc n)) (suc m))
                                                             (_⌣ₖ_ {n = suc (suc n)} {m = suc m} ∣ merid a i ∣ₕ ∣ b ∣ₕ)))
                                             ∙∙ cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (transp0₂ n m)) i) j)
                          (Kn→ΩKn+10ₖ _) (~ l) i j))})
        (hcomp (λ l →
          λ { (i = i0) → ∣ north ∣
            ; (i = i1) → ∣ north ∣
            ; (j = i0) → Kn→ΩKn+10ₖ _ r i
            ; (j = i1) → Kn→ΩKn+10ₖ _ r i
            ; (r = i0) → lem₄ n m q p a b i1 j i
            ; (r = i1) → lem₅ n m p q a b (~ l) i j})
            (hcomp (λ l →
              λ { (i = i0) → ∣ north ∣
                ; (i = i1) → ∣ north ∣
                ; (j = i0) → Kn→ΩKn+10ₖ _ (r ∨ ~ l) i
                ; (j = i1) → Kn→ΩKn+10ₖ _ (r ∨ ~ l) i
                ; (r = i0) → doubleCompPath-filler
                               (sym (Kn→ΩKn+10ₖ _))
                               (lem₄ n m q p a b i1)
                               (Kn→ΩKn+10ₖ _) (~ l) j i
                ; (r = i1) → Kn→Ω²Kn+2 (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q
                                            (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
                                              (subst coHomK (cong suc (sym (+-suc n m)))
                                                (gradedComm'-elimCase k n m
                                                  (+-comm n m ∙∙ cong predℕ (+-comm (suc m) n) ∙∙ cong (predℕ ∘ predℕ) term)
                                                  (evenOrOdd (suc n)) (evenOrOdd (suc m)) a b (~ l))))) i j})
                (lem₆ n m p q a b r i j))))
  where
  help₁ : I → I → I → coHomK _
  help₁ l i j =
    Kn→ΩKn+1 _
      (hcomp (λ r
        → λ { (i = i0) → compPath-filler' (cong ((-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p)) (sym (transp0₂ n m)))
                            (sym (gradedComm'-elimCase (suc k) m (suc n) (+-suc m n ∙ +-comm (suc m) n ∙ cong predℕ term)
                                                        (evenOrOdd (suc m)) p b north)) r l
              ; (i = i1) → compPath-filler' (cong ((-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p)) (sym (transp0₂ n m)))
                             (sym (gradedComm'-elimCase (suc k) m (suc n) (+-suc m n ∙ +-comm (suc m) n ∙ cong predℕ term)
                                                        (evenOrOdd (suc m)) p b south)) r l
              ; (l = i0) → doubleCompPath-filler (sym (cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (transp0₂ n m)))
                                                  (λ i → -ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p
                                                           (subst coHomK (+'-comm (suc (suc n)) (suc m))
                                                             (_⌣ₖ_ {n = suc (suc n)} {m = suc m} ∣ merid a i ∣ₕ ∣ b ∣ₕ)))
                                                  (cong (-ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p) (transp0₂ n m)) r i
              ; (l = i1) → _⌣ₖ_ {n = suc m} {m = suc (suc n)} ∣ b ∣ₕ ∣ merid a i ∣ₕ})
          (gradedComm'-elimCase (suc k) m (suc n) (+-suc m n ∙ +-comm (suc m) n ∙ cong predℕ term)
            (evenOrOdd (suc m)) p b (merid a i) (~ l))) j

  help₂ : I → I → I → coHomK _
  help₂ l i j =
    hcomp (λ r →
      λ { (i = i0) → ∣ north ∣
         ; (i = i1) → ∣ north ∣
         ; (j = i0) →
           Kn→ΩKn+1 (suc (suc (n + suc m)))
                (compPath-filler (gradedComm'-elimCase (suc k) n (suc m)
                                  (cong predℕ term) (evenOrOdd (suc n)) q a north)
                  (cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q)  (transp0₂ m n)) r (~ l)) i
         ; (j = i1) →
              Kn→ΩKn+1 (suc (suc (n + suc m)))
                (compPath-filler (gradedComm'-elimCase (suc k) n (suc m)
                                 (cong predℕ term) (evenOrOdd (suc n)) q a south)
                  (cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (transp0₂ m n)) r (~ l)) i
         ; (l = i0) →
           Kn→ΩKn+1 _
             (doubleCompPath-filler (sym (cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (transp0₂ m n)))
                                    (λ j → -ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q
                                             (subst coHomK (+'-comm (suc (suc m)) (suc n))
                                               (_⌣ₖ_ {n = suc (suc m)} {m = (suc n)} ∣ merid b j ∣ₕ ∣ a ∣)))
                                    (cong (-ₖ'-gen (suc n) (suc (suc m)) (evenOrOdd (suc n)) q) (transp0₂ m n)) r j) i
         ; (l = i1) → Kn→ΩKn+1 _ (_⌣ₖ_ {n = (suc n)} {m = suc (suc m)} ∣ a ∣ ∣ merid b j ∣ₕ) i})
          (hcomp (λ r →
            λ { (i = i0) → ∣ north ∣
              ; (i = i1) → ∣ north ∣
              ; (j = i0) → Kn→ΩKn+1 (suc (suc (n + suc m)))
                             (gradedComm'-elimCase (suc k) n (suc m)
                               (cong predℕ term) (evenOrOdd (suc n)) q a north (~ l ∨ ~ r)) i
              ; (j = i1) → Kn→ΩKn+1 (suc (suc (n + suc m)))
                             (gradedComm'-elimCase (suc k) n (suc m)
                               (cong predℕ term) (evenOrOdd (suc n)) q a south (~ l ∨ ~ r)) i
              ; (l = i0) → Kn→ΩKn+1 (suc (suc (n + suc m)))
                             (gradedComm'-elimCase (suc k) n (suc m)
                               (cong predℕ term) (evenOrOdd (suc n)) q a (merid b j) i1) i
              ; (l = i1) → Kn→ΩKn+1 _ (gradedComm'-elimCase (suc k) n (suc m) (cong predℕ term)
                                          (evenOrOdd (suc n)) q a (merid b j) (~ r)) i})
               (Kn→ΩKn+1 (suc (suc (n + suc m)))
                 (gradedComm'-elimCase (suc k) n (suc m) (cong predℕ term)
                   (evenOrOdd (suc n)) q a (merid b j) i1) i))

private
  coherence-transp : (n m : ℕ) (p : _) (q : _)
   → -ₖ'-gen (suc n) (suc m) p q
        (subst coHomK (+'-comm (suc m) (suc n)) (0ₖ (suc m +' suc n))) ≡ 0ₖ _
  coherence-transp zero zero p q = refl
  coherence-transp zero (suc m) p q = refl
  coherence-transp (suc n) zero p q = refl
  coherence-transp (suc n) (suc m) p q = refl

gradedComm'-⌣ₖ∙ : (n m : ℕ) (p : _) (q : _) (a : _)
    → ⌣ₖ∙ (suc n) (suc m) a
  ≡ ((λ b → -ₖ'-gen (suc n) (suc m) p q (subst coHomK (+'-comm (suc m) (suc n)) (b ⌣ₖ a)))
    , (cong (-ₖ'-gen (suc n) (suc m) p q)
       (cong (subst coHomK (+'-comm (suc m) (suc n)))
        (0ₖ-⌣ₖ (suc m) (suc n) a))
   ∙ coherence-transp n m p q))
gradedComm'-⌣ₖ∙ n m p q =
  T.elim (λ _ → isOfHLevelPath (3 + n) ((isOfHLevel↑∙ (suc n) m)) _ _)
    λ a → →∙Homogeneous≡ (isHomogeneousKn _) (funExt λ b → funExt⁻ (cong fst (f₁≡f₂ b)) a)
  where
  f₁ : coHomK (suc m) → S₊∙ (suc n) →∙ coHomK-ptd (suc n +' suc m)
  fst (f₁ b) a = _⌣ₖ_ {n = suc n} {m = suc m} ∣ a ∣ₕ b
  snd (f₁ b) = 0ₖ-⌣ₖ (suc n) (suc m) b

  f₂ : coHomK (suc m) → S₊∙ (suc n) →∙ coHomK-ptd (suc n +' suc m)
  fst (f₂ b) a =
    -ₖ'-gen (suc n) (suc m) p q (subst coHomK (+'-comm (suc m) (suc n))
      (_⌣ₖ_ {n = suc m} {m = suc n} b ∣ a ∣ₕ))
  snd (f₂ b) =
    (cong (-ₖ'-gen (suc n) (suc m) p q)
            (cong (subst coHomK (+'-comm (suc m) (suc n)))
             (⌣ₖ-0ₖ (suc m) (suc n) b))
       ∙ coherence-transp n m p q)

  f₁≡f₂ : (b : _) → f₁ b ≡ f₂ b
  f₁≡f₂ =
    T.elim (λ _ → isOfHLevelPath (3 + m)
                    (subst (isOfHLevel (3 + m))
                     (λ i → S₊∙ (suc n) →∙ coHomK-ptd (+'-comm (suc n) (suc m) (~ i)))
                      (isOfHLevel↑∙' (suc m) n)) _ _)
     λ b → →∙Homogeneous≡ (isHomogeneousKn _)
             (funExt λ a → gradedComm'-elimCase (n + m) n m refl p q a b)

-- Finally, graded commutativity:
gradedComm'-⌣ₖ : (n m : ℕ) (a : coHomK n) (b : coHomK m)
  → a ⌣ₖ b ≡ (-ₖ'^ n · m) (subst coHomK (+'-comm m n) (b ⌣ₖ a))
gradedComm'-⌣ₖ zero zero a b = sym (transportRefl _) ∙ cong (transport refl) (comm-·₀ a b)
gradedComm'-⌣ₖ zero (suc m) a b =
      sym (transportRefl _)
  ∙∙ (λ k → subst coHomK (isSetℕ _ _ refl (+'-comm (suc m) zero) k) (b ⌣ₖ a))
  ∙∙ sym (-ₖ'-gen-inl-left zero (suc m) tt (evenOrOdd (suc m))
          (subst coHomK (+'-comm (suc m) zero) (b ⌣ₖ a)))
gradedComm'-⌣ₖ (suc n) zero a b =
     sym (transportRefl _)
  ∙∙ ((λ k → subst coHomK (isSetℕ _ _ refl (+'-comm zero (suc n)) k) (b ⌣ₖ a)))
  ∙∙ sym (-ₖ'-gen-inl-right (suc n) zero (evenOrOdd (suc n)) tt
          (subst coHomK (+'-comm zero (suc n)) (b ⌣ₖ a)))
gradedComm'-⌣ₖ (suc n) (suc m) a b =
  funExt⁻ (cong fst (gradedComm'-⌣ₖ∙ n m (evenOrOdd (suc n)) (evenOrOdd (suc m)) a)) b

gradedComm'-⌣ : {A : Type ℓ} (n m : ℕ) (a : coHom n A) (b : coHom m A)
  → a ⌣ b ≡ (-ₕ'^ n · m) (subst (λ n → coHom n A) (+'-comm m n) (b ⌣ a))
gradedComm'-⌣ n m =
  ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
    λ f g →
      cong ∣_∣₂ (funExt (λ x →
        gradedComm'-⌣ₖ n m (f x) (g x)
      ∙ cong ((-ₖ'^ n · m) ∘ (subst coHomK (+'-comm m n)))
         λ i → g (transportRefl x (~ i)) ⌣ₖ f (transportRefl x (~ i))))

-----------------------------------------------------------------------------
-- The previous code introduces another - to facilitate proof
-- This a reformulation with the usual -ₕ' definition (the one of the ring) of the results

-ₕ^-gen : {k : ℕ} → {A : Type ℓ} → (n m : ℕ)
         → (p : isEvenT n ⊎ isOddT n)
         → (q : isEvenT m ⊎ isOddT m)
         → (a : coHom k A) → coHom k A
-ₕ^-gen n m (inl p) q a       = a
-ₕ^-gen n m (inr p) (inl q) a = a
-ₕ^-gen n m (inr p) (inr q) a = -ₕ a

-ₕ^_·_ : {k : ℕ} → {A : Type ℓ} → (n m : ℕ) → (a : coHom k A) → coHom k A
-ₕ^_·_ n m a = -ₕ^-gen n m (evenOrOdd n) (evenOrOdd m) a

-ₕ^-gen-eq : ∀ {ℓ} {k : ℕ} {A : Type ℓ} (n m : ℕ)
  → (p : isEvenT n ⊎ isOddT n) (q : isEvenT m ⊎ isOddT m)
  → (x : coHom k A)
  → -ₕ^-gen n m p q x  ≡ (ST.map λ f x → (-ₖ'-gen n m p q) (f x)) x
-ₕ^-gen-eq {k = k} n m (inl p) q = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (funExt λ x → sym (-ₖ'-gen-inl-left n m p q (f x)))
-ₕ^-gen-eq {k = k} n m (inr p) (inl q) = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (funExt λ z → sym (-ₖ'-gen-inl-right n m (inr p) q (f z)))
-ₕ^-gen-eq {k = k} n m (inr p) (inr q) = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (funExt λ z → sym (-ₖ'-gen-inr≡-ₖ' n m p q (f z)))

-ₕ^-eq : ∀ {ℓ} {k : ℕ} {A : Type ℓ} (n m : ℕ) → (a : coHom k A)
             → (-ₕ^ n · m) a  ≡ (-ₕ'^ n · m) a
-ₕ^-eq n m a = -ₕ^-gen-eq n m (evenOrOdd n) (evenOrOdd m) a

gradedComm-⌣ : ∀ {ℓ} {A : Type ℓ} (n m : ℕ) (a : coHom n A) (b : coHom m A)
  → a ⌣ b ≡ (-ₕ^ n · m) (subst (λ n → coHom n A) (+'-comm m n) (b ⌣ a))
gradedComm-⌣ n m a b = (gradedComm'-⌣ n m a b) ∙ (sym (-ₕ^-eq n m (subst (λ n₁ → coHom n₁ _) (+'-comm m n) (b ⌣ a))))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Divisibility
------------------------------------------------------------------------

module Data.Nat.Divisibility where

open import Data.Nat as Nat
open import Data.Nat.DivMod
import Data.Nat.Properties as NatProp
open import Data.Fin as Fin using (Fin; zero; suc)
import Data.Fin.Properties as FP
open NatProp.SemiringSolver
open import Algebra
private
  module CS = CommutativeSemiring NatProp.commutativeSemiring
open import Data.Product
open import Relation.Nullary
open import Relation.Binary
import Relation.Binary.PartialOrderReasoning as PartialOrderReasoning
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym; cong; subst)
open import Function

-- m ∣ n is inhabited iff m divides n. Some sources, like Hardy and
-- Wright's "An Introduction to the Theory of Numbers", require m to
-- be non-zero. However, some things become a bit nicer if m is
-- allowed to be zero. For instance, _∣_ becomes a partial order, and
-- the gcd of 0 and 0 becomes defined.

infix 4 _∣_

data _∣_ : ℕ → ℕ → Set where
  divides : {m n : ℕ} (q : ℕ) (eq : n ≡ q * m) → m ∣ n

-- Extracts the quotient.

quotient : ∀ {m n} → m ∣ n → ℕ
quotient (divides q _) = q

-- If m divides n, and n is positive, then m ≤ n.

∣⇒≤ : ∀ {m n} → m ∣ suc n → m ≤ suc n
∣⇒≤         (divides zero    ())
∣⇒≤ {m} {n} (divides (suc q) eq) = begin
  m          ≤⟨ NatProp.m≤m+n m (q * m) ⟩
  suc q * m  ≡⟨ sym eq ⟩
  suc n      ∎
  where open ≤-Reasoning

-- _∣_ is a partial order.

poset : Poset _ _ _
poset = record
  { Carrier        = ℕ
  ; _≈_            = _≡_
  ; _≤_            = _∣_
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = PropEq.isEquivalence
      ; reflexive     = reflexive
      ; trans         = trans
      }
    ; antisym = antisym
    }
  }
  where
  module DTO = DecTotalOrder Nat.decTotalOrder
  open PropEq.≡-Reasoning

  reflexive : _≡_ ⇒ _∣_
  reflexive {n} refl = divides 1 (sym $ proj₁ CS.*-identity n)

  antisym : Antisymmetric _≡_ _∣_
  antisym (divides {n = zero} q₁ eq₁) (divides {n = n₂} q₂ eq₂) = begin
    n₂      ≡⟨ eq₂ ⟩
    q₂ * 0  ≡⟨ CS.*-comm q₂ 0 ⟩
    0       ∎
  antisym (divides {n = n₁} q₁ eq₁) (divides {n = zero} q₂ eq₂) = begin
    0       ≡⟨ CS.*-comm 0 q₁ ⟩
    q₁ * 0  ≡⟨ sym eq₁ ⟩
    n₁      ∎
  antisym (divides {n = suc n₁} q₁ eq₁) (divides {n = suc n₂} q₂ eq₂) =
    DTO.antisym (∣⇒≤ (divides q₁ eq₁)) (∣⇒≤ (divides q₂ eq₂))

  trans : Transitive _∣_
  trans (divides q₁ refl) (divides q₂ refl) =
    divides (q₂ * q₁) (sym (CS.*-assoc q₂ q₁ _))

module ∣-Reasoning = PartialOrderReasoning poset
  renaming (_≤⟨_⟩_ to _∣⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_)

private module P = Poset poset

-- 1 divides everything.

1∣_ : ∀ n → 1 ∣ n
1∣ n = divides n (sym $ proj₂ CS.*-identity n)

-- Everything divides 0.

_∣0 : ∀ n → n ∣ 0
n ∣0 = divides 0 refl

-- 0 only divides 0.

0∣⇒≡0 : ∀ {n} → 0 ∣ n → n ≡ 0
0∣⇒≡0 {n} 0∣n = P.antisym (n ∣0) 0∣n

-- Only 1 divides 1.

∣1⇒≡1 : ∀ {n} → n ∣ 1 → n ≡ 1
∣1⇒≡1 {n} n∣1 = P.antisym n∣1 (1∣ n)

-- If i divides m and n, then i divides their sum.

∣-+ : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m + n
∣-+ (divides {m = i} q refl) (divides q' refl) =
  divides (q + q') (sym $ proj₂ CS.distrib i q q')

-- If i divides m and n, then i divides their difference.

∣-∸ : ∀ {i m n} → i ∣ m + n → i ∣ m → i ∣ n
∣-∸ (divides {m = i} q' eq) (divides q refl) =
  divides (q' ∸ q)
          (sym $ NatProp.im≡jm+n⇒[i∸j]m≡n q' q i _ $ sym eq)

-- A simple lemma: n divides kn.

∣-* : ∀ k {n} → n ∣ k * n
∣-* k = divides k refl

-- If i divides j, then ki divides kj.

*-cong : ∀ {i j} k → i ∣ j → k * i ∣ k * j
*-cong {i} {j} k (divides q eq) = divides q lemma
  where
  open PropEq.≡-Reasoning
  lemma = begin
    k * j        ≡⟨ cong (_*_ k) eq ⟩
    k * (q * i)  ≡⟨ solve 3 (λ k q i → k :* (q :* i)
                                   :=  q :* (k :* i))
                            refl k q i ⟩
    q * (k * i)  ∎

-- If ki divides kj, and k is positive, then i divides j.

/-cong : ∀ {i j} k → suc k * i ∣ suc k * j → i ∣ j
/-cong {i} {j} k (divides q eq) = divides q lemma
  where
  open PropEq.≡-Reasoning
  k′    = suc k
  lemma = NatProp.cancel-*-right j (q * i) (begin
    j * k′        ≡⟨ CS.*-comm j k′ ⟩
    k′ * j        ≡⟨ eq ⟩
    q * (k′ * i)  ≡⟨ solve 3 (λ q k i → q :* (k :* i)
                                    :=  q :* i :* k)
                             refl q k′ i ⟩
    q * i * k′    ∎)

-- If the remainder after division is non-zero, then the divisor does
-- not divide the dividend.

nonZeroDivisor-lemma
  : ∀ m q (r : Fin (1 + m)) → Fin.toℕ r ≢ 0 →
    ¬ (1 + m) ∣ (Fin.toℕ r + q * (1 + m))
nonZeroDivisor-lemma m zero r r≢zero (divides zero eq) = r≢zero $ begin
  Fin.toℕ r
    ≡⟨ sym $ proj₁ CS.*-identity (Fin.toℕ r) ⟩
  1 * Fin.toℕ r
    ≡⟨ eq ⟩
  0
    ∎
  where open PropEq.≡-Reasoning
nonZeroDivisor-lemma m zero r r≢zero (divides (suc q) eq) =
  NatProp.¬i+1+j≤i m $ begin
    m + suc (q * suc m)
      ≡⟨ solve 2 (λ m q → m :+ (con 1 :+ q)  :=  con 1 :+ m :+ q)
                 refl m (q * suc m) ⟩
    suc (m + q * suc m)
      ≡⟨ sym eq ⟩
    1 * Fin.toℕ r
      ≡⟨ proj₁ CS.*-identity (Fin.toℕ r) ⟩
    Fin.toℕ r
      ≤⟨ ≤-pred $ FP.bounded r ⟩
    m
      ∎
  where open ≤-Reasoning
nonZeroDivisor-lemma m (suc q) r r≢zero d =
  nonZeroDivisor-lemma m q r r≢zero (∣-∸ d' P.refl)
  where
  lem = solve 3 (λ m r q → r :+ (m :+ q)  :=  m :+ (r :+ q))
                refl (suc m) (Fin.toℕ r) (q * suc m)
  d' = subst (λ x → (1 + m) ∣ x) lem d

-- Divisibility is decidable.

_∣?_ : Decidable _∣_
zero  ∣? zero                         = yes (0 ∣0)
zero  ∣? suc n                        = no ((λ ()) ∘′ 0∣⇒≡0)
suc m ∣? n                            with n divMod suc m
suc m ∣? .(q * suc m)                 | result q zero    refl =
  yes $ divides q refl
suc m ∣? .(1 + Fin.toℕ r + q * suc m) | result q (suc r) refl =
  no $ nonZeroDivisor-lemma m q (suc r) (λ())

ext: agda


text:
------------------------------------------------------------------------
-- An alternative (non-standard) classical definition of weak
-- bisimilarity
------------------------------------------------------------------------

-- This definition is based on the function "wb" in Section 6.5.1 of
-- Pous and Sangiorgi's "Enhancements of the bisimulation proof
-- method".

{-# OPTIONS --sized-types #-}

open import Labelled-transition-system

module Bisimilarity.Weak.Alternative.Classical {ℓ} (lts : LTS ℓ) where

open import Prelude

import Bisimilarity.Classical

open LTS lts

-- We get weak bisimilarity by instantiating strong bisimilarity with
-- a different LTS.

private
  module WB = Bisimilarity.Classical (weak lts)

open WB public
  using (⟪_,_⟫)
  renaming ( Bisimulation  to Weak-bisimulation
           ; Bisimilarity′ to Weak-bisimilarity′
           ; Bisimilarity  to Weak-bisimilarity
           ; _∼_           to _≈_
           )

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
------------------------------------------------------------------------------
-- Properties related with the group commutator
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module GroupTheory.Commutator.PropertiesATP where

open import GroupTheory.Base
open import GroupTheory.Commutator

------------------------------------------------------------------------------

-- From: A. G. Kurosh. The Theory of Groups, vol. 1. Chelsea Publising
-- Company, 2nd edition, 1960. p. 99.
postulate commutatorInverse : ∀ a b → [ a , b ] · [ b , a ] ≡ ε
{-# ATP prove commutatorInverse #-}

-- If the commutator is associative, then commutator of any two
-- elements lies in the center of the group, i.e. a [b,c] = [b,c] a.
-- From: TPTP 6.4.0 problem GRP/GRP024-5.p.
postulate commutatorAssocCenter : (∀ a b c → commutatorAssoc a b c) →
                                  (∀ a b c → a · [ b , c ] ≡ [ b , c ] · a)
{-# ATP prove commutatorAssocCenter #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- 2014-01-01 Andreas, test case constructed by Christian Sattler

{-# OPTIONS --allow-unsolved-metas #-}

-- unguarded recursive record
record R : Set where
  constructor cons
  field
    r : R

postulate F : (R → Set) → Set

q : (∀ P → F P) → (∀ P → F P)
q h P = h (λ {(cons x) → {!!}})

-- ISSUE WAS: Bug in implementation of eta-expansion of projected var,
-- leading to loop in Agda.

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of format strings and printf
------------------------------------------------------------------------

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

module README.Text.Printf where

open import Data.Nat.Base
open import Data.Char.Base
open import Data.List.Base
open import Data.String.Base
open import Data.Sum.Base

open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Format strings

open import Text.Format

-- We can specify a format by writing a string which will get interpreted
-- by a lexer into a list of formatting directives.

-- The specification types are always started with a '%' character:

-- Integers (%d or %i)
-- Naturals (%u)
-- Floats   (%f)
-- Chars    (%c)
-- Strings  (%s)

-- Anything which is not a type specification is a raw string to be spliced
-- in the output of printf.

-- For instance the following format alternates types and raw strings

_ : lexer "%s: %u + %u ≡ %u"
  ≡ inj₂ (`String ∷ Raw ": " ∷ `ℕ ∷ Raw " + " ∷ `ℕ ∷ Raw " ≡ " ∷ `ℕ ∷ [])
_ = refl

-- Lexing can fail. There are two possible errors:

-- If we start a specification type with a '%' but the string ends then
-- we get an UnexpectedEndOfString error

_ : lexer "%s: %u + %u ≡ %"
  ≡ inj₁ (UnexpectedEndOfString "%s: %u + %u ≡ %")
_ = refl

-- If we start a specification type with a '%' and the following character
-- does not correspond to an existing type, we get an InvalidType error
-- together with a focus highlighting the position of the problematic type.

_ : lexer "%s: %u + %a ≡ %u"
  ≡ inj₁ (InvalidType "%s: %u + %" 'a' " ≡ %u")
_ = refl

------------------------------------------------------------------------
-- Printf

open import Text.Printf

-- printf is a function which takes a format string as an argument and
-- returns a function expecting a value for each type specification present
-- in the format and returns a string splicing in these values into the
-- format string.

-- For instance `printf "%s: %u + %u ≡ %u"` is a
-- `String → ℕ → ℕ → ℕ → String` function.

_ : String → ℕ → ℕ → ℕ → String
_ = printf "%s: %u + %u ≡ %u"

_ : printf "%s: %u + %u ≡ %u" "example" 3 2 5
  ≡ "example: 3 + 2 ≡ 5"
_ = refl

-- If the format string str is invalid then `printf str` will have type
-- `Error e` where `e` is the lexing error.

_ : Text.Printf.Error (UnexpectedEndOfString "%s: %u + %u ≡ %")
_ = printf "%s: %u + %u ≡ %"

_ : Text.Printf.Error (InvalidType "%s: %u + %" 'a' " ≡ %u")
_ = printf "%s: %u + %a ≡ %u"

-- Trying to pass arguments to such an ̀Error` type will lead to a
-- unification error which hopefully makes the problem clear e.g.
-- `printf "%s: %u + %a ≡ %u" "example" 3 2 5` fails with the error:

-- Text.Printf.Error (InvalidType "%s: %u + %" 'a' " ≡ %u") should be
-- a function type, but it isn't
-- when checking that "example" 3 2 5 are valid arguments to a
-- function of type Text.Printf.Printf (lexer "%s: %u + %a ≡ %u")


text:
module Inference-of-implicit-function-space where

postulate
  _⇔_         : Set → Set → Set
  equivalence : {A B : Set} → (A → B) → (B → A) → A ⇔ B
  A           : Set

P : Set
P = {x : A} → A ⇔ A

works : P ⇔ P
works = equivalence (λ r {x} → r {x = x}) (λ r {x} → r {x = x})

works₂ : P ⇔ P
works₂ = equivalence {A = P} (λ r {x} → r {x = x}) (λ r {y} → r {y})

fails : P ⇔ P
fails = equivalence (λ r {x} → r {x = x}) (λ r {y} → r {y})

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Transp {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance as I
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions.Sigma
open import Definition.LogicalRelation.Substitution.Introductions.Fst
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.Lambda
open import Definition.LogicalRelation.Substitution.Introductions.Application
open import Definition.LogicalRelation.Substitution.Introductions.Cast
open import Definition.LogicalRelation.Substitution.Introductions.Id
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.MaybeEmbed
open import Definition.LogicalRelation.Substitution.Escape
open import Definition.LogicalRelation.Substitution.Introductions.Universe
open import Definition.LogicalRelation.Substitution.Reduction
open import Definition.LogicalRelation.Substitution.Weakening
open import Definition.LogicalRelation.Substitution.ProofIrrelevance

open import Tools.Product
import Tools.PropositionalEquality as PE

IdSymᵗᵛ : ∀ {A l t u e Γ}
         ([Γ] : ⊩ᵛ Γ)
         ([U] : Γ ⊩ᵛ⟨ ∞ ⟩ U l ^ [ ! , next l ] / [Γ])
         ([AU] : Γ ⊩ᵛ⟨ ∞ ⟩ A ∷ U l ^ [ ! , next l ] / [Γ] / [U])
         ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ^ [ ! , ι l ] / [Γ])
         ([t] : Γ ⊩ᵛ⟨ ∞ ⟩ t ∷ A ^ [ ! , ι l ] / [Γ] / [A])
         ([u] : Γ ⊩ᵛ⟨ ∞ ⟩ u ∷ A ^ [ ! , ι l ] / [Γ] / [A])
         ([Id] : Γ ⊩ᵛ⟨ ∞ ⟩ Id A t u ^ [ % , ι l ] / [Γ]) →
         ([Idinv] : Γ ⊩ᵛ⟨ ∞ ⟩ Id A u t ^ [ % , ι l ] / [Γ]) →
         ([e] : Γ ⊩ᵛ⟨ ∞ ⟩ e ∷ Id A t u ^ [ % , ι l ] / [Γ] / [Id] ) →
         Γ ⊩ᵛ⟨ ∞ ⟩ Idsym A t u e ∷ Id A u t  ^ [ % , ι l ] / [Γ] / [Idinv]
IdSymᵗᵛ {A} {l} {t} {u} {e} {Γ} [Γ] [U] [AU] [A] [t] [u] [Id] [Idinv] [e] = validityIrr {A = Id A u t} {t = Idsym A t u e} [Γ] [Idinv] λ {Δ} {σ} ⊢Δ [σ] →
  PE.subst (λ X → Δ ⊢ X ∷ subst σ (Id A u t) ^ [ % , ι l ] ) (PE.sym (subst-Idsym σ A t u e))
    (Idsymⱼ {A = subst σ A} {x = subst σ t} {y = subst σ u} (escapeTerm (proj₁ ([U] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([AU] ⊢Δ [σ])))
            (escapeTerm (proj₁ ([A] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ])))
            (escapeTerm (proj₁ ([A] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([u] ⊢Δ [σ])))
            (escapeTerm (proj₁ ([Id] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([e] ⊢Δ [σ]))))

abstract
  transpᵗᵛ : ∀ {A P l t s u e Γ}
           ([Γ] : ⊩ᵛ Γ)
           ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ^ [ ! , l ] / [Γ])
           ([P] : Γ ∙ A ^ [ ! , l ] ⊩ᵛ⟨ ∞ ⟩ P ^ [ % , l ] / (_∙_ {A = A} [Γ] [A]))
           ([t] : Γ ⊩ᵛ⟨ ∞ ⟩ t ∷ A ^ [ ! , l ] / [Γ] / [A])
           ([s] : Γ ⊩ᵛ⟨ ∞ ⟩ s ∷ P [ t ]  ^ [ % , l ] / [Γ] / substS {A} {P} {t} [Γ] [A] [P] [t])
           ([u] : Γ ⊩ᵛ⟨ ∞ ⟩ u ∷ A ^ [ ! , l ] / [Γ] / [A])
           ([Id] : Γ ⊩ᵛ⟨ ∞ ⟩ Id A t u ^ [ % , l ] / [Γ]) →
           ([e] : Γ ⊩ᵛ⟨ ∞ ⟩ e ∷ Id A t u ^ [ % , l ] / [Γ] / [Id] ) →
           Γ ⊩ᵛ⟨ ∞ ⟩ transp A P t s u e ∷ P [ u ]  ^ [ % , l ] / [Γ] / substS {A} {P} {u} [Γ] [A] [P] [u]
  transpᵗᵛ {A} {P} {l} {t} {s} {u} {e} {Γ} [Γ] [A] [P] [t] [s] [u] [Id] [e] =
    validityIrr {A = P [ u ]} {t = transp A P t s u e } [Γ] (substS {A} {P} {u} [Γ] [A] [P] [u]) λ {Δ} {σ} ⊢Δ [σ] →
    let [liftσ] = liftSubstS {F = A} [Γ] ⊢Δ [A] [σ]
        [A]σ = proj₁ ([A] {Δ} {σ} ⊢Δ [σ])
        [P[t]]σ = I.irrelevance′ (singleSubstLift P t) (proj₁ (substS {A} {P} {t} [Γ] [A] [P] [t] {Δ} {σ} ⊢Δ [σ]))
        X = transpⱼ (escape [A]σ) (escape (proj₁ ([P] {Δ ∙ subst σ A ^ [ ! , l ]} {liftSubst σ} (⊢Δ ∙ (escape [A]σ)) [liftσ])))
                            (escapeTerm [A]σ (proj₁ ([t] ⊢Δ [σ]))) (escapeTerm [P[t]]σ (I.irrelevanceTerm′ (singleSubstLift P t) PE.refl PE.refl (proj₁ (substS {A} {P} {t} [Γ] [A] [P] [t] {Δ} {σ} ⊢Δ [σ])) [P[t]]σ (proj₁ ([s] ⊢Δ [σ]))))
                            (escapeTerm [A]σ (proj₁ ([u] ⊢Δ [σ]))) (escapeTerm (proj₁ ([Id] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([e] ⊢Δ [σ])))
    in PE.subst (λ X → Δ ⊢ transp (subst σ A) ( subst (liftSubst σ) P) (subst σ t) (subst σ s) (subst σ u) (subst σ e) ∷ X ^ [ % , l ] ) (PE.sym (singleSubstLift P u)) X

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --sized-types --guardedness #-}

open import Data.Product
open import Data.Vec
open import Codata.Colist as Colist
open import Agda.Builtin.Equality
open import Size
open import Codata.Thunk
open import Data.Fin
open import Data.Nat
open import Data.Maybe
open import Examples.Colists.Auxiliary.Colist_member

open import is-lib.InfSys

module Examples.Colists.member {A : Set} where

  U = A × Colist A ∞

  data memberRN : Set where
    mem-h mem-t : memberRN

  mem-h-r : FinMetaRule U
  mem-h-r .Ctx = A × Thunk (Colist A) ∞
  mem-h-r .comp (x , xs) =
    [] ,
    ----------------
    (x , x ∷ xs)

  mem-t-r : FinMetaRule U
  mem-t-r .Ctx = A × A × Thunk (Colist A) ∞
  mem-t-r .comp (x , y , xs) =
    ((x , xs .force) ∷ []) ,
    ----------------
    (x , y ∷ xs)

  memberIS : IS U
  memberIS .Names = memberRN
  memberIS .rules mem-h = from mem-h-r
  memberIS .rules mem-t = from mem-t-r

  _member_ : A → Colist A ∞ → Set
  x member xs = Ind⟦ memberIS ⟧ (x , xs)

  memSpec : U → Set
  memSpec (x , xs) = Σ[ i ∈ ℕ ] (Colist.lookup i xs ≡ just x)

  memSpecClosed : ISClosed memberIS memSpec
  memSpecClosed mem-h _ _ = zero , refl
  memSpecClosed mem-t _ pr =
    let (i , proof) = pr Fin.zero in
    (suc i) , proof

  memberSound : ∀{x xs} → x member xs → memSpec (x , xs)
  memberSound = ind[ memberIS ] memSpec memSpecClosed

  -- Completeness using memSpec does not terminate
  -- Product implemented as record. Record projections do not decrease
  memSpec' : U → ℕ → Set
  memSpec' (x , xs) i = Colist.lookup i xs ≡ just x

  memberCompl : ∀{x xs i} → memSpec' (x , xs) i → x member xs
  memberCompl {.x} {x ∷ _} {zero} refl = apply-ind mem-h _ λ ()
  memberCompl {x} {y ∷ xs} {suc i} eq = apply-ind mem-t _ λ{zero → memberCompl eq}

  memberComplete : ∀{x xs} → memSpec (x , xs) → x member xs
  memberComplete (i , eq) = memberCompl eq

  {- Correctness wrt to Agda DataType -}

  ∈-sound : ∀{x xs} → x ∈ xs → x member xs
  ∈-sound here = apply-ind mem-h _ λ ()
  ∈-sound (there mem) = apply-ind mem-t _ λ{zero → ∈-sound mem}

  ∈-complete : ∀{x xs} → x member xs → x ∈ xs
  ∈-complete (fold (mem-h , _ , refl , _)) = here
  ∈-complete (fold (mem-t , _ , refl , prem)) = there (∈-complete (prem zero))

max_stars_repo_name: LcicC/inference-systems-agda

max_issues_repo_name: LcicC/inference-systems-agda

max_forks_repo_name: LcicC/inference-systems-agda


text:
{-# OPTIONS --cubical-compatible #-}
open import Common.Prelude
open import Common.Equality
open import Common.Product

data _≅_ {A : Set} (a : A) : {B : Set} (b : B) → Set₁ where
  refl : a ≅ a

data D : Bool → Set where
  x  : D true
  y  : D false

P : Set -> Set₁
P S = Σ S (\s → s ≅ x)

pbool : P (D true)
pbool = _ , refl

¬pfin : P (D false) → ⊥
¬pfin (y , ())


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

open import Categories.Category.Monoidal.Bundle
  using (SymmetricMonoidalCategory)

module Categories.Category.Construction.SymmetricMonoidalFunctors
  {o ℓ e o′ ℓ′ e′}
  (C : SymmetricMonoidalCategory o ℓ e)
  (D : SymmetricMonoidalCategory o′ ℓ′ e′) where

-- The symmetric monoidal category [C , D] of symmetric monoidal
-- functors between the symmetric monoidal categories C and D.

open import Level
open import Data.Product using (_,_; uncurry′)

open import Categories.Category using (Category)
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Braided using (Braided)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
import Categories.Functor.Monoidal.Symmetric as SMF
import Categories.Functor.Monoidal.PointwiseTensor as PT
import Categories.NaturalTransformation.Monoidal.Symmetric as SMNT
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI
open import Categories.Functor.Bifunctor using (Bifunctor)

import Categories.Morphism as Morphism
open SymmetricMonoidalCategory D

module Lax where
  open SMF.Lax
  open SMNT.Lax renaming (id to idNT)

  -- The category of symmetric monoidal functors.

  MonoidalFunctorsU : Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′)
                               (o ⊔ e′)
  MonoidalFunctorsU = record
    { Obj = SymmetricMonoidalFunctor C D
    ; _⇒_ = SymmetricMonoidalNaturalTransformation
    ; _≈_ = λ α β → ∀ {X} → η α X ≈ η β X
    ; id  = idNT
    ; _∘_ = _∘ᵥ_
    ; assoc     = assoc
    ; sym-assoc = sym-assoc
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    ; identity² = identity²
    ; equiv     = record
      { refl  = Equiv.refl
      ; sym   = λ α≈β → Equiv.sym α≈β
      ; trans = λ α≈β β≈γ → Equiv.trans α≈β β≈γ
      }
    ; ∘-resp-≈ = λ α₁≈β₁ α₂≈β₂ → ∘-resp-≈ α₁≈β₁ α₂≈β₂
    }
    where open SymmetricMonoidalNaturalTransformation using (η)

  open SMNI.Lax using (_≃_)
  open Morphism MonoidalFunctorsU using (_≅_)

  -- Symmetric natural isos are isos in the functor category.

  ≃⇒≅ : ∀ {F G : SymmetricMonoidalFunctor C D} → F ≃ G → F ≅ G
  ≃⇒≅ ni = record
    { from = ni.F⇒G-monoidal
    ; to   = ni.F⇐G-monoidal
    ; iso  = record
      { isoˡ = λ {X} → ni.iso.isoˡ X
      ; isoʳ = λ {X} → ni.iso.isoʳ X
      }
    }
    where module ni = SMNI.Lax.SymmetricMonoidalNaturalIsomorphism ni

  open PT.Lax

  MonoidalFunctorsU-monoidal : Monoidal MonoidalFunctorsU
  MonoidalFunctorsU-monoidal = monoidalHelper MonoidalFunctorsU (record
    { ⊗ = record
      { F₀            = uncurry′ _⊗̇₀_
      ; F₁            = uncurry′ _⊗̇₁_
      ; identity      = ⊗.identity
      ; homomorphism  = ⊗.homomorphism
      ; F-resp-≈      = λ{ (eq₁ , eq₂) → ⊗.F-resp-≈ (eq₁ , eq₂) }
      }
    ; unit            = unitF
    ; unitorˡ         = λ {F} → ≃⇒≅ (⊗̇-unitorˡ {F = F})
    ; unitorʳ         = λ {F} → ≃⇒≅ (⊗̇-unitorʳ {F = F})
    ; associator      = λ {F G H} → record
      -- NOTE: this is clearly the same as
      --
      --   ≃⇒≅ (⊗̇-associator {F = F} {G} {H})
      --
      -- but the manual expansion seems necessary for Agda to finish
      -- typechecking it.
      { from          = record
        { U           = ⊗̇-associator.F⇒G {F = F} {G} {H}
        ; isMonoidal  = record
          { ε-compat      = ⊗̇-associator.ε-compat {F = F} {G} {H}
          ; ⊗-homo-compat = ⊗̇-associator.⊗-homo-compat {F = F} {G} {H}
          }
        }
      ; to            = record
        { U           = ⊗̇-associator.F⇐G {F = F} {G} {H}
        ; isMonoidal  = record
          { ε-compat      = ⊗̇-associator.⇐.ε-compat {F = F} {G} {H}
          ; ⊗-homo-compat = ⊗̇-associator.⇐.⊗-homo-compat {F = F} {G} {H}
          }
        }
      ; iso           = record
        { isoˡ        = associator.isoˡ
        ; isoʳ        = associator.isoʳ
        }
      }
    ; unitorˡ-commute = unitorˡ-commute-from
    ; unitorʳ-commute = unitorʳ-commute-from
    ; assoc-commute   = assoc-commute-from
    ; triangle        = triangle
    ; pentagon        = pentagon
    })

  MonoidalFunctorsU-braided : Braided MonoidalFunctorsU-monoidal
  MonoidalFunctorsU-braided = record
    { braiding            = niHelper (record
      { η                 = λ{ (F , G) → record
        { U               = ⊗̇-braiding.F⇒G {F = F} {G}
        ; isMonoidal      = record
          { ε-compat      = ⊗̇-braiding.ε-compat {F = F} {G}
          ; ⊗-homo-compat = ⊗̇-braiding.⊗-homo-compat {F = F} {G}
          }
        } }
      ; η⁻¹               = λ{ (F , G) → record
        { U               = ⊗̇-braiding.F⇐G {F = F} {G}
        ; isMonoidal      = record
          { ε-compat      = ⊗̇-braiding.⇐.ε-compat {F = F} {G}
          ; ⊗-homo-compat = ⊗̇-braiding.⇐.⊗-homo-compat {F = F} {G}
          }
        } }
      ; commute = λ{ (β , γ) {X} →
                     let module β = SymmetricMonoidalNaturalTransformation β
                         module γ = SymmetricMonoidalNaturalTransformation γ
                     in braiding.⇒.commute (β.η X , γ.η X) }
      ; iso     = λ _ → record
        { isoˡ  = braiding.iso.isoˡ _
        ; isoʳ  = braiding.iso.isoʳ _ }
      })
    ; hexagon₁  = hexagon₁
    ; hexagon₂  = hexagon₂
    }

  MonoidalFunctorsU-symmetric : Symmetric MonoidalFunctorsU-monoidal
  MonoidalFunctorsU-symmetric = record
    { braided     = MonoidalFunctorsU-braided
    ; commutative = commutative
    }

  MonoidalFunctors : SymmetricMonoidalCategory (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′)
                                               (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
  MonoidalFunctors = record
    { U         = MonoidalFunctorsU
    ; monoidal  = MonoidalFunctorsU-monoidal
    ; symmetric = MonoidalFunctorsU-symmetric
    }

module Strong where
  open SMF.Strong
  open SMNT.Strong renaming (id to idNT)

  -- The category of symmetric monoidal functors.

  MonoidalFunctorsU : Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′)
                               (o ⊔ e′)
  MonoidalFunctorsU = record
    { Obj = SymmetricMonoidalFunctor C D
    ; _⇒_ = SymmetricMonoidalNaturalTransformation
    ; _≈_ = λ α β → ∀ {X} → η α X ≈ η β X
    ; id  = idNT
    ; _∘_ = _∘ᵥ_
    ; assoc     = assoc
    ; sym-assoc = sym-assoc
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    ; identity² = identity²
    ; equiv     = record
      { refl  = Equiv.refl
      ; sym   = λ α≈β → Equiv.sym α≈β
      ; trans = λ α≈β β≈γ → Equiv.trans α≈β β≈γ
      }
    ; ∘-resp-≈ = λ α₁≈β₁ α₂≈β₂ → ∘-resp-≈ α₁≈β₁ α₂≈β₂
    }
    where open SymmetricMonoidalNaturalTransformation using (η)

  open SMNI.Strong using (_≃_)
  open Morphism MonoidalFunctorsU using (_≅_)

  -- Symmetric natural isos are isos in the functor category.

  ≃⇒≅ : ∀ {F G : SymmetricMonoidalFunctor C D} → F ≃ G → F ≅ G
  ≃⇒≅ ni = record
    { from = ni.F⇒G-monoidal
    ; to   = ni.F⇐G-monoidal
    ; iso  = record
      { isoˡ = λ {X} → ni.iso.isoˡ X
      ; isoʳ = λ {X} → ni.iso.isoʳ X
      }
    }
    where module ni = SMNI.Strong.SymmetricMonoidalNaturalIsomorphism ni

  open PT.Strong

  MonoidalFunctorsU-monoidal : Monoidal MonoidalFunctorsU
  MonoidalFunctorsU-monoidal = monoidalHelper MonoidalFunctorsU (record
    { ⊗ = record
      { F₀            = uncurry′ _⊗̇₀_
      ; F₁            = uncurry′ _⊗̇₁_
      ; identity      = ⊗.identity
      ; homomorphism  = ⊗.homomorphism
      ; F-resp-≈      = λ{ (eq₁ , eq₂) → ⊗.F-resp-≈ (eq₁ , eq₂) }
      }
    ; unit            = unitF
    ; unitorˡ         = λ {F} → ≃⇒≅ (⊗̇-unitorˡ {F = F})
    ; unitorʳ         = λ {F} → ≃⇒≅ (⊗̇-unitorʳ {F = F})
    ; associator      = λ {F G H} → record
      -- NOTE: this is clearly the same as
      --
      --   ≃⇒≅ (⊗̇-associator {F = F} {G} {H})
      --
      -- but the manual expansion seems necessary for Agda to finish
      -- typechecking it.
      { from          = record
        { U           = ⊗̇-associator.F⇒G {F = F} {G} {H}
        ; isMonoidal  = record
          { ε-compat      = ⊗̇-associator.ε-compat {F = F} {G} {H}
          ; ⊗-homo-compat = ⊗̇-associator.⊗-homo-compat {F = F} {G} {H}
          }
        }
      ; to            = record
        { U           = ⊗̇-associator.F⇐G {F = F} {G} {H}
        ; isMonoidal  = record
          { ε-compat      = ⊗̇-associator.⇐.ε-compat {F = F} {G} {H}
          ; ⊗-homo-compat = ⊗̇-associator.⇐.⊗-homo-compat {F = F} {G} {H}
          }
        }
      ; iso           = record
        { isoˡ        = associator.isoˡ
        ; isoʳ        = associator.isoʳ
        }
      }
    ; unitorˡ-commute = unitorˡ-commute-from
    ; unitorʳ-commute = unitorʳ-commute-from
    ; assoc-commute   = assoc-commute-from
    ; triangle        = triangle
    ; pentagon        = pentagon
    })

  MonoidalFunctorsU-braided : Braided MonoidalFunctorsU-monoidal
  MonoidalFunctorsU-braided = record
    { braiding            = niHelper (record
      { η                 = λ{ (F , G) → record
        { U               = ⊗̇-braiding.F⇒G {F = F} {G}
        ; isMonoidal      = record
          { ε-compat      = ⊗̇-braiding.ε-compat {F = F} {G}
          ; ⊗-homo-compat = ⊗̇-braiding.⊗-homo-compat {F = F} {G}
          }
        } }
      ; η⁻¹               = λ{ (F , G) → record
        { U               = ⊗̇-braiding.F⇐G {F = F} {G}
        ; isMonoidal      = record
          { ε-compat      = ⊗̇-braiding.⇐.ε-compat {F = F} {G}
          ; ⊗-homo-compat = ⊗̇-braiding.⇐.⊗-homo-compat {F = F} {G}
          }
        } }
      ; commute = λ{ (β , γ) {X} →
                     let module β = SymmetricMonoidalNaturalTransformation β
                         module γ = SymmetricMonoidalNaturalTransformation γ
                     in braiding.⇒.commute (β.η X , γ.η X) }
      ; iso     = λ _ → record
        { isoˡ  = braiding.iso.isoˡ _
        ; isoʳ  = braiding.iso.isoʳ _ }
      })
    ; hexagon₁  = hexagon₁
    ; hexagon₂  = hexagon₂
    }

  MonoidalFunctorsU-symmetric : Symmetric MonoidalFunctorsU-monoidal
  MonoidalFunctorsU-symmetric = record
    { braided     = MonoidalFunctorsU-braided
    ; commutative = commutative
    }

  MonoidalFunctors : SymmetricMonoidalCategory (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′)
                                               (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
  MonoidalFunctors = record
    { U         = MonoidalFunctorsU
    ; monoidal  = MonoidalFunctorsU-monoidal
    ; symmetric = MonoidalFunctorsU-symmetric
    }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-

This file contains:

- An implementation of the free group of a type of generators as a HIT

-}
{-# OPTIONS --safe #-}

module Cubical.HITs.FreeGroup.Base where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level

data FreeGroup (A : Type ℓ) : Type ℓ where
  η     : A → FreeGroup A
  _·_   : FreeGroup A → FreeGroup A → FreeGroup A
  ε     : FreeGroup A
  inv   : FreeGroup A → FreeGroup A
  assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z
  idr   : ∀ x → x ≡ x · ε
  idl   : ∀ x → x ≡ ε · x
  invr  : ∀ x → x · (inv x) ≡ ε
  invl  : ∀ x → (inv x) · x ≡ ε
  trunc : isSet (FreeGroup A)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical