{-# OPTIONS --without-K #-}
module segal.composition.l4 where

open import equality
open import hott.level
open import function.isomorphism
open import sum

open import segal.preliminaries
open import segal.composition.l1
open import segal.composition.l2
open import segal.composition.l3
open import segal.composition.l4.core

module _ {i}(W : Wild₃ i) where
  private X = invert≅ segal-wild₃ W

  open WildOps₃ W
  open SegalOps₃ X

  is-segal-is-wild₄ : IsSegal₄ X ≅ IsWild₄ W
  is-segal-is-wild₄ = begin
      IsSegal₄ X
    ≅⟨ record
         { to = λ { (X₄ , hf₄)
              → λ {(x0 , x1 , x2 , x3 , x4 , x01 , x02 , x03 , x04 ,
                     x12 , x13 , x14 , x23 , x24 , x34 , x012 , x013 ,
                     x014 , x023 , x024 , x034 , x123 , x124 , x134 ,
                     x234 , x0123 , x0124 , x0134 , x1234)
              → (λ x0234 → X₄ x0 x1 x2 x3 x4 x01 x02 x03 x04 x12 x13
                              x14 x23 x24 x34 x012 x013 x014 x023 x024
                              x034 x123 x124 x134 x234 x0123 x0124 x0134
                              x0234 x1234) ,
                 (hf₄ (x0 , x1 , x2 , x3 , x4 , x01 , x02 , x03 , x04 ,
                       x12 , x13 , x14 , x23 , x24 , x34 , x012 , x013 ,
                       x014 , x023 , x024 , x034 , x123 , x124 , x134 ,
                       x234 , x0123 , x0124 , x0134 , x1234)) } }
         ; from = λ t
                → ( λ x0 x1 x2 x3 x4 x01 x02 x03 x04 x12 x13 x14 x23 x24 x34 x012 x013
                      x014 x023 x024 x034 x123 x124 x134 x234 x0123 x0124 x0134 x0234 x1234
                    → proj₁ (t (x0 , x1 , x2 , x3 , x4 , x01 , x02 , x03 , x04 ,
                                x12 , x13 , x14 , x23 , x24 , x34 , x012 , x013 ,
                                x014 , x023 , x024 , x034 , x123 , x124 , x134 ,
                                x234 , x0123 , x0124 , x0134 , x1234)) x0234 ) ,
                   (λ h → proj₂ (t h))
         ; iso₁ = λ _ → refl
         ; iso₂ = λ _ → refl } ⟩
      ((h : Horn-4-1 X)
      → let (x0 , x1 , x2 , x3 , x4 , x01 , x02 , x03 , x04 , x12 , x13 ,
             x14 , x23 , x24 , x34 , x012 , x013 , x014 , x023 , x024 ,
             x034 , x123 , x124 , x134 , x234 , x0123 , x0124 , x0134 , x1234) = h
        in ( Σ (X₃' x023 x024 x034 x234 → Set i) λ Fill
        → contr (Σ _ Fill)))
    ≅⟨ (Π-ap-iso refl≅ λ _ → contr-predicate) ⟩
      ((h : Horn-4-1 X)
      → let (x0 , x1 , x2 , x3 , x4 , x01 , x02 , x03 , x04 , x12 , x13 ,
             x14 , x23 , x24 , x34 , x012 , x013 , x014 , x023 , x024 ,
             x034 , x123 , x124 , x134 , x234 , x0123 , x0124 , x0134 , x1234) = h
        in X₃' x023 x024 x034 x234 )
    ≅⟨ (Π-ap-iso (sym≅ (spine-horn₄ W)) λ s → refl≅) ⟩
      ((s : Spine-4 X) → let (x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34) = s
        in X₃' (assoc₁ x01 x12 x23) (assoc₁ x01 x12 (x34 ∘ x23))
               (assoc₁ x01 (x23 ∘ x12) x34 · ap (λ u → u ∘ x01) (assoc₁ x12 x23 x34) · refl)
               refl )
    ≅⟨ refl≅ ⟩
      ((s : Spine-4 X) → let (x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34) = s
        in sym (ap (λ u → x34 ∘ u) (assoc₁ x01 x12 x23)) ·
           assoc₁ (x12 ∘ x01) x23 x34 · refl · assoc₁ x01 x12 (x34 ∘ x23)
           ≡ assoc₁ x01 (x23 ∘ x12) x34 · ap (λ u → u ∘ x01) (assoc₁ x12 x23 x34) · refl)
    ≅⟨ (Π-ap-iso refl≅ λ {(x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34)
         → lem (ap (λ u → x34 ∘ u) (assoc₁ x01 x12 x23)) _ _ _ _ } ) ⟩
      ((s : Spine-4 X) → let (x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34) = s
        in assoc₁ (x12 ∘ x01) x23 x34 · assoc₁ x01 x12 (x34 ∘ x23)
        ≡ ap (λ u → x34 ∘ u) (assoc₁ x01 x12 x23) · assoc₁ x01 (x23 ∘ x12) x34 ·
          ap (λ u → u ∘ x01) (assoc₁ x12 x23 x34))
    ≅⟨ record
         { to = λ t → λ {x0}{x1}{x2}{x3}{x4} x01 x12 x23 x34
              → t ((x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34))
         ; from = λ t → λ { (x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34)
                → t x01 x12 x23 x34 }
         ; iso₁ = λ _ → refl
         ; iso₂ = λ _ → refl } ⟩
      IsWild₄ W
    ∎
    where
      open ≅-Reasoning

      lem : ∀ {j}{A : Set j}{a b c d e : A}
          → (p : a ≡ b)(t : b ≡ c)(s : c ≡ d)
          → (q : a ≡ e)(r : e ≡ d)
          → (sym p · q · refl · r ≡ t · s · refl)
          ≅ (q · r ≡ p · t · s)
      lem refl refl refl refl r = refl≅