------------------------------------------------------------------------
-- The Agda standard library
--
-- Substitution lemmas
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Fin.Substitution.Lemmas where

open import Data.Fin.Substitution
open import Data.Nat.Base using (; zero; suc; _+_)
open import Data.Fin.Base using (Fin; zero; suc; lift)
open import Data.Vec.Base using (lookup; []; _∷_; map)
import Data.Vec.Properties as Vec
open import Function.Base as Fun using (_∘_; _$_; flip)
open import Level using (Level; _⊔_)
open import Relation.Binary.PropositionalEquality.Core as 
  using (_≡_; refl; sym; cong; cong₂)
open import Relation.Binary.PropositionalEquality.Properties
  using (module ≡-Reasoning)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star; ε; _◅_; _▻_)
open ≡-Reasoning
open import Relation.Unary using (Pred)

private
  variable
     ℓ₁ ℓ₂ : Level
    m n o p : 

------------------------------------------------------------------------
-- A lemma which does not refer to any substitutions.

lift-commutes :  k j (x : Fin (j + (k + n))) 
                lift j suc (lift j (lift k suc) x) 
                lift j (lift (suc k) suc) (lift j suc x)
lift-commutes k zero    x       = refl
lift-commutes k (suc j) zero    = refl
lift-commutes k (suc j) (suc x) = cong suc (lift-commutes k j x)

------------------------------------------------------------------------
-- The modules below prove a number of substitution lemmas, on the
-- assumption that the underlying substitution machinery satisfies
-- certain properties.

record Lemmas₀ (T : Pred  ) : Set  where
  field simple : Simple T

  open Simple simple

  extensionality : {ρ₁ ρ₂ : Sub T m n} 
                   (∀ x  lookup ρ₁ x  lookup ρ₂ x)  ρ₁  ρ₂
  extensionality {ρ₁ = []}      {[]}       hyp = refl
  extensionality {ρ₁ = t₁  ρ₁} { t₂  ρ₂} hyp with hyp zero
  extensionality {ρ₁ = t₁  ρ₁} {.t₁  ρ₂} hyp | refl =
    cong (_∷_ t₁) (extensionality (hyp  suc))

  id-↑⋆ :  {n} k  id ↑⋆ k  id {k + n}
  id-↑⋆ zero    = refl
  id-↑⋆ (suc k) = begin
    (id ↑⋆ k)  ≡⟨ cong _↑ (id-↑⋆ k) 
    id         

  lookup-map-weaken-↑⋆ :  k x {ρ : Sub T m n} 
                         lookup (map weaken ρ ↑⋆ k) x 
                         lookup ((ρ ) ↑⋆ k) (lift k suc x)
  lookup-map-weaken-↑⋆ zero    x           = refl
  lookup-map-weaken-↑⋆ (suc k) zero        = refl
  lookup-map-weaken-↑⋆ (suc k) (suc x) {ρ} = begin
    lookup (map weaken (map weaken ρ ↑⋆ k)) x        ≡⟨ Vec.lookup-map x weaken (map weaken ρ ↑⋆ k) 
    weaken (lookup (map weaken ρ ↑⋆ k) x)            ≡⟨ cong weaken (lookup-map-weaken-↑⋆ k x) 
    weaken (lookup ((ρ ) ↑⋆ k) (lift k suc x))      ≡⟨ sym $ Vec.lookup-map (lift k suc x) weaken ((ρ ) ↑⋆ k) 
    lookup (map weaken ((ρ ) ↑⋆ k)) (lift k suc x)  

