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

open import HoTT
open import homotopy.SuspSmash

module homotopy.SuspSmashComm where

module Σ∧Σ-PathElim
  {i} {j} {k} {A : Type i} {B : Type j} {C : Type k}
  (f g : ⊙Susp A ∧ ⊙Susp B → C)
  (n-n : f (smin north north) == g (smin north north))
  (n-s : f (smin north south) == g (smin north south))
  (s-n : f (smin south north) == g (smin south north))
  (s-s : f (smin south south) == g (smin south south))
  (n-m : ∀ b → Square n-n (ap (λ sb → f (smin north sb)) (merid b))
                          (ap (λ sb → g (smin north sb)) (merid b)) n-s)
  (s-m : ∀ b → Square s-n (ap (λ sb → f (smin south sb)) (merid b))
                          (ap (λ sb → g (smin south sb)) (merid b)) s-s)
  (m-n : ∀ a → Square n-n (ap (λ sa → f (smin sa north)) (merid a))
                          (ap (λ sa → g (smin sa north)) (merid a)) s-n)
  (m-s : ∀ a → Square n-s (ap (λ sa → f (smin sa south)) (merid a))
                          (ap (λ sa → g (smin sa south)) (merid a)) s-s)
  (m-m : ∀ a b →
    Cube (m-n a)
         (m-s a)
         (n-m b)
         (natural-square (λ sb → ap (λ sa → f (smin sa sb)) (merid a)) (merid b))
         (natural-square (λ sb → ap (λ sa → g (smin sa sb)) (merid a)) (merid b))
         (s-m b))
  (basel : f smbasel == g smbasel)
  (baser : f smbaser == g smbaser)
  (gluel-north : Square n-n (ap f (smgluel north)) (ap g (smgluel north)) basel)
  (gluel-south : Square s-n (ap f (smgluel south)) (ap g (smgluel south)) basel)
  (gluel-merid : ∀ a →
    Cube gluel-north
         gluel-south
         (m-n a)
         (natural-square (λ sa → ap f (smgluel sa)) (merid a))
         (natural-square (λ sa → ap g (smgluel sa)) (merid a))
         (natural-square (λ sa → basel) (merid a)))
  (gluer-north : Square n-n (ap f (smgluer north)) (ap g (smgluer north)) baser)
  (gluer-south : Square n-s (ap f (smgluer south)) (ap g (smgluer south)) baser)
  (gluer-merid : ∀ b →
    Cube gluer-north
         gluer-south
         (n-m b)
         (natural-square (λ a → ap f (smgluer a)) (merid b))
         (natural-square (λ a → ap g (smgluer a)) (merid b))
         (natural-square (λ a → baser) (merid b))
  )
  where

  private
    module M =
      SuspDoublePathElim
        (λ sa sb → f (smin sa sb))
        (λ sa sb → g (smin sa sb))
        n-n n-s s-n s-s n-m s-m m-n m-s m-m
    module P =
      SmashElim
        {P = λ sa∧sb → f sa∧sb == g sa∧sb}
        M.p
        basel
        baser
        (λ sa → ↓-='-from-square $
          Susp-elim
            {P = λ sa → Square (M.p sa north) (ap f (smgluel sa)) (ap g (smgluel sa)) basel}
            gluel-north
            gluel-south
            (λ a → cube-to-↓-square $
                   cube-shift-back (! (M.merid-north-square-β a)) $
                   gluel-merid a)
            sa)
        (λ sb → ↓-='-from-square $
          Susp-elim
            {P = λ sb → Square (M.p north sb) (ap f (smgluer sb)) (ap g (smgluer sb)) baser}
            gluer-north
            gluer-south
            (λ b → cube-to-↓-square $
                   cube-shift-back (! (M.north-merid-square-β b)) $
                   gluer-merid b)
            sb)

  open P using (f) public

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  private
    f : ⊙Susp (de⊙ X) ∧ ⊙Susp (de⊙ Y) → Susp (Susp (X ∧ Y))
    f = Susp-fmap (∧Σ-out X Y) ∘ Σ∧-out X (⊙Susp (de⊙ Y))

    g : ⊙Susp (de⊙ X) ∧ ⊙Susp (de⊙ Y) → Susp (Susp (X ∧ Y))
    g = Susp-flip ∘ Susp-fmap (Σ∧-out X Y) ∘ ∧Σ-out (⊙Susp (de⊙ X)) Y

    f-merid-x : ∀ x sy →
      ap (λ sx → f (smin sx sy)) (merid x)
      =-=
      merid (Susp-fmap (smin x) sy)
    f-merid-x x sy =
      ap (Susp-fmap (∧Σ-out X Y) ∘ Susp-fmap (λ x' → smin x' sy)) (merid x)
        =⟪ ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' sy)) (merid x) ⟫
      ap (Susp-fmap (∧Σ-out X Y)) (ap (Susp-fmap (λ x' → smin x' sy)) (merid x))
        =⟪ ap (ap (Susp-fmap (∧Σ-out X Y)))
              (SuspFmap.merid-β (λ x' → smin x' sy) x) ⟫
      ap (Susp-fmap (∧Σ-out X Y)) (merid (smin x sy))
        =⟪ SuspFmap.merid-β (∧Σ-out X Y) (smin x sy) ⟫
      merid (Susp-fmap (smin x) sy) ∎∎

    g-merid-y : ∀ sx y →
      ap (g ∘ smin sx) (merid y)
      =-=
      ! (merid (Susp-fmap (λ x' → smin x' y) sx))
    g-merid-y sx y =
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y) ∘ Susp-fmap (smin sx)) (merid y)
        =⟪ ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin sx)) (merid y) ⟫
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (ap (Susp-fmap (smin sx)) (merid y))
        =⟪ ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
              (SuspFmap.merid-β (smin sx) y) ⟫
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin sx y))
        =⟪ ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) (merid (smin sx y)) ⟫
      ap Susp-flip (ap (Susp-fmap (Σ∧-out X Y)) (merid (smin sx y)))
        =⟪ ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) (smin sx y)) ⟫
      ap Susp-flip (merid (Susp-fmap (λ x' → smin x' y) sx))
        =⟪ SuspFlip.merid-β (Susp-fmap (λ x' → smin x' y) sx) ⟫
      ! (merid (Susp-fmap (λ x' → smin x' y) sx)) ∎∎

    n-n : f (smin north north) == g (smin north north)
    n-n = merid north

    n-s : f (smin north south) == g (smin north south)
    n-s = idp

    s-n : f (smin south north) == g (smin south north)
    s-n = idp

    s-s : f (smin south south) == g (smin south south)
    s-s = ! (merid south)

    n-m : ∀ y → Square n-n (ap (f ∘ smin north) (merid y))
                           (ap (g ∘ smin north) (merid y)) n-s
    n-m y = ap-cst north (merid y) ∙v⊡ (lb-square (merid north) ⊡v∙ ! (↯ (g-merid-y north y)))

    s-m : ∀ y → Square s-n (ap (f ∘ smin south) (merid y))
                           (ap (g ∘ smin south) (merid y)) s-s
    s-m y = ap-cst south (merid y) ∙v⊡ br-square (! (merid south)) ⊡v∙ ! (↯ (g-merid-y south y))

    m-n : ∀ x → Square n-n (ap (λ sx → f (smin sx north)) (merid x))
                           (ap (λ sx → g (smin sx north)) (merid x)) s-n
    m-n x = ↯ (f-merid-x x north) ∙v⊡ (lt-square (merid north) ⊡v∙ ! (ap-cst south (merid x)))

    m-s : ∀ x → Square n-s (ap (λ sx → f (smin sx south)) (merid x))
                           (ap (λ sx → g (smin sx south)) (merid x)) s-s
    m-s x = ↯ (f-merid-x x south) ∙v⊡ (tr-square (merid south) ⊡v∙ ! (ap-cst north (merid x)))

    m-m : ∀ x y →
      Cube (m-n x)
           (m-s x)
           (n-m y)
           (natural-square (λ sy → ap (λ sx → f (smin sx sy)) (merid x)) (merid y))
           (natural-square (λ sy → ap (λ sx → g (smin sx sy)) (merid x)) (merid y))
           (s-m y)
    m-m x y =
      custom-cube-∙v⊡
        (↯ (f-merid-x x north))
        (↯ (f-merid-x x south))
        (ap-cst north (merid y))
        (ap-cst south (merid y)) $
      cube-shift-top (! top-path) $
      custom-cube-⊡v∙
        (! (ap-cst south (merid x)))
        (ap-cst north (merid x))
        (! (↯ (g-merid-y north y)))
        (↯ (g-merid-y south y)) $
      cube-shift-bot (! bot-path) $
      custom-cube (merid north) (merid south) (ap merid (merid (smin x y)))
      where
      custom-cube-∙v⊡ : ∀ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
        {p₀₋₀  : a₀₀₀ == a₀₁₀}
        {p₋₀₀ p₋₀₀' : a₀₀₀ == a₁₀₀} (q₋₀₀ : p₋₀₀ == p₋₀₀')
        {p₋₁₀ : a₀₁₀ == a₁₁₀}
        {p₁₋₀ : a₁₀₀ == a₁₁₀}
        {sq₋₋₀ : Square p₀₋₀ p₋₀₀' p₋₁₀ p₁₋₀} -- left
        {p₀₋₁ : a₀₀₁ == a₀₁₁}
        {p₋₀₁ p₋₀₁' : a₀₀₁ == a₁₀₁} (q₋₀₁ : p₋₀₁ == p₋₀₁')
        {p₋₁₁ : a₀₁₁ == a₁₁₁}
        {p₁₋₁ : a₁₀₁ == a₁₁₁}
        {sq₋₋₁ : Square p₀₋₁ p₋₀₁' p₋₁₁ p₁₋₁} -- right
        {p₀₀₋ p₀₀₋' : a₀₀₀ == a₀₀₁} (q₀₀₋ : p₀₀₋ == p₀₀₋')
        {p₀₁₋ : a₀₁₀ == a₀₁₁}
        {p₁₀₋ p₁₀₋' : a₁₀₀ == a₁₀₁} (q₁₀₋ : p₁₀₋ == p₁₀₋')
        {p₁₁₋ : a₁₁₀ == a₁₁₁}
        {sq₀₋₋ : Square p₀₋₀ p₀₀₋' p₀₁₋ p₀₋₁} -- back
        {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
        {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
        {sq₁₋₋ : Square p₁₋₀ p₁₀₋' p₁₁₋ p₁₋₁} -- front
        → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ (! q₀₀₋ ∙v⊡ (! q₋₀₀ ∙h⊡ sq₋₀₋ ⊡h∙ q₋₀₁) ⊡v∙ q₁₀₋) sq₋₁₋ sq₁₋₋
        → Cube (q₋₀₀ ∙v⊡ sq₋₋₀) (q₋₀₁ ∙v⊡ sq₋₋₁) (q₀₀₋ ∙v⊡ sq₀₋₋) sq₋₀₋ sq₋₁₋ (q₁₀₋ ∙v⊡ sq₁₋₋)
      custom-cube-∙v⊡ idp idp idp idp c = c
      custom-cube-⊡v∙ : ∀ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
        {p₀₋₀  : a₀₀₀ == a₀₁₀}
        {p₋₀₀ : a₀₀₀ == a₁₀₀}
        {p₋₁₀ p₋₁₀' : a₀₁₀ == a₁₁₀} (q₋₁₀ : p₋₁₀ == p₋₁₀')
        {p₁₋₀ : a₁₀₀ == a₁₁₀}
        {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left
        {p₀₋₁ : a₀₀₁ == a₀₁₁}
        {p₋₀₁ : a₀₀₁ == a₁₀₁}
        {p₋₁₁ p₋₁₁' : a₀₁₁ == a₁₁₁} (q₋₁₁ : p₋₁₁' == p₋₁₁)
        {p₁₋₁ : a₁₀₁ == a₁₁₁}
        {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right
        {p₀₀₋ : a₀₀₀ == a₀₀₁}
        {p₀₁₋ p₀₁₋' : a₀₁₀ == a₀₁₁} (q₀₁₋ : p₀₁₋ == p₀₁₋')
        {p₁₀₋ : a₁₀₀ == a₁₀₁}
        {p₁₁₋ p₁₁₋' : a₁₁₀ == a₁₁₁} (q₁₁₋ : p₁₁₋' == p₁₁₋)
        {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
        {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
        {sq₋₁₋ : Square p₋₁₀' p₀₁₋' p₁₁₋' p₋₁₁'} -- bottom
        {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
        → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ (square-symmetry (q₋₁₀ ∙v⊡ (q₀₁₋ ∙h⊡ square-symmetry sq₋₁₋ ⊡h∙ q₁₁₋) ⊡v∙ q₋₁₁)) sq₁₋₋
        → Cube (sq₋₋₀ ⊡v∙ q₋₁₀) (sq₋₋₁ ⊡v∙ ! q₋₁₁) (sq₀₋₋ ⊡v∙ q₀₁₋) sq₋₀₋ sq₋₁₋ (sq₁₋₋ ⊡v∙ ! q₁₁₋)
      custom-cube-⊡v∙ idp idp idp idp {sq₋₁₋ = sq₋₁₋} c =
        cube-shift-bot (square-sym-inv sq₋₁₋) c
      custom-cube : ∀ {i} {S : Type i} {n s : S}
        (p q : n == s) (r : p == q)
        → Cube (lt-square p)
               (tr-square q)
               (lb-square p)
               (horiz-degen-square r)
               (vert-degen-square (ap ! r))
               (br-square (! q))
      custom-cube p@idp q@.idp r@idp = idc
      top-path :
        ! (ap-cst north (merid y)) ∙v⊡
        (! (↯ (f-merid-x x north)) ∙h⊡
         natural-square (λ sy → ap (λ sx → f (smin sx sy)) (merid x)) (merid y) ⊡h∙
         ↯ (f-merid-x x south)) ⊡v∙
        ap-cst south (merid y)
        ==
        horiz-degen-square (ap merid (merid (smin x y)))
      top-path =
        ! (ap-cst north (merid y)) ∙v⊡
        (! (↯ (f-merid-x x north)) ∙h⊡
         natural-square (λ sy → ap (λ sx → f (smin sx sy)) (merid x)) (merid y) ⊡h∙
         ↯ (f-merid-x x south)) ⊡v∙
        ap-cst south (merid y)
          =⟨ ap (λ u → ! (ap-cst north (merid y)) ∙v⊡ u ⊡v∙ ap-cst south (merid y)) $
             natural-square-path
               (λ sy → merid (Susp-fmap (smin x) sy))
               (λ sy → ap (λ sx → f (smin sx sy)) (merid x))
               (λ sy → ↯ (f-merid-x x sy))
               (merid y) ⟩
        ! (ap-cst north (merid y)) ∙v⊡
        natural-square (λ sy → merid (Susp-fmap (smin x) sy)) (merid y) ⊡v∙
        ap-cst south (merid y)
          =⟨ natural-square-cst
               north
               south
               (λ sy → merid (Susp-fmap (smin x) sy))
               (merid y) ⟩
        horiz-degen-square (ap (merid ∘ Susp-fmap (smin x)) (merid y))
          =⟨ ap horiz-degen-square (ap-∘ merid (Susp-fmap (smin x)) (merid y)) ⟩
        horiz-degen-square (ap merid (ap (Susp-fmap (smin x)) (merid y)))
          =⟨ ap (horiz-degen-square ∘ ap merid) (SuspFmap.merid-β (smin x) y) ⟩
        horiz-degen-square (ap merid (merid (smin x y))) =∎
      bot-path :
        square-symmetry
         (! (ap-cst south (merid x)) ∙v⊡
          (! (↯ (g-merid-y north y)) ∙h⊡
           square-symmetry (natural-square
             (λ sy → ap (λ sx → g (smin sx sy)) (merid x)) (merid y)) ⊡h∙
           ↯ (g-merid-y south y)) ⊡v∙
          ap-cst north (merid x))
        ==
        vert-degen-square (ap ! (ap merid (merid (smin x y))))
      bot-path =
        square-symmetry
         (! (ap-cst south (merid x)) ∙v⊡
          (! (↯ (g-merid-y north y)) ∙h⊡
           square-symmetry (natural-square
             (λ sy → ap (λ sx → g (smin sx sy)) (merid x)) (merid y)) ⊡h∙
           ↯ (g-merid-y south y)) ⊡v∙
          ap-cst north (merid x))
          =⟨ ap (λ u → square-symmetry
                        (! (ap-cst south (merid x)) ∙v⊡
                         (! (↯ (g-merid-y north y)) ∙h⊡
                          u ⊡h∙
                          ↯ (g-merid-y south y)) ⊡v∙
                         ap-cst north (merid x))) $
             natural-square-symmetry
               (λ sx sy → g (smin sx sy))
               (merid x)
               (merid y) ⟩
        square-symmetry
         (! (ap-cst south (merid x)) ∙v⊡
          (! (↯ (g-merid-y north y)) ∙h⊡
           natural-square (λ sx → ap (g ∘ smin sx) (merid y)) (merid x) ⊡h∙
           ↯ (g-merid-y south y)) ⊡v∙
          ap-cst north (merid x))
          =⟨ ap (λ u → square-symmetry
                         (! (ap-cst south (merid x)) ∙v⊡ u ⊡v∙ ap-cst north (merid x))) $
             natural-square-path
               (λ sx → ! (merid (Susp-fmap (λ x' → smin x' y) sx)))
               (λ sx → ap (g ∘ smin sx) (merid y))
               (λ sx → ↯ (g-merid-y sx y))
               (merid x) ⟩
        square-symmetry
         (! (ap-cst south (merid x)) ∙v⊡
          natural-square (λ sx → ! (merid (Susp-fmap (λ x' → smin x' y) sx))) (merid x) ⊡v∙
          ap-cst north (merid x))
          =⟨ ap square-symmetry $
             natural-square-cst
               south
               north
               (λ sx → ! (merid (Susp-fmap (λ x' → smin x' y) sx)))
               (merid x) ⟩
        square-symmetry
          (horiz-degen-square
            (ap (λ sx → ! (merid (Susp-fmap (λ x' → smin x' y) sx))) (merid x)))
          =⟨ horiz-degen-square-symmetry
               (ap (λ sx → ! (merid (Susp-fmap (λ x' → smin x' y) sx))) (merid x)) ⟩
        vert-degen-square (ap (! ∘ merid ∘ Susp-fmap (λ x' → smin x' y)) (merid x))
          =⟨ ap vert-degen-square (ap-∘ (! ∘ merid) (Susp-fmap (λ x' → smin x' y)) (merid x)) ⟩
        vert-degen-square (ap (! ∘ merid) (ap (Susp-fmap (λ x' → smin x' y)) (merid x)))
          =⟨ ap (vert-degen-square ∘ ap (! ∘ merid)) (SuspFmap.merid-β (λ x' → smin x' y) x) ⟩
        vert-degen-square (ap (! ∘ merid) (merid (smin x y)))
          =⟨ ap vert-degen-square (ap-∘ ! merid (merid (smin x y))) ⟩
        vert-degen-square (ap ! (ap merid (merid (smin x y)))) =∎

    basel : f smbasel == g smbasel
    basel = merid north

    baser : f smbaser == g smbaser
    baser = merid north

    f-smgluel : ∀ sx → ap f (smgluel sx) == ap (Susp-fmap (∧Σ-out X Y)) (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y)) sx)
    f-smgluel sx =
      ap f (smgluel sx)
        =⟨ ap-∘ (Susp-fmap (∧Σ-out X Y)) (Σ∧-out X (⊙Susp (de⊙ Y))) (smgluel sx) ⟩
      ap (Susp-fmap (∧Σ-out X Y)) (ap (Σ∧-out X (⊙Susp (de⊙ Y))) (smgluel sx))
        =⟨ ap (ap (Susp-fmap (∧Σ-out  X Y)))
              (Σ∧Out.smgluel-β X (⊙Susp (de⊙ Y)) sx) ⟩
      ap (Susp-fmap (∧Σ-out X Y)) (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y)) sx) =∎

    f-smgluel-north : ap f (smgluel north) == idp
    f-smgluel-north = f-smgluel north

    f-smgluel-south : ap f (smgluel south) =-= ! (merid north)
    f-smgluel-south =
      ap f (smgluel south)
        =⟪ f-smgluel south ⟫
      ap (Susp-fmap (∧Σ-out X Y)) (! (merid (smin (pt X) north)))
        =⟪ ap-! (Susp-fmap (∧Σ-out X Y)) (merid (smin (pt X) north)) ⟫
      ! (ap (Susp-fmap (∧Σ-out X Y)) (merid (smin (pt X) north)))
        =⟪ ap ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ⟫
      ! (merid north) ∎∎

    g-smgluel : ∀ sx → ap g (smgluel sx) == idp
    g-smgluel sx =
      ap g (smgluel sx)
        =⟨ ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (∧Σ-out (⊙Susp (de⊙ X)) Y) (smgluel sx) ⟩
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (ap (∧Σ-out (⊙Susp (de⊙ X)) Y) (smgluel sx))
        =⟨ ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
              (∧ΣOut.smgluel-β (⊙Susp (de⊙ X)) Y sx) ⟩
      idp =∎

    smgluel-north : Square n-n (ap f (smgluel north)) (ap g (smgluel north)) basel
    smgluel-north = f-smgluel-north ∙v⊡ hid-square ⊡v∙ ! (g-smgluel north)

    smgluel-south : Square s-n (ap f (smgluel south)) (ap g (smgluel south)) basel
    smgluel-south = ↯ f-smgluel-south ∙v⊡ rt-square (merid north) ⊡v∙ ! (g-smgluel south)

    custom-cube-⊡v∙ : ∀ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
      {p₀₋₀  : a₀₀₀ == a₀₁₀}
      {p₋₀₀ : a₀₀₀ == a₁₀₀}
      {p₋₁₀ p₋₁₀' : a₀₁₀ == a₁₁₀} (q₋₁₀ : p₋₁₀ == p₋₁₀')
      {p₁₋₀ : a₁₀₀ == a₁₁₀}
      {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left
      {p₀₋₁ : a₀₀₁ == a₀₁₁}
      {p₋₀₁ : a₀₀₁ == a₁₀₁}
      {p₋₁₁ p₋₁₁' : a₀₁₁ == a₁₁₁} (q₋₁₁ : p₋₁₁' == p₋₁₁)
      {p₁₋₁ : a₁₀₁ == a₁₁₁}
      {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right
      {p₀₀₋ : a₀₀₀ == a₀₀₁}
      {p₀₁₋ p₀₁₋' : a₀₁₀ == a₀₁₁} (q₀₁₋ : p₀₁₋ == p₀₁₋')
      {p₁₀₋ : a₁₀₀ == a₁₀₁}
      {p₁₁₋ p₁₁₋' : a₁₁₀ == a₁₁₁} (q₁₁₋ : p₁₁₋ == p₁₁₋')
      {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
      {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
      {sq₋₁₋ : Square p₋₁₀' p₀₁₋' p₁₁₋ p₋₁₁'} -- bottom
      {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
      → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ (q₀₁₋ ∙v⊡ (q₋₁₀ ∙h⊡ sq₋₁₋ ⊡h∙ q₋₁₁) ⊡v∙ q₁₁₋) (sq₁₋₋ ⊡v∙ q₁₁₋)
      → Cube (sq₋₋₀ ⊡v∙ q₋₁₀) (sq₋₋₁ ⊡v∙ ! q₋₁₁) (sq₀₋₋ ⊡v∙ q₀₁₋) sq₋₀₋ sq₋₁₋ sq₁₋₋
    custom-cube-⊡v∙ idp idp idp idp c = c

    smgluel-merid : ∀ x →
      Cube smgluel-north
           smgluel-south
           (m-n x)
           (natural-square (λ sx → ap f (smgluel sx)) (merid x))
           (natural-square (λ sx → ap g (smgluel sx)) (merid x))
           (natural-square (λ sx → basel) (merid x))
    smgluel-merid x =
      custom-cube-∙v⊡
        f-smgluel-north
        (f-smgluel south) (↯ (tail f-smgluel-south))
        (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x))
        (↯ (tail (f-merid-x x north)))
        (ap-cst north (merid x)) $
      cube-shift-top (! (top-path x)) $
      custom-cube-⊡v∙
        (! (g-smgluel north))
        (g-smgluel south)
        (! (ap-cst south (merid x)))
        (ap-cst south (merid x)) $
      cube-shift-front (! (front-path x)) $
      cube-shift-bot (! (bot-path x)) $
      custom-cube (merid north)
      where
      custom-cube-∙v⊡ : ∀ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
        {p₀₋₀  : a₀₀₀ == a₀₁₀}
        {p₋₀₀ p₋₀₀' : a₀₀₀ == a₁₀₀} (q₋₀₀ : p₋₀₀ == p₋₀₀')
        {p₋₁₀ : a₀₁₀ == a₁₁₀}
        {p₁₋₀ : a₁₀₀ == a₁₁₀}
        {sq₋₋₀ : Square p₀₋₀ p₋₀₀' p₋₁₀ p₁₋₀} -- left
        {p₀₋₁ : a₀₀₁ == a₀₁₁}
        {p₋₀₁ p₋₀₁' p₋₀₁'' : a₀₀₁ == a₁₀₁} (q₋₀₁ : p₋₀₁ == p₋₀₁') (q₋₀₁' : p₋₀₁' == p₋₀₁'')
        {p₋₁₁ : a₀₁₁ == a₁₁₁}
        {p₁₋₁ : a₁₀₁ == a₁₁₁}
        {sq₋₋₁ : Square p₀₋₁ p₋₀₁'' p₋₁₁ p₁₋₁} -- right
        {p₀₀₋ p₀₀₋' p₀₀₋'' : a₀₀₀ == a₀₀₁} (q₀₀₋ : p₀₀₋ == p₀₀₋') (q₀₀₋' : p₀₀₋' == p₀₀₋'')
        {p₀₁₋ : a₀₁₀ == a₀₁₁}
        {p₁₀₋ p₁₀₋' : a₁₀₀ == a₁₀₁} (q₁₀₋ : p₁₀₋ == p₁₀₋')
        {p₁₁₋ : a₁₁₀ == a₁₁₁}
        {sq₀₋₋ : Square p₀₋₀ p₀₀₋'' p₀₁₋ p₀₋₁} -- back
        {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
        {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
        {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
        → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋
               ((! q₀₀₋' ∙v⊡ (! q₀₀₋ ∙v⊡ (! q₋₀₀ ∙h⊡ sq₋₀₋ ⊡h∙ q₋₀₁)) ⊡v∙ q₁₀₋) ⊡h∙ q₋₀₁')
               sq₋₁₋ (! q₁₀₋ ∙v⊡ sq₁₋₋)
        → Cube (q₋₀₀ ∙v⊡ sq₋₋₀) ((q₋₀₁ ∙ q₋₀₁') ∙v⊡ sq₋₋₁) ((q₀₀₋ ∙ q₀₀₋') ∙v⊡ sq₀₋₋) sq₋₀₋ sq₋₁₋ sq₁₋₋
      custom-cube-∙v⊡ idp idp idp idp idp idp c = c
      custom-cube : ∀ {i} {S : Type i} {n s : S} (p : n == s)
        → Cube hid-square (rt-square p) (lt-square p) (tr-square p) ids hid-square
      custom-cube p@idp = idc
      top-path : ∀ x →
        (! (↯ (tail (f-merid-x x north))) ∙v⊡
         (! (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ∙v⊡
          (! f-smgluel-north ∙h⊡
           natural-square (λ sx → ap f (smgluel sx)) (merid x) ⊡h∙
           f-smgluel south)) ⊡v∙
         ap-cst north (merid x)) ⊡h∙
        ↯ (tail f-smgluel-south)
        ==
        tr-square (merid north)
      top-path x =
        (! (↯ (tail (f-merid-x x north))) ∙v⊡
         (! (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ∙v⊡
          (! f-smgluel-north ∙h⊡
           natural-square (λ sx → ap f (smgluel sx)) (merid x) ⊡h∙
           f-smgluel south)) ⊡v∙
         ap-cst north (merid x)) ⊡h∙
        ↯ (tail f-smgluel-south)
          =⟨ ap (λ u → (! (↯ (tail (f-merid-x x north))) ∙v⊡
                        (! (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ∙v⊡
                         u) ⊡v∙
                        ap-cst north (merid x)) ⊡h∙
                       ↯ (tail f-smgluel-south)) $
             natural-square-path
               (ap (Susp-fmap (∧Σ-out X Y)) ∘ Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y)))
               (λ sx → ap f (smgluel sx))
               f-smgluel
               (merid x) ⟩
        (! (↯ (tail (f-merid-x x north))) ∙v⊡
         (! (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ∙v⊡
          natural-square (ap (Susp-fmap (∧Σ-out X Y)) ∘ Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x)) ⊡v∙
         ap-cst north (merid x)) ⊡h∙
        ↯ (tail f-smgluel-south)
          =⟨ ap (λ v → (! (↯ (tail (f-merid-x x north))) ∙v⊡
                        v ⊡v∙
                        ap-cst north (merid x)) ⊡h∙
                       ↯ (tail f-smgluel-south)) $
             ! (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ∙v⊡
             natural-square (ap (Susp-fmap (∧Σ-out X Y)) ∘ Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x)
               =⟨ ap (! (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ∙v⊡_) $
                  natural-square-ap (Susp-fmap (∧Σ-out X Y)) (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x) ⟩
             ! (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ∙v⊡
             ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x) ∙v⊡
             ap-square (Susp-fmap (∧Σ-out X Y)) (natural-square (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x)) ⊡v∙
             ∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x)
               =⟨ ! $ ∙v⊡-assoc
                    (! (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)))
                    (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x))
                    (ap-square (Susp-fmap (∧Σ-out X Y)) (natural-square (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x)) ⊡v∙
                     ∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x)) ⟩
             (! (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ∙
              ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ∙v⊡
             ap-square (Susp-fmap (∧Σ-out X Y)) (natural-square (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x)) ⊡v∙
             ∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x)
               =⟨ ap (_∙v⊡ ap-square (Susp-fmap (∧Σ-out X Y)) (natural-square (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x)) ⊡v∙
                           ∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x)) $
                  !-inv-l (ap-∘ (Susp-fmap (∧Σ-out X Y)) (Susp-fmap (λ x' → smin x' north)) (merid x)) ⟩
             ap-square (Susp-fmap (∧Σ-out X Y)) (natural-square (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x)) ⊡v∙
             ∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x) =∎ ⟩
        (! (↯ (tail (f-merid-x x north))) ∙v⊡
         (ap-square (Susp-fmap (∧Σ-out X Y)) (natural-square (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x)) ⊡v∙
          ∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x)) ⊡v∙
         ap-cst north (merid x)) ⊡h∙
        ↯ (tail f-smgluel-south)
          =⟨ ap (λ u → (! (↯ (tail (f-merid-x x north))) ∙v⊡
                        u) ⊡h∙
                       ↯ (tail f-smgluel-south)) $
             (ap-square (Susp-fmap (∧Σ-out X Y)) (natural-square (Σ∧OutSmgluel.f X (⊙Susp (de⊙ Y))) (merid x)) ⊡v∙
              ∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x)) ⊡v∙
             ap-cst north (merid x)
               =⟨ ap (λ u → (ap-square (Susp-fmap (∧Σ-out X Y)) u ⊡v∙
                             ∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x)) ⊡v∙
                            ap-cst north (merid x)) $
                  Σ∧OutSmgluel.merid-square-β X (⊙Susp (de⊙ Y)) x ⟩
             (ap-square (Susp-fmap (∧Σ-out X Y)) (Σ∧-out-smgluel-merid X (⊙Susp (de⊙ Y)) x) ⊡v∙
              ∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x)) ⊡v∙
             ap-cst north (merid x)
               =⟨ ⊡v∙-assoc
                    (ap-square (Susp-fmap (∧Σ-out X Y)) (Σ∧-out-smgluel-merid X (⊙Susp (de⊙ Y)) x))
                    (∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x))
                    (ap-cst north (merid x)) ⟩
             ap-square (Susp-fmap (∧Σ-out X Y)) (Σ∧-out-smgluel-merid X (⊙Susp (de⊙ Y)) x) ⊡v∙
             (∘-ap (Susp-fmap (∧Σ-out X Y)) (λ _ → north) (merid x) ∙
              ap-cst north (merid x))
               =⟨ ap (ap-square (Susp-fmap (∧Σ-out X Y)) (Σ∧-out-smgluel-merid X (⊙Susp (de⊙ Y)) x) ⊡v∙_) $
                  =ₛ-out $ ap-∘-cst-coh (Susp-fmap (∧Σ-out X Y)) north (merid x) ⟩
             ap-square (Susp-fmap (∧Σ-out X Y)) (Σ∧-out-smgluel-merid X (⊙Susp (de⊙ Y)) x) ⊡v∙
             ap (ap (Susp-fmap (∧Σ-out X Y))) (ap-cst north (merid x))
               =⟨ ap-square-⊡v∙
                    (Susp-fmap (∧Σ-out X Y))
                    (Σ∧-out-smgluel-merid X (⊙Susp (de⊙ Y)) x)
                    (ap-cst north (merid x)) ⟩
             ap-square
               (Susp-fmap (∧Σ-out X Y))
               (Σ∧-out-smgluel-merid X (⊙Susp (de⊙ Y)) x ⊡v∙ ap-cst north (merid x))
               =⟨ ap (ap-square (Susp-fmap (∧Σ-out X Y))) $
                  ⊡v∙-assoc
                    ((SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x)) ∙v⊡
                     tr-square (merid (smin (pt X) north)))
                    (! (ap-cst north (merid x)))
                    (ap-cst north (merid x)) ⟩
             ap-square
               (Susp-fmap (∧Σ-out X Y))
               (((SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x)) ∙v⊡
                 tr-square (merid (smin (pt X) north))) ⊡v∙
                (! (ap-cst north (merid x)) ∙ ap-cst north (merid x)))
               =⟨ ap (λ u → ap-square (Susp-fmap (∧Σ-out X Y)) $
                            ((SuspFmap.merid-β (λ x' → smin x' north) x ∙
                              ap merid (∧-norm-l x)) ∙v⊡
                             tr-square (merid (smin (pt X) north))) ⊡v∙
                            u) $
                  !-inv-l (ap-cst north (merid x)) ⟩
             ap-square
               (Susp-fmap (∧Σ-out X Y))
               ((SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x)) ∙v⊡
                tr-square (merid (smin (pt X) north)))
               =⟨ ! $ ap-square-∙v⊡
                    (Susp-fmap (∧Σ-out X Y))
                    (SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x))
                    (tr-square (merid (smin (pt X) north))) ⟩
             ap (ap (Susp-fmap (∧Σ-out X Y)))
                (SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x)) ∙v⊡
             ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north))) =∎
           ⟩
        (! (↯ (tail (f-merid-x x north))) ∙v⊡
         ap (ap (Susp-fmap (∧Σ-out X Y)))
            (SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x)) ∙v⊡
         ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north)))) ⊡h∙
        ↯ (tail f-smgluel-south)
          =⟨ ! $ ap (_⊡h∙ ↯ (tail f-smgluel-south)) $
             ∙v⊡-assoc (! (↯ (tail (f-merid-x x north))))
                       (ap (ap (Susp-fmap (∧Σ-out X Y)))
                           (SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x)))
                       (ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north)))) ⟩
        ((! (↯ (tail (f-merid-x x north))) ∙
          ap (ap (Susp-fmap (∧Σ-out X Y)))
             (SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x))) ∙v⊡
         ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north)))) ⊡h∙
        ↯ (tail f-smgluel-south)
          =⟨ ap (λ u → (u ∙v⊡ ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north)))) ⊡h∙
                       ↯ (tail f-smgluel-south)) $ =ₛ-out $
             ! (↯ (tail (f-merid-x x north))) ◃∙
             ap (ap (Susp-fmap (∧Σ-out X Y)))
                (SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x)) ◃∎
               =ₛ⟨ 0 & 1 & !-∙-seq (tail (f-merid-x x north)) ⟩
             ! (SuspFmap.merid-β (∧Σ-out X Y) (smin x north)) ◃∙
             ! (ap (ap (Susp-fmap (∧Σ-out X Y))) (SuspFmap.merid-β (λ x' → smin x' north) x)) ◃∙
             ap (ap (Susp-fmap (∧Σ-out X Y)))
                (SuspFmap.merid-β (λ x' → smin x' north) x ∙ ap merid (∧-norm-l x)) ◃∎
               =ₛ⟨ 2 & 1 &
                   ap-seq-∙
                     (ap (Susp-fmap (∧Σ-out X Y)))
                     (SuspFmap.merid-β (λ x' → smin x' north) x ◃∙
                      ap merid (∧-norm-l x) ◃∎) ⟩
             ! (SuspFmap.merid-β (∧Σ-out X Y) (smin x north)) ◃∙
             ! (ap (ap (Susp-fmap (∧Σ-out X Y))) (SuspFmap.merid-β (λ x' → smin x' north) x)) ◃∙
             ap (ap (Susp-fmap (∧Σ-out X Y))) (SuspFmap.merid-β (λ x' → smin x' north) x) ◃∙
             ap (ap (Susp-fmap (∧Σ-out X Y))) (ap merid (∧-norm-l x)) ◃∎
               =ₛ⟨ 1 & 2 & seq-!-inv-l $
                   ap (ap (Susp-fmap (∧Σ-out X Y)))
                      (SuspFmap.merid-β (λ x' → smin x' north) x) ◃∎ ⟩
             ! (SuspFmap.merid-β (∧Σ-out X Y) (smin x north)) ◃∙
             ap (ap (Susp-fmap (∧Σ-out X Y))) (ap merid (∧-norm-l x)) ◃∎
               =ₛ₁⟨ 1 & 1 & ∘-ap (ap (Susp-fmap (∧Σ-out X Y))) merid (∧-norm-l x) ⟩
             ! (SuspFmap.merid-β (∧Σ-out X Y) (smin x north)) ◃∙
             ap (ap (Susp-fmap (∧Σ-out X Y)) ∘ merid) (∧-norm-l x) ◃∎
               =ₛ⟨ !ₛ $
                   homotopy-naturality
                     (merid ∘ ∧Σ-out X Y)
                     (ap (Susp-fmap (∧Σ-out X Y)) ∘ merid)
                     (! ∘ SuspFmap.merid-β (∧Σ-out X Y))
                     (∧-norm-l x) ⟩
             ap (merid ∘ ∧Σ-out X Y) (∧-norm-l x) ◃∙
             ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ◃∎
               =ₛ⟨ 0 & 1 & =ₛ-in {t = []} $
                   ap-∘ merid (∧Σ-out X Y) (∧-norm-l x) ∙
                   ap (ap merid) (∧Σ-out-∧-norm-l X Y x) ⟩
             ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ◃∎ ∎ₛ ⟩
        (! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ∙v⊡
         ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north)))) ⊡h∙
        ↯ (tail f-smgluel-south)
          =⟨ ∙v⊡-⊡h∙-comm
               (! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)))
               (ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north))))
               (↯ (tail f-smgluel-south)) ⟩
        ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ∙v⊡
        ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north))) ⊡h∙
        ↯ (tail f-smgluel-south)
          =⟨ ! $ ap (! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ∙v⊡_) $
             ⊡h∙-assoc
               (ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north))))
               (ap-! (Susp-fmap (∧Σ-out X Y)) (merid (smin (pt X) north)))
               (ap ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north))) ⟩
        ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ∙v⊡
        ap-square (Susp-fmap (∧Σ-out X Y)) (tr-square (merid (smin (pt X) north))) ⊡h∙
        ap-! (Susp-fmap (∧Σ-out X Y)) (merid (smin (pt X) north)) ⊡h∙
        ap ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north))
          =⟨ ap (λ u → ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ∙v⊡
                       u ⊡h∙
                       ap ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north))) $
             ap-tr-square (Susp-fmap (∧Σ-out X Y)) (merid (smin (pt X) north)) ⟩
        ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ∙v⊡
        tr-square (ap (Susp-fmap (∧Σ-out X Y)) (merid (smin (pt X) north))) ⊡h∙
        ap ! (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north))
          =⟨ tr-square-∙v⊡-⊡h∙ (SuspFmap.merid-β (∧Σ-out X Y) (smin (pt X) north)) ⟩
        tr-square (merid north) =∎
      front-path : ∀ (x : de⊙ X) →
        (! (ap-cst north (merid x)) ∙v⊡
         natural-square (λ sx → basel) (merid x)) ⊡v∙
        ap-cst south (merid x)
        ==
        hid-square
      front-path x =
        (! (ap-cst north (merid x)) ∙v⊡
         natural-square (λ sx → basel) (merid x)) ⊡v∙
        ap-cst south (merid x)
          =⟨ ∙v⊡-⊡v∙-comm
               (! (ap-cst north (merid x)))
               (natural-square (λ sx → basel) (merid x))
               (ap-cst south (merid x)) ⟩
        ! (ap-cst north (merid x)) ∙v⊡
        natural-square (λ sx → basel) (merid x) ⊡v∙
        ap-cst south (merid x)
          =⟨ natural-square-cst north south (λ sx → basel) (merid x) ⟩
        horiz-degen-square (ap (λ sx → basel) (merid x))
          =⟨ ap horiz-degen-square (ap-cst basel (merid x)) ⟩
        horiz-degen-square idp
          =⟨ horiz-degen-square-idp ⟩
        hid-square =∎
      bot-path : ∀ (x : de⊙ X) →
        ! (ap-cst south (merid x)) ∙v⊡
        (! (g-smgluel north) ∙h⊡
         natural-square (λ sx → ap g (smgluel sx)) (merid x) ⊡h∙
         g-smgluel south) ⊡v∙
        ap-cst south (merid x)
        ==
        ids
      bot-path x =
        ! (ap-cst south (merid x)) ∙v⊡
        (! (g-smgluel north) ∙h⊡
         natural-square (λ sx → ap g (smgluel sx)) (merid x) ⊡h∙
         g-smgluel south) ⊡v∙
        ap-cst south (merid x)
          =⟨ ap (λ u → ! (ap-cst south (merid x)) ∙v⊡ u ⊡v∙ ap-cst south (merid x)) $
             natural-square-path
               (λ sx → idp)
               (λ sx → ap g (smgluel sx))
               g-smgluel
               (merid x) ⟩
        ! (ap-cst south (merid x)) ∙v⊡
        natural-square (λ sx → idp) (merid x) ⊡v∙
        ap-cst south (merid x)
          =⟨ natural-square-cst
               south
               south
               (λ sx → idp)
               (merid x) ⟩
        disc-to-square (ap (λ sx → idp) (merid x))
          =⟨ ap disc-to-square (ap-cst idp (merid x)) ⟩
        ids =∎

    f-smgluer : ∀ sy → ap f (smgluer sy) == idp
    f-smgluer sy =
      ap f (smgluer sy)
        =⟨ ap-∘ (Susp-fmap (∧Σ-out X Y)) (Σ∧-out X (⊙Susp (de⊙ Y))) (smgluer sy) ⟩
      ap (Susp-fmap (∧Σ-out X Y)) (ap (Σ∧-out X (⊙Susp (de⊙ Y))) (smgluer sy))
        =⟨ ap (ap (Susp-fmap (∧Σ-out  X Y)))
              (Σ∧Out.smgluer-β X (⊙Susp (de⊙ Y)) sy) ⟩
      idp =∎

    g-smgluer : ∀ sy →
      ap g (smgluer sy)
      ==
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (∧ΣOutSmgluer.f (⊙Susp (de⊙ X)) Y sy)
    g-smgluer sy =
      ap g (smgluer sy)
        =⟨ ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (∧Σ-out (⊙Susp (de⊙ X)) Y) (smgluer sy) ⟩
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (ap (∧Σ-out (⊙Susp (de⊙ X)) Y) (smgluer sy))
        =⟨ ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
              (∧ΣOut.smgluer-β (⊙Susp (de⊙ X)) Y sy) ⟩
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (∧ΣOutSmgluer.f (⊙Susp (de⊙ X)) Y sy) =∎

    g-smgluer-north : ap g (smgluer north) == idp
    g-smgluer-north = g-smgluer north

    g-smgluer-south-step :
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))
      ==
      ! (merid north)
    g-smgluer-south-step = ↯ $
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))
        =⟪ ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y))) ⟫
      ap Susp-flip (ap (Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y))))
        =⟪ ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) (smin north (pt Y))) ⟫
      ap Susp-flip (merid north)
        =⟪ SuspFlip.merid-β north ⟫
      ! (merid north) ∎∎

    g-smgluer-south : ap g (smgluer south) =-= merid north
    g-smgluer-south =
      ap g (smgluer south)
        =⟪ g-smgluer south ⟫
      ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (! (merid (smin north (pt Y))))
        =⟪ ap-! (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y))) ⟫
      ! (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y))))
        =⟪ ap ! g-smgluer-south-step ⟫
      ! (! (merid north))
        =⟪ !-! (merid north) ⟫
      merid north ∎∎

    smgluer-north : Square n-n (ap f (smgluer north)) (ap g (smgluer north)) baser
    smgluer-north = f-smgluer north ∙v⊡ hid-square ⊡v∙ ! g-smgluer-north

    smgluer-south : Square n-s (ap f (smgluer south)) (ap g (smgluer south)) baser
    smgluer-south = f-smgluer south ∙v⊡ br-square (merid north) ⊡v∙ ! (↯ (g-smgluer-south))

    smgluer-merid : ∀ (y : de⊙ Y) →
      Cube smgluer-north
           smgluer-south
           (n-m y)
           (natural-square (λ a → ap f (smgluer a)) (merid y))
           (natural-square (λ a → ap g (smgluer a)) (merid y))
           (natural-square (λ a → baser) (merid y))
    smgluer-merid y =
      smgluer-merid-custom-cube-∙v⊡
        (f-smgluer north)
        (f-smgluer south)
        (ap-cst north (merid y))
        (ap-cst north (merid y)) $
      cube-shift-top (! top-path) $
      custom-cube-⊡v∙
        (! g-smgluer-north)
        (↯ g-smgluer-south)
        (! (↯ (g-merid-y north y)))
        (ap-cst south (merid y)) $
      cube-shift-front (! front-path) $
      cube-shift-bot (! bot-path) $
      custom-cube (merid north)
      where
      smgluer-merid-custom-cube-∙v⊡ :
        ∀ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
        {p₀₋₀  : a₀₀₀ == a₀₁₀}
        {p₋₀₀ p₋₀₀' : a₀₀₀ == a₁₀₀} (q₋₀₀ : p₋₀₀' == p₋₀₀)
        {p₋₁₀ : a₀₁₀ == a₁₁₀}
        {p₁₋₀ : a₁₀₀ == a₁₁₀}
        {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left
        {p₀₋₁ : a₀₀₁ == a₀₁₁}
        {p₋₀₁ p₋₀₁' : a₀₀₁ == a₁₀₁} (q₋₀₁ : p₋₀₁' == p₋₀₁)
        {p₋₁₁ : a₀₁₁ == a₁₁₁}
        {p₁₋₁ : a₁₀₁ == a₁₁₁}
        {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right
        {p₀₀₋ p₀₀₋' : a₀₀₀ == a₀₀₁} (q₀₀₋ : p₀₀₋' == p₀₀₋)
        {p₀₁₋ : a₀₁₀ == a₀₁₁}
        {p₁₀₋ p₁₀₋' : a₁₀₀ == a₁₀₁} (q₁₀₋ : p₁₀₋ == p₁₀₋')
        {p₁₁₋ : a₁₁₀ == a₁₁₁}
        {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
        {sq₋₀₋ : Square p₋₀₀' p₀₀₋' p₁₀₋ p₋₀₁'} -- top
        {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
        {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
        → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ (! q₀₀₋ ∙v⊡ (! q₋₀₀ ∙h⊡ sq₋₀₋ ⊡h∙ q₋₀₁) ⊡v∙ q₁₀₋) sq₋₁₋ (! q₁₀₋ ∙v⊡ sq₁₋₋)
        → Cube (q₋₀₀ ∙v⊡ sq₋₋₀) (q₋₀₁ ∙v⊡ sq₋₋₁) (q₀₀₋ ∙v⊡ sq₀₋₋) sq₋₀₋ sq₋₁₋ sq₁₋₋
      smgluer-merid-custom-cube-∙v⊡ idp idp idp idp c = c
      top-path :
        ! (ap-cst north (merid y)) ∙v⊡
        (! (f-smgluer north) ∙h⊡
         natural-square (λ sy → ap f (smgluer sy)) (merid y) ⊡h∙
         f-smgluer south) ⊡v∙
        ap-cst north (merid y)
        ==
        ids
      top-path =
        ! (ap-cst north (merid y)) ∙v⊡
        (! (f-smgluer north) ∙h⊡
         natural-square (λ sy → ap f (smgluer sy)) (merid y) ⊡h∙
         f-smgluer south) ⊡v∙
        ap-cst north (merid y)
          =⟨ ap (λ u → ! (ap-cst north (merid y)) ∙v⊡ u ⊡v∙ ap-cst north (merid y)) $
             natural-square-path
               (λ sy → idp)
               (λ sy → ap f (smgluer sy))
               f-smgluer
               (merid y) ⟩
        ! (ap-cst north (merid y)) ∙v⊡
        natural-square (λ sy → idp) (merid y) ⊡v∙
        ap-cst north (merid y)
          =⟨ natural-square-cst
               north
               north
               (λ sy → idp)
               (merid y) ⟩
        disc-to-square (ap (λ sy → idp) (merid y))
          =⟨ ap disc-to-square (ap-cst idp (merid y)) ⟩
        ids =∎
      front-path :
        (! (ap-cst north (merid y)) ∙v⊡
         natural-square (λ sy → baser) (merid y)) ⊡v∙
        ap-cst south (merid y)
        ==
        hid-square
      front-path =
        (! (ap-cst north (merid y)) ∙v⊡
         natural-square (λ sy → baser) (merid y)) ⊡v∙
        ap-cst south (merid y)
          =⟨ ∙v⊡-⊡v∙-comm (! (ap-cst north (merid y)))
                          (natural-square (λ sy → baser) (merid y))
                          (ap-cst south (merid y)) ⟩
        ! (ap-cst north (merid y)) ∙v⊡
        natural-square (λ sy → baser) (merid y) ⊡v∙
        ap-cst south (merid y)
          =⟨ natural-square-cst
               north
               south
               (λ sy → baser)
               (merid y) ⟩
        horiz-degen-square (ap (λ sy → baser) (merid y))
          =⟨ ap horiz-degen-square (ap-cst baser (merid y)) ⟩
        horiz-degen-square idp
          =⟨ horiz-degen-square-idp ⟩
        hid-square =∎
      bot-path :
        ! (↯ (g-merid-y north y)) ∙v⊡
        (! g-smgluer-north ∙h⊡
         natural-square (λ sy → ap g (smgluer sy)) (merid y) ⊡h∙
         ↯ g-smgluer-south) ⊡v∙
        ap-cst south (merid y)
        ==
        rt-square (merid north)
      bot-path =
        ! (↯ (g-merid-y north y)) ∙v⊡
        (! g-smgluer-north ∙h⊡
         natural-square (λ sy → ap g (smgluer sy)) (merid y) ⊡h∙
         ↯ g-smgluer-south) ⊡v∙
        ap-cst south (merid y)
          =⟨ ap (λ u → ! (↯ (g-merid-y north y)) ∙v⊡ u ⊡v∙ ap-cst south (merid y)) $
             ! g-smgluer-north ∙h⊡
             natural-square (λ sy → ap g (smgluer sy)) (merid y) ⊡h∙
             ↯ g-smgluer-south
               =⟨ ! $ ap (! g-smgluer-north ∙h⊡_) $
                  ⊡h∙-assoc
                    (natural-square (λ sy → ap g (smgluer sy)) (merid y))
                    (g-smgluer south)
                    (↯ (tail g-smgluer-south)) ⟩
             ! g-smgluer-north ∙h⊡
             natural-square (λ sy → ap g (smgluer sy)) (merid y) ⊡h∙
             g-smgluer south ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ! $ ∙h⊡-⊡h∙-comm
                    (! g-smgluer-north)
                    (natural-square (λ sy → ap g (smgluer sy)) (merid y) ⊡h∙ g-smgluer south)
                    (↯ (tail g-smgluer-south)) ⟩
             (! g-smgluer-north ∙h⊡
              natural-square (λ sy → ap g (smgluer sy)) (merid y) ⊡h∙
              g-smgluer south) ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ap (_⊡h∙ ↯ (tail g-smgluer-south)) $
                  natural-square-path
                    (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) ∘ ∧ΣOutSmgluer.f (⊙Susp (de⊙ X)) Y)
                    (λ sy → ap g (smgluer sy))
                    g-smgluer
                    (merid y) ⟩
             natural-square (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) ∘ ∧ΣOutSmgluer.f (⊙Susp (de⊙ X)) Y) (merid y) ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ap (_⊡h∙ ↯ (tail g-smgluer-south)) $
                  natural-square-ap
                    (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                    (∧ΣOutSmgluer.f (⊙Susp (de⊙ X)) Y)
                    (merid y) ⟩
             (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
              ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                        (natural-square (∧ΣOutSmgluer.f (⊙Susp (de⊙ X)) Y) (merid y)) ⊡v∙
              ∘-ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (λ _ → north) (merid y)) ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ap (λ u → (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
                             ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) u ⊡v∙
                             ∘-ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (λ _ → north) (merid y)) ⊡h∙
                            ↯ (tail g-smgluer-south)) $
                  ∧ΣOutSmgluer.merid-square-β (⊙Susp (de⊙ X)) Y y ⟩
             (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
              ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                        (∧Σ-out-smgluer-merid (⊙Susp (de⊙ X)) Y y) ⊡v∙
              ∘-ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (λ _ → north) (merid y)) ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ap (λ u → (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
                             u ⊡v∙
                             ∘-ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (λ _ → north) (merid y)) ⊡h∙
                            ↯ (tail g-smgluer-south)) $ ! $
                  ap-square-⊡v∙
                    (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                    ((SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ∙v⊡
                     tr-square (merid (smin north (pt Y))))
                    (! (ap-cst north (merid y))) ⟩
             (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
              ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                        ((SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ∙v⊡
                         tr-square (merid (smin north (pt Y)))) ⊡v∙
              ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (! (ap-cst north (merid y))) ⊡v∙
              ∘-ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (λ _ → north) (merid y)) ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ap (λ u → (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡ u) ⊡h∙
                            ↯ (tail g-smgluer-south)) $
                  ⊡v∙-assoc
                    (ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                       ((SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ∙v⊡
                        tr-square (merid (smin north (pt Y)))))
                    (ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (! (ap-cst north (merid y))))
                    (∘-ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (λ _ → north) (merid y)) ⟩
             (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
              ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                        ((SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ∙v⊡
                         tr-square (merid (smin north (pt Y)))) ⊡v∙
              (ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (! (ap-cst north (merid y))) ∙
               ∘-ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (λ _ → north) (merid y))) ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ap (λ u → (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
                             ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                                       ((SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ∙v⊡
                                        tr-square (merid (smin north (pt Y)))) ⊡v∙
                             u) ⊡h∙
                            ↯ (tail g-smgluer-south)) $ =ₛ-out $
                  ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (! (ap-cst north (merid y))) ◃∙
                  ∘-ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (λ _ → north) (merid y) ◃∎
                    =ₛ⟨ 1 & 1 &
                        post-rotate-in {p = _ ◃∎} $
                        ap-∘-cst-coh (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) north (merid y) ⟩
                  ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (! (ap-cst north (merid y))) ◃∙
                  ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (ap-cst north (merid y)) ◃∙
                  ! (ap-cst south (merid y)) ◃∎
                    =ₛ⟨ 0 & 2 & ap-seq-=ₛ (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) $
                                seq-!-inv-l (ap-cst north (merid y) ◃∎) ⟩
                  ! (ap-cst south (merid y)) ◃∎ ∎ₛ ⟩
             (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
              ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                        ((SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ∙v⊡
                         tr-square (merid (smin north (pt Y)))) ⊡v∙
              ! (ap-cst south (merid y))) ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ap (λ u → (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡ u ⊡v∙
                             (! (ap-cst south (merid y)))) ⊡h∙
                            ↯ (tail g-smgluer-south)) $ ! $
                  ap-square-∙v⊡
                    (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                    (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))
                    (tr-square (merid (smin north (pt Y)))) ⟩
             (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
              (ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                  (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ∙v⊡
               ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                         (tr-square (merid (smin north (pt Y))))) ⊡v∙
              ! (ap-cst south (merid y))) ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ! $ ap (_⊡h∙ ↯ (tail g-smgluer-south)) $
                  ∙v⊡-⊡v∙-comm
                    (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y))
                    (ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                        (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ∙v⊡
                     ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                               (tr-square (merid (smin north (pt Y)))))
                    (! (ap-cst south (merid y))) ⟩
             (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙v⊡
              ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                 (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ∙v⊡
              ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                        (tr-square (merid (smin north (pt Y))))) ⊡v∙
             ! (ap-cst south (merid y)) ⊡h∙
             ↯ (tail g-smgluer-south)
               =⟨ ! $ ap (λ u → u ⊡v∙ ! (ap-cst south (merid y)) ⊡h∙ ↯ (tail g-smgluer-south)) $
                  ∙v⊡-assoc
                    (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y))
                    (ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                        (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)))
                    (ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                               (tr-square (merid (smin north (pt Y))))) ⟩
             ((ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
               ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                  (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
              ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                        (tr-square (merid (smin north (pt Y))))) ⊡v∙
             ! (ap-cst south (merid y)) ⊡h∙
             ↯ (tail g-smgluer-south) =∎
           ⟩
        ! (↯ (g-merid-y north y)) ∙v⊡
        (((ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
           ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
              (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
          ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                    (tr-square (merid (smin north (pt Y))))) ⊡v∙
         ! (ap-cst south (merid y)) ⊡h∙
         ↯ (tail g-smgluer-south)) ⊡v∙
        ap-cst south (merid y)
          =⟨ ap (! (↯ (g-merid-y north y)) ∙v⊡_) $ ! $
             ⊡v∙-⊡h∙-comm
               (((ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
                  ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                     (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
                 ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                           (tr-square (merid (smin north (pt Y))))) ⊡v∙
                ! (ap-cst south (merid y)))
               (ap-cst south (merid y))
               (↯ (tail g-smgluer-south)) ⟩
        ! (↯ (g-merid-y north y)) ∙v⊡
        (((ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
           ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
              (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
          ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                    (tr-square (merid (smin north (pt Y))))) ⊡v∙
         ! (ap-cst south (merid y)) ⊡v∙
         ap-cst south (merid y)) ⊡h∙
        ↯ (tail g-smgluer-south)
          =⟨ ap (λ u → ! (↯ (g-merid-y north y)) ∙v⊡ u ⊡h∙ ↯ (tail g-smgluer-south)) $
             ⊡v∙-assoc
               ((ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
                 ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                    (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
                ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                          (tr-square (merid (smin north (pt Y)))))
               (! (ap-cst south (merid y)))
               (ap-cst south (merid y)) ⟩
        ! (↯ (g-merid-y north y)) ∙v⊡
        (((ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
           ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
              (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
          ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                    (tr-square (merid (smin north (pt Y))))) ⊡v∙
         (! (ap-cst south (merid y)) ∙ ap-cst south (merid y))) ⊡h∙
        ↯ (tail g-smgluer-south)
          =⟨ ap (λ u → ! (↯ (g-merid-y north y)) ∙v⊡
                       (((ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
                          ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                             (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
                         ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                                   (tr-square (merid (smin north (pt Y))))) ⊡v∙
                        u) ⊡h∙
                       ↯ (tail g-smgluer-south)) $
             !-inv-l (ap-cst south (merid y)) ⟩
        ! (↯ (g-merid-y north y)) ∙v⊡
        ((ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
          ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
             (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
         ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                   (tr-square (merid (smin north (pt Y))))) ⊡h∙
        ↯ (tail g-smgluer-south)
          =⟨ ap (! (↯ (g-merid-y north y)) ∙v⊡_) $
             ∙v⊡-⊡h∙-comm
               (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
                ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                   (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)))
               (ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                          (tr-square (merid (smin north (pt Y)))))
               (↯ (tail g-smgluer-south)) ⟩
        ! (↯ (g-merid-y north y)) ∙v⊡
        (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
         ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
            (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
        ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                  (tr-square (merid (smin north (pt Y)))) ⊡h∙
        ↯ (tail g-smgluer-south)
          =⟨ ! $
             ∙v⊡-assoc
               (! (↯ (g-merid-y north y)))
               (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
                ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                   (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)))
               (ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                          (tr-square (merid (smin north (pt Y)))) ⊡h∙
                ↯ (tail g-smgluer-south)) ⟩
        (! (↯ (g-merid-y north y)) ∙
         ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ∙
         ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
            (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y))) ∙v⊡
        ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                  (tr-square (merid (smin north (pt Y)))) ⊡h∙
        ↯ (tail g-smgluer-south)
          =⟨ ap (_∙v⊡ ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                                (tr-square (merid (smin north (pt Y)))) ⊡h∙
                      ↯ (tail g-smgluer-south)) $ =ₛ-out $
             ! (↯ (g-merid-y north y)) ◃∙
             ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ◃∙
             ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                (SuspFmap.merid-β (smin north) y ∙ ap merid (∧-norm-r y)) ◃∎
               =ₛ⟨ 2 & 1 & ap-seq-∙ (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) $
                     (SuspFmap.merid-β (smin north) y ◃∙
                      ap merid (∧-norm-r y) ◃∎) ⟩
             ! (↯ (g-merid-y north y)) ◃∙
             ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ◃∙
             ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (SuspFmap.merid-β (smin north) y) ◃∙
             ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (ap merid (∧-norm-r y)) ◃∎
               =ₛ⟨ 0 & 1 & !-∙-seq (g-merid-y north y) ⟩
             ! (SuspFlip.merid-β north) ◃∙
             ! (ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) (smin north y))) ◃∙
             ! (ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) (merid (smin north y))) ◃∙
             ! (ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (SuspFmap.merid-β (smin north) y)) ◃∙
             ! (ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y)) ◃∙
             ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ◃∙
             ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (SuspFmap.merid-β (smin north) y) ◃∙
             ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (ap merid (∧-norm-r y)) ◃∎
               =ₛ⟨ 3 & 4 & seq-!-inv-l $
                   ap-∘ (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (Susp-fmap (smin north)) (merid y) ◃∙
                   ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (SuspFmap.merid-β (smin north) y) ◃∎ ⟩
             ! (SuspFlip.merid-β north) ◃∙
             ! (ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) (smin north y))) ◃∙
             ! (ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) (merid (smin north y))) ◃∙
             ap (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))) (ap merid (∧-norm-r y)) ◃∎
               =ₛ⟨ 2 & 2 & !ₛ $
                   homotopy-naturality
                     (ap Susp-flip ∘ ap (Susp-fmap (Σ∧-out X Y)))
                     (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)))
                     (λ p → ! (ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) p))
                     (ap merid (∧-norm-r y)) ⟩
             ! (SuspFlip.merid-β north) ◃∙
             ! (ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) (smin north y))) ◃∙
             ap (ap Susp-flip ∘ ap (Susp-fmap (Σ∧-out X Y))) (ap merid (∧-norm-r y)) ◃∙
             ! (ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))) ◃∎
               =ₛ₁⟨ 2 & 1 &
                    ∘-ap (ap Susp-flip ∘ ap (Susp-fmap (Σ∧-out X Y))) merid (∧-norm-r y) ⟩
             ! (SuspFlip.merid-β north) ◃∙
             ! (ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) (smin north y))) ◃∙
             ap (ap Susp-flip ∘ ap (Susp-fmap (Σ∧-out X Y)) ∘ merid) (∧-norm-r y) ◃∙
             ! (ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))) ◃∎
               =ₛ⟨ 1 & 2 & !ₛ $
                   homotopy-naturality
                     (ap Susp-flip ∘ merid ∘ Σ∧Out.f X Y)
                     (ap Susp-flip ∘ ap (Susp-fmap (Σ∧-out X Y)) ∘ merid)
                     (λ w → ! (ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) w)))
                     (∧-norm-r y) ⟩
             ! (SuspFlip.merid-β north) ◃∙
             ap (ap Susp-flip ∘ merid ∘ Σ∧-out X Y) (∧-norm-r y) ◃∙
             ! (ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) (smin north (pt Y)))) ◃∙
             ! (ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))) ◃∎
               =ₛ⟨ 1 & 1 & =ₛ-in {t = []} $
                   ap-∘ (ap Susp-flip ∘ merid) (Σ∧-out X Y) (∧-norm-r y) ∙
                   ap (ap (ap Susp-flip ∘ merid)) (Σ∧-out-∧-norm-r X Y y) ⟩
             ! (SuspFlip.merid-β north) ◃∙
             ! (ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) (smin north (pt Y)))) ◃∙
             ! (ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))) ◃∎
               =ₛ⟨ ∙-!-seq $
                   ap-∘ Susp-flip (Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y))) ◃∙
                   ap (ap Susp-flip) (SuspFmap.merid-β (Σ∧-out X Y) (smin north (pt Y))) ◃∙
                   SuspFlip.merid-β north ◃∎ ⟩
             ! g-smgluer-south-step ◃∎ ∎ₛ
           ⟩
        ! g-smgluer-south-step ∙v⊡
        ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                  (tr-square (merid (smin north (pt Y)))) ⊡h∙
        ↯ (tail g-smgluer-south)
          =⟨ ! $ ap (! g-smgluer-south-step ∙v⊡_) $
             ⊡h∙-assoc
               (ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                          (tr-square (merid (smin north (pt Y)))))
               (ap-! (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y))))
               (ap ! g-smgluer-south-step ∙ !-! (merid north)) ⟩
        ! g-smgluer-south-step ∙v⊡
        ap-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y))
                  (tr-square (merid (smin north (pt Y)))) ⊡h∙
        ap-! (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y))) ⊡h∙
        (ap ! g-smgluer-south-step ∙ !-! (merid north))
          =⟨ ap (λ u → ! g-smgluer-south-step ∙v⊡ u ⊡h∙
                       (ap ! g-smgluer-south-step ∙ !-! (merid north))) $
             ap-tr-square (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y))) ⟩
        ! g-smgluer-south-step ∙v⊡
        tr-square (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))) ⊡h∙
        (ap ! g-smgluer-south-step ∙ !-! (merid north))
          =⟨ ! $ ap (! g-smgluer-south-step ∙v⊡_) $
             ⊡h∙-assoc
               (tr-square (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))))
               (ap ! g-smgluer-south-step)
               (!-! (merid north)) ⟩
        ! g-smgluer-south-step ∙v⊡
        tr-square (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))) ⊡h∙
        ap ! g-smgluer-south-step ⊡h∙
        !-! (merid north)
          =⟨ ! $ ∙v⊡-⊡h∙-comm
               (! g-smgluer-south-step)
               (tr-square (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))) ⊡h∙
                ap ! g-smgluer-south-step)
               (!-! (merid north)) ⟩
        (! g-smgluer-south-step ∙v⊡
         tr-square (ap (Susp-flip ∘ Susp-fmap (Σ∧-out X Y)) (merid (smin north (pt Y)))) ⊡h∙
         ap ! g-smgluer-south-step) ⊡h∙
        !-! (merid north)
          =⟨ ap (_⊡h∙ !-! (merid north)) $
             tr-square-∙v⊡-⊡h∙ g-smgluer-south-step ⟩
        tr-square (! (merid north)) ⊡h∙ !-! (merid north)
          =⟨ tr-square-! (merid north) ⟩
        rt-square (merid north) =∎
      custom-cube : ∀ {i} {S : Type i} {n s : S} (p : n == s)
        → Cube hid-square (br-square p) (lb-square p) ids (rt-square p) hid-square
      custom-cube p@idp = idc

  module ∧Σ-Σ∧-Out =
    Σ∧Σ-PathElim
      f g
      n-n n-s s-n s-s
      n-m s-m m-n m-s
      m-m
      basel
      baser
      smgluel-north
      smgluel-south
      smgluel-merid
      smgluer-north
      smgluer-south
      smgluer-merid

  ∧Σ-Σ∧-out : Susp-fmap (∧Σ-out X Y) ∘ Σ∧-out X (⊙Susp (de⊙ Y))
            ∼ Susp-flip ∘ Susp-fmap (Σ∧-out X Y) ∘ ∧Σ-out (⊙Susp (de⊙ X)) Y
  ∧Σ-Σ∧-out = ∧Σ-Σ∧-Out.f

  ⊙∧Σ-Σ∧-out : ⊙Susp-fmap (∧Σ-out X Y) ◃⊙∘
               ⊙Σ∧-out X (⊙Susp (de⊙ Y)) ◃⊙idf
               =⊙∘
               ⊙Susp-flip (⊙Susp (X ∧ Y)) ◃⊙∘
               ⊙Susp-fmap (Σ∧-out X Y) ◃⊙∘
               ⊙∧Σ-out (⊙Susp (de⊙ X)) Y ◃⊙idf
  ⊙∧Σ-Σ∧-out =
    ⊙seq-λ= ∧Σ-Σ∧-out $ !ₛ $
    merid north ◃∙
    idp ◃∙
    idp ◃∙
    ! (merid north) ◃∎
      =ₛ⟨ 1 & 1 & expand [] ⟩
    merid north ◃∙
    idp ◃∙
    ! (merid north) ◃∎
      =ₛ⟨ 1 & 1 & expand [] ⟩
    merid north ◃∙
    ! (merid north) ◃∎
      =ₛ₁⟨ !-inv-r (merid north) ⟩
    idp ◃∎
      =ₛ⟨ 0 & 0 & contract ⟩
    idp ◃∙
    idp ◃∎ ∎ₛ

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --type-in-type #-}
open import Data.Unit
open import Data.Product hiding ( curry ; uncurry )
open import Data.List hiding ( concat )
open import Data.String
open import Relation.Binary.PropositionalEquality
module Spire.Examples.PropositionalDesc where

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

