open import Cubical.Foundations.Prelude hiding (Sub)
open import Cubical.Foundations.Equiv.Base
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels
open import Cubical.Data.Unit
open import Cubical.Data.Empty.Base
import Cubical.Data.Equality.Base as E
open import Cubical.Data.Equality.Conversion

module TT.Groupoid.NTy (X : hSet ℓ-zero) (Y : X .fst → hSet ℓ-zero) where

open import TT.Groupoid.Syntax X Y
open import TT.Groupoid.TyElimSet X Y

private variable
  Γ Δ Θ Ξ : Con

data NTy : Con → Type
⌜_⌝ : NTy Γ → Ty Γ

data NTy where
  U : NTy Γ
  El : Tm Γ U → NTy Γ
  Π : (Aᴺ : NTy Γ) → NTy (Γ ▹ ⌜ Aᴺ ⌝) → NTy Γ

⌜ U ⌝ = U
⌜ El  ⌝ = El Â
⌜ Π Aᴺ Bᴺ ⌝ = Π ⌜ Aᴺ ⌝ ⌜ Bᴺ ⌝

private variable
  A₀ᴺ A₁ᴺ B₀ᴺ B₁ᴺ : NTy Γ

module NTyPath where
  substDep : A₀ᴺ E.≡ A₁ᴺ → NTy (Γ ▹ ⌜ A₀ᴺ ⌝) → NTy (Γ ▹ ⌜ A₁ᴺ ⌝)
  substDep E.refl Bᴺ = Bᴺ

  Cover : NTy Γ → NTy Γ → Type
  decode : (A₀ᴺ A₁ᴺ : NTy Γ) → Cover A₀ᴺ A₁ᴺ → A₀ᴺ E.≡ A₁ᴺ
  decode-Π₁ :
    (A₀₁ᴺ : A₀ᴺ E.≡ A₁ᴺ) →
    Cover (substDep A₀₁ᴺ B₀ᴺ) B₁ᴺ → Π A₀ᴺ B₀ᴺ E.≡ Π A₁ᴺ B₁ᴺ

  Cover U U = Unit
  Cover (El Â₀) (El Â₁) = Â₀ E.≡ Â₁
  Cover (Π A₀ᴺ B₀ᴺ) (Π A₁ᴺ B₁ᴺ) =
    Σ[ A₀₁ᴺ ∈ Cover A₀ᴺ A₁ᴺ ] Cover (substDep (decode A₀ᴺ A₁ᴺ A₀₁ᴺ) B₀ᴺ) B₁ᴺ
  {-# CATCHALL #-}
  Cover _ _ = ⊥

  decode U U tt = E.refl
  decode (El Â₀) (El Â₁) E.refl = E.refl
  decode (Π A₀ᴺ B₀ᴺ) (Π A₁ᴺ B₁ᴺ) (A₀₁ᴺ , B₀₁ᴺ) =
    decode-Π₁ (decode A₀ᴺ A₁ᴺ A₀₁ᴺ) B₀₁ᴺ

  decode-Π₁ E.refl B₀₁ᴺ = E.ap (Π _) (decode _ _ B₀₁ᴺ)

  reflCode : (Aᴺ : NTy Γ) → Cover Aᴺ Aᴺ
  decodeRefl : (Aᴺ : NTy Γ) → decode Aᴺ Aᴺ (reflCode Aᴺ) ≡ E.refl

  reflCode U = tt
  reflCode (El Â) = E.refl
  reflCode (Π Aᴺ Bᴺ) = reflCode Aᴺ , filler i1
    module reflCode-Π where
    filler : (i : I) → Cover (substDep (decodeRefl Aᴺ (~ i)) Bᴺ) Bᴺ
    filler i =
      transport⁻-filler
        (λ i → Cover (substDep (decodeRefl Aᴺ i) Bᴺ) Bᴺ)
        (reflCode Bᴺ)
        i

  decodeRefl U = refl
  decodeRefl (El Â) = refl
  decodeRefl (Π Aᴺ Bᴺ) =
    (λ i → decode-Π₁ (decodeRefl Aᴺ i) (reflCode-Π.filler Aᴺ Bᴺ (~ i))) ∙
    cong (E.ap (Π Aᴺ)) (decodeRefl Bᴺ)

  encode : (A₀ᴺ A₁ᴺ : NTy Γ) → A₀ᴺ E.≡ A₁ᴺ → Cover A₀ᴺ A₁ᴺ
  encode A₀ᴺ .A₀ᴺ E.refl = reflCode A₀ᴺ

  decodeEncode :
    (A₀ᴺ A₁ᴺ : NTy Γ) (A₀₁ᴺ : A₀ᴺ E.≡ A₁ᴺ) →
    decode A₀ᴺ A₁ᴺ (encode A₀ᴺ A₁ᴺ A₀₁ᴺ) ≡ A₀₁ᴺ
  decodeEncode A₀ᴺ .A₀ᴺ E.refl = decodeRefl A₀ᴺ

  isPropCover : (A₀ᴺ A₁ᴺ : NTy Γ) → isProp (Cover A₀ᴺ A₁ᴺ)
  isPropCover U U = isPropUnit
  isPropCover (El Â₀) (El Â₁) =
    isOfHLevelRetractFromIso  (invIso PathIsoEq) (isSetTm _ U Â₀ Â₁)
  isPropCover (Π A₀ᴺ B₀ᴺ) (Π A₁ᴺ B₁ᴺ) =
    isPropΣ (isPropCover A₀ᴺ A₁ᴺ) λ A₀₁ᴺ →
      isPropCover (substDep (decode A₀ᴺ A₁ᴺ A₀₁ᴺ) B₀ᴺ) B₁ᴺ

isSetNTy : (Γ : Con) → isSet (NTy Γ)
isSetNTy Γ A₀ᴺ A₁ᴺ =
  isPropRetract
    (λ A₀₁ᴺ → encode A₀ᴺ A₁ᴺ (pathToEq A₀₁ᴺ))
    (λ A₀₁ᴺ → eqToPath (decode A₀ᴺ A₁ᴺ A₀₁ᴺ))
    (λ A₀₁ᴺ →
      cong eqToPath (decodeEncode A₀ᴺ A₁ᴺ (pathToEq A₀₁ᴺ)) ∙
      eqToPath-pathToEq A₀₁ᴺ)
    (isPropCover A₀ᴺ A₁ᴺ)
  where
  open NTyPath

infixl  _[_]ᵀᴺ
_[_]ᵀᴺ : NTy Γ → Sub Δ Γ → NTy Δ
⌜⌝-[] : (Aᴺ : NTy Γ) (γ : Sub Δ Γ) → ⌜ Aᴺ ⌝ [ γ ]ᵀ ≡ ⌜ Aᴺ [ γ ]ᵀᴺ ⌝

U [ γ ]ᵀᴺ = U
El  [ γ ]ᵀᴺ = El ( [ γ ]ᵘ)
Π Aᴺ Bᴺ [ γ ]ᵀᴺ = Π (Aᴺ [ γ ]ᵀᴺ) (filler i1)
  module []ᵀᴺ-Π where
  filler : (i : I) → NTy (_ ▹ ⌜⌝-[] Aᴺ γ i)
  filler i = transport-filler (λ i → NTy (_ ▹ ⌜⌝-[] Aᴺ γ i)) (Bᴺ [ γ ⁺ ]ᵀᴺ) i

⌜⌝-[] U γ = U-[] γ
⌜⌝-[] (El Â) γ = El-[] Â γ
⌜⌝-[] (Π Aᴺ Bᴺ) γ = λ i → filler i1 i
  module ⌜⌝-[]-Π where
  filler : I → I → Ty _
  filler j i =
    doubleCompPath-filler
      (Π-[] ⌜ Aᴺ ⌝ ⌜ Bᴺ ⌝ γ)
      (cong (Π (⌜ Aᴺ ⌝ [ γ ]ᵀ)) (⌜⌝-[] Bᴺ (γ ⁺)))
      (λ i → Π (⌜⌝-[] Aᴺ γ i) ⌜ []ᵀᴺ-Π.filler Aᴺ Bᴺ γ i ⌝)
      j i

[]ᵀᴺ-∘ :
  (Aᴺ : NTy Γ) (γ : Sub Δ Γ) (δ : Sub Θ Δ) → Aᴺ [ γ ∘ δ ]ᵀᴺ ≡ Aᴺ [ γ ]ᵀᴺ [ δ ]ᵀᴺ
⌜⌝-[]-∘ :
  (Aᴺ : NTy Γ) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
  Square
    ([]ᵀ-∘ ⌜ Aᴺ ⌝ γ δ)
    (cong ⌜_⌝ ([]ᵀᴺ-∘ Aᴺ γ δ))
    (⌜⌝-[] Aᴺ (γ ∘ δ))
    (cong _[ δ ]ᵀ (⌜⌝-[] Aᴺ γ) ∙ ⌜⌝-[] (Aᴺ [ γ ]ᵀᴺ) δ)

[]ᵀᴺ-∘ U γ δ = refl
[]ᵀᴺ-∘ (El Â) γ δ = congS El ([]ᵘ-∘ Â γ δ)
[]ᵀᴺ-∘ (Π Aᴺ Bᴺ) γ δ = λ i → Π ([]ᵀᴺ-∘ Aᴺ γ δ i) (filler₃ i1 i)
  module []ᵀᴺ-∘-Π where
  filler₁ :
    (j i : I) →
    NTy
      (_
        ▹ compPath-filler
            (cong _[ δ ]ᵀ (⌜⌝-[] Aᴺ γ))
            (⌜⌝-[] (Aᴺ [ γ ]ᵀᴺ) δ)
            j i)
  filler₁ j i =
    fill
      (λ j →
        NTy
          (_
            ▹ compPath-filler
                (cong _[ δ ]ᵀ (⌜⌝-[] Aᴺ γ))
                (⌜⌝-[] (Aᴺ [ γ ]ᵀᴺ) δ)
                j i))
      (λ where
        j (i = i0) → Bᴺ [ γ ⁺ ]ᵀᴺ [ δ ⁺ ]ᵀᴺ
        j (i = i1) → []ᵀᴺ-Π.filler (Aᴺ [ γ ]ᵀᴺ) ([]ᵀᴺ-Π.filler Aᴺ Bᴺ γ i1) δ j)
      (inS ([]ᵀᴺ-Π.filler Aᴺ Bᴺ γ i [ δ ⁺ ]ᵀᴺ))
      j
  filler₂ : I → (i : I) → NTy (_ ▹ []ᵀ-∘ ⌜ Aᴺ ⌝ γ δ i)
  filler₂ j i =
    hfill
      (λ where
        j (i = i0) → Bᴺ [ (γ ∘ δ) ⁺ ]ᵀᴺ
        j (i = i1) → []ᵀᴺ-∘ Bᴺ (γ ⁺) (δ ⁺) j)
      (inS (Bᴺ [ ⁺-∘ γ δ i ]ᵀᴺ))
      j
  filler₃ : (j i : I) → NTy (_ ▹ ⌜⌝-[]-∘ Aᴺ γ δ j i)
  filler₃ j i =
    fill (λ j → NTy (_ ▹ ⌜⌝-[]-∘ Aᴺ γ δ j i))
      (λ where
        j (i = i0) → []ᵀᴺ-Π.filler Aᴺ Bᴺ (γ ∘ δ) j
        j (i = i1) → filler₁ i1 j)
      (inS (filler₂ i1 i))
      j

⌜⌝-[]-∘ U γ δ = U-[]-∘ γ δ
⌜⌝-[]-∘ (El Â) γ δ = El-[]-∘ Â γ δ
⌜⌝-[]-∘ (Π Aᴺ Bᴺ) γ δ i j =
  hcomp
    (λ where
      k (i = i0) → Π-[]-∘ ⌜ Aᴺ ⌝ ⌜ Bᴺ ⌝ γ δ (~ k) j
      k (i = i1) → Π (⌜⌝-[]-∘ Aᴺ γ δ k j) ⌜ []ᵀᴺ-∘-Π.filler₃ Aᴺ Bᴺ γ δ k j ⌝
      k (j = i0) → ⌜⌝-[]-Π.filler Aᴺ Bᴺ (γ ∘ δ) k i
      k (j = i1) →
        hcomp
          (λ where
            j (i = i0) →
              ( cong _[ δ ]ᵀ (Π-[] ⌜ Aᴺ ⌝ ⌜ Bᴺ ⌝ γ) ∙
                Π-[] (⌜ Aᴺ ⌝ [ γ ]ᵀ) (⌜ Bᴺ ⌝ [ γ ⁺ ]ᵀ) δ)
                (~ k)
            j (i = i1) →
              hcomp
                (λ where
                  i (j = i0) →
                    Π-[]
                      (⌜⌝-[] Aᴺ γ k)
                      ⌜ []ᵀᴺ-Π.filler Aᴺ Bᴺ γ k ⌝
                      δ
                      (~ i ∨ ~ k)
                  i (j = i1) →
                    Π (compPath-filler
                        (cong _[ δ ]ᵀ (⌜⌝-[] Aᴺ γ))
                        (⌜⌝-[] (Aᴺ [ γ ]ᵀᴺ) δ)
                        i k)
                      ⌜ []ᵀᴺ-∘-Π.filler₁ Aᴺ Bᴺ γ δ i k ⌝
                  i (k = i0) →
                    Π (⌜ Aᴺ ⌝ [ γ ]ᵀ [ δ ]ᵀ) (⌜⌝-[] (Bᴺ [ γ ⁺ ]ᵀᴺ) (δ ⁺) j)
                  i (k = i1) →
                    ⌜⌝-[]-Π.filler
                      (Aᴺ [ γ ]ᵀᴺ)
                      ([]ᵀᴺ-Π.filler Aᴺ Bᴺ γ i1)
                      δ
                      i j)
                (Π
                  (⌜⌝-[] Aᴺ γ k [ δ ]ᵀ)
                  (⌜⌝-[] ([]ᵀᴺ-Π.filler Aᴺ Bᴺ γ k) (δ ⁺) j))
            j (k = i0) →
              Π (⌜ Aᴺ ⌝ [ γ ]ᵀ [ δ ]ᵀ)
                (compPath-filler
                  (cong _[ δ ⁺ ]ᵀ (⌜⌝-[] Bᴺ (γ ⁺)))
                  (⌜⌝-[] (Bᴺ [ γ ⁺ ]ᵀᴺ) (δ ⁺))
                  j i)
            j (k = i1) →
              compPath-filler
                (cong _[ δ ]ᵀ (⌜⌝-[] (Π Aᴺ Bᴺ) γ))
                (⌜⌝-[] (Π Aᴺ Bᴺ [ γ ]ᵀᴺ) δ)
                j i)
          (hcomp
            (λ where
              j (i = i0) →
                compPath-filler
                  (cong _[ δ ]ᵀ (Π-[] ⌜ Aᴺ ⌝ ⌜ Bᴺ ⌝ γ))
                  (Π-[] (⌜ Aᴺ ⌝ [ γ ]ᵀ) (⌜ Bᴺ ⌝ [ γ ⁺ ]ᵀ) δ)
                  j (~ k)
              j (i = i1) →
                Π-[] (⌜⌝-[] Aᴺ γ k) ⌜ []ᵀᴺ-Π.filler Aᴺ Bᴺ γ k ⌝ δ (j ∧ ~ k)
              j (k = i0) → Π-[] (⌜ Aᴺ ⌝ [ γ ]ᵀ) (⌜⌝-[] Bᴺ (γ ⁺) i) δ j
              j (k = i1) → ⌜⌝-[]-Π.filler Aᴺ Bᴺ γ i1 i [ δ ]ᵀ)
            (⌜⌝-[]-Π.filler Aᴺ Bᴺ γ k i [ δ ]ᵀ)))
    (Π
      ([]ᵀ-∘ ⌜ Aᴺ ⌝ γ δ j)
      (hcomp
        (λ where
          k (i = i0) → []ᵀ-⁺-∘-filler ⌜ Bᴺ ⌝ γ δ k j
          k (i = i1) → ⌜ []ᵀᴺ-∘-Π.filler₂ Aᴺ Bᴺ γ δ k j ⌝
          k (j = i0) → ⌜⌝-[] Bᴺ ((γ ∘ δ) ⁺) i
          k (j = i1) → ⌜⌝-[]-∘ Bᴺ (γ ⁺) (δ ⁺) i k)
        (⌜⌝-[] Bᴺ (⁺-∘ γ δ j) i)))

[]ᵀᴺ-id : (Aᴺ : NTy Γ) → Aᴺ [ id ]ᵀᴺ ≡ Aᴺ
⌜⌝-[]-id :
  (Aᴺ : NTy Γ) →
  Square ([]ᵀ-id ⌜ Aᴺ ⌝) (cong ⌜_⌝ ([]ᵀᴺ-id Aᴺ)) (⌜⌝-[] Aᴺ id) refl

[]ᵀᴺ-id U = refl
[]ᵀᴺ-id (El Â) = congS El ([]ᵘ-id Â)
[]ᵀᴺ-id (Π Aᴺ Bᴺ) = λ i → Π ([]ᵀᴺ-id Aᴺ i) (filler₂ i1 i)
  module []ᵀᴺ-id-Π where
  filler₁ : I → (i : I) → NTy (_ ▹ []ᵀ-id ⌜ Aᴺ ⌝ i)
  filler₁ j i =
    hfill
      (λ where
        j (i = i0) → Bᴺ [ id ⁺ ]ᵀᴺ
        j (i = i1) → []ᵀᴺ-id Bᴺ j)
      (inS (Bᴺ [ ⁺-id i ]ᵀᴺ))
      j
  filler₂ : (j i : I) → NTy (_ ▹ ⌜⌝-[]-id Aᴺ j i)
  filler₂ j i =
    fill (λ j → NTy (_ ▹ ⌜⌝-[]-id Aᴺ j i))
      (λ where
        j (i = i0) → []ᵀᴺ-Π.filler Aᴺ Bᴺ id j
        j (i = i1) → Bᴺ)
      (inS (filler₁ i1 i))
      j

⌜⌝-[]-id U = U-[]-id
⌜⌝-[]-id (El Â) = El-[]-id Â
⌜⌝-[]-id (Π Aᴺ Bᴺ) i j =
  hcomp
    (λ where
      k (i = i0) → Π-[]-id ⌜ Aᴺ ⌝ ⌜ Bᴺ ⌝ (~ k) j
      k (i = i1) → Π (⌜⌝-[]-id Aᴺ k j) ⌜ []ᵀᴺ-id-Π.filler₂ Aᴺ Bᴺ k j ⌝
      k (j = i0) → ⌜⌝-[]-Π.filler Aᴺ Bᴺ id k i
      k (j = i1) → Π ⌜ Aᴺ ⌝ ⌜ Bᴺ ⌝)
    (Π
      ([]ᵀ-id ⌜ Aᴺ ⌝ j)
      (hcomp
        (λ where
          k (i = i0) → []ᵀ-⁺-id-filler ⌜ Bᴺ ⌝ k j
          k (i = i1) → ⌜ []ᵀᴺ-id-Π.filler₁ Aᴺ Bᴺ k j ⌝
          k (j = i0) → ⌜⌝-[] Bᴺ (id ⁺) i
          k (j = i1) → ⌜⌝-[]-id Bᴺ i k)
        (⌜⌝-[] Bᴺ (⁺-id j) i)))

module norm where
  open DModel

  M : DModel
  M .Tyᴹ Γ A = fiber ⌜_⌝ A
  M .isSetTyᴹ Γ A = isSetΣ (isSetNTy Γ) λ Aᴺ → isGroupoidTy Γ ⌜ Aᴺ ⌝ A

  M ._[_]ᵀᴹ (Aᴺ , Aᴾ) γ = Aᴺ [ γ ]ᵀᴺ , λ i → filler i1 i
    module []ᵀᴹ where
    filler : I → I → Ty _
    filler j i = compPath-filler (sym (⌜⌝-[] Aᴺ γ)) (cong _[ γ ]ᵀ Aᴾ) j i
  M .[]ᵀ-∘ᴹ (Aᴺ , Aᴾ) γ δ i =
    []ᵀᴺ-∘ Aᴺ γ δ i ,
    λ j →
      hcomp
        (λ where
          k (i = i0) → []ᵀᴹ.filler Aᴺ Aᴾ (γ ∘ δ) k j
          k (i = i1) →
            hcomp
              (λ where
                i (j = i0) → ⌜ Aᴺ [ γ ]ᵀᴺ [ δ ]ᵀᴺ ⌝
                i (j = i1) → []ᵀᴹ.filler Aᴺ Aᴾ γ k i [ δ ]ᵀ
                i (k = i0) →
                  compPath-filler'
                    (cong _[ δ ]ᵀ (⌜⌝-[] Aᴺ γ))
                    (⌜⌝-[] (Aᴺ [ γ ]ᵀᴺ) δ)
                    i (~ j)
                i (k = i1) →
                  []ᵀᴹ.filler
                    (Aᴺ [ γ ]ᵀᴺ)
                    (λ j → []ᵀᴹ.filler Aᴺ Aᴾ γ i1 j)
                    δ
                    i j)
              (⌜⌝-[] (Aᴺ [ γ ]ᵀᴺ) δ (~ j))
          k (j = i0) → ⌜ []ᵀᴺ-∘ Aᴺ γ δ i ⌝
          k (j = i1) → []ᵀ-∘ (Aᴾ k) γ δ i)
        (⌜⌝-[]-∘ Aᴺ γ δ (~ j) i)
  M .[]ᵀ-idᴹ (Aᴺ , Aᴾ) i =
    []ᵀᴺ-id Aᴺ i ,
    λ j →
      hcomp
        (λ where
          k (i = i0) → []ᵀᴹ.filler Aᴺ Aᴾ id k j
          k (i = i1) → Aᴾ (j ∧ k)
          k (j = i0) → ⌜ []ᵀᴺ-id Aᴺ i ⌝
          k (j = i1) → []ᵀ-id (Aᴾ k) i)
        (⌜⌝-[]-id Aᴺ (~ j) i)

  M .Uᴹ = U , refl
  M .U-[]ᴹ γ i =
    U ,
    λ j →
      hcomp
        (λ where
          k (i = i0) → []ᵀᴹ.filler U refl γ k j
          k (i = i1) → U
          k (j = i0) → U
          k (j = i1) → U-[] γ i)
        (U-[] γ (i ∨ ~ j))

  M .Elᴹ  = El  , refl
  M .El-[]ᴹ Â γ i =
    El (Â [ γ ]ᵘ) ,
    λ j →
      hcomp
        (λ where
          k (i = i0) → []ᵀᴹ.filler (El Â) refl γ k j
          k (i = i1) → El (Â [ γ ]ᵘ)
          k (j = i0) → El (Â [ γ ]ᵘ)
          k (j = i1) → El-[] Â γ i)
        (El-[] Â γ (i ∨ ~ j))

  M .Πᴹ (Aᴺ , Aᴾ) (Bᴺ , Bᴾ) = Π Aᴺ (filler₁ i1) , λ i → Π (Aᴾ i) (filler₂ i1 i)
    module Πᴹ where
    filler₁ : (i : I) → NTy (_ ▹ Aᴾ (~ i))
    filler₁ i = transport-filler (λ i → NTy (_ ▹ Aᴾ (~ i))) Bᴺ i
    filler₂ : I → (i : I) → Ty (_ ▹ Aᴾ i)
    filler₂ j i =
      hfill
        (λ where
          j (i = i0) → ⌜ filler₁ i1 ⌝
          j (i = i1) → Bᴾ j)
        (inS ⌜ filler₁ (~ i) ⌝)
        j
  M .Π-[]ᴹ {A = A} (Aᴺ , Aᴾ) (Bᴺ , Bᴾ) γ = λ i →
    Π (Aᴺ [ γ ]ᵀᴺ) (filler₁ i1 i) ,
    λ j →
      hcomp
        (λ where
          k (i = i0) →
            hcomp
              (λ where
                i (j = i0) →
                  Π (⌜⌝-[] Aᴺ γ k) ⌜ []ᵀᴺ-Π.filler Aᴺ (Πᴹ-A-B.filler₁ i1) γ k ⌝
                i (j = i1) →
                  hcomp
                    (λ where
                      j (i = i0) → Π-[] ⌜ Aᴺ ⌝ ⌜ Πᴹ-A-B.filler₁ i1 ⌝ γ (j ∧ ~ k)
                      j (i = i1) →
                        Π (Aᴾ (j ∧ k)) (Πᴹ-A-B.filler₂ i1 (j ∧ k)) [ γ ]ᵀ
                      j (k = i0) → Π-[] ⌜ Aᴺ ⌝ ⌜ Πᴹ-A-B.filler₁ i1 ⌝ γ (~ i ∧ j)
                      j (k = i1) →
                        Π (Aᴾ (i ∧ j)) (Πᴹ-A-B.filler₂ i1 (i ∧ j)) [ γ ]ᵀ)
                    (Π ⌜ Aᴺ ⌝ ⌜ Πᴹ-A-B.filler₁ i1 ⌝ [ γ ]ᵀ)
                i (k = i0) →
                  compPath-filler'
                    (Π-[] ⌜ Aᴺ ⌝ ⌜ Πᴹ-A-B.filler₁ i1 ⌝ γ)
                    (cong (Π (⌜ Aᴺ ⌝ [ γ ]ᵀ)) (⌜⌝-[] (Πᴹ-A-B.filler₁ i1) (γ ⁺)))
                    i (~ j)
                i (k = i1) →
                  []ᵀᴹ.filler
                    (Π Aᴺ (Πᴹ-A-B.filler₁ i1))
                    (λ j → Π (Aᴾ j) (Πᴹ-A-B.filler₂ i1 j))
                    γ
                    i j)
              (⌜⌝-[]-Π.filler Aᴺ (Πᴹ-A-B.filler₁ i1) γ k (~ j))
          k (i = i1) →
            Π ([]ᵀᴹ.filler Aᴺ Aᴾ γ i1 (j ∨ ~ k))
              (hcomp
                (λ where
                  i (j = i0) → ⌜ Πᴹ-A-B-[γ].filler₁ k ⌝
                  i (j = i1) → []ᵀᴹ.filler Bᴺ Bᴾ (γ ⁺) k i
                  i (k = i0) → []ᵀᴹ.filler Bᴺ Bᴾ (γ ⁺) i0 (i ∧ j)
                  i (k = i1) → Πᴹ-A-B-[γ].filler₂ i j)
                ⌜ Πᴹ-A-B-[γ].filler₁ (~ j ∧ k) ⌝)
          k (j = i0) → Π ([]ᵀᴹ.filler Aᴺ Aᴾ γ i (~ k)) ⌜ filler₁ k i ⌝
          k (j = i1) →
            hcomp
              (λ where
                j (i = i0) → Π (Aᴾ k) (Πᴹ-A-B.filler₂ j k) [ γ ]ᵀ
                j (i = i1) → Π (A [ γ ]ᵀ) (Bᴾ (j ∧ k) [ γ ⁺ ]ᵀ)
                j (k = i0) → Π-[] (Aᴾ i) ⌜ Πᴹ-A-B.filler₁ (~ i) ⌝ γ i
                j (k = i1) → Π-[] A (Bᴾ j) γ i)
              (Π-[] (Aᴾ (i ∨ k)) ⌜ Πᴹ-A-B.filler₁ (~ i ∧ ~ k) ⌝ γ i))
        (hcomp
          (λ where
            k (i = i0) →
              compPath-filler
                (Π-[] ⌜ Aᴺ ⌝ ⌜ Πᴹ-A-B.filler₁ i1 ⌝ γ)
                (cong (Π (⌜ Aᴺ ⌝ [ γ ]ᵀ)) (⌜⌝-[] (Πᴹ-A-B.filler₁ i1) (γ ⁺)))
                k (~ j)
            k (i = i1) → Π (A [ γ ]ᵀ) (⌜⌝-[] Bᴺ (γ ⁺) (~ j ∧ k))
            k (j = i0) → Π (Aᴾ i [ γ ]ᵀ) (⌜⌝-[] (Πᴹ-A-B.filler₁ (~ i)) (γ ⁺) k)
            k (j = i1) → Π-[] (Aᴾ i) ⌜ Πᴹ-A-B.filler₁ (~ i) ⌝ γ i)
          (Π-[] (Aᴾ i) ⌜ Πᴹ-A-B.filler₁ (~ i) ⌝ γ (i ∨ ~ j)))
    where
    module Πᴹ-A-B = Πᴹ Aᴺ Aᴾ Bᴺ Bᴾ
    module Πᴹ-A-B-[γ] =
      Πᴹ
        (Aᴺ [ γ ]ᵀᴺ)
        (λ i → []ᵀᴹ.filler Aᴺ Aᴾ γ i1 i)
        (Bᴺ [ γ ⁺ ]ᵀᴺ)
        (λ i → []ᵀᴹ.filler Bᴺ Bᴾ (γ ⁺) i1 i)
    filler₁ : (j i : I) → NTy (_ ▹ []ᵀᴹ.filler Aᴺ Aᴾ γ i (~ j))
    filler₁ j i =
      fill
        (λ j → NTy (_ ▹ []ᵀᴹ.filler Aᴺ Aᴾ γ i (~ j)))
        (λ where
          j (i = i0) → []ᵀᴺ-Π.filler Aᴺ (Πᴹ-A-B.filler₁ i1) γ j
          j (i = i1) → Πᴹ-A-B-[γ].filler₁ j)
        (inS (Πᴹ-A-B.filler₁ (~ i) [ γ ⁺ ]ᵀᴺ))
        j

  open Elim M public

norm : Ty Γ → NTy Γ
norm A = norm.⟦ A ⟧ .fst

⌜⌝-norm : (A : Ty Γ) → ⌜ norm A ⌝ ≡ A
⌜⌝-norm A = norm.⟦ A ⟧ .snd

isSetTy : (Γ : Con) → isSet (Ty Γ)
isSetTy Γ = isSetRetract norm ⌜_⌝ ⌜⌝-norm (isSetNTy _)

module Coh where
  []ᵀ-assoc :
    (A : Ty Γ) (γ : Sub Δ Γ) (δ : Sub Θ Δ) (θ : Sub Ξ Θ) →
    Square
      (cong (A [_]ᵀ) (assoc γ δ θ))
      ([]ᵀ-∘ (A [ γ ]ᵀ) δ θ)
      ([]ᵀ-∘ A γ (δ ∘ θ))
      ([]ᵀ-∘ A (γ ∘ δ) θ ∙ cong _[ θ ]ᵀ ([]ᵀ-∘ A γ δ))
  []ᵀ-assoc A γ δ θ = isSet→isSet' (isSetTy _) _ _ _ _

  []ᵀ-idl :
    (A : Ty Γ) (γ : Sub Δ Γ) →
    Square (cong (A [_]ᵀ) (idl γ)) (cong _[ γ ]ᵀ ([]ᵀ-id A)) ([]ᵀ-∘ A id γ) refl
  []ᵀ-idl A γ = isSet→isSet' (isSetTy _) _ _ _ _

  []ᵀ-idr :
    (A : Ty Γ) (γ : Sub Δ Γ) →
    Square (cong (A [_]ᵀ) (idr γ)) ([]ᵀ-id (A [ γ ]ᵀ)) ([]ᵀ-∘ A γ id) refl
  []ᵀ-idr A γ = isSet→isSet' (isSetTy _) _ _ _ _