record Lemmas₁ (T : Pred  ) : Set  where
  field lemmas₀ : Lemmas₀ T

  open Lemmas₀ lemmas₀
  open Simple simple

  field weaken-var :  {n} {x : Fin n}  weaken (var x)  var (suc x)

  lookup-map-weaken :  x {y} {ρ : Sub T m n} 
                      lookup             ρ  x  var      y 
                      lookup (map weaken ρ) x  var (suc y)
  lookup-map-weaken x {y} {ρ} hyp = begin
    lookup (map weaken ρ) x  ≡⟨ Vec.lookup-map x weaken ρ 
    weaken (lookup ρ x)      ≡⟨ cong weaken hyp 
    weaken (var y)           ≡⟨ weaken-var 
    var (suc y)              

  mutual

    lookup-id : (x : Fin n)  lookup id x  var x
    lookup-id zero    = refl
    lookup-id (suc x) = lookup-wk x

    lookup-wk : (x : Fin n)  lookup wk x  var (suc x)
    lookup-wk x = lookup-map-weaken x {ρ = id} (lookup-id x)

  lookup-↑⋆ : (f : Fin m  Fin n) {ρ : Sub T m n} 
              (∀ x  lookup ρ x  var (f x)) 
               k x  lookup (ρ ↑⋆ k) x  var (lift k f x)
  lookup-↑⋆ f         hyp zero    x       = hyp x
  lookup-↑⋆ f         hyp (suc k) zero    = refl
  lookup-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) =
    lookup-map-weaken x {ρ = ρ ↑⋆ k} (lookup-↑⋆ f hyp k x)

  lookup-lift-↑⋆ : (f : Fin n  Fin m) {ρ : Sub T m n} 
                   (∀ x  lookup ρ (f x)  var x) 
                    k x  lookup (ρ ↑⋆ k) (lift k f x)  var x
  lookup-lift-↑⋆ f         hyp zero    x       = hyp x
  lookup-lift-↑⋆ f         hyp (suc k) zero    = refl
  lookup-lift-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) =
    lookup-map-weaken (lift k f x) {ρ = ρ ↑⋆ k} (lookup-lift-↑⋆ f hyp k x)

  lookup-wk-↑⋆ :  k (x : Fin (k + n)) 
                 lookup (wk ↑⋆ k) x  var (lift k suc x)
  lookup-wk-↑⋆ = lookup-↑⋆ suc lookup-wk

  lookup-wk-↑⋆-↑⋆ :  k j (x : Fin (j + (k + n))) 
                    lookup (wk ↑⋆ k ↑⋆ j) x 
                    var (lift j (lift k suc) x)
  lookup-wk-↑⋆-↑⋆ k = lookup-↑⋆ (lift k suc) (lookup-wk-↑⋆ k)

  lookup-sub-↑⋆ :  {t} k (x : Fin (k + n)) 
                  lookup (sub t ↑⋆ k) (lift k suc x)  var x
  lookup-sub-↑⋆ = lookup-lift-↑⋆ suc lookup-id

  open Lemmas₀ lemmas₀ public

