Skip to content

Commit

Permalink
[ re #10 ] separate Size & I
Browse files Browse the repository at this point in the history
  • Loading branch information
@gallais
gallais committed Nov 22, 2021
1 parent d2eeaa0 commit 0f7c7f9
Show file tree
Hide file tree
Showing 4 changed files with 40 additions and 38 deletions.
37 changes: 19 additions & 18 deletions doc/common/Data/Environment.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,8 @@ private

variable
I A : Set
i σ : I
i : Size
σ : I
S T : List I → Set
𝓥 𝓦 𝓒 : I ─Scoped
Γ Δ Θ : List I
Expand All @@ -30,7 +31,7 @@ infix 3 _─Env
\begin{code}
record _─Env (Γ : List I) (𝓥 : I ─Scoped) (Δ : List I) : Set where
constructor pack
field lookup : Var i Γ → 𝓥 i Δ
field lookup : Var σ Γ → 𝓥 σ Δ
\end{code}
%</env>
\begin{code}
Expand All @@ -51,17 +52,17 @@ lookup ε ()
%</empty>
%<*envmap>
\begin{code}
_<$>_ : (∀ {i} → 𝓥 i Δ → 𝓦 i Θ) → (Γ ─Env) 𝓥 Δ → (Γ ─Env) 𝓦 Θ
_<$>_ : (∀ {σ} → 𝓥 σ Δ → 𝓦 σ Θ) → (Γ ─Env) 𝓥 Δ → (Γ ─Env) 𝓦 Θ
lookup (f <$> ρ) k = f (lookup ρ k)
\end{code}
%</envmap>
\begin{code}

data Split (i : I) Γ Δ : Var i (Γ ++ Δ) → Set where
inj₁ : (k : Var i Γ) → Split i Γ Δ (injectˡ Δ k)
inj₂ : (k : Var i Δ) → Split i Γ Δ (injectʳ Γ k)
data Split (σ : I) Γ Δ : Var σ (Γ ++ Δ) → Set where
inj₁ : (k : Var σ Γ) → Split σ Γ Δ (injectˡ Δ k)
inj₂ : (k : Var σ Δ) → Split σ Γ Δ (injectʳ Γ k)

split : ∀ Γ (k : Var i (Γ ++ Δ)) → Split i Γ Δ k
split : ∀ Γ (k : Var σ (Γ ++ Δ)) → Split σ Γ Δ k
split [] k = inj₂ k
split (σ ∷ Γ) z = inj₁ z
split (σ ∷ Γ) (s k) with split Γ k
Expand All @@ -81,11 +82,11 @@ lookup (_>>_ {Γ = Γ} ρ₁ ρ₂) k with split Γ k
... | inj₁ k₁ = lookup ρ₁ k₁
... | inj₂ k₂ = lookup ρ₂ k₂

injectˡ->> : ∀ (ρ₁ : (Γ ─Env) 𝓥 Θ) (ρ₂ : (Δ ─Env) 𝓥 Θ) (v : Var i Γ) →
injectˡ->> : ∀ (ρ₁ : (Γ ─Env) 𝓥 Θ) (ρ₂ : (Δ ─Env) 𝓥 Θ) (v : Var σ Γ) →
lookup (ρ₁ >> ρ₂) (injectˡ Δ v) ≡ lookup ρ₁ v
injectˡ->> {Δ = Δ} ρ₁ ρ₂ v rewrite split-injectˡ Δ v = refl

injectʳ->> : ∀ (ρ₁ : (Γ ─Env) 𝓥 Θ) (ρ₂ : (Δ ─Env) 𝓥 Θ) (v : Var i Δ) →
injectʳ->> : ∀ (ρ₁ : (Γ ─Env) 𝓥 Θ) (ρ₂ : (Δ ─Env) 𝓥 Θ) (v : Var σ Δ) →
lookup (ρ₁ >> ρ₂) (injectʳ Γ v) ≡ lookup ρ₂ v
injectʳ->> {Γ = Γ} ρ₁ ρ₂ v rewrite split-injectʳ Γ v = refl

Expand Down Expand Up @@ -130,12 +131,12 @@ _<+>_ : (Δ ─Env) 𝓥 Θ → (Γ ─Env) 𝓥 Θ → (Γ ++ Δ ─Env) 𝓥
_<+>_ {Γ = []} ρ₁ ρ₂ = ρ₁
_<+>_ {Γ = _ ∷ Γ} ρ₁ ρ₂ = (ρ₁ <+> select weaken ρ₂) ∙ lookup ρ₂ z

injectˡ-<+> : ∀ Δ (ρ₁ : (Δ ─Env) 𝓥 Θ) (ρ₂ : (Γ ─Env) 𝓥 Θ) (v : Var i Γ) →
injectˡ-<+> : ∀ Δ (ρ₁ : (Δ ─Env) 𝓥 Θ) (ρ₂ : (Γ ─Env) 𝓥 Θ) (v : Var σ Γ) →
lookup (ρ₁ <+> ρ₂) (injectˡ Δ v) ≡ lookup ρ₂ v
injectˡ-<+> Δ ρ₁ ρ₂ z = refl
injectˡ-<+> Δ ρ₁ ρ₂ (s v) = injectˡ-<+> Δ ρ₁ (select weaken ρ₂) v

injectʳ-<+> : ∀ Γ (ρ₁ : (Δ ─Env) 𝓥 Θ) (ρ₂ : (Γ ─Env) 𝓥 Θ) (v : Var i Δ) →
injectʳ-<+> : ∀ Γ (ρ₁ : (Δ ─Env) 𝓥 Θ) (ρ₂ : (Γ ─Env) 𝓥 Θ) (v : Var σ Δ) →
lookup (ρ₁ <+> ρ₂) (injectʳ Γ v) ≡ lookup ρ₁ v
injectʳ-<+> [] ρ₁ ρ₂ v = refl
injectʳ-<+> (x ∷ Γ) ρ₁ ρ₂ v = injectʳ-<+> Γ ρ₁ (select weaken ρ₂) v
Expand Down Expand Up @@ -184,13 +185,13 @@ Thinnable T = ∀[ T ⇒ □ T ]
%</thinnable>
%<*thVar>
\begin{code}
th^Var : Thinnable (Var i)
th^Var : Thinnable (Var σ)
th^Var v ρ = lookup ρ v
\end{code}
%</thVar>
%<*thEnv>
\begin{code}
th^Env : (∀ {i} → Thinnable (𝓥 i)) → Thinnable ((Γ ─Env) 𝓥)
th^Env : (∀ {σ} → Thinnable (𝓥 σ)) → Thinnable ((Γ ─Env) 𝓥)
lookup (th^Env th^𝓥 ρ ren) k = th^𝓥 (lookup ρ k) ren
\end{code}
%</thEnv>
Expand Down Expand Up @@ -264,12 +265,12 @@ Kripke 𝓥 𝓒 Δ j = □ ((Δ ─Env) 𝓥 ⇒ 𝓒 j)
%</kripke>
\begin{code}

_$$_ : ∀[ Kripke 𝓥 𝓒 Γ i ⇒ (Γ ─Env) 𝓥 ⇒ 𝓒 i ]
_$$_ : ∀[ Kripke 𝓥 𝓒 Γ σ ⇒ (Γ ─Env) 𝓥 ⇒ 𝓒 σ ]
_$$_ {Γ = []} f ts = f
_$$_ {Γ = _ ∷ _} f ts = extract f ts

th^Kr : (Γ : List I) → (∀ {i} → Thinnable (𝓒 i)) →
Thinnable (Kripke 𝓥 𝓒 Γ i)
th^Kr : (Γ : List I) → (∀ {σ} → Thinnable (𝓒 σ)) →
Thinnable (Kripke 𝓥 𝓒 Γ σ)
th^Kr [] th^𝓒 = th^𝓒
th^Kr (_ ∷ _) th^𝓒 = th^□

Expand All @@ -280,10 +281,10 @@ module _ {A : Set → Set} {{app : RawApplicative A}} where
private module A = RawApplicative app
open A

sequenceA : (Γ ─Env) (λ i Γ → A (𝓥 i Γ)) Δ → A ((Γ ─Env) 𝓥 Δ)
sequenceA : (Γ ─Env) (λ σ Γ → A (𝓥 σ Γ)) Δ → A ((Γ ─Env) 𝓥 Δ)
sequenceA = go _ where

go : ∀ Γ → (Γ ─Env) (λ i Γ → A (𝓥 i Γ)) Δ → A ((Γ ─Env) 𝓥 Δ)
go : ∀ Γ → (Γ ─Env) (λ σ Γ → A (𝓥 σ Γ)) Δ → A ((Γ ─Env) 𝓥 Δ)
go [] ρ = pure ε
go (σ ∷ Γ) ρ = _∙_ A.<$> go Γ (select weaken ρ) ⊛ lookup ρ z
\end{code}
2 changes: 1 addition & 1 deletion doc/common/Data/Var.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ data Var : I ─Scoped where
%</var>
\begin{code}
infixl 3 _─_
_─_ : {i : I} (Γ : List I) → Var i Γ → List I
_─_ : {σ : I} (Γ : List I) → Var σ Γ → List I
_ ∷ Γ ─ z = Γ
σ ∷ Γ ─ s v = σ ∷ (Γ ─ v)

Expand Down
37 changes: 19 additions & 18 deletions src/Data/Environment.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,8 @@ private

variable
I A : Set
i σ : I
i : Size
σ : I
S T : List I → Set
𝓥 𝓦 𝓒 : I ─Scoped
Γ Δ Θ : List I
Expand All @@ -27,7 +28,7 @@ infix 3 _─Env

record _─Env (Γ : List I) (𝓥 : I ─Scoped) (Δ : List I) : Set where
constructor pack
field lookup : Var i Γ → 𝓥 i Δ
field lookup : Var σ Γ → 𝓥 σ Δ


open _─Env public
Expand All @@ -38,15 +39,15 @@ Thinning Γ Δ = (Γ ─Env) Var Δ
ε : ([] ─Env) 𝓥 Δ
lookup ε ()

_<$>_ : (∀ {i} → 𝓥 i Δ → 𝓦 i Θ) → (Γ ─Env) 𝓥 Δ → (Γ ─Env) 𝓦 Θ
_<$>_ : (∀ {σ} → 𝓥 σ Δ → 𝓦 σ Θ) → (Γ ─Env) 𝓥 Δ → (Γ ─Env) 𝓦 Θ
lookup (f <$> ρ) k = f (lookup ρ k)


data Split (i : I) Γ Δ : Var i (Γ ++ Δ) → Set where
inj₁ : (k : Var i Γ) → Split i Γ Δ (injectˡ Δ k)
inj₂ : (k : Var i Δ) → Split i Γ Δ (injectʳ Γ k)
data Split (σ : I) Γ Δ : Var σ (Γ ++ Δ) → Set where
inj₁ : (k : Var σ Γ) → Split σ Γ Δ (injectˡ Δ k)
inj₂ : (k : Var σ Δ) → Split σ Γ Δ (injectʳ Γ k)

split : ∀ Γ (k : Var i (Γ ++ Δ)) → Split i Γ Δ k
split : ∀ Γ (k : Var σ (Γ ++ Δ)) → Split σ Γ Δ k
split [] k = inj₂ k
split (σ ∷ Γ) z = inj₁ z
split (σ ∷ Γ) (s k) with split Γ k
Expand All @@ -66,11 +67,11 @@ lookup (_>>_ {Γ = Γ} ρ₁ ρ₂) k with split Γ k
... | inj₁ k₁ = lookup ρ₁ k₁
... | inj₂ k₂ = lookup ρ₂ k₂

injectˡ->> : ∀ (ρ₁ : (Γ ─Env) 𝓥 Θ) (ρ₂ : (Δ ─Env) 𝓥 Θ) (v : Var i Γ) →
injectˡ->> : ∀ (ρ₁ : (Γ ─Env) 𝓥 Θ) (ρ₂ : (Δ ─Env) 𝓥 Θ) (v : Var σ Γ) →
lookup (ρ₁ >> ρ₂) (injectˡ Δ v) ≡ lookup ρ₁ v
injectˡ->> {Δ = Δ} ρ₁ ρ₂ v rewrite split-injectˡ Δ v = refl

injectʳ->> : ∀ (ρ₁ : (Γ ─Env) 𝓥 Θ) (ρ₂ : (Δ ─Env) 𝓥 Θ) (v : Var i Δ) →
injectʳ->> : ∀ (ρ₁ : (Γ ─Env) 𝓥 Θ) (ρ₂ : (Δ ─Env) 𝓥 Θ) (v : Var σ Δ) →
lookup (ρ₁ >> ρ₂) (injectʳ Γ v) ≡ lookup ρ₂ v
injectʳ->> {Γ = Γ} ρ₁ ρ₂ v rewrite split-injectʳ Γ v = refl

Expand Down Expand Up @@ -98,12 +99,12 @@ _<+>_ : (Δ ─Env) 𝓥 Θ → (Γ ─Env) 𝓥 Θ → (Γ ++ Δ ─Env) 𝓥
_<+>_ {Γ = []} ρ₁ ρ₂ = ρ₁
_<+>_ {Γ = _ ∷ Γ} ρ₁ ρ₂ = (ρ₁ <+> select weaken ρ₂) ∙ lookup ρ₂ z

injectˡ-<+> : ∀ Δ (ρ₁ : (Δ ─Env) 𝓥 Θ) (ρ₂ : (Γ ─Env) 𝓥 Θ) (v : Var i Γ) →
injectˡ-<+> : ∀ Δ (ρ₁ : (Δ ─Env) 𝓥 Θ) (ρ₂ : (Γ ─Env) 𝓥 Θ) (v : Var σ Γ) →
lookup (ρ₁ <+> ρ₂) (injectˡ Δ v) ≡ lookup ρ₂ v
injectˡ-<+> Δ ρ₁ ρ₂ z = refl
injectˡ-<+> Δ ρ₁ ρ₂ (s v) = injectˡ-<+> Δ ρ₁ (select weaken ρ₂) v

injectʳ-<+> : ∀ Γ (ρ₁ : (Δ ─Env) 𝓥 Θ) (ρ₂ : (Γ ─Env) 𝓥 Θ) (v : Var i Δ) →
injectʳ-<+> : ∀ Γ (ρ₁ : (Δ ─Env) 𝓥 Θ) (ρ₂ : (Γ ─Env) 𝓥 Θ) (v : Var σ Δ) →
lookup (ρ₁ <+> ρ₂) (injectʳ Γ v) ≡ lookup ρ₁ v
injectʳ-<+> [] ρ₁ ρ₂ v = refl
injectʳ-<+> (x ∷ Γ) ρ₁ ρ₂ v = injectʳ-<+> Γ ρ₁ (select weaken ρ₂) v
Expand Down Expand Up @@ -136,10 +137,10 @@ module □ where
Thinnable : (List I → Set) → Set
Thinnable T = ∀[ T ⇒ □ T ]

th^Var : Thinnable (Var i)
th^Var : Thinnable (Var σ)
th^Var v ρ = lookup ρ v

th^Env : (∀ {i} → Thinnable (𝓥 i)) → Thinnable ((Γ ─Env) 𝓥)
th^Env : (∀ {σ} → Thinnable (𝓥 σ)) → Thinnable ((Γ ─Env) 𝓥)
lookup (th^Env th^𝓥 ρ ren) k = th^𝓥 (lookup ρ k) ren

th^□ : Thinnable (□ T)
Expand Down Expand Up @@ -200,12 +201,12 @@ Kripke 𝓥 𝓒 [] j = 𝓒 j
Kripke 𝓥 𝓒 Δ j = □ ((Δ ─Env) 𝓥 ⇒ 𝓒 j)


_$$_ : ∀[ Kripke 𝓥 𝓒 Γ i ⇒ (Γ ─Env) 𝓥 ⇒ 𝓒 i ]
_$$_ : ∀[ Kripke 𝓥 𝓒 Γ σ ⇒ (Γ ─Env) 𝓥 ⇒ 𝓒 σ ]
_$$_ {Γ = []} f ts = f
_$$_ {Γ = _ ∷ _} f ts = extract f ts

th^Kr : (Γ : List I) → (∀ {i} → Thinnable (𝓒 i)) →
Thinnable (Kripke 𝓥 𝓒 Γ i)
th^Kr : (Γ : List I) → (∀ {σ} → Thinnable (𝓒 σ)) →
Thinnable (Kripke 𝓥 𝓒 Γ σ)
th^Kr [] th^𝓒 = th^𝓒
th^Kr (_ ∷ _) th^𝓒 = th^□

Expand All @@ -216,9 +217,9 @@ module _ {A : Set → Set} {{app : RawApplicative A}} where
private module A = RawApplicative app
open A

sequenceA : (Γ ─Env) (λ i Γ → A (𝓥 i Γ)) Δ → A ((Γ ─Env) 𝓥 Δ)
sequenceA : (Γ ─Env) (λ σ Γ → A (𝓥 σ Γ)) Δ → A ((Γ ─Env) 𝓥 Δ)
sequenceA = go _ where

go : ∀ Γ → (Γ ─Env) (λ i Γ → A (𝓥 i Γ)) Δ → A ((Γ ─Env) 𝓥 Δ)
go : ∀ Γ → (Γ ─Env) (λ σ Γ → A (𝓥 σ Γ)) Δ → A ((Γ ─Env) 𝓥 Δ)
go [] ρ = pure ε
go (σ ∷ Γ) ρ = _∙_ A.<$> go Γ (select weaken ρ) ⊛ lookup ρ z
2 changes: 1 addition & 1 deletion src/Data/Var.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ data Var : I ─Scoped where
s : ∀[ Var σ ⇒ (τ ∷_) ⊢ Var σ ]

infixl 3 _─_
_─_ : {i : I} (Γ : List I) → Var i Γ → List I
_─_ : {σ : I} (Γ : List I) → Var σ Γ → List I
_ ∷ Γ ─ z = Γ
σ ∷ Γ ─ s v = σ ∷ (Γ ─ v)

Expand Down

0 comments on commit 0f7c7f9

Please sign in to comment.