open import Cubical.Foundations.Prelude hiding (Sub)
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels
open import Cubical.Data.Unit
open import Cubical.Data.Empty.Base

module TT.Set.ConPath (X : hSet ℓ-zero) (Y : X .fst → hSet ℓ-zero) where

open import TT.Set.Syntax X Y

Cover : Con → Con → Type
decode : (Γ₀ Γ₁ : Con) → Cover Γ₀ Γ₁ → Γ₀ ≡ Γ₁

Cover ◇ ◇ = Unit
Cover (Γ₀ ▹ A₀) (Γ₁ ▹ A₁) =
  Σ[ Γ₀₁ ∈ Cover Γ₀ Γ₁ ] PathP (λ i → Ty (decode Γ₀ Γ₁ Γ₀₁ i)) A₀ A₁
{-# CATCHALL #-}
Cover _ _ = ⊥

decode ◇ ◇ tt = refl
decode (Γ₀ ▹ A₀) (Γ₁ ▹ A₁) (Γ₀₁ , A₀₁) = cong₂ _▹_ (decode Γ₀ Γ₁ Γ₀₁) A₀₁

reflCode : (Γ : Con) → Cover Γ Γ
decodeRefl : (Γ : Con) → decode Γ Γ (reflCode Γ) ≡ refl

reflCode ◇ = tt
reflCode (Γ ▹ A) = reflCode Γ , filler i1
  module reflCode-▹ where
  filler : (i : I) → PathP (λ j → Ty (decodeRefl Γ (~ i) j)) A A
  filler i =
    transport⁻-filler (λ i → PathP (λ j → Ty (decodeRefl Γ i j)) A A) refl i

decodeRefl ◇ i = refl
decodeRefl (Γ ▹ A) i = cong₂ _▹_ (decodeRefl Γ i) (reflCode-▹.filler Γ A (~ i))

encode : (Γ₀ Γ₁ : Con) → Γ₀ ≡ Γ₁ → Cover Γ₀ Γ₁
encode Γ₀ Γ₁ Γ₀₁ = transport (λ i → Cover Γ₀ (Γ₀₁ i)) (reflCode Γ₀)

decodeEncode :
  (Γ₀ Γ₁ : Con) (Γ₀₁ : Γ₀ ≡ Γ₁) → decode Γ₀ Γ₁ (encode Γ₀ Γ₁ Γ₀₁) ≡ Γ₀₁
decodeEncode Γ₀ Γ₁ Γ₀₁ =
  J (λ Γ₁ Γ₀₁ → decode Γ₀ Γ₁ (encode Γ₀ Γ₁ Γ₀₁) ≡ Γ₀₁)
    (cong (decode Γ₀ Γ₀) (transportRefl _) ∙ decodeRefl Γ₀)
    Γ₀₁

isPropCover : (Γ₀ Γ₁ : Con) → isProp (Cover Γ₀ Γ₁)
isPropCover ◇ ◇ = isPropUnit
isPropCover (Γ₀ ▹ A₀) (Γ₁ ▹ A₁) =
  isPropΣ (isPropCover Γ₀ Γ₁) λ Γ₀₁ → isOfHLevelPathP'  (isSetTy Γ₁) A₀ A₁

isSetCon : isSet Con
isSetCon Γ₀ Γ₁ =
  isPropRetract
    (encode Γ₀ Γ₁)
    (decode Γ₀ Γ₁)
    (decodeEncode Γ₀ Γ₁)
    (isPropCover Γ₀ Γ₁)