record Lemmas₂ (T : Pred  ) : Set  where
  field
    lemmas₁     : Lemmas₁ T
    application : Application T T

  open Lemmas₁ lemmas₁

  subst : Subst T
  subst = record { simple = simple; application = application }

  open Subst subst

  field var-/ :  {m n x} {ρ : Sub T m n}  var x / ρ  lookup ρ x

  suc-/-sub :  {x} {t : T n}  var (suc x) / sub t  var x
  suc-/-sub {x = x} {t} = begin
    var (suc x) / sub t     ≡⟨ var-/ 
    lookup (sub t) (suc x)  ≡⟨ refl 
    lookup id x             ≡⟨ lookup-id x 
    var x                   

  lookup-⊙ :  x {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} 
             lookup (ρ₁  ρ₂) x  lookup ρ₁ x / ρ₂
  lookup-⊙ x {ρ₁} {ρ₂} = Vec.lookup-map x  t  t / ρ₂) ρ₁

  lookup-⨀ :  x (ρs : Subs T m n) 
             lookup ( ρs) x  var x /✶ ρs
  lookup-⨀ x ε                = lookup-id x
  lookup-⨀ x (ρ  ε)          = sym var-/
  lookup-⨀ x (ρ  (ρ′  ρs′)) = begin
    lookup ( (ρ  ρs)) x  ≡⟨ refl 
    lookup ( ρs  ρ) x    ≡⟨ lookup-⊙ x {ρ₁ =  (ρ′  ρs′)} 
    lookup ( ρs) x / ρ    ≡⟨ cong₂ _/_ (lookup-⨀ x (ρ′  ρs′)) refl 
    var x /✶ ρs / ρ        
    where ρs = ρ′  ρs′

  id-⊙ : {ρ : Sub T m n}  id  ρ  ρ
  id-⊙ {ρ = ρ} = extensionality λ x  begin
    lookup (id  ρ) x  ≡⟨ lookup-⊙ x {ρ₁ = id} 
    lookup  id x / ρ   ≡⟨ cong₂ _/_ (lookup-id x) refl 
    var x        / ρ   ≡⟨ var-/ 
    lookup ρ x         

  lookup-wk-↑⋆-⊙ :  k {x} {ρ : Sub T (k + suc m) n} 
                   lookup (wk ↑⋆ k  ρ) x  lookup ρ (lift k suc x)
  lookup-wk-↑⋆-⊙ k {x} {ρ} = begin
    lookup (wk ↑⋆ k  ρ) x   ≡⟨ lookup-⊙ x {ρ₁ = wk ↑⋆ k} 
    lookup (wk ↑⋆ k) x / ρ   ≡⟨ cong₂ _/_ (lookup-wk-↑⋆ k x) refl 
    var (lift k suc x) / ρ   ≡⟨ var-/ 
    lookup ρ (lift k suc x)  

  wk-⊙-sub′ :  {t : T n} k  wk ↑⋆ k  sub t ↑⋆ k  id
  wk-⊙-sub′ {t = t} k = extensionality λ x  begin
    lookup (wk ↑⋆ k  sub t ↑⋆ k) x     ≡⟨ lookup-wk-↑⋆-⊙ k 
    lookup (sub t ↑⋆ k) (lift k suc x)  ≡⟨ lookup-sub-↑⋆ k x 
    var x                               ≡⟨ sym (lookup-id x) 
    lookup id x                         

  wk-⊙-sub : {t : T n}  wk  sub t  id
  wk-⊙-sub = wk-⊙-sub′ zero

  var-/-wk-↑⋆ :  {n} k (x : Fin (k + n)) 
                var x / wk ↑⋆ k  var (lift k suc x)
  var-/-wk-↑⋆ k x = begin
    var x / wk ↑⋆ k     ≡⟨ var-/ 
    lookup (wk ↑⋆ k) x  ≡⟨ lookup-wk-↑⋆ k x 
    var (lift k suc x)  

  wk-↑⋆-⊙-wk :  k j 
               wk {n} ↑⋆ k ↑⋆ j  wk ↑⋆ j 
               wk ↑⋆ j  wk ↑⋆ suc k ↑⋆ j
  wk-↑⋆-⊙-wk k j = extensionality λ x  begin
    lookup (wk ↑⋆ k ↑⋆ j  wk ↑⋆ j) x               ≡⟨ lookup-⊙ x {ρ₁ = wk ↑⋆ k ↑⋆ j} 
    lookup (wk ↑⋆ k ↑⋆ j) x / wk ↑⋆ j               ≡⟨ cong₂ _/_ (lookup-wk-↑⋆-↑⋆ k j x) refl 
    var (lift j (lift k suc) x) / wk ↑⋆ j           ≡⟨ var-/-wk-↑⋆ j (lift j (lift k suc) x) 
    var (lift j suc (lift j (lift k suc) x))        ≡⟨ cong var (lift-commutes k j x) 
    var (lift j (lift (suc k) suc) (lift j suc x))  ≡⟨ sym (lookup-wk-↑⋆-↑⋆ (suc k) j (lift j suc x)) 
    lookup (wk ↑⋆ suc k ↑⋆ j) (lift j suc x)        ≡⟨ sym var-/ 
    var (lift j suc x) / wk ↑⋆ suc k ↑⋆ j           ≡⟨ cong₂ _/_ (sym (lookup-wk-↑⋆ j x)) refl 
    lookup (wk ↑⋆ j) x / wk ↑⋆ suc k ↑⋆ j           ≡⟨ sym (lookup-⊙ x {ρ₁ = wk ↑⋆ j}) 
    lookup (wk ↑⋆ j  wk ↑⋆ suc k ↑⋆ j) x           

  open Subst   subst   public hiding (simple; application)
  open Lemmas₁ lemmas₁ public

