A way to model coercions

Cast.agda

module Cast where

open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin renaming (Fin to Var; zero to vz; suc to vs)
open import Data.Vec using (Vec; []; _∷_; lookup)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

data Ty : Set where
  arr : Ty → Ty → Ty

data Co (m : ℕ) : Set where
  rfl : Ty → Co m
  sym : Co m → Co m
  arr : Co m → Co m → Co m

data Tm (n : ℕ) (m : ℕ) : Set where
  var : Var n → Tm n m
  app : Tm n m → Tm n m → Tm n m
  lam : Tm (suc n) m → Tm n m

  coe : Tm n m → Co m → Tm n m

data _⊩_⦂_≡_ {m} (Δ : Vec (Ty × Ty) m) : Co m → Ty → Ty → Set where
  rflₜ : {A : Ty} →
    -----------------
    Δ ⊩ rfl A ⦂ A ≡ A

  symₜ : {A B : Ty} {co : Co m} →
    Δ ⊩ co ⦂ A ≡ B →
    ------------------
    Δ ⊩ sym co ⦂ B ≡ A

  arrₜ : {A B C D : Ty} {co₁ co₂ : Co m} →
    Δ ⊩ co₁ ⦂ C ≡ A →
    Δ ⊩ co₂ ⦂ D ≡ B →
    -----------------------------------
    Δ ⊩ arr co₁ co₂ ⦂ arr C D ≡ arr A B
    
data _⨟_⊢_⦂_ {n} {m} (Γ : Vec Ty n) (Δ : Vec (Ty × Ty) m) : (t : Tm n m) → Ty → Set where
  varₜ : ∀ {x : Var n} →
    --------------------------
    Γ ⨟ Δ ⊢ var x ⦂ lookup Γ x

  appₜ : ∀ {f t : Tm n m} {A B : Ty} →
    Γ ⨟ Δ ⊢ f ⦂ arr A B →
    Γ ⨟ Δ ⊢ t ⦂ A →
    -----------------------------
    Γ ⨟ Δ ⊢ app f t ⦂ B

  lamₜ : ∀ {t : Tm (suc n) m} {A B : Ty} →
    (A ∷ Γ) ⨟ Δ ⊢ t ⦂ B →
    -----------------------------
    Γ ⨟ Δ ⊢ lam t ⦂ arr A B

  coeₜ : ∀ {t : Tm n m} {co : Co m} {A B : Ty} →
    Γ ⨟ Δ ⊢ t ⦂ A →
    Δ ⊩ co ⦂ A ≡ B →
    ---------------------
    Γ ⨟ Δ ⊢ coe t co ⦂ B

postulate
  subst : ∀ {n m} → Tm (suc n) m → Tm n m → Tm n m
  weaken : ∀ {n m} → Tm n m → Tm (suc n) m

data step {n} {m} : Tm n m → Tm n m → Set where
  appᵦ : ∀ {t : Tm (suc n) m} {s : Tm n m} →
    step
      (app (lam t) s)
      (subst t s)

  rflₖ : ∀ {A : Ty} {t : Tm n m} →
    step
      (coe t (rfl A))
      t

  arrₖ : {t : Tm n m} {co₁ co₂ : Co m} →
    step
      (coe t (arr co₁ co₂))
      (lam (coe (app (weaken t) (coe (var vz) (sym co₁))) co₂))

postulate
  weakenₜ : ∀ {n m} {Γ : Vec Ty n} {Δ : Vec (Ty × Ty) m} {t : Tm n m} (A B : Ty) →
    Γ ⨟ Δ ⊢ t ⦂ A →
    --------------------------
    (B ∷ Γ) ⨟ Δ ⊢ weaken t ⦂ A

module Preservation-arrₖ {n m} {t : Tm n m} {co₁ co₂ : Co m} {Γ : Vec Ty n} {Δ : Vec (Ty × Ty) m} {A B : Ty} where
  lemma
    : Γ ⨟ Δ ⊢ coe t (arr co₁ co₂)                                     ⦂ arr A B
    → Γ ⨟ Δ ⊢ lam (coe (app (weaken t) (coe (var vz) (sym co₁))) co₂) ⦂ arr A B
  lemma (coeₜ tₜ (arrₜ {C = C} {D = D} co₁ₜ co₂ₜ)) =
    lamₜ (coeₜ (appₜ (weakenₜ (arr C D) A tₜ) (coeₜ varₜ (symₜ co₁ₜ))) co₂ₜ)