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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Unit
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.NType2

open import lib.types.PathSeq

open import nicolai.pseudotruncations.Liblemmas
open import nicolai.pseudotruncations.SeqColim


open import nicolai.pseudotruncations.wconst-preparation

module nicolai.pseudotruncations.heptagon
  {i} {C : Sequence {i}} (wc : wconst-chain C) (a₀ : fst C O) where

  {- î-def is defined in this module: -}
  open wconst-init {i} {C} wc a₀
  
  module _ (n : ℕ) (a : A n) where

    {- Let us formulate different simplification steps of the 
       heptagon. -}

    full-hepta : seq-loop (ins (S n) (f n a)) 
    full-hepta = (î-def (S n) (f n a)) ⋯ (‼ (î-def n a) ⋯ toSeq (glue n a))

    remove-g : seq-loop (ins (S n) (f n a)) 
    remove-g = (î-def (S n) (f n a))
               ⋯ ‼ (ins (S n) (f n a)
                      =⟪ ap (ins (S n)) (wc n _ _) ⟫
                    ins (S n) (lift-point C a₀ (S n)) 
                      =⟪ ! (lift-point-= C a₀ (S n)) ⟫
                    ins O a₀
                      ∎∎)

    simplify-‼ : seq-loop (ins (S n) (f n a)) 
    simplify-‼ = (î-def (S n) (f n a))
               ⋯ (ins O a₀
                    =⟪ lift-point-= C a₀ (S n) ⟫
                  ins (S n) (lift-point C a₀ (S n)) 
                    =⟪ ! (ap (ins (S n)) (wc n _ _)) ⟫
                  ins (S n) (f n a)
                    ∎∎)

    simplify-one-g : seq-loop (ins {C = C} (S n) (f n a))
    simplify-one-g =
                  ins (S n) (f n a)
                    =⟪ glue (S n) (f n a) ⟫
                  ins (S (S n)) (f (S n) (f n a))
                    =⟪ ap (ins (S (S n))) (wc (S n) (f n a) (lift-point C a₀ (S n))) ⟫
                  ins (S (S n)) (lift-point C a₀ (S (S n)))
                    =⟪ ! (glue (S n) (lift-point C a₀ (S n))) ⟫
                  ins (S n) (lift-point C a₀ (S n))
                    =⟪ ! (lift-point-= C a₀ (S n)) ⟫
                  ins O a₀
                    =⟪ lift-point-= C a₀ (S n) ⟫
                  ins (S n) (lift-point C a₀ (S n))
                    =⟪ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n))) ⟫
                  ins (S n) (f n a)
                    ∎∎

    simplify-many-g : seq-loop (ins {C = C} (S n) (f n a))
    simplify-many-g =
                  ins (S n) (f n a)
                    =⟪ glue (S n) (f n a) ⟫
                  ins (S (S n)) (f (S n) (f n a))
                    =⟪ ap (ins (S (S n))) (wc (S n) (f n a) (lift-point C a₀ (S n))) ⟫
                  ins (S (S n)) (lift-point C a₀ (S (S n)))
                    =⟪ ! (glue (S n) (lift-point C a₀ (S n))) ⟫
                  ins (S n) (lift-point C a₀ (S n))
                    =⟪ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n))) ⟫
                  ins (S n) (f n a)
                    ∎∎

    replace-ap-SSn : seq-loop (ins {C = C} (S n) (f n a))
    replace-ap-SSn =
                  ins (S n) (f n a)
                    =⟪ glue (S n) (f n a) ⟫
                  ins (S (S n)) (f (S n) (f n a))
                    =⟪ ap (ins (S (S n))) (ap (f (S n)) (wc n a (lift-point C a₀ n))) ⟫
                  ins (S (S n)) (lift-point C a₀ (S (S n)))
                    =⟪ ! (glue (S n) (lift-point C a₀ (S n))) ⟫
                  ins (S n) (lift-point C a₀ (S n))
                    =⟪ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n))) ⟫
                  ins (S n) (f n a)
                    ∎∎

    {-
      Now, let us generalize:
        x   for   f n a 
        y   for   lift-point C a₀ (S n) 
        q   for   wc n a (lift C a₀ n)
      Then, we can show that the square commutes by induction on q.
    -}
    generalize-square : (x y : A (S n)) (q : x == y)
              → (↯ 
                  ins {C = C} (S n) x
                    =⟪ glue (S n) x ⟫
                  ins (S (S n)) (f (S n) x)
                    =⟪ ap (ins (S (S n))) (ap (f (S n)) q) ⟫
                  ins (S (S n)) (f (S n) y)
                    =⟪ ! (glue (S n) y) ⟫
                  ins (S n) y
                    =⟪ ! (ap (ins (S n)) q) ⟫
                  ins (S n) x
                    ∎∎
               ) == idp
    generalize-square x .x idp = 
                  glue (S n) x ∙ ! (glue (S n) x) ∙ idp
                    =⟨ ap (λ q → (glue (S n) x) ∙ q) (∙-unit-r _) ⟩
                  glue (S n) x ∙ ! (glue (S n) x)
                    =⟨ !-inv-r (glue (S n) x) ⟩
                  idp
                    ∎ 

    {- Let us use some ad-hoc lemmas; these could all be done via
       very tedious concatenations of library lemmas.
       Of course, our ad-hoc way is somewhat ugly, but it saves a
       lot of work compared to using concatenations and nestings of
       library lemmas. The strategy is to formulate the equality 
       that we need and solve it by trivial path induction.

       This ad-hoc approach is surely not the best way one can 
       think of. 
       The best way to do it would probably be a more principled 
       approach with more powerful high-level lemmas that allow the
       manipulation of paths; however, such a technology is not
       implemented so far. -}
    adhoc-!-∙ : ∀ {i} {X : Type i} {x y z u v w o : X}
                         (p : x == y) (q : y == z) (r : u == z)
                         (s : v == u) (t : v == w) (l : w == o)
                         → (↯ x =⟪ p ⟫ y =⟪ q ⟫ z =⟪ ! (s ∙ r) ⟫ v =⟪ t ⟫ w =⟪ l ⟫ o ∎∎ )
                           ==
                           (↯ x =⟪ p ⟫ y =⟪ q ⟫ z =⟪ ! r ⟫ u =⟪ ! s ⟫ v =⟪ t ⟫ w =⟪ l ⟫ o ∎∎)
    adhoc-!-∙ idp idp idp idp idp idp = idp


    adhoc-cancel-inv : ∀ {i} {X : Type i} {x y z u v w : X}
                         (p : x == y) (q : y == z) (r : z == u)
                         (s : v == u) (t : u == w)
                         → (↯ x =⟪ p ⟫ y =⟪ q ⟫ z =⟪ r ⟫ u =⟪ ! s ⟫ v =⟪ s ⟫ u =⟪ t ⟫ w ∎∎ )
                           ==
                           (↯ x =⟪ p ⟫ y =⟪ q ⟫ z =⟪ r ⟫ u =⟪ t ⟫ w ∎∎)
    adhoc-cancel-inv idp idp idp idp idp = idp


    {- Now, we are ready to show that the heptagon is trivial! -}
    ĝ-def :  (↯ full-hepta) == idp
    ĝ-def = 

      (↯ full-hepta)

        =⟨ ap (λ q → (glue (S n) (f n a))
                   ∙ ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n)))
                   ∙ ! ((lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
                        ∙ glue (S n) (snd C n (lift-point C a₀ n)))
                   ∙ ! (! (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n)))
                   ∙ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))
                   ∙ q )
              (!-inv-l (glue n a)) ⟩

      (↯ (remove-g ⋯ (toSeq idp)))

        =⟨ ap (λ q → (glue (S n) (f n a))
                    ∙ ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n)))
                    ∙ ! ((lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
                    ∙ glue (S n) (snd C n (lift-point C a₀ n)))
                    ∙ ! (! (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n)))
                    ∙ q )
              (∙-unit-r (! (ap (ins (S n)) (wc n a (lift-point C a₀ n))))) ⟩
      (↯ remove-g)

        =⟨ ap (λ q → (glue (S n) (f n a))
                    ∙ ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n)))
                    ∙ ! ((lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
                    ∙ glue (S n) (snd C n (lift-point C a₀ n)))
                    ∙ q
                    ∙ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))
               )
               (!-! (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))) ⟩

      (↯ simplify-‼) 

        =⟨ adhoc-!-∙
              (glue (S n) (f n a))
              (ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n))))
              (glue (S n) (snd C n (lift-point C a₀ n)))
              (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
              (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
              (! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))) ⟩
      (↯ simplify-one-g) 
        =⟨ adhoc-cancel-inv
             (glue (S n) (f n a))
             (ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n))))
             (! (glue (S n) (snd C n (lift-point C a₀ n))))
             (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
             (! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))) ⟩

      (↯ simplify-many-g) 

        =⟨ ap (λ q → (glue (S n) (f n a))
                    ∙ q
                    ∙ ! (glue (S n) (snd C n (lift-point C a₀ n)))
                    ∙ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))
               )
               (ap-wconst (ins (S (S n)))
                          (ins-wconst (S (S n)))
                          (wc (S n) (f n a) (snd C n (lift-point C a₀ n)))
                          (ap (f (S n)) (wc n a (lift-point C a₀ n)))
               ) ⟩

      (↯ replace-ap-SSn) 

        =⟨ generalize-square (f n a) (lift-point C a₀ (S n)) (wc n a (lift-point C a₀ n)) ⟩

      idp
        ∎