<p>The thing is, the definition is &quot;too&quot; dependent. In order to define the <em>type</em> of substitution or renaming, you need to something like</p>
<pre><code>Substitution : Context -&gt; Context -&gt; Set
Substitution Γ Δ = ∀ {α} -&gt; Var Γ α -&gt; Term Δ {!  !}
</code></pre>
<p>Here <code>Var</code> and <code>Term</code> corresponds to your <code>_∋_</code> and <code>_⊢_</code>. Now you can't fill in the hole, because it is expecting something of type <code>Type Δ</code>. But <code>α</code> is of type <code>Type Γ</code>. This means you need to make a substitution depending on the previous variables.</p>
<p>So, whenever you extend a substitution list by a little, you will have to refer to the previously built part. This means that defining substitution in the PLFA style doesn't work, and you will have to use an inductive type for substitution.</p>
<p>Ok, fair. So let's try the easy one. Let's define renaming, which, different from the PLFA style, needs to keep the variables in order (the PLFA definition allows for arbitrary permutations) to keep the dependency straight. So the obvious thing is to have <code>keep</code> and <code>drop</code> as the constructors. You may realize that this is analogous to the inductive list-containment predicate. Let's start out:</p>
<pre><code>data Ren : Context -&gt; Context -&gt; Set
rent : Ren Δ Γ -&gt; Type Γ -&gt; Type Δ
</code></pre>
<p>where <code>rent</code> stands for <code>renaming on types</code>. And you <em>do</em> get to define:</p>
<pre><code>data Ren where
    stop : Ren ∅ ∅
    drop : Ren Γ Δ -&gt; Ren (Γ ◂ α) Δ
    keep : (ρ : Ren Γ Δ) -&gt; Ren (Γ ◂ rent ρ α) (Δ ◂ α)
</code></pre>
<p>where the black triangle (input sequence <code>\t</code>) is my queer notation for a context extension. Now you just need an element <code>ren-id : Ren Γ Γ</code>, and then you get to construct <code>drop ren-id</code> as the <span class="math-container">$\mathsf p$</span> thing in the literature.</p>
<p>But there is a problem, you can't just define <code>ren-id</code> by induction:</p>
<pre><code>ren-id : Ren Γ Γ
ren-id {Γ = ∅} = stop
ren-id {Γ = Γ ◂ α} = {! keep !}
</code></pre>
<p>The types don't match up. You need to simultaneously prove that renaming with <code>ren-id</code> is the identity. But at this point you haven't even <strong>defined</strong> <code>rent</code> yet! So let's define that first. When you encounter type variables, you need to fetch the renamed variable, and to fetch that, you need to first define the variables:</p>
<pre><code>data Var where
     : Var (Γ ◂ α) (rent  α)
    _ : Var Γ α -&gt; Var (Γ ◂ β) (rent  α)

fetch : (ρ : Ren Γ Δ) -&gt; Var Δ α -&gt; Var Γ (rent ρ α)
fetch ρ  = {!   !}
fetch ρ ( i) = {!   !}

rent ρ ⋆ = ⋆
rent ρ (var i) = var (fetch ρ i)
rent ρ (Π t) = Π {!   !}
rent ρ (t ⇒ s) = rent ρ t ⇒ rent ρ s
</code></pre>
<p>I'm using system F as an example. But this looks bad: the signature of <code>fetch</code> has <code>rent</code> in it again! By the way, this triggers a bug in Agda, which I'm going to report. You can go on fiddling with that, but I think this demonstrates that it is not going to work out.</p>

CC BY-SA 4.0
2022-02-14T16:07:28.147Z
2022-02-14T16:07:28.147Z
Trebor
<p>I am playing around the <a href="https://plfa.github.io/" rel="noreferrer">Programming Language Foundations in Agda</a> exercises and wondering if we can achieve the same level of theories with dependent types. With simple types, the definition usually goes like the following:</p>
<pre><code>data Type : Set where -- well formed types
    ...
    _→̇_ : Type → Type → Type

Context = List Type

