{-# OPTIONS --safe --without-K #-}
module IS4.Norm.NbE.Model where

open import Data.Product using (Σ ;  ; _×_ ; _,_ ; -,_ ; proj₁ ; proj₂)

open import Relation.Binary
  using    (Reflexive ; Transitive ; Irrelevant)
open import Relation.Binary.PropositionalEquality
  using    (_≡_ ; subst ; cong ; cong₂ ; cong-id ; subst-application)
  renaming (refl to ≡-refl ; sym to ≡-sym ; trans to ≡-trans ; isEquivalence to ≡-equiv)

open import PUtil

open import IS4.Term as Term hiding (factorWk)

import Semantics.Presheaf.Evaluation.IS4

factor :  (Γ◁Δ : Γ ◁IS4 Δ) (w : Δ  Δ')   λ Γ'  Γ  Γ' × Γ' ◁IS4 Δ'
factor (_ , Γ◁Δ) w = -, Term.factorWk Γ◁Δ w , -, factorExt Γ◁Δ w

factorWk :  (Γ◁Δ : Γ ◁IS4 Δ) (w : Δ  Δ')  Γ  _
factorWk r w = factor r w .proj₂ .proj₁

factor◁ :  (Γ◁Δ : Γ ◁IS4 Δ) (w : Δ  Δ')  _ ◁IS4 Δ'
factor◁ r w = factor r w .proj₂ .proj₂

private
  factor-pres-id :  (Γ◁Δ : Γ ◁IS4 Δ)  factor Γ◁Δ idWk  (-, idWk , Γ◁Δ)
  factor-pres-id (_ , Γ◁Δ) = Σ×-≡,≡,≡→≡ (lCtxPresId Γ◁Δ , factorWkPresId Γ◁Δ , ◁IS4-irrel _ _)

  factor-pres-∙ :  (Γ◁Δ : Γ ◁IS4 Δ) (w : Δ  Δ') (w' : Δ'  Δ'')  factor Γ◁Δ (w  w')  (-, factorWk Γ◁Δ w  factorWk (factor◁ Γ◁Δ w) w' , factor◁ (factor◁ Γ◁Δ w) w')
  factor-pres-∙ (_ , Γ◁Δ) w w' = Σ×-≡,≡,≡→≡ (lCtxPres∙ Γ◁Δ w w' , factorWkPres∙ Γ◁Δ w w' , ◁IS4-irrel _ _)

  factor-pres-refl :  (w : Γ  Γ')  factor ◁IS4-refl w  (-, w , ◁IS4-refl)
  factor-pres-refl w = Σ-≡,≡→≡ (lCtxPresRefl {θ = tt} w , ×-≡,≡→≡ (factorWkPresRefl {θ = tt} w , ◁IS4-irrel _ _))

  factor-pres-trans :  (Γ◁Δ : Γ ◁IS4 Δ) (Δ◁Θ : Δ ◁IS4 Θ) (w : Θ  Θ')  factor (◁IS4-trans Γ◁Δ Δ◁Θ) w  (-, factorWk Γ◁Δ (factorWk Δ◁Θ w) , ◁IS4-trans (factor◁ Γ◁Δ (factorWk Δ◁Θ w)) (factor◁ Δ◁Θ w))
  factor-pres-trans (_ , Γ◁Δ) (_ , Δ◁Θ) w = Σ×-≡,≡,≡→≡ (lCtxPresTrans Γ◁Δ Δ◁Θ w , factorWkPresTrans Γ◁Δ Δ◁Θ w , ◁IS4-irrel _ _)

module PresheafEvaluationIS4 = Semantics.Presheaf.Evaluation.IS4
                                 Ctx
                                 _⊆_ _∙_  w w' w''  ≡-sym (assocWk w w' w'')) idWk rightIdWk leftIdWk
                                 _◁IS4_ ◁IS4-trans ◁IS4-trans-assoc ◁IS4-refl ◁IS4-refl-unit-left ◁IS4-refl-unit-right
                                 factor factor-pres-id factor-pres-∙ factor-pres-refl factor-pres-trans

open PresheafEvaluationIS4 public
  hiding   (_→̇_ ; unbox')
  renaming (module Eval to PresheafEvaluationIS4Eval ; module EvalProperties to PresheafEvaluationIS4EvalProperties)

𝒩ℯ : (a : Ty)  Psh
𝒩ℯ a = record
  { Fam           = λ Γ  Ne Γ a
  ; _≋_           = _≡_
  ; ≋-equiv       = λ _  ≡-equiv
  ; wk            = wkNe
  ; wk-pres-≋     = λ w  cong (wkNe w)
  ; wk-pres-refl  = wkNePresId
  ; wk-pres-trans = λ w w' n  ≡-sym (wkNePres∙ w w' n)
  }

open PresheafEvaluationIS4Eval (𝒩ℯ ι)           public
  hiding (Sub' ; Tm')
open PresheafEvaluationIS4EvalProperties (𝒩ℯ ι) public

𝒩𝒻 : (a : Ty)  Psh
𝒩𝒻 a = record
  { Fam           = λ Γ  Nf Γ a
  ; _≋_           = _≡_
  ; ≋-equiv       = λ _  ≡-equiv
  ; wk            = wkNf
  ; wk-pres-≋     = λ w  cong (wkNf w)
  ; wk-pres-refl  = wkNfPresId
  ; wk-pres-trans = λ w w' n  ≡-sym (wkNfPres∙ w w' n)
  }

-- renaming environments, representable presheaf, Yoneda embedding
ℛℯ𝓃 : (Γ : Ctx)  Psh
ℛℯ𝓃 Γ = record
  { Fam           = Γ ⊆_
  ; _≋_           = _≡_
  ; ≋-equiv       = λ _  ≡-equiv
  ; wk            = λ w w'  w'  w
  ; wk-pres-≋     = λ w  cong (_∙ w)
  ; wk-pres-refl  = rightIdWk
  ; wk-pres-trans = λ w w' w''  ≡-sym (assocWk w'' w w')
  }

𝒯𝓂 : (a : Ty)  Psh
𝒯𝓂 a = record
  { Fam           = λ Γ  Tm Γ a
  ; _≋_           = _≡_
  ; ≋-equiv       = λ _  ≡-equiv
  ; wk            = wkTm
  ; wk-pres-≋     = λ w  cong (wkTm w)
  ; wk-pres-refl  = wkTmPresId
  ; wk-pres-trans = λ w w' t  ≡-sym (wkTmPres∙ w w' t)
  }

𝒮𝓊𝒷 : (Γ : Ctx)  Psh
𝒮𝓊𝒷 Γ = record
  { Fam           = λ Δ  Sub Δ Γ
  ; _≋_           = _≡_
  ; ≋-equiv       = λ _  ≡-equiv
  ; wk            = wkSub
  ; wk-pres-≋     = λ w  cong (wkSub w)
  ; wk-pres-refl  = wkSubPresId
  ; wk-pres-trans = λ w w' s  ≡-sym (wkSubPres∙ w w' s)
  }