elimEq : (A : Set) (x : A) (P : (y : A) → x ≡ y → Set)
  → P x refl
  → (y : A) (p : x ≡ y) → P y p
elimEq A .x P prefl x refl = prefl

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

Label : Set
Label = String

Enum : Set
Enum = List Label

data Tag : Enum → Set where
  here : ∀{l E} → Tag (l ∷ E)
  there : ∀{l E} → Tag E → Tag (l ∷ E)

Cases : (E : Enum) (P : Tag E → Set) → Set
Cases [] P = ⊤
Cases (l ∷ E) P = P here × Cases E λ t → P (there t)

case : (E : Enum) (P : Tag E → Set) (cs : Cases E P) (t : Tag E) → P t
case (l ∷ E) P (c , cs) here = c
case (l ∷ E) P (c , cs) (there t) = case E (λ t → P (there t)) cs t

UncurriedCases : (E : Enum) (P : Tag E → Set) (X : Set)
  → Set
UncurriedCases E P X = Cases E P → X

CurriedCases : (E : Enum) (P : Tag E → Set) (X : Set)
  → Set
CurriedCases [] P X = X
CurriedCases (l ∷ E) P X = P here → CurriedCases E (λ t → P (there t)) X

curryCases : (E : Enum) (P : Tag E → Set) (X : Set)
  (f : UncurriedCases E P X) → CurriedCases E P X