record Lemmas₃ (T : Pred  ) : Set  where
  field lemmas₂ : Lemmas₂ T

  open Lemmas₂ lemmas₂

  field
    /✶-↑✶ :  {m n} (ρs₁ ρs₂ : Subs T m n) 
            (∀ k x  var x /✶ ρs₁ ↑✶ k  var x /✶ ρs₂ ↑✶ k) 
             k t  t /✶ ρs₁ ↑✶ k  t /✶ ρs₂ ↑✶ k

  /✶-↑✶′ : (ρs₁ ρs₂ : Subs T m n) 
           (∀ k   (ρs₁ ↑✶ k)   (ρs₂ ↑✶ k)) 
            k t  t /✶ ρs₁ ↑✶ k  t /✶ ρs₂ ↑✶ k
  /✶-↑✶′ ρs₁ ρs₂ hyp = /✶-↑✶ ρs₁ ρs₂  k x  begin
    var x /✶ ρs₁ ↑✶ k        ≡⟨ sym (lookup-⨀ x (ρs₁ ↑✶ k)) 
    lookup ( (ρs₁ ↑✶ k)) x  ≡⟨ cong (flip lookup x) (hyp k) 
    lookup ( (ρs₂ ↑✶ k)) x  ≡⟨ lookup-⨀ x (ρs₂ ↑✶ k) 
    var x /✶ ρs₂ ↑✶ k        )

  id-vanishes : (t : T n)  t / id  t
  id-vanishes = /✶-↑✶′ (ε  id) ε id-↑⋆ zero

  ⊙-id : {ρ : Sub T m n}  ρ  id  ρ
  ⊙-id {ρ = ρ} = begin
    map  t  t / id) ρ  ≡⟨ Vec.map-cong id-vanishes ρ 
    map Fun.id         ρ  ≡⟨ Vec.map-id ρ 
    ρ                     

  open Lemmas₂ lemmas₂ public hiding (wk-⊙-sub′)

