Skip to content

Instantly share code, notes, and snippets.

@FrozenWinters

FrozenWinters/untyped-lambda.agda

Created May 11, 2022 17:59
Show Gist options
  • Save FrozenWinters/4f79bde2facd543170f919db6200ac24 to your computer and use it in GitHub Desktop.
Save FrozenWinters/4f79bde2facd543170f919db6200ac24 to your computer and use it in GitHub Desktop.
Download ZIP
Untyped lambda calculus syntax with explicit substitutions
Raw
untyped-lambda.agda
{-# OPTIONS --cubical --guardedness #-}
module untyped-lambda where
open import Agda.Primitive using (Level; lzero; lsuc; _βŠ”_) public
open import Cubical.Core.Everything public
open import Cubical.Foundations.Everything renaming (cong to ap) public
open import Cubical.Data.Nat renaming (zero to Z ; suc to S)
-- Construction of untyped lambda-calculus syntax
infixl 10 _βŠ•_
data 𝐸𝑙𝑠 (el : Type) : β„• β†’ Type where
! : 𝐸𝑙𝑠 el Z
_βŠ•_ : {n : β„•} β†’ 𝐸𝑙𝑠 el n β†’ el β†’ 𝐸𝑙𝑠 el (S n)
map𝐸𝑙𝑠 : {el₁ elβ‚‚ : Type} (f : el₁ β†’ elβ‚‚) {n : β„•} β†’ 𝐸𝑙𝑠 el₁ n β†’ 𝐸𝑙𝑠 elβ‚‚ n
map𝐸𝑙𝑠 f ! = !
map𝐸𝑙𝑠 f (Οƒ βŠ• t) = map𝐸𝑙𝑠 f Οƒ βŠ• f t
π𝐸𝑙𝑠 : {el : Type} {n : β„•} β†’ 𝐸𝑙𝑠 el (S n) β†’ 𝐸𝑙𝑠 el n
π𝐸𝑙𝑠 (Οƒ βŠ• t) = Οƒ
π‘‡π‘šπ‘  : (tm : β„• β†’ Type) β†’ β„• β†’ β„• β†’ Type
π‘‡π‘šπ‘  tm n m = 𝐸𝑙𝑠 (tm n) m
data Fin : (n : β„•) β†’ Type where
𝑍 : {n : β„•} β†’ Fin (S n)
𝑆 : {n : β„•} β†’ Fin n β†’ Fin (S n)
Ren = π‘‡π‘šπ‘  Fin
W₁Ren : {n m : β„•} β†’ Ren n m β†’ Ren (S n) m
W₁Ren Οƒ = map𝐸𝑙𝑠 𝑆 Οƒ
Wβ‚‚Ren : {n m : β„•} β†’ Ren n m β†’ Ren (S n) (S m)
Wβ‚‚Ren Οƒ = W₁Ren Οƒ βŠ• 𝑍
idRen : (n : β„•) β†’ Ren n n
idRen Z = !
idRen (S n) = Wβ‚‚Ren (idRen n)
Ο€Ren : {n : β„•} β†’ Ren (S n) n
Ο€Ren {n} = π𝐸𝑙𝑠 (idRen (S n))
derive : {el : Type} {n : β„•} β†’ 𝐸𝑙𝑠 el n β†’ Fin n β†’ el
derive (Οƒ βŠ• t) 𝑍 = t
derive (Οƒ βŠ• t) (𝑆 n) = derive Οƒ n
deriveRen : {el : Type} {n m : β„•} β†’ 𝐸𝑙𝑠 el n β†’ Ren n m β†’ 𝐸𝑙𝑠 el m
deriveRen Οƒ Ο„ = map𝐸𝑙𝑠 (derive Οƒ) Ο„
data Tm : (n : β„•) β†’ Type
Tms = π‘‡π‘šπ‘  Tm
_∘Tms_ : {n m k : β„•} β†’ Tms m k β†’ Tms n m β†’ Tms n k
idTms : (n : β„•) β†’ Tms n n
W₁Tm : {n : β„•} β†’ Tm n β†’ Tm (S n)
W₁Tms : {n m : β„•} β†’ Tms n m β†’ Tms (S n) m
Wβ‚‚Tms : {n m : β„•} β†’ Tms n m β†’ Tms (S n) (S m)
infixl 20 _[_]
data Tm where
V : {n : β„•} β†’ Fin n β†’ Tm n
Lam : {n : β„•} β†’ Tm (S n) β†’ Tm n
App : {n : β„•} β†’ Tm n β†’ Tm n β†’ Tm n
_[_] : {n m : β„•} β†’ Tm m β†’ Tms n m β†’ Tm n
Ξ² : {n : β„•} (t : Tm (S n)) (s : Tm n) β†’ App (Lam t) s ≑ t [ idTms n βŠ• s ]
Ξ· : {n : β„•} (t : Tm n) β†’ t ≑ Lam (App (W₁Tm t) (V 𝑍))
V[] : {n m : β„•} (v : Fin m) (Οƒ : Tms n m) β†’ V v [ Οƒ ] ≑ derive Οƒ v
Lam[] : {n m : β„•} (t : Tm (S m)) (Οƒ : Tms n m) β†’ Lam t [ Οƒ ] ≑ Lam (t [ Wβ‚‚Tms Οƒ ])
App[] : {n m : β„•} (t s : Tm m) (Οƒ : Tms n m) β†’ App t s [ Οƒ ] ≑ App (t [ Οƒ ]) (s [ Οƒ ])
[][] : {n m k : β„•} (t : Tm k) (Οƒ : Tms m k) (Ο„ : Tms n m) β†’ t [ Οƒ ] [ Ο„ ] ≑ t [ Οƒ ∘Tms Ο„ ]
trunc : {n : β„•} β†’ isSet (Tm n)
Οƒ ∘Tms Ο„ = map𝐸𝑙𝑠 _[ Ο„ ] Οƒ
varify : {n m : β„•} β†’ Ren n m β†’ Tms n m
varify Οƒ = map𝐸𝑙𝑠 V Οƒ
idTms n = varify (idRen n)
W₁Tm t = t [ varify Ο€Ren ]
W₁Tms Οƒ = map𝐸𝑙𝑠 W₁Tm Οƒ
Wβ‚‚Tms Οƒ = W₁Tms Οƒ βŠ• V 𝑍
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment