{-# OPTIONS -WnoUnsupportedIndexedMatch #-}
{-# OPTIONS --lossy-unification #-}
-- Free Simple Category with families generated by a groupoid of base types
module Cubical.Categories.WithFamilies.Simple.Instances.Free.Base where

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.More

open import Cubical.Data.FinData hiding (elim)
open import Cubical.Data.List hiding (elim; [_])
open import Cubical.Data.List.FinData hiding (ℓ; A; B)
open import Cubical.Data.List.Dependent
open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Constructions.Fiber hiding (fiber)
open import Cubical.Categories.Constructions.TotalCategory using (∫C)
open import Cubical.Categories.Functor
open import Cubical.Categories.Limits.Terminal.More
open import Cubical.Categories.Presheaf
open import Cubical.Categories.Presheaf.Constructions
open import Cubical.Categories.Presheaf.More

open import Cubical.Categories.Displayed.Base
open import Cubical.Categories.Displayed.Functor
open import Cubical.Categories.Displayed.Section
open import Cubical.Categories.Displayed.Presheaf

open import Cubical.Categories.WithFamilies.Simple.Base
open import Cubical.Categories.WithFamilies.Simple.Displayed
open import Cubical.Categories.WithFamilies.Simple.Properties

private
  variable
    ℓ ℓ' ℓC ℓC' ℓT ℓT' : Level

open Category
open Functor
open Functorᴰ
open Section
open UniversalElement

module _ (Σ₀ : hGroupoid ℓ) where
  private
    variable
      Δ Γ Θ Ξ : List ⟨ Σ₀ ⟩
      A B C : ⟨ Σ₀ ⟩
  data Var : (Γ : List ⟨ Σ₀ ⟩) → ⟨ Σ₀ ⟩ → Type ℓ where
    vz : ∀ {Γ A} → Var (A ∷ Γ) A
    vs : ∀ {Γ A B} → Var Γ A → Var (B ∷ Γ) A

  Var' : (Γ : List ⟨ Σ₀ ⟩) → (A : ⟨ Σ₀ ⟩) → Type ℓ
  Var' Γ = fiber (lookup Γ)

  isSetVar' : isSet (Var' Γ A)
  isSetVar' = isSetΣ isSetFin λ _ → Σ₀ .snd _ _

  isSetVar : isSet (Var Γ A)
  isSetVar {Γ = Γ} = isSetRetract var→var' var'→var (r _ _) (isSetVar' {Γ = Γ}) where
    var→var' : ∀ {Γ A} → Var Γ A → Var' Γ A
    var→var' vz = zero , refl
    var→var' (vs x) = suc (x' .fst) , x' .snd where
      x' = var→var' x

    var'→var : ∀ {Γ A} → Var' Γ A → Var Γ A
    var'→var {A' ∷ Γ}{A} (zero , x':A) =
      subst (λ A' → Var (A' ∷ Γ) A) (sym x':A) vz
    var'→var {A' ∷ Γ}{A} (suc x' , x':A) =
      vs (var'→var (x' , x':A))

    r : ∀ Γ A (x : Var Γ A) → var'→var (var→var' x) ≡ x
    r Γ A vz = transportRefl _
    r Γ A (vs x) = cong vs (r _ _ x)

  Renaming : (Δ : List ⟨ Σ₀ ⟩) (Γ : List ⟨ Σ₀ ⟩) → Type ℓ
  Renaming Δ = ListP (Var Δ)

  ⟨_⟩∷⟨_⟩ :
    ∀ {x x' : Var Δ A}{γ γ' : Renaming Δ Γ}
    → x ≡ x'
    → γ ≡ γ'
    → Path (Renaming Δ (A ∷ Γ)) (x ∷ γ) (x' ∷ γ')
  ⟨ x ⟩∷⟨ γ ⟩ i = x i ∷ γ i

  private
    variable
      γ δ θ : Renaming Δ Γ

  -- Renamings act on variables
  ren : Renaming Δ Γ → Var Γ A → Var Δ A
  ren (y ∷ γ) vz = y
  ren (y ∷ γ) (vs x) = ren γ x

  wkRen : Renaming Δ Γ → Renaming (A ∷ Δ) Γ
  wkRen [] = []
  wkRen (x ∷ θ) = (vs x) ∷ (wkRen θ)

  idRen : ∀ Γ → Renaming Γ Γ
  idRen [] = []
  idRen (x ∷ Γ) = vz ∷ wkRen (idRen Γ)

  _⋆Ren_ : Renaming Θ Δ → Renaming Δ Γ → Renaming Θ Γ
  δ ⋆Ren [] = []
  δ ⋆Ren (x ∷ γ) = ren δ x ∷ (δ ⋆Ren γ)

  renWkRen : ∀ (γ : Renaming Δ Γ)(x : Var Γ A)
    → ren (wkRen {A = B} γ) x ≡ vs (ren γ x)
  renWkRen (y ∷ γ) vz = refl
  renWkRen (y ∷ γ) (vs x) = renWkRen γ x

  renId : ∀ {A} Γ (x : Var Γ A) → ren (idRen Γ) x ≡ x
  renId (B ∷ Γ) vz = refl
  renId (B ∷ Γ) (vs x) =
    renWkRen (idRen Γ) x
    ∙ cong vs (renId Γ x)

  ren⋆ : ∀ {Θ Δ Γ A}{δ : Renaming Θ Δ}(γ : Renaming Δ Γ)(x : Var Γ A)
    → ren (δ ⋆Ren γ) x ≡ ren δ (ren γ x)
  ren⋆ (y ∷ γ) vz = refl
  ren⋆ (y ∷ γ) (vs x) = ren⋆ γ x

  ⋆Ren⋆IdL : ∀ (γ : Renaming Δ Γ) → (idRen Δ ⋆Ren γ) ≡ γ
  ⋆Ren⋆IdL [] = refl
  ⋆Ren⋆IdL (x ∷ γ) = ⟨ renId _ x ⟩∷⟨ ⋆Ren⋆IdL γ ⟩

  ⋆RenWk :
    ∀ (γ : Renaming Δ Γ) (δ : Renaming Θ Δ) (x : Var Θ A) →
    (x ∷ δ) ⋆Ren wkRen γ ≡ (δ ⋆Ren γ)
  ⋆RenWk [] δ x = refl
  ⋆RenWk (y ∷ γ) δ x = ⟨ refl ⟩∷⟨ ⋆RenWk γ δ x ⟩

  ⋆Ren⋆IdR : ∀ Γ (γ : Renaming Δ Γ) → (γ ⋆Ren idRen Γ) ≡ γ
  ⋆Ren⋆IdR [] [] = refl
  ⋆Ren⋆IdR (A ∷ Γ) (x ∷ γ) = ⟨ refl ⟩∷⟨ ⋆RenWk (idRen _) γ x ∙ ⋆Ren⋆IdR Γ γ ⟩

  ⋆Ren⋆Assoc :
    ∀ (θ : Renaming Ξ Θ)
    → (δ : Renaming Θ Δ)
    → (γ : Renaming Δ Γ)
    → ((θ ⋆Ren δ) ⋆Ren γ) ≡ θ ⋆Ren (δ ⋆Ren γ)
  ⋆Ren⋆Assoc _ _ [] = refl
  ⋆Ren⋆Assoc θ δ (x ∷ γ) = ⟨ ren⋆ δ x ⟩∷⟨ ⋆Ren⋆Assoc _ _ _ ⟩

  RenamingCategory : Category ℓ ℓ
  RenamingCategory .ob = List ⟨ Σ₀ ⟩
  RenamingCategory .Hom[_,_] = Renaming
  RenamingCategory .id = idRen _
  RenamingCategory ._⋆_ = _⋆Ren_
  RenamingCategory .⋆IdL = ⋆Ren⋆IdL
  RenamingCategory .⋆IdR = ⋆Ren⋆IdR _
  RenamingCategory .⋆Assoc = ⋆Ren⋆Assoc
  RenamingCategory .isSetHom = isOfHLevelSucSuc-ListP  λ _ → isSetVar

  VarPsh : ∀ (A : ⟨ Σ₀ ⟩) → Presheaf RenamingCategory ℓ
  VarPsh A .F-ob Γ .fst = Var Γ A
  VarPsh A .F-ob Γ .snd = isSetVar
  VarPsh A .F-hom = ren
  VarPsh A .F-id = funExt (renId _)
  VarPsh A .F-seq γ δ = funExt (ren⋆ γ)

  TermCtx : Terminal' RenamingCategory
  TermCtx .vertex = []
  TermCtx .element = tt
  TermCtx .universal Γ = isIsoToIsEquiv
    ((λ z → []) , ((λ _ → refl) , (λ { [] → refl })))

  CtxExt : ∀ A → LocallyRepresentable (VarPsh A)
  CtxExt A Γ .vertex = A ∷ Γ
  CtxExt A Γ .element = (wkRen $ idRen _) , vz
  CtxExt A Γ .universal Δ = isIsoToIsEquiv
    ( (λ γx → (γx .snd) ∷ (γx .fst))
    , (λ γx → ΣPathP ((⋆RenWk _ _ _ ∙ ⋆Ren⋆IdR _ _) , refl))
    , λ { (x ∷ γ) → ⟨ refl ⟩∷⟨ ⋆RenWk _ _ _ ∙ ⋆Ren⋆IdR _ _ ⟩ })

  FreeSCwF : SCwF ℓ ℓ ℓ ℓ
  FreeSCwF .fst = RenamingCategory
  FreeSCwF .snd .fst = ⟨ Σ₀ ⟩
  FreeSCwF .snd .snd .fst = VarPsh
  FreeSCwF .snd .snd .snd .fst = TermCtx
  FreeSCwF .snd .snd .snd .snd = CtxExt

  module _ (M : SCwFᴰ FreeSCwF ℓC ℓC' ℓT ℓT') where
    private
      module M = SCwFᴰNotation M
      ∫Cᴰ = ∫C M.Cᴰ
      module ∫Tmᴰ {A}{Aᴰ : M.Tyᴰ A} = PresheafNotation (∫P (M.Tmᴰ Aᴰ))
    open PshSection
    module _ (ı : ∀ A → M.Tyᴰ A) where
      elimS-F-ob : ∀ Γ → M.Cᴰ.ob[ Γ ]
      elimS-F-ob [] = M.termᴰ.vertexᴰ
      elimS-F-ob (A ∷ Γ) = M.extᴰ.vertexᴰ {Γᴰ = elimS-F-ob Γ}{Aᴰ = ı A}

      elimVar : ∀ {Γ A} (x : Var Γ A) → ⟨ M.Tmᴰ (ı A) .F-obᴰ (elimS-F-ob Γ) x ⟩
      elimVar {Γ = A ∷ Γ}{A = A} vz = M.extᴰ.elementᴰ .snd
      elimVar (vs x) = M.Tmᴰ.reind lemma $ (M.extᴰ.elementᴰ .fst) M.Tmᴰ.⋆ᴰ elimVar x
        where
          lemma : ∀ {B} → ren (wkRen {A = B} $ idRen _) x ≡ vs x
          lemma = renWkRen (idRen _) x ∙ cong vs (renId _ _)

      elimRen : ∀ {Δ Γ} (γ : Renaming Δ Γ) → M.Cᴰ [ γ ][ elimS-F-ob Δ , elimS-F-ob Γ ]
      elimRen [] = M.termᴰ.introᴰ _
      elimRen (x ∷ γ) = M.extᴰ.introᴰ (elimRen γ , elimVar x)

      elimRenWkRen : ∀ {Δ Γ A}(γ : Renaming Δ Γ)
        → Path (∫Cᴰ [ (A ∷ Δ , _) , (Γ , _) ])
            (_ , elimRen (wkRen γ))
            (_ , M.extᴰ.elementᴰ .fst M.Cᴰ.⋆ᴰ elimRen γ)
      elimRenWkRen [] = M.termᴰ.extensionalityᴰ refl
      elimRenWkRen (x ∷ γ) =
        M.extᴰ.introᴰ≡ (ΣPathPᴰ (elimRenWkRen γ ∙ M.Cᴰ.⟨ refl ⟩⋆⟨ sym $ PathPᴰΣ M.extᴰ.βᴰ .fst ⟩ ∙ sym (M.Cᴰ.⋆Assoc _ _ _))
                           (((sym $ M.Tmᴰ.reind-filler _ _) ∙ M.Tmᴰ.⟨⟩⋆⟨ sym $ PathPᴰΣ M.extᴰ.βᴰ .snd ⟩) ∙ sym (M.Tmᴰ.⋆Assoc _ _ _)))

      elimRen-Var : ∀ {Δ Γ A}
        → (γ : Renaming Δ Γ)
        → (x : Var Γ A)
        → Path ∫Tmᴰ.p[ _ ]
            (_ , elimVar (ren γ x))
            (_ , elimRen γ M.Tmᴰ.⋆ᴰ elimVar x)
      elimRen-Var (y ∷ γ) vz = sym $ PathPᴰΣ M.extᴰ.βᴰ .snd
      elimRen-Var (y ∷ γ) (vs x) =
        elimRen-Var γ x
        ∙ M.Tmᴰ.⟨ sym $ PathPᴰΣ M.extᴰ.βᴰ .fst ⟩⋆⟨⟩
        ∙ M.Tmᴰ.⋆Assoc _ _ _
        ∙ M.Tmᴰ.⟨⟩⋆⟨ M.Tmᴰ.reind-filler _ _ ⟩

      elimRen-Id : ∀ Γ →
        Path (∫Cᴰ [ _ , _ ])
          (_ , elimRen (idRen Γ))
          (_ , M.Cᴰ.idᴰ)
      elimRen-Id [] = M.termᴰ.extensionalityᴰ refl
      elimRen-Id (x ∷ Γ) =
        M.extᴰ.introᴰ≡
          (ΣPathPᴰ
            (elimRenWkRen _ ∙ M.Cᴰ.⟨ refl ⟩⋆⟨ elimRen-Id Γ ⟩ ∙ M.Cᴰ.⋆IdR _ ∙ sym (M.Cᴰ.⋆IdL _))
            (sym $ M.Tmᴰ.⋆IdL _))

      elimRen-Seq : ∀ {Θ Δ Γ}
        → {δ : Renaming Θ Δ}
        → (γ : Renaming Δ Γ)
        → Path (∫Cᴰ [ _ , _ ])
            (_ , elimRen (δ ⋆Ren γ))
            (_ , elimRen δ M.Cᴰ.⋆ᴰ elimRen γ)
      elimRen-Seq [] = M.termᴰ.extensionalityᴰ refl
      elimRen-Seq (y ∷ γ) = M.extᴰ.introᴰ≡ (ΣPathPᴰ
        (elimRen-Seq γ ∙ M.Cᴰ.⟨ refl ⟩⋆⟨ sym $ PathPᴰΣ M.extᴰ.βᴰ .fst ⟩ ∙ sym (M.Cᴰ.⋆Assoc _ _ _))
        (elimRen-Var _ _ ∙ M.Tmᴰ.⟨⟩⋆⟨ sym $ PathPᴰΣ M.extᴰ.βᴰ .snd ⟩ ∙ sym (M.Tmᴰ.⋆Assoc _ _ _)))

      elimSection : GlobalSection (M .fst)
      elimSection .F-obᴰ = elimS-F-ob
      elimSection .F-homᴰ = elimRen
      elimSection .F-idᴰ = M.Cᴰ.rectify $ M.Cᴰ.≡out $ elimRen-Id _
      elimSection .F-seqᴰ δ γ = M.Cᴰ.rectify $ M.Cᴰ.≡out $ elimRen-Seq γ

      elimPshSection : ∀ {A} → PshSection elimSection (M.Tmᴰ $ ı A)
      elimPshSection .N-ob x = elimVar x
      elimPshSection .N-hom γ x =
        M.Tmᴰ.rectify $ M.Tmᴰ.≡out $ elimRen-Var _ _

      elim : StrictSection FreeSCwF M
      elim .fst = elimSection
      elim .snd .fst = ı
      elim .snd .snd .fst = λ _ → elimPshSection
      elim .snd .snd .snd .fst = refl
      elim .snd .snd .snd .snd A Γ =
        ΣPathP (refl , (ΣPathP
          ((M.Cᴰ.rectify $ M.Cᴰ.≡out $
            elimRenWkRen _
            ∙ M.Cᴰ.⟨ refl ⟩⋆⟨ elimRen-Id _ ⟩
            ∙ M.Cᴰ.⋆IdR _)
          , refl)))