curryCases [] P X f = f tt
curryCases (l ∷ E) P X f = λ c → curryCases E (λ t → P (there t)) X (λ cs → f (c , cs))

uncurryCases : (E : Enum) (P : Tag E → Set) (X : Set)
  (f : CurriedCases E P X) → UncurriedCases E P X
uncurryCases [] P X x tt = x
uncurryCases (l ∷ E) P X f (c , cs) = uncurryCases E (λ t → P (there t)) X (f c) cs

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

data Desc (I : Set) : Set₁ where
  `End : (i : I) → Desc I
  `Rec : (i : I) (D : Desc I) → Desc I
  `Arg : (A : Set) (B : A → Desc I) → Desc I
  `RecFun : (A : Set) (B : A → I) (D : Desc I) → Desc I

ISet : Set → Set₁
ISet I = I → Set

El : (I : Set) (D : Desc I) (X : ISet I) → ISet I
El I (`End j) X i = j ≡ i
El I (`Rec j D) X i = X j × El I D X i
El I (`Arg A B) X i = Σ A (λ a → El I (B a) X i)
El I (`RecFun A B D) X i = ((a : A) → X (B a)) × El I D X i

Hyps : (I : Set) (D : Desc I) (X : ISet I) (P : (i : I) → X i → Set) (i : I) (xs : El I D X i) → Set
Hyps I (`End j) X P i q = ⊤
Hyps I (`Rec j D) X P i (x , xs) = P j x × Hyps I D X P i xs
Hyps I (`Arg A B) X P i (a , b) = Hyps I (B a) X P i b
Hyps I (`RecFun A B D) X P i (f , xs) = ((a : A) → P (B a) (f a)) × Hyps I D X P i xs

