Agdaの標準ライブラリのData.Fin.Substitutionで相互定義された型の代入を処理する

Question

Agdaでisorecursive型のpush-valueラムダ計算をコードでエンコードしようとしています。そこで、以下のように、最大​​n個の空き値型変数を持つ値型と計算型を相互に定義します（これは単なる回帰型に値型を代入する必要があります）。スタイルhereで

data VType (n : ℕ) : Set where 
    vunit : VType n    -- unit type 
    var : Fin n → VType n  -- type variable 
    u  : CType n → VType n  -- thunk 
    μ : VType (1 + n) → VType n -- isorecursive type 

data CType (n : ℕ) : Set where 
    _⇒_ : VType n → CType n → CType n -- lambda abstraction 
    f : VType n → CType n   -- a value-producer 

、私はctに

example : CType 0 
example = f (var (# 0)) C[/ vunit ] 

どこ

_C[/_] : ∀ {n} → CType (1 + n) → VType n → CType n 
ct [/ vt ] = ? 

後の代替vtのような置換を行うことができるようにしたいです。注意：計算型に値型を代入したいと思います。標準ライブラリを使用してVTypeをVTypeに置き換えますが、上記のようにVTypeをCTypeに設定することはできません。私はType sから行くのが自然アンラップ機能を使用してみました

data VorC : Set where 
    v : VorC 
    c : VorC 

data Type : VorC → ℕ → Set where 
    vtype : ∀ {n} → VType n → Type v n 
    ctype : ∀ {n} → CType n → Type c n 

：

module TypeSubst where 
    -- Following Data.Substitutions.Example 
    module TypeApp {T} (l : Lift T VType) where 
    open Lift l hiding (var) 

    -- Applies a substitution to a type 
    infixl 8 _/v_ 

    _/v_ : ∀ {m n} → VType m → Sub T m n → VType n 
    _/c_ : ∀ {m n} → CType m → Sub T m n → CType n 
    vunit /v ρ = vunit 
    (var x) /v ρ = lift (lookup x ρ) 
    (u σ) /v ρ = u (σ /c ρ) 
    (μ τ) /v ρ = μ (τ /v ρ ↑) 
    (σ ⇒ τ) /c ρ = σ /v ρ ⇒ τ /c ρ 
    f x /c ρ = f (x /v ρ) 

    open Application (record { _/_ = _/v_ }) using (_/✶_) 

    typeSubst : TermSubst VType 
    typeSubst = record { var = var; app = TypeApp._/v_ } 

    open TermSubst typeSubst public hiding (var) 

    weaken↑ : ∀ {n} → VType (1 + n) → VType (2 + n) 
    weaken↑ τ = τ/wk ↑ 

    infix 8 _[/_] 

    -- single type substitution 
    _[/_] : ∀ {n} → VType (1 + n) → VType n → VType n 
    τ [/ σ ] = τ/sub σ 

私は新しいデータ型Typeで作業しようとしました：私は、そうのようなData.Fin.Substitutionを使用して（hereを参照）ことをやりますVType 'またはCType' 'になりますが、標準ライブラリのモジュールを模倣しようとすると、これが動作しないか、終了チェックの問題が発生します。

標準ライブラリのData.Fin.Substitutionを使用することができますか？誰かが私にそのモジュールを説明できますか？これに関するドキュメントはありません。標準ライブラリを使用することができない場合は、この問題にどのようにアプローチするかについての指針も歓迎します。ありがとう！

Answer 1

Applicationは、TermSubstを開く代わりにCTypeを開くことができます（私には間違っていることは分かりません）。関連する部分は次のとおりです。

typeSubst : TermSubst VType 
typeSubst = record { var = var; app = TypeApp._/v_ } 

open TermSubst typeSubst public hiding (var) 

module TypeSubst where 
    _[/v_] : ∀ {n} → VType (1 + n) → VType n → VType n 
    τ [/v σ ] = τ/sub σ 

open Application (record { _/_ = TypeApp._/c_ termLift }) renaming (_/_ to _/c_) using() 

_[/c_] : ∀ {n} → CType (1 + n) → VType n → CType n 
τ [/c σ ] = τ /c sub σ 

全体がcodeです。

標準ライブラリの内容を理解するには、Type-Preserving Renaming and Substitution用紙を読む必要があります。しかし、stdlibのコードはかなり抽象的です。

ところで、order preserving embeddingsを使用すると、名前の変更と名前の変更を定義して置換を定義できます。穴を埋めるhere。