{-# OPTIONS --without-K #-}
module segal.identities.l3 where

open import equality
open import function.extensionality
open import function.isomorphism
open import sum

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

module _ {i} (W : Wild₃ i) where
  open WildOps₃ W
  record HasId₃' (Wid : HasId₂ W|2) : Set i where
    constructor mk-id₃'
    open HasId₂ Wid
    field
      id-coh : (x y z : obj 𝓒)
             → (f : hom 𝓒 x y) (g : hom 𝓒 y z)
             → assoc₁ f (id y) g
             · ap (λ u → u ∘ f) (id-ρ _ _ g)
             ≡ ap (λ u → g ∘ u) (id-λ _ _ f)

  record HasId₃ : Set i where
    constructor mk-id₃
    field
      has-id₂ : HasId₂ W|2
      has-id₃' : HasId₃' has-id₂
    open HasId₃' has-id₃' public

module _ {i} (X : Segal₃ i) where
  open SegalOps₃ X
  record HasDeg₃' (Xdeg : HasDeg₂ X|2) : Set i where
    constructor mk-deg₃'
    open HasDeg₂ Xdeg

    field
      s21 : (s : Δ² X|2)
          → let (x0 , x1 , x2 , x01 , x02 , x12 , x012) = s
         in X₃' (s11 (x0 , x1 , x01)) x012 x012 (s10 (x1 , x2 , x12))

  record HasDeg₃ : Set i where
    constructor mk-deg₃
    field
      has-deg₂ : HasDeg₂ X|2
      has-deg₃' : HasDeg₃' has-deg₂

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

  module _ {Wid : HasId₂ W|2} where
    private Xdeg = invert≅ deg-id₂ Wid
    open HasId₂ Wid
    open HasDeg₂ Xdeg

    deg-id₃' : HasDeg₃' X Xdeg ≅ HasId₃' W Wid
    deg-id₃' = begin
        HasDeg₃' X Xdeg
      ≅⟨ record
           { to = λ { (mk-deg₃' coh) → coh }
           ; from = mk-deg₃'
           ; iso₁ = λ _ → refl
           ; iso₂ = λ _ → refl } ⟩
        ( (x : Δ² X|2)
        → let (x0 , x1 , x2 , x01 , x02 , x12 , x012) = x
        in X₃' (s11 (x0 , x1 , x01)) x012 x012 (s10 (x1 , x2 , x12)) )
      ≅⟨ (Π-ap-iso (sym≅ (spine-Δ² X|2)) λ _ → refl≅ ) ⟩
        ( (s : Spine-2 X|1)
        → let (x0 , x1 , x2 , x01 , x12) = s
        in X₃' (s11 (x0 , x1 , x01)) refl refl (s10 (x1 , x2 , x12)) )
      ≅⟨ record
           { to = λ coh → λ x y z f g → coh (x , y , z , f , g)
           ; from = λ coh → λ { (x , y , z , f , g) → coh x y z f g }
           ; iso₁ = λ _ → refl
           ; iso₂ = λ _ → refl } ⟩
        ( (x y z : obj 𝓒)
        → (f : hom 𝓒 x y)(g : hom 𝓒 y z)
        → ( sym (ap (λ u → g ∘ u) (id-λ _ _ f))
         · assoc₁ f (id y) g
         · ap (λ u → u ∘ f) (id-ρ _ _ g)
         · refl
         ≡ refl ) )
      ≅⟨ ( Π-ap-iso refl≅ λ x
         → Π-ap-iso refl≅ λ y
         → Π-ap-iso refl≅ λ z
         → Π-ap-iso refl≅ λ f
         → Π-ap-iso refl≅ λ g
         → lem₁ (assoc₁ f (id y) g)
                 (ap (λ u → u ∘ f) (id-ρ _ _ g))
                 (ap (λ u → g ∘ u) (id-λ _ _ f))
                 refl
         ·≅ lem₂ _ _
                 ) ⟩
        ( (x y z : obj 𝓒)
        → (f : hom 𝓒 x y)(g : hom 𝓒 y z)
        → ( assoc₁ f (id y) g
          · ap (λ u → u ∘ f) (id-ρ _ _ g)
          ≡ ap (λ u → g ∘ u) (id-λ _ _ f) ) )
      ≅⟨ record
           { to = mk-id₃'
           ; from = λ { (mk-id₃' coh) → coh }
           ; iso₁ = λ _ → refl
           ; iso₂ = λ _ → refl } ⟩
        HasId₃' W Wid
      ∎
      where
        open ≅-Reasoning
        lem₁ : ∀ {j}{A : Set j}
             → {a b c d : A}
             → (p : a ≡ b)(q : b ≡ c)(r : a ≡ d)(s : d ≡ c)
             → (sym r · p · q · refl ≡ s)
             ≅ (p · q ≡ r · s)
        lem₁ refl refl refl s = refl≅

        lem₂ : ∀ {j}{A : Set j}
             → {a b : A}
             → (p q : a ≡ b)
             → (p ≡ q · refl)
             ≅ (p ≡ q)
        lem₂ p refl = refl≅

  deg-id₃ : HasDeg₃ X ≅ HasId₃ W
  deg-id₃ = begin
      HasDeg₃ X
    ≅⟨ record
         { to = λ { (mk-deg₃ a b) → (a , b) }
         ; from = λ { (a , b) → mk-deg₃ a b }
         ; iso₁ = λ _ → refl
         ; iso₂ = λ _ → refl } ⟩
      ( Σ (HasDeg₂ X|2) (HasDeg₃' X) )
    ≅⟨ (Σ-ap-iso' deg-id₂ (λ _ → deg-id₃')) ⟩
      ( Σ (HasId₂ W|2) (HasId₃' W) )
    ≅⟨ record
         { to = λ { (a , b) → mk-id₃ a b }
         ; from = λ { (mk-id₃ a b) → (a , b) }
         ; iso₁ = λ _ → refl
         ; iso₂ = λ _ → refl } ⟩
      HasId₃ W
    ∎
    where open ≅-Reasoning