record Lemmas₄ (T : Pred  ) : Set  where
  field lemmas₃ : Lemmas₃ T

  open Lemmas₃ lemmas₃

  field /-wk :  {n} {t : T n}  t / wk  weaken t

  private

    ↑-distrib′ : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} 
                 (∀ t  t / ρ₂ / wk  t / wk / ρ₂ ) 
                 (ρ₁  ρ₂)   ρ₁   ρ₂ 
    ↑-distrib′ {ρ₁ = ρ₁} {ρ₂} hyp = begin
      (ρ₁  ρ₂)                              ≡⟨ refl 
      var zero         map weaken (ρ₁  ρ₂)  ≡⟨ cong₂ _∷_ (sym var-/) lemma 
      var zero / ρ₂   map weaken ρ₁  ρ₂   ≡⟨ refl 
      ρ₁   ρ₂                              
      where
      lemma = begin
        map weaken (map  t  t / ρ₂) ρ₁)    ≡⟨ sym (Vec.map-∘ _ _ _) 
        map  t  weaken (t / ρ₂)) ρ₁        ≡⟨ Vec.map-cong  t  begin
                                                   weaken (t / ρ₂)  ≡⟨ sym /-wk 
                                                   t / ρ₂ / wk      ≡⟨ hyp t 
                                                   t / wk / ρ₂     ≡⟨ cong₂ _/_ /-wk refl 
                                                   weaken t / ρ₂   ) ρ₁ 
        map  t  weaken t / ρ₂ ) ρ₁        ≡⟨ Vec.map-∘ _ _ _ 
        map  t  t / ρ₂ ) (map weaken ρ₁)  

    ↑⋆-distrib′ : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} 
                  (∀ k t  t / ρ₂ ↑⋆ k / wk  t / wk / ρ₂ ↑⋆ suc k) 
                   k  (ρ₁  ρ₂) ↑⋆ k  ρ₁ ↑⋆ k  ρ₂ ↑⋆ k
    ↑⋆-distrib′                hyp zero    = refl
    ↑⋆-distrib′ {ρ₁ = ρ₁} {ρ₂} hyp (suc k) = begin
      (ρ₁  ρ₂) ↑⋆ suc k         ≡⟨ cong _↑ (↑⋆-distrib′ hyp k) 
      (ρ₁ ↑⋆ k  ρ₂ ↑⋆ k)       ≡⟨ ↑-distrib′ (hyp k) 
      ρ₁ ↑⋆ suc k  ρ₂ ↑⋆ suc k  

  map-weaken : {ρ : Sub T m n}  map weaken ρ  ρ  wk
  map-weaken {ρ = ρ} = begin
    map weaken ρ          ≡⟨ Vec.map-cong  _  sym /-wk) ρ 
    map  t  t / wk) ρ  ≡⟨ refl 
    ρ  wk                

  private

    ⊙-wk′ :  {ρ : Sub T m n} k 
            ρ ↑⋆ k  wk ↑⋆ k  wk ↑⋆ k  ρ  ↑⋆ k
    ⊙-wk′ {ρ = ρ} k = sym (begin
      wk ↑⋆ k  ρ  ↑⋆ k  ≡⟨ lemma 
      map weaken ρ ↑⋆ k   ≡⟨ cong  ρ′  ρ′ ↑⋆ k) map-weaken 
      (ρ  wk) ↑⋆ k       ≡⟨ ↑⋆-distrib′  k t 
                               /✶-↑✶′ (ε  wk ↑⋆ k  wk) (ε  wk  wk ↑⋆ suc k)
                                      (wk-↑⋆-⊙-wk k) zero t) k 
      ρ ↑⋆ k  wk ↑⋆ k    )
      where
      lemma = extensionality λ x  begin
        lookup (wk ↑⋆ k  ρ  ↑⋆ k) x     ≡⟨ lookup-wk-↑⋆-⊙ k 
        lookup (ρ  ↑⋆ k) (lift k suc x)  ≡⟨ sym (lookup-map-weaken-↑⋆ k x) 
        lookup (map weaken ρ ↑⋆ k) x      

  ⊙-wk : {ρ : Sub T m n}  ρ  wk  wk  ρ 
  ⊙-wk = ⊙-wk′ zero

  wk-commutes :  {ρ : Sub T m n} t 
                t / ρ / wk  t / wk / ρ 
  wk-commutes {ρ = ρ} = /✶-↑✶′ (ε  ρ  wk) (ε  wk  ρ ) ⊙-wk′ zero

  ↑⋆-distrib : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} 
                k  (ρ₁  ρ₂) ↑⋆ k  ρ₁ ↑⋆ k  ρ₂ ↑⋆ k
  ↑⋆-distrib = ↑⋆-distrib′  _  wk-commutes)

  /-⊙ :  {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} t 
        t / ρ₁  ρ₂  t / ρ₁ / ρ₂
  /-⊙ {ρ₁ = ρ₁} {ρ₂} t =
    /✶-↑✶′ (ε  ρ₁  ρ₂) (ε  ρ₁  ρ₂) ↑⋆-distrib zero t

  ⊙-assoc : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} {ρ₃ : Sub T o p} 
            ρ₁  (ρ₂  ρ₃)  (ρ₁  ρ₂)  ρ₃
  ⊙-assoc {ρ₁ = ρ₁} {ρ₂} {ρ₃} = begin
    map  t  t / ρ₂  ρ₃) ρ₁                  ≡⟨ Vec.map-cong /-⊙ ρ₁ 
    map  t  t / ρ₂ / ρ₃) ρ₁                  ≡⟨ Vec.map-∘ _ _ _ 
    map  t  t / ρ₃) (map  t  t / ρ₂) ρ₁)  

  map-weaken-⊙-sub :  {ρ : Sub T m n} {t}  map weaken ρ  sub t  ρ
  map-weaken-⊙-sub {ρ = ρ} {t} = begin
    map weaken ρ  sub t  ≡⟨ cong₂ _⊙_ map-weaken refl 
    ρ  wk  sub t        ≡⟨ sym ⊙-assoc 
    ρ  (wk  sub t)      ≡⟨ cong (_⊙_ ρ) wk-⊙-sub 
    ρ  id                ≡⟨ ⊙-id 
    ρ                     

  sub-⊙ :  {ρ : Sub T m n} t  sub t  ρ  ρ   sub (t / ρ)
  sub-⊙ {ρ = ρ} t = begin
    sub t  ρ                           ≡⟨ refl 
    t / ρ  id  ρ                      ≡⟨ cong (_∷_ (t / ρ)) id-⊙ 
    t / ρ  ρ                           ≡⟨ cong (_∷_ (t / ρ)) (sym map-weaken-⊙-sub) 
    t / ρ  map weaken ρ  sub (t / ρ)  ≡⟨ cong₂ _∷_ (sym var-/) refl 
    ρ   sub (t / ρ)                   

  suc-/-↑ :  {ρ : Sub T m n} x 
            var (suc x) / ρ   var x / ρ / wk
  suc-/-↑ {ρ = ρ} x = begin
    var (suc x) / ρ         ≡⟨ var-/ 
    lookup (map weaken ρ) x  ≡⟨ cong (flip lookup x) (map-weaken {ρ = ρ}) 
    lookup (ρ  wk)       x  ≡⟨ lookup-⊙ x {ρ₁ = ρ} 
    lookup ρ x / wk          ≡⟨ cong₂ _/_ (sym var-/) refl 
    var x / ρ / wk           

  weaken-↑ :  t {ρ : Sub T m n}  weaken t / (ρ )  weaken (t / ρ)
  weaken-↑ t {ρ} = begin
    weaken t / (ρ ) ≡⟨ cong (_/ ρ ) (sym /-wk) 
    t / wk / ρ      ≡⟨ sym (wk-commutes t) 
    t / ρ / wk       ≡⟨ /-wk 
    weaken (t / ρ)   

  open Lemmas₃ lemmas₃ public
    hiding (/✶-↑✶; /✶-↑✶′; wk-↑⋆-⊙-wk;
            lookup-wk-↑⋆-⊙; lookup-map-weaken-↑⋆)

