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

open import equality
open import function.isomorphism
open import sum

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

module _ {i} (W : Wild₂ i) where
  open WildOps₂ W
  record HasId₂' (Wid : HasId₁ 𝓒) : Set i where
    constructor mk-id₂'
    open HasId₁ Wid public
    field
      id-λ : (x y : obj 𝓒)(f : hom 𝓒 x y) → id y ∘ f ≡ f
      id-ρ : (x y : obj 𝓒)(f : hom 𝓒 x y) → f ∘ id x ≡ f

  record HasId₂ : Set i where
    constructor mk-id₂
    field
      has-id₁ : HasId₁ 𝓒
      has-id₂' : HasId₂' has-id₁
    open HasId₂' has-id₂' public

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

  record HasDeg₂' (Xdeg : HasDeg₁ X|1) : Set i where
    constructor mk-deg₂'
    open HasDeg₁ Xdeg public
    field
      s10 : (s : Δ¹ X|1)
          → let (x0 , x1 , x01) = s
         in X₂' (s00 x0) x01 x01
      s11 : (s : Δ¹ X|1)
          → let (x0 , x1 , x01) = s
         in X₂' x01 x01 (s00 x1)

  record HasDeg₂ : Set i where
    constructor mk-deg₂
    field
      has-deg₁ : HasDeg₁ X|1
      has-deg₂' : HasDeg₂' has-deg₁
    open HasDeg₂' has-deg₂' public

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

  module _ {Wid : HasId₁ 𝓒} where
    private Xdeg = invert≅ deg-id₁ Wid
    open HasId₁ Wid
    open HasDeg₁ Xdeg

    deg-id₂' : HasDeg₂' X Xdeg ≅ HasId₂' W Wid
    deg-id₂' = record
      { to = λ { (mk-deg₂' s10 s11) → record
                    { id-λ = λ x y f → s11 (x , y , f)
                    ; id-ρ = λ x y f → s10 (x , y , f) } }
      ; from = λ { (mk-id₂' id-λ id-ρ) → record
                    { s10 = λ { (x0 , x1 , x01) → id-ρ x0 x1 x01 }
                    ; s11 = λ { (x0 , x1 , x01) → id-λ x0 x1 x01 } } }
      ; iso₁ = λ _ → refl
      ; iso₂ = λ _ → 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|1) (HasDeg₂' X) )
    ≅⟨ (Σ-ap-iso' deg-id₁ (λ _ → deg-id₂')) ⟩
      ( Σ (HasId₁ 𝓒) (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