caseD : (E : Enum) (I : Set) (cs : Cases E (λ _ → Desc I)) (t : Tag E) → Desc I
caseD E I cs t = case E (λ _ → Desc I) cs t

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

TagDesc : (I : Set) → Set
TagDesc I = Σ Enum (λ E → Cases E (λ _ → Desc I))

toCase : (I : Set) (E,cs : TagDesc I) → Tag (proj₁ E,cs) → Desc I
toCase I (E , cs) = case E (λ _ → Desc I) cs

toDesc : (I : Set) → TagDesc I → Desc I
toDesc I (E , cs) = `Arg (Tag E) (toCase I (E , cs))

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

UncurriedEl : (I : Set) (D : Desc I) (X : ISet I) → Set
UncurriedEl I D X = {i : I} → El I D X i → X i

CurriedEl : (I : Set) (D : Desc I) (X : ISet I) → Set
CurriedEl I (`End i) X = X i
CurriedEl I (`Rec j D) X = (x : X j) → CurriedEl I D X
CurriedEl I (`Arg A B) X = (a : A) → CurriedEl I (B a) X
CurriedEl I (`RecFun A B D) X = ((a : A) → X (B a)) → CurriedEl I D X

curryEl : (I : Set) (D : Desc I) (X : ISet I)
  (cn : UncurriedEl I D X) → CurriedEl I D X
curryEl I (`End i) X cn = cn refl
curryEl I (`Rec i D) X cn = λ x → curryEl I D X (λ xs → cn (x , xs))
curryEl I (`Arg A B) X cn = λ a → curryEl I (B a) X (λ xs → cn (a , xs))
curryEl I (`RecFun A B D) X cn = λ f → curryEl I D X (λ xs → cn (f , xs))

uncurryEl : (I : Set) (D : Desc I) (X : ISet I)
  (cn : CurriedEl I D X) → UncurriedEl I D X
uncurryEl I (`End i) X cn refl = cn
uncurryEl I (`Rec i D) X cn (x , xs) = uncurryEl I D X (cn x) xs
uncurryEl I (`Arg A B) X cn (a , xs) = uncurryEl I (B a) X (cn a) xs
uncurryEl I (`RecFun A B D) X cn (f , xs) = uncurryEl I D X (cn f) xs

data μ (I : Set) (D : Desc I) : I → Set where
  con : UncurriedEl I D (μ I D)

con2 : (I : Set) (D : Desc I) → CurriedEl I D (μ I D)
con2 I D = curryEl I D (μ I D) con

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

UncurriedHyps : (I : Set) (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl I D X)
  → Set
UncurriedHyps I D X P cn =
  (i : I) (xs : El I D X i) → Hyps I D X P i xs → P i (cn xs)

CurriedHyps : (I : Set) (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl I D X)
  → Set
CurriedHyps I (`End i) X P cn =
  P i (cn refl)