------------------------------------------------------------------------
-- For an example of how AppLemmas can be used, see
-- Data.Fin.Substitution.List.

record AppLemmas (T₁ : Pred  ℓ₁) (T₂ : Pred  ℓ₂) : Set (ℓ₁  ℓ₂) where
  field
    application : Application T₁ T₂
    lemmas₄     : Lemmas₄ T₂

  open Application application using (_/_; _/✶_)
  open Lemmas₄ lemmas₄
    using (id; _⊙_; wk; weaken; sub; _↑; ; /-wk) renaming (_/_ to _⊘_)

  field
    id-vanishes :  {n} (t : T₁ n)  t / id  t
    /-⊙         :  {m n k} {ρ₁ : Sub T₂ m n} {ρ₂ : Sub T₂ n k} t 
                  t / ρ₁  ρ₂  t / ρ₁ / ρ₂

  private module L₄ = Lemmas₄ lemmas₄

  /-⨀ :  t (ρs : Subs T₂ m n)  t /  ρs  t /✶ ρs
  /-⨀ t ε                = id-vanishes t
  /-⨀ t (ρ  ε)          = refl
  /-⨀ t (ρ  (ρ′  ρs′)) = begin
    t /  ρs  ρ  ≡⟨ /-⊙ t 
    t /  ρs / ρ  ≡⟨ cong₂ _/_ (/-⨀ t (ρ′  ρs′)) refl 
    t /✶ ρs / ρ   
    where ρs = ρ′  ρs′

  ⨀→/✶ : (ρs₁ ρs₂ : Subs T₂ m n) 
          ρs₁   ρs₂   t  t /✶ ρs₁  t /✶ ρs₂
  ⨀→/✶ ρs₁ ρs₂ hyp t = begin
    t /✶ ρs₁   ≡⟨ sym (/-⨀ t ρs₁) 
    t /  ρs₁  ≡⟨ cong (_/_ t) hyp 
    t /  ρs₂  ≡⟨ /-⨀ t ρs₂ 
    t /✶ ρs₂   

  wk-commutes :  {ρ : Sub T₂ m n} t 
                t / ρ / wk  t / wk / ρ 
  wk-commutes {ρ = ρ} = ⨀→/✶ (ε  ρ  wk) (ε  wk  ρ ) L₄.⊙-wk

  sub-commutes :  {t′} {ρ : Sub T₂ m n} t 
                 t / sub t′ / ρ  t / ρ  / sub (t′  ρ)
  sub-commutes {t′ = t′} {ρ} =
    ⨀→/✶ (ε  sub t′  ρ) (ε  ρ   sub (t′  ρ)) (L₄.sub-⊙ t′)

  wk-sub-vanishes :  {t′} (t : T₁ n)  t / wk / sub t′  t
  wk-sub-vanishes {t′ = t′} = ⨀→/✶ (ε  wk  sub t′) ε L₄.wk-⊙-sub

  /-weaken :  {ρ : Sub T₂ m n} t  t / map weaken ρ  t / ρ / wk
  /-weaken {ρ = ρ} = ⨀→/✶ (ε  map weaken ρ) (ε  ρ  wk) L₄.map-weaken

  open Application application public
  open L₄ public
    hiding (application; _⊙_; _/_; _/✶_;
            id-vanishes; /-⊙; wk-commutes)

record Lemmas₅ {} (T : Pred  ) : Set  where
  field lemmas₄ : Lemmas₄ T

  private module L₄ = Lemmas₄ lemmas₄

  appLemmas : AppLemmas T T
  appLemmas = record
    { application = L₄.application
    ; lemmas₄     = lemmas₄
    ; id-vanishes = L₄.id-vanishes
    ; /-⊙         = L₄./-⊙
    }

  open AppLemmas appLemmas public hiding (lemmas₄)

------------------------------------------------------------------------
-- Instantiations and code for facilitating instantiations

-- Lemmas about variable substitutions (renamings).

