```{-# OPTIONS --without-K #-}
module Model.Quantification where

open import Model.RGraph as RG using (RGraph)
open import Model.Size as MS using (_<_ ; ⟦_⟧Δ ; ⟦_⟧n ; ⟦_⟧σ)
open import Model.Type.Core
open import Source.Size.Substitution.Theory
open import Source.Size.Substitution.Universe as SS using (Sub⊢ᵤ)
open import Util.HoTT.Equiv
open import Util.HoTT.FunctionalExtensionality
open import Util.HoTT.HLevel
open import Util.Prelude hiding (_∘_)
open import Util.Relation.Binary.PropositionalEquality using
( Σ-≡⁺ ; subst-sym-subst ; subst-subst-sym )

import Source.Size as SS
import Source.Type as ST

open RGraph
open RG._⇒_
open SS.Ctx
open SS.Sub⊢ᵤ

record ⟦∀⟧′ {Δ} n (T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ) (δ : Obj ⟦ Δ ⟧Δ) : Set where
no-eta-equality
field
arr : ∀ m (m<n : m < ⟦ n ⟧n .fobj δ) → Obj T (δ , m , m<n)
param : ∀ m m<n m′ m′<n → eq T _ (arr m m<n) (arr m′ m′<n)

open ⟦∀⟧′ public

⟦∀⟧′Canon : ∀ {Δ} n (T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ) (δ : Obj ⟦ Δ ⟧Δ) → Set
⟦∀⟧′Canon n T δ
= Σ[ f ∈ (∀ m (m<n : m < ⟦ n ⟧n .fobj δ) → Obj T (δ , m , m<n)) ]
(∀ m m<n m′ m′<n → eq T _ (f m m<n) (f m′ m′<n))

⟦∀⟧′≅⟦∀⟧′Canon : ∀ {Δ n T δ} → ⟦∀⟧′ {Δ} n T δ ≅ ⟦∀⟧′Canon n T δ
⟦∀⟧′≅⟦∀⟧′Canon = record
{ forth = λ { record { arr = x ; param = y } → x , y }
; isIso = record
{ back = λ x → record { arr = proj₁ x ; param = proj₂ x }
; back∘forth = λ { record {} → refl }
; forth∘back = λ _ → refl
}
}

abstract
⟦∀⟧′Canon-IsSet : ∀ {Δ n T δ} → IsSet (⟦∀⟧′Canon {Δ} n T δ)
⟦∀⟧′Canon-IsSet {T = T} = Σ-IsSet
(∀-IsSet λ m → ∀-IsSet λ m<n → λ _ _ → T .Obj-IsSet _ _)
(λ f → IsOfHLevel-suc 1 (∀-IsProp λ m → ∀-IsProp λ m<n → ∀-IsProp λ m′
→ ∀-IsProp λ m′<n → T .eq-IsProp))

⟦∀⟧′-IsSet : ∀ {Δ n T δ} → IsSet (⟦∀⟧′ {Δ} n T δ)
⟦∀⟧′-IsSet {Δ} {n} {T} {δ}
= ≅-pres-IsOfHLevel 2 (≅-sym ⟦∀⟧′≅⟦∀⟧′Canon) (⟦∀⟧′Canon-IsSet {Δ} {n} {T} {δ})

⟦∀⟧′-≡⁺ : ∀ {Δ n T δ} (f g : ⟦∀⟧′ {Δ} n T δ)
→ (∀ m m<n → f .arr m m<n ≡ g .arr m m<n)
→ f ≡ g
⟦∀⟧′-≡⁺ {T = T} record{} record{} f≈g = ≅-Injective ⟦∀⟧′≅⟦∀⟧′Canon (Σ-≡⁺
( (funext λ m → funext λ m<n → f≈g m m<n)
, funext λ m → funext λ m<n → funext λ m′ → funext λ m<n′ → T .eq-IsProp _ _))

⟦∀⟧′-resp-≈⟦Type⟧ : ∀ {Δ n T U}
→ T ≈⟦Type⟧ U
→ ∀ {δ} → ⟦∀⟧′ {Δ} n T δ ≅ ⟦∀⟧′ n U δ
⟦∀⟧′-resp-≈⟦Type⟧ T≈U = record
{ forth = λ f → record
{ arr = λ m m<n → T≈U .forth .fobj (f .arr m m<n)
; param = λ m m<n m′ m′<n → T≈U .forth .feq _ (f .param m m<n m′ m′<n)
}
; isIso = record
{ back = λ f → record
{ arr = λ m m<n → T≈U .back .fobj (f .arr m m<n)
; param = λ m m<n m′ m′<n → T≈U .back .feq _ (f .param m m<n m′ m′<n)
}
; back∘forth = λ x → ⟦∀⟧′-≡⁺ _ _ λ m m<n → T≈U .back-forth .≈⁻ _ _
; forth∘back = λ x → ⟦∀⟧′-≡⁺ _ _ λ m m<n → T≈U .forth-back .≈⁻ _ _
}
}

⟦∀⟧ : ∀ {Δ} n (T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ) → ⟦Type⟧ ⟦ Δ ⟧Δ
⟦∀⟧ n T = record
{ ObjHSet = λ δ → HLevel⁺ (⟦∀⟧′ n T δ) ⟦∀⟧′-IsSet
; eqHProp = λ _ f g → ∀-HProp _ λ m → ∀-HProp _ λ m<n → ∀-HProp _ λ m′
→ ∀-HProp _ λ m′<n → T .eqHProp _ (f .arr m m<n) (g .arr m′ m′<n)
; eq-refl = λ f → f .param
}

⟦∀⟧-resp-≈⟦Type⟧ : ∀ {Δ} n {T U : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ}
→ T ≈⟦Type⟧ U
→ ⟦∀⟧ n T ≈⟦Type⟧ ⟦∀⟧ n U
⟦∀⟧-resp-≈⟦Type⟧ n T≈U = record
{ forth = record
{ fobj = ⟦∀⟧′-resp-≈⟦Type⟧ T≈U .forth
; feq = λ δ≈δ′ x≈y a a₁ a₂ a₃ → T≈U .forth .feq _ (x≈y a a₁ a₂ a₃)
}
; back = record
{ fobj = ⟦∀⟧′-resp-≈⟦Type⟧ T≈U .back
; feq = λ δ≈δ′ x≈y a a₁ a₂ a₃ → T≈U .back .feq _ (x≈y a a₁ a₂ a₃)
}
; back-forth = ≈⁺ λ δ x → ⟦∀⟧′-resp-≈⟦Type⟧ T≈U .back∘forth _
; forth-back = ≈⁺ λ δ x → ⟦∀⟧′-resp-≈⟦Type⟧ T≈U .forth∘back _
}

absₛ : ∀ {Δ n} {Γ : ⟦Type⟧ ⟦ Δ ⟧Δ} {T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ}
→ subT ⟦ SS.Wk ⟧σ Γ ⇒ T
→ Γ ⇒ ⟦∀⟧ n T
absₛ {Δ} {n} {Γ} {T} f = record
{ fobj = λ {δ} x → record
{ arr = λ m m<n → f .fobj x
; param = λ m m<n m′ m′<n → f .feq _ (Γ .eq-refl x)
}
; feq = λ _ x≈y m m′ m<nγ m′<nγ′ → f .feq ⊤.tt x≈y
}

appₛ : ∀ {Δ n m} {Γ : ⟦Type⟧ ⟦ Δ ⟧Δ} {T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ}
→ (m<n : m SS.< n)
→ Γ ⇒ ⟦∀⟧ n T
→ Γ ⇒ subT ⟦ SS.Sing m<n ⟧σ T
appₛ {m = m} {T = T} m<n f = record
{ fobj = λ {δ} x → f .fobj x .arr (⟦ m ⟧n .fobj δ) (MS.⟦<⟧ m<n)
; feq = λ δ≈δ′ {x y} x≈y → f .feq _ x≈y _ _ _ _
}

subT-⟦∀⟧ : ∀ {Δ Ω n σ} (⊢σ : σ ∶ Δ ⇒ᵤ Ω) (T : ⟦Type⟧ ⟦ Ω ∙ n ⟧Δ)
→ ⟦∀⟧ (n [ σ ]ᵤ)
(subT (⟦_⟧σ {Ω = Ω ∙ n} (Lift ⊢σ refl)) T)
≈⟦Type⟧ subT ⟦ ⊢σ ⟧σ (⟦∀⟧ n T)
subT-⟦∀⟧ {Δ} {Ω} {n} {σ} ⊢σ T = record
{ forth = record
{ fobj = λ {γ} f → record
{ arr = λ m m<n
→ transportObj T
(MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl)
(f .arr m (subst (m <_) (sym (MS.⟦sub⟧ ⊢σ n)) m<n))
; param = λ m m<n m′ m′<n
→ transportObj-resp-eq T _ _ (f .param _ _ _ _)
}
; feq = λ γ≈γ′ f≈g a a₁ a₂ a₃ → transportObj-resp-eq T _ _ (f≈g _ _ _ _)
}
; back = record
{ fobj = λ {γ} f → record
{ arr = λ m m<n
→ transportObj T
(MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl)
(f .arr m (subst (m <_) (MS.⟦sub⟧ ⊢σ n) m<n))
; param = λ m m<n m′ m′<n
→ transportObj-resp-eq T _ _ (f .param _ _ _ _)
}
; feq = λ γ≈γ′ f≈g a a₁ a₂ a₃ → transportObj-resp-eq T _ _ (f≈g _ _ _ _)
}
; back-forth = ≈⁺ λ γ f → ⟦∀⟧′-≡⁺ _ _ λ m m<n
→ trans
(transportObj∘transportObj T
(MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl)
(MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl))
(trans
(cong
(λ p → transportObj T
(trans
(MS.⟦Δ∙n⟧-≡⁺ Ω n
(subst (m <_) (MS.⟦sub⟧ ⊢σ n) p)
(subst (m <_) (MS.⟦sub⟧ ⊢σ n) m<n)
refl refl)
(MS.⟦Δ∙n⟧-≡⁺ Ω n
(subst (m <_) (MS.⟦sub⟧ ⊢σ n) m<n)
(subst (m <_) (MS.⟦sub⟧ ⊢σ n) m<n)
refl refl))
(f .arr m p))
(subst-sym-subst (MS.⟦sub⟧ ⊢σ n)))
(transportObj-refl T _))
; forth-back = ≈⁺ λ γ f → ⟦∀⟧′-≡⁺ _ _ λ m m<n
→ trans
(transportObj∘transportObj T
(MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl)
(MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl))
(trans
(cong
(λ p → transportObj T
(trans
(MS.⟦Δ∙n⟧-≡⁺ Ω n p p refl refl)
(MS.⟦Δ∙n⟧-≡⁺ Ω n p m<n refl refl))
(f .arr m p))
(subst-subst-sym (MS.⟦sub⟧ ⊢σ n)))
(transportObj-refl T _))
}
```