CurriedHyps I (`Rec i D) X P cn =
  (x : X i) → P i x → CurriedHyps I D X P (λ xs → cn (x , xs))
CurriedHyps I (`Arg A B) X P cn =
  (a : A) → CurriedHyps I (B a) X P (λ xs → cn (a , xs))
CurriedHyps I (`RecFun A B D) X P cn =
  (f : (a : A) → X (B a)) (ihf : (a : A) → P (B a) (f a)) → CurriedHyps I D X P (λ xs → cn (f , xs))

curryHyps : (I : Set) (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl I D X)
  (pf : UncurriedHyps I D X P cn)
  → CurriedHyps I D X P cn
curryHyps I (`End i) X P cn pf =
  pf i refl tt
curryHyps I (`Rec i D) X P cn pf =
  λ x ih → curryHyps I D X P (λ xs → cn (x , xs)) (λ i xs ihs → pf i (x , xs) (ih , ihs))
curryHyps I (`Arg A B) X P cn pf =
  λ a → curryHyps I (B a) X P (λ xs → cn (a , xs)) (λ i xs ihs → pf i (a , xs) ihs)
curryHyps I (`RecFun A B D) X P cn pf =
  λ f ihf → curryHyps I D X P (λ xs → cn (f , xs)) (λ i xs ihs → pf i (f , xs) (ihf , ihs))

uncurryHyps : (I : Set) (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl I D X)
  (pf : CurriedHyps I D X P cn)
  → UncurriedHyps I D X P cn
uncurryHyps I (`End .i) X P cn pf i refl tt =
  pf