module VarLemmas where

  open VarSubst

  lemmas₃ : Lemmas₃ Fin
  lemmas₃ = record
    { lemmas₂ = record
      { lemmas₁ = record
        { lemmas₀ = record
          { simple = simple
          }
        ; weaken-var = refl
        }
      ; application = application
      ; var-/       = refl
      }
    ; /✶-↑✶ = λ _ _ hyp  hyp
    }

  private module L₃ = Lemmas₃ lemmas₃

  lemmas₅ : Lemmas₅ Fin
  lemmas₅ = record
    { lemmas₄ = record
      { lemmas₃ = lemmas₃
      ; /-wk    = L₃.lookup-wk _
      }
    }

  open Lemmas₅ lemmas₅ public hiding (lemmas₃)

-- Lemmas about "term" substitutions.

record TermLemmas (T :   Set) : Set₁ where
  field
    termSubst : TermSubst T

  open TermSubst termSubst
  private module T = TermSubst termSubst

  field
    app-var :  {T′} {lift : Lift T′ T} {m n x} {ρ : Sub T′ m n} 
              app lift (var x) ρ  Lift.lift lift (lookup ρ x)
    /✶-↑✶   :  {T₁ T₂} {lift₁ : Lift T₁ T} {lift₂ : Lift T₂ T} 
              let open Lifted lift₁
                    using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
                  open Lifted lift₂
                    using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)
              in
               {m n} (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n) 
              (∀ k x  var x /✶₁ ρs₁ ↑✶₁ k  var x /✶₂ ρs₂ ↑✶₂ k) 
               k t  t /✶₁ ρs₁ ↑✶₁ k  t /✶₂ ρs₂ ↑✶₂ k

  private module V = VarLemmas

  lemmas₃ : Lemmas₃ T
  lemmas₃ = record
    { lemmas₂ = record
      { lemmas₁ = record
        { lemmas₀ = record
          { simple = simple
          }
        ; weaken-var = λ {_ x}  begin
            var x /Var V.wk      ≡⟨ app-var 
            var (lookup V.wk x)  ≡⟨ cong var (V.lookup-wk x) 
            var (suc x)          
        }
      ; application = Subst.application subst
      ; var-/       = app-var
      }
    ; /✶-↑✶ = /✶-↑✶
    }

  private module L₃ = Lemmas₃ lemmas₃

  lemmas₅ : Lemmas₅ T
  lemmas₅ = record
    { lemmas₄ = record
      { lemmas₃ = lemmas₃
      ; /-wk    = λ {_ t}  begin
          t / wk       ≡⟨ /✶-↑✶ (ε  wk) (ε  V.wk)
                             k x  begin
                               var x / wk ↑⋆ k                 ≡⟨ L₃.var-/-wk-↑⋆ k x 
                               var (lift k suc x)              ≡⟨ cong var (sym (V.var-/-wk-↑⋆ k x)) 
                               var (lookup (V._↑⋆_ V.wk k) x)  ≡⟨ sym app-var 
                               var x /Var V._↑⋆_ V.wk k        )
                            zero t 
          t /Var V.wk  ≡⟨⟩
          weaken t     
      }
    }

  open Lemmas₅ lemmas₅ public hiding (lemmas₃)

  wk-⊙-∷ : (t : T n) (ρ : Sub T m n)  (T.wk T.⊙ (t  ρ))  ρ
  wk-⊙-∷ t ρ = extensionality λ x  begin
    lookup (T.wk T.⊙ (t  ρ)) x ≡⟨ L₃.lookup-wk-↑⋆-⊙ 0 {ρ = t  ρ} 
    lookup ρ x                  

  weaken-∷ : (t₁ : T m) {t₂ : T n} {ρ : Sub T m n} 
    T.weaken t₁ T./ (t₂  ρ)  t₁ T./ ρ
  weaken-∷ t₁ {t₂} {ρ} = begin
    T.weaken t₁ T./ (t₂  ρ)   ≡⟨ cong (T._/ (t₂  ρ)) (sym /-wk) 
    (t₁ T./ T.wk) T./ (t₂  ρ) ≡⟨ ⨀→/✶ ((t₂  ρ)  T.wk  ε) (ρ  ε) (wk-⊙-∷ t₂ ρ) t₁ 
    t₁ T./ ρ                   

  weaken-sub : (t₁ : T n) {t₂ : T n}  T.weaken t₁ T./ (T.sub t₂)  t₁
  weaken-sub t₁ {t₂} = begin
    T.weaken t₁ T./ (T.sub t₂) ≡⟨ weaken-∷ t₁ 
    t₁ T./ T.id                ≡⟨ id-vanishes t₁ 
    t₁                         

  -- Lemmas relating renamings to substitutions.

  map-var≡ : {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m  Fin n} 
             (∀ x  lookup ρ₁ x  f x) 
             (∀ x  lookup ρ₂ x  T.var (f x)) 
             map T.var ρ₁  ρ₂
  map-var≡ {ρ₁ = ρ₁} {ρ₂ = ρ₂} {f = f} hyp₁ hyp₂ = extensionality λ x 
    lookup (map T.var ρ₁) x  ≡⟨ Vec.lookup-map x _ ρ₁ 
    T.var (lookup ρ₁ x)      ≡⟨ cong T.var $ hyp₁ x 
    T.var (f x)              ≡⟨ sym $ hyp₂ x 
    lookup ρ₂ x              

  wk≡wk : map T.var VarSubst.wk  T.wk {n = n}
  wk≡wk = map-var≡ VarLemmas.lookup-wk lookup-wk

  id≡id : map T.var VarSubst.id  T.id {n = n}
  id≡id = map-var≡ VarLemmas.lookup-id lookup-id

  sub≡sub : {x : Fin n}  map T.var (VarSubst.sub x)  T.sub (T.var x)
  sub≡sub = cong (_ ∷_) id≡id

  ↑≡↑ : {ρ : Sub Fin m n}  map T.var (ρ VarSubst.↑)  map T.var ρ T.↑
  ↑≡↑ {ρ = ρ} = map-var≡
    (VarLemmas.lookup-↑⋆ (lookup ρ)  _  refl) 1)
    (lookup-↑⋆ (lookup ρ)  _  Vec.lookup-map _ _ ρ) 1)

  /Var≡/ :  {ρ : Sub Fin m n} {t}  t /Var ρ  t T./ map T.var ρ
  /Var≡/ {ρ = ρ} {t = t} =
    /✶-↑✶ (ε  ρ) (ε  map T.var ρ)
       k x 
         T.var x /Var ρ VarSubst.↑⋆ k        ≡⟨ app-var 
         T.var (lookup (ρ VarSubst.↑⋆ k) x)  ≡⟨ cong T.var $ VarLemmas.lookup-↑⋆ _  _  refl) k _ 
         T.var (lift k (VarSubst._/ ρ) x)    ≡⟨ sym $ lookup-↑⋆ _  _  Vec.lookup-map _ _ ρ) k _ 
         lookup (map T.var ρ T.↑⋆ k) x       ≡⟨ sym app-var 
         T.var x T./ map T.var ρ T.↑⋆ k      )
      zero t

  sub-renaming-commutes :  {t x} {ρ : Sub T m n} 
    t /Var VarSubst.sub x T./ ρ  t T./ ρ T.↑ T./ T.sub (lookup ρ x)
  sub-renaming-commutes {t = t} {x = x} {ρ = ρ} =
    t /Var VarSubst.sub x T./ ρ             ≡⟨ cong (T._/ ρ) /Var≡/ 
    t T./ map T.var (VarSubst.sub x) T./ ρ  ≡⟨ cong  ρ′  t T./ ρ′ T./ ρ) sub≡sub 
    t T./ T.sub (T.var x) T./ ρ             ≡⟨ sub-commutes _ 
    t T./ ρ T.↑ T./ T.sub (T.var x T./ ρ)   ≡⟨ cong  t′  t T./ ρ T.↑ T./ T.sub t′) app-var 
    t T./ ρ T.↑ T./ T.sub (lookup ρ x)      

  sub-commutes-with-renaming :  {t t′} {ρ : Sub Fin m n} 
    t T./ T.sub t′ /Var ρ  t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ)
  sub-commutes-with-renaming {t = t} {t′ = t′} {ρ = ρ} =
    t T./ T.sub t′ /Var ρ                                          ≡⟨ /Var≡/ 
    t T./ T.sub t′ T./ map T.var ρ                                 ≡⟨ sub-commutes _ 
    t T./ map T.var ρ T.↑ T./ T.sub (t′ T./ map T.var ρ)           ≡⟨ sym $ cong  ρ′  t T./ ρ′ T./ T.sub (t′ T./ map T.var ρ)) ↑≡↑ 
    t T./ map T.var (ρ VarSubst.↑) T./ T.sub (t′ T./ map T.var ρ)  ≡⟨ sym $ cong₂  t ρ  t T./ T.sub ρ) /Var≡/ /Var≡/ 
    t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ)