dbphoas.agda

  module STLC where
    
    infixr 9 _⇒_
    data Ty : Set where
      _⇒_ : Ty → Ty → Ty
    
    data Context : Set where
      <> : Context
      _,_ : Context → Ty → Context
    
    data Var (s : Ty → Set) : Context → Ty → Set where
      here : ∀ {Γ A} → s A → Var s (Γ , A) A
      there : ∀ {Γ A B} → Var s Γ A → Var s (Γ , B) A
    
    infixl 9 _$_
    data Tm' (s : Ty → Set) (Γ : Context) : Ty → Set where
      var : ∀ {A} → Var s Γ A → Tm' s Γ A
      lam : ∀ {A B} → (s A → Tm' s (Γ , A) B) → Tm' s Γ (A ⇒ B)
      _$_ : ∀ {A B} → Tm' s Γ (A ⇒ B) → Tm' s Γ A → Tm' s Γ B
    
    id : ∀ {s A} → Tm' s <> (A ⇒ A)
    id = lam λ x → var (here x)
    
    flip : ∀ {s A B C} → Tm' s <> ((A ⇒ B ⇒ C) ⇒ (B ⇒ A ⇒ C))
    flip = lam λ f → lam λ y → lam λ x → var (there (there (here f))) $ var (here x) $ var (there (here y))
    
    no-naughty-business : ∀ {s A} → Tm' s <> (A ⇒ A)
    no-naughty-business = lam λ x → {!can't match on x because x : s <> A!}
    
  module MLL where
    
    infixr 9 _⊗_
    infixr 8 _-o_
    data Ty : Set where
      _⊗_ _-o_ : Ty → Ty → Ty
    
    infixl 7 _,_
    data Context : Set where
      <> : Context
      _,_ : Context → Ty → Context
    
    infixl 6 _++_
    _++_ : Context → Context → Context
    Γ ++ <> = Γ
    Γ ++ (Γ' , A) = (Γ ++ Γ') , A
    
    data Var (s : Ty → Set) : Context → Ty → Set where
      here : ∀ {A} → s A → Var s (<> , A) A
    
    data Structure : Context → Context → Set where
      ex : ∀ Γ A B Γ' → Structure (Γ , A , B ++ Γ') (Γ , B , A ++ Γ')
    
    infixl 9 _$_
    data Tm' (s : Ty → Set) : Context → Ty → Set where
      var : ∀ {Γ A} → Var s Γ A → Tm' s Γ A
      str : ∀ {C} Γ Γ' → Structure Γ Γ' → Tm' s Γ C → Tm' s Γ' C
      pair : ∀ {Γ Γ' A B} → Tm' s Γ A → Tm' s Γ' B → Tm' s (Γ ++ Γ') (A ⊗ B)
      split : ∀ {Γ Δ Δ' A B C} → Tm' s Γ (A ⊗ B) → Tm' s (Δ , A , B ++ Δ') C → Tm' s (Δ ++ Γ ++ Δ') C
      lam : ∀ {Γ A B} → (s A → Tm' s (Γ , A) B) → Tm' s Γ (A -o B)
      _$_ : ∀ {Γ Γ' A B} → Tm' s Γ (A -o B) → Tm' s Γ' A → Tm' s (Γ ++ Γ') B
    
    flip : ∀ {s A B C} → Tm' s <> ((A -o B -o C) -o (B -o A -o C))
    flip {s} {A} {B} {C}
      = lam λ f → lam λ y → lam λ x →
          str (<> , A -o B -o C , A , B) (<> , A -o B -o C , B , A)
              (ex (<> , A -o B -o C) A B <>)
              (var (here f) $ var (here x) $ var (here y))
    
    no-delta-1 : ∀ {s A} → Tm' s <> (A -o A ⊗ A)
    no-delta-1 {A = A} = lam λ x → pair {Γ = <> , A} {Γ' = <>} (var (here x)) {! no proof of A is left !}
    
    no-delta-2 : ∀ {s A} → Tm' s <> (A -o A ⊗ A)
    no-delta-2 {A = A} = lam λ x → pair {Γ = <>} {Γ' = <> , A} {! no proof of A is left !} (var (here x))
    
    no-const : ∀ {s A B} → Tm' s <> (A -o B -o A)
    no-const = lam λ x → lam λ y → {!x is in context A, B, but needs to be just in context A!}

here is a problem:

  module Modal where

    infixr 9 _⇒_
    data Ty : Set where
      _⇒_ : Ty → Ty → Ty
      □ : Ty → Ty

    data Context : Set where
      <> : Context
      _,_ : Context → Ty → Context

    data Var (s : Ty → Set) : Context → Ty → Set where
      here : ∀ {Γ A} → s A → Var s (Γ , A) A
      there : ∀ {Γ A B} → Var s Γ A → Var s (Γ , B) A

    infixl 9 _$_
    data Tm' (s : Ty → Set) (Δ Γ : Context) : Ty → Set where
      var : ∀ {A} → Var s Γ A → Tm' s Δ Γ A
      lam : ∀ {A B} → (s A → Tm' s Δ (Γ , A) B) → Tm' s Δ Γ (A ⇒ B)
      _$_ : ∀ {A B} → Tm' s Δ Γ (A ⇒ B) → Tm' s Δ Γ A → Tm' s Δ Γ B
      var* : ∀ {A} → Var s Δ A → Tm' s Δ Γ A
      box : ∀ {A} → Tm' s Δ <> A → Tm' s Δ Γ (□ A)
      unbox : ∀ {A C} → Tm' s Δ Γ (□ A) → (s A → Tm' s (Δ , A) Γ C) → Tm' s Δ Γ C

    problem : ∀ {s A} → Tm' s <> <> (A ⇒ □ (A ⇒ A))
    problem = lam λ x → box (lam (λ y → var (here x)))