-- family of maps between interpretations
_→̇_ : (Ctx  Set)  (Ctx  Set)  Set
_→̇_ A B = {Δ : Ctx}  A Δ  B Δ

-- interpretation of types
Tm' : (Γ : Ctx)  (a : Ty)  Set
Tm' Γ a = evalTy a  Γ

Tm'- : Ty  Ctx  Set
Tm'- a Γ = Tm' Γ a

-- interpretation of contexts ("environments")
Sub' : (Γ : Ctx)  (Δ : Ctx)  Set
Sub' Γ Δ = evalCtx Δ  Γ

Sub'- : Ctx  Ctx  Set
Sub'- Δ Γ = Sub' Γ Δ

variable
  ρ ρ' ρ'' : Sub' Γ Δ

-- values in the model can be weakened
wkTy' wkTm' : (a : Ty)  (w : Γ  Γ')  (x : Tm' Γ a)  Tm' Γ' a
wkTy' a = wk[ evalTy a ]
wkTm' = wkTy'

-- environments in the model can be weakened
wkSub' : (Δ : Ctx)  (w : Γ  Γ')  (ρ : Sub' Γ Δ)  Sub' Γ' Δ
wkSub' Δ = wk[ evalCtx Δ ]

-- semantic counterpart of `unbox` from `Tm`
unbox' : Tm' ΓL ( a)  CExt Γ ΓL ΓR  Tm' Γ a
unbox' (elem bx _bx-nat) e = bx idWk (-, e)

unlock' : Sub' Δ (Γ #)  Σ (Ctx × Ctx) λ { (ΔL , ΔR)  Sub' ΔL Γ × CExt Δ ΔL ΔR }
unlock' (elem (ΔL , (ΔR , e), s)) = (ΔL , ΔR) , (s , e)

-- interpretation of variables
substVar' : Var Γ a  Sub'- Γ →̇ Tm'- a
substVar' v = evalVar v .apply

CExt' : CExt Γ ΓL ΓR  Sub'- Γ →̇ Sub'- (ΓL #)
CExt' e = evalAcc e .apply

module _ (e : CExt Γ ΓL ΓR) (s : Sub' Δ Γ) (let elem (ΔL , (ΔR , e') , s') = evalAcc e .apply s) where
  -- "Left" context of factoring with a substitution (see factorExtₛ)
  lCtxₛ' : Ctx
  lCtxₛ' = ΔL

  -- "Right" context of factoring with a substitution (see factorExtₛ)
  rCtxₛ' : Ctx
  rCtxₛ' = ΔR

  -- same as factorExtₛ
  factorExtₛ' : CExt Δ lCtxₛ' rCtxₛ'
  factorExtₛ' = e'

  -- same as factorSubₛ
  factorSubₛ' : Sub' lCtxₛ' ΓL
  factorSubₛ' = s'

-- interpretation of terms
eval : Tm Γ a  (Sub'- Γ →̇ Tm'- a)
eval t s = evalTm t .apply s

-- interpretation of substitutions
evalₛ : Sub Γ Δ  Sub'- Γ  →̇ Sub'- Δ
evalₛ s γ = evalSub s .apply γ

Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.