Arities.agda

infixr 9 _->>_

data Arity : Set where
  * : Arity
  _->>_ : Arity → Arity → Arity

infixl 3 _,_
data Ctx : Set where
  <> : Ctx
  _,_ : Ctx → Arity → Ctx

_++_ : Ctx → Ctx → Ctx
Γ ++ <> = Γ
Γ ++ (Γ' , A) = (Γ ++ Γ') , A

data Var : Ctx → Arity → Set where
  here : ∀ {Γ A} → Var (Γ , A) A
  there : ∀ {Γ A B} → Var Γ A → Var (Γ , B) A

infixl 9 _$_

data Syntax (C : Arity → Set) : Ctx → Arity → Set where
  var : ∀ {Γ A} → Var Γ A → Syntax C Γ A
  scope : ∀ {Γ A B} → Syntax C (Γ , A) B → Syntax C Γ (A ->> B)
  _$_ : ∀ {Γ A B} → Syntax C Γ (A ->> B) → Syntax C Γ A → Syntax C Γ B
  con : ∀ {Γ A} → C A → Syntax C Γ A

data Substitution (C : Arity → Set) (Γ : Ctx) : Ctx → Set where
  <> : Substitution C Γ <>
  _,_ : ∀ {Γ' A} → Substitution C Γ Γ' → Syntax C Γ A → Substitution C Γ (Γ' , A)

lookup : ∀ {C Γ Γ' A} → Var Γ' A → Substitution C Γ Γ' → Syntax C Γ A
lookup here (σ , x) = x
lookup (there x) (σ , _) = lookup x σ

weakenVar : ∀ {Γ} Γ' {A B} → Var (Γ ++ Γ') B → Var ((Γ , A) ++ Γ') B
weakenVar <> x = there x
weakenVar (Γ' , _) here = here
weakenVar (Γ' , _) (there x) = there (weakenVar Γ' x)

weaken : ∀ {C Γ} Γ' {A B} → Syntax C (Γ ++ Γ') B → Syntax C ((Γ , A) ++ Γ') B
weaken Γ' (var x) = var (weakenVar Γ' x)
weaken Γ' (scope M) = scope (weaken (Γ' , _) M)
weaken Γ' (M $ N) = weaken Γ' M $ weaken Γ' N
weaken Γ' (con x) = con x

weakenCtx : ∀ {C Γ Γ' A} → Substitution C Γ Γ' → Substitution C (Γ , A) Γ'
weakenCtx <> = <>
weakenCtx (σ , M) = weakenCtx σ , weaken <> M

[_]_ : ∀ {C Γ Γ' A} → Substitution C Γ Γ' → Syntax C Γ' A → Syntax C Γ A
[ σ ] var x = lookup x σ
[ σ ] scope M = scope ([ weakenCtx σ , var here ] M)
[ σ ] (M $ N) = ([ σ ] M) $ ([ σ ] N)
[ σ ] con c = con c

data RawTermC : Arity → Set where
  true false : RawTermC *
  if : RawTermC (* ->> * ->> * ->> *)
  pair : RawTermC (* ->> * ->> *)
  fst snd : RawTermC (* ->> *)
  lam : RawTermC ((* ->> *) ->> *)
  app : RawTermC (* ->> * ->> *)

data Type : Set where
  Bool : Type
  _×_ _⇒_ : Type → Type → Type

data TypeCtx : Set where
  <> : TypeCtx
  _,_ : TypeCtx → Type → TypeCtx

⌊_⌋ctx : TypeCtx → Ctx
⌊ <> ⌋ctx = <>
⌊ Γ , _ ⌋ctx = ⌊ Γ ⌋ctx , *

data CtxVar : TypeCtx → Type → Set where
  here : ∀ {Γ A} → CtxVar (Γ , A) A
  there : ∀ {Γ A B} → CtxVar Γ A → CtxVar (Γ , B) A

⌊_⌋var : ∀ {Γ A} → CtxVar Γ A → Var ⌊ Γ ⌋ctx *
⌊ here ⌋var = here
⌊ there x ⌋var = there ⌊ x ⌋var

data _⊢_∈_ : (Γ : TypeCtx) → Syntax RawTermC ⌊ Γ ⌋ctx * → Type → Set where
  hyp : ∀ {Γ A} → (x : CtxVar Γ A) → Γ ⊢ var ⌊ x ⌋var ∈ A
  ×-Intro : ∀ {Γ A B M N} → Γ ⊢ M ∈ A → Γ ⊢ N ∈ B → Γ ⊢ con pair $ M $ N ∈ (A × B)
  Bool-Intro-1 : ∀ {Γ} → Γ ⊢ con true ∈ Bool
  Bool-Intro-2 : ∀ {Γ} → Γ ⊢ con false ∈ Bool
  Bool-Elim : ∀ {Γ C M N P} → Γ ⊢ M ∈ Bool → Γ ⊢ N ∈ C → Γ ⊢ P ∈ C → Γ ⊢ con if $ M $ N $ P ∈ C
  ×-Elim-1 : ∀ {Γ A B P} → Γ ⊢ P ∈ (A × B) → Γ ⊢ con fst $ P ∈ A
  ×-Elim-2 : ∀ {Γ A B P} → Γ ⊢ P ∈ (A × B) → Γ ⊢ con snd $ P ∈ B
  ⇒-Intro : ∀ {Γ A B M} → (Γ , A) ⊢ M ∈ B → Γ ⊢ con lam $ scope M ∈ (A ⇒ B)
  ⇒-Elim : ∀ {Γ A B M N} → Γ ⊢ M ∈ (A ⇒ B) → Γ ⊢ N ∈ A → Γ ⊢ con app $ M $ N ∈ B

proj1 : ∀ {Γ A B} → Γ ⊢ con lam $ scope (con fst $ var here) ∈ ((A × B) ⇒ A)
proj1 {Γ} {A} {B} = ⇒-Intro      -- Γ ⊢ con lam $ scope (con fst $ var here) ∈ ((A × B) ⇒ A)
                      (×-Elim-1  -- (Γ , (A × B)) ⊢ con fst $ var here ∈ A
                        (hyp here))