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

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

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

module _ {i} (W : Wild₃ i) where
  open WildOps₃ W

  IsWild₄ : Set i
  IsWild₄ = {a b c d e : obj 𝓒}
          → (f : hom 𝓒 a b) → (g : hom 𝓒 b c)
          → (h : hom 𝓒 c d) → (k : hom 𝓒 d e)
          → assoc₁ (g ∘ f) h k · assoc₁ f g (k ∘ h)
          ≡ ap (λ u → k ∘ u) (assoc₁ f g h)
              · assoc₁ f (h ∘ g) k
              · ap (λ u → u ∘ f) (assoc₁ g h k)

module _ {i} (X : Segal₃ i) where
  open SegalOps₃ X

  Horn-4-1 = Σ X₀ λ x0 → Σ X₀ λ x1 → Σ X₀ λ x2 → Σ X₀ λ x3 → Σ X₀ λ x4
           → Σ (X₁ x0 x1) λ x01 → Σ (X₁ x0 x2) λ x02
           → Σ (X₁ x0 x3) λ x03 → Σ (X₁ x0 x4) λ x04
           → Σ (X₁ x1 x2) λ x12 → Σ (X₁ x1 x3) λ x13
           → Σ (X₁ x1 x4) λ x14 → Σ (X₁ x2 x3) λ x23
           → Σ (X₁ x2 x4) λ x24 → Σ (X₁ x3 x4) λ x34
           → Σ (X₂' x01 x02 x12) λ x012 → Σ (X₂' x01 x03 x13) λ x013
           → Σ (X₂' x01 x04 x14) λ x014 → Σ (X₂' x02 x03 x23) λ x023
           → Σ (X₂' x02 x04 x24) λ x024 → Σ (X₂' x03 x04 x34) λ x034
           → Σ (X₂' x12 x13 x23) λ x123 → Σ (X₂' x12 x14 x24) λ x124
           → Σ (X₂' x13 x14 x34) λ x134 → Σ (X₂' x23 x24 x34) λ x234
           → X₃' x012 x013 x023 x123 × X₃' x012 x014 x024 x124
           × X₃' x013 x014 x034 x134 × X₃' x123 x124 x134 x234

  Spine-4 = Σ X₀ λ x0 → Σ X₀ λ x1 → Σ X₀ λ x2 → Σ X₀ λ x3 → Σ X₀ λ x4
          → X₁ x0 x1 × X₁ x1 x2 × X₁ x2 x3 × X₁ x3 x4

  Filler₄ = (x0 x1 x2 x3 x4 : X₀)
           → (x01 : X₁ x0 x1) (x02 : X₁ x0 x2)
           → (x03 : X₁ x0 x3) (x04 : X₁ x0 x4)
           → (x12 : X₁ x1 x2) (x13 : X₁ x1 x3)
           → (x14 : X₁ x1 x4) (x23 : X₁ x2 x3)
           → (x24 : X₁ x2 x4) (x34 : X₁ x3 x4)
           → (x012 : X₂' x01 x02 x12) (x013 : X₂' x01 x03 x13)
           → (x014 : X₂' x01 x04 x14) (x023 : X₂' x02 x03 x23)
           → (x024 : X₂' x02 x04 x24) (x034 : X₂' x03 x04 x34)
           → (x123 : X₂' x12 x13 x23) (x124 : X₂' x12 x14 x24)
           → (x134 : X₂' x13 x14 x34) (x234 : X₂' x23 x24 x34)
           → X₃' x012 x013 x023 x123 → X₃' x012 x014 x024 x124
           → X₃' x013 x014 x034 x134 → X₃' x023 x024 x034 x234
           → X₃' x123 x124 x134 x234 → Set i

  SegalCondition₄ : Filler₄ → Set _
  SegalCondition₄ X₄ = (h : Horn-4-1)
    → 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 contr (Σ (X₃' x023 x024 x034 x234) λ x0234
        → X₄ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
             x0123 x0124 x0134 x0234 x1234)

  IsSegal₄ : Set (lsuc i)
  IsSegal₄ = Σ Filler₄ SegalCondition₄

private
  module spine-horn-iso-tmp {i} (X : Segal₃ i) where
    open SegalOps₃ X

    spine-horn₄ : Spine-4 X ≅ Horn-4-1 X
    spine-horn₄ = begin
        Spine-4 X
      ≅⟨ add-contr (λ {(x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34)
        → Σ-contr (hf₂ (x1 , x2 , x3 , x12 , x23)) λ { (x13 , x123)
        → Σ-contr (hf₂ (x2 , x3 , x4 , x23 , x34)) λ { (x24 , x234)
        → Σ-contr (hf₂ (x1 , x2 , x4 , x12 , x24)) λ { (x14 , x124)
        → Σ-contr (hf₃ (x1 , x2 , x3 , x4 ,
                        x12 , x13 , x14 , x23 , x24 , x34 ,
                        x123 , x124 , x234)) λ { (x134 , x1234)
        → Σ-contr (hf₂ (x0 , x1 , x2 , x01 , x12)) λ { (x02 , x012)
        → Σ-contr (hf₂ (x0 , x1 , x3 , x01 , x13)) λ { (x03 , x013)
        → Σ-contr (hf₂ (x0 , x1 , x4 , x01 , x14)) λ { (x04 , x014)
        → Σ-contr (hf₃ (x0 , x1 , x2 , x3 ,
                        x01 , x02 , x03 , x12 , x13 , x23 ,
                        x012 , x013 , x123)) λ { (x023 , x0123)
        → Σ-contr (hf₃ (x0 , x1 , x2 , x4 ,
                        x01 , x02 , x04 , x12 , x14 , x24 ,
                        x012 , x014 , x124)) λ { (x024 , x0124)
        →  (hf₃ (x0 , x1 , x3 , x4 ,
                  x01 , x03 , x04 , x13 , x14 , x34 ,
                  x013 , x014 , x134)) } } } } } } } } } }) ⟩
        ( Σ (Spine-4 X) λ s
        → let (x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34) = s
        in Σ (Σ (X₁ x1 x3) λ x13 → X₂' x12 x13 x23) λ { (x13 , x123)
        → Σ (Σ (X₁ x2 x4) λ x24 → X₂' x23 x24 x34) λ { (x24 , x234)
        → Σ (Σ (X₁ x1 x4) λ x14 → X₂' x12 x14 x24) λ { (x14 , x124)
        → Σ (Σ (X₂' x13 x14 x34) λ x134 → X₃' x123 x124 x134 x234) λ { (x134 , x1234)
        → Σ (Σ (X₁ x0 x2) λ x02 → X₂' x01 x02 x12) λ { (x02 , x012)
        → Σ (Σ (X₁ x0 x3) λ x03 → X₂' x01 x03 x13) λ { (x03 , x013)
        → Σ (Σ (X₁ x0 x4) λ x04 → X₂' x01 x04 x14) λ { (x04 , x014)
        → Σ (Σ (X₂' x02 x03 x23) λ x023 → X₃' x012 x013 x023 x123) λ { (x023 , x0123)
        → Σ (Σ (X₂' x02 x04 x24) λ x024 → X₃' x012 x014 x024 x124) λ { (x024 , x0124)
        → (Σ (X₂' x03 x04 x34) λ x034 → X₃' x013 x014 x034 x134) } } } } } } } } } )
      ≅⟨ record
          { to = λ { ((x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34) ,
                      (x13 , x123) , (x24 , x234) , (x14 , x124) , (x134 , x1234) ,
                      (x02 , x012) , (x03 , x013) , (x04 , x014) , (x023 , x0123) ,
                      (x024 , x0124) , (x034 , x0134))
                  → (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 = λ { (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)
                    → ((x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34) ,
                      (x13 , x123) , (x24 , x234) , (x14 , x124) , (x134 , x1234) ,
                      (x02 , x012) , (x03 , x013) , (x04 , x014) , (x023 , x0123) ,
                      (x024 , x0124) , (x034 , x0134)) }
          ; iso₁ = λ _ → refl
          ; iso₂ = λ _ → refl } ⟩
        Horn-4-1 X
      ∎ where open ≅-Reasoning

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

  private
    module spine-horn-tmp where
      open spine-horn-iso-tmp

      f : Spine-4 X → Horn-4-1 X
      f (x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34) =
        (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)
        where
          lem : ∀ {i}{A : Set i}{a b : A}{p : a ≡ b}
              → p · refl · refl ≡ p
          lem {p = refl} = refl

          x02 = x12 ∘ x01; x012 = refl
          x13 = x23 ∘ x12; x123 = refl
          x24 = x34 ∘ x23; x234 = refl
          x03 = x13 ∘ x01; x013 = refl
          x14 = x24 ∘ x12; x124 = refl
          x04 = x14 ∘ x01; x014 = refl
          x134 = assoc₁ x12 x23 x34; x1234 = lem
          x023 = assoc₁ x01 x12 x23; x0123 = lem
          x024 = assoc₁ x01 x12 x24; x0124 = lem
          x034 = assoc₁ x01 x13 x34 · ap (λ u → u ∘ x01) x134 · x014; x0134 = refl

      g : Horn-4-1 X → Spine-4 X
      g (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) =
        (x0 , x1 , x2 , x3 , x4 , x01 , x12 , x23 , x34)

      α : (s : Spine-4 X) → g (f s) ≡ s
      α s = refl

      β : (h : Horn-4-1 X) → f (g h) ≡ h
      β h = iso⇒inj (sym≅ (spine-horn₄ X)) refl

  spine-horn₄ : Spine-4 X ≅ Horn-4-1 X
  spine-horn₄ = iso f g α β
    where
      open spine-horn-tmp