{-# OPTIONS --safe --without-K #-}
open import Data.Product using (; _,_; -,_) renaming (_×_ to _∧_; proj₁ to fst; proj₂ to snd)

open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)

module Semantics.Clouston.Evaluation.IML.Base
  (Ctx' : Set₁)

  (_→̇_ : (P Q : Ctx')  Set) (let infixr 19 _→̇_; _→̇_ = _→̇_)

  (_≈̇_     : {P Q : Ctx'}  (φ ψ : P →̇ Q)  Set) (let infix 18 _≈̇_; _≈̇_ = _≈̇_)
  (≈̇-refl  :  {P Q : Ctx'} {φ : P →̇ Q}  φ ≈̇ φ)
  (≈̇-sym   :  {P Q : Ctx'} {φ ψ : P →̇ Q}  (φ≈̇ψ : φ ≈̇ ψ)  ψ ≈̇ φ)
  (≈̇-trans :  {P Q : Ctx'} {φ ψ ω : P →̇ Q}  (φ≈̇ψ : φ ≈̇ ψ)  (ψ≈̇ω : ψ ≈̇ ω)  φ ≈̇ ω)

  (_∘_ : {P Q R : Ctx'}  (ψ : Q →̇ R)  (φ : P →̇ Q)  (P →̇ R)) (let infixr 19 _∘_; _∘_ = _∘_)
  (let _[_]' = _∘_)

  (id'[_] : (P : Ctx')  P →̇ P)

  ([]'   : Ctx')
  (unit' : {P : Ctx'}  P →̇ []')

  (_×'_   : (P Q : Ctx')  Ctx')
  (⟨_,_⟩' : {R P Q : Ctx'}  (φ : R →̇ P)  (ψ : R →̇ Q)  R →̇ P ×' Q)
  (π₁'[_] : {P : Ctx'}  (Q : Ctx')  P ×' Q →̇ P)
  (π₂'[_] : (P : Ctx')  {Q : Ctx'}  P ×' Q →̇ Q)
  (let fst'[_]_ = λ {R} {P} Q φ  _∘_ {R} {P ×' Q} {P} π₁'[ Q ] φ)
  (let snd'[_]_ = λ {R} P {Q} φ  _∘_ {R} {P ×' Q} {Q} π₂'[ P ] φ)
  (let _×'-map_ = λ {P} {P'} {Q} {Q'} φ ψ  ⟨_,_⟩' {P ×' Q} {P'} {Q'} (φ  π₁'[ Q ]) (ψ  π₂'[ P ]))

  (let Ty' = Ctx')

  (_⇒'_ : (P Q : Ty')  Ty')
  (lam' : {R P Q : Ty'}  (φ : R ×' P →̇ Q)  R →̇ P ⇒' Q)
  (app' : {R P Q : Ty'}  (φ : R →̇ P ⇒' Q)  (ψ : R →̇ P)  R →̇ Q)

  (✦'_     : (P : Ctx')  Ctx')
  (✦'-map_ : {P Q : Ctx'}  (φ : P →̇ Q)  ✦' P →̇ ✦' Q)

  (□'_  : (P : Ty')  Ty')
  (box' : {P Q : Ty'}  (φ : ✦' P →̇ Q)  P →̇ □' Q)
  (λ'   : {P Q : Ty'}  (φ : P →̇ □' Q)  ✦' P →̇ Q)
  where

open import Level using (0ℓ)

open import Relation.Binary using (Reflexive; Symmetric; Transitive; IsEquivalence; Setoid)

import Relation.Binary.Reasoning.Setoid as EqReasoning

open import Type
open import Context Ty Ty-Decidable

≈̇-equiv :  (P Q : Ctx')  IsEquivalence (_≈̇_ {P} {Q})
≈̇-equiv  P Q = record { refl = ≈̇-refl {P} {Q} ; sym = ≈̇-sym {P} {Q} ; trans = ≈̇-trans {P} {Q} }

→̇-setoid : (P Q : Ctx')  Setoid 0ℓ 0ℓ
→̇-setoid P Q = record { Carrier = P →̇ Q ; _≈_ = _≈̇_ ; isEquivalence = ≈̇-equiv P Q }

id' = λ {P}  id'[ P ]

π₁'       = λ {P} {Q}  π₁'[_] {P} Q
π₁'[_][_] = λ P Q  π₁'[_] {P} Q

π₂'       = λ {P} {Q}  π₂'[_] P {Q}
π₂'[_][_] = λ P Q  π₂'[_] P {Q}

-- Δ' : {P P : Ctx'} → P →̇ P ×' P

unbox' : {R P Q : Ty'}  (φ : P →̇ □' Q)  (ψ : R →̇ ✦' P)  R →̇ Q
unbox' φ ψ = λ' φ  ψ

module Eval (N : Ty') where
  evalTy : (a : Ty)  Ty'
  evalTy ι       = N
  evalTy (a  b) = evalTy a ⇒' evalTy b
  evalTy ( a)   = □' evalTy a

  evalCtx : (Γ : Ctx)  Ty'
  evalCtx []       = []'
  evalCtx (Γ `, a) = evalCtx Γ ×' evalTy a
  evalCtx (Γ #)    = ✦' evalCtx Γ

  evalWk : (w : Γ  Δ)  evalCtx Δ →̇ evalCtx Γ
  evalWk base             = unit'
  evalWk (drop {a = a} w) = evalWk w  π₁'[ evalTy a ]
  evalWk (keep {a = a} w) = evalWk w ×'-map id'[ evalTy a ]
  evalWk (keep# w)        = ✦'-map (evalWk w)

  evalVar : (v : Var Γ a)  evalCtx Γ →̇ evalTy a
  evalVar (zero {Γ})       = π₂'[ evalCtx Γ ]
  evalVar (succ {b = b} v) = evalVar v  π₁'[ evalTy b ]

  Sub' = λ Δ Γ  evalCtx Δ →̇ evalCtx Γ

  Sub'-setoid = λ Δ Γ  →̇-setoid (evalCtx Δ) (evalCtx Γ)

  Tm' = λ Γ a  evalCtx Γ →̇ evalTy a

  Tm'-setoid = λ Γ a  →̇-setoid (evalCtx Γ) (evalTy a)

Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.