Skip to content
Snippets Groups Projects
Commit fa063583 authored by Max New's avatar Max New
Browse files

work on new syntx

parent 2b99239d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
formalizations/guarded-cubical/Syntax/Context.agda 0 → 100644
+ 110
− 0
View file @ fa063583
module Syntax.Context where
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Relation.Nullary
open import Cubical.Foundations.Prelude
open import Cubical.Functions.FunExtEquiv
open import Cubical.Functions.Embedding
open import Cubical.Data.Nat
-- open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma
open import Cubical.Data.Sum hiding (map)
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit
-- open import Cubical.Data.Fin hiding (_/_)
open import Cubical.Data.FinSet
open import Cubical.Data.FinSet.Constructors
private
variable
ℓ ℓ' ℓ'' : Level
record Ctx (A : Type ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ-zero)) where
field
var : Type
isFinSetVar : isFinSet var
el : var → A
varFinSet : FinSet ℓ-zero
varFinSet = var , isFinSetVar
open Ctx
module _ {A : Type ℓ} where
Var : Ctx A → Type
Var Γ = Γ .var
Ctx≡ : (Γ Δ : Ctx A)
→ (p : Var Γ ≡ Var Δ)
→ PathP (λ i → p i → A) (Γ .el) (Δ .el)
→ Γ ≡ Δ
Ctx≡ Γ Δ p q i .var = p i
Ctx≡ Γ Δ p q i .isFinSetVar = lem i
where
lem : PathP (λ i → isFinSet (p i)) (Γ .isFinSetVar) (Δ .isFinSetVar)
lem = (isProp→PathP (λ i → isPropIsFinSet) (Γ .isFinSetVar) (Δ .isFinSetVar))
Ctx≡ Γ Δ p q i .el x = q i x
empty-ctx : Ctx A
empty-ctx .var = ⊥
empty-ctx .isFinSetVar = isFinSetFin
empty-ctx .el = λ ()
singleton : A → Ctx A
singleton a .var = Unit
singleton a .isFinSetVar = isFinSetUnit
singleton a .el = λ _ → a
-- the-var : (a : A) → singleton a .var
-- the-var a = tt
append : Ctx A → Ctx A → Ctx A
var (append Γ₁ Γ₂) = Γ₁ .var ⊎ Γ₂ .var
isFinSetVar (append Γ₁ Γ₂) = isFinSet⊎ (varFinSet Γ₁) (varFinSet Γ₂)
el (append Γ₁ Γ₂) (inl x₁) = Γ₁ .el x₁
el (append Γ₁ Γ₂) (inr x₂) = Γ₂ .el x₂
append-i₁-el : ∀ Γ₁ Γ₂ (x₁ : Γ₁ .var) → (append Γ₁ Γ₂) .el (inl x₁) ≡ Γ₁ .el x₁
append-i₁-el = λ Γ₁ Γ₂ x₁ → refl
cons : Ctx A → A → Ctx A
cons Γ a = append Γ (singleton a)
module _ (B : A → Type ℓ') where
substitution : ∀ (Γ : Ctx A) → Type ℓ'
substitution Γ = ∀ (x : Γ . var) → B (Γ .el x)
singleton-subst : (x : A) → B x → substitution (singleton x)
singleton-subst x b tt = b
append-subst : ∀ {Γ₁ Γ₂} → substitution Γ₁ → substitution Γ₂ → substitution (append Γ₁ Γ₂)
append-subst γ₁ γ₂ (inl x) = γ₁ x
append-subst γ₁ γ₂ (inr x) = γ₂ x
append-subst-inl : {Γ₁ Γ₂ : Ctx A} → (γ₁ : substitution Γ₁) → (γ₂ : substitution Γ₂)
→ (x₁ : Var Γ₁)
→ (append-subst {Γ₁ = Γ₁}{Γ₂ = Γ₂} γ₁ γ₂ (inl x₁)) ≡ (γ₁ x₁)
append-subst-inl γ₁ Γ₂ x₁ = refl
cons-subst : ∀ {Γ x} → substitution Γ → B x → substitution (cons Γ x)
cons-subst γ v = append-subst γ (singleton-subst _ v)
finProd : (X : FinSet ℓ-zero) → (X .fst → Ctx A) → Ctx A
finProd X Γs .var = Σ[ x ∈ X .fst ] Γs x .var
finProd X Γs .isFinSetVar = isFinSetΣ X λ x → _ , (Γs x .isFinSetVar)
finProd X Γs .el (x , y) = Γs x .el y
append-inj-el : ∀ (X : FinSet ℓ-zero) (Γs : X .fst → Ctx A) (x : X .fst) (y : Γs x .var)
→ finProd X Γs .el (x , y) ≡ Γs x .el y
append-inj-el X Γs x y = refl
module _ (B : A → Type ℓ') (X : FinSet ℓ-zero) (Γs : X .fst → Ctx A) where
finProdSubsts : (∀ (x : X .fst) → substitution B (Γs x)) → substitution B (finProd X Γs)
finProdSubsts γs (x , y) = γs x y
map : ∀ {A : Type ℓ}{A' : Type ℓ'} → (A → A') → Ctx A → Ctx A'
map f Γ .var = Γ .var
map f Γ .isFinSetVar = Γ .isFinSetVar
map f Γ .el x = f (Γ .el x)
formalizations/guarded-cubical/Syntax/SyntaxNew.agda
+ 190
− 153
View file @ fa063583
......@@ -9,10 +9,8 @@ open import Common.Later hiding (next)
module Syntax.SyntaxNew where
open import Cubical.Foundations.Prelude renaming (comp to compose)
open import Cubical.Data.Nat hiding (_·_) renaming (ℕ to Nat)
open import Cubical.Data.Nat hiding (_·_)
open import Cubical.Relation.Nullary
open import Cubical.Foundations.Function
open import Cubical.Data.Prod hiding (map)
......@@ -23,33 +21,15 @@ open import Cubical.Data.List
open import Cubical.Data.Empty renaming (rec to exFalso)
import Syntax.DeBruijnCommon
open import Syntax.Context
-- import Syntax.DeBruijnCommon
private
variable
ℓ : Level
ℓ ℓ' ℓ'' : Level
open import Syntax.Types
private
variable
α : IntExt
open Ctx
-- ############### Terms / Term Precision ###############
-- All constructors below except for those for upcast and downcast are simultaneously
......@@ -58,163 +38,220 @@ private
-- This explains why Ξ is generic in all but the up and dn constructors,
-- where it is Empty to indicate that we do not obtain term precision congruence rules.
data PureImpure : Type where
Pure Impure : PureImpure
data Tm : {v : PureImpure} -> {α : IntExt} -> {Ξ : iCtx} -> (Γ : Ctx {α} Ξ) -> Ty {α} Ξ -> Type ℓ-zero
-- data Val : {α : IntExt} -> {Ξ : iCtx} -> (Γ : Ctx {α} Ξ) -> Ty {α} Ξ -> Type ℓ-zero
tm-endpt : ∀ {v} {α} (p : Interval) -> {Γ : Ctx {α} Full} -> {c : Ty {α} Full} ->
Tm {v} {α} {Full} Γ c ->
Tm {v} {α} {Empty} (ctx-endpt p Γ) (ty-endpt p c)
_[_] : ∀ {α Γ A B}
→ Tm {Impure} {α} {Empty} (B :: Γ) A
→ Tm {Pure} {α} {Empty} Γ B
→ Tm {Impure} {α} {Empty} Γ A
_[_] = {!!}
wk : ∀ {v α Γ A B} -> Tm {v} {α} {Empty} Γ A ->
Tm {v} {α} {Empty} (B :: Γ) A
wk = {!!}
-- data Val where
data Tm where
var : ∀ {α Ξ Γ T} -> Γ ∋ T -> Tm {Pure} {α} {Ξ} Γ T
lda : ∀ {α Ξ Γ S T} -> (Tm {Impure} {α} {Ξ} (S :: Γ) T) -> Tm {Pure} Γ (S ⇀ T)
app : ∀ {α Ξ Γ S T} -> (Tm {Pure} {α} {Ξ} Γ (S ⇀ T)) -> (Tm {Pure} Γ S) -> (Tm {Impure} Γ T)
err : ∀ {α Ξ Γ A} -> Tm {Impure} {α} {Ξ} Γ A
zro : ∀ {α Ξ Γ} -> Tm {Pure} {α} {Ξ} Γ nat
suc : ∀ {α Ξ Γ} -> Tm {Pure} {α} {Ξ} Γ nat -> Tm {Pure} Γ nat
ret : ∀ {α Ξ Γ A} -> Tm {Pure} {α} {Ξ} Γ A -> Tm {Impure} Γ A
bind : ∀ {α Ξ Γ A B} -> Tm {Pure} {α} {Ξ} Γ A ->
Tm {Impure} {α} {Ξ} (A :: Γ) B -> Tm {Impure} {α} {Ξ} Γ B
inj-nat : ∀ {α Ξ Γ} -> Tm {Pure} {α} {Ξ} Γ nat -> Tm {Pure} Γ dyn
inj-arr-ext : ∀ {Ξ Γ} -> Tm {Pure} {Ext} {Ξ} Γ (dyn ⇀ dyn) -> Tm {Pure} {Ext} Γ dyn
inj-arr-int : ∀ {Ξ Γ} -> Tm {Pure} {Int} {Ξ} Γ (▹ (dyn ⇀ dyn)) -> Tm {Pure} {Int} Γ dyn
case-nat : ∀ {α Ξ Γ B} -> Tm {Pure} {α} {Ξ} Γ dyn ->
Tm {Impure} {α} {Ξ} (nat :: Γ) B -> Tm {Impure} {α} Γ B
case-arr-ext : ∀ {Ξ Γ B} -> Tm {Pure} {Ext} {Ξ} Γ dyn ->
Tm {Impure} {Ext} {Ξ} ((dyn ⇀ dyn) :: Γ) B -> Tm {Impure} {Ext} Γ B
case-arr-int : ∀ {Ξ Γ B} -> Tm {Pure} {Int} {Ξ} Γ dyn ->
Tm {Impure} {Int} {Ξ} ((▹ (dyn ⇀ dyn)) :: Γ) B -> Tm {Impure} {Int} Γ B
-- Other term precision rules:
data Val : (Ξ : iCtx) -> (Γ : TyCtx Ξ) -> Ty Ξ -> Type (ℓ-suc ℓ-zero)
data Comp : (Ξ : iCtx) -> (Γ : TyCtx Ξ) -> Ty Ξ -> Type (ℓ-suc ℓ-zero)
data EvCtx : (Ξ : iCtx) -> (Γ : TyCtx Ξ) -> Ty Ξ -> Ty Ξ -> Type (ℓ-suc ℓ-zero)
val-endpt : ∀ (p : Interval) -> {Γ : TyCtx Full} -> {c : Ty Full} ->
Val Full Γ c ->
Val Empty (ctx-endpt p Γ) (ty-endpt p c)
comp-endpt : ∀ (p : Interval) -> {Γ : TyCtx Full} -> {c : Ty Full} ->
Comp Full Γ c ->
Comp Empty (ctx-endpt p Γ) (ty-endpt p c)
evctx-endpt : ∀ (p : Interval) -> {Γ : TyCtx Full} -> {c : Ty Full} {d : Ty Full} ->
EvCtx Full Γ c d ->
EvCtx Empty (ctx-endpt p Γ) (ty-endpt p c) (ty-endpt p d)
-- TODO: strengthen the inductive hypothesis
--
-- Substitution : ∀ {Ξ} → TyCtx Ξ → TyCtx Ξ → Type (ℓ-suc ℓ-zero)
_[_]v : ∀ {Δ Γ A}
→ Val Empty Γ A
→ substitution (Val Empty Δ) Γ
→ Val Empty Δ A
_[_]c : ∀ {Δ Γ A}
→ Comp Empty Γ A
→ substitution (Val Empty Δ) Γ
→ Comp Empty Δ A
_[_]c1 : ∀ {Γ A B}
→ Comp Empty (cons Γ A) B
→ (Val Empty Γ A)
→ Comp Empty Γ B
-- wk : ∀ {v α Γ A B} -> Tm {v} {Empty} Γ A ->
-- Tm {v} {Empty} (B :: Γ) A
-- wk = {!!}
data Val where
varVal : ∀ {Ξ Γ} -> (x : Γ .var) -> Val Ξ Γ (Γ .el x)
lda : ∀ {Ξ Γ S T} -> (Comp Ξ (cons Γ S) T) -> Val Ξ Γ (S ⇀ T)
zro : ∀ {Ξ Γ} -> Val Ξ Γ nat
suc : ∀ {Ξ Γ} -> Val Ξ Γ nat -> Val Ξ Γ nat
up : ∀ {Γ} -> (S⊑T : Ty Full) -> Val Empty Γ (ty-left S⊑T) -> Val Empty Γ (ty-right S⊑T)
up-UB : ∀ {Γ} → (S⊑T : Ty Full) → Val Full Γ (ty-refl (ty-left S⊑T)) -> Val Full Γ S⊑T
up-LUB : ∀ {Γ} → (S⊑T : Ty Full) → Val Full Γ S⊑T -> Val Full Γ (ty-refl (ty-right S⊑T))
η-fun : ∀ {Γ A B} (Vf : Val Empty Γ (A ⇀ B)) ->
Vf ≡ lda (app ? ?)
-- lda (app (wk Vf) (var x)) ≡ Vf
trans : ∀ {Γ Δ : TyCtx Full} -> {A B : Ty Full} ->
(V : Val Full Γ A) -> (U : Val Full Δ B) ->
(ctx-p : ctx-endpt l Δ ≡ ctx-endpt r Γ) ->
(ty-p : ty-endpt l B ≡ ty-endpt r A)
(tm-p : PathP (λ i → Val Empty (ctx-p i) (ty-p i))
(val-endpt l {Δ} {B} U)
(val-endpt r {Γ} {A} V)) ->
Val Full (CompCtx Δ Γ ctx-p) (comp B A ty-p)
ord-squash : ∀ {Γ c} (leq leq' : Val Full Γ c) ->
(val-endpt l leq ≡ val-endpt l leq') →
(val-endpt r leq ≡ val-endpt r leq') ->
leq ≡ leq'
isSetVal : ∀ {Γ S} → isSet (Val Empty Γ S)
data Comp where
app : ∀ {Ξ Γ S T} → Val Ξ Γ (S ⇀ T) → Val Ξ Γ S → Comp Ξ Γ T
err : ∀ {Ξ Γ S} → Comp Ξ Γ S
ret : ∀ {Ξ Γ S} → Val Ξ Γ S → Comp Ξ Γ S
bind : ∀ {Ξ Γ S T} → Comp Ξ Γ S → Comp Ξ (cons Γ S) T → Comp Ξ Γ T
matchNat : ∀ {Ξ Γ S} → Val Ξ Γ nat → Comp Ξ Γ S → Comp Ξ (cons Γ nat) S → Comp Ξ Γ S
dn : ∀ {Γ} → (S⊑T : Ty Full) → Comp Empty Γ (ty-right S⊑T) → Comp Empty Γ (ty-left S⊑T)
dn-LB : ∀ {Γ} → (S⊑T : Ty Full) → Comp Full Γ (ty-refl (ty-right S⊑T)) -> Comp Full Γ S⊑T
dn-GLB : ∀ {Γ} → (S⊑T : Ty Full) → Comp Full Γ S⊑T -> Comp Full Γ (ty-refl (ty-left S⊑T))
-- effect rules
err-bot : ∀ {Γ} (B : Ty Empty) (M : Comp Empty Γ B) -> Comp Full (ctx-refl Γ) (ty-refl B)
-- TODO: strictness
-- βη
β-fun : ∀ {Γ A B} (M : Comp Empty (cons Γ A) B) (V : Val Empty Γ A) ->
app (lda M) V ≡ (M [ V ]c1)
trans : ∀ {Γ Δ : TyCtx Full} -> {A B : Ty Full} ->
(M : Comp Full Γ A) -> (N : Comp Full Δ B) ->
(ctx-p : ctx-endpt l Δ ≡ ctx-endpt r Γ) ->
(ty-p : ty-endpt l B ≡ ty-endpt r A)
(tm-p : PathP (λ i → Comp Empty (ctx-p i) (ty-p i))
(comp-endpt l {Δ} {B} N)
(comp-endpt r {Γ} {A} M)) ->
Comp Full (CompCtx Δ Γ ctx-p) (comp B A ty-p)
ord-squash : ∀ {Γ c} (leq leq' : Comp Full Γ c) ->
(comp-endpt l leq ≡ comp-endpt l leq') →
(comp-endpt r leq ≡ comp-endpt r leq') ->
leq ≡ leq'
isSetComp : ∀ {Γ S} → isSet (Comp Empty Γ S)
data EvCtx where
val-endpt = {!!}
comp-endpt = {!!}
evctx-endpt = {!!}
_[_]v = {!!}
_[_]c = {!!}
M [ V ]c1 = M [ cons-subst (Val Empty _) varVal V ]c
-- data Tm where
-- app : ∀ {α Ξ Γ S T} -> (Tm {Pure} {Ξ} Γ (S ⇀ T)) -> (Tm {Pure} Γ S) -> (Tm {Impure} Γ T)
-- err : ∀ {α Ξ Γ A} -> Tm {Impure} {Ξ} Γ A
-- ret : ∀ {α Ξ Γ A} -> Tm {Pure} {Ξ} Γ A -> Tm {Impure} Γ A
-- bind : ∀ {α Ξ Γ A B} -> Tm {Pure} {Ξ} Γ A ->
-- Tm {Impure} {Ξ} (A :: Γ) B -> Tm {Impure} {Ξ} Γ B
-- inj-nat : ∀ {α Ξ Γ} -> Tm {Pure} {Ξ} Γ nat -> Tm {Pure} Γ dyn
-- inj-arr-ext : ∀ {Ξ Γ} -> Tm {Pure} {Ext} {Ξ} Γ (dyn ⇀ dyn) -> Tm {Pure} {Ext} Γ dyn
-- inj-arr-int : ∀ {Ξ Γ} -> Tm {Pure} {Int} {Ξ} Γ (▹ (dyn ⇀ dyn)) -> Tm {Pure} {Int} Γ dyn
-- case-nat : ∀ {α Ξ Γ B} -> Tm {Pure} {Ξ} Γ dyn ->
-- Tm {Impure} {Ξ} (nat :: Γ) B -> Tm {Impure} Γ B
-- case-arr-ext : ∀ {Ξ Γ B} -> Tm {Pure} {Ext} {Ξ} Γ dyn ->
-- Tm {Impure} {Ext} {Ξ} ((dyn ⇀ dyn) :: Γ) B -> Tm {Impure} {Ext} Γ B
-- case-arr-int : ∀ {Ξ Γ B} -> Tm {Pure} {Int} {Ξ} Γ dyn ->
-- Tm {Impure} {Int} {Ξ} ((▹ (dyn ⇀ dyn)) :: Γ) B -> Tm {Impure} {Int} Γ B
-- -- Other term precision rules:
err-bot : ∀ {α Γ} (B : Ty {α} Empty) (M : Tm {Impure} {α} {Empty} Γ B) -> Tm {Impure} {α} {Full} (ctx-refl Γ) (ty-refl B)
--err-bot : ∀ {α} {Γ : Ctx Full} (c : Ty Full)
-- (M : Tm {Impure} {α} {Empty} (ctx-endpt r Γ) (ty-right c)) -> Tm {Impure} {α} {Full} Γ c
-- TODO do we need to restrict the left endpoint of Γ?
-- err-bot : ∀ {α Γ} (B : Ty Empty) (M : Tm {Impure} {Empty} Γ B) -> Tm {Impure} {Full} (ctx-refl Γ) (ty-refl B)
-- --err-bot : ∀ {Γ : TyCtx Full} (c : Ty Full)
-- -- (M : Tm {Impure} {Empty} (ctx-endpt r Γ) (ty-right c)) -> Tm {Impure} {Full} Γ c
-- -- TODO do we need to restrict the left endpoint of Γ?
trans : ∀ {v : PureImpure} {Γ Δ : Ctx {α} Full} -> {A B : Ty Full} ->
(M : Tm {v} Γ A) -> (N : Tm {v} Δ B) ->
(ctx-p : ctx-endpt l Δ ≡ ctx-endpt r Γ) ->
(ty-p : ty-endpt l B ≡ ty-endpt r A)
(tm-p : PathP (λ i → Tm {v} (ctx-p i) (ty-p i)) (tm-endpt l {Δ} {B} N) (tm-endpt r {Γ} {A} M)) ->
Tm {v} (CompCtx Δ Γ ctx-p) (comp B A ty-p)
-- trans : ∀ {v : PureImpure} {Γ Δ : TyCtx Full} -> {A B : Ty Full} ->
-- (M : Tm {v} Γ A) -> (N : Tm {v} Δ B) ->
-- (ctx-p : ctx-endpt l Δ ≡ ctx-endpt r Γ) ->
-- (ty-p : ty-endpt l B ≡ ty-endpt r A)
-- (tm-p : PathP (λ i → Tm {v} (ctx-p i) (ty-p i)) (tm-endpt l {Δ} {B} N) (tm-endpt r {Γ} {A} M)) ->
-- Tm {v} (CompCtx Δ Γ ctx-p) (comp B A ty-p)
-- Cast rules
-- -- Cast rules
-- Equational theory:
-- -- Equational theory:
β-fun : ∀ {α Γ A B} {M : Tm {Impure} {α} {Empty} (A :: Γ) B} {V : Tm {Pure} {α} {Empty} Γ A} ->
app (lda M) V ≡ M [ V ]
η-fun : ∀ {α Γ A B} {Vf : Tm {Pure} {α} {Empty} Γ (A ⇀ B)} {x : (A :: Γ) ∋ A} ->
lda (app (wk Vf) (var x)) ≡ Vf
-- {-
-- β-case :
{-
β-case :
η-case :
-- η-case :
β-ret :
-- β-ret :
η-ret :
-}
-- η-ret :
-- -}
-- Propositional truncation:
-- -- Propositional truncation:
-- squash : ∀ {v α Ξ Γ A} -> (M N : Tm {v} {α} {Ξ} Γ A) -> (p q : M ≡ N) -> p ≡ q
squash : ∀ {v α Ξ Γ A} -> isSet (Tm {v} {α} {Ξ} Γ A)
-- -- squash : ∀ {v α Ξ Γ A} -> (M N : Tm {v} {Ξ} Γ A) -> (p q : M ≡ N) -> p ≡ q
-- squash : ∀ {v α Ξ Γ A} -> isSet (Tm {v} {Ξ} Γ A)
-- Quotient the ordering:
-- -- Quotient the ordering:
ord-squash : ∀ {v α Γ c}
(M : Tm {v} {α} {Empty} (ctx-endpt l Γ) (ty-left c))
(N : Tm {v} {α} {Empty} (ctx-endpt r Γ) (ty-right c)) ->
(leq leq' : Tm {v} {α} {Full} Γ c) ->
(tm-endpt l {Γ} {c} leq ≡ M) -> (tm-endpt r {Γ} {c} leq ≡ N) ->
(tm-endpt l {Γ} {c} leq' ≡ M) -> (tm-endpt r {Γ} {c} leq' ≡ N) ->
leq ≡ leq'
_⊑tm_ : ∀ {v α Γ A B} {c : A ⊑ B} ->
Tm {v} {α} {Empty} (ctx-endpt l Γ) A -> Tm {v} {α} {Empty} (ctx-endpt r Γ) B -> Type
-- _⊑tm_ : ∀ {v α Γ A B} {c : A ⊑ B} ->
-- Tm {v} {Empty} (ctx-endpt l Γ) A -> Tm {v} {Empty} (ctx-endpt r Γ) B -> Type
_⊑tm_ {v} {α} {Γ} {A} {B} {c , eq1 , eq2} M N = Σ[ M⊑N ∈ Tm {v} {α} {Full} Γ c ]
((tm-endpt l {Γ} {c} M⊑N ≡ subst (Tm (ctx-endpt l Γ)) (sym eq1) M) ×
(tm-endpt r {Γ} {c} M⊑N ≡ subst (Tm (ctx-endpt r Γ)) (sym eq2) N))
-- _⊑tm_ {v} {Γ} {A} {B} {c , eq1 , eq2} M N = Σ[ M⊑N ∈ Tm {v} {Full} Γ c ]
-- ((tm-endpt l {Γ} {c} M⊑N ≡ subst (Tm (ctx-endpt l Γ)) (sym eq1) M) ×
-- (tm-endpt r {Γ} {c} M⊑N ≡ subst (Tm (ctx-endpt r Γ)) (sym eq2) N))
-- Recall:
-- tm-endpt : (p : Interval) -> {Γ : Ctx Full} -> {c : Ty Full} ->
-- tm-endpt : (p : Interval) -> {Γ : TyCtx Full} -> {c : Ty Full} ->
-- Tm {Full} Γ c ->
-- Tm {Empty} (ctx-endpt p Γ) (ty-endpt p c)
-- tm-endpt = ?
-- tm-endpt p {Γ} {c} (var x) = var (∋-ctx-endpt p x)
-- tm-endpt p {Γ} {(_ ⇀ cout)} (lda M1⊑M2) = lda (tm-endpt p {(_ :: Γ)} {cout} M1⊑M2)
-- tm-endpt p {Γ} {cout} (app {S = cin} M1⊑M2 N1⊑N2) =
-- app (tm-endpt p {Γ} {(cin ⇀ cout)} M1⊑M2) (tm-endpt p {Γ} {cin} N1⊑N2)
tm-endpt p {Γ} {c} (var x) = var (∋-ctx-endpt p x)
tm-endpt p {Γ} {(_ ⇀ cout)} (lda M1⊑M2) = lda (tm-endpt p {(_ :: Γ)} {cout} M1⊑M2)
tm-endpt p {Γ} {cout} (app {S = cin} M1⊑M2 N1⊑N2) =
app (tm-endpt p {Γ} {(cin ⇀ cout)} M1⊑M2) (tm-endpt p {Γ} {cin} N1⊑N2)
tm-endpt p {Γ} {c} err = err
tm-endpt p {Γ} zro = zro
tm-endpt p {Γ} (suc M1⊑M2) = suc (tm-endpt p {Γ} {nat} M1⊑M2)
-- tm-endpt p {Γ} {c} err = err
-- tm-endpt p {Γ} zro = zro
-- tm-endpt p {Γ} (suc M1⊑M2) = suc (tm-endpt p {Γ} {nat} M1⊑M2)
-- Term-precision-only rules
--tm-endpt l .(ctx-refl _) c (err-bot .c N) = err
--tm-endpt r .(ctx-refl _) c (err-bot {Γ} .c N) =
-- transport (sym (λ i → Tm (ctx-endpt-refl {Γ} r i) (ty-right c))) N
-- Goal: Tm Γ (ty-right c) ≡ Tm (ctx-endpt r (ctx-refl Γ)) (ty-right c)
-- -- Term-precision-only rules
-- --tm-endpt l .(ctx-refl _) c (err-bot .c N) = err
-- --tm-endpt r .(ctx-refl _) c (err-bot {Γ} .c N) =
-- -- transport (sym (λ i → Tm (ctx-endpt-refl {Γ} r i) (ty-right c))) N
-- -- Goal: Tm Γ (ty-right c) ≡ Tm (ctx-endpt r (ctx-refl Γ)) (ty-right c)
tm-endpt p (err-bot B x) = {!!}
-- tm-endpt p (err-bot B x) = {!!}
tm-endpt l {Γ} (trans c _ _ _ _) = {!!}
tm-endpt r {Γ} (trans c _ _ _ _) = {!!}
-- tm-endpt l {Γ} (trans c _ _ _ _) = {!!}
-- tm-endpt r {Γ} (trans c _ _ _ _) = {!!}
-- Truncation
tm-endpt p {Γ} {c} (squash M1⊑M2 M1'⊑M2' eq eq' i j) =
squash (tm-endpt p {Γ} {c} M1⊑M2) (tm-endpt p {Γ} {c} M1'⊑M2')
(λ k → tm-endpt p {Γ} {c} (eq k)) (λ k → tm-endpt p {Γ} {c} (eq' k)) i j
-- -- Truncation
-- tm-endpt p {Γ} {c} (squash M1⊑M2 M1'⊑M2' eq eq' i j) =
-- squash (tm-endpt p {Γ} {c} M1⊑M2) (tm-endpt p {Γ} {c} M1'⊑M2')
-- (λ k → tm-endpt p {Γ} {c} (eq k)) (λ k → tm-endpt p {Γ} {c} (eq' k)) i j
tm-endpt p (ret x) = {!!}
tm-endpt p (bind x x₁) = {!!}
tm-endpt p (inj-nat x) = {!!}
tm-endpt p (inj-arr-ext x) = {!!}
tm-endpt p (inj-arr-int x) = {!!}
tm-endpt p (case-nat x x₁) = {!!}
tm-endpt p (case-arr-ext x x₁) = {!!}
tm-endpt p (case-arr-int x x₁) = {!!}
tm-endpt p (ord-squash x x₁ x₂ x₃ x₄ x₅ x₆ x₇ i) = {!!}
-- tm-endpt p (ret x) = {!!}
-- tm-endpt p (bind x x₁) = {!!}
-- tm-endpt p (inj-nat x) = {!!}
-- tm-endpt p (inj-arr-ext x) = {!!}
-- tm-endpt p (inj-arr-int x) = {!!}
-- tm-endpt p (case-nat x x₁) = {!!}
-- tm-endpt p (case-arr-ext x x₁) = {!!}
-- tm-endpt p (case-arr-int x x₁) = {!!}
-- tm-endpt p (ord-squash x x₁ x₂ x₃ x₄ x₅ x₆ x₇ i) = {!!}
......@@ -224,13 +261,13 @@ tm-endpt p (ord-squash x x₁ x₂ x₃ x₄ x₅ x₆ x₇ i) = {!!}
{-
-- Substitution and Renaming using De Bruijn framework
module DB_Base = Syntax.DeBruijnCommon (Ty Empty) (Ctx Empty) · (_::_) _∋_ vz vs (Tm Ext {Empty})
module DB_Base = Syntax.DeBruijnCommon (Ty Empty) (TyCtx Empty) · (_::_) _∋_ vz vs (Tm Ext {Empty})
open DB_Base -- Brings in definitions of ProofT, Kit, Subst
-- Lift function --
lft : {Δ Γ : Ctx Empty} {S : Ty Empty} {_◈_ : ProofT}
lft : {Δ Γ : TyCtx Empty} {S : Ty Empty} {_◈_ : ProofT}
(K : Kit _◈_) (τ : Subst Δ Γ _◈_) {T : Ty Empty} (h : (Γ :: S) ∋ T) -> (Δ :: S) ◈ T
lft (kit vr tm wk) τ vz = vr vz
lft (kit vr tm wk) τ (vs x) = wk (τ x)
......@@ -238,7 +275,7 @@ lft (kit vr tm wk) τ (vs x) = wk (τ x)
-- Traversal function --
trav : {Δ Γ : Ctx Empty} {T : Ty Empty} {_◈_ : ProofT} (K : Kit _◈_)
trav : {Δ Γ : TyCtx Empty} {T : Ty Empty} {_◈_ : ProofT} (K : Kit _◈_)
(τ : Subst Δ Γ _◈_) (t : Tm Ext Γ T) -> Tm Ext Δ T
trav (kit vr tm wk) τ (var x) = tm (τ x)
trav K τ (lda t') = (lda (trav K (lft K τ) t'))
......
formalizations/guarded-cubical/Syntax/Types.agda
+ 5
− 9
View file @ fa063583
......@@ -10,14 +10,10 @@ open import Common.Later hiding (next)
module Syntax.Types where
open import Cubical.Foundations.Prelude renaming (comp to compose)
open import Cubical.Data.Nat hiding (_·_) renaming (ℕ to Nat)
open import Cubical.Data.Nat
open import Cubical.Relation.Nullary
open import Cubical.Foundations.Function
open import Cubical.Data.Prod hiding (map)
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.List
using (List ; length ; map ; _++_ ; cons-inj₁ ; cons-inj₂)
renaming ([] to · ; _∷_ to _::_)
open import Cubical.Data.Empty renaming (rec to exFalso)
open import Syntax.Context as Context
......@@ -36,10 +32,12 @@ data iCtx : Type where
Empty : iCtx
Full : iCtx
endpt-fun : ∀ {ℓ} → (iCtx → Type ℓ) → Type ℓ
endpt-fun {ℓ} A = Interval → A Full → A Empty
data Ty : iCtx -> Type
ty-endpt : Interval -> Ty Full -> Ty Empty
ty-endpt : endpt-fun Ty
_⊑_ : Ty Empty -> Ty Empty -> Type
A ⊑ B = Σ[ c ∈ Ty Full ] ((ty-endpt l c ≡ A) × (ty-endpt r c ≡ B))
......@@ -108,7 +106,7 @@ TyCtx : iCtx → Type (ℓ-suc ℓ-zero)
TyCtx Ξ = Ctx (Ty Ξ)
-- Endpoints of a full context
ctx-endpt : (p : Interval) -> TyCtx Full -> TyCtx Empty
ctx-endpt : endpt-fun TyCtx
ctx-endpt p = Context.map (ty-endpt p)
CompCtx : (Δ Γ : TyCtx Full)
......@@ -143,5 +141,3 @@ ctx-refl = Context.map ty-refl
-- context are the typing context itself.
ctx-endpt-refl : {Γ : TyCtx Empty} -> (p : Interval) -> ctx-endpt p (ctx-refl Γ) ≡ Γ
ctx-endpt-refl {Γ} p = Ctx≡ _ _ refl (funExt λ x → ty-endpt-refl {A = Γ .el x} p)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment