Is there a way to define dependent types without explicit substitutions internally within agda?

Question

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
    Ṡet : {Γ : Context} → Type Γ
    El : {Γ : Context} → Γ ⊢ Ṡ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
    
    ȧ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?

Answer 1

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.