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

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

open import segal.composition.l1
open import segal.preliminaries

IsWild₂ : ∀ {i} (𝓒 : Wild₁ i) → Set i
IsWild₂ 𝓒 = (x0 x1 x2 : obj 𝓒) → hom 𝓒 x1 x2 → hom 𝓒 x0 x1 → hom 𝓒 x0 x2

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

  Horn-2-1 = Σ X₀ λ x0 → Σ X₀ λ x1 → Σ X₀ λ x2 → (X₁ x0 x1) × (X₁ x1 x2)

  Spine-2 = Horn-2-1

  Boundary-2 = Σ X₀ λ x0 → Σ X₀ λ x1 → Σ X₀ λ x2 → (X₁ x0 x1) × (X₁ x0 x2) × (X₁ x1 x2)

  Filler₂ = (x0 x1 x2 : X₀) → X₁ x0 x1 → X₁ x0 x2 → X₁ x1 x2 → Set i

  SegalCondition₂ : Filler₂ → Set i
  SegalCondition₂ X₂ = (h : Horn-2-1) → let (x0 , x1 , x2 , x01 , x12) = h in
    contr (Σ (X₁ x0 x2) λ x02 → X₂ _ _ _ x01 x02 x12)

  IsSegal₂ : Set _
  IsSegal₂ = Σ Filler₂ SegalCondition₂

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

  is-segal-is-wild₂ : IsSegal₂ X ≅ IsWild₂ W
  is-segal-is-wild₂ = begin
         IsSegal₂ X
       ≅⟨ record { to = λ {(X₂ , hf₂) → λ x0 x1 x2 x01 x12 → (λ x02 → X₂ x0 x1 x2 x01 x02 x12)
                          , (hf₂ (x0 , x1 , x2 , x01 , x12)) }
                 ; from = λ t → (λ x0 x1 x2 x01 x02 x12 → proj₁ (t x0 x1 x2 x01 x12) x02) ,
                                (λ { (x0 , x1 , x2 , x01 , x12) → proj₂ (t x0 x1 x2 x01 x12) })
                 ; iso₁ = λ _ → refl
                 ; iso₂ = λ _ → refl } ⟩
         ( (x0 x1 x2 : X₀)(x01 : X₁ x0 x1)(x12 : X₁ x1 x2) →
           ( Σ (X₁ x0 x2 → Set i) λ Fill →
             contr (Σ (X₁ x0 x2) Fill) ) )
       ≅⟨ ( Π-ap-iso refl≅ λ x0 → Π-ap-iso refl≅ λ x1 → Π-ap-iso refl≅ λ x2 →
            Π-ap-iso refl≅ λ x01 → Π-ap-iso refl≅ λ x12 → contr-predicate) ⟩
            ( (x0 x1 x2 : X₀) → X₁ x0 x1 → X₁ x1 x2 → X₁ x0 x2 )
       ≅⟨ ( Π-ap-iso refl≅ λ x0 → Π-ap-iso refl≅ λ x1 → Π-ap-iso refl≅ λ x2 →
            Π-comm-iso ) ⟩
         IsWild₂ W
       ∎
       where open ≅-Reasoning

Wild₂ : (i : Level) → Set (lsuc i)
Wild₂ i = Σ (Wild₁ i) IsWild₂

module WildOps₂ {i} (W : Wild₂ i) where
  open Σ W renaming (proj₁ to 𝓒; proj₂ to assoc₀) public
  _∘_ : {a b c : obj 𝓒} → hom 𝓒 b c → hom 𝓒 a b → hom 𝓒 a c
  g ∘ f = assoc₀ _ _ _ g f

Segal₂ : (i : Level) → Set (lsuc i)
Segal₂ i = Σ (Segal₁ i) IsSegal₂

module SegalOps₂ {i} (X : Segal₂ i) where
  open Σ X renaming (proj₁ to X|1; proj₂ to sX₂) public
  open Segal₁ X|1 public
  open Σ sX₂ renaming (proj₁ to X₂; proj₂ to hf₂) public

  X₂' : {x0 x1 x2 : X₀} → X₁ x0 x1 → X₁ x0 x2 → X₁ x1 x2 → Set i
  X₂' x01 x02 x12 = X₂ _ _ _ x01 x02 x12

segal-wild₂ : ∀ {i} → Segal₂ i ≅ Wild₂ i
segal-wild₂ = Σ-ap-iso' segal-wild₁ is-segal-is-wild₂

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

  Δ² : Set i
  Δ² = Σ X₀ λ x0 → Σ X₀ λ x1 → Σ X₀ λ x2
     → Σ (X₁ x0 x1) λ x01
     → Σ (X₁ x0 x2) λ x02
     → Σ (X₁ x1 x2) λ x12
     → X₂' x01 x02 x12

  spine-Δ² : Spine-2 X|1 ≅ Δ²
  spine-Δ² = begin
      Spine-2 X|1
    ≅⟨ add-contr hf₂ ⟩
      ( Σ (Spine-2 X|1) λ { (x0 , x1 , x2 , x01 , x12)
        → ( Σ (X₁ x0 x2) λ x02 → X₂' x01 x02 x12 ) } )
    ≅⟨ record
         { to = λ {((x0 , x1 , x2 , x01 , x12) , x02 , x012)
                → (x0 , x1 , x2 , x01 , x02 , x12 , x012) }
         ; from = λ { (x0 , x1 , x2 , x01 , x02 , x12 , x012)
                  → ((x0 , x1 , x2 , x01 , x12) , x02 , x012) }
         ; iso₁ = λ _ → refl
         ; iso₂ = λ _ → refl } ⟩
      Δ²
    ∎
    where open ≅-Reasoning