T.agda

-- Q: How to fix the last two commented lines?
--
-- Summary: Two intrinsically typed calculi A and B, and a translation from A to B.
-- The translation consists of a translation on types, followed by a translation on terms
-- indexed by the translation on types.
-- Agda won't let me case-split in the translation of (term) variables.
--
-- Signs of trouble:
-- - green slime in _A.∋_ and _B.∋_
-- - with clauses (rather than only pattern-matching on arguments)
--
-- Calculus A: System F. Quantifier indexed by kind. [∀] κ A
-- Calculus B: Two sorts of quantifiers, [∀₁] A, [∀₂] A
--
-- Minimized example: Kind contexts Ctxᵏ, type variables _∋ᵏ_, types _⊢ᵀ_, contexts Ctx, variables _∋_. (terms omitted)
--
-- Translate A into B by mapping quantifiers of special kind K, [∀] K, to [∀₂],
-- and other kinds, [∀] κ where κ ≢ K, to [∀₁].

module T where

open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Data.Empty using (⊥-elim)

module A where
  data Kind : Set where
    K TYP : Kind  -- imagine there's many more

  _≡?_ : (κ κ' : Kind) → Dec (κ ≡ κ')
  K ≡? K = yes refl
  TYP ≡? TYP = yes refl
  K ≡? TYP = no λ()
  TYP ≡? K = no λ()

  infixl 4 _▷_
  infix 2 _∋ᵏ_ _⊢ᵀ_

  data Ctxᵏ : Set where
    ∅ : Ctxᵏ
    _▷_ : Ctxᵏ → Kind → Ctxᵏ

  private variable
    κ κ' : Kind
    Γ Γ' : Ctxᵏ

  data _∋ᵏ_ : Ctxᵏ → Kind → Set where
    Z : Γ ▷ κ ∋ᵏ κ
    S_ : Γ ∋ᵏ κ' → Γ ▷ κ ∋ᵏ κ'

  data _⊢ᵀ_ (Γ : Ctxᵏ) : Kind → Set where
    `_ : Γ ∋ᵏ κ → Γ ⊢ᵀ κ
    [∀] : (κ : Kind) → Γ ▷ κ ⊢ᵀ TYP → Γ ⊢ᵀ TYP

  data Ctx : Ctxᵏ → Set where
    ∅ : Ctx ∅
    _▷ᵀ_ : Ctx Γ → (κ : Kind) → Ctx (Γ ▷ κ)
    _▷_ : Ctx Γ → Γ ⊢ᵀ TYP → Ctx Γ

  infix 2 _→ᵀʳ_ _→ᵀˢ_

  _→ᵀʳ_ : Ctxᵏ → Ctxᵏ → Set
  Γ →ᵀʳ Γ' = ∀ {κ} → Γ ∋ᵏ κ → Γ' ∋ᵏ κ

  _→ᵀˢ_ : Ctxᵏ → Ctxᵏ → Set
  Γ →ᵀˢ Γ' = ∀ {κ} → Γ ∋ᵏ κ → Γ' ⊢ᵀ κ

  ren▷ : (Γ →ᵀʳ Γ') → (Γ ▷ κ →ᵀʳ Γ' ▷ κ)
  ren▷ ρ Z = Z
  ren▷ ρ (S α) = S (ρ α)

  renᵀ : (Γ →ᵀʳ Γ') → Γ ⊢ᵀ κ → Γ' ⊢ᵀ κ
  renᵀ ρ (` α) = ` ρ α
  renᵀ ρ ([∀] κ A) = [∀] κ (renᵀ (ren▷ ρ) A)

  sub▷ : (Γ →ᵀˢ Γ') → (Γ ▷ κ →ᵀˢ Γ' ▷ κ)
  sub▷ σ Z = ` Z
  sub▷ σ (S α) = renᵀ S_ (σ α)

  subᵀ : (Γ →ᵀˢ Γ') → Γ ⊢ᵀ κ → Γ' ⊢ᵀ κ
  subᵀ σ (` α) = σ α
  subᵀ σ ([∀] κ A) = [∀] κ (subᵀ (sub▷ σ) A)

  private variable
    A B : Γ ⊢ᵀ κ
    Δ : Ctx Γ

  infix 2 _∋_

  data _∋_ : Ctx Γ → Γ ⊢ᵀ TYP → Set where
    Z : Δ ▷ A ∋ A
    S_ : Δ ∋ A → Δ ▷ B ∋ A
    Sᵀ_ : Δ ∋ A → Δ ▷ᵀ κ ∋ renᵀ S_ A

module B where
  infixl 4 _▷-
  infix 2 _⨟_∋ᵏ- _⨟_⊢ᵀ-

  data Ctxᵏ : Set where
    ∅ : Ctxᵏ
    _▷- : Ctxᵏ → Ctxᵏ

  private variable
    Γ Γ' Ξ Ξ' : Ctxᵏ

  data _⨟_∋ᵏ- : Ctxᵏ → Ctxᵏ → Set where
    Z : Γ ▷- ⨟ Ξ ∋ᵏ-
    S₁_ : Γ ⨟ Ξ ∋ᵏ- → Γ ▷- ⨟ Ξ ∋ᵏ-
    S₂_ : Γ ⨟ Ξ ∋ᵏ- → Γ ⨟ Ξ ▷- ∋ᵏ-

  data _⨟_⊢ᵀ- (Γ Ξ : Ctxᵏ) : Set where
    `_ : Γ ⨟ Ξ ∋ᵏ- → Γ ⨟ Ξ ⊢ᵀ-
    [∀₁] : Γ ▷- ⨟ Ξ ⊢ᵀ- → Γ ⨟ Ξ ⊢ᵀ-
    [∀₂] : Γ ⨟ Ξ ▷- ⊢ᵀ- → Γ ⨟ Ξ ⊢ᵀ-


  data Ctx : Ctxᵏ → Ctxᵏ → Set where
    ∅ : Ctx ∅ ∅
    _▷₁- : Ctx Γ Ξ → Ctx (Γ ▷-) Ξ
    _▷₂- : Ctx Γ Ξ → Ctx Γ (Ξ ▷-)
    _▷_ : Ctx Γ Ξ → Γ ⨟ Ξ ⊢ᵀ- → Ctx Γ Ξ

  infix 2 _⨟_→ᵀʳ_⨟_ _⨟_→ᵀˢ_⨟_

  _⨟_→ᵀʳ_⨟_ : Ctxᵏ → Ctxᵏ → Ctxᵏ → Ctxᵏ → Set
  Γ ⨟ Ξ →ᵀʳ Γ' ⨟ Ξ' = Γ ⨟ Ξ ∋ᵏ- → Γ' ⨟ Ξ' ∋ᵏ-

  _⨟_→ᵀˢ_⨟_ : Ctxᵏ → Ctxᵏ → Ctxᵏ → Ctxᵏ → Set
  Γ ⨟ Ξ →ᵀˢ Γ' ⨟ Ξ' = Γ ⨟ Ξ ∋ᵏ- → Γ' ⨟ Ξ' ⊢ᵀ-

  ren▷₁ : (∀ {Ξ} → Γ ⨟ Ξ →ᵀʳ Γ' ⨟ Ξ) → (Γ ▷- ⨟ Ξ →ᵀʳ Γ' ▷- ⨟ Ξ)
  ren▷₁ ρ Z = Z
  ren▷₁ ρ (S₁ α) = S₁ (ρ α)
  ren▷₁ ρ (S₂ α) = S₂ (ren▷₁ ρ α)

  ren▷₂ : (∀ {Γ} → Γ ⨟ Ξ →ᵀʳ Γ ⨟ Ξ') → (Γ ⨟ Ξ ▷- →ᵀʳ Γ ⨟ Ξ' ▷-)
  ren▷₂ ρ Z = Z
  ren▷₂ ρ (S₁ α) = S₁ (ren▷₂ ρ α)
  ren▷₂ ρ (S₂ α) = S₂ (ρ α)

  renᵀ : (∀ {Ξ} → Γ ⨟ Ξ →ᵀʳ Γ' ⨟ Ξ) → Γ ⨟ Ξ ⊢ᵀ- → Γ' ⨟ Ξ ⊢ᵀ-
  renᵀ ρ (` α) = ` ρ α
  renᵀ ρ ([∀₁] A) = [∀₁] (renᵀ (ren▷₁ ρ) A)
  renᵀ ρ ([∀₂] A) = [∀₂] (renᵀ ρ A)

  renᵀ₂ : (∀ {Γ} → Γ ⨟ Ξ →ᵀʳ Γ ⨟ Ξ') → Γ ⨟ Ξ ⊢ᵀ- → Γ ⨟ Ξ' ⊢ᵀ-
  renᵀ₂ ρ (` α) = ` ρ α
  renᵀ₂ ρ ([∀₁] A) = [∀₁] (renᵀ₂ ρ A)
  renᵀ₂ ρ ([∀₂] A) = [∀₂] (renᵀ₂ (ren▷₂ ρ) A)

{-
  sub▷ : (Γ ⨟ Ξ →ᵀˢ Γ' ⨟ Ξ') → (Γ ▷- ⨟ Ξ →ᵀˢ Γ' ▷- ⨟ Ξ')
  sub▷ σ Z = ` Z
  sub▷ σ (S₁ α) = renᵀ S₁_ (σ α)

  subᵀ : (Γ ⨟ Ξ →ᵀˢ Γ' ⨟ Ξ') → Γ ⨟ Ξ ⊢ᵀ- → Γ' ⨟ Ξ ⊢ᵀ-
  subᵀ σ (` α) = σ α
  subᵀ σ ([∀₁] A) = [∀₁] (subᵀ (sub▷ σ) A)
-}

  private variable
    A B : Γ ⨟ Ξ ⊢ᵀ-
    Δ : Ctx Γ Ξ

  infix 2 _∋_

  data _∋_ : Ctx Γ Ξ → Γ ⨟ Ξ ⊢ᵀ- → Set where
    Z : Δ ▷ A ∋ A
    S_ : Δ ∋ A → Δ ▷ B ∋ A
    S₁_ : Δ ∋ A → Δ ▷₁- ∋ renᵀ S₁_ A
    S₂_ : Δ ∋ A → Δ ▷₂- ∋ renᵀ₂ S₂_ A

module T where
  open A
  open B

  ⟦_⟧ᴷ : A.Ctxᵏ → B.Ctxᵏ
  ⟦ ∅ ⟧ᴷ = ∅
  ⟦ Γ ▷ κ ⟧ᴷ with κ ≡? K  -- Assume there are many other Kind constructors so it's not practical to pattern-match on κ here
  ... | yes _ = ⟦ Γ ⟧ᴷ
  ... | no _  = ⟦ Γ ⟧ᴷ ▷-

  ⟦_⟧ᴸ : A.Ctxᵏ → B.Ctxᵏ
  ⟦ ∅ ⟧ᴸ = ∅
  ⟦ Γ ▷ κ ⟧ᴸ with κ ≡? K
  ... | yes _ = ⟦ Γ ⟧ᴸ ▷-
  ... | no _  = ⟦ Γ ⟧ᴸ

  ⟦_⟧∋ᴷ : {Γ : A.Ctxᵏ} {κ : A.Kind} → Γ ∋ᵏ κ → κ ≢ K → ⟦ Γ ⟧ᴷ B.⨟ ⟦ Γ ⟧ᴸ ∋ᵏ-
  ⟦ Z {κ = κ} ⟧∋ᴷ κ≢K with κ ≡? K
  ... | yes e = ⊥-elim (κ≢K e)
  ... | no _ = Z
  ⟦ S_ {κ = κ} x ⟧∋ᴷ κ≢K with κ ≡? K
  ... | yes _ = S₂ (⟦ x ⟧∋ᴷ κ≢K)
  ... | no _ = S₁ (⟦ x ⟧∋ᴷ κ≢K)

  ⟦_⟧ᵀ : {Γ : A.Ctxᵏ} {κ : A.Kind} → Γ ⊢ᵀ κ → κ ≢ K → ⟦ Γ ⟧ᴷ B.⨟ ⟦ Γ ⟧ᴸ ⊢ᵀ-
  ⟦ ` x ⟧ᵀ κ≢K = ` ⟦ x ⟧∋ᴷ κ≢K
  ⟦ [∀] κ A ⟧ᵀ κ≢K with κ ≡? K | ⟦ A ⟧ᵀ (λ())
  ... | yes _ | ⟦A⟧ = [∀₂] ⟦A⟧
  ... | no _  | ⟦A⟧ = [∀₁] ⟦A⟧

  ⟦_⟧ˣ : ∀ {Γ} → A.Ctx Γ → B.Ctx ⟦ Γ ⟧ᴷ ⟦ Γ ⟧ᴸ
  ⟦ ∅ ⟧ˣ = ∅
  ⟦ Δ ▷ᵀ κ ⟧ˣ with κ ≡? K
  ... | yes _ = ⟦ Δ ⟧ˣ ▷₂-
  ... | no _ = ⟦ Δ ⟧ˣ ▷₁-
  ⟦ Δ ▷ A ⟧ˣ = ⟦ Δ ⟧ˣ ▷ (⟦ A ⟧ᵀ (λ()))

  ⟦_⟧∋ : ∀ {Γ} {Δ : A.Ctx Γ} {A : Γ A.⊢ᵀ TYP} → Δ A.∋ A → ⟦ Δ ⟧ˣ B.∋ ⟦ A ⟧ᵀ (λ())
  ⟦ Z ⟧∋ = Z
  ⟦ S x ⟧∋ = S ⟦ x ⟧∋
  -- ⟦ Sᵀ_ {κ = κ} x ⟧∋ with κ ≡? K
  -- ... | _ = ?

{-
T.agda:214,3-14
κ ≡? K != w of type Dec (κ ≡ K)
when checking that the type
{κ : Kind} (w : Dec (κ ≡ K)) {B.Γ.1 : A.Ctxᵏ} {Δ : A.Ctx B.Γ.1}
{A : B.Γ.1 ⊢ᵀ TYP} {A = A₁ : B.Γ.1 ▷ κ ⊢ᵀ TYP} (x : Δ A.∋ A)
(e : A.renᵀ S_ A ≡ A₁) →
(⟦ Δ ▷ᵀ κ ⟧ˣ | w) B.∋ ⟦ A₁ ⟧ᵀ (λ ())
of the generated with function is well-formed
(https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#ill-typed-with-abstractions)
-}