uncurryHyps I (`Rec j D) X P cn pf i (x , xs) (ih , ihs) =
  uncurryHyps I D X P (λ ys → cn (x , ys)) (pf x ih) i xs ihs
uncurryHyps I (`Arg A B) X P cn pf i (a , xs) ihs =
  uncurryHyps I (B a) X P (λ ys → cn (a , ys)) (pf a) i xs ihs
uncurryHyps I (`RecFun A B D) X P cn pf i (f , xs) (ihf , ihs) =
  uncurryHyps I D X P (λ ys → cn (f , ys)) (pf f ihf) i xs ihs

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

ind :
  (I : Set)
  (D : Desc I)
  (P : (i : I) → μ I D i → Set)
  (pcon : UncurriedHyps I D (μ I D) P con)
  (i : I)
  (x : μ I D i)
  → P i x

hyps :
  (I : Set)
  (D₁ : Desc I)
  (P : (i : I) → μ I D₁ i → Set)
  (pcon : UncurriedHyps I D₁ (μ I D₁) P con)
  (D₂ : Desc I)
  (i : I)
  (xs : El I D₂ (μ I D₁) i)
  → Hyps I D₂ (μ I D₁) P i xs

ind I D P pcon i (con xs) = pcon i xs (hyps I D P pcon D i xs)

hyps I D P pcon (`End j) i q = tt
hyps I D P pcon (`Rec j A) i (x , xs) = ind I D P pcon j x , hyps I D P pcon A i xs
hyps I D P pcon (`Arg A B) i (a , b) = hyps I D P pcon (B a) i b
hyps I D P pcon (`RecFun A B E) i (f , xs) = (λ a → ind I D P pcon (B a) (f a)) , hyps I D P pcon E i xs

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

ind2 :
  (I : Set)
  (D : Desc I)
  (P : (i : I) → μ I D i → Set)
  (pcon : CurriedHyps I D (μ I D) P con)
  (i : I)
  (x : μ I D i)
  → P i x
ind2 I D P pcon i x = ind I D P (uncurryHyps I D (μ I D) P con pcon) i x

elim :
  (I : Set)
  (TD : TagDesc I)
  → let
    D = toDesc I TD
    E = proj₁ TD
    Cs = toCase I TD
  in (P : (i : I) → μ I D i → Set)
  → let
    Q = λ t → CurriedHyps I (Cs t) (μ I D) P (λ xs → con (t , xs))
    X = (i : I) (x : μ I D i) → P i x
  in UncurriedCases E Q X
elim I TD P cs i x =
  let
    D = toDesc I TD
    E = proj₁ TD
    Cs = toCase I TD
    Q = λ t → CurriedHyps I (Cs t) (μ I D) P (λ xs → con (t , xs))
    p = case E Q cs
  in ind2 I D P p i x

elim2 :
  (I : Set)
  (TD : TagDesc I)
  → let
    D = toDesc I TD
    E = proj₁ TD
    Cs = toCase I TD
  in (P : (i : I) → μ I D i → Set)
  → let
    Q = λ t → CurriedHyps I (Cs t) (μ I D) P (λ xs → con (t , xs))
    X = (i : I) (x : μ I D i) → P i x
  in CurriedCases E Q X
elim2 I TD P =
  let
    D = toDesc I TD
    E = proj₁ TD
    Cs = toCase I TD
    Q = λ t → CurriedHyps I (Cs t) (μ I D) P (λ xs → con (t , xs))
    X = (i : I) (x : μ I D i) → P i x
  in curryCases E Q X (elim I TD P)

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

module Sugared where

  data ℕT : Set where `zero `suc : ℕT
  data VecT : Set where `nil `cons : VecT

  ℕD : Desc ⊤
  ℕD = `Arg ℕT λ
    { `zero → `End tt
    ; `suc → `Rec tt (`End tt)
    }

  ℕ : ⊤ → Set
  ℕ = μ ⊤ ℕD

  zero : ℕ tt
  zero = con (`zero , refl)

  suc : ℕ tt → ℕ tt
  suc n = con (`suc , n , refl)

  VecD : (A : Set) → Desc (ℕ tt)
  VecD A = `Arg VecT λ
    { `nil  → `End zero
    ; `cons → `Arg (ℕ tt) λ n → `Arg A λ _ → `Rec n (`End (suc n))
    }

  Vec : (A : Set) (n : ℕ tt) → Set
  Vec A n = μ (ℕ tt) (VecD A) n

  nil : (A : Set) → Vec A zero
  nil A = con (`nil , refl)

  cons : (A : Set) (n : ℕ tt) (x : A) (xs : Vec A n) → Vec A (suc n)
  cons A n x xs = con (`cons , n , x , xs , refl)

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

  add : ℕ tt → ℕ tt → ℕ tt
  add = ind ⊤ ℕD (λ _ _ → ℕ tt → ℕ tt)
    (λ
      { tt (`zero , q) tt n → n
      ; tt (`suc , m , q) (ih , tt) n → suc (ih n)
      }
    )
    tt

  mult : ℕ tt → ℕ tt → ℕ tt
  mult = ind ⊤ ℕD (λ _ _ → ℕ tt → ℕ tt)
    (λ
      { tt (`zero , q) tt n → zero
      ; tt (`suc , m , q) (ih , tt) n → add n (ih n)
      }
    )
    tt

  append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
  append A = ind (ℕ tt) (VecD A) (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n))
    (λ
      { .(con (`zero , refl)) (`nil , refl) ih n ys → ys
      ; .(con (`suc , m , refl)) (`cons , m , x , xs , refl) (ih , tt) n ys → cons A (add m n) x (ih n ys)
      }
    )

  concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Vec A (mult n m)
  concat A m = ind (ℕ tt) (VecD (Vec A m)) (λ n xss → Vec A (mult n m))
    (λ
      { .(con (`zero , refl)) (`nil , refl) tt → nil A
      ; .(con (`suc , n , refl)) (`cons , n , xs , xss , refl) (ih , tt) → append A m xs (mult n m) ih
      }
    )

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

module Desugared where

  ℕT : Enum
  ℕT = "zero" ∷ "suc" ∷ []

  VecT : Enum
  VecT = "nil" ∷ "cons" ∷ []

  ℕTD : TagDesc ⊤
  ℕTD = ℕT
    , `End tt
    , `Rec tt (`End tt)
    , tt

  ℕCs : Tag ℕT → Desc ⊤
  ℕCs = toCase ⊤ ℕTD

  ℕD : Desc ⊤
  ℕD = toDesc ⊤ ℕTD

  ℕ : ⊤ → Set
  ℕ = μ ⊤ ℕD

  zero : ℕ tt
  zero = con (here , refl)

  suc : ℕ tt → ℕ tt
  suc n = con (there here , n , refl)

  zero2 : ℕ tt
  zero2 = con2 ⊤ ℕD here

  suc2 : ℕ tt → ℕ tt
  suc2 = con2 ⊤ ℕD (there here)

  VecTD : (A : Set) → TagDesc (ℕ tt)
  VecTD A = VecT
    , `End zero
    , `Arg (ℕ tt) (λ n → `Arg A λ _ → `Rec n (`End (suc n)))
    , tt

  VecCs : (A : Set) → Tag VecT → Desc (ℕ tt)
  VecCs A = toCase (ℕ tt) (VecTD A)

  VecD : (A : Set) → Desc (ℕ tt)
  VecD A = toDesc (ℕ tt) (VecTD A)

  Vec : (A : Set) (n : ℕ tt) → Set
  Vec A n = μ (ℕ tt) (VecD A) n

  nil : (A : Set) → Vec A zero
  nil A = con (here , refl)

  cons : (A : Set) (n : ℕ tt) (x : A) (xs : Vec A n) → Vec A (suc n)
  cons A n x xs = con (there here , n , x , xs , refl)

  nil2 : (A : Set) → Vec A zero
  nil2 A = con2 (ℕ tt) (VecD A) here

  cons2 : (A : Set) (n : ℕ tt) (x : A) (xs : Vec A n) → Vec A (suc n)
  cons2 A = con2 (ℕ tt) (VecD A) (there here)

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

  module Induction where

    add : ℕ tt → ℕ tt → ℕ tt
    add = ind ⊤ ℕD (λ _ _ → ℕ tt → ℕ tt)
      (λ u t,c → case ℕT
        (λ t → (c : El ⊤ (ℕCs t) ℕ u)
               (ih : Hyps ⊤ ℕD ℕ (λ u n → ℕ u → ℕ u) u (t , c))
               → ℕ u → ℕ u
        )
        ( (λ q ih n → n)
        , (λ m,q ih,tt n → suc (proj₁ ih,tt n))
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )
      tt

    mult : ℕ tt → ℕ tt → ℕ tt
    mult = ind ⊤ ℕD (λ _ _ → ℕ tt → ℕ tt)
      (λ u t,c → case ℕT
        (λ t → (c : El ⊤ (ℕCs t) ℕ u)
               (ih : Hyps ⊤ ℕD ℕ (λ u n → ℕ u → ℕ u) u (t , c))
               → ℕ u → ℕ u
        )
        ( (λ q ih n → zero)
        , (λ m,q ih,tt n → add n (proj₁ ih,tt n))
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )
      tt

    append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
    append A = ind (ℕ tt) (VecD A) (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n))
      (λ m t,c → case VecT
        (λ t → (c : El (ℕ tt) (VecCs A t) (Vec A) m)
               (ih : Hyps (ℕ tt) (VecD A) (Vec A) (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)) m (t , c))
               (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
        )
        ( (λ q ih n ys → subst (λ m → Vec A (add m n)) q ys)
        , (λ m',x,xs,q ih,tt n ys →
            let m' = proj₁ m',x,xs,q
                x = proj₁ (proj₂ m',x,xs,q)
                q = proj₂ (proj₂ (proj₂ m',x,xs,q))
                ih = proj₁ ih,tt
            in
            subst (λ m → Vec A (add m n)) q (cons A (add m' n) x (ih n ys))
          )
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )

    concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Vec A (mult n m)
    concat A m = ind (ℕ tt) (VecD (Vec A m)) (λ n xss → Vec A (mult n m))
      (λ n t,c → case VecT
        (λ t → (c : El (ℕ tt) (VecCs (Vec A m) t) (Vec (Vec A m)) n)
               (ih : Hyps (ℕ tt) (VecD (Vec A m)) (Vec (Vec A m)) (λ n xss → Vec A (mult n m)) n (t , c))
               → Vec A (mult n m)
        )
        ( (λ q ih → subst (λ n → Vec A (mult n m)) q (nil A))
        , (λ n',xs,xss,q ih,tt →
            let n' = proj₁ n',xs,xss,q
                xs = proj₁ (proj₂ n',xs,xss,q)
                q = proj₂ (proj₂ (proj₂ n',xs,xss,q))
                ih = proj₁ ih,tt
            in
            subst (λ n → Vec A (mult n m)) q (append A m xs (mult n' m) ih)
          )
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )

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

  module Eliminator where

    elimℕ : (P : (ℕ tt) → Set)
      (pzero : P zero)
      (psuc : (m : ℕ tt) → P m → P (suc m))
      (n : ℕ tt)
      → P n
    elimℕ P pzero psuc = ind ⊤ ℕD (λ u n → P n)
      (λ u t,c → case ℕT
        (λ t → (c : El ⊤ (ℕCs t) ℕ u)
               (ih : Hyps ⊤ ℕD ℕ (λ u n → P n) u (t , c))
               → P (con (t , c))
        )
        ( (λ q ih →
            elimEq ⊤ tt (λ u q → P (con (here , q)))
              pzero
              u q
          )
        , (λ n,q ih,tt →
            elimEq ⊤ tt (λ u q → P (con (there here , proj₁ n,q , q)))
              (psuc (proj₁ n,q) (proj₁ ih,tt))
              u (proj₂ n,q)
          )
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )
      tt

    elimVec : (A : Set) (P : (n : ℕ tt) → Vec A n → Set)
      (pnil : P zero (nil A))
      (pcons : (n : ℕ tt) (a : A) (xs : Vec A n) → P n xs → P (suc n) (cons A n a xs))
      (n : ℕ tt)
      (xs : Vec A n)
      → P n xs
    elimVec A P pnil pcons = ind (ℕ tt) (VecD A) (λ n xs → P n xs)
      (λ n t,c → case VecT
        (λ t → (c : El (ℕ tt) (VecCs A t) (Vec A) n)
               (ih : Hyps (ℕ tt) (VecD A) (Vec A) (λ n xs → P n xs) n (t , c))
               → P n (con (t , c))
        )
        ( (λ q ih →
            elimEq (ℕ tt) zero (λ n q → P n (con (here , q)))
              pnil
              n q
          )
        , (λ n',x,xs,q ih,tt →
            let n' = proj₁ n',x,xs,q
                x = proj₁ (proj₂ n',x,xs,q)
                xs = proj₁ (proj₂ (proj₂ n',x,xs,q))
                q = proj₂ (proj₂ (proj₂ n',x,xs,q))
                ih = proj₁ ih,tt
            in
            elimEq (ℕ tt) (suc n') (λ n q → P n (con (there here , n' , x , xs , q)))
              (pcons n' x xs ih )
              n q
          )
        , tt
        )
        (proj₁ t,c)
        (proj₂ t,c)
      )

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

    add : ℕ tt → ℕ tt → ℕ tt
    add = elimℕ (λ _ → ℕ tt → ℕ tt)
      (λ n → n)
      (λ m ih n → suc (ih n))

    mult : ℕ tt → ℕ tt → ℕ tt
    mult = elimℕ (λ _ → ℕ tt → ℕ tt)
      (λ n → zero)
      (λ m ih n → add n (ih n))

    append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
    append A = elimVec A (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n))
      (λ n ys → ys)
      (λ m x xs ih n ys → cons A (add m n) x (ih n ys))

    concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Vec A (mult n m)
    concat A m = elimVec (Vec A m) (λ n xss → Vec A (mult n m))
      (nil A)
      (λ n xs xss ih → append A m xs (mult n m) ih)

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

  module GenericEliminator where

    add : ℕ tt → ℕ tt → ℕ tt
    add = elim2 ⊤ ℕTD _
      (λ n → n)
      (λ m ih n → suc (ih n))
      tt

    mult : ℕ tt → ℕ tt → ℕ tt
    mult = elim2 ⊤ ℕTD _
      (λ n → zero)
      (λ m ih n → add n (ih n))
      tt

    append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
    append A = elim2 (ℕ tt) (VecTD A) _
      (λ n ys → ys)
      (λ m x xs ih n ys → cons A (add m n) x (ih n ys))

    concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Vec A (mult n m)
    concat A m = elim2 (ℕ tt) (VecTD (Vec A m)) _
      (nil A)
      (λ n xs xss ih → append A m xs (mult n m) ih)

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

ext: agda

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
{-# OPTIONS --safe --warning=error --without-K --guardedness #-}

open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import LogicalFormulae
open import Orders.Total.Definition
open import Orders.Partial.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Sequences
open import Setoids.Orders.Partial.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Setoids.Orders.Partial.Sequences {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Rel {a} {c} A} (p : SetoidPartialOrder S _<_) where

open SetoidPartialOrder p

WeaklyIncreasing' : (Sequence A) → Set (b ⊔ c)
WeaklyIncreasing' s = (m n : ℕ) → (m <N n) → (index s m) <= (index s n)

WeaklyIncreasing : (Sequence A) → Set (b ⊔ c)
WeaklyIncreasing s = (m : ℕ) → (index s m) <= index s (succ m)

tailRespectsWeaklyIncreasing : (a : Sequence A) → WeaklyIncreasing a → WeaklyIncreasing (Sequence.tail a)
tailRespectsWeaklyIncreasing a incr m = incr (succ m)

weaklyIncreasingImplies' : (a : Sequence A) → WeaklyIncreasing a → WeaklyIncreasing' a
weaklyIncreasingImplies' a x zero (succ zero) m<n = x 0
weaklyIncreasingImplies' a x zero (succ (succ n)) m<n = <=Transitive (weaklyIncreasingImplies' a x zero (succ n) (succIsPositive n)) (x (succ n))
weaklyIncreasingImplies' a x (succ m) (succ n) m<n = weaklyIncreasingImplies' (Sequence.tail a) (tailRespectsWeaklyIncreasing a x) m n (canRemoveSuccFrom<N m<n)

weaklyIncreasing'Implies : (a : Sequence A) → WeaklyIncreasing' a → WeaklyIncreasing a
weaklyIncreasing'Implies a incr m = incr m (succ m) (le 0 refl)

StrictlyIncreasing' : (Sequence A) → Set (c)
StrictlyIncreasing' s = (m n : ℕ) → (m <N n) → (index s m) < (index s n)

StrictlyIncreasing : (Sequence A) → Set (c)
StrictlyIncreasing s = (m : ℕ) → (index s m) < index s (succ m)

tailRespectsStrictlyIncreasing : (a : Sequence A) → StrictlyIncreasing a → StrictlyIncreasing (Sequence.tail a)
tailRespectsStrictlyIncreasing a incr m = incr (succ m)

strictlyIncreasingImplies' : (a : Sequence A) → StrictlyIncreasing a → StrictlyIncreasing' a
strictlyIncreasingImplies' a x zero (succ zero) m<n = x 0
strictlyIncreasingImplies' a x zero (succ (succ n)) m<n = <Transitive (strictlyIncreasingImplies' a x zero (succ n) (succIsPositive n)) (x (succ n))
strictlyIncreasingImplies' a x (succ m) (succ n) m<n = strictlyIncreasingImplies' (Sequence.tail a) (tailRespectsStrictlyIncreasing a x) m n (canRemoveSuccFrom<N m<n)

strictlyIncreasing'Implies : (a : Sequence A) → StrictlyIncreasing' a → StrictlyIncreasing a
strictlyIncreasing'Implies a incr m = incr m (succ m) (le 0 refl)


text:
open import Level using (Level; suc; zero; _⊔_)
open import Function using (const)
open import Algebra
open import Algebra.Structures
open import Algebra.OrderedMonoid
open import Algebra.Pregroup
open import Algebra.FunctionProperties as FunctionProperties using (Op₁; Op₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary
open import Relation.Binary.PartialOrderReasoning as ≤-Reasoning using ()

module Algebra.PregroupPlus where

record IsPregroupPlus
       {a ℓ₁ ℓ₂} {A : Set a} (≈ : Rel A ℓ₁) (≤ : Rel A ℓ₂)
       (∙ : Op₂ A) (ε₁ : A) (ˡ : Op₁ A) (ʳ : Op₁ A)
       (+ : Op₂ A) (ε₀ : A) (ᵘ : Op₁ A) (ᵈ : Op₁ A)
       : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where

  field
    ∙-isPregroup : IsPregroup ≈ ≤ ∙ ε₁ ˡ ʳ
    +-isPregroup : IsPregroup ≈ ≤ + ε₀ ᵘ ᵈ

  open IsPregroup ∙-isPregroup public
       using (ˡ-cong; ʳ-cong; ˡ-contract; ʳ-contract
             ;ˡ-expand; ʳ-expand; ∙-cong)
       renaming (assoc to ∙-assoc; identity to ∙-identity
                ;compatibility to ∙-compatibility)
  open IsPregroup +-isPregroup public
       using (≤-refl; ≤-reflexive; ≤-trans; ≤-resp-≈; refl; sym; trans; antisym)
       renaming (ˡ-cong to ᵈ-cong; ʳ-cong to ᵘ-cong
                ;ˡ-contract to ᵈ-contract; ʳ-contract to ᵘ-contract
                ;ˡ-expand to ᵈ-expand; ʳ-expand to ᵘ-expand
                ;∙-cong to +-cong; assoc to +-assoc; identity to +-identity
                ;compatibility to +-compatibility)

record PregroupPlus c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infixl 7 _∙_
  infixl 6 _+_
  infix  4 _≈_
  infix  4 _≤_
  field
    Carrier         : Set c
    _≈_             : Rel Carrier ℓ₁
    _≤_             : Rel Carrier ℓ₂
    _∙_             : Op₂ Carrier
    ε₁              : Carrier
    _ˡ              : Op₁ Carrier
    _ʳ              : Op₁ Carrier
    _+_             : Op₂ Carrier
    ε₀              : Carrier
    _ᵘ              : Op₁ Carrier
    _ᵈ              : Op₁ Carrier
    isPregroupPlus  : IsPregroupPlus _≈_ _≤_ _∙_ ε₁ _ˡ _ʳ _+_ ε₀ _ᵘ _ᵈ

  open IsPregroupPlus isPregroupPlus public

  ∙-pregroup : Pregroup _ _ _
  ∙-pregroup = record { isPregroup = ∙-isPregroup }
  open Pregroup ∙-pregroup public using (
    ˡ-unique; ˡ-identity; ˡ-distrib; ˡ-contra; ˡʳ-cancel;
    ʳ-unique; ʳ-identity; ʳ-distrib; ʳ-contra; ʳˡ-cancel)

  +-pregroup : Pregroup _ _ _
  +-pregroup = record { isPregroup = +-isPregroup }
  open Pregroup +-pregroup public using () renaming (
    ˡ-unique to ᵈ-unique; ˡ-identity to ᵈ-identity; ˡ-distrib to ᵈ-distrib;
    ˡ-contra to ᵈ-contra; ˡʳ-cancel to ᵈᵘ-cancel;
    ʳ-unique to ᵘ-unique; ʳ-identity to ᵘ-identity; ʳ-distrib to ᵘ-distrib;
    ʳ-contra to ᵘ-contra; ʳˡ-cancel to ᵘᵈ-calcel)

max_stars_repo_name: wenkokke/agda-pregroup

max_issues_repo_name: wenkokke/agda-pregroup

max_forks_repo_name: wenkokke/agda-pregroup


text:
-- Everything is strictly positive, but Agda doesn't see this.
{-# OPTIONS --no-positivity-check #-}

module Generic.Core where

open import Generic.Lib.Prelude public

infix  4 _≤ℓ_
infixr 5 _⇒_ _⊛_

_≤ℓ_ : Level -> Level -> Set
α ≤ℓ β = α ⊔ β ≡ β

mutual
  Binder : ∀ {ι} α β γ -> ArgInfo -> ι ⊔ lsuc (α ⊔ β) ≡ γ -> Set ι -> Set γ
  Binder α β γ i q I = Coerce q (∃ λ (A : Set α) -> < relevance i > A -> Desc I β)

  data Desc {ι} (I : Set ι) β : Set (ι ⊔ lsuc β) where
    var : I -> Desc I β
    π   : ∀ {α} i
        -> (q : α ≤ℓ β)
        -> Binder α β _ i (cong (λ αβ -> ι ⊔ lsuc αβ) q) I
        -> Desc I β
    _⊛_ : Desc I β -> Desc I β -> Desc I β

pattern DPi i A D = π i refl (coerce (A , D))

{-# DISPLAY π i refl (coerce (A , D)) = DPi i A D #-}

pattern explRelDPi A D = DPi explRelInfo A D
pattern explIrrDPi A D = DPi explIrrInfo A D
pattern implRelDPi A D = DPi implRelInfo A D
pattern implIrrDPi A D = DPi implIrrInfo A D
pattern instRelDPi A D = DPi instRelInfo A D
pattern instIrrDPi A D = DPi instIrrInfo A D

{-# DISPLAY DPi explRelInfo A D = explRelDPi A D #-}
{-# DISPLAY DPi explIrrInfo A D = explIrrDPi A D #-}
{-# DISPLAY DPi implRelInfo A D = implRelDPi A D #-}
{-# DISPLAY DPi implIrrInfo A D = implIrrDPi A D #-}
{-# DISPLAY DPi instRelInfo A D = instRelDPi A D #-}
{-# DISPLAY DPi instIrrInfo A D = instIrrDPi A D #-}

_⇒_ : ∀ {ι α β} {I : Set ι} {{q : α ≤ℓ β}} -> Set α -> Desc I β -> Desc I β
_⇒_ {{q}} A D = π (explRelInfo) q (qcoerce (A , λ _ -> D))

mutual
  ⟦_⟧ : ∀ {ι β} {I : Set ι} -> Desc I β -> (I -> Set β) -> Set β
  ⟦ var i   ⟧ B = B i
  ⟦ π i q C ⟧ B = ⟦ i / C ⟧ᵇ q B
  ⟦ D ⊛ E   ⟧ B = ⟦ D ⟧ B × ⟦ E ⟧ B

  ⟦_/_⟧ᵇ : ∀ {α ι β γ q} {I : Set ι} i
         -> Binder α β γ i q I -> α ≤ℓ β -> (I -> Set β) -> Set β
  ⟦ i / coerce (A , D) ⟧ᵇ q B = Coerce′ q $ Pi i A λ x -> ⟦ D x ⟧ B

mutual
  Extend : ∀ {ι β} {I : Set ι} -> Desc I β -> (I -> Set β) -> I -> Set β
  Extend (var i)   B j = Lift _ (i ≡ j)
  Extend (π i q C) B j = Extendᵇ i C q B j
  Extend (D ⊛ E)   B j = ⟦ D ⟧ B × Extend E B j

  Extendᵇ : ∀ {ι α β γ q} {I : Set ι} i
          -> Binder α β γ i q I -> α ≤ℓ β -> (I -> Set β) -> I -> Set β
  Extendᵇ i (coerce (A , D)) q B j = Coerce′ q $ ∃ λ x -> Extend (D x) B j

module _ {ι β} {I : Set ι} (D : Data (Desc I β)) where
  mutual
    data μ j : Set β where
      node : Node D j -> μ j

    Node : Data (Desc I β) -> I -> Set β
    Node D j = Any (λ C -> Extend C μ j) (consTypes D)

mutual
  Cons : ∀ {ι β} {I : Set ι} -> (I -> Set β) -> Desc I β -> Set β
  Cons B (var i)   = B i
  Cons B (π i q C) = Consᵇ B i C q
  Cons B (D ⊛ E)   = ⟦ D ⟧ B -> Cons B E

  Consᵇ : ∀ {ι α β γ q} {I : Set ι}
        -> (I -> Set β) -> ∀ i -> Binder α β γ i q I -> α ≤ℓ β -> Set β
  Consᵇ B i (coerce (A , D)) q = Coerce′ q $ Pi i A λ x -> Cons B (D x)

cons : ∀ {ι β} {I : Set ι} {D} -> (D₀ : Data (Desc I β)) -> D ∈ consTypes D₀ -> Cons (μ D₀) D
cons {D = D} D₀ p = go D λ e ->
  node (mapAny (consTypes D₀) (λ q -> subst (λ E -> Extend E _ _) q e) p) where
    mutual
      go : ∀ {ι β} {I : Set ι} {B : I -> Set β}
         -> (D : Desc I β) -> (∀ {j} -> Extend D B j -> B j) -> Cons B D
      go (var i)   k = k lrefl
      go (π a q C) k = goᵇ a C k
      go (D ⊛ E)   k = λ x -> go E (k ∘ _,_ x)

      goᵇ : ∀ {ι α β γ q q′} {I : Set ι} {B : I -> Set β} i
          -> (C : Binder α β γ i q′ I) -> (∀ {j} -> Extendᵇ i C q B j -> B j) -> Consᵇ B i C q
      goᵇ {q = q} i (coerce (A , D)) k =
        coerce′ q $ lamPi i λ x -> go (D x) (k ∘ coerce′ q ∘ _,_ x)

allCons : ∀ {ι β} {I : Set ι} -> (D : Data (Desc I β)) -> All (Cons (μ D)) (consTypes D)
allCons D = allIn _ (cons D)

node-inj : ∀ {i β} {I : Set i} {D : Data (Desc I β)} {j} {e₁ e₂ : Node D D j}
         -> node {D = D} e₁ ≡ node e₂ -> e₁ ≡ e₂
node-inj refl = refl

μ′ : ∀ {β} -> Data (Desc ⊤₀ β) -> Set β
μ′ D = μ D tt

pos : ∀ {β} -> Desc ⊤₀ β
pos = var tt

pattern #₀ p = node (inj₁ p)
pattern #₁ p = node (inj₂ (inj₁ p))
pattern #₂ p = node (inj₂ (inj₂ (inj₁ p)))
pattern #₃ p = node (inj₂ (inj₂ (inj₂ (inj₁ p))))
pattern #₄ p = node (inj₂ (inj₂ (inj₂ (inj₂ (inj₁ p)))))
pattern #₅ p = node (inj₂ (inj₂ (inj₂ (inj₂ (inj₂ (inj₁ p))))))

pattern !#₀ p = node p
pattern !#₁ p = node (inj₂ p)
pattern !#₂ p = node (inj₂ (inj₂ p))
pattern !#₃ p = node (inj₂ (inj₂ (inj₂ p)))
pattern !#₄ p = node (inj₂ (inj₂ (inj₂ (inj₂ p))))
pattern !#₅ p = node (inj₂ (inj₂ (inj₂ (inj₂ (inj₂ p)))))

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
{-# OPTIONS --cubical --safe --postfix-projections #-}

module Data.Rational.Unnormalised where

open import Prelude
open import Data.Integer using (ℤ; ⁺)
import Data.Integer as ℤ
import Data.Nat as ℕ
open import Data.Nat.DivMod using (nonZero)

infixl 7 _/_ _/suc_
record ℚ : Type where
  constructor _/suc_
  field
    num : ℤ
    den-pred : ℕ

  den : ℕ
  den = suc den-pred
open ℚ public

_/_ : (n : ℤ) → (d : ℕ) → ⦃ d≢0 : T (nonZero d) ⦄ → ℚ
n / suc d = n /suc d

{-# DISPLAY _/suc_ n d = n / suc d #-}

infixl 6 _+_
_+_ : ℚ → ℚ → ℚ
(x + y) .num = num x ℤ.* ⁺ (den y) ℤ.+ num y ℤ.* ⁺ (den x)
(x + y) .den-pred = x .den-pred ℕ.+ y .den-pred ℕ.+ x .den-pred ℕ.* y .den-pred

infixl 7 _*_
_*_ : ℚ → ℚ → ℚ
(x * y) .num = x .num ℤ.* y .num
(x * y) .den-pred = x .den-pred ℕ.+ y .den-pred ℕ.+ x .den-pred ℕ.* y .den-pred

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Permutation.Propositional.Properties
-- directly.
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Permutation.Inductive.Properties where

{-# WARNING_ON_IMPORT
"Data.List.Relation.Binary.Permutation.Inductive.Properties was deprecated in v1.1.
Use Data.List.Relation.Binary.Permutation.Propositional.Properties instead."
#-}

open import Data.List.Relation.Binary.Permutation.Propositional.Properties public


text:
-- This example comes from the discussion on Issue423.
module SolveNeutralApplication where

postulate
  A : Set
  a b : A
  T : A → Set
  mkT : ∀ a → T a

data Bool : Set where
  true false : Bool

f : Bool → A → A
f true x = a
f false x = b

-- We can solve the constraint
--   f x _4 == f x y
-- with
--   _4 := y
-- since the application of f is neutral.
g : (x : Bool)(y : A) → T (f x y)
g x y = mkT (f x _)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
-- ASR (31 December 2015). The error message for this test was changed
-- by fixing Issue 1763.

module Issue586 where

{-# NO_TERMINATION_CHECK #-}
Foo : Set
Foo = Foo

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-07-29, issue and test case by Nisse

{-# OPTIONS --profile=interactive #-}

A : Set
A = {!Set!} -- Give to provoke error

-- This issue concerns the AgdaInfo buffer,
-- the behavior on the command line might be different.

-- ERROR WAS (note the "Total 0ms"):
-- Set₁ != Set
-- when checking that the expression Set has type SetTotal 0ms

-- Expected:
-- Set₁ != Set
-- when checking that the expression Set has type Set

-- Issue2602.out:
-- ...
-- ((last . 1) . (agda2-goals-action '(0)))
-- (agda2-verbose "Total 0ms ")
-- (agda2-info-action "*Error*" "1,1-4 Set₁ != Set when checking that the expression Set has type Set" nil)
-- ...

max_stars_repo_name: sseefried/agda