{-# OPTIONS --allow-unsolved-metas --sized-types #-}
module A201607.OldBasicILP.Syntax.Projection where
open import A201607.Common.UntypedContext public
import A201607.OldBasicILP.UntypedSyntax.ClosedHilbertSequential as CHS
import A201607.OldBasicILP.UntypedSyntax.ClosedHilbert as CH
module ClosedHilbertSequential where
open import A201607.OldBasicILP.Syntax.ClosedHilbertSequential
mutual
⌊_⌋ᵀ : Ty → CHS.Ty
⌊ α P ⌋ᵀ = CHS.α P
⌊ A ▻ B ⌋ᵀ = ⌊ A ⌋ᵀ CHS.▻ ⌊ B ⌋ᵀ
⌊ p ⦂ A ⌋ᵀ = ⌊ p ⌋ᴾ CHS.⦂ ⌊ A ⌋ᵀ
⌊ A ∧ B ⌋ᵀ = ⌊ A ⌋ᵀ CHS.∧ ⌊ B ⌋ᵀ
⌊ ⊤ ⌋ᵀ = CHS.⊤
postulate
⌊_⌋ᴾ : ∀ {Ξ A} → Proof Ξ A → CHS.Proof
⌊_⌋ᵀ⋆ : Cx Ty → Cx CHS.Ty
⌊ ∅ ⌋ᵀ⋆ = ∅
⌊ Γ , A ⌋ᵀ⋆ = ⌊ Γ ⌋ᵀ⋆ , ⌊ A ⌋ᵀ
⌊_⌋∈ : ∀ {Ξ A} → A ∈ Ξ → ⌊ A ⌋ᵀ ∈ ⌊ Ξ ⌋ᵀ⋆
⌊ top ⌋∈ = top
⌊ pop i ⌋∈ = pop ⌊ i ⌋∈
⌊_⌋ᴰ : ∀ {Ξ} → ⊢ᴰ Ξ → CHS.⊢ᴰ ⌊ Ξ ⌋ᵀ⋆
⌊ nil ⌋ᴰ = CHS.nil
⌊ mp i j d ⌋ᴰ = CHS.mp ⌊ i ⌋∈ ⌊ j ⌋∈ ⌊ d ⌋ᴰ
⌊ ci d ⌋ᴰ = CHS.ci ⌊ d ⌋ᴰ
⌊ ck d ⌋ᴰ = CHS.ck ⌊ d ⌋ᴰ
⌊ cs d ⌋ᴰ = CHS.cs ⌊ d ⌋ᴰ
⌊ nec `d d ⌋ᴰ = {!CHS.nec ⌊ `d ⌋ᴰ ⌊ d ⌋ᴰ!}
⌊ cdist d ⌋ᴰ = {!CHS.cdist ⌊ d ⌋ᴰ!}
⌊ cup d ⌋ᴰ = {!CHS.cup ⌊ d ⌋ᴰ!}
⌊ cdown d ⌋ᴰ = CHS.cdown ⌊ d ⌋ᴰ
⌊ cpair d ⌋ᴰ = CHS.cpair ⌊ d ⌋ᴰ
⌊ cfst d ⌋ᴰ = CHS.cfst ⌊ d ⌋ᴰ
⌊ csnd d ⌋ᴰ = CHS.csnd ⌊ d ⌋ᴰ
⌊ unit d ⌋ᴰ = CHS.unit ⌊ d ⌋ᴰ
⌊_⌋ : ∀ {A} → ⊢ A → CHS.⊢ ⌊ A ⌋ᵀ
⌊ Ξ , d ⌋ = ⌊ Ξ ⌋ᵀ⋆ , ⌊ d ⌋ᴰ
module ClosedHilbert where
open import A201607.OldBasicILP.Syntax.ClosedHilbert
mutual
⌊_⌋ᵀ : Ty → CH.Ty
⌊ α P ⌋ᵀ = CH.α P
⌊ A ▻ B ⌋ᵀ = ⌊ A ⌋ᵀ CH.▻ ⌊ B ⌋ᵀ
⌊ p ⦂ A ⌋ᵀ = ⌊ p ⌋ᴾ CH.⦂ ⌊ A ⌋ᵀ
⌊ A ∧ B ⌋ᵀ = ⌊ A ⌋ᵀ CH.∧ ⌊ B ⌋ᵀ
⌊ ⊤ ⌋ᵀ = CH.⊤
⌊_⌋ᴾ : ∀ {A} → Proof A → CH.Proof
⌊ [ d ] ⌋ᴾ = CH.[ CH.ᴿ⌊ ⌊ d ⌋ ⌋ ]
⌊_⌋ : ∀ {A} → ⊢ A → CH.⊢ ⌊ A ⌋ᵀ
⌊ app d₁ d₂ ⌋ = CH.app ⌊ d₁ ⌋ ⌊ d₂ ⌋
⌊ ci ⌋ = CH.ci
⌊ ck ⌋ = CH.ck
⌊ cs ⌋ = CH.cs
⌊ box d ⌋ = CH.box ⌊ d ⌋
⌊ cdist ⌋ = CH.cdist
⌊ cup ⌋ = CH.cup
⌊ cdown ⌋ = CH.cdown
⌊ cpair ⌋ = CH.cpair
⌊ cfst ⌋ = CH.cfst
⌊ csnd ⌋ = CH.csnd
⌊ unit ⌋ = CH.unit