data _∋_ : Context → Type → Set where -- De Bruijn indices
    here : {Γ : Context} → {A : Type}
        → Γ ‚ A ∋ A
    there : {Γ : Context} → {A B : Type}
        → Γ ∋ B
        → Γ ‚ A ∋ B

data _⊢_ : Context → Type → Set where -- well formed terms
    lookup : {Γ : Context} → {A : Type} -- variables
        → Γ ∋ A
        → Γ ⊢ A
    λ̇_ : {Γ : Context} → {A B : Type}
        → Γ ‚ A ⊢ B
        → Γ ⊢ A →̇ B
    _·_ : {Γ : Context} → {A B : Type}
        → Γ ⊢ A →̇ B
        → Γ ⊢ A
        → Γ ⊢ B
    ...

</code></pre>
<p>On the other hand, dependent types usually use mutual inductive-inductive/recursive definitions that goes like the following (sorry if I miss any constructors, and usage of the dot notation):</p>
<pre><code>data Context : Set
data Substitution : Context → Context → Set

data Type : Context → Set
data _⊢_ : (Γ : Context) → Type Γ → Set

data Context where
    [] : Context
    _‚_ : (Γ : Context) → Type Γ → Context

data Type where
    Ṡet : {Γ : Context} → Type Γ
    El : {Γ : Context} → Γ ⊢ Ṡet → Type Γ

    _→̇_ : {Γ : Context} → (A : Type Γ) → Type (Γ ‚ A) → Type Γ

    substitute-type : {Γ Δ : Context} → Substitution Δ Γ → Type Γ → Type Δ

data Substitution where
    [] : {Δ : Context} → Substitution Δ []
    _‚_ : {Γ Δ : Context} → {A : Type Γ} → (σ : Substitution Δ Γ) → (Δ ⊢ substitute-type σ A) → Substitution Δ (Γ ‚ A)

    id : {Γ : Context} → Substitution Γ Γ
    _∘_ : {Γ Δ Ε : Context} → Substitution Δ Γ → Substitution Ε Δ → Substitution Ε Γ

    p₁ : {Γ Δ : Context} → {A : Type Γ} → Substitution Δ (Γ ‚ A) → Substitution Δ Γ

shift : {Γ : Context} → {A : Type Γ} → Substitution (Γ ‚ A) Γ
shift = p₁ id

data _⊢_ where

    here : {Γ : Context} → {A : Type Γ}
        → Γ ‚ A ⊢ substitute-type shift A

    substitute-term : {Γ Δ : Context} → (σ : Substitution Δ Γ) → {A : Type Γ} → (Γ ⊢ A) → (Δ ⊢ substitute-type σ A)

    p₂ : {Γ Δ : Context} → {A : Type Γ} → (σ : Substitution Δ (Γ ‚ A)) → (Δ ⊢ substitute-type (p₁ σ) A)

    λ̇_ : {Γ : Context} → {A : Type Γ} → {B : Type (Γ ‚ A)}
        → Γ ‚ A ⊢ B
        → Γ ⊢ A →̇ B
    
    ȧpp : {Γ : Context} → {A : Type Γ} → {B : Type (Γ ‚ A)}
        → Γ ⊢ A →̇ B
        → Γ ‚ A ⊢ B
