Skip to content
Permalink
Browse files

QTT agda sketch

  • Loading branch information...
andy-morris committed Aug 12, 2019
1 parent 6a910a7 commit f3e4d365c825745b6abe4deb418735c6fca0054c
@@ -21,3 +21,6 @@ tmp/
# Idris temporary
*.ibc
stack.yaml.lock

# Agda temporary
*.agdai
@@ -0,0 +1,76 @@
module AlgebraExtras where

open import Level
open import Algebra.Structures
open import Algebra.FunctionProperties
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

-- "POSR" = Partially-Ordered SemiRing

module _ {a ℓ₁ ℓ₂} {A : Set a}
(≈ : Rel A ℓ₁) (≤ : Rel A ℓ₂) (+ * : Op₂ A) (0# 1# : A)
where
record IsPOSR : Set (suc (a ⊔ ℓ₁ ⊔ ℓ₂)) where
field
isSemiring : IsSemiring ≈ + * 0# 1#
isPartialOrder : IsPartialOrder ≈ ≤

open IsSemiring isSemiring public
renaming (refl to ≈-refl ; reflexive to ≈-reflexive)
open IsPartialOrder isPartialOrder public
renaming (refl to ≤-refl ; reflexive to ≤-reflexive)

record IsDecPOSR : Set (suc (a ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≟_ _≤?_
field
isPosr : IsPOSR
_≟_ : Decidable ≈
_≤?_ : Decidable ≤


record RawPOSR′ c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _*_
infixl 6 _+_
infix 4 _≤_
field
Carrier : Set c
_≤_ : Rel Carrier ℓ
_+_ _*_ : Op₂ Carrier
0# 1# : Carrier

record RawPOSR c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
field rawPosr′ : RawPOSR′ c ℓ₁
open RawPOSR′ rawPosr′ public
infix 4 _≈_
field _≈_ : Rel Carrier ℓ₂


record POSR′ c ℓ : Set (suc (c ⊔ ℓ)) where
field rawPosr′ : RawPOSR′ c ℓ
open RawPOSR′ rawPosr′ public
field isPosr : IsPOSR _≡_ _≤_ _+_ _*_ 0# 1#
open IsPOSR isPosr public

record POSR c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
field rawPosr : RawPOSR c ℓ₁ ℓ₂
open RawPOSR rawPosr public
field isPosr : IsPOSR _≈_ _≤_ _+_ _*_ 0# 1#
open IsPOSR isPosr public


record DecPOSR′ c ℓ : Set (suc (c ⊔ ℓ)) where
field rawPosr′ : RawPOSR′ c ℓ
open RawPOSR′ rawPosr′ public
field isDecPosr : IsDecPOSR _≡_ _≤_ _+_ _*_ 0# 1#
open IsDecPOSR isDecPosr public
posr′ : POSR′ c ℓ
posr′ = record { isPosr = isPosr }

record DecPOSR c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
field rawPosr : RawPOSR c ℓ₁ ℓ₂
open RawPOSR rawPosr public
field isDecPosr : IsDecPOSR _≈_ _≤_ _+_ _*_ 0# 1#
open IsDecPOSR isDecPosr public
posr : POSR c ℓ₁ ℓ₂
posr = record { isPosr = isPosr }
@@ -0,0 +1,189 @@
open import AlgebraExtras

-- todo: use a posr with arbitrary equivalence instead of _≡_?
-- not really the point tho
module DL {c ℓ} (posr′ : POSR′ c ℓ) where

open import Algebra.Structures
open import Level using (0ℓ ; _⊔_)
open import Function
open import Data.Nat ashiding (_⊔_)
open import Data.Fin as Fin
open import Data.Product hiding (Σ)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

private variable m n : ℕ

module Quantity = POSR′ posr′
open Quantity using (0# ; 1#)
renaming (Carrier to Quantity ; _+_ to _⊕_ ; _*_ to _⊗_ ; _≤_ to _⊑_)
private variable π π′ ρ ρ′ : Quantity

Var = Fin
private variable x y : Var n

Universe =
private variable u v : Universe

data Tm n : Set c
data Elim n : Set c
Typ = Tm

data Tm n where
sort : (u : Universe) Typ n
Π : (π : Quantity) (S : Typ n) (T : Typ (suc n)) Typ n
Λ : (t : Tm (suc n)) Tm n
[_] : (e : Elim n) Tm n
private variable s s′ t t′ : Tm n ; S S′ T T′ R R′ : Typ n

data Elim n where
`_ : (x : Var n) Elim n
_∙_ : (f : Elim n) (s : Tm n) Elim n
_⦂_ : (s : Tm n) (S : Typ n) Elim n
infix 1000 `_ ; infixl 200 _∙_ ; infix 100 _⦂_
private variable e e′ f f′ : Elim n


data _≼_ : Rel (Typ n) 0ℓ where
sort : u ℕ.≤ v sort u ≼ sort {n} v
Π : S′ ≼ S T ≼ T′ Π π S T ≼ Π π S′ T′
refl : S ≼ S
-- (maybe recurse into other structures?)
infix 4 _≼_

weakₜ′ : Var (suc n) Tm n Tm (suc n)
weakₑ′ : Var (suc n) Elim n Elim (suc n)
weakₜ′ i (sort u) = sort u
weakₜ′ i (Π π S T) = Π π (weakₜ′ i S) (weakₜ′ (suc i) T)
weakₜ′ i (Λ t) = Λ (weakₜ′ (suc i) t)
weakₜ′ i [ e ] = [ weakₑ′ i e ]
weakₑ′ i (` x) = ` punchIn i x
weakₑ′ i (f ∙ s) = weakₑ′ i f ∙ weakₜ′ i s
weakₑ′ i (s ⦂ S) = weakₜ′ i s ⦂ weakₜ′ i S

weakₜ : Tm n Tm (suc n)
weakₜ = weakₜ′ zero
weakₑ : Elim n Elim (suc n)
weakₑ = weakₑ′ zero

substₜ′ : Var (suc n) Tm (suc n) Elim n Tm n
substₑ′ : Var (suc n) Elim (suc n) Elim n Elim n
substₜ′ i (sort u) e = sort u
substₜ′ i (Π π S T) e = Π π (substₜ′ i S e) (substₜ′ (suc i) T (weakₑ′ i e))
substₜ′ i (Λ t) e = Λ (substₜ′ (suc i) t (weakₑ′ i e))
substₜ′ i [ f ] e = [ substₑ′ i f e ]
substₑ′ i (` x) e =
case i Fin.≟ x of λ{(yes _) e ; (no i≢x) ` Fin.punchOut i≢x}
substₑ′ i (f ∙ s) e = substₑ′ i f e ∙ substₜ′ i s e
substₑ′ i (s ⦂ S) e = substₜ′ i s e ⦂ substₜ′ i S e

substₜ : Tm (suc n) Elim n Tm n
substₜ = substₜ′ zero
substₑ : Elim (suc n) Elim n Elim n
substₑ = substₑ′ zero

data _⟿ₜ_ : Rel (Tm n) 0ℓ
data _⟿ₑ_ : Rel (Elim n) 0ℓ
infix 1 _⟿ₜ_ _⟿ₑ_

data _⟿ₜ_ where
υ : [ t ⦂ T ] ⟿ₜ t
Πˡ : S ⟿ₜ S′ Π π S T ⟿ₜ Π π S′ T
-- reducing under binders?
Πʳ : T ⟿ₜ T′ Π π S T ⟿ₜ Π π S T′
Λ : t ⟿ₜ t′ Λ t ⟿ₜ Λ t′
[_] : e ⟿ₑ e′ [ e ] ⟿ₜ [ e′ ]

data _⟿ₑ_ where
β : (Λ t ⦂ Π π S T) ∙ s ⟿ₑ substₑ (t ⦂ T) (s ⦂ S)
∙ˡ : f ⟿ₑ f′ f ∙ s ⟿ₑ f′ ∙ s
∙ʳ : s ⟿ₜ s′ f ∙ s ⟿ₑ f ∙ s′
⦂ˡ : s ⟿ₜ s′ s ⦂ S ⟿ₑ s′ ⦂ S
⦂ʳ : S ⟿ₜ S′ s ⦂ S ⟿ₑ s ⦂ S′


data Ctx′ {a} (F : ℕ → Set a) : ℕ → Set a where
ε : Ctx′ F 0
_⨟_ : Ctx′ F n F n Ctx′ F (suc n)
infixl 5 _⨟_

module _ where
private variable F G H : ℕ Set _

czipWith : (∀ {n} F n G n H n) Ctx′ F n Ctx′ G n Ctx′ H n
czipWith f ε ε = ε
czipWith f (xs ⨟ x) (ys ⨟ y) = czipWith f xs ys ⨟ f x y

clookup′ : (∀ {n} F n F (suc n)) Ctx′ F n Var n F n
clookup′ f (xs ⨟ x) zero = f x
clookup′ f (xs ⨟ x) (suc i) = f $ clookup′ f xs i

Ctx = Ctx′ Typ
private variable Γ Γ₁ Γ₂ : Ctx n

clookup : Ctx n Var n Typ n
clookup = clookup′ weakₜ

Skel = Ctx′ λ _ Quantity
private variable Σ Σ₁ Σ₂ : Skel n

slookup : Skel n Var n Quantity
slookup = clookup′ id

data Zero : Skel n → Set where
ε : Zero ε
_⨟0# : Zero Σ Zero (Σ ⨟ 0#)
infixl 5 _⨟0#

data Only : Quantity → Fin n → Skel n → Set where
_⨟_ : Zero Σ ρ Only ρ zero (Σ ⨟ ρ)
_⨟0# : Only ρ x Σ Only ρ (suc x) (Σ ⨟ 0#)

_⊞_ : Skel n Skel n Skel n
_⊞_ = czipWith _⊕_
infixl 10 _⊞_

data _⊑*_ : Rel (Skel n) ℓ where
ε : ε ⊑* ε
_⨟_ : Σ₁ ⊑* Σ₂ π ⊑ ρ Σ₁ ⨟ π ⊑* Σ₂ ⨟ ρ
infix 4 _⊑*_


data _⊢_-_∋_▷_ : Ctx n → Quantity → Typ n → Tm n → Skel n → Set (c ⊔ ℓ)
data _⊢_-_∈_▷_ : Ctx n → Quantity → Elim n → Typ n → Skel n → Set (c ⊔ ℓ)
infix 0 _⊢_-_∋_▷_ _⊢_-_∈_▷_

data _⊢_-_∋_▷_ where
pre : T ⟿ₜ R
Γ ⊢ ρ - R ∋ t ▷ Σ
Γ ⊢ ρ - T ∋ t ▷ Σ
sort : u ℕ.< v Zero Σ
Γ ⊢ 0# - sort v ∋ sort u ▷ Σ
fun : Zero Σ
Γ ⊢ 0# - sort u ∋ S ▷ Σ
Γ ⨟ S ⊢ 0# - sort u ∋ T ▷ Σ ⨟ 0#
Γ ⊢ 0# - sort u ∋ Π π S T ▷ Σ
lam : ρ′ ⊑ ρ ⊗ π -- for no subusaging: ρ′ ≡ ρ ⊗ π
Γ ⨟ S ⊢ ρ - T ∋ t ▷ Σ ⨟ ρ′
Γ ⊢ ρ - Π π S T ∋ Λ t ▷ Σ
elim : S ≼ T
Γ ⊢ ρ - e ∈ S ▷ Σ
Γ ⊢ ρ - T ∋ [ e ] ▷ Σ

data _⊢_-_∈_▷_ where
post : Γ ⊢ ρ - e ∈ S ▷ Σ S ⟿ₜ R
Γ ⊢ ρ - e ∈ R ▷ Σ
var : clookup Γ x ≡ S Only ρ x Σ
Γ ⊢ ρ - ` x ∈ T ▷ Σ
-- var just use whatever ρ it's told. lam will check that it's ok later.
app : π S -- (these seem to be hard for Agda to infer)
ρ′ ≡ ρ ⊗ π Σ ≡ Σ₁ ⊞ Σ₂ T′ ≡ substₜ T (s ⦂ S)
Γ ⊢ ρ - f ∈ Π π S T ▷ Σ₁
Γ ⊢ ρ′ - S ∋ s ▷ Σ₂
Γ ⊢ ρ - f ∙ s ∈ T′ ▷ Σ
cut : Zero Σ₁
Γ ⊢ 0# - sort u ∋ S ▷ Σ₁
Γ ⊢ ρ - S ∋ s ▷ Σ₂
Γ ⊢ ρ - s ⦂ S ∈ S ▷ Σ₂
@@ -0,0 +1,34 @@
module Example where

open import AlgebraExtras
open import Function
open import Data.Nat
open import Data.Fin
open import Relation.Binary.PropositionalEquality

open import Three
open import DL (DecPOSR′.posr′ decPosr)

variable
n :
e : Elim n

`f = Elim 2 ∋ ` zero
`x = Elim 2 ∋ ` suc zero

postulate
A : {n} Tm n
A-ground : A {n} ≡ substₜ A e

-- the problem judgment from the bottom of p14 of the QTT paper (almost)
-- the example wouldn't mean much as-is because f is free so its usage wouldn't
-- be checked, so it's put in a λ here
-- ⊢ 1 (1 f: (1 x: A) → A) (ω x: A) → A ∋ λf x. f x
_ : ε ⊢ 1# - Π 1# (Π 1# A A) (Π ω# A A) ∋ Λ (Λ [ `f ∙ [ `x ] ]) ▷ ε
_ =
lam refl
(lam (1# ⊑ω#) -- ← hey look, subusaging‼
(elim refl
(app 1# A refl refl A-ground
(var refl (ε ⨟0# ⨟ 1#))
(elim refl (var refl (ε ⨟ 1# ⨟0#))))))

0 comments on commit f3e4d36

Please sign in to comment.
You can’t perform that action at this time.