{-# OPTIONS --overlapping-instances #-}
{-# OPTIONS --instance-search-depth=3 #-}
open import Data.List using (List; []; _∷_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Any using (here; there)
open import Relation.Binary.PropositionalEquality using (refl)
pattern here! = here refl
open import Data.List.Relation.Binary.Sublist.Propositional
using (_⊆_)
renaming (skip to weak; keep to lift; base to [])
renaming (lookup to renVar)
open import Data.List.Relation.Binary.Sublist.Propositional.Properties
using (⊆-refl; ⊆-trans)
infixr 15 _⇒_
data Ty : Set where
_⇒_ : (A B : Ty) → Ty
Cxt = List Ty
Var = _∈_
variable
A B C : Ty
Γ Δ Φ : Cxt
x y : Var A Γ
module DB where
data Tm : (A : Ty) (Γ : Cxt) → Set where
var : (x : Var A Γ) → Tm A Γ
app : (t : Tm (A ⇒ B) Γ) (u : Tm A Γ) → Tm B Γ
abs : (t : Tm B (A ∷ Γ)) → Tm (A ⇒ B) Γ
open DB using (Tm)
CSet = Cxt → Set
_•_ : (P : CSet) (A : Ty) → CSet
(P • A) Γ = P (A ∷ Γ)
_→̇_ : (P Q : CSet) → CSet
(P →̇ Q) Γ = P Γ → Q Γ
□ : CSet → CSet
□ P Δ = ∀{Γ} {{τ : Δ ⊆ Γ}} → P Γ
_→̂_ : (P Q : CSet) → CSet
P →̂ Q = □ (P →̇ Q)
[_] : CSet → Set
[ P ] = ∀{Γ} → P Γ
infixl 15 _•_
infixr 10 _→̇_ _→̂_
data _⊆⁺_ : (Γ Δ : Cxt) → Set where
instance
ε : Γ ⊆⁺ Γ
_◅_ : ⦃ τ : Δ ⊆ Γ ⦄ ⦃ τs : Φ ⊆⁺ Δ ⦄ → Φ ⊆⁺ Γ
rensVar : (τs : Δ ⊆⁺ Γ) → Var A Δ → Var A Γ
rensVar ε x = x
rensVar (_◅_ ⦃ τ ⦄ ⦃ τs ⦄) x = renVar τ (rensVar τs x)
infixl 4 _∙_
_∙_ : [ Tm (A ⇒ B) →̇ Tm A →̇ Tm B ]
t ∙ u = DB.app t u
abs : [ (Var A →̂ Tm B) →̇ Tm (A ⇒ B) ]
abs {A = A} {Γ = Γ} f = DB.abs (f {A ∷ Γ} ⦃ τ = weak ⊆-refl ⦄ here!)
var : ⦃ τs : Δ ⊆⁺ Γ ⦄ → Var A Δ → Tm A Γ
var ⦃ τs ⦄ x = DB.var (rensVar τs x)
K : [ Tm (A ⇒ (B ⇒ A)) ]
K = abs λ x → abs λ y → var x
K* : [ Tm (A ⇒ (B ⇒ B)) ]
K* = abs λ x → abs λ y → var y
S : [ Tm ((A ⇒ (B ⇒ C)) ⇒ (A ⇒ B) ⇒ A ⇒ C) ]
S = abs λ x → abs λ y → abs λ z →
var x ∙ var z ∙ (var y ∙ var z)
Bind : [ Tm ( ((A ⇒ C) ⇒ C)
⇒ (A ⇒ ((B ⇒ C) ⇒ C))
⇒ (B ⇒ C) ⇒ C) ]
Bind = abs λ ma →
abs λ mb →
abs λ k →
var ma ∙ abs λ a →
var mb ∙ var a ∙ var k