</code></pre>
<p>I found a few papers about this subject (see ref section of <a href="https://ncatlab.org/nlab/show/internal+type+theory" rel="noreferrer">https://ncatlab.org/nlab/show/internal+type+theory</a>, as well as <a href="http://www.cs.nott.ac.uk/%7Epsztxa/publ/tt-in-tt.pdf" rel="noreferrer">Type Theory in Type Theory using Quotient Inductive Types</a>, <a href="https://drops.dagstuhl.de/opus/volltexte/2016/5972/pdf/LIPIcs-FSCD-2016-6.pdf" rel="noreferrer">Normalisation by Evaluation for Dependent Types</a>, and many others). All of the implementation seems to use <a href="http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/explicit+substitution" rel="noreferrer">Explicit Substitution</a>. I think the usage is due to the context category in the category with families/attributes models, but on syntactical level, can we show substitution must be a first party operation (as some sort of dependent list of types) instead of a meta-theoretical operation for dependent types? I tried to define it but it goes into a circular definition (since the dependent list of types uses the action of substitution on types). Is it so happens that we can define substitution in the meta-theory (i.e., agda) in the simple type case?</p>

CC BY-SA 4.0
2022-02-09T07:05:34.510Z
What's the problem with the definition? It's not "circular", just recursive: substitution of $n+1$ variables relies on substitution of $n$ variables being already defined.
Andrej Bauer
CC BY-SA 4.0
2022-02-09T08:01:46.473Z
You may be able to do that with induction-recursion. But that probably means a lot of equational reasoning.
Trebor
<type-theory><dependent-type><model-theory><agda>
Is there a way to define dependent types without explicit substitutions internally within agda?
Kaa1el
# Is there a way to define dependent types without explicit substitutions internally within agda?

(Asked by: username_0 on 2022-02-08)

I am playing around the Programming Language Foundations in Agda exercises and wondering if we can achieve the same level of theories with dependent types. With simple types, the definition usually goes like the following:
data Type : Set where -- well formed types
    ...
    _→̇_ : Type → Type → Type

Context = List Type

data _∋_ : Context → Type → Set where -- De Bruijn indices
    here : {Γ : Context} → {A : Type}
        → Γ ‚ A ∋ A
    there : {Γ : Context} → {A B : Type}
        → Γ ∋ B
        → Γ ‚ A ∋ B

data _⊢_ : Context → Type → Set where -- well formed terms
    lookup : {Γ : Context} → {A : Type} -- variables
        → Γ ∋ A
        → Γ ⊢ A
    λ̇_ : {Γ : Context} → {A B : Type}
        → Γ ‚ A ⊢ B
        → Γ ⊢ A →̇ B
    _·_ : {Γ : Context} → {A B : Type}
        → Γ ⊢ A →̇ B
        → Γ ⊢ A
        → Γ ⊢ B
    ...


On the other hand, dependent types usually use mutual inductive-inductive/recursive definitions that goes like the following (sorry if I miss any constructors, and usage of the dot notation):
data Context : Set
data Substitution : Context → Context → Set

data Type : Context → Set
data _⊢_ : (Γ : Context) → Type Γ → Set

data Context where
    [] : Context
    _‚_ : (Γ : Context) → Type Γ → Context

data Type where
    Ṡet : {Γ : Context} → Type Γ
    El : {Γ : Context} → Γ ⊢ Ṡet → Type Γ

    _→̇_ : {Γ : Context} → (A : Type Γ) → Type (Γ ‚ A) → Type Γ

    substitute-type : {Γ Δ : Context} → Substitution Δ Γ → Type Γ → Type Δ

data Substitution where
    [] : {Δ : Context} → Substitution Δ []
    _‚_ : {Γ Δ : Context} → {A : Type Γ} → (σ : Substitution Δ Γ) → (Δ ⊢ substitute-type σ A) → Substitution Δ (Γ ‚ A)

    id : {Γ : Context} → Substitution Γ Γ
    _∘_ : {Γ Δ Ε : Context} → Substitution Δ Γ → Substitution Ε Δ → Substitution Ε Γ

    p₁ : {Γ Δ : Context} → {A : Type Γ} → Substitution Δ (Γ ‚ A) → Substitution Δ Γ

shift : {Γ : Context} → {A : Type Γ} → Substitution (Γ ‚ A) Γ
shift = p₁ id

data _⊢_ where

    here : {Γ : Context} → {A : Type Γ}
        → Γ ‚ A ⊢ substitute-type shift A

    substitute-term : {Γ Δ : Context} → (σ : Substitution Δ Γ) → {A : Type Γ} → (Γ ⊢ A) → (Δ ⊢ substitute-type σ A)

    p₂ : {Γ Δ : Context} → {A : Type Γ} → (σ : Substitution Δ (Γ ‚ A)) → (Δ ⊢ substitute-type (p₁ σ) A)

    λ̇_ : {Γ : Context} → {A : Type Γ} → {B : Type (Γ ‚ A)}
        → Γ ‚ A ⊢ B
        → Γ ⊢ A →̇ B
    
    ȧpp : {Γ : Context} → {A : Type Γ} → {B : Type (Γ ‚ A)}
        → Γ ⊢ A →̇ B
        → Γ ‚ A ⊢ B

I found a few papers about this subject (see ref section of https://ncatlab.org/nlab/show/internal+type+theory, as well as Type Theory in Type Theory using Quotient Inductive Types, Normalisation by Evaluation for Dependent Types, and many others). All of the implementation seems to use Explicit Substitution. I think the usage is due to the context category in the category with families/attributes models, but on syntactical level, can we show substitution must be a first party operation (as some sort of dependent list of types) instead of a meta-theoretical operation for dependent types? I tried to define it but it goes into a circular definition (since the dependent list of types uses the action of substitution on types). Is it so happens that we can define substitution in the meta-theory (i.e., agda) in the simple type case?

**Tags:** type-theory, dependent-type, model-theory, agda
> **Comments:**
> **username_1**: What's the problem with the definition? It's not "circular", just recursive: substitution of $n+1$ variables relies on substitution of $n$ variables being already defined.  
> **username_2**: You may be able to do that with induction-recursion. But that probably means a lot of equational reasoning.  

---

## 1 answers

### Answer by username_2 on 2022-02-14. Score: 4 | Accepted answer

The thing is, the definition is "too" dependent. In order to define the type of substitution or renaming, you need to something like
Substitution : Context -> Context -> Set
Substitution Γ Δ = ∀ {α} -> Var Γ α -> Term Δ {!  !}

Here Var and Term corresponds to your _∋_ and _⊢_. Now you can't fill in the hole, because it is expecting something of type Type Δ. But α is of type Type Γ. This means you need to make a substitution depending on the previous variables.
So, whenever you extend a substitution list by a little, you will have to refer to the previously built part. This means that defining substitution in the PLFA style doesn't work, and you will have to use an inductive type for substitution.
Ok, fair. So let's try the easy one. Let's define renaming, which, different from the PLFA style, needs to keep the variables in order (the PLFA definition allows for arbitrary permutations) to keep the dependency straight. So the obvious thing is to have keep and drop as the constructors. You may realize that this is analogous to the inductive list-containment predicate. Let's start out:
data Ren : Context -> Context -> Set
rent : Ren Δ Γ -> Type Γ -> Type Δ

where rent stands for renaming on types. And you do get to define:
data Ren where
    stop : Ren ∅ ∅
    drop : Ren Γ Δ -> Ren (Γ ◂ α) Δ
    keep : (ρ : Ren Γ Δ) -> Ren (Γ ◂ rent ρ α) (Δ ◂ α)

where the black triangle (input sequence \t) is my queer notation for a context extension. Now you just need an element ren-id : Ren Γ Γ, and then you get to construct drop ren-id as the $\mathsf p$ thing in the literature.
But there is a problem, you can't just define ren-id by induction:
ren-id : Ren Γ Γ
ren-id {Γ = ∅} = stop
ren-id {Γ = Γ ◂ α} = {! keep !}

The types don't match up. You need to simultaneously prove that renaming with ren-id is the identity. But at this point you haven't even defined rent yet! So let's define that first. When you encounter type variables, you need to fetch the renamed variable, and to fetch that, you need to first define the variables:
data Var where
     : Var (Γ ◂ α) (rent  α)
    _ : Var Γ α -> Var (Γ ◂ β) (rent  α)

fetch : (ρ : Ren Γ Δ) -> Var Δ α -> Var Γ (rent ρ α)
fetch ρ  = {!   !}
fetch ρ ( i) = {!   !}

rent ρ ⋆ = ⋆
rent ρ (var i) = var (fetch ρ i)
rent ρ (Π t) = Π {!   !}
rent ρ (t ⇒ s) = rent ρ t ⇒ rent ρ s

I'm using system F as an example. But this looks bad: the signature of fetch has rent in it again! By the way, this triggers a bug in Agda, which I'm going to report. You can go on fiddling with that, but I think this demonstrates that it is not going to work out.


---

