module Definition.Untyped.Properties {a} (M : Set a) where
open import Definition.Untyped M
open import Definition.Untyped.Inversion M
open import Definition.Untyped.Properties.NotParametrised public
open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.List
open import Tools.Nat as Nat
open import Tools.Relation
open import Tools.Product as Σ
open import Tools.PropositionalEquality as PE
open import Tools.Reasoning.PropositionalEquality
open import Tools.Relation
open import Tools.Sum
open import Tools.Vec as Vec using (ε)
private
variable
j ℓ m m₁ m₂ n n₁ n₂ o α β : Nat
x x₁ x₂ : Fin _
as : List _
eq eq₁ eq₂ : _ ≡ _
𝕋 𝕌 : Set _
∇ ∇′ : DCon _ _
ξ : DExt _ _ _
Γ : Con Term _
Δ : Cons _ _
φ : Unfolding _
A A₁ A₂ B B₁ B₂ C C₁ C₂ D E F G H
l l′ l₁ l₂ t t₁ t₂ u u₁ u₂ v v₁ v₂ v₃ w w₁ w₂ :
Term[ _ ] _
k : Term-kind
ts₁ ts₂ : Args _ _
ρ ρ′ : Wk m n
η : Wk n ℓ
σ σ₁ σ₂ σ′ : Subst m n
p p₁ p₂ q q₁ q₂ r r₁ r₂ : M
s s₁ s₂ : Strength
b₁ b₂ : BinderMode
f : 𝕋 → 𝕌
𝓙 : Judgement _
opaque
↦∷∈⇒↦∈ : ∀ {A t} → α ↦ t ∷ A ∈ ∇ → α ↦∷ A ∈ ∇
↦∷∈⇒↦∈ here = here
↦∷∈⇒↦∈ (there α↦t) = there (↦∷∈⇒↦∈ α↦t)
opaque
↦⊘∈⇒↦∈ : ∀ {A} → α ↦⊘∷ A ∈ ∇ → α ↦∷ A ∈ ∇
↦⊘∈⇒↦∈ here = here
↦⊘∈⇒↦∈ (there α↦⊘) = there (↦⊘∈⇒↦∈ α↦⊘)
opaque
scoped-↦∈ : ∀ {∇ : DCon 𝕋 n} {A} → α ↦∷ A ∈ ∇ → α < n
scoped-↦∈ here = s≤s ≤-refl
scoped-↦∈ (there α↦∷A) = s≤s (≤⇒pred≤ (scoped-↦∈ α↦∷A))
opaque
scoped-↦∷∈ : ∀ {∇ : DCon 𝕋 n} {A t} → α ↦ t ∷ A ∈ ∇ → α < n
scoped-↦∷∈ α↦t = scoped-↦∈ (↦∷∈⇒↦∈ α↦t)
opaque
scoped-↦⊘∈ : ∀ {∇ : DCon 𝕋 n} {A} → α ↦⊘∷ A ∈ ∇ → α < n
scoped-↦⊘∈ α↦⊘ = scoped-↦∈ (↦⊘∈⇒↦∈ α↦⊘)
opaque
unique-↦∈ : ∀ {A B} → α ↦∷ A ∈ ∇ → β ↦∷ B ∈ ∇ → α ≡ β → A ≡ B
unique-↦∈ here here _ = refl
unique-↦∈ here (there α↦u) refl = ⊥-elim (n≮n _ (scoped-↦∈ α↦u))
unique-↦∈ (there α↦t) here refl = ⊥-elim (n≮n _ (scoped-↦∈ α↦t))
unique-↦∈ (there α↦t) (there β↦u) α≡β = unique-↦∈ α↦t β↦u α≡β
opaque
unique-↦∷∈ :
∀ {A B t u} → α ↦ t ∷ A ∈ ∇ → β ↦ u ∷ B ∈ ∇ → α ≡ β → A ≡ B × t ≡ u
unique-↦∷∈ here here _ = refl , refl
unique-↦∷∈ here (there α↦u) refl = ⊥-elim (n≮n _ (scoped-↦∷∈ α↦u))
unique-↦∷∈ (there α↦t) here refl = ⊥-elim (n≮n _ (scoped-↦∷∈ α↦t))
unique-↦∷∈ (there α↦t) (there β↦u) α≡β = unique-↦∷∈ α↦t β↦u α≡β
opaque
unique-↦⊘∈ : ∀ {A B} → α ↦⊘∷ A ∈ ∇ → β ↦⊘∷ B ∈ ∇ → α ≡ β → A ≡ B
unique-↦⊘∈ α↦⊘ β↦⊘ α≡β = unique-↦∈ (↦⊘∈⇒↦∈ α↦⊘) (↦⊘∈⇒↦∈ β↦⊘) α≡β
opaque
coerce-↦∷∈ : ∀ {A B t} → α ↦∷ B ∈ ∇ → α ↦ t ∷ A ∈ ∇ → α ↦ t ∷ B ∈ ∇
coerce-↦∷∈ α↦∷B α↦t = subst (_ ↦ _ ∷_∈ _)
(unique-↦∈ (↦∷∈⇒↦∈ α↦t) α↦∷B refl)
α↦t
opaque
coerce-↦⊘∈ : ∀ {A B} → α ↦∷ B ∈ ∇ → α ↦⊘∷ A ∈ ∇ → α ↦⊘∷ B ∈ ∇
coerce-↦⊘∈ α↦∷B α↦⊘ = subst (_ ↦⊘∷_∈ _)
(unique-↦∈ (↦⊘∈⇒↦∈ α↦⊘) α↦∷B refl)
α↦⊘
opaque
dichotomy-↦∈ : ∀ {A} → α ↦∷ A ∈ ∇ → (∃ λ t → α ↦ t ∷ A ∈ ∇) ⊎ (α ↦⊘∷ A ∈ ∇)
dichotomy-↦∈ {∇ = ∇ ∙⟨ opa φ ⟩[ t ∷ A ]} here = inj₂ here
dichotomy-↦∈ {∇ = ∇ ∙⟨ tra ⟩[ t ∷ A ]} here = inj₁ (t , here)
dichotomy-↦∈ (there α↦∷A) =
case dichotomy-↦∈ α↦∷A of λ where
(inj₁ (t , α↦t)) → inj₁ (t , there α↦t)
(inj₂ α↦⊘) → inj₂ (there α↦⊘)
opaque
exclusion-↦∈ :
∀ {A B t} → α ↦⊘∷ A ∈ ∇ → ¬ α ↦ t ∷ B ∈ ∇
exclusion-↦∈ here (there α↦t) = n≮n _ (scoped-↦∷∈ α↦t)
exclusion-↦∈ (there α↦⊘) here = n≮n _ (scoped-↦⊘∈ α↦⊘)
exclusion-↦∈ (there α↦⊘) (there α↦t) = exclusion-↦∈ α↦⊘ α↦t
opaque
unfolding _⊔ᵒ_
assoc-⊔ᵒ :
(φ φ′ φ″ : Unfolding n) → φ ⊔ᵒ (φ′ ⊔ᵒ φ″) PE.≡ (φ ⊔ᵒ φ′) ⊔ᵒ φ″
assoc-⊔ᵒ ε ε ε = PE.refl
assoc-⊔ᵒ (φ ⁰) (φ′ ⁰) (φ″ ⁰) = PE.cong _⁰ (assoc-⊔ᵒ φ φ′ φ″)
assoc-⊔ᵒ (φ ⁰) (φ′ ⁰) (φ″ ¹) = PE.cong _¹ (assoc-⊔ᵒ φ φ′ φ″)
assoc-⊔ᵒ (φ ⁰) (φ′ ¹) (φ″ ⁰) = PE.cong _¹ (assoc-⊔ᵒ φ φ′ φ″)
assoc-⊔ᵒ (φ ⁰) (φ′ ¹) (φ″ ¹) = PE.cong _¹ (assoc-⊔ᵒ φ φ′ φ″)
assoc-⊔ᵒ (φ ¹) (φ′ ⁰) (φ″ ⁰) = PE.cong _¹ (assoc-⊔ᵒ φ φ′ φ″)
assoc-⊔ᵒ (φ ¹) (φ′ ⁰) (φ″ ¹) = PE.cong _¹ (assoc-⊔ᵒ φ φ′ φ″)
assoc-⊔ᵒ (φ ¹) (φ′ ¹) (φ″ ⁰) = PE.cong _¹ (assoc-⊔ᵒ φ φ′ φ″)
assoc-⊔ᵒ (φ ¹) (φ′ ¹) (φ″ ¹) = PE.cong _¹ (assoc-⊔ᵒ φ φ′ φ″)
opaque
unfolding _⊔ᵒ_
comm-⊔ᵒ : (φ φ′ : Unfolding n) → φ ⊔ᵒ φ′ PE.≡ φ′ ⊔ᵒ φ
comm-⊔ᵒ ε ε = PE.refl
comm-⊔ᵒ (φ ⁰) (φ′ ⁰) = PE.cong _⁰ (comm-⊔ᵒ φ φ′)
comm-⊔ᵒ (φ ⁰) (φ′ ¹) = PE.cong _¹ (comm-⊔ᵒ φ φ′)
comm-⊔ᵒ (φ ¹) (φ′ ⁰) = PE.cong _¹ (comm-⊔ᵒ φ φ′)
comm-⊔ᵒ (φ ¹) (φ′ ¹) = PE.cong _¹ (comm-⊔ᵒ φ φ′)
opaque
unfolding ones _⊔ᵒ_
ones-⊔ᵒˡ : ones ⊔ᵒ φ ≡ ones
ones-⊔ᵒˡ {φ = ε} = refl
ones-⊔ᵒˡ {φ = _ Vec.∷ _} = cong (_ Vec.∷_) ones-⊔ᵒˡ
opaque
ones-⊔ᵒʳ : φ ⊔ᵒ ones ≡ ones
ones-⊔ᵒʳ {φ} =
φ ⊔ᵒ ones ≡⟨ comm-⊔ᵒ _ _ ⟩
ones ⊔ᵒ φ ≡⟨ ones-⊔ᵒˡ ⟩
ones ∎
opaque
unfolding zeros _⊔ᵒ_
zeros-⊔ᵒˡ : zeros ⊔ᵒ φ PE.≡ φ
zeros-⊔ᵒˡ {φ = ε} = refl
zeros-⊔ᵒˡ {φ = _ Vec.∷ _} = cong (_ Vec.∷_) zeros-⊔ᵒˡ
opaque
zeros-⊔ᵒʳ : φ ⊔ᵒ zeros PE.≡ φ
zeros-⊔ᵒʳ {φ} =
φ ⊔ᵒ zeros ≡⟨ comm-⊔ᵒ _ _ ⟩
zeros ⊔ᵒ φ ≡⟨ zeros-⊔ᵒˡ ⟩
φ ∎
opaque
glassify-↦∈ : ∀ {A} → α ↦∷ A ∈ ∇ → α ↦∷ A ∈ glassify ∇
glassify-↦∈ here = here
glassify-↦∈ (there α↦∷A) = there (glassify-↦∈ α↦∷A)
opaque
unglass-↦∈ : ∀ {A} → α ↦∷ A ∈ glassify ∇ → α ↦∷ A ∈ ∇
unglass-↦∈ {∇ = ε} ()
unglass-↦∈ {∇ = ∇ ∙⟨ ω ⟩[ t ∷ A ]} here = here
unglass-↦∈ {∇ = ∇ ∙⟨ ω ⟩[ t ∷ A ]} (there α↦∷A) = there (unglass-↦∈ α↦∷A)
opaque
glassify-↦∷∈ : ∀ {A t} → α ↦ t ∷ A ∈ ∇ → α ↦ t ∷ A ∈ glassify ∇
glassify-↦∷∈ here = here
glassify-↦∷∈ (there α↦t) = there (glassify-↦∷∈ α↦t)
opaque
glass-↦⊘∈ : ∀ {A} → ¬ α ↦⊘∷ A ∈ glassify ∇
glass-↦⊘∈ {∇ = ε} ()
glass-↦⊘∈ {∇ = ∇ ∙⟨ ω ⟩[ t ∷ A ]} (there α↦⊘) = glass-↦⊘∈ α↦⊘
opaque
glass-↦∈ : ∀ {A} → α ↦∷ A ∈ glassify ∇ → ∃ λ t → α ↦ t ∷ A ∈ glassify ∇
glass-↦∈ α↦∷A = case dichotomy-↦∈ α↦∷A of λ where
(inj₁ ∃t) → ∃t
(inj₂ α↦⊘) → ⊥-elim (glass-↦⊘∈ α↦⊘)
opaque
glassify-↦∈′ : ∀ {A} → α ↦∷ A ∈ ∇ → ∃ λ t → α ↦ t ∷ A ∈ glassify ∇
glassify-↦∈′ = glass-↦∈ ∘→ glassify-↦∈
opaque
glassify-map-DCon : glassify (map-DCon f ∇) ≡ map-DCon f (glassify ∇)
glassify-map-DCon {∇ = ε} = refl
glassify-map-DCon {∇ = _ ∙!} = cong _∙! glassify-map-DCon
opaque
toTerm∘fromTerm : (t : Term[ k ] n) → toTerm (fromTerm t) ≡ t
toTerm∘fromTerm (var x) = refl
toTerm∘fromTerm (defn α) = refl
toTerm∘fromTerm Level = refl
toTerm∘fromTerm zeroᵘ = refl
toTerm∘fromTerm (sucᵘ l) = cong sucᵘ (toTerm∘fromTerm l)
toTerm∘fromTerm (l₁ supᵘ l₂) =
cong₂ _supᵘ_ (toTerm∘fromTerm l₁) (toTerm∘fromTerm l₂)
toTerm∘fromTerm (ωᵘ+ _) = refl
toTerm∘fromTerm (level t) = cong level (toTerm∘fromTerm t)
toTerm∘fromTerm (U l) = cong U (toTerm∘fromTerm l)
toTerm∘fromTerm (Lift l A) =
cong₂ Lift (toTerm∘fromTerm l) (toTerm∘fromTerm A)
toTerm∘fromTerm (lift a) =
cong lift (toTerm∘fromTerm a)
toTerm∘fromTerm (lower a) =
cong lower (toTerm∘fromTerm a)
toTerm∘fromTerm (ΠΣ⟨ b ⟩ p , q ▷ A ▹ B) =
cong₂ (ΠΣ⟨ b ⟩ p , q ▷_▹_) (toTerm∘fromTerm A) (toTerm∘fromTerm B)
toTerm∘fromTerm (lam p t) =
cong (lam p) (toTerm∘fromTerm t)
toTerm∘fromTerm (t ∘⟨ p ⟩ u) =
cong₂ (_∘⟨ p ⟩_) (toTerm∘fromTerm t) (toTerm∘fromTerm u)
toTerm∘fromTerm (prod s p t u) =
cong₂ (prod s p) (toTerm∘fromTerm t) (toTerm∘fromTerm u)
toTerm∘fromTerm (fst p t) =
cong (fst p) (toTerm∘fromTerm t)
toTerm∘fromTerm (snd p t) =
cong (snd p) (toTerm∘fromTerm t)
toTerm∘fromTerm (prodrec r p q A t u) =
cong₃ (prodrec r p q) (toTerm∘fromTerm A)
(toTerm∘fromTerm t) (toTerm∘fromTerm u)
toTerm∘fromTerm ℕ = refl
toTerm∘fromTerm zero = refl
toTerm∘fromTerm (suc t) =
cong suc (toTerm∘fromTerm t)
toTerm∘fromTerm (natrec p q r A z s n) =
cong₄ (natrec p q r) (toTerm∘fromTerm A) (toTerm∘fromTerm z)
(toTerm∘fromTerm s) (toTerm∘fromTerm n)
toTerm∘fromTerm (Unit s) = refl
toTerm∘fromTerm (star s) = refl
toTerm∘fromTerm (unitrec p q A t u) =
cong₃ (unitrec p q) (toTerm∘fromTerm A)
(toTerm∘fromTerm t) (toTerm∘fromTerm u)
toTerm∘fromTerm Empty = refl
toTerm∘fromTerm (emptyrec p A t) =
cong₂ (emptyrec p) (toTerm∘fromTerm A) (toTerm∘fromTerm t)
toTerm∘fromTerm (Id A t u) =
cong₃ Id (toTerm∘fromTerm A) (toTerm∘fromTerm t) (toTerm∘fromTerm u)
toTerm∘fromTerm rfl = refl
toTerm∘fromTerm (J p q A t B u v w) =
cong₆ (J p q) (toTerm∘fromTerm A) (toTerm∘fromTerm t)
(toTerm∘fromTerm B) (toTerm∘fromTerm u)
(toTerm∘fromTerm v) (toTerm∘fromTerm w)
toTerm∘fromTerm (K p A t B u v) =
cong₅ (K p) (toTerm∘fromTerm A) (toTerm∘fromTerm t)
(toTerm∘fromTerm B) (toTerm∘fromTerm u) (toTerm∘fromTerm v)
toTerm∘fromTerm ([]-cong s l A t u v) =
cong₅ ([]-cong s) (toTerm∘fromTerm l) (toTerm∘fromTerm A)
(toTerm∘fromTerm t) (toTerm∘fromTerm u) (toTerm∘fromTerm v)
toTerm∘fromTerm (Quot A B) =
cong₂ Quot (toTerm∘fromTerm A) (toTerm∘fromTerm B)
toTerm∘fromTerm (class t) =
cong class (toTerm∘fromTerm t)
toTerm∘fromTerm (resp A B t u v) =
cong₅ resp (toTerm∘fromTerm A) (toTerm∘fromTerm B)
(toTerm∘fromTerm t) (toTerm∘fromTerm u) (toTerm∘fromTerm v)
toTerm∘fromTerm (set A B t u v w) =
cong₆ set (toTerm∘fromTerm A) (toTerm∘fromTerm B)
(toTerm∘fromTerm t) (toTerm∘fromTerm u) (toTerm∘fromTerm v)
(toTerm∘fromTerm w)
toTerm∘fromTerm (qrec C t u v w) =
cong₅ qrec (toTerm∘fromTerm C) (toTerm∘fromTerm t)
(toTerm∘fromTerm u) (toTerm∘fromTerm v) (toTerm∘fromTerm w)
opaque
fromTerm∘toTerm : (t : Term[ k ]′ n) → fromTerm (toTerm t) ≡ t
fromTerm∘toTerm (var x) =
refl
fromTerm∘toTerm (con (defnᵏ α) []) =
refl
fromTerm∘toTerm (con Levelᵏ []) =
refl
fromTerm∘toTerm (con zeroᵘᵏ []) =
refl
fromTerm∘toTerm (con sucᵘᵏ (t ∷ₜ [])) =
cong (λ t → con sucᵘᵏ (t ∷ₜ [])) (fromTerm∘toTerm t)
fromTerm∘toTerm (con supᵘᵏ (t₁ ∷ₜ t₂ ∷ₜ [])) =
cong₂ (λ t₁ t₂ → con supᵘᵏ (t₁ ∷ₜ t₂ ∷ₜ [])) (fromTerm∘toTerm t₁)
(fromTerm∘toTerm t₂)
fromTerm∘toTerm (con (ωᵘ+ᵏ _) []) =
refl
fromTerm∘toTerm (con levelᵏ (t ∷ₜ [])) =
cong (λ t → con levelᵏ (t ∷ₜ [])) (fromTerm∘toTerm t)
fromTerm∘toTerm (con Uᵏ (l ∷ₜ [])) =
cong (λ l → con Uᵏ (l ∷ₜ [])) (fromTerm∘toTerm l)
fromTerm∘toTerm (con Liftᵏ (l ∷ₜ A ∷ₜ [])) =
cong₂ (λ l A → con Liftᵏ (l ∷ₜ A ∷ₜ [])) (fromTerm∘toTerm l)
(fromTerm∘toTerm A)
fromTerm∘toTerm (con liftᵏ (t ∷ₜ [])) =
cong (λ t → con liftᵏ (t ∷ₜ [])) (fromTerm∘toTerm t)
fromTerm∘toTerm (con lowerᵏ (t ∷ₜ [])) =
cong (λ t → con lowerᵏ (t ∷ₜ [])) (fromTerm∘toTerm t)
fromTerm∘toTerm (con Emptyᵏ []) = refl
fromTerm∘toTerm (con (emptyrecᵏ p) (A ∷ₜ t ∷ₜ [])) =
cong₂ (λ A t → con (emptyrecᵏ p) (A ∷ₜ t ∷ₜ [])) (fromTerm∘toTerm A)
(fromTerm∘toTerm t)
fromTerm∘toTerm (con (Unitᵏ s) []) =
refl
fromTerm∘toTerm (con (starᵏ s) []) =
refl
fromTerm∘toTerm (con (unitrecᵏ p q) (A ∷ₜ t ∷ₜ u ∷ₜ [])) =
cong₃ (λ A t u → con (unitrecᵏ p q) (A ∷ₜ t ∷ₜ u ∷ₜ []))
(fromTerm∘toTerm A) (fromTerm∘toTerm t) (fromTerm∘toTerm u)
fromTerm∘toTerm (con (ΠΣᵏ b p q) (A ∷ₜ B ∷ₜ [])) =
cong₂ (λ A B → con (ΠΣᵏ b p q) (A ∷ₜ B ∷ₜ [])) (fromTerm∘toTerm A)
(fromTerm∘toTerm B)
fromTerm∘toTerm (con (lamᵏ p) (t ∷ₜ [])) =
cong (λ t → con (lamᵏ p) (t ∷ₜ [])) (fromTerm∘toTerm t)
fromTerm∘toTerm (con (appᵏ p) (t ∷ₜ u ∷ₜ [])) =
cong₂ (λ t u → con (appᵏ p) (t ∷ₜ u ∷ₜ [])) (fromTerm∘toTerm t)
(fromTerm∘toTerm u)
fromTerm∘toTerm (con (prodᵏ s p) (t ∷ₜ u ∷ₜ [])) =
cong₂ (λ t u → con (prodᵏ s p) (t ∷ₜ u ∷ₜ [])) (fromTerm∘toTerm t)
(fromTerm∘toTerm u)
fromTerm∘toTerm (con (fstᵏ p) (t ∷ₜ [])) =
cong (λ t → con (fstᵏ p) (t ∷ₜ [])) (fromTerm∘toTerm t)
fromTerm∘toTerm (con (sndᵏ p) (t ∷ₜ [])) =
cong (λ t → con (sndᵏ p) (t ∷ₜ [])) (fromTerm∘toTerm t)
fromTerm∘toTerm (con (prodrecᵏ r p q) (A ∷ₜ t ∷ₜ u ∷ₜ [])) =
cong₃ (λ A t u → con (prodrecᵏ r p q) (A ∷ₜ t ∷ₜ u ∷ₜ []))
(fromTerm∘toTerm A) (fromTerm∘toTerm t) (fromTerm∘toTerm u)
fromTerm∘toTerm (con ℕᵏ []) =
refl
fromTerm∘toTerm (con zeroᵏ []) =
refl
fromTerm∘toTerm (con sucᵏ (t ∷ₜ [])) =
cong (λ t → con sucᵏ (t ∷ₜ [])) (fromTerm∘toTerm t)
fromTerm∘toTerm (con (natrecᵏ p q r) (A ∷ₜ z ∷ₜ s ∷ₜ n ∷ₜ [])) =
cong₄ (λ A z s n → con (natrecᵏ p q r) (A ∷ₜ z ∷ₜ s ∷ₜ n ∷ₜ []))
(fromTerm∘toTerm A) (fromTerm∘toTerm z) (fromTerm∘toTerm s)
(fromTerm∘toTerm n)
fromTerm∘toTerm (con Idᵏ (A ∷ₜ t ∷ₜ u ∷ₜ [])) =
cong₃ (λ A t u → con Idᵏ (A ∷ₜ t ∷ₜ u ∷ₜ [])) (fromTerm∘toTerm A)
(fromTerm∘toTerm t) (fromTerm∘toTerm u)
fromTerm∘toTerm (con rflᵏ []) = refl
fromTerm∘toTerm (con (Jᵏ p q) (A ∷ₜ t ∷ₜ B ∷ₜ u ∷ₜ v ∷ₜ w ∷ₜ [])) =
cong₆ (λ A t B u v w →
con (Jᵏ p q) (A ∷ₜ t ∷ₜ B ∷ₜ u ∷ₜ v ∷ₜ w ∷ₜ []))
(fromTerm∘toTerm A) (fromTerm∘toTerm t) (fromTerm∘toTerm B)
(fromTerm∘toTerm u) (fromTerm∘toTerm v) (fromTerm∘toTerm w)
fromTerm∘toTerm (con (Kᵏ p) (A ∷ₜ t ∷ₜ B ∷ₜ u ∷ₜ v ∷ₜ [])) =
cong₅ (λ A t B u v → con (Kᵏ p) (A ∷ₜ t ∷ₜ B ∷ₜ u ∷ₜ v ∷ₜ []))
(fromTerm∘toTerm A) (fromTerm∘toTerm t) (fromTerm∘toTerm B)
(fromTerm∘toTerm u) (fromTerm∘toTerm v)
fromTerm∘toTerm (con ([]-congᵏ s) (l ∷ₜ A ∷ₜ t ∷ₜ u ∷ₜ v ∷ₜ [])) =
cong₅
(λ l A t u v → con ([]-congᵏ s) (l ∷ₜ A ∷ₜ t ∷ₜ u ∷ₜ v ∷ₜ []))
(fromTerm∘toTerm l) (fromTerm∘toTerm A) (fromTerm∘toTerm t)
(fromTerm∘toTerm u) (fromTerm∘toTerm v)
fromTerm∘toTerm (con Quotᵏ (A ∷ₜ B ∷ₜ [])) =
cong₂ (λ A B → con Quotᵏ (A ∷ₜ B ∷ₜ [])) (fromTerm∘toTerm A)
(fromTerm∘toTerm B)
fromTerm∘toTerm (con classᵏ (t ∷ₜ [])) =
cong (λ t → con classᵏ (t ∷ₜ [])) (fromTerm∘toTerm t)
fromTerm∘toTerm (con respᵏ (A ∷ₜ B ∷ₜ t ∷ₜ u ∷ₜ v ∷ₜ [])) =
cong₅ (λ A B t u v → con respᵏ (A ∷ₜ B ∷ₜ t ∷ₜ u ∷ₜ v ∷ₜ []))
(fromTerm∘toTerm A) (fromTerm∘toTerm B) (fromTerm∘toTerm t)
(fromTerm∘toTerm u) (fromTerm∘toTerm v)
fromTerm∘toTerm (con setᵏ (A ∷ₜ B ∷ₜ t ∷ₜ u ∷ₜ v ∷ₜ w ∷ₜ [])) =
cong₆ (λ A B t u v w → con setᵏ (A ∷ₜ B ∷ₜ t ∷ₜ u ∷ₜ v ∷ₜ w ∷ₜ []))
(fromTerm∘toTerm A) (fromTerm∘toTerm B) (fromTerm∘toTerm t)
(fromTerm∘toTerm u) (fromTerm∘toTerm v) (fromTerm∘toTerm w)
fromTerm∘toTerm (con qrecᵏ (C ∷ₜ t ∷ₜ u ∷ₜ v ∷ₜ w ∷ₜ [])) =
cong₅ (λ C t u v w → con qrecᵏ (C ∷ₜ t ∷ₜ u ∷ₜ v ∷ₜ w ∷ₜ []))
(fromTerm∘toTerm C) (fromTerm∘toTerm t) (fromTerm∘toTerm u)
(fromTerm∘toTerm v) (fromTerm∘toTerm w)
opaque
toTerm-injective :
{t₁ t₂ : Term[ k ]′ n} → toTerm t₁ ≡ toTerm t₂ → t₁ ≡ t₂
toTerm-injective {t₁} {t₂} eq =
t₁ ≡˘⟨ fromTerm∘toTerm _ ⟩
fromTerm (toTerm t₁) ≡⟨ cong fromTerm eq ⟩
fromTerm (toTerm t₂) ≡⟨ fromTerm∘toTerm _ ⟩
t₂ ∎
opaque
fromTerm-injective : fromTerm t₁ ≡ fromTerm t₂ → t₁ ≡ t₂
fromTerm-injective {t₁} {t₂} eq =
t₁ ≡˘⟨ toTerm∘fromTerm _ ⟩
toTerm (fromTerm t₁) ≡⟨ cong toTerm eq ⟩
toTerm (fromTerm t₂) ≡⟨ toTerm∘fromTerm _ ⟩
t₂ ∎
Level≢B : ∀ W → Level PE.≢ ⟦ W ⟧ F ▹ G
Level≢B (BΠ p q) ()
Level≢B (BΣ m p q) ()
Level≢ΠΣ : ∀ b → Level PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
Level≢ΠΣ BMΠ ()
Level≢ΠΣ (BMΣ s) ()
U≢B : ∀ W → U l PE.≢ ⟦ W ⟧ F ▹ G
U≢B (BΠ p q) ()
U≢B (BΣ m p q) ()
U≢ΠΣ : ∀ b → U l PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
U≢ΠΣ BMΠ ()
U≢ΠΣ (BMΣ s) ()
Lift≢B : ∀ W → Lift l A PE.≢ ⟦ W ⟧ F ▹ G
Lift≢B (BΠ p q) ()
Lift≢B (BΣ m p q) ()
Lift≢ΠΣ : ∀ b → Lift l A PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
Lift≢ΠΣ BMΠ ()
Lift≢ΠΣ (BMΣ s) ()
ℕ≢B : ∀ W → ℕ PE.≢ ⟦ W ⟧ F ▹ G
ℕ≢B (BΠ p q) ()
ℕ≢B (BΣ m p q) ()
ℕ≢ΠΣ : ∀ b → ℕ PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
ℕ≢ΠΣ BMΠ ()
ℕ≢ΠΣ (BMΣ s) ()
Empty≢B : ∀ W → Empty PE.≢ ⟦ W ⟧ F ▹ G
Empty≢B (BΠ p q) ()
Empty≢B (BΣ m p q) ()
Empty≢ΠΣ : ∀ b → Empty PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
Empty≢ΠΣ BMΠ ()
Empty≢ΠΣ (BMΣ _) ()
Unit≢B : ∀ W → Unit s PE.≢ ⟦ W ⟧ F ▹ G
Unit≢B (BΠ p q) ()
Unit≢B (BΣ m p q) ()
Unit≢ΠΣ : ∀ b → Unit s PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
Unit≢ΠΣ BMΠ ()
Unit≢ΠΣ (BMΣ _) ()
Id≢⟦⟧▷ : ∀ W → Id A t u PE.≢ ⟦ W ⟧ F ▹ G
Id≢⟦⟧▷ (BΠ _ _) ()
Id≢⟦⟧▷ (BΣ _ _ _) ()
Id≢ΠΣ : ∀ b → Id A t u PE.≢ ΠΣ⟨ b ⟩ p , q ▷ F ▹ G
Id≢ΠΣ BMΠ ()
Id≢ΠΣ (BMΣ _) ()
Quot≢⟦⟧▷ : ∀ W → Quot A B PE.≢ ⟦ W ⟧ C ▹ D
Quot≢⟦⟧▷ (BΠ _ _) ()
Quot≢⟦⟧▷ (BΣ _ _ _) ()
Quot≢ΠΣ : ∀ b → Quot A B PE.≢ ΠΣ⟨ b ⟩ p , q ▷ C ▹ D
Quot≢ΠΣ BMΠ ()
Quot≢ΠΣ (BMΣ _) ()
Π≢Σ : ∀ {m} → Π p₁ , q₁ ▷ F ▹ G PE.≢ Σ⟨ m ⟩ p₂ , q₂ ▷ H ▹ E
Π≢Σ ()
Σˢ≢Σʷ : Σˢ p₁ , q₁ ▷ F ▹ G PE.≢ Σʷ p₂ , q₂ ▷ H ▹ E
Σˢ≢Σʷ ()
opaque
wk≡wk′ : (t : Term[ k ] n) → wk ρ t ≡ toTerm (wk′ ρ (fromTerm t))
wk≡wk′ (var x) = refl
wk≡wk′ (defn α) = refl
wk≡wk′ Level = refl
wk≡wk′ zeroᵘ = refl
wk≡wk′ (sucᵘ t) = cong sucᵘ (wk≡wk′ t)
wk≡wk′ (t₁ supᵘ t₂) = cong₂ _supᵘ_ (wk≡wk′ t₁) (wk≡wk′ t₂)
wk≡wk′ (ωᵘ+ _) = refl
wk≡wk′ (level t) = cong level (wk≡wk′ t)
wk≡wk′ (U l) = cong U (wk≡wk′ l)
wk≡wk′ (Lift l A) = cong₂ Lift (wk≡wk′ l) (wk≡wk′ A)
wk≡wk′ (lift a) = cong lift (wk≡wk′ a)
wk≡wk′ (lower a) = cong lower (wk≡wk′ a)
wk≡wk′ (ΠΣ⟨ b ⟩ p , q ▷ t ▹ t₁) =
cong₂ (ΠΣ⟨ b ⟩ p , q ▷_▹_) (wk≡wk′ t) (wk≡wk′ t₁)
wk≡wk′ (lam p t) = cong (lam p) (wk≡wk′ t)
wk≡wk′ (t ∘⟨ p ⟩ t₁) = cong₂ _∘_ (wk≡wk′ t) (wk≡wk′ t₁)
wk≡wk′ (prod x p t t₁) = cong₂ prod! (wk≡wk′ t) (wk≡wk′ t₁)
wk≡wk′ (fst p t) = cong (fst p) (wk≡wk′ t)
wk≡wk′ (snd p t) = cong (snd p) (wk≡wk′ t)
wk≡wk′ (prodrec r p q t t₁ t₂) =
cong₃ (prodrec r p q) (wk≡wk′ t) (wk≡wk′ t₁) (wk≡wk′ t₂)
wk≡wk′ ℕ = refl
wk≡wk′ zero = refl
wk≡wk′ (suc t) = cong suc (wk≡wk′ t)
wk≡wk′ (natrec p q r t t₁ t₂ t₃) =
cong₄ (natrec p q r) (wk≡wk′ t) (wk≡wk′ t₁) (wk≡wk′ t₂) (wk≡wk′ t₃)
wk≡wk′ (Unit x) = refl
wk≡wk′ (star x) = refl
wk≡wk′ (unitrec p q t t₁ t₂) =
cong₃ (unitrec p q) (wk≡wk′ t) (wk≡wk′ t₁) (wk≡wk′ t₂)
wk≡wk′ Empty = refl
wk≡wk′ (emptyrec p t t₁) =
cong₂ (emptyrec p) (wk≡wk′ t) (wk≡wk′ t₁)
wk≡wk′ (Id t t₁ t₂) =
cong₃ Id (wk≡wk′ t) (wk≡wk′ t₁) (wk≡wk′ t₂)
wk≡wk′ rfl = refl
wk≡wk′ (J p q t t₁ t₂ t₃ t₄ t₅) =
cong₆ (J p q) (wk≡wk′ t) (wk≡wk′ t₁) (wk≡wk′ t₂)
(wk≡wk′ t₃) (wk≡wk′ t₄) (wk≡wk′ t₅)
wk≡wk′ (K p t t₁ t₂ t₃ t₄) =
cong₅ (K p) (wk≡wk′ t) (wk≡wk′ t₁) (wk≡wk′ t₂)
(wk≡wk′ t₃) (wk≡wk′ t₄)
wk≡wk′ ([]-cong _ l A t u v) =
cong₅ []-cong! (wk≡wk′ l) (wk≡wk′ A) (wk≡wk′ t) (wk≡wk′ u)
(wk≡wk′ v)
wk≡wk′ (Quot A B) =
cong₂ Quot (wk≡wk′ A) (wk≡wk′ B)
wk≡wk′ (class t) =
cong class (wk≡wk′ t)
wk≡wk′ (resp A B t u v) =
cong₅ resp (wk≡wk′ A) (wk≡wk′ B) (wk≡wk′ t) (wk≡wk′ u) (wk≡wk′ v)
wk≡wk′ (set A B t u v w) =
cong₆ set (wk≡wk′ A) (wk≡wk′ B) (wk≡wk′ t) (wk≡wk′ u) (wk≡wk′ v)
(wk≡wk′ w)
wk≡wk′ (qrec C t u v w) =
cong₅ qrec (wk≡wk′ C) (wk≡wk′ t) (wk≡wk′ u) (wk≡wk′ v) (wk≡wk′ w)
opaque mutual
wkVar-to-wk′ :
(∀ x → wkVar ρ x ≡ wkVar ρ′ x) →
(t : Term[ k ]′ n) → wk′ ρ t ≡ wk′ ρ′ t
wkVar-to-wk′ eq (var x) = cong var (eq x)
wkVar-to-wk′ eq (con k ts) = cong (con k) (wkVar-to-wkArgs eq ts)
wkVar-to-wkArgs :
(∀ x → wkVar ρ x ≡ wkVar ρ′ x) →
(ts : Args n as) → wkArgs ρ ts ≡ wkArgs ρ′ ts
wkVar-to-wkArgs eq [] = refl
wkVar-to-wkArgs eq (_∷ₜ_ {m} t ts) =
cong₂ _∷ₜ_ (wkVar-to-wk′ (wkVar-lifts eq m) t)
(wkVar-to-wkArgs eq ts)
opaque
wkVar-to-wk :
(∀ x → wkVar ρ x ≡ wkVar ρ′ x) →
(t : Term[ k ] n) → wk ρ t ≡ wk ρ′ t
wkVar-to-wk {ρ} {ρ′} eq t = begin
wk ρ t ≡⟨ wk≡wk′ t ⟩
toTerm (wk′ ρ (fromTerm t)) ≡⟨ cong toTerm (wkVar-to-wk′ eq _) ⟩
toTerm (wk′ ρ′ (fromTerm t)) ≡˘⟨ wk≡wk′ t ⟩
wk ρ′ t ∎
opaque mutual
wk′-id : (t : Term[ k ]′ n) → wk′ id t ≡ t
wk′-id (var x) = refl
wk′-id (con k ts) = cong (con k) (wkArgs-id ts)
wkArgs-id : (ts : Args n as) → wkArgs id ts ≡ ts
wkArgs-id [] = refl
wkArgs-id (_∷ₜ_ {m} t ts) =
cong₂ _∷ₜ_ (trans (wkVar-to-wk′ (wkVar-lifts-id m) t) (wk′-id t))
(wkArgs-id ts)
opaque
wk-id : (t : Term[ k ] n) → wk id t ≡ t
wk-id t = begin
wk id t ≡⟨ wk≡wk′ t ⟩
toTerm (wk′ id (fromTerm t)) ≡⟨ cong toTerm (wk′-id _) ⟩
toTerm (fromTerm t) ≡⟨ toTerm∘fromTerm _ ⟩
t ∎
opaque
wk-liftn-id : ∀ m (t : Term[ k ] (m + n)) → wk (liftn id m) t ≡ t
wk-liftn-id m t =
wk (liftn id m) t ≡⟨ wkVar-to-wk (wkVar-lifts-id _) t ⟩
wk id t ≡⟨ wk-id _ ⟩
t ∎
wk-lift-id : (t : Term[ k ] (1+ n)) → wk (lift id) t ≡ t
wk-lift-id = wk-liftn-id _
opaque mutual
wk′-comp :
(ρ : Wk m ℓ) (ρ′ : Wk ℓ n) (t : Term[ k ]′ n) →
wk′ ρ (wk′ ρ′ t) ≡ wk′ (ρ • ρ′) t
wk′-comp ρ ρ′ (var x) = cong var (wkVar-comp ρ ρ′ x)
wk′-comp _ _ (con k ts) = cong (con k) (wkArgs-comp ts)
wkArgs-comp :
(ts : Args n as) →
wkArgs ρ (wkArgs ρ′ ts) ≡ wkArgs (ρ • ρ′) ts
wkArgs-comp [] = refl
wkArgs-comp (_∷ₜ_ {m} t ts) =
cong₂ _∷ₜ_
(trans (wk′-comp _ _ t) (wkVar-to-wk′ (wkVar-comps m _ _) t))
(wkArgs-comp ts)
opaque
wk-comp :
(ρ : Wk m ℓ) (ρ′ : Wk ℓ n) (t : Term[ k ] n) →
wk ρ (wk ρ′ t) ≡ wk (ρ • ρ′) t
wk-comp ρ ρ′ t = begin
wk ρ (wk ρ′ t) ≡⟨ cong (wk ρ) (wk≡wk′ t) ⟩
wk ρ (toTerm (wk′ ρ′ (fromTerm t))) ≡⟨ wk≡wk′ _ ⟩
toTerm (wk′ ρ (fromTerm (toTerm (wk′ ρ′ (fromTerm t))))) ≡⟨ cong (λ x → toTerm (wk′ ρ x)) (fromTerm∘toTerm _) ⟩
toTerm (wk′ ρ (wk′ ρ′ (fromTerm t))) ≡⟨ cong toTerm (wk′-comp ρ ρ′ _) ⟩
toTerm (wk′ (ρ • ρ′) (fromTerm t)) ≡˘⟨ wk≡wk′ t ⟩
wk (ρ • ρ′) t ∎
opaque
•-idʳ : (ρ : Wk m n) → ρ • id ≡ ρ
•-idʳ id = refl
•-idʳ (step ρ) = cong step (•-idʳ ρ)
•-idʳ (lift ρ) = refl
opaque
wk₀-comp : (ρ : Wk m n) (t : Term[ k ] 0) → wk ρ (wk wk₀ t) ≡ wk wk₀ t
wk₀-comp ρ t = begin
wk ρ (wk wk₀ t) ≡⟨ wk-comp ρ wk₀ t ⟩
wk (ρ • wk₀) t ≡⟨ cong (λ w → wk w t) (wk₀-invariant ρ) ⟩
wk wk₀ t ∎
wk1-wk : (ρ : Wk m n) (t : Term[ k ] n) → wk1 (wk ρ t) ≡ wk (step ρ) t
wk1-wk ρ t = wk-comp (step id) ρ t
lift-wk1 :
(ρ : Wk m n) (t : Term[ k ] n) → wk (lift ρ) (wk1 t) ≡ wk (step ρ) t
lift-wk1 pr A = trans (wk-comp (lift pr) (step id) A)
(sym (cong (λ x → wk x A) (lift-step-comp pr)))
wk1-wk≡lift-wk1 :
(ρ : Wk m n) (t : Term[ k ] n) → wk1 (wk ρ t) ≡ wk (lift ρ) (wk1 t)
wk1-wk≡lift-wk1 ρ t = trans (wk1-wk ρ t) (sym (lift-wk1 ρ t))
opaque mutual
wk′-injective : {t₁ t₂ : Term[ k ]′ n} → wk′ ρ t₁ ≡ wk′ ρ t₂ → t₁ ≡ t₂
wk′-injective {t₁ = var x₁} {t₂ = var x₂} eq =
cong var (wkVar-injective (var-cong⁻¹ eq))
wk′-injective {t₁ = var _} {t₂ = con _ _} ()
wk′-injective {t₁ = con _ _} {t₂ = var _} ()
wk′-injective {t₁ = con k₁ ts₁} {t₂ = con k₂ ts₂} eq
with con-cong⁻¹ eq
… | refl , refl , eq = cong (con _) (wkArgs-injective eq)
wkArgs-injective : wkArgs ρ ts₁ ≡ wkArgs ρ ts₂ → ts₁ ≡ ts₂
wkArgs-injective {ts₁ = []} {ts₂ = []} _ = refl
wkArgs-injective {ts₁ = _ ∷ₜ _} {ts₂ = _ ∷ₜ _} eq with ∷-cong⁻¹ eq
… | eq₁ , eq₂ = cong₂ _∷ₜ_ (wk′-injective eq₁) (wkArgs-injective eq₂)
opaque
wk-injective : wk ρ t₁ ≡ wk ρ t₂ → t₁ ≡ t₂
wk-injective {ρ} {t₁} {t₂} =
wk ρ t₁ ≡ wk ρ t₂ →⟨ (λ eq → trans (sym (wk≡wk′ _)) (trans eq (wk≡wk′ _))) ⟩
toTerm (wk′ ρ (fromTerm t₁)) ≡ toTerm (wk′ ρ (fromTerm t₂)) →⟨ toTerm-injective ⟩
wk′ ρ (fromTerm t₁) ≡ wk′ ρ (fromTerm t₂) →⟨ wk′-injective ⟩
fromTerm t₁ ≡ fromTerm t₂ →⟨ fromTerm-injective ⟩
t₁ ≡ t₂ □
opaque
subst≡subst′ :
(t : Term[ k ] n) → t [ σ ] ≡ toTerm (fromTerm t [ σ ]′)
subst≡subst′ (var x) = sym (toTerm∘fromTerm _)
subst≡subst′ (defn α) = refl
subst≡subst′ Level = refl
subst≡subst′ zeroᵘ = refl
subst≡subst′ (sucᵘ t) = cong sucᵘ (subst≡subst′ t)
subst≡subst′ (t₁ supᵘ t₂) =
cong₂ _supᵘ_ (subst≡subst′ t₁) (subst≡subst′ t₂)
subst≡subst′ (ωᵘ+ _) =
refl
subst≡subst′ (level t) =
cong level (subst≡subst′ t)
subst≡subst′ (U l) = cong U (subst≡subst′ l)
subst≡subst′ (Lift l A) = cong₂ Lift (subst≡subst′ l) (subst≡subst′ A)
subst≡subst′ (lift a) = cong lift (subst≡subst′ a)
subst≡subst′ (lower a) = cong lower (subst≡subst′ a)
subst≡subst′ (ΠΣ⟨ b ⟩ p , q ▷ t ▹ t₁) =
cong₂ (ΠΣ⟨ b ⟩ p , q ▷_▹_) (subst≡subst′ t) (subst≡subst′ t₁)
subst≡subst′ (lam p t) = cong (lam p) (subst≡subst′ t)
subst≡subst′ (t ∘⟨ p ⟩ t₁) =
cong₂ _∘_ (subst≡subst′ t) (subst≡subst′ t₁)
subst≡subst′ (prod x p t t₁) =
cong₂ prod! (subst≡subst′ t) (subst≡subst′ t₁)
subst≡subst′ (fst p t) = cong (fst p) (subst≡subst′ t)
subst≡subst′ (snd p t) = cong (snd p) (subst≡subst′ t)
subst≡subst′ (prodrec r p q t t₁ t₂) =
cong₃ (prodrec r p q) (subst≡subst′ t)
(subst≡subst′ t₁) (subst≡subst′ t₂)
subst≡subst′ ℕ = refl
subst≡subst′ zero = refl
subst≡subst′ (suc t) = cong suc (subst≡subst′ t)
subst≡subst′ (natrec p q r t t₁ t₂ t₃) =
cong₄ (natrec p q r) (subst≡subst′ t)
(subst≡subst′ t₁) (subst≡subst′ t₂) (subst≡subst′ t₃)
subst≡subst′ (Unit x) = refl
subst≡subst′ (star x) = refl
subst≡subst′ (unitrec p q t t₁ t₂) =
cong₃ (unitrec p q) (subst≡subst′ t)
(subst≡subst′ t₁) (subst≡subst′ t₂)
subst≡subst′ Empty = refl
subst≡subst′ (emptyrec p t t₁) =
cong₂ (emptyrec p) (subst≡subst′ t) (subst≡subst′ t₁)
subst≡subst′ (Id t t₁ t₂) =
cong₃ Id (subst≡subst′ t) (subst≡subst′ t₁) (subst≡subst′ t₂)
subst≡subst′ rfl = refl
subst≡subst′ (J p q t t₁ t₂ t₃ t₄ t₅) =
cong₆ (J p q) (subst≡subst′ t) (subst≡subst′ t₁) (subst≡subst′ t₂)
(subst≡subst′ t₃) (subst≡subst′ t₄) (subst≡subst′ t₅)
subst≡subst′ (K p t t₁ t₂ t₃ t₄) =
cong₅ (K p) (subst≡subst′ t) (subst≡subst′ t₁) (subst≡subst′ t₂)
(subst≡subst′ t₃) (subst≡subst′ t₄)
subst≡subst′ ([]-cong _ l A t u v) =
cong₅ []-cong! (subst≡subst′ l) (subst≡subst′ A) (subst≡subst′ t)
(subst≡subst′ u) (subst≡subst′ v)
subst≡subst′ (Quot A B) =
cong₂ Quot (subst≡subst′ A) (subst≡subst′ B)
subst≡subst′ (class t) =
cong class (subst≡subst′ t)
subst≡subst′ (resp A B t u v) =
cong₅ resp (subst≡subst′ A) (subst≡subst′ B) (subst≡subst′ t)
(subst≡subst′ u) (subst≡subst′ v)
subst≡subst′ (set A B t u v w) =
cong₆ set (subst≡subst′ A) (subst≡subst′ B) (subst≡subst′ t)
(subst≡subst′ u) (subst≡subst′ v) (subst≡subst′ w)
subst≡subst′ (qrec C t u v w) =
cong₅ qrec (subst≡subst′ C) (subst≡subst′ t) (subst≡subst′ u)
(subst≡subst′ v) (subst≡subst′ w)
substVar-lift : (∀ x → σ x ≡ σ′ x) → ∀ x → liftSubst σ x ≡ liftSubst σ′ x
substVar-lift eq x0 = refl
substVar-lift eq (x +1) = cong wk1 (eq x)
substVar-lifts : (∀ x → σ x ≡ σ′ x) → ∀ n x → liftSubstn σ n x ≡ liftSubstn σ′ n x
substVar-lifts eq 0 x = eq x
substVar-lifts eq (1+ n) x0 = refl
substVar-lifts eq (1+ n) (x +1) = cong wk1 (substVar-lifts eq n x)
opaque
consSubst-cong :
t₁ ≡ t₂ →
(∀ x → σ₁ x ≡ σ₂ x) →
∀ x → consSubst σ₁ t₁ x ≡ consSubst σ₂ t₂ x
consSubst-cong refl _ x0 = refl
consSubst-cong _ eq (x +1) = eq x
opaque
consSubst-η : ∀ x → consSubst (tail σ) (head σ) x ≡ σ x
consSubst-η x0 = refl
consSubst-η (_ +1) = refl
wk1Subst-cong :
(∀ x → σ x ≡ σ′ x) →
∀ x → wk1Subst σ x ≡ wk1Subst σ′ x
wk1Subst-cong eq x = cong wk1 (eq x)
opaque
wkSubst-cong :
(∀ x → σ₁ x ≡ σ₂ x) →
∀ x → wkSubst n σ₁ x ≡ wkSubst n σ₂ x
wkSubst-cong {n = 0} σ₁≡σ₂ = σ₁≡σ₂
wkSubst-cong {n = 1+ _} σ₁≡σ₂ = wk1Subst-cong (wkSubst-cong σ₁≡σ₂)
opaque mutual
substVar-to-subst′ :
((x : Fin n) → σ x ≡ σ′ x) →
(t : Term[ k ]′ n) → t [ σ ]′ ≡ t [ σ′ ]′
substVar-to-subst′ eq (var x) = cong fromTerm (eq x)
substVar-to-subst′ eq (con k ts) =
cong (con k) (substVar-to-substArgs eq ts)
substVar-to-substArgs :
((x : Fin n) → σ₁ x ≡ σ₂ x) →
(ts : Args n as) → substArgs ts σ₁ ≡ substArgs ts σ₂
substVar-to-substArgs eq [] = refl
substVar-to-substArgs eq (_∷ₜ_ {m} t ts) =
cong₂ _∷ₜ_ (substVar-to-subst′ (substVar-lifts eq m) t)
(substVar-to-substArgs eq ts)
opaque
substVar-to-subst :
((x : Fin n) → σ₁ x ≡ σ₂ x) →
(t : Term[ k ] n) → t [ σ₁ ] ≡ t [ σ₂ ]
substVar-to-subst {σ₁} {σ₂} eq t =
t [ σ₁ ] ≡⟨ subst≡subst′ t ⟩
toTerm (fromTerm t [ σ₁ ]′) ≡⟨ cong toTerm (substVar-to-subst′ eq (fromTerm t)) ⟩
toTerm (fromTerm t [ σ₂ ]′) ≡˘⟨ subst≡subst′ t ⟩
t [ σ₂ ] ∎
subst-lift-id : (x : Fin (1+ n)) → (liftSubst idSubst) x ≡ idSubst x
subst-lift-id x0 = refl
subst-lift-id (x +1) = refl
subst-lifts-id : (n : Nat) → (x : Fin (n + m)) → (liftSubstn idSubst n) x ≡ idSubst x
subst-lifts-id 0 x = refl
subst-lifts-id (1+ n) x0 = refl
subst-lifts-id (1+ n) (x +1) = cong wk1 (subst-lifts-id n x)
opaque mutual
subst′-id : (t : Term[ k ]′ n) → t [ idSubst ]′ ≡ t
subst′-id (var x) = refl
subst′-id (con k ts) = cong (con k) (substArgs-id ts)
substArgs-id : (ts : Args n as) → substArgs ts idSubst ≡ ts
substArgs-id [] = refl
substArgs-id (_∷ₜ_ {m} t ts) =
cong₂ _∷ₜ_
(trans (substVar-to-subst′ (subst-lifts-id m) t) (subst′-id _))
(substArgs-id ts)
opaque
subst-id : (t : Term[ k ] n) → t [ idSubst ] ≡ t
subst-id t = begin
t [ idSubst ] ≡⟨ subst≡subst′ t ⟩
toTerm (fromTerm t [ idSubst ]′) ≡⟨ cong toTerm (subst′-id (fromTerm t)) ⟩
toTerm (fromTerm t) ≡⟨ toTerm∘fromTerm t ⟩
t ∎
opaque
idSubst-ₛ•ₛˡ : (x : Fin n) → (idSubst ₛ•ₛ σ) x ≡ σ x
idSubst-ₛ•ₛˡ _ = subst-id _
opaque
idSubst-ₛ•ₛʳ : (x : Fin n) → (σ ₛ•ₛ idSubst) x ≡ σ x
idSubst-ₛ•ₛʳ _ = refl
opaque
[idSubst⇑ⁿ]≡ :
∀ m {t : Term[ k ] (m + n)} → t [ liftSubstn idSubst m ] ≡ t
[idSubst⇑ⁿ]≡ m {t} =
t [ liftSubstn idSubst m ] ≡⟨ substVar-to-subst (subst-lifts-id m) t ⟩
t [ idSubst ] ≡⟨ subst-id _ ⟩
t ∎
subst-lift-•ₛ : (t : Term[ k ] (1+ n))
→ t [ lift ρ •ₛ liftSubst σ ]
≡ t [ liftSubst (ρ •ₛ σ) ]
subst-lift-•ₛ =
substVar-to-subst (λ { x0 → refl ; (x +1) → sym (wk1-wk≡lift-wk1 _ _)})
helper1 : (n : Nat) (x : Fin (1+ n + m)) →
(lift (liftn ρ n) •ₛ liftSubst (liftSubstn σ n)) x ≡
liftSubst (liftSubstn (ρ •ₛ σ) n) x
helper1 0 x0 = refl
helper1 0 (x +1) = sym (wk1-wk≡lift-wk1 _ _)
helper1 (1+ n) x0 = refl
helper1 (1+ n) (x +1) = trans (sym (wk1-wk≡lift-wk1 _ _)) (cong wk1 (helper1 n x))
subst-lifts-•ₛ :
∀ m (t : Term[ k ] (m + n)) →
t [ liftn ρ m •ₛ (σ ⇑[ m ]) ] ≡ t [ (ρ •ₛ σ) ⇑[ m ] ]
subst-lifts-•ₛ 0 t = refl
subst-lifts-•ₛ (1+ n) t = substVar-to-subst (helper1 n) t
subst′-lifts-•ₛ :
∀ m (t : Term[ k ]′ (m + n)) →
t [ liftn ρ m •ₛ (σ ⇑[ m ]) ]′ ≡ t [ (ρ •ₛ σ) ⇑[ m ] ]′
subst′-lifts-•ₛ 0 t = refl
subst′-lifts-•ₛ (1+ n) t = substVar-to-subst′ (helper1 n) t
subst-lift-ₛ• : (t : Term[ k ] (1+ n))
→ t [ liftSubst σ ₛ• lift ρ ]
≡ t [ liftSubst (σ ₛ• ρ) ]
subst-lift-ₛ• = substVar-to-subst (λ { x0 → refl ; (x +1) → refl})
helper2 : (n : Nat) → (x : Fin (1+ n + m))
→ liftSubst (liftSubstn σ n) (wkVar (lift (liftn ρ n)) x) ≡
liftSubst (liftSubstn (λ x₁ → σ (wkVar ρ x₁)) n) x
helper2 0 x0 = refl
helper2 0 (x +1) = refl
helper2 (1+ n) x0 = refl
helper2 (1+ n) (x +1) = cong wk1 (helper2 n x)
subst-lifts-ₛ• :
∀ m (t : Term[ k ] (m + n)) →
t [ (σ ⇑[ m ]) ₛ• liftn ρ m ] ≡ t [ (σ ₛ• ρ) ⇑[ m ] ]
subst-lifts-ₛ• 0 t = refl
subst-lifts-ₛ• (1+ n) t = substVar-to-subst (helper2 n) t
opaque
subst′-lifts-ₛ• :
∀ m (t : Term[ k ]′ (m + n)) →
t [ (σ ⇑[ m ]) ₛ• liftn ρ m ]′ ≡ t [ (σ ₛ• ρ) ⇑[ m ] ]′
subst′-lifts-ₛ• 0 t = refl
subst′-lifts-ₛ• (1+ n) t = substVar-to-subst′ (helper2 n) t
opaque mutual
wk′-subst′ : (t : Term[ k ]′ n) → wk′ ρ (t [ σ ]′) ≡ t [ ρ •ₛ σ ]′
wk′-subst′ {ρ} {σ} (var x) = begin
wk′ ρ (var x [ σ ]′) ≡⟨⟩
wk′ ρ (fromTerm (σ x)) ≡˘⟨ fromTerm∘toTerm _ ⟩
fromTerm (toTerm (wk′ ρ (fromTerm (σ x)))) ≡˘⟨ cong fromTerm (wk≡wk′ (σ x)) ⟩
fromTerm (wk ρ (σ x)) ≡⟨⟩
(var x [ ρ •ₛ σ ]′) ∎
wk′-subst′ (con k ts) = cong (con k) (wkArgs-substArgs ts)
wkArgs-substArgs :
(ts : Args n as) → wkArgs ρ (substArgs ts σ) ≡ substArgs ts (ρ •ₛ σ)
wkArgs-substArgs [] = refl
wkArgs-substArgs (_∷ₜ_ {m} t ts) =
cong₂ _∷ₜ_
(trans (wk′-subst′ t)
(substVar-to-subst′ (subst-lifts-•ₛ m ∘→ var) t))
(wkArgs-substArgs ts)
opaque
wk-subst : (t : Term[ k ] n) → wk ρ (t [ σ ]) ≡ t [ ρ •ₛ σ ]
wk-subst {ρ} {σ} t = begin
wk ρ (t [ σ ]) ≡⟨ cong (wk ρ) (subst≡subst′ t) ⟩
wk ρ (toTerm (fromTerm t [ σ ]′)) ≡⟨ wk≡wk′ _ ⟩
toTerm (wk′ ρ (fromTerm (toTerm (fromTerm t [ σ ]′)))) ≡⟨ cong (λ x → toTerm (wk′ ρ x)) (fromTerm∘toTerm _ ) ⟩
toTerm (wk′ ρ (fromTerm t [ σ ]′)) ≡⟨ cong toTerm (wk′-subst′ (fromTerm t)) ⟩
toTerm (fromTerm t [ ρ •ₛ σ ]′) ≡˘⟨ subst≡subst′ t ⟩
t [ ρ •ₛ σ ] ∎
mutual
subst′-wk′ : (t : Term[ k ]′ n) → wk′ ρ t [ σ ]′ ≡ t [ σ ₛ• ρ ]′
subst′-wk′ (var x) = refl
subst′-wk′ (con k ts) = cong (con k) (substArgs-wkArgs ts)
substArgs-wkArgs :
(ts : Args n as) → substArgs (wkArgs ρ ts) σ ≡ substArgs ts (σ ₛ• ρ)
substArgs-wkArgs [] = refl
substArgs-wkArgs (_∷ₜ_ {m} t ts) =
cong₂ _∷ₜ_
(trans (subst′-wk′ t)
(substVar-to-subst′ (subst-lifts-ₛ• m ∘→ var) t))
(substArgs-wkArgs ts)
opaque
subst-wk : (t : Term[ k ] n) → wk ρ t [ σ ] ≡ t [ σ ₛ• ρ ]
subst-wk {ρ} {σ} t = begin
wk ρ t [ σ ] ≡⟨ cong (_[ σ ]) (wk≡wk′ t) ⟩
toTerm (wk′ ρ (fromTerm t)) [ σ ] ≡⟨ subst≡subst′ (toTerm (wk′ ρ (fromTerm t))) ⟩
toTerm (fromTerm (toTerm (wk′ ρ (fromTerm t))) [ σ ]′) ≡⟨ cong (λ x → toTerm (x [ σ ]′)) (fromTerm∘toTerm (wk′ ρ (fromTerm t))) ⟩
toTerm (wk′ ρ (fromTerm t) [ σ ]′) ≡⟨ cong toTerm (subst′-wk′ (fromTerm t)) ⟩
toTerm (fromTerm t [ σ ₛ• ρ ]′) ≡˘⟨ subst≡subst′ t ⟩
t [ σ ₛ• ρ ] ∎
opaque
wk1Subst-wk1 : (t : Term[ k ] n) → t [ wk1Subst σ ] ≡ wk1 (t [ σ ])
wk1Subst-wk1 {σ} t =
t [ wk1Subst σ ] ≡⟨⟩
t [ step id •ₛ σ ] ≡˘⟨ wk-subst t ⟩
wk1 (t [ σ ]) ∎
opaque
wk1-liftSubst :
(t : Term[ k ] n) → wk1 t [ liftSubst σ ] ≡ wk1 (t [ σ ])
wk1-liftSubst {σ} t =
wk1 t [ liftSubst σ ] ≡⟨ subst-wk t ⟩
t [ liftSubst σ ₛ• step id ] ≡⟨⟩
t [ wk1Subst σ ] ≡⟨ wk1Subst-wk1 t ⟩
wk1 (t [ σ ]) ∎
opaque
wk2-liftSubst :
(t : Term[ k ] n) → wk2 t [ σ ⇑[ 2 ] ] ≡ wk2 (t [ σ ])
wk2-liftSubst {σ} t =
wk2 t [ σ ⇑[ 2 ] ] ≡⟨ wk1-liftSubst (wk1 t) ⟩
wk1 (wk1 t [ σ ⇑ ]) ≡⟨ cong wk1 (wk1-liftSubst t) ⟩
wk2 (t [ σ ]) ∎
wk-subst-lift : (G : Term[ k ] (1+ n))
→ wk (lift ρ) (G [ liftSubst σ ])
≡ G [ liftSubst (ρ •ₛ σ) ]
wk-subst-lift G = trans (wk-subst G) (subst-lift-•ₛ G)
wk≡subst : (ρ : Wk m n) (t : Term[ k ] n) → wk ρ t ≡ t [ toSubst ρ ]
wk≡subst ρ t = trans (cong (wk ρ) (sym (subst-id t))) (wk-subst t)
opaque
toSubst-liftn : ∀ k x → toSubst (liftn ρ k) x ≡ (toSubst ρ ⇑[ k ]) x
toSubst-liftn 0 _ = refl
toSubst-liftn (1+ _) x0 = refl
toSubst-liftn (1+ k) (x +1) =
cong wk1 $ toSubst-liftn k x
opaque
wk-liftn :
∀ m {t : Term[ k ] (m + n)} →
wk (liftn ρ m) t ≡ t [ toSubst ρ ⇑[ m ] ]
wk-liftn {ρ} m {t} =
wk (liftn ρ m) t ≡⟨ wk≡subst _ _ ⟩
t [ toSubst (liftn ρ m) ] ≡⟨ substVar-to-subst (toSubst-liftn m) t ⟩
t [ toSubst ρ ⇑[ m ] ] ∎
substCompLift : ∀ x
→ (liftSubst σ ₛ•ₛ liftSubst σ′) x
≡ (liftSubst (σ ₛ•ₛ σ′)) x
substCompLift x0 = refl
substCompLift {σ = σ} {σ′ = σ′} (x +1) = trans (subst-wk (σ′ x)) (sym (wk-subst (σ′ x)))
substCompLifts : ∀ n x
→ (liftSubstn σ n ₛ•ₛ liftSubstn σ′ n) x
≡ (liftSubstn (σ ₛ•ₛ σ′) n) x
substCompLifts 0 x = refl
substCompLifts (1+ n) x0 = refl
substCompLifts {σ = σ} {σ′ = σ′} (1+ n) (x +1) =
trans (substCompLift {σ = liftSubstn σ n} {σ′ = liftSubstn σ′ n} (x +1))
(cong wk1 (substCompLifts n x))
opaque mutual
subst′CompEq :
(t : Term[ k ]′ n) → t [ σ′ ]′ [ σ ]′ ≡ t [ σ ₛ•ₛ σ′ ]′
subst′CompEq {σ′} {σ} (var x) = begin
fromTerm (σ′ x) [ σ ]′ ≡˘⟨ fromTerm∘toTerm _ ⟩
fromTerm (toTerm (fromTerm (σ′ x) [ σ ]′)) ≡˘⟨ cong fromTerm (subst≡subst′ (σ′ x)) ⟩
fromTerm (σ′ x [ σ ]) ∎
subst′CompEq (con k ts) = cong (con k) (substArgsCompEq ts)
substArgsCompEq :
(ts : Args n as) →
substArgs (substArgs ts σ₂) σ₁ ≡ substArgs ts (σ₁ ₛ•ₛ σ₂)
substArgsCompEq [] = refl
substArgsCompEq (_∷ₜ_ {m} t ts) =
cong₂ _∷ₜ_
(trans (subst′CompEq t) (substVar-to-subst′ (substCompLifts m) t))
(substArgsCompEq ts)
opaque
substCompEq : (t : Term[ k ] n) → t [ σ′ ] [ σ ] ≡ t [ σ ₛ•ₛ σ′ ]
substCompEq {σ′} {σ} t = begin
t [ σ′ ] [ σ ] ≡⟨ subst≡subst′ (t [ σ′ ]) ⟩
toTerm (fromTerm (t [ σ′ ]) [ σ ]′) ≡⟨ cong (λ x → toTerm (fromTerm x [ σ ]′)) (subst≡subst′ t) ⟩
toTerm (fromTerm (toTerm (fromTerm t [ σ′ ]′)) [ σ ]′) ≡⟨ cong (λ x → toTerm (x [ σ ]′)) (fromTerm∘toTerm (fromTerm t [ σ′ ]′)) ⟩
toTerm ((fromTerm t [ σ′ ]′) [ σ ]′) ≡⟨ cong toTerm (subst′CompEq (fromTerm t)) ⟩
toTerm (fromTerm t [ σ ₛ•ₛ σ′ ]′) ≡˘⟨ subst≡subst′ t ⟩
t [ σ ₛ•ₛ σ′ ] ∎
wk-comp-subst :
(ρ : Wk m ℓ) (ρ′ : Wk ℓ n) (t : Term[ k ] (1+ n)) →
wk (lift (ρ • ρ′)) t [ u ]₀ ≡ wk (lift ρ) (wk (lift ρ′) t) [ u ]₀
wk-comp-subst _ _ t =
cong _[ _ ]₀ (sym (wk-comp _ _ t))
wk-β :
(t : Term[ k ] (1+ n)) → wk ρ (t [ u ]₀) ≡ wk (lift ρ) t [ wk ρ u ]₀
wk-β t = trans (wk-subst t) (sym (trans (subst-wk t)
(substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) t)))
wk-β↑ :
(t : Term[ k ] (1+ n)) →
wk (lift ρ) (t [ u ]↑) ≡ wk (lift ρ) t [ wk (lift ρ) u ]↑
wk-β↑ t = trans (wk-subst t) (sym (trans (subst-wk t)
(substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) t)))
wk-β↑² :
(t : Term[ k ] (1+ n)) →
wk (liftn ρ 2) (t [ u ]↑²) ≡ wk (lift ρ) t [ wk (liftn ρ 2) u ]↑²
wk-β↑² t = trans (wk-subst t) (sym (trans (subst-wk t)
(substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) t)))
substVarSingletonComp : ∀ {u} (x : Fin (1+ n))
→ (sgSubst u ₛ•ₛ liftSubst σ) x ≡ (consSubst σ u) x
substVarSingletonComp x0 = refl
substVarSingletonComp {σ = σ} (x +1) = trans (subst-wk (σ x)) (subst-id (σ x))
substSingletonComp :
(t : Term[ k ] (1+ n)) →
t [ sgSubst u ₛ•ₛ (σ ⇑) ] ≡ t [ consSubst σ u ]
substSingletonComp = substVar-to-subst substVarSingletonComp
singleSubstComp :
∀ u (σ : Subst m n) (t : Term[ k ] (1+ n)) →
t [ σ ⇑ ] [ u ]₀ ≡ t [ consSubst σ u ]
singleSubstComp _ _ t =
trans (substCompEq t) (substSingletonComp t)
singleSubstWkComp :
∀ u (σ : Subst m n) (t : Term[ k ] (1+ n)) →
wk (lift ρ) (t [ σ ⇑ ]) [ u ]₀ ≡ t [ consSubst (ρ •ₛ σ) u ]
singleSubstWkComp _ _ t =
trans (cong _[ _ ] (trans (wk-subst t) (subst-lift-•ₛ t)))
(trans (substCompEq t) (substSingletonComp t))
singleSubstLift :
∀ (t : Term[ k ] (1+ n)) u → t [ u ]₀ [ σ ] ≡ t [ σ ⇑ ] [ u [ σ ] ]₀
singleSubstLift t _ =
trans (substCompEq t) $
trans (substVar-to-subst (λ { x0 → refl; (_ +1) → refl}) t) $
sym $
trans (substCompEq t) $
substSingletonComp t
idWkLiftSubstLemma :
(σ : Subst m n) (t : Term[ k ] (1+ n)) →
wk (lift (step id)) (t [ σ ⇑ ]) [ var x0 ]₀ ≡ t [ σ ⇑ ]
idWkLiftSubstLemma _ t =
trans (singleSubstWkComp _ _ t)
(substVar-to-subst (λ { x0 → refl; (_ +1) → refl}) t)
substVarComp↑ : ∀ {t} (σ : Subst m n) x
→ (consSubst (wk1Subst idSubst) (t [ liftSubst σ ]) ₛ•ₛ liftSubst σ) x
≡ (liftSubst σ ₛ•ₛ consSubst (wk1Subst idSubst) t) x
substVarComp↑ σ x0 = refl
substVarComp↑ σ (x +1) = trans (subst-wk (σ x)) (sym (wk≡subst (step id) (σ x)))
singleSubstLift↑ :
∀ (σ : Subst m n) (t : Term[ k ] (1+ n)) u →
t [ u ]↑ [ σ ⇑ ] ≡ t [ σ ⇑ ] [ u [ σ ⇑ ] ]↑
singleSubstLift↑ _ t _ =
trans (substCompEq t) $
sym $
trans (substCompEq t) $
substVar-to-subst (substVarComp↑ _) t
substConsComp :
t [ consSubst (λ x → σ (x +1)) (u [ tail σ ]) ] ≡
t [ consSubst (λ x → var (x +1)) (wk1 u) ] [ σ ]
substConsComp {t} {u} =
trans
(substVar-to-subst (λ { x0 → sym (subst-wk u); (_ +1) → refl }) t) $
sym (substCompEq t)
wkSingleSubstId :
(t : Term[ k ] (1+ n)) → (wk (lift (step id)) t) [ var x0 ]₀ ≡ t
wkSingleSubstId t =
trans (subst-wk t) $
trans (substVar-to-subst (λ { x0 → refl; (_ +1) → refl }) t) $
subst-id _
wkSingleSubstWk1 :
(t : Term[ k ] (1+ n)) →
wk (lift (step (step id))) t [ var (x0 +1) ]₀ ≡ wk1 t
wkSingleSubstWk1 t =
trans (subst-wk t) $
trans (substVar-to-subst (λ { x0 → refl; (_ +1) → refl }) t) $
sym (wk≡subst _ _)
cons-wk-subst :
∀ (ρ : Wk m n) (σ : Subst n ℓ) u (t : Term[ k ] (1+ ℓ)) →
t [ sgSubst u ₛ• lift ρ ₛ•ₛ (σ ⇑) ] ≡ t [ consSubst (ρ •ₛ σ) u ]
cons-wk-subst _ σ _ =
substVar-to-subst
(λ { x0 → refl
; (x +1) → trans (subst-wk (σ x)) (sym (wk≡subst _ _))
})
wk-β-natrec :
(ρ : Wk m n) (t : Term[ k ] (1+ n)) →
wk (liftn ρ 2) (t [ suc (var x1) ]↑²) ≡
wk (lift ρ) t [ suc (var x1) ]↑²
wk-β-natrec _ = wk-β↑²
wk-β-prodrec :
(ρ : Wk m n) (t : Term[ k ] (1+ n)) →
wk (liftn ρ 2) (t [ prod s p (var x1) (var x0) ]↑²) ≡
wk (lift ρ) t [ prod s p (var x1) (var x0) ]↑²
wk-β-prodrec _ = wk-β↑²
wk-β-doubleSubst :
(ρ : Wk m n) (t : Term[ k ] (2+ n)) (u v : Term n) →
wk ρ (t [ u , v ]₁₀) ≡ wk (liftn ρ 2) t [ wk ρ u , wk ρ v ]₁₀
wk-β-doubleSubst ρ t u v =
wk ρ (t [ σₜ u v ]) ≡⟨ wk-subst t ⟩
t [ ρ •ₛ σₜ u v ] ≡⟨ substVar-to-subst eq′ t ⟩
t [ σₜ (wk ρ u) (wk ρ v) ₛ• liftn ρ 2 ] ≡⟨ sym (subst-wk t) ⟩
wk (liftn ρ 2) t [ wk ρ u , wk ρ v ]₁₀ ∎
where
σₜ : (u v : Term ℓ) → Subst ℓ (2+ ℓ)
σₜ u v = consSubst (consSubst idSubst u) v
eq′ :
∀ x →
substVar (ρ •ₛ σₜ u v) x ≡
substVar (σₜ (wk ρ u) (wk ρ v)) (wkVar (liftn ρ 2) x)
eq′ x0 = refl
eq′ (x0 +1) = refl
eq′ (_ +2) = refl
natrecSucCaseLemma : (x : Fin (1+ n))
→ (liftSubstn σ 2 ₛ•ₛ consSubst (wkSubst 2 idSubst) (suc (var x1))) x
≡ (consSubst (wkSubst 2 idSubst) (suc (var x1)) ₛ•ₛ liftSubst σ) x
natrecSucCaseLemma x0 = refl
natrecSucCaseLemma {σ = σ} (_+1 x) = begin
wk1 (wk1 (σ x))
≡⟨ wk-comp (step id) (step id) (σ x) ⟩
wk (step id • step id) (σ x)
≡⟨ wk≡subst (step id • step id) (σ x) ⟩
σ x [ wkSubst 2 idSubst ]
≡⟨⟩
σ x [ consSubst (wkSubst 2 idSubst) (suc (var x1)) ₛ• step id ]
≡˘⟨ subst-wk (σ x) ⟩
wk1 (σ x) [ consSubst (wkSubst 2 idSubst) (suc (var x1)) ] ∎
natrecSucCase :
(σ : Subst m n) (t : Term[ k ] (1+ n)) →
t [ suc (var x1) ]↑² [ σ ⇑[ 2 ] ] ≡
t [ σ ⇑ ] [ suc (var x1) ]↑²
natrecSucCase σ t = begin
t [ suc (var x1) ]↑² [ σ ⇑[ 2 ] ] ≡⟨ substCompEq t ⟩
t [ (σ ⇑[ 2 ]) ₛ•ₛ σₛ ] ≡⟨ substVar-to-subst natrecSucCaseLemma t ⟩
t [ σₛ ₛ•ₛ (σ ⇑) ] ≡˘⟨ substCompEq t ⟩
t [ σ ⇑ ] [ suc (var x1) ]↑² ∎
where
σₛ : Subst (2+ ℓ) (1+ ℓ)
σₛ = consSubst (wkSubst 2 idSubst) (suc (var x1))
natrecIrrelevantSubstLemma : ∀ p q r F z s m (σ : Subst ℓ n) (x : Fin (1+ n))
→ (sgSubst (natrec p q r
(F [ liftSubst σ ])
(z [ σ ])
(s [ liftSubstn σ 2 ])
m
)
ₛ•ₛ liftSubst (sgSubst m)
ₛ•ₛ liftSubst (liftSubst σ)
ₛ• step id
ₛ•ₛ consSubst (tail idSubst) (suc (var x0))) x
≡ (consSubst σ (suc m)) x
natrecIrrelevantSubstLemma p q r F z s m σ x0 =
cong suc (trans (subst-wk m) (subst-id m))
natrecIrrelevantSubstLemma p q r F z s m σ (x +1) =
trans (subst-wk (wk (step id) (σ x)))
(trans (subst-wk (σ x))
(subst-id (σ x)))
natrecIrrelevantSubst : ∀ p q r F z s m (σ : Subst ℓ n)
→ F [ consSubst σ (suc m) ]
≡ wk1 (F [ suc (var x0) ]↑)
[ liftSubstn σ 2 ]
[ liftSubst (sgSubst m) ]
[ natrec p q r (F [ liftSubst σ ]) (z [ σ ]) (s [ liftSubstn σ 2 ]) m ]₀
natrecIrrelevantSubst p q r F z s m σ =
sym (trans (substCompEq (_[ liftSubstn σ 2 ]
(wk (step id)
(F [ consSubst (tail idSubst) (suc (var x0)) ]))))
(trans (substCompEq (wk (step id)
(F [ consSubst (tail idSubst) (suc (var x0)) ])))
(trans
(subst-wk (F [ consSubst (tail idSubst) (suc (var x0)) ]))
(trans (substCompEq F)
(substVar-to-subst (natrecIrrelevantSubstLemma p q r F z s m σ) F)))))
natrecIrrelevantSubstLemma′ : ∀ (p q r : M) F z s n (x : Fin (1+ m))
→ (sgSubst (natrec p q r F z s n)
ₛ•ₛ liftSubst (sgSubst n)
ₛ• step id
ₛ•ₛ consSubst (tail idSubst) (suc (var x0))) x
≡ (consSubst var (suc n)) x
natrecIrrelevantSubstLemma′ p q r F z s n x0 =
cong suc (trans (subst-wk n) (subst-id n))
natrecIrrelevantSubstLemma′ p q r F z s n (x +1) = refl
natrecIrrelevantSubst′ : ∀ p q r (F : Term (1+ m)) z s n
→ wk1 (F [ suc (var x0) ]↑) [ (liftSubst (sgSubst n)) ] [ natrec p q r F z s n ]₀
≡ F [ suc n ]₀
natrecIrrelevantSubst′ p q r F z s n =
trans (substCompEq (wk (step id)
(F [ consSubst (tail idSubst) (suc (var x0)) ])))
(trans (subst-wk (F [ consSubst (tail idSubst) (suc (var x0)) ]))
(trans (substCompEq F)
(substVar-to-subst (natrecIrrelevantSubstLemma′ p q r F z s n) F)))
cons0wkLift1-id :
(σ : Subst m n) (t : Term[ k ] (1+ n)) →
wk (lift (step id)) (t [ σ ⇑ ]) [ var x0 ]₀ ≡ t [ σ ⇑ ]
cons0wkLift1-id σ t =
trans (subst-wk (t [ _ ])) $
trans (substVar-to-subst (λ { x0 → refl; (_ +1) → refl }) (t [ _ ])) $
subst-id _
substConsId :
(t : Term[ k ] (1+ n)) →
t [ consSubst σ (u [ σ ]) ] ≡ t [ u ]₀ [ σ ]
substConsId t =
sym $
trans (substCompEq t) $
substVar-to-subst (λ { x0 → refl; (_ +1) → refl }) t
substConsTailId :
t [ consSubst (tail σ) (u [ σ ]) ] ≡
t [ consSubst (tail idSubst) u ] [ σ ]
substConsTailId {t} =
trans (substVar-to-subst (λ { x0 → refl; (_ +1) → refl }) t) $
sym (substCompEq t)
substConcatSingleton′ :
(t : Term[ k ] (1+ n)) →
t [ σ ₛ•ₛ sgSubst u ] ≡ t [ consSubst σ (u [ σ ]) ]
substConcatSingleton′ t = substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) t
step-consSubst :
(t : Term[ k ] n) →
wk (step ρ) t [ consSubst σ u ] ≡ wk ρ t [ σ ]
step-consSubst {ρ} {σ} {u} t = begin
wk (step ρ) t [ consSubst σ u ] ≡⟨ subst-wk t ⟩
t [ consSubst σ u ₛ• step ρ ] ≡⟨ substVar-to-subst (λ _ → refl) t ⟩
t [ σ ₛ• ρ ] ≡˘⟨ subst-wk t ⟩
wk ρ t [ σ ] ∎
wk1-tail : (t : Term[ k ] n) → wk1 t [ σ ] ≡ t [ tail σ ]
wk1-tail {σ = σ} t = begin
wk1 t [ σ ] ≡⟨⟩
wk (step id) t [ σ ] ≡⟨ subst-wk t ⟩
t [ σ ₛ• step id ] ≡⟨⟩
t [ tail σ ] ∎
wk1-tailId : (t : Term[ k ] n) → wk1 t ≡ t [ tail idSubst ]
wk1-tailId t = trans (sym (subst-id (wk1 t))) (subst-wk t)
wk2-tail : (t : Term[ k ] n) → wk2 t [ σ ] ≡ t [ tail[ 2 ] σ ]
wk2-tail {σ = σ} t = begin
wk2 t [ σ ] ≡⟨ wk1-tail (wk1 t) ⟩
wk1 t [ tail σ ] ≡⟨ wk1-tail t ⟩
t [ tail (tail σ) ] ∎
opaque
tail[]≡ :
∀ k {σ : Subst m (k + n)} →
∀ x → tail[ k ] σ x ≡ (σ ₛ•ₛ wkSubst k idSubst) x
tail[]≡ 0 _ = refl
tail[]≡ (1+ k) {σ} x =
tail[ k ] (tail σ) x ≡⟨ tail[]≡ k _ ⟩
(tail σ ₛ•ₛ wkSubst k idSubst) x ≡⟨⟩
wkSubst k idSubst x [ tail σ ] ≡˘⟨ wk1-tail (wkSubst k _ _) ⟩
wk1 (wkSubst k idSubst x) [ σ ] ≡⟨⟩
(σ ₛ•ₛ wk1Subst (wkSubst k idSubst)) x ≡⟨⟩
(σ ₛ•ₛ wkSubst (1+ k) idSubst) x ∎
step-sgSubst : ∀ (t : Term[ k ] n) u → wk (step ρ) t [ u ]₀ ≡ wk ρ t
step-sgSubst t _ = trans (step-consSubst t) (subst-id _)
wk1-sgSubst : ∀ (t : Term[ k ] n) u → wk1 t [ u ]₀ ≡ t
wk1-sgSubst _ _ = trans (step-sgSubst _ _) (wk-id _)
opaque
wk2-[,] : wk2 t [ u , v ]₁₀ ≡ t
wk2-[,] {t} {u} {v} =
wk2 t [ u , v ]₁₀ ≡⟨ wk2-tail t ⟩
t [ idSubst ] ≡⟨ subst-id _ ⟩
t ∎
opaque
wk₂-[,] : wk₂ t [ u , v ]₁₀ ≡ t
wk₂-[,] {t} {u} {v} =
wk₂ t [ u , v ]₁₀ ≡⟨ subst-wk t ⟩
t [ idSubst ] ≡⟨ subst-id _ ⟩
t ∎
[1]↑² : t [ var x1 ]↑² ≡ wk1 t
[1]↑² {t = t} =
t [ consSubst (λ x → var (x +2)) (var x1) ] ≡⟨ (flip substVar-to-subst t λ where
x0 → refl
(_ +1) → refl) ⟩
t [ (λ x → var (x +1)) ] ≡˘⟨ wk≡subst _ _ ⟩
wk1 t ∎
[wk1]↑² : (t : Term[ k ] (1 + n)) → t [ wk1 u ]↑² ≡ wk1 (t [ u ]↑)
[wk1]↑² {u = u} t =
t [ consSubst (λ x → var (x +2)) (wk1 u) ] ≡⟨ (flip substVar-to-subst t λ where
x0 → refl
(_ +1) → refl) ⟩
t [ wk1 ∘→ consSubst (λ x → var (x +1)) u ] ≡˘⟨ wk-subst t ⟩
wk1 (t [ consSubst (λ x → var (x +1)) u ]) ∎
subst-β-prodrec :
(t : Term[ k ] (1+ n)) (σ : Subst m n) →
t [ prod s p (var x1) (var x0) ]↑² [ σ ⇑[ 2 ] ] ≡
t [ σ ⇑ ] [ prod s p (var x1) (var x0) ]↑²
subst-β-prodrec {n} t σ =
t [ t₁′ ]↑² [ σ ⇑[ 2 ] ] ≡⟨ substCompEq t ⟩
t [ (σ ⇑[ 2 ]) ₛ•ₛ replace₁ 2 t₁′ ] ≡⟨ substVar-to-subst varEq t ⟩
t [ consSubst (wkSubst 2 idSubst) t₂′ ₛ•ₛ (σ ⇑) ] ≡˘⟨ substCompEq t ⟩
t [ σ ⇑ ] [ t₂′ ]↑² ∎
where
t₁′ = prod! (var (x0 +1)) (var x0)
t₂′ = prod! (var (x0 +1)) (var x0)
varEq :
(x : Fin (1+ n)) →
(liftSubstn σ 2 ₛ•ₛ consSubst (wkSubst 2 idSubst) t₁′) x ≡
(consSubst (wkSubst 2 idSubst) t₂′ ₛ•ₛ liftSubst σ) x
varEq x0 = refl
varEq (x +1) = begin
wk1 (wk1 (σ x))
≡⟨ wk≡subst (step id) (wk1 (σ x)) ⟩
wk1 (σ x) [ wk1Subst idSubst ]
≡⟨ subst-wk (σ x) ⟩
σ x [ wk1Subst idSubst ₛ• step id ]
≡⟨ substVar-to-subst (λ x₁ → refl) (σ x) ⟩
σ x [ (λ y → var (y +2)) ]
≡˘⟨ wk1-tail (σ x) ⟩
wk1 (σ x) [ consSubst (λ y → var (y +2)) t₂′ ] ∎
substComp↑² :
(t : Term (1+ n)) (u : Term (2 + n)) →
t [ consSubst (tail[ 2 ] σ) (u [ σ ]) ] ≡ t [ u ]↑² [ σ ]
substComp↑² {σ} t u =
t [ consSubst (tail[ 2 ] σ) (u [ σ ]) ] ≡⟨ substVar-to-subst (λ { x0 → refl; (_ +1) → refl }) t ⟩
t [ σ ₛ•ₛ replace₁ 2 u ] ≡˘⟨ substCompEq t ⟩
t [ u ]↑² [ σ ] ∎
substCompProdrec :
(t : Term[ k ] (1+ n)) (u v : Term m) (σ : Subst m n) →
t [ σ ⇑ ] [ prod s p u v ]₀ ≡
t [ prod s p (var x1) (var x0) ]↑² [ consSubst (consSubst σ u) v ]
substCompProdrec t u v σ =
t [ σ ⇑ ] [ prod! u v ]₀ ≡⟨ substCompEq t ⟩
t [ sgSubst (prod! u v) ₛ•ₛ (σ ⇑) ] ≡⟨ flip substVar-to-subst t
(λ { x0 → refl; (x +1) → trans (wk1-tail (σ x)) (subst-id _) }) ⟩
t [ consSubst (consSubst σ u) v ₛ•ₛ replace₁ 2 px ] ≡˘⟨ substCompEq t ⟩
t [ px ]↑² [ consSubst (consSubst σ u) v ] ∎
where
px = prod! (var (x0 +1)) (var x0)
opaque
[1,0]↑²[,] :
(t : Term[ k ] (1+ n)) →
t [ prod s p (var x1) (var x0) ]↑² [ u , v ]₁₀ ≡
t [ prod s p u v ]₀
[1,0]↑²[,] {s} {p} {u} {v} t =
t [ prod s p (var x1) (var x0) ]↑² [ u , v ]₁₀ ≡˘⟨ substCompProdrec t _ _ _ ⟩
t [ liftSubst idSubst ] [ prod s p u v ]₀ ≡⟨ cong _[ _ ] $
trans (substVar-to-subst subst-lift-id t) $
subst-id t ⟩
t [ prod s p u v ]₀ ∎
opaque
doubleSubstComp′ :
(t : Term[ k ] (2+ n)) →
t [ liftSubstn σ₁ 2 ] [ consSubst (consSubst σ₂ u) v ] ≡
t [ consSubst (consSubst (σ₂ ₛ•ₛ σ₁) u) v ]
doubleSubstComp′ {σ₁} {σ₂} {u} {v} t =
t [ liftSubstn σ₁ 2 ] [ consSubst (consSubst σ₂ u) v ] ≡⟨ substCompEq t ⟩
t [ consSubst (consSubst σ₂ u) v ₛ•ₛ liftSubstn σ₁ 2 ] ≡⟨ (flip substVar-to-subst t λ {
x0 → refl;
(x0 +1) → refl;
((x +1) +1) →
wk2 (σ₁ x) [ consSubst (consSubst σ₂ u) v ] ≡⟨ wk2-tail (σ₁ _) ⟩
σ₁ x [ σ₂ ] ∎ }) ⟩
t [ consSubst (consSubst (σ₂ ₛ•ₛ σ₁) u) v ] ∎
doubleSubstComp :
(t : Term[ k ] (2+ n)) (u v : Term m) (σ : Subst m n) →
t [ σ ⇑[ 2 ] ] [ u , v ]₁₀ ≡ t [ consSubst (consSubst σ u) v ]
doubleSubstComp t u v σ =
t [ σ ⇑[ 2 ] ] [ u , v ]₁₀ ≡⟨ doubleSubstComp′ t ⟩
t [ consSubst (consSubst (idSubst ₛ•ₛ σ) u) v ] ≡⟨ flip substVar-to-subst t $ consSubst-cong refl $ consSubst-cong refl idSubst-ₛ•ₛˡ ⟩
t [ consSubst (consSubst σ u) v ] ∎
head-tail-subst :
(t : Term[ k ] (1+ n)) → t [ σ ] ≡ t [ consSubst (tail σ) (head σ) ]
head-tail-subst t =
substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) t
opaque
wk-subst-closed : {ρ : Wk n 0} {σ : Subst 0 n}
→ (t : Term[ k ] 0)
→ wk ρ t [ σ ] ≡ t
wk-subst-closed {0} {ρ = id} {σ} t = begin
wk id t [ σ ] ≡⟨ cong (_[ σ ]) (wk-id t) ⟩
t [ σ ] ≡⟨ substVar-to-subst (λ ()) t ⟩
t [ idSubst ] ≡⟨ subst-id t ⟩
t ∎
wk-subst-closed {1+ n} {ρ = step ρ} {σ} t = begin
wk (step ρ) t [ σ ] ≡⟨ head-tail-subst (wk (step ρ) t) ⟩
wk (step ρ) t [ consSubst (tail σ) (head σ) ] ≡⟨ step-consSubst t ⟩
wk ρ t [ tail σ ] ≡⟨ wk-subst-closed t ⟩
t ∎
opaque
wk₀-subst : (t : Term[ k ] 0) → wk wk₀ t [ σ ] ≡ t
wk₀-subst t = wk-subst-closed t
opaque
wk₀-closed : {t : Term[ k ] 0} → wk wk₀ t ≡ t
wk₀-closed {t} =
wk wk₀ t ≡˘⟨ subst-id _ ⟩
wk wk₀ t [ idSubst ] ≡⟨ wk₀-subst _ ⟩
t ∎
opaque
wk-wk₀-[]≡ : wk wk₀ t [ σ ] ≡ wk wk₀ t
wk-wk₀-[]≡ {t} {σ} =
wk wk₀ t [ σ ] ≡⟨ subst-wk t ⟩
t [ σ ₛ• wk₀ ] ≡⟨ substVar-to-subst (λ ()) t ⟩
t [ toSubst wk₀ ] ≡˘⟨ wk≡subst _ _ ⟩
wk wk₀ t ∎
opaque
wk-subst-lift-closed : {ρ : Wk n 0} {σ : Subst 0 n}
→ (t : Term[ k ] 1)
→ wk (lift ρ) t [ liftSubst σ ] ≡ t
wk-subst-lift-closed {ρ} {σ} t = begin
wk (lift ρ) t [ liftSubst σ ] ≡⟨ subst-wk t ⟩
t [ liftSubst σ ₛ• lift ρ ] ≡⟨ subst-lift-ₛ• t ⟩
t [ liftSubst (σ ₛ• ρ) ] ≡⟨ substVar-to-subst (substVar-lift (λ ())) t ⟩
t [ liftSubst idSubst ] ≡⟨ substVar-to-subst subst-lift-id t ⟩
t [ idSubst ] ≡⟨ subst-id t ⟩
t ∎
opaque
lifts-step-sgSubst :
(m : Nat) (t : Term (m + n)) →
wk (liftn ρ m) t ≡ wk (liftn (step ρ) m) t [ sgSubst u ⇑[ m ] ]
lifts-step-sgSubst {ρ} {u} m t =
wk (liftn ρ m) t ≡⟨ wk≡subst (liftn ρ m) t ⟩
t [ toSubst (liftn ρ m) ] ≡⟨ substVar-to-subst (lemma m) t ⟩
t [ (sgSubst u ₛ• step ρ) ⇑[ m ] ] ≡˘⟨ subst-lifts-ₛ• m t ⟩
t [ (sgSubst u ⇑[ m ]) ₛ• liftn (step ρ) m ] ≡˘⟨ subst-wk t ⟩
wk (liftn (step ρ) m) t [ sgSubst u ⇑[ m ] ] ∎
where
lemma :
∀ (m : Nat) x →
toSubst (liftn ρ m) x ≡ ((sgSubst u ₛ• step ρ) ⇑[ m ]) x
lemma 0 _ = refl
lemma (1+ _) x0 = refl
lemma (1+ m) (x +1) = cong wk1 (lemma m x)
opaque
lifts-step-[,] :
(m : Nat) (t : Term[ k ] (m + n)) →
wk (liftn ρ m) t ≡
wk (liftn (stepn ρ 2) m) t [ consSubst (sgSubst u) v ⇑[ m ] ]
lifts-step-[,] {ρ} {u} {v} m t =
wk (liftn ρ m) t ≡⟨ wk≡subst (liftn ρ m) t ⟩
t [ toSubst (liftn ρ m) ] ≡⟨ substVar-to-subst (lemma m) t ⟩
t [ (consSubst (sgSubst u) v ⇑[ m ]) ₛ• liftn (stepn ρ 2) m ] ≡˘⟨ subst-wk t ⟩
wk (liftn (stepn ρ 2) m) t [ consSubst (sgSubst u) v ⇑[ m ] ] ∎
where
lemma :
∀ (m : Nat) x →
toSubst (liftn ρ m) x ≡
((consSubst (sgSubst u) v ⇑[ m ]) ₛ• liftn (stepn ρ 2) m) x
lemma 0 _ = refl
lemma (1+ m) x0 = refl
lemma (1+ m) (x +1) = cong wk1 (lemma m x)
opaque
[]≡wk-wk₀ : {σ : Subst n 0} (t : Term[ k ] 0) → t [ σ ] ≡ wk wk₀ t
[]≡wk-wk₀ {σ} t =
t [ σ ] ≡⟨ substVar-to-subst (λ ()) t ⟩
t [ toSubst wk₀ ] ≡˘⟨ wk≡subst _ _ ⟩
wk wk₀ t ∎
opaque
[]-closed : {t : Term[ k ] 0} → t [ σ ] ≡ t
[]-closed {σ} {t} =
t [ σ ] ≡⟨ []≡wk-wk₀ t ⟩
wk wk₀ t ≡⟨ wk₀-closed ⟩
t ∎
opaque
[,]≡[wk1]₀[]₀ :
(t : Term[ k ] (2+ n)) → t [ u , v ]₁₀ PE.≡ t [ wk1 v ]₀ [ u ]₀
[,]≡[wk1]₀[]₀ {u} {v} t =
t [ u , v ]₁₀ ≡˘⟨ PE.cong (t [ _ ,_]₁₀) $ wk1-sgSubst _ _ ⟩
t [ u , wk1 v [ u ]₀ ]₁₀ ≡⟨ substConsId t ⟩
t [ wk1 v ]₀ [ u ]₀ ∎
opaque
[,]-[]-fusion :
(t : Term[ k ] (2+ n)) →
t [ u , v ]₁₀ [ σ ] ≡
t [ consSubst (consSubst σ (u [ σ ])) (v [ σ ]) ]
[,]-[]-fusion {u} {v} {σ} t =
t [ u , v ]₁₀ [ σ ] ≡⟨ substCompEq t ⟩
t [ σ ₛ•ₛ consSubst (sgSubst u) v ] ≡⟨ (flip substVar-to-subst t λ where
x0 → refl
(x0 +1) → refl
(_ +2) → refl) ⟩
t [ consSubst (consSubst σ (u [ σ ])) (v [ σ ]) ] ∎
opaque
[,]-[]-commute :
(t : Term[ k ] (2+ n)) →
t [ u , v ]₁₀ [ σ ] ≡
t [ liftSubstn σ 2 ] [ u [ σ ] , v [ σ ] ]₁₀
[,]-[]-commute {u} {v} {σ} t =
t [ u , v ]₁₀ [ σ ] ≡⟨ [,]-[]-fusion t ⟩
t [ consSubst (consSubst σ (u [ σ ])) (v [ σ ]) ] ≡˘⟨ doubleSubstComp t _ _ _ ⟩
t [ liftSubstn σ 2 ] [ u [ σ ] , v [ σ ] ]₁₀ ∎
opaque
≡Unit-wk1[]₀ :
Unit s ≡ Unit s [ t ]₀
≡Unit-wk1[]₀ {s} {t} = refl
opaque
≡Id-wk1-wk1-0[]₀ :
Id A t u ≡ Id (wk1 A) (wk1 t) (var x0) [ u ]₀
≡Id-wk1-wk1-0[]₀ {A} {t} {u} =
Id A t u ≡˘⟨ cong₂ (λ A t → Id A t _) (wk1-sgSubst _ _) (wk1-sgSubst _ _) ⟩
Id (wk1 A [ u ]₀) (wk1 t [ u ]₀) u ≡⟨⟩
Id (wk1 A) (wk1 t) (var x0) [ u ]₀ ∎
opaque
≡Id-wk2-wk2-1[,] :
Id A t u ≡ Id (wk2 A) (wk2 t) (var x1) [ u , v ]₁₀
≡Id-wk2-wk2-1[,] {A} {t} {u} {v} =
Id A t u ≡˘⟨ cong₂ (λ A t → Id A t _) wk2-[,] wk2-[,] ⟩
Id (wk2 A [ u , v ]₁₀) (wk2 t [ u , v ]₁₀) u ≡⟨⟩
Id (wk2 A) (wk2 t) (var x1) [ u , v ]₁₀ ∎
opaque
Id-wk1-wk1-0[⇑]≡ :
∀ A t →
Id (wk1 A) (wk1 t) (var x0) [ liftSubst σ ] ≡
Id (wk1 (A [ σ ])) (wk1 (t [ σ ])) (var x0)
Id-wk1-wk1-0[⇑]≡ {σ} A t =
Id (wk1 A) (wk1 t) (var x0) [ liftSubst σ ] ≡⟨⟩
Id (wk1 A [ liftSubst σ ]) (wk1 t [ liftSubst σ ]) (var x0) ≡⟨ cong₂ (λ A t → Id A t _) (wk1-liftSubst A) (wk1-liftSubst t) ⟩
Id (wk1 (A [ σ ])) (wk1 (t [ σ ])) (var x0) ∎
opaque
[]↑-[]₀ :
(t : Term[ k ] (1+ n)) →
t [ u ]↑ [ v ]₀ ≡ t [ u [ v ]₀ ]₀
[]↑-[]₀ {u} {v} t =
t [ u ]↑ [ v ]₀ ≡⟨ substCompEq t ⟩
t [ sgSubst v ₛ•ₛ replace₁ 1 u ] ≡⟨ substVar-to-subst lemma t ⟩
t [ u [ v ]₀ ]₀ ∎
where
lemma : ∀ x → (sgSubst v ₛ•ₛ replace₁ 1 u) x ≡ sgSubst (u [ v ]₀) x
lemma x0 = refl
lemma (_ +1) = refl
opaque
lift-step-natrec : ∀ A z s n
→ natrec p q r
(wk (lift ρ) A [ liftSubst σ ])
(wk ρ z [ σ ])
(wk (liftn ρ 2) s [ liftSubstn σ 2 ])
n
≡ natrec p q r
(wk (liftn ρ 2) (wk (lift (step id)) A) [ liftSubst (consSubst σ u) ])
(wk (lift ρ) (wk1 z) [ consSubst σ u ])
(wk (liftn ρ 3) (wk (liftn (step id) 2) s) [ liftSubstn (consSubst σ u) 2 ])
n
lift-step-natrec {ρ} {σ} {u} A z s n =
case begin
wk (lift ρ) A [ liftSubst σ ]
≡⟨ subst-wk A ⟩
A [ liftSubst σ ₛ• lift ρ ]
≡⟨ substVar-to-subst (λ { x0 → refl ; (_+1 x) → refl}) A ⟩
A [ liftSubst (consSubst σ u) ₛ• lift (step ρ) ]
≡˘⟨ cong (λ x → A [ liftSubst (consSubst σ u) ₛ• lift (step x) ]) (•-idʳ ρ) ⟩
A [ liftSubst (consSubst σ u) ₛ• lift (step (ρ • id)) ]
≡˘⟨ subst-wk A ⟩
wk (lift (step (ρ • id))) A [ liftSubst (consSubst σ u) ]
≡˘⟨ cong (_[ liftSubst (consSubst σ u) ]) (wk-comp (liftn ρ 2) (lift (step id)) A) ⟩
wk (liftn ρ 2) (wk (lift (step id)) A) [ liftSubst (consSubst σ u) ] ∎ of λ
A≡A′ →
case begin
wk ρ z [ σ ] ≡˘⟨ step-consSubst z ⟩
wk (step ρ) z [ consSubst σ u ] ≡˘⟨ cong (_[ consSubst σ u ]) (lift-wk1 ρ z) ⟩
wk (lift ρ) (wk1 z) [ consSubst σ u ] ∎ of λ
z≡z′ →
case begin
wk (liftn ρ 2) s [ liftSubstn σ 2 ]
≡⟨ subst-wk s ⟩
s [ liftSubstn σ 2 ₛ• liftn ρ 2 ]
≡⟨ substVar-to-subst (λ { x0 → refl ; (x0 +1) → refl ; (x +2) → refl}) s ⟩
s [ liftSubstn (consSubst σ u) 2 ₛ• liftn (step ρ) 2 ]
≡˘⟨ subst-wk s ⟩
wk (liftn (step ρ) 2) s [ liftSubstn (consSubst σ u) 2 ]
≡˘⟨ cong (λ x → wk (liftn (step x) 2) s [ liftSubstn (consSubst σ u) 2 ]) (•-idʳ ρ) ⟩
wk (liftn (step (ρ • id)) 2) s [ liftSubstn (consSubst σ u) 2 ]
≡˘⟨ cong (_[ liftSubstn (consSubst σ u) 2 ]) (wk-comp (liftn ρ 3) (liftn (step id) 2) s) ⟩
wk (liftn ρ 3) (wk (liftn (step id) 2) s) [ liftSubstn (consSubst σ u) 2 ] ∎ of λ
s≡s′ →
cong₃ (λ A z s → natrec _ _ _ A z s n)
A≡A′ z≡z′ s≡s′
opaque
lift-step-natrec′ : ∀ A z s t
→ let σ′ = consSubst (consSubst σ u) v in
natrec p q r
(wk (lift ρ) A [ liftSubst σ ])
(wk ρ z [ σ ])
(wk (liftn ρ 2) s [ liftSubstn σ 2 ])
(t [ σ ])
≡ natrec p q r
(wk (lift (step (step id))) (wk (lift ρ) A) [ liftSubst σ′ ])
(wk (step (step id)) (wk ρ z) [ σ′ ])
(wk (liftn (step (step id)) 2) (wk (liftn ρ 2) s) [ liftSubstn σ′ 2 ])
(wk (step (step id)) t [ σ′ ] )
lift-step-natrec′ {(m)} {(n)} {σ} {u} {v} {ρ} A z s t =
case begin
wk (lift ρ) A [ liftSubst σ ] ≡⟨ subst-wk A ⟩
A [ liftSubst σ ₛ• lift ρ ] ≡⟨ substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) A ⟩
A [ liftSubst σ₊ ₛ• lift (step (step ρ)) ] ≡˘⟨ subst-wk A ⟩
wk (lift (step (step ρ))) A [ liftSubst σ₊ ] ≡˘⟨ cong (_[ liftSubst σ₊ ]) (wk-comp _ _ A) ⟩
wk (lift (step (step id))) (wk (lift ρ) A) [ liftSubst σ₊ ] ∎ of λ
A≡A′ →
case begin
wk ρ z [ σ ] ≡⟨ subst-wk z ⟩
z [ σ ₛ• ρ ] ≡⟨ substVar-to-subst (λ _ → refl) z ⟩
z [ σ₊ ₛ• step (step ρ) ] ≡˘⟨ subst-wk z ⟩
wk (step (step ρ)) z [ σ₊ ] ≡˘⟨ cong (_[ σ₊ ]) (wk-comp _ _ z) ⟩
wk (step (step id)) (wk ρ z) [ σ₊ ] ∎ of λ
z≡z′ →
case begin
wk (liftn ρ 2) s [ liftSubstn σ 2 ] ≡⟨ subst-wk s ⟩
s [ liftSubstn σ 2 ₛ• liftn ρ 2 ] ≡⟨ substVar-to-subst (λ { x0 → refl ; (x0 +1) → refl ; (x +2) → refl }) s ⟩
s [ liftSubstn σ₊ 2 ₛ• liftn (step (step ρ)) 2 ] ≡˘⟨ subst-wk s ⟩
wk (liftn (step (step ρ)) 2) s [ liftSubstn σ₊ 2 ] ≡˘⟨ cong (_[ liftSubstn σ₊ 2 ]) (wk-comp _ _ s) ⟩
wk (liftn (step (step id)) 2) (wk (liftn ρ 2) s) [ liftSubstn σ₊ 2 ] ∎ of λ
s≡s′ →
cong₄ (natrec _ _ _) A≡A′ z≡z′ s≡s′
(sym (trans (step-consSubst t) (wk1-tail t)))
where
σ₊ : Subst m (2+ n)
σ₊ = consSubst (consSubst σ u) v
opaque
push-subst-[] :
∀ t → subst Term[ k ] eq (t [ σ ]) ≡ t [ subst Term eq ∘→ σ ]
push-subst-[] {eq = refl} _ = refl
opaque
subst-cong-1+-wk1 :
(eq : m ≡ n) →
subst Term[ k ] (cong 1+ eq) (wk1 t) ≡
wk1 (subst Term[ k ] eq t)
subst-cong-1+-wk1 refl = refl
opaque
subst-Fin-x0 :
(eq : 1+ m ≡ 1+ n) →
subst Fin eq x0 ≡ x0
subst-Fin-x0 refl = refl
opaque
subst-Fin-+1 :
(eq : m ≡ n) →
subst Fin (cong 1+ eq) (x +1) ≡ subst Fin eq x +1
subst-Fin-+1 refl = refl
opaque
subst-Term-var-x0 :
(eq : 1+ m ≡ 1+ n) →
subst Term eq (var x0) ≡ var x0
subst-Term-var-x0 refl = refl
opaque
wk[]≡wk[]′ : wk[ n ] t ≡ wk[ n ]′ t
wk[]≡wk[]′ {n = 0} {t} =
t ≡˘⟨ wk-id _ ⟩
wk id t ∎
wk[]≡wk[]′ {n = 1+ n} {t} =
wk1 (wk[ n ] t) ≡⟨ cong wk1 wk[]≡wk[]′ ⟩
wk1 (wk[ n ]′ t) ≡⟨ wk-comp _ _ _ ⟩
wk[ 1+ n ]′ t ∎
opaque
wk[]≡[] : ∀ n → wk[ n ] t ≡ t [ wkSubst n idSubst ]
wk[]≡[] {t} 0 =
t ≡˘⟨ subst-id _ ⟩
t [ idSubst ] ∎
wk[]≡[] {t} (1+ n) =
wk1 (wk[ n ] t) ≡⟨ cong wk1 $ wk[]≡[] n ⟩
wk1 (t [ wkSubst n idSubst ]) ≡⟨ wk≡subst _ _ ⟩
t [ wkSubst n idSubst ] [ wk1Subst idSubst ] ≡⟨ substCompEq t ⟩
t [ wk1Subst idSubst ₛ•ₛ wkSubst n idSubst ] ≡⟨ substVar-to-subst lemma t ⟩
t [ wkSubst (1+ n) idSubst ] ∎
where
lemma :
(x : Fin m) →
(wk1Subst idSubst ₛ•ₛ wkSubst n idSubst) x ≡
wkSubst (1+ n) idSubst x
lemma x =
(wk1Subst idSubst ₛ•ₛ wkSubst n idSubst) x ≡⟨⟩
wkSubst n idSubst x [ wk1Subst idSubst ] ≡⟨ wk1Subst-wk1 (wkSubst n _ _) ⟩
wk1 (wkSubst n idSubst x [ idSubst ]) ≡⟨ cong wk1 $ subst-id _ ⟩
wk1 (wkSubst n idSubst x) ≡⟨⟩
wkSubst (1+ n) idSubst x ∎
opaque
wk[]≡wkSubst : ∀ n x → wk[ n ] (σ x) ≡ wkSubst n σ x
wk[]≡wkSubst 0 _ = refl
wk[]≡wkSubst (1+ n) _ = cong wk1 (wk[]≡wkSubst n _)
opaque
wk[]′≡wkSubst : ∀ n x → wk[ n ]′ (σ x) ≡ wkSubst n σ x
wk[]′≡wkSubst {σ} n x =
wk[ n ]′ (σ x) ≡˘⟨ wk[]≡wk[]′ ⟩
wk[ n ] (σ x) ≡⟨ wk[]≡wkSubst n _ ⟩
wkSubst n σ x ∎
opaque
wkSubst-as-composition :
∀ n x → wkSubst n σ x ≡ (toSubst (stepn id n) ₛ•ₛ σ) x
wkSubst-as-composition {σ} n x =
wkSubst n σ x ≡˘⟨ wk[]′≡wkSubst n _ ⟩
wk[ n ]′ (σ x) ≡⟨ wk≡subst _ _ ⟩
σ x [ toSubst (stepn id n) ] ∎
opaque
wkSubst-idSubst-ₛ•ₛ :
∀ n x → (wkSubst n idSubst ₛ•ₛ σ) x ≡ wkSubst n σ x
wkSubst-idSubst-ₛ•ₛ {σ} n x =
σ x [ wkSubst n idSubst ] ≡˘⟨ wk[]≡[] n ⟩
wk[ n ] (σ x) ≡⟨ wk[]≡wkSubst n _ ⟩
wkSubst n σ x ∎
opaque
wkSubst-comp :
∀ m x →
subst Term (+-assoc m n o) (wkSubst (m + n) σ x) ≡
wkSubst m (wkSubst n σ) x
wkSubst-comp 0 _ = refl
wkSubst-comp {n} {o} {σ} (1+ m) x =
subst Term (cong 1+ (+-assoc m n o)) (wk1 (wkSubst (m + n) σ x)) ≡⟨ subst-cong-1+-wk1 (+-assoc m _ _) ⟩
wk1 (subst Term (+-assoc m n o) (wkSubst (m + n) σ x)) ≡⟨ cong wk1 $ wkSubst-comp m _ ⟩
wk1 (wkSubst m (wkSubst n σ) x) ∎
opaque
wk[]-comp :
∀ m →
subst Term[ k ] (+-assoc m n o) (wk[ m + n ] t) ≡
wk[ m ] (wk[ n ] t)
wk[]-comp {k} {n} {o} {t} m =
subst Term[ k ] (+-assoc m n o) (wk[ m + n ] t) ≡⟨ cong (subst _ _) $ wk[]≡[] (m + _) ⟩
subst Term[ k ] (+-assoc m n o) (t [ wkSubst (m + n) idSubst ]) ≡⟨ push-subst-[] t ⟩
t [ subst Term (+-assoc m n o) ∘→ wkSubst (m + n) idSubst ] ≡⟨ flip substVar-to-subst t $ wkSubst-comp m ⟩
t [ wkSubst m (wkSubst n idSubst) ] ≡˘⟨ flip substVar-to-subst t $ wkSubst-idSubst-ₛ•ₛ m ⟩
t [ wkSubst m idSubst ₛ•ₛ wkSubst n idSubst ] ≡˘⟨ substCompEq t ⟩
t [ wkSubst n idSubst ] [ wkSubst m idSubst ] ≡˘⟨ wk[]≡[] m ⟩
wk[ m ] (t [ wkSubst n idSubst ]) ≡˘⟨ cong wk[ m ] $ wk[]≡[] n ⟩
wk[ m ] (wk[ n ] t) ∎
opaque
wk[]′-comp :
∀ m →
subst Term[ k ] (+-assoc m n o) (wk[ m + n ]′ t) ≡
wk[ m ]′ (wk[ n ]′ t)
wk[]′-comp {k} {n} {o} {t} m =
subst Term[ k ] (+-assoc m n o) (wk[ m + n ]′ t) ≡˘⟨ cong (subst Term[ _ ] (+-assoc m _ _)) wk[]≡wk[]′ ⟩
subst Term[ k ] (+-assoc m n o) (wk[ m + n ] t) ≡⟨ wk[]-comp m ⟩
wk[ m ] (wk[ n ] t) ≡⟨ trans wk[]≡wk[]′ $
cong wk[ _ ]′ wk[]≡wk[]′ ⟩
wk[ m ]′ (wk[ n ]′ t) ∎
opaque
wk[]-wk[]′-comp :
∀ m →
subst Term[ k ] (+-assoc m n o) (wk[ m + n ]′ t) ≡
wk[ m ] (wk[ n ]′ t)
wk[]-wk[]′-comp {k} {n} {o} {t} m =
subst Term[ k ] (+-assoc m n o) (wk[ m + n ]′ t) ≡⟨ wk[]′-comp _ ⟩
wk[ m ]′ (wk[ n ]′ t) ≡˘⟨ wk[]≡wk[]′ ⟩
wk[ m ] (wk[ n ]′ t) ∎
opaque
wk[]-⇑[] : ∀ n → wk[ n ] t [ σ ⇑[ n ] ] ≡ wk[ n ] (t [ σ ])
wk[]-⇑[] 0 = refl
wk[]-⇑[] {t} {σ} (1+ n) =
wk1 (wk[ n ] t) [ σ ⇑[ n ] ⇑ ] ≡⟨ wk1-liftSubst (wk[ n ] _) ⟩
wk1 (wk[ n ] t [ σ ⇑[ n ] ]) ≡⟨ cong wk1 $ wk[]-⇑[] n ⟩
wk1 (wk[ n ] (t [ σ ])) ∎
opaque
wk-liftn-[⇑] :
∀ m (t : Term[ k ] (m + o)) →
wk (liftn ρ m) t [ σ ⇑[ m ] ] ≡
t [ (σ ₛ• ρ) ⇑[ m ] ]
wk-liftn-[⇑] {ρ} {σ} m t =
wk (liftn ρ m) t [ σ ⇑[ m ] ] ≡⟨ subst-wk t ⟩
t [ (σ ⇑[ m ]) ₛ• liftn ρ m ] ≡⟨ substVar-to-subst (lemma m) t ⟩
t [ (σ ₛ• ρ) ⇑[ m ] ] ∎
where
lemma : ∀ m x → ((σ ⇑[ m ]) ₛ• liftn ρ m) x ≡ ((σ ₛ• ρ) ⇑[ m ]) x
lemma 0 _ = refl
lemma (1+ _) x0 = refl
lemma (1+ m) (x +1) = cong wk1 (lemma m x)
opaque
wk-liftn-stepn-[⇑]₁ :
∀ m (t : Term[ k ] (m + o)) →
wk (liftn (stepn id n) m) (t [ σ ⇑[ m ] ]) ≡
t [ wkSubst n σ ⇑[ m ] ]
wk-liftn-stepn-[⇑]₁ {n} m t =
trans (wk-liftn m) $
trans (substCompEq t) $
flip substVar-to-subst t λ x →
trans (substCompLifts m x) $
substVar-lifts (sym ∘→ wkSubst-as-composition n) m x
private opaque
wk-liftn-stepn-[⇑]₂-lemma :
∀ {o₁ o₂} {σ : Subst o₁ o₂} m →
let cast₁ = PE.subst Fin (sym (+-assoc m n o₂))
cast₂ = PE.subst Term (sym (+-assoc m n o₁))
in
∀ x →
((σ ⇑[ m + n ] ∘→ cast₁) ₛ• liftn (stepn id n) m) x ≡
(cast₂ ∘→ wkSubst n σ ⇑[ m ]) x
wk-liftn-stepn-[⇑]₂-lemma {n = 0} 0 _ = refl
wk-liftn-stepn-[⇑]₂-lemma {n = 1+ n} {σ} 0 x =
wk1 ((σ ⇑[ n ]) (wkVar (stepn id n) x)) ≡⟨ cong wk1 (wk-liftn-stepn-[⇑]₂-lemma {n = n} 0 x) ⟩
wk1 (wkSubst n σ x) ∎
wk-liftn-stepn-[⇑]₂-lemma {n} {σ} (1+ m) x0 =
(σ ⇑[ m + n ] ⇑) (subst Fin (sym (+-assoc (1+ m) _ _)) x0) ≡⟨ cong (_ ⇑) (subst-Fin-x0 (sym (+-assoc (1+ m) _ _))) ⟩
(σ ⇑[ m + n ] ⇑) x0 ≡⟨⟩
var x0 ≡˘⟨ subst-Term-var-x0 (sym (+-assoc (1+ m) _ _)) ⟩
subst Term (sym (+-assoc (1+ m) _ _)) (var x0) ∎
wk-liftn-stepn-[⇑]₂-lemma {n} {σ} (1+ m) (x +1) =
(σ ⇑[ m + n ] ⇑)
(subst Fin (sym (cong 1+ (+-assoc m _ _)))
(wkVar (liftn (stepn id n) m) x +1)) ≡˘⟨ cong (_ ⇑) (cong (flip (subst _) _) (cong-sym (+-assoc m _ _))) ⟩
(σ ⇑[ m + n ] ⇑)
(subst Fin (cong 1+ (sym (+-assoc m _ _)))
(wkVar (liftn (stepn id n) m) x +1)) ≡⟨ cong (_ ⇑) (subst-Fin-+1 (sym (+-assoc m _ _))) ⟩
(σ ⇑[ m + n ] ⇑)
(subst Fin (sym (+-assoc m _ _))
(wkVar (liftn (stepn id n) m) x) +1) ≡⟨⟩
wk1
((σ ⇑[ m + n ])
(subst Fin (sym (+-assoc m _ _))
((wkVar (liftn (stepn id n) m) x)))) ≡⟨ cong wk1 (wk-liftn-stepn-[⇑]₂-lemma m x) ⟩
wk1 (subst Term (sym (+-assoc m _ _)) ((wkSubst n σ ⇑[ m ]) x)) ≡˘⟨ subst-cong-1+-wk1 (sym (+-assoc m _ _)) ⟩
subst Term (cong 1+ (sym (+-assoc m _ _)))
(wk1 ((wkSubst n σ ⇑[ m ]) x)) ≡⟨ cong (flip (subst _) _) (cong-sym (+-assoc m _ _)) ⟩
subst Term (sym (+-assoc (1+ m) _ _)) (wk1 ((wkSubst n σ ⇑[ m ]) x)) ∎
opaque
wk-liftn-stepn-[⇑]₂ :
∀ {o₁ o₂} {σ : Subst o₁ o₂} m →
let cast₁ = PE.subst Fin (sym (+-assoc m n o₂))
cast₂ = PE.subst Term[ k ] (sym (+-assoc m n o₁))
in
(t : Term[ k ] (m + o₂)) →
wk (liftn (stepn id n) m) t [ σ ⇑[ m + n ] ∘→ cast₁ ] ≡
cast₂ (wk (liftn (stepn id n) m) (t [ σ ⇑[ m ] ]))
wk-liftn-stepn-[⇑]₂ {n} {σ} m t =
let cast₁ = PE.subst Fin (sym (+-assoc m _ _))
cast₂ = PE.subst Term[ _ ] (sym (+-assoc m _ _))
cast₃ = PE.subst Term (sym (+-assoc m _ _))
in
wk (liftn (stepn id n) m) t [ σ ⇑[ m + n ] ∘→ cast₁ ] ≡⟨ subst-wk t ⟩
t [ (σ ⇑[ m + n ] ∘→ cast₁) ₛ• liftn (stepn id n) m ] ≡⟨ substVar-to-subst (wk-liftn-stepn-[⇑]₂-lemma m) t ⟩
t [ cast₃ ∘→ wkSubst n σ ⇑[ m ] ] ≡˘⟨ push-subst-[] t ⟩
cast₂ (t [ wkSubst n σ ⇑[ m ] ]) ≡˘⟨ cong cast₂ (wk-liftn-stepn-[⇑]₁ m t) ⟩
cast₂ (wk (liftn (stepn id n) m) (t [ σ ⇑[ m ] ])) ∎
opaque
wk[]′-[⇑] :
(t : Term[ k ] m) → wk[ n ]′ t [ σ ⇑[ n ] ] ≡ wk[ n ]′ (t [ σ ])
wk[]′-[⇑] = wk-liftn-stepn-[⇑]₂ 0
opaque
wk[]′-[]↑ : wk[ 1+ n ]′ t [ u ]↑ ≡ wk[ 1+ n ]′ t
wk[]′-[]↑ {n} {t} {u} =
wk[ 1+ n ]′ t [ u ]↑ ≡⟨⟩
wk[ 1+ n ]′ t [ consSubst (wk1Subst idSubst) u ] ≡⟨ subst-wk t ⟩
t [ consSubst (wk1Subst idSubst) u ₛ• stepn id (1+ n) ] ≡⟨⟩
t [ toSubst (stepn id (1+ n)) ] ≡˘⟨ wk≡subst _ _ ⟩
wk[ 1+ n ]′ t ∎
opaque
wk[1+]′-[]₀≡ : wk[ 1+ n ]′ t [ u ]₀ ≡ wk[ n ]′ t
wk[1+]′-[]₀≡ {n} {t} {u} =
wk[ 1+ n ]′ t [ u ]₀ ≡˘⟨ cong _[ _ ]₀ $ wk[]≡wk[]′ {n = 1+ n} ⟩
wk[ 1+ n ] t [ u ]₀ ≡⟨ wk1-sgSubst _ _ ⟩
wk[ n ] t ≡⟨ wk[]≡wk[]′ ⟩
wk[ n ]′ t ∎
opaque
wk[+1]′-[₀⇑]≡ :
{t : Term[ k ] m} →
subst Term[ k ] (+-assoc n _ _) (wk[ n + 1 ]′ t)
[ sgSubst u ⇑[ n ] ] ≡
wk[ n ]′ t
wk[+1]′-[₀⇑]≡ {k} {n} {u} {t} =
subst Term[ k ] (+-assoc n _ _) (wk[ n + 1 ]′ t) [ sgSubst u ⇑[ n ] ] ≡⟨ cong _[ _ ] $ wk[]′-comp {t = t} _ ⟩
wk[ n ]′ (wk1 t) [ sgSubst u ⇑[ n ] ] ≡⟨ wk[]′-[⇑] (wk1 t) ⟩
wk[ n ]′ (wk1 t [ u ]₀) ≡⟨ cong wk[ _ ]′ $ wk1-sgSubst _ _ ⟩
wk[ n ]′ t ∎
opaque
wk[2+]′-[,]≡ : wk[ 2+ n ]′ t [ u , v ]₁₀ ≡ wk[ n ]′ t
wk[2+]′-[,]≡ {n} {t} {u} {v} =
wk[ 2+ n ]′ t [ u , v ]₁₀ ≡˘⟨ cong _[ _ , _ ]₁₀ $ wk[]≡wk[]′ {n = 2+ n} ⟩
wk[ 2+ n ] t [ u , v ]₁₀ ≡⟨ wk2-[,] ⟩
wk[ n ] t ≡⟨ wk[]≡wk[]′ ⟩
wk[ n ]′ t ∎
opaque
wk[2+]′[,⇑]≡ :
{t : Term[ k ] m} →
subst Term[ k ] (+-assoc n _ _) (wk[ n + 2 ]′ t)
[ consSubst (sgSubst u) v ⇑[ n ] ] ≡
wk[ n ]′ t
wk[2+]′[,⇑]≡ {k} {n} {u} {v} {t} =
subst Term[ k ] (+-assoc n _ _) (wk[ n + 2 ]′ t)
[ consSubst (sgSubst u) v ⇑[ n ] ] ≡⟨ cong _[ _ ] $ wk[]′-comp n ⟩
wk[ n ]′ (wk[ 2 ]′ t) [ consSubst (sgSubst u) v ⇑[ n ] ] ≡⟨ wk[]′-[⇑] (wk[ _ ]′ t) ⟩
wk[ n ]′ (wk[ 2 ]′ t [ u , v ]₁₀) ≡⟨ cong wk[ _ ]′ wk₂-[,] ⟩
wk[ n ]′ t ∎
opaque
wk₂-tail : (t : Term[ k ] n) → wk₂ t [ σ ] ≡ t [ tail[ 2 ] σ ]
wk₂-tail {σ} t = begin
wk₂ t [ σ ] ≡˘⟨ cong _[ σ ] $ wk[]≡wk[]′ {t = t} ⟩
wk2 t [ σ ] ≡⟨ wk2-tail t ⟩
t [ tail[ 2 ] σ ] ∎
opaque
wk[]-tail :
∀ n {σ : Subst m (n + o)} → wk[ n ] t [ σ ] ≡ t [ tail[ n ] σ ]
wk[]-tail 0 = PE.refl
wk[]-tail {t} (1+ n) {σ} =
wk1 (wk[ n ] t) [ σ ] ≡⟨ wk1-tail (wk[ n ] _) ⟩
wk[ n ] t [ tail σ ] ≡⟨ wk[]-tail n ⟩
t [ tail[ n ] (tail σ) ] ∎
opaque
wk[]′-tail : (t : Term[ k ] m) → wk[ n ]′ t [ σ ] ≡ t [ tail[ n ] σ ]
wk[]′-tail {n} {σ} t =
wk[ n ]′ t [ σ ] ≡˘⟨ PE.cong _[ _ ] (wk[]≡wk[]′ {t = t}) ⟩
wk[ n ] t [ σ ] ≡⟨ wk[]-tail n ⟩
t [ tail[ n ] σ ] ∎
opaque
wk-lift-step-id-wk[1+]′≡ :
wk (lift (step id)) (wk[ 1+ n ]′ t) ≡ wk[ 2+ n ]′ t
wk-lift-step-id-wk[1+]′≡ {n} {t} =
wk (lift (step id)) (wk[ 1+ n ]′ t) ≡˘⟨ cong (wk _) $ wk-comp _ _ _ ⟩
wk (lift (step id)) (wk1 (wk[ n ]′ t)) ≡˘⟨ wk1-wk≡lift-wk1 _ _ ⟩
wk[ 2 ] (wk[ n ]′ t) ≡⟨ trans (wk[]≡wk[]′ {n = 2}) $
wk-comp _ _ _ ⟩
wk[ 2+ n ]′ t ∎
opaque
wk[]′-wk : wk[ n ]′ (wk ρ t) ≡ wk (stepn ρ n) t
wk[]′-wk {n} {ρ} {t} =
wk[ n ]′ (wk ρ t) ≡⟨ wk-comp _ _ _ ⟩
wk (stepn id n • ρ) t ≡⟨ cong (flip wk _) (stepn-id-• n) ⟩
wk (stepn ρ n) t ∎
opaque
wk⇑[]-wk[]≡ :
∀ n → wk (liftn ρ n) (wk[ n ]′ t) PE.≡ wk[ n ]′ (wk ρ t)
wk⇑[]-wk[]≡ {ρ} {t} n =
wk (liftn ρ n) (wk[ n ]′ t) ≡⟨ wk-comp _ _ _ ⟩
wk (liftn ρ n • stepn id n) t ≡˘⟨ cong (flip wk _) (liftn-stepn-comp n) ⟩
wk (stepn ρ n) t ≡˘⟨ wk[]′-wk ⟩
wk[ n ]′ (wk ρ t) ∎
opaque
doubleSubstWkComp :
(t : Term[ k ] (2+ n)) →
wk (liftn ρ 2) (t [ σ ⇑[ 2 ] ]) [ u , v ]₁₀ ≡
t [ consSubst (consSubst (ρ •ₛ σ) u) v ]
doubleSubstWkComp {ρ} {σ} {u} {v} t =
wk (liftn ρ 2) (t [ σ ⇑[ 2 ] ]) [ u , v ]₁₀ ≡⟨ cong _[ _ , _ ]₁₀ (wk-subst t) ⟩
t [ liftn ρ 2 •ₛ (σ ⇑[ 2 ]) ] [ u , v ]₁₀ ≡⟨ substCompEq t ⟩
t [ consSubst (sgSubst u) v ₛ•ₛ (liftn ρ 2 •ₛ (σ ⇑[ 2 ])) ] ≡⟨ (flip substVar-to-subst t λ {
x0 → refl;
(x0 +1) → refl;
(x +1 +1) →
wk (liftn ρ 2) (wk[ 2 ] (σ x)) [ u , v ]₁₀ ≡⟨ cong _[ _ , _ ]₁₀ (cong (wk _) (wk[]≡wk[]′ {t = σ _})) ⟩
wk (liftn ρ 2) (wk[ 2 ]′ (σ x)) [ u , v ]₁₀ ≡⟨ cong _[ _ , _ ]₁₀ (wk⇑[]-wk[]≡ {t = σ _} _) ⟩
wk[ 2 ]′ (wk ρ (σ x)) [ u , v ]₁₀ ≡⟨ wk₂-[,] ⟩
wk ρ (σ x) ∎ }) ⟩
t [ consSubst (consSubst (ρ •ₛ σ) u) v ] ∎
opaque
tripleSubstComp :
(t : Term (3+ n)) →
t [ σ ⇑[ 3 ] ] [ u , v , w ]₂₁₀ PE.≡
t [ consSubst (consSubst (consSubst σ u) v) w ]
tripleSubstComp {σ} {u} {v} {w} t =
t [ σ ⇑[ 3 ] ] [ u , v , w ]₂₁₀ ≡⟨ substCompEq t ⟩
t [ consSubst (consSubst (sgSubst u) v) w ₛ•ₛ (σ ⇑[ 3 ]) ] ≡⟨ (flip substVar-to-subst t λ where
x0 → PE.refl
(x0 +1) → PE.refl
(x0 +1 +1) → PE.refl
(_ +1 +1 +1) → wk[]-tail {t = σ _} 3) ⟩
t [ consSubst (consSubst (consSubst (idSubst ₛ•ₛ σ) u) v) w ] ≡⟨ flip substVar-to-subst t $
consSubst-cong PE.refl $
consSubst-cong PE.refl $
consSubst-cong PE.refl $
idSubst-ₛ•ₛˡ ⟩
t [ consSubst (consSubst (consSubst σ u) v) w ] ∎
opaque
[][]↑-[] :
∀ m {u} {σ : Subst n₁ (m + n₂)} (t : Term[ k ] (1+ n₂)) →
t [ m ][ u ]↑ [ σ ] ≡ t [ consSubst (tail[ m ] σ) (u [ σ ]) ]
[][]↑-[] m {u} {σ} t =
t [ m ][ u ]↑ [ σ ] ≡⟨ substCompEq t ⟩
t [ σ ₛ•ₛ replace₁ m u ] ≡˘⟨ (flip substVar-to-subst t λ where
x0 → refl
(_ +1) → tail[]≡ m _) ⟩
t [ consSubst (tail[ m ] σ) (u [ σ ]) ] ∎
private
_ : (t : Term[ k ] (1+ n)) → t [ u ]↑ [ v ]₀ ≡ t [ u [ v ]₀ ]₀
_ = [][]↑-[] 1
private
_ :
(t : Term[ k ] (2+ n)) →
t [ u ]↑ [ v , w ]₁₀ ≡ t [ v , u [ v , w ]₁₀ ]₁₀
_ = [][]↑-[] 1
private
_ :
(t : Term[ k ] (1+ n)) →
t [ 2 ][ u ]↑ [ v , w ]₁₀ ≡ t [ u [ v , w ]₁₀ ]₀
_ = [][]↑-[] 2
private
_ :
(t : Term[ k ] (1+ n)) →
t [ u ]↑ [ m ][ v ]↑ ≡ t [ m ][ u [ m ][ v ]↑ ]↑
_ = [][]↑-[] 1
opaque
[][]↑≡′ :
(t : Term[ k ] (1+ m)) →
t [ n ][ u ]↑ ≡ t [ consSubst (tail[ n ] idSubst) u ]
[][]↑≡′ {n} {u} t =
t [ n ][ u ]↑ ≡˘⟨ subst-id _ ⟩
t [ n ][ u ]↑ [ idSubst ] ≡⟨ [][]↑-[] _ t ⟩
t [ consSubst (tail[ n ] idSubst) (u [ idSubst ]) ] ≡⟨ substVar-to-subst (consSubst-cong (subst-id _) (λ _ → refl)) t ⟩
t [ consSubst (tail[ n ] idSubst) u ] ∎
opaque
[][]↑≡ :
(t : Term[ k ] (1+ m)) →
t [ n ][ u ]↑ ≡ wk (lift (stepn id n)) t [ u ]₀
[][]↑≡ {n} {u} t =
t [ replace₁ n u ] ≡⟨ (flip substVar-to-subst t λ where
x0 → refl
(x +1) →
trans (sym $ wk[]≡wkSubst n _) $
wk[]≡wk[]′ {t = var x}) ⟩
t [ sgSubst u ₛ• lift (stepn id n) ] ≡˘⟨ subst-wk t ⟩
wk (lift (stepn id n)) t [ u ]₀ ∎
opaque
wk-liftn-[][]↑ :
(t : Term[ k ] (1+ m)) →
wk (liftn ρ n) (t [ n ][ u ]↑) ≡
wk (lift ρ) t [ n ][ wk (liftn ρ n) u ]↑
wk-liftn-[][]↑ {ρ} {n} {u} t =
wk (liftn ρ n) (t [ n ][ u ]↑) ≡⟨ cong (wk _) ([][]↑≡ t) ⟩
wk (liftn ρ n) (wk (lift (stepn id n)) t [ u ]₀) ≡⟨ wk-subst (wk _ t) ⟩
wk (lift (stepn id n)) t [ liftn ρ n •ₛ sgSubst u ] ≡⟨ subst-wk t ⟩
t [ liftn ρ n •ₛ sgSubst u ₛ• lift (stepn id n) ] ≡⟨ (flip substVar-to-subst t λ where
x0 → refl
(_ +1) → wk⇑[]-wk[]≡ n) ⟩
t [ sgSubst (wk (liftn ρ n) u) ₛ• lift (stepn id n) ₛ• lift ρ ] ≡˘⟨ subst-wk t ⟩
wk (lift ρ) t [ sgSubst (wk (liftn ρ n) u) ₛ• lift (stepn id n) ] ≡˘⟨ subst-wk (wk _ t) ⟩
wk (lift (stepn id n)) (wk (lift ρ) t) [ wk (liftn ρ n) u ]₀ ≡˘⟨ [][]↑≡ (wk _ t) ⟩
wk (lift ρ) t [ n ][ wk (liftn ρ n) u ]↑ ∎
opaque
[][]↑-commutes :
(t : Term[ k ] (1+ m)) →
t [ n ][ u ]↑ [ σ ⇑[ n ] ] ≡
t [ σ ⇑ ] [ n ][ u [ σ ⇑[ n ] ] ]↑
[][]↑-commutes {m} {n} {u} {σ} t =
t [ n ][ u ]↑ [ σ ⇑[ n ] ] ≡⟨ substCompEq t ⟩
t [ (σ ⇑[ n ]) ₛ•ₛ replace₁ n u ] ≡⟨ (flip substVar-to-subst t λ where
x0 → refl
(x +1) → lemma (var x)) ⟩
t [ replace₁ n (u [ σ ⇑[ n ] ]) ₛ•ₛ (σ ⇑) ] ≡˘⟨ substCompEq t ⟩
t [ σ ⇑ ] [ n ][ u [ σ ⇑[ n ] ] ]↑ ∎
where
lemma :
(t : Term[ k ] m) →
t [ wkSubst n idSubst ] [ σ ⇑[ n ] ] ≡
wk1 (t [ σ ]) [ n ][ u [ σ ⇑[ n ] ] ]↑
lemma t =
t [ wkSubst n idSubst ] [ σ ⇑[ n ] ] ≡˘⟨ cong _[ _ ] $ wk[]≡[] n ⟩
wk[ n ] t [ σ ⇑[ n ] ] ≡⟨ wk[]-⇑[] n ⟩
wk[ n ] (t [ σ ]) ≡⟨ wk[]≡[] n ⟩
t [ σ ] [ wkSubst n idSubst ] ≡˘⟨ subst-wk (t [ _ ]) ⟩
wk1 (t [ σ ]) [ n ][ u [ σ ⇑[ n ] ] ]↑ ∎
opaque
[][]↑-commutes-+ :
let cast =
subst₂ Subst (sym $ +-assoc ℓ m₂ n) (sym $ +-assoc ℓ m₁ n)
in
(t : Term[ k ] (1+ n)) →
(∀ x → wk[ m₁ ] (var x) [ σ ] ≡ wk[ m₂ ] (var x)) →
t [ ℓ + m₁ ][ u ]↑ [ cast (σ ⇑[ ℓ ]) ] ≡
t [ ℓ + m₂ ][ u [ cast (σ ⇑[ ℓ ]) ] ]↑
[][]↑-commutes-+ {ℓ} {m₂} {n} {m₁} {σ} {u} t hyp =
t [ consSubst (wkSubst (ℓ + m₁) idSubst) u ] [ cast₁ (σ ⇑[ ℓ ]) ] ≡⟨ substCompEq t ⟩
t [ cast₁ (σ ⇑[ ℓ ]) ₛ•ₛ consSubst (wkSubst (ℓ + m₁) idSubst) u ] ≡⟨ (flip substVar-to-subst t λ where
x0 → refl
(_ +1) → lemma₂ _) ⟩
t [ consSubst (wkSubst (ℓ + m₂) idSubst) (u [ cast₁ (σ ⇑[ ℓ ]) ]) ] ∎
where
cast₁ :
Subst (ℓ + (m₂ + n)) (ℓ + (m₁ + n)) →
Subst (ℓ + m₂ + n) (ℓ + m₁ + n)
cast₁ = subst₂ Subst (sym $ +-assoc ℓ _ _) (sym $ +-assoc ℓ _ _)
cast₂ : Term (ℓ + (m₂ + n)) → Term (ℓ + m₂ + n)
cast₂ = subst Term (sym $ +-assoc ℓ _ _)
lemma₁ :
v [ subst₂ Subst eq₁ (sym eq₂) σ′ ] ≡
subst Term eq₁ (subst Term eq₂ v [ σ′ ])
lemma₁ {eq₁ = refl} {eq₂ = refl} = refl
lemma₂ :
∀ x →
wkSubst (ℓ + m₁) idSubst x [ cast₁ (σ ⇑[ ℓ ]) ] ≡
wkSubst (ℓ + m₂) idSubst x
lemma₂ x =
wkSubst (ℓ + m₁) idSubst x [ cast₁ (σ ⇑[ ℓ ]) ] ≡˘⟨ cong _[ _ ] $ wk[]≡wkSubst (ℓ + _) _ ⟩
wk[ ℓ + m₁ ] (var x) [ cast₁ (σ ⇑[ ℓ ]) ] ≡⟨ lemma₁ {eq₁ = sym $ +-assoc ℓ _ _} {eq₂ = +-assoc ℓ _ _} ⟩
cast₂
(subst Term (+-assoc ℓ _ _) (wk[ ℓ + m₁ ] (var x))
[ σ ⇑[ ℓ ] ]) ≡⟨ cong cast₂ $ cong _[ _ ] $ wk[]-comp ℓ ⟩
cast₂ (wk[ ℓ ] (wk[ m₁ ] (var x)) [ σ ⇑[ ℓ ] ]) ≡⟨ cong cast₂ $ wk[]-⇑[] ℓ ⟩
cast₂ (wk[ ℓ ] (wk[ m₁ ] (var x) [ σ ])) ≡⟨ cong cast₂ $ cong wk[ ℓ ] $ hyp _ ⟩
cast₂ (wk[ ℓ ] (wk[ m₂ ] (var x))) ≡⟨ swap-subst $ wk[]-comp ℓ ⟩
wk[ ℓ + m₂ ] (var x) ≡⟨ wk[]≡[] (ℓ + _) ⟩
var x [ wkSubst (ℓ + m₂) idSubst ] ≡⟨⟩
wkSubst (ℓ + m₂) idSubst x ∎
opaque
[][]↑-[₀⇑] :
∀ ℓ {u} (t : Term[ k ] (1+ n)) →
let cast =
subst₂ Subst (sym $ +-assoc ℓ m n) (sym $ +-assoc ℓ (1+ m) n)
in
t [ ℓ + 1+ m ][ u ]↑ [ cast (sgSubst v ⇑[ ℓ ]) ] ≡
t [ ℓ + m ][ u [ cast (sgSubst v ⇑[ ℓ ]) ] ]↑
[][]↑-[₀⇑] {m} {v} _ t =
[][]↑-commutes-+ t λ x →
wk[ 1+ m ] (var x) [ v ]₀ ≡⟨⟩
wk1 (wk[ m ] (var x)) [ v ]₀ ≡⟨ wk1-sgSubst _ _ ⟩
wk[ m ] (var x) ∎
private opaque
_ :
(t : Term[ k ] (1+ m)) →
t [ 1+ n ][ u ]↑ [ v ]₀ ≡
t [ n ][ u [ v ]₀ ]↑
_ = [][]↑-[₀⇑] 0
opaque
[][]↑-[,⇑] :
∀ ℓ {u} (t : Term[ k ] (1+ n)) →
let cast =
subst₂ Subst (sym $ +-assoc ℓ m n) (sym $ +-assoc ℓ (2+ m) n)
in
t [ ℓ + 2+ m ][ u ]↑ [ cast (consSubst (sgSubst v) w ⇑[ ℓ ]) ] ≡
t [ ℓ + m ][ u [ cast (consSubst (sgSubst v) w ⇑[ ℓ ]) ] ]↑
[][]↑-[,⇑] {m} {v} {w} _ t =
[][]↑-commutes-+ t λ x →
wk[ 2+ m ] (var x) [ v , w ]₁₀ ≡⟨ wk2-[,] ⟩
wk[ m ] (var x) ∎
private opaque
_ :
(t : Term[ k ] (1+ m)) →
t [ 2+ n ][ u ]↑ [ v , w ]₁₀ ≡
t [ n ][ u [ v , w ]₁₀ ]↑
_ = [][]↑-[,⇑] 0
opaque
[][]↑-[,,⇑] :
∀ ℓ {u} (t : Term[ k ] (1+ n)) →
let cast =
subst₂ Subst (sym $ +-assoc ℓ m n) (sym $ +-assoc ℓ (3+ m) n)
in
t [ ℓ + 3+ m ][ u ]↑
[ cast (consSubst (consSubst (sgSubst v₁) v₂) v₃ ⇑[ ℓ ]) ] ≡
t [ ℓ + m ][
u [ cast (consSubst (consSubst (sgSubst v₁) v₂) v₃ ⇑[ ℓ ]) ] ]↑
[][]↑-[,,⇑] {m} {v₁} {v₂} {v₃} _ t =
[][]↑-commutes-+ t λ x →
wk[ 3+ m ] (var x) [ v₁ , v₂ , v₃ ]₂₁₀ ≡⟨ wk[]-tail {t = wk[ m ] _} 3 ⟩
wk[ m ] (var x) [ idSubst ] ≡⟨ subst-id _ ⟩
wk[ m ] (var x) ∎
private opaque
_ :
(t : Term[ k ] (1+ m)) →
t [ 3+ n ][ u ]↑ [ v₁ , v₂ , v₃ ]₂₁₀ ≡
t [ n ][ u [ v₁ , v₂ , v₃ ]₂₁₀ ]↑
_ = [][]↑-[,,⇑] 0
opaque
[][]↑-[↑⇑] :
∀ ℓ {u} (t : Term[ k ] (1+ n)) →
let σ = wk1Subst idSubst
cast =
subst₂ Subst (sym $ +-assoc ℓ (1+ m) n)
(sym $ +-assoc ℓ (1+ m) n)
in
t [ ℓ + 1+ m ][ u ]↑ [ cast (consSubst σ v ⇑[ ℓ ]) ] ≡
t [ ℓ + 1+ m ][ u [ cast (consSubst σ v ⇑[ ℓ ]) ] ]↑
[][]↑-[↑⇑] {m} {v} _ t =
[][]↑-commutes-+ t λ x →
wk[ 1+ m ] (var x) [ consSubst (wk1Subst idSubst) v ] ≡⟨ wk1-tail (wk[ m ] _) ⟩
wk[ m ] (var x) [ wk1Subst idSubst ] ≡˘⟨ wk[]≡[] 1 ⟩
wk[ 1+ m ] (var x) ∎
private opaque
_ :
(t : Term[ k ] (1+ m)) →
t [ 1+ n ][ u ]↑ [ v ]↑ ≡
t [ 1+ n ][ u [ v ]↑ ]↑
_ = [][]↑-[↑⇑] 0
opaque
[][wk[]′]↑ :
(t : Term[ k ] (1+ m)) →
t [ n ][ wk[ n ]′ u ]↑ ≡ wk[ n ]′ (t [ u ]₀)
[][wk[]′]↑ {n} {u} t =
t [ n ][ wk[ n ]′ u ]↑ ≡⟨ [][]↑≡ t ⟩
wk (lift (stepn id n)) t [ wk[ n ]′ u ]₀ ≡˘⟨ wk-β t ⟩
wk[ n ]′ (t [ u ]₀) ∎
opaque
wk[]′[][]↑ :
∀ ℓ →
let cast = λ {k} → subst Term[ k ] (sym $ +-assoc ℓ m n) in
(t : Term[ k ] (1+ n)) →
cast (wk[ ℓ ]′ (t [ m ][ u ]↑)) ≡
t [ ℓ + m ][ cast (wk[ ℓ ]′ u) ]↑
wk[]′[][]↑ {m} {n} {u} ℓ t =
cast (wk[ ℓ ]′ (t [ consSubst (wkSubst m idSubst) u ])) ≡⟨ cong cast $ wk-subst t ⟩
cast (t [ stepn id ℓ •ₛ consSubst (wkSubst m idSubst) u ]) ≡⟨ lemma₁ ⟩
t [ cast ∘→ (stepn id ℓ •ₛ consSubst (wkSubst m idSubst) u) ] ≡⟨ (flip substVar-to-subst t λ where
x0 → refl
(_ +1) → lemma₂ _) ⟩
t [ consSubst (wkSubst (ℓ + m) idSubst) (cast (wk[ ℓ ]′ u)) ] ∎
where
cast : Term[ k ] (ℓ + (m + n)) → Term[ k ] ((ℓ + m) + n)
cast = subst Term[ _ ] (sym $ +-assoc ℓ m n)
lemma₁ : cast (t [ σ ]) ≡ t [ cast ∘→ σ ]
lemma₁ rewrite +-assoc ℓ m n = refl
lemma₂ :
∀ x →
cast (wk[ ℓ ]′ (wkSubst m idSubst x)) ≡ wkSubst (ℓ + m) idSubst x
lemma₂ x =
cast (wk[ ℓ ]′ (wkSubst m idSubst x)) ≡˘⟨ cong cast wk[]≡wk[]′ ⟩
cast (wk[ ℓ ] (wkSubst m idSubst x)) ≡⟨ cong cast $ wk[]≡wkSubst ℓ _ ⟩
cast (wkSubst ℓ (wkSubst m idSubst) x) ≡⟨ swap-subst $ wkSubst-comp ℓ _ ⟩
wkSubst (ℓ + m) idSubst x ∎
private opaque
_ :
(t : Term[ k ] (1+ m)) →
wk1 (t [ n ][ u ]↑) ≡ t [ 1+ n ][ wk1 u ]↑
_ = wk[]′[][]↑ 1
opaque
wk1-[][]↑ : ∀ n {u} → wk1 t [ n ][ u ]↑ ≡ wk[ n ] t
wk1-[][]↑ {t} n {u} =
wk1 t [ consSubst (wkSubst n idSubst) u ] ≡⟨ subst-wk t ⟩
t [ consSubst (wkSubst n idSubst) u ₛ• step id ] ≡⟨⟩
t [ wkSubst n idSubst ] ≡˘⟨ wk[]≡[] n ⟩
wk[ n ] t ∎
opaque
wk1-[][]↑′ : wk1 t [ n ][ u ]↑ ≡ wk[ n ]′ t
wk1-[][]↑′ {t} {n} {u} =
wk1 t [ n ][ u ]↑ ≡⟨ wk1-[][]↑ n ⟩
wk[ n ] t ≡⟨ wk[]≡wk[]′ ⟩
wk[ n ]′ t ∎
≡+1++ : ∀ m n o → 1+ m + (n + o) ≡ m + 1+ n + o
≡+1++ 0 _ _ = refl
≡+1++ (1+ m) n o = cong 1+ (≡+1++ m n o)
opaque
[+][var]↑ :
∀ {t : Term[ k ] (1+ o)} m →
t [ m + 1+ n ][ subst Term (≡+1++ m n o) (var (fromℕ m)) ]↑ ≡
subst Term[ k ] (sym (+-assoc m (1+ n) o))
(wk (stepn (lift (stepn id n)) m) t)
[+][var]↑ {k} {o} {n} {t} 0 =
t [ 1+ n ][ var x0 ]↑ ≡⟨ [][]↑≡ t ⟩
wk (lift (stepn id (1+ n))) t [ var x0 ]₀ ≡⟨ subst-wk t ⟩
t [ sgSubst (var x0) ₛ• lift (stepn id (1+ n)) ] ≡⟨ (flip substVar-to-subst t λ where
x0 → refl
(_ +1) → refl) ⟩
t [ toSubst (lift (stepn id n)) ] ≡˘⟨ wk≡subst _ _ ⟩
wk (lift (stepn id n)) t ∎
[+][var]↑ {k} {o} {n} {t} (1+ m) =
t [ 1+ m + 1+ n ][
subst Term (cong 1+ (≡+1++ m n o)) (wk1 (var (fromℕ m))) ]↑ ≡⟨ cong (t [ _ ][_]↑) (subst-cong-1+-wk1 (≡+1++ m _ _)) ⟩
t [ 1+ m + 1+ n ][ wk1 (subst Term (≡+1++ m n o) (var (fromℕ m))) ]↑ ≡˘⟨ wk[]′[][]↑ 1 t ⟩
wk1
(t [ m + 1+ n ][ subst Term (≡+1++ m n o) (var (fromℕ m)) ]↑) ≡⟨ cong wk1 ([+][var]↑ m) ⟩
wk1
(subst Term[ k ] (sym (+-assoc m (1+ n) o))
(wk (stepn (lift (stepn id n)) m) t)) ≡˘⟨ subst-cong-1+-wk1 (sym (+-assoc m _ _)) ⟩
subst Term[ k ] (cong 1+ (sym (+-assoc m (1+ n) o)))
(wk1 (wk (stepn (lift (stepn id n)) m) t)) ≡⟨ cong₂ (subst Term[ _ ]) (cong-sym (+-assoc m _ _))
(wk-comp (step id) _ _) ⟩
subst Term[ k ] (sym (+-assoc (1+ m) (1+ n) o))
(wk (stepn (lift (stepn id n)) (1+ m)) t) ∎
opaque
_ : t [ 1+ n ][ var x0 ]↑ ≡ wk (lift (stepn id n)) t
_ = [+][var]↑ 0
opaque
[0]↑ : t [ var x0 ]↑ ≡ t
[0]↑ {t} =
t [ var x0 ]↑ ≡⟨ [+][var]↑ 0 ⟩
wk (lift id) t ≡⟨ wk-lift-id _ ⟩
t ∎
opaque
[][var]↑ :
(t : Term[ k ] (1+ n)) →
t [ 1+ m ][ var (fromℕ m) ]↑ ≡
subst Term[ k ] (+-suc m n) (wk[ m ]′ t)
[][var]↑ {m = 0} t =
t [ var x0 ]↑ ≡⟨ [][]↑≡ t ⟩
wk (lift (step id)) t [ var x0 ]₀ ≡⟨ wkSingleSubstId _ ⟩
t ≡⟨ wk[]≡wk[]′ ⟩
wk[ 0 ]′ t ∎
[][var]↑ {k} {n} {m = 1+ m} t =
t [ 2+ m ][ var (fromℕ m +1) ]↑ ≡⟨ sym (wk[]′[][]↑ 1 t) ⟩
wk1 (t [ 1+ m ][ var (fromℕ m) ]↑) ≡⟨ cong wk1 ([][var]↑ t) ⟩
wk1 (subst Term[ k ] (+-suc m n) (wk[ m ]′ t)) ≡˘⟨ subst-cong-1+-wk1 (+-suc m _) ⟩
subst Term[ k ] (cong 1+ (+-suc m n)) (wk1 (wk[ m ]′ t)) ≡⟨ cong (subst _ (cong _ (+-suc m _))) (wk-comp _ _ _) ⟩
subst Term[ k ] (cong 1+ (+-suc m n)) (wk[ 1+ m ]′ t) ∎
_ : (t : Term[ k ] (1+ n)) → t [ var x1 ]↑² ≡ wk1 t
_ = [][var]↑
opaque
unfolding replace₂
wk[2+]′-[replace₂] :
wk[ 2+ n ]′ t [ replace₂ u v ] ≡ wk[ 2+ n ]′ t
wk[2+]′-[replace₂] {n} {t} {u} {v} =
wk[ 2+ n ]′ t [ replace₂ u v ] ≡⟨ subst-wk t ⟩
t [ replace₂ u v ₛ• stepn id (2+ n) ] ≡⟨⟩
t [ toSubst (stepn id (2+ n)) ] ≡˘⟨ wk≡subst _ _ ⟩
wk[ 2+ n ]′ t ∎
opaque
wk[2+]-[replace₂] :
wk[ 2+ n ] t [ replace₂ u v ] ≡ wk[ 2+ n ] t
wk[2+]-[replace₂] {n} {t} {u} {v} =
wk[ 2+ n ] t [ replace₂ u v ] ≡⟨ PE.cong _[ _ ] $ wk[]≡wk[]′ {n = 2+ n} ⟩
wk[ 2+ n ]′ t [ replace₂ u v ] ≡⟨ wk[2+]′-[replace₂] ⟩
wk[ 2+ n ]′ t ≡˘⟨ wk[]≡wk[]′ ⟩
wk[ 2+ n ] t ∎
opaque
unfolding replace₂
[replace₂]-[⇑] :
(t : Term[ k ] (2+ m + n₂)) (σ : Subst n₁ n₂) →
let σ⇑ = σ ⇑[ 2 + m ] in
t [ replace₂ u v ] [ σ⇑ ] ≡
t [ σ⇑ ] [ replace₂ (u [ σ⇑ ]) (v [ σ⇑ ]) ]
[replace₂]-[⇑] {m} {u} {v} t σ =
let σ⇑ = σ ⇑[ 2 + m ] in
t [ replace₂ u v ] [ σ⇑ ] ≡⟨ substCompEq t ⟩
t [ σ⇑ ₛ•ₛ replace₂ u v ] ≡⟨ (flip substVar-to-subst t λ where
x0 → PE.refl
(x0 +1) → PE.refl
(_ +1 +1) → PE.sym $ wk[2+]-[replace₂] {n = 0}) ⟩
t [ replace₂ (u [ σ⇑ ]) (v [ σ⇑ ]) ₛ•ₛ σ⇑ ] ≡˘⟨ substCompEq t ⟩
t [ σ⇑ ] [ replace₂ (u [ σ⇑ ]) (v [ σ⇑ ]) ] ∎
opaque
unfolding replace₂
[replace₂]-[,]₁₀ :
(t : Term[ k ] (2+ n)) →
t [ replace₂ u₁ u₂ ] [ v₁ , v₂ ]₁₀ ≡
t [ u₁ [ v₁ , v₂ ]₁₀ , u₂ [ v₁ , v₂ ]₁₀ ]₁₀
[replace₂]-[,]₁₀ t =
trans (substCompEq t) $
flip substVar-to-subst t λ where
x0 → refl
(x0 +1) → refl
(_ +1 +1) → refl
opaque
unfolding replace₂
[2][]↑-[replace₂] :
(t : Term[ k ] (1+ n)) →
t [ 2 ][ u ]↑ [ replace₂ v₁ v₂ ] ≡
t [ u [ replace₂ v₁ v₂ ] ]↑²
[2][]↑-[replace₂] t =
PE.trans (substCompEq t) $
flip substVar-to-subst t λ where
x0 → refl
(_ +1) → refl
opaque
isNumeral? : (t : Term n) → Dec (Numeral t)
isNumeral? zero = yes zeroₙ
isNumeral? (suc t) =
case isNumeral? t of λ where
(yes n) → yes (sucₙ n)
(no ¬n) → no (λ { (sucₙ n) → ¬n n})
isNumeral? (var x) = no (λ ())
isNumeral? (defn α) = no (λ ())
isNumeral? Level = no (λ ())
isNumeral? zeroᵘ = no (λ ())
isNumeral? (sucᵘ _) = no (λ ())
isNumeral? (_ supᵘ _) = no (λ ())
isNumeral? (U n) = no (λ ())
isNumeral? (Lift _ _) = no λ ()
isNumeral? (lift _) = no λ ()
isNumeral? (lower _) = no λ ()
isNumeral? ℕ = no λ ()
isNumeral? Empty = no λ ()
isNumeral? Unit! = no λ ()
isNumeral? (ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _) = no λ ()
isNumeral? (Id _ _ _) = no λ ()
isNumeral? (lam _ _) = no λ ()
isNumeral? (_ ∘ _) = no λ ()
isNumeral? (prod! _ _) = no λ ()
isNumeral? (fst _ _) = no λ ()
isNumeral? (snd _ _) = no λ ()
isNumeral? (prodrec _ _ _ _ _ _) = no λ ()
isNumeral? (natrec _ _ _ _ _ _ _) = no λ ()
isNumeral? star! = no λ ()
isNumeral? (unitrec _ _ _ _ _) = no λ ()
isNumeral? (emptyrec _ _ _) = no λ ()
isNumeral? rfl = no λ ()
isNumeral? (J _ _ _ _ _ _ _ _) = no λ ()
isNumeral? (K _ _ _ _ _ _) = no λ ()
isNumeral? ([]-cong! _ _ _ _ _) = no λ ()
isNumeral? (Quot _ _) = no λ ()
isNumeral? (class _) = no λ ()
isNumeral? (resp _ _ _ _ _) = no λ ()
isNumeral? (set _ _ _ _ _ _) = no λ ()
isNumeral? (qrec _ _ _ _ _) = no λ ()
opaque
wk-numeral : Numeral t → Numeral (wk ρ t)
wk-numeral zeroₙ = zeroₙ
wk-numeral (sucₙ n) = sucₙ (wk-numeral n)
opaque
subst-numeral : Numeral t → t [ σ ] ≡ t
subst-numeral zeroₙ = refl
subst-numeral (sucₙ n) = cong suc (subst-numeral n)
opaque
sucⁿ-Numeral : ∀ k → Numeral (sucⁿ {n} k)
sucⁿ-Numeral 0 = zeroₙ
sucⁿ-Numeral (1+ k) = sucₙ (sucⁿ-Numeral k)
opaque
Numeral→sucⁿ : Numeral t → ∃ λ k → t ≡ sucⁿ k
Numeral→sucⁿ zeroₙ = 0 , refl
Numeral→sucⁿ (sucₙ n) =
case (Numeral→sucⁿ n) of
λ (k , t≡) →
1+ k , cong suc t≡
opaque
subst-sucⁿ : ∀ k → sucⁿ k [ σ ] ≡ sucⁿ k
subst-sucⁿ 0 = refl
subst-sucⁿ (1+ k) = cong suc (subst-sucⁿ k)
opaque
wk-sucⁿ : ∀ k → wk ρ (sucⁿ k) ≡ sucⁿ k
wk-sucⁿ 0 = refl
wk-sucⁿ (1+ k) = cong suc (wk-sucⁿ k)
U-PE-injectivity : U l₁ PE.≡ U l₂ → l₁ PE.≡ l₂
U-PE-injectivity PE.refl = PE.refl
Lift-PE-injectivity :
Lift l₁ A₁ PE.≡ Lift l₂ A₂ → l₁ PE.≡ l₂ × A₁ PE.≡ A₂
Lift-PE-injectivity PE.refl = PE.refl , PE.refl
sucᵘ-PE-injectivity : Term[_].sucᵘ t₁ PE.≡ sucᵘ t₂ → t₁ PE.≡ t₂
sucᵘ-PE-injectivity PE.refl = PE.refl
supᵘ-PE-injectivity : t₁ supᵘ u₁ PE.≡ t₂ supᵘ u₂ → t₁ PE.≡ t₂ × u₁ PE.≡ u₂
supᵘ-PE-injectivity PE.refl = PE.refl , PE.refl
ωᵘ+-PE-injectivity : Term[_].ωᵘ+ {n = n} m₁ PE.≡ ωᵘ+ m₂ → m₁ PE.≡ m₂
ωᵘ+-PE-injectivity PE.refl = PE.refl
level-PE-injectivity : Term[_].level t₁ PE.≡ level t₂ → t₁ PE.≡ t₂
level-PE-injectivity PE.refl = PE.refl
BΠ-PE-injectivity : BM BMΠ p₁ q₁ PE.≡ BM BMΠ p₂ q₂ → p₁ PE.≡ p₂ × q₁ PE.≡ q₂
BΠ-PE-injectivity PE.refl = PE.refl , PE.refl
BΣ-PE-injectivity :
BM (BMΣ s₁) p₁ q₁ PE.≡ BM (BMΣ s₂) p₂ q₂ → p₁ PE.≡ p₂ × q₁ PE.≡ q₂ × s₁ PE.≡ s₂
BΣ-PE-injectivity PE.refl = PE.refl , PE.refl , PE.refl
var-PE-injectivity : Term[_].var {n = n} x₁ PE.≡ var x₂ → x₁ PE.≡ x₂
var-PE-injectivity PE.refl = PE.refl
defn-PE-injectivity : Term[_].defn {n = n} α PE.≡ defn β → α PE.≡ β
defn-PE-injectivity PE.refl = PE.refl
ΠΣ-PE-injectivity :
ΠΣ⟨ b₁ ⟩ p₁ , q₁ ▷ A₁ ▹ B₁ PE.≡ ΠΣ⟨ b₂ ⟩ p₂ , q₂ ▷ A₂ ▹ B₂ →
b₁ PE.≡ b₂ × p₁ PE.≡ p₂ × q₁ PE.≡ q₂ × A₁ PE.≡ A₂ × B₁ PE.≡ B₂
ΠΣ-PE-injectivity PE.refl =
PE.refl , PE.refl , PE.refl , PE.refl , PE.refl
B-PE-injectivity :
∀ W₁ W₂ → ⟦ W₁ ⟧ A₁ ▹ B₁ PE.≡ ⟦ W₂ ⟧ A₂ ▹ B₂ →
A₁ PE.≡ A₂ × B₁ PE.≡ B₂ × W₁ PE.≡ W₂
B-PE-injectivity (BM _ _ _) (BM _ _ _) PE.refl =
PE.refl , PE.refl , PE.refl
∘-PE-injectivity :
t₁ ∘⟨ p₁ ⟩ u₁ PE.≡ t₂ ∘⟨ p₂ ⟩ u₂ →
p₁ PE.≡ p₂ × t₁ PE.≡ t₂ × u₁ PE.≡ u₂
∘-PE-injectivity PE.refl = PE.refl , PE.refl , PE.refl
lam-PE-injectivity :
lam p₁ t₁ PE.≡ lam p₂ t₂ →
p₁ PE.≡ p₂ × t₁ PE.≡ t₂
lam-PE-injectivity PE.refl = PE.refl , PE.refl
prod-PE-injectivity :
prod s₁ p₁ t₁ u₁ PE.≡ prod s₂ p₂ t₂ u₂ →
s₁ PE.≡ s₂ × p₁ PE.≡ p₂ × t₁ PE.≡ t₂ × u₁ PE.≡ u₂
prod-PE-injectivity PE.refl = PE.refl , PE.refl , PE.refl , PE.refl
prodrec-PE-injectivity :
prodrec r₁ p₁ q₁ A₁ t₁ u₁ PE.≡ prodrec r₂ p₂ q₂ A₂ t₂ u₂ →
r₁ PE.≡ r₂ × p₁ PE.≡ p₂ × q₁ PE.≡ q₂ × A₁ PE.≡ A₂ × t₁ PE.≡ t₂ ×
u₁ PE.≡ u₂
prodrec-PE-injectivity PE.refl =
PE.refl , PE.refl , PE.refl , PE.refl , PE.refl , PE.refl
emptyrec-PE-injectivity :
emptyrec p₁ A₁ t₁ PE.≡ emptyrec p₂ A₂ t₂ →
p₁ PE.≡ p₂ × A₁ PE.≡ A₂ × t₁ PE.≡ t₂
emptyrec-PE-injectivity PE.refl = PE.refl , PE.refl , PE.refl
Unit-PE-injectivity :
_≡_ {A = Term n} (Unit s₁) (Unit s₂) →
s₁ ≡ s₂
Unit-PE-injectivity refl = refl
star-PE-injectivity :
_≡_ {A = Term n} (star s₁) (star s₂) → s₁ PE.≡ s₂
star-PE-injectivity PE.refl = PE.refl
unitrec-PE-injectivity :
unitrec p₁ q₁ A₁ t₁ u₁ PE.≡ unitrec p₂ q₂ A₂ t₂ u₂ →
p₁ PE.≡ p₂ × q₁ PE.≡ q₂ × A₁ PE.≡ A₂ × t₁ PE.≡ t₂ ×
u₁ PE.≡ u₂
unitrec-PE-injectivity PE.refl =
PE.refl , PE.refl , PE.refl , PE.refl , PE.refl
suc-PE-injectivity : suc t₁ PE.≡ suc t₂ → t₁ PE.≡ t₂
suc-PE-injectivity PE.refl = PE.refl
opaque
sucⁿ-PE-injectivity : sucⁿ {n = n} n₁ ≡ sucⁿ n₂ → n₁ ≡ n₂
sucⁿ-PE-injectivity {n₁ = 0} {n₂ = 0} _ = refl
sucⁿ-PE-injectivity {n₁ = 0} {n₂ = 1+ _} ()
sucⁿ-PE-injectivity {n₁ = 1+ _} {n₂ = 0} ()
sucⁿ-PE-injectivity {n₁ = 1+ _} {n₂ = 1+ _} eq =
cong 1+ (sucⁿ-PE-injectivity (suc-PE-injectivity eq))
natrec-PE-injectivity :
natrec p₁ q₁ r₁ A₁ t₁ u₁ v₁ PE.≡ natrec p₂ q₂ r₂ A₂ t₂ u₂ v₂ →
p₁ PE.≡ p₂ × q₁ PE.≡ q₂ × r₁ PE.≡ r₂ × A₁ PE.≡ A₂ × t₁ PE.≡ t₂ ×
u₁ PE.≡ u₂ × v₁ PE.≡ v₂
natrec-PE-injectivity PE.refl =
PE.refl , PE.refl , PE.refl , PE.refl , PE.refl , PE.refl , PE.refl
Id-PE-injectivity :
Id A₁ t₁ u₁ PE.≡ Id A₂ t₂ u₂ →
A₁ PE.≡ A₂ × t₁ PE.≡ t₂ × u₁ PE.≡ u₂
Id-PE-injectivity PE.refl = PE.refl , PE.refl , PE.refl
J-PE-injectivity :
J p₁ q₁ A₁ t₁ B₁ u₁ v₁ w₁ PE.≡ J p₂ q₂ A₂ t₂ B₂ u₂ v₂ w₂ →
p₁ PE.≡ p₂ × q₁ PE.≡ q₂ × A₁ PE.≡ A₂ × t₁ PE.≡ t₂ × B₁ PE.≡ B₂ ×
u₁ PE.≡ u₂ × v₁ PE.≡ v₂ × w₁ PE.≡ w₂
J-PE-injectivity PE.refl =
PE.refl , PE.refl , PE.refl , PE.refl , PE.refl , PE.refl ,
PE.refl , PE.refl
K-PE-injectivity :
K p₁ A₁ t₁ B₁ u₁ v₁ PE.≡ K p₂ A₂ t₂ B₂ u₂ v₂ →
p₁ PE.≡ p₂ × A₁ PE.≡ A₂ × t₁ PE.≡ t₂ × B₁ PE.≡ B₂ × u₁ PE.≡ u₂ ×
v₁ PE.≡ v₂
K-PE-injectivity PE.refl =
PE.refl , PE.refl , PE.refl , PE.refl , PE.refl , PE.refl
[]-cong-PE-injectivity :
[]-cong s₁ l₁ A₁ t₁ u₁ v₁ PE.≡ []-cong s₂ l₂ A₂ t₂ u₂ v₂ →
s₁ PE.≡ s₂ × l₁ PE.≡ l₂ × A₁ PE.≡ A₂ × t₁ PE.≡ t₂ × u₁ PE.≡ u₂ ×
v₁ PE.≡ v₂
[]-cong-PE-injectivity PE.refl =
PE.refl , PE.refl , PE.refl , PE.refl , PE.refl , PE.refl
Quot-PE-injectivity :
Quot A₁ B₁ ≡ Quot A₂ B₂ →
A₁ ≡ A₂ × B₁ ≡ B₂
Quot-PE-injectivity refl = refl , refl
class-PE-injectivity : class t₁ ≡ class t₂ → t₁ ≡ t₂
class-PE-injectivity refl = refl
resp-PE-injectivity :
resp A₁ B₁ t₁ u₁ v₁ ≡ resp A₂ B₂ t₂ u₂ v₂ →
A₁ ≡ A₂ × B₁ ≡ B₂ × t₁ ≡ t₂ × u₁ ≡ u₂ × v₁ ≡ v₂
resp-PE-injectivity refl = refl , refl , refl , refl , refl
set-PE-injectivity :
set A₁ B₁ t₁ u₁ v₁ w₁ ≡ set A₂ B₂ t₂ u₂ v₂ w₂ →
A₁ ≡ A₂ × B₁ ≡ B₂ × t₁ ≡ t₂ × u₁ ≡ u₂ × v₁ ≡ v₂ × w₁ ≡ w₂
set-PE-injectivity refl = refl , refl , refl , refl , refl , refl
qrec-PE-injectivity :
qrec C₁ t₁ u₁ v₁ w₁ ≡ qrec C₂ t₂ u₂ v₂ w₂ →
C₁ ≡ C₂ × t₁ ≡ t₂ × u₁ ≡ u₂ × v₁ ≡ v₂ × w₁ ≡ w₂
qrec-PE-injectivity refl = refl , refl , refl , refl , refl
opaque
unfolding inline-Con
or-empty-inline-Con :
{A : Set a} ⦃ ok : A or-empty Γ ⦄ →
A or-empty inline-Con ξ Γ
or-empty-inline-Con ⦃ ok = ε ⦄ = ε
or-empty-inline-Con ⦃ ok = possibly-nonempty ⦄ = possibly-nonempty
opaque
unfolding inline-Conᵈ
or-empty-inline-Conᵈ :
{A : Set a} ⦃ ok : A or-empty Γ ⦄ →
A or-empty inline-Conᵈ ∇ Γ
or-empty-inline-Conᵈ = or-empty-inline-Con
opaque
unfolding inline-Nat
inline-Nat-id :
{eq : m ≡ n} →
inline-Nat (id eq) α ≡ defn α
inline-Nat-id {m} {α} {eq = refl} with m ≤? α
… | no _ = refl
… | yes m≤α with α <′? m
… | no _ = refl
… | yes α<m = ⊥-elim (n≮n _ (≤-trans (<′⇒< α<m) m≤α))
opaque
unfolding inline
inline-id : (t : Term[ k ] n) → inline (id eq) t ≡ t
inline-id (var _) =
refl
inline-id {eq} (defn _) =
PE.cong (wk _) (inline-Nat-id {eq = eq})
inline-id Level =
refl
inline-id zeroᵘ =
refl
inline-id (sucᵘ t) =
cong sucᵘ (inline-id t)
inline-id (t supᵘ u) =
cong₂ _supᵘ_ (inline-id t) (inline-id u)
inline-id (ωᵘ+ _) =
refl
inline-id (level t) =
cong level (inline-id t)
inline-id (U l) =
cong U (inline-id l)
inline-id (Lift l A) =
cong₂ Lift (inline-id l) (inline-id A)
inline-id (lift t) =
cong lift (inline-id t)
inline-id (lower t) =
cong lower (inline-id t)
inline-id Empty =
refl
inline-id (emptyrec p A t) =
cong₂ (emptyrec _) (inline-id A) (inline-id t)
inline-id (Unit _) =
refl
inline-id (star _) =
refl
inline-id (unitrec _ _ A t u) =
cong₃ (unitrec _ _) (inline-id A) (inline-id t) (inline-id u)
inline-id (ΠΣ⟨ _ ⟩ _ , _ ▷ A ▹ B) =
cong₂ (ΠΣ⟨ _ ⟩ _ , _ ▷_▹_) (inline-id A) (inline-id B)
inline-id (lam p t) =
cong (lam _) (inline-id t)
inline-id (t ∘⟨ p ⟩ u) =
cong₂ (_∘⟨ _ ⟩_) (inline-id t) (inline-id u)
inline-id (prod s p t u) =
cong₂ (prod _ _) (inline-id t) (inline-id u)
inline-id (fst p t) =
cong (fst _) (inline-id t)
inline-id (snd p t) =
cong (snd _) (inline-id t)
inline-id (prodrec r p q A t u) =
cong₃ (prodrec _ _ _) (inline-id A) (inline-id t) (inline-id u)
inline-id ℕ =
refl
inline-id zero =
refl
inline-id (suc t) =
cong suc (inline-id t)
inline-id (natrec p q r A t u v) =
cong₄ (natrec _ _ _) (inline-id A) (inline-id t) (inline-id u)
(inline-id v)
inline-id (Id A t u) =
cong₃ Id (inline-id A) (inline-id t) (inline-id u)
inline-id rfl =
refl
inline-id (J p q A t B u v w) =
cong₆ (J _ _) (inline-id A) (inline-id t) (inline-id B)
(inline-id u) (inline-id v) (inline-id w)
inline-id (K p A t B u v) =
cong₅ (K _) (inline-id A) (inline-id t) (inline-id B) (inline-id u)
(inline-id v)
inline-id ([]-cong _ l A t u v) =
cong₅ ([]-cong _) (inline-id l) (inline-id A) (inline-id t)
(inline-id u) (inline-id v)
inline-id (Quot A B) =
cong₂ Quot (inline-id A) (inline-id B)
inline-id (class t) =
cong class (inline-id t)
inline-id (resp A B t u v) =
cong₅ resp (inline-id A) (inline-id B) (inline-id t) (inline-id u)
(inline-id v)
inline-id (set A B t u v w) =
cong₆ set (inline-id A) (inline-id B) (inline-id t) (inline-id u)
(inline-id v) (inline-id w)
inline-id (qrec C t u v w) =
cong₅ qrec (inline-id C) (inline-id t) (inline-id u) (inline-id v)
(inline-id w)
opaque
unfolding inline-Con
inline-Con-id :
(Γ : Con Term m) → inline-Con {m₂ = n} idᵉ Γ ≡ Γ
inline-Con-id ε = refl
inline-Con-id (_ ∙ _) = cong₂ _∙_ (inline-Con-id _) (inline-id _)
opaque
unfolding inline
wk-inline : (t : Term[ k ] n) → wk ρ (inline ξ t) ≡ inline ξ (wk ρ t)
wk-inline (var _) =
refl
wk-inline (defn _) =
wk₀-comp _ _
wk-inline Level =
refl
wk-inline zeroᵘ =
refl
wk-inline (sucᵘ t) =
cong sucᵘ (wk-inline t)
wk-inline (t supᵘ u) =
cong₂ _supᵘ_ (wk-inline t) (wk-inline u)
wk-inline (ωᵘ+ _) =
refl
wk-inline (level t) =
cong level (wk-inline t)
wk-inline (U l) =
cong U (wk-inline l)
wk-inline (Lift l A) =
cong₂ Lift (wk-inline l) (wk-inline A)
wk-inline (lift t) =
cong lift (wk-inline t)
wk-inline (lower t) =
cong lower (wk-inline t)
wk-inline Empty =
refl
wk-inline (emptyrec p A t) =
cong₂ (emptyrec _) (wk-inline A) (wk-inline t)
wk-inline (Unit _) =
refl
wk-inline (star _) =
refl
wk-inline (unitrec _ _ A t u) =
cong₃ (unitrec _ _) (wk-inline A) (wk-inline t) (wk-inline u)
wk-inline (ΠΣ⟨ _ ⟩ _ , _ ▷ A ▹ B) =
cong₂ (ΠΣ⟨ _ ⟩ _ , _ ▷_▹_) (wk-inline A) (wk-inline B)
wk-inline (lam p t) =
cong (lam _) (wk-inline t)
wk-inline (t ∘⟨ p ⟩ u) =
cong₂ (_∘⟨ _ ⟩_) (wk-inline t) (wk-inline u)
wk-inline (prod s p t u) =
cong₂ (prod _ _) (wk-inline t) (wk-inline u)
wk-inline (fst p t) =
cong (fst _) (wk-inline t)
wk-inline (snd p t) =
cong (snd _) (wk-inline t)
wk-inline (prodrec r p q A t u) =
cong₃ (prodrec _ _ _) (wk-inline A) (wk-inline t) (wk-inline u)
wk-inline ℕ =
refl
wk-inline zero =
refl
wk-inline (suc t) =
cong suc (wk-inline t)
wk-inline (natrec p q r A t u v) =
cong₄ (natrec _ _ _) (wk-inline A) (wk-inline t) (wk-inline u)
(wk-inline v)
wk-inline (Id A t u) =
cong₃ Id (wk-inline A) (wk-inline t) (wk-inline u)
wk-inline rfl =
refl
wk-inline (J p q A t B u v w) =
cong₆ (J _ _) (wk-inline A) (wk-inline t) (wk-inline B)
(wk-inline u) (wk-inline v) (wk-inline w)
wk-inline (K p A t B u v) =
cong₅ (K _) (wk-inline A) (wk-inline t) (wk-inline B) (wk-inline u)
(wk-inline v)
wk-inline ([]-cong _ l A t u v) =
cong₅ ([]-cong _) (wk-inline l) (wk-inline A) (wk-inline t)
(wk-inline u) (wk-inline v)
wk-inline (Quot A B) =
cong₂ Quot (wk-inline A) (wk-inline B)
wk-inline (class t) =
cong class (wk-inline t)
wk-inline (resp A B t u v) =
cong₅ resp (wk-inline A) (wk-inline B) (wk-inline t) (wk-inline u)
(wk-inline v)
wk-inline (set A B t u v w) =
cong₆ set (wk-inline A) (wk-inline B) (wk-inline t) (wk-inline u)
(wk-inline v) (wk-inline w)
wk-inline (qrec C t u v w) =
cong₅ qrec (wk-inline C) (wk-inline t) (wk-inline u) (wk-inline v)
(wk-inline w)
opaque
unfolding inline inline-Subst
inline-Subst-⇑ :
(x : Fin (1+ n)) →
inline-Subst ξ (σ ⇑) x ≡ (inline-Subst ξ σ ⇑) x
inline-Subst-⇑ x0 = refl
inline-Subst-⇑ {ξ} {σ} (x +1) =
inline ξ (wk1 (σ x)) ≡˘⟨ wk-inline (σ _) ⟩
wk1 (inline ξ (σ x)) ∎
opaque
inline-Subst-⇑[] :
∀ m (x : Fin (m + n)) →
inline-Subst ξ (σ ⇑[ m ]) x ≡ (inline-Subst ξ σ ⇑[ m ]) x
inline-Subst-⇑[] 0 _ = refl
inline-Subst-⇑[] {ξ} {σ} (1+ m) x =
inline-Subst ξ (σ ⇑[ m ] ⇑) x ≡⟨ inline-Subst-⇑ x ⟩
(inline-Subst ξ (σ ⇑[ m ]) ⇑) x ≡⟨ substVar-lift (inline-Subst-⇑[] m) x ⟩
(inline-Subst ξ σ ⇑[ m ] ⇑) x ∎
opaque
unfolding inline-Subst
inline-Subst-consSubst :
(x : Fin (1+ n)) →
inline-Subst ξ (consSubst σ t) x ≡
consSubst (inline-Subst ξ σ) (inline ξ t) x
inline-Subst-consSubst x0 = refl
inline-Subst-consSubst (_ +1) = refl
opaque
unfolding inline inline-Subst
inline-Subst-idSubst :
(x : Fin n) →
inline-Subst ξ idSubst x ≡ idSubst x
inline-Subst-idSubst _ = refl
opaque
inline-Subst-sgSubst :
(x : Fin (1+ n)) →
inline-Subst ξ (sgSubst t) x ≡
sgSubst (inline ξ t) x
inline-Subst-sgSubst {ξ} {t} x =
inline-Subst ξ (consSubst idSubst t) x ≡⟨ inline-Subst-consSubst x ⟩
consSubst (inline-Subst ξ idSubst) (inline ξ t) x ≡⟨ consSubst-cong refl inline-Subst-idSubst x ⟩
consSubst idSubst (inline ξ t) x ∎
opaque
unfolding inline-Subst
inline-Subst-wk1Subst :
(x : Fin (1+ n)) →
inline-Subst ξ (wk1Subst σ) x ≡
wk1Subst (inline-Subst ξ σ) x
inline-Subst-wk1Subst {σ} _ = sym $ wk-inline (σ _)
opaque
unfolding inline-Subst
inline-Subst-wkSubst :
∀ k (x : Fin n) →
inline-Subst ξ (wkSubst k σ) x ≡
wkSubst k (inline-Subst ξ σ) x
inline-Subst-wkSubst 0 _ =
refl
inline-Subst-wkSubst {ξ} {σ} (1+ k) x =
inline ξ (wk1 (wkSubst k σ x)) ≡˘⟨ wk-inline (wkSubst k _ _) ⟩
wk1 (inline-Subst ξ (wkSubst k σ) x) ≡⟨ cong wk1 $ inline-Subst-wkSubst k _ ⟩
wk1 (wkSubst k (inline-Subst ξ σ) x) ∎
opaque
unfolding inline inline-Subst
mutual
inline-[] :
(t : Term[ k ] n) →
inline ξ (t [ σ ]) ≡ inline ξ t [ inline-Subst ξ σ ]
inline-[] (var _) =
refl
inline-[] (defn _) =
sym wk-wk₀-[]≡
inline-[] Level =
refl
inline-[] zeroᵘ =
refl
inline-[] (sucᵘ t) =
cong sucᵘ (inline-[] t)
inline-[] (t supᵘ u) =
cong₂ _supᵘ_ (inline-[] t) (inline-[] u)
inline-[] (ωᵘ+ _) =
refl
inline-[] (level t) =
cong level (inline-[] t)
inline-[] (U l) =
cong U (inline-[] l)
inline-[] (Lift l A) =
cong₂ Lift (inline-[] l) (inline-[] A)
inline-[] (lift t) =
cong lift (inline-[] t)
inline-[] (lower t) =
cong lower (inline-[] t)
inline-[] Empty =
refl
inline-[] (emptyrec _ A t) =
cong₂ (emptyrec _) (inline-[] A) (inline-[] t)
inline-[] (Unit _) =
refl
inline-[] (star _) =
refl
inline-[] (unitrec _ _ A t u) =
cong₃ (unitrec _ _) (inline-[⇑] 1 A) (inline-[] t) (inline-[] u)
inline-[] (ΠΣ⟨ _ ⟩ _ , _ ▷ A ▹ B) =
cong₂ (ΠΣ⟨ _ ⟩ _ , _ ▷_▹_) (inline-[] A) (inline-[⇑] 1 B)
inline-[] (lam _ t) =
cong (lam _) (inline-[⇑] 1 t)
inline-[] (t ∘⟨ _ ⟩ u) =
cong₂ (_∘⟨ _ ⟩_) (inline-[] t) (inline-[] u)
inline-[] (prod _ _ t u) =
cong₂ (prod _ _) (inline-[] t) (inline-[] u)
inline-[] (fst _ t) =
cong (fst _) (inline-[] t)
inline-[] (snd _ t) =
cong (snd _) (inline-[] t)
inline-[] (prodrec _ _ _ A t u) =
cong₃ (prodrec _ _ _) (inline-[⇑] 1 A) (inline-[] t)
(inline-[⇑] 2 u)
inline-[] ℕ =
refl
inline-[] zero =
refl
inline-[] (suc t) =
cong suc (inline-[] t)
inline-[] (natrec _ _ _ A t u v) =
cong₄ (natrec _ _ _) (inline-[⇑] 1 A) (inline-[] t) (inline-[⇑] 2 u)
(inline-[] v)
inline-[] (Id A t u) =
cong₃ Id (inline-[] A) (inline-[] t) (inline-[] u)
inline-[] rfl =
refl
inline-[] (J _ _ A t B u v w) =
cong₆ (J _ _) (inline-[] A) (inline-[] t) (inline-[⇑] 2 B)
(inline-[] u) (inline-[] v) (inline-[] w)
inline-[] (K _ A t B u v) =
cong₅ (K _) (inline-[] A) (inline-[] t) (inline-[⇑] 1 B)
(inline-[] u) (inline-[] v)
inline-[] ([]-cong _ l A t u v) =
cong₅ ([]-cong _) (inline-[] l) (inline-[] A) (inline-[] t)
(inline-[] u) (inline-[] v)
inline-[] (Quot A B) =
cong₂ Quot (inline-[] A) (inline-[⇑] 2 B)
inline-[] (class t) =
cong class (inline-[] t)
inline-[] (resp A B t u v) =
cong₅ resp (inline-[] A) (inline-[⇑] 2 B) (inline-[] t)
(inline-[] u) (inline-[] v)
inline-[] (set A B t u v w) =
cong₆ set (inline-[] A) (inline-[⇑] 2 B) (inline-[] t) (inline-[] u)
(inline-[] v) (inline-[] w)
inline-[] (qrec C t u v w) =
cong₅ qrec (inline-[⇑] 1 C) (inline-[⇑] 1 t) (inline-[⇑] 3 u)
(inline-[⇑] 5 v) (inline-[] w)
inline-[⇑] :
∀ m (t : Term[ k ] (m + n)) →
inline ξ (t [ σ ⇑[ m ] ]) ≡
inline ξ t [ inline-Subst ξ σ ⇑[ m ] ]
inline-[⇑] {ξ} {σ} m t =
inline ξ (t [ σ ⇑[ m ] ]) ≡⟨ inline-[] t ⟩
inline ξ t [ inline-Subst ξ (σ ⇑[ m ]) ] ≡⟨ substVar-to-subst (inline-Subst-⇑[] m) (inline _ t) ⟩
inline ξ t [ inline-Subst ξ σ ⇑[ m ] ] ∎
opaque
inline-[]₀ :
(t : Term[ k ] (1+ n)) →
inline ξ (t [ u ]₀) ≡ inline ξ t [ inline ξ u ]₀
inline-[]₀ {ξ} {u} t =
inline ξ (t [ u ]₀) ≡⟨ inline-[] t ⟩
inline ξ t [ inline-Subst ξ (sgSubst u) ] ≡⟨ substVar-to-subst inline-Subst-sgSubst (inline _ t) ⟩
inline ξ t [ inline ξ u ]₀ ∎
opaque
inline-[]₁₀ :
(t : Term[ k ] (2+ n)) →
inline ξ (t [ u , v ]₁₀) ≡
inline ξ t [ inline ξ u , inline ξ v ]₁₀
inline-[]₁₀ {ξ} {u} {v} t =
inline ξ (t [ u , v ]₁₀) ≡⟨ inline-[] t ⟩
inline ξ t [ inline-Subst ξ (consSubst (sgSubst u) v) ] ≡⟨ (flip substVar-to-subst (inline _ t) λ x →
trans (inline-Subst-consSubst x) $
consSubst-cong refl inline-Subst-sgSubst x) ⟩
inline ξ t [ inline ξ u , inline ξ v ]₁₀ ∎
opaque
inline-[][]↑ :
(t : Term[ k ] (1+ m)) →
inline ξ (t [ n ][ u ]↑) ≡ inline ξ t [ n ][ inline ξ u ]↑
inline-[][]↑ {ξ} {n} {u} t =
inline ξ (t [ n ][ u ]↑) ≡⟨ inline-[] t ⟩
inline ξ t [ inline-Subst ξ (consSubst (wkSubst n idSubst) u) ] ≡⟨ (flip substVar-to-subst (inline _ t) λ x →
trans (inline-Subst-consSubst x) $
flip (consSubst-cong refl) x $ λ x →
trans (inline-Subst-wkSubst n x) $
wkSubst-cong inline-Subst-idSubst x) ⟩
inline ξ t [ n ][ inline ξ u ]↑ ∎
opaque
unfolding inline-Nat
<-inline-Nat :
{ξ : DExt (Term 0) n m}
{m≤α : m ≤ α} {α<n : α <′ n} →
inline-Nat ξ α ≡ inline-< ξ m≤α α<n
<-inline-Nat {n} {m} {α} {ξ} {m≤α} {α<n} with m ≤? α
… | no m≰α = ⊥-elim (m≰α m≤α)
… | yes _ with α <′? n
… | no α≮n = ⊥-elim (α≮n α<n)
… | yes _ =
cong₂ (inline-< ξ) ≤-propositional <′-propositional
opaque
unfolding inline
inline-Level-literal :
Level-literal t → inline ξ t ≡ t
inline-Level-literal zeroᵘ = PE.refl
inline-Level-literal (sucᵘ t-lit) =
cong sucᵘ (inline-Level-literal t-lit)
inline-Level-literal ωᵘ+ =
refl
inline-Level-literal (level t-lit) =
cong level (inline-Level-literal t-lit)
opaque
Level-literal-inline :
Level-literal t → Level-literal (inline ξ t)
Level-literal-inline t-lit =
PE.subst Level-literal (PE.sym $ inline-Level-literal t-lit) t-lit
opaque
unfolding inline glassifyᵉ
mutual
inline-<-glassifyᵉ :
(ξ : DExt (Term 0) n m) (m≤α : m ≤ α) (α<n : α <′ n) →
inline-< (glassifyᵉ ξ) m≤α α<n ≡ inline-< ξ m≤α α<n
inline-<-glassifyᵉ idᵉ m≤α α<n =
⊥-elim (n≮n _ (≤-trans (<′⇒< α<n) m≤α))
inline-<-glassifyᵉ (step _ _ _ t) _ (≤′-reflexive _) =
inline-glassifyᵉ t
inline-<-glassifyᵉ (step ξ _ _ _) m≤α (≤′-step α<n) =
inline-<-glassifyᵉ ξ m≤α α<n
inline-Nat-glassifyᵉ :
(ξ : DExt (Term 0) n m) →
inline-Nat (glassifyᵉ ξ) α ≡ inline-Nat ξ α
inline-Nat-glassifyᵉ {n} {m} {α} ξ with m ≤? α
… | no _ = refl
… | yes m≤α with α <′? n
… | no _ = refl
… | yes α<n = inline-<-glassifyᵉ ξ m≤α α<n
inline-glassifyᵉ :
(t : Term[ k ] n) → inline (glassifyᵉ ξ) t ≡ inline ξ t
inline-glassifyᵉ (var _) =
refl
inline-glassifyᵉ {ξ} (defn _) =
cong (wk _) (inline-Nat-glassifyᵉ ξ)
inline-glassifyᵉ Level =
refl
inline-glassifyᵉ zeroᵘ =
refl
inline-glassifyᵉ (sucᵘ t) =
cong sucᵘ (inline-glassifyᵉ t)
inline-glassifyᵉ (t supᵘ u) =
cong₂ _supᵘ_ (inline-glassifyᵉ t) (inline-glassifyᵉ u)
inline-glassifyᵉ (ωᵘ+ _) =
refl
inline-glassifyᵉ (level t) =
cong level (inline-glassifyᵉ t)
inline-glassifyᵉ (U l) =
cong U (inline-glassifyᵉ l)
inline-glassifyᵉ (Lift l A) =
cong₂ Lift (inline-glassifyᵉ l) (inline-glassifyᵉ A)
inline-glassifyᵉ (lift t) =
cong lift (inline-glassifyᵉ t)
inline-glassifyᵉ (lower t) =
cong lower (inline-glassifyᵉ t)
inline-glassifyᵉ Empty =
refl
inline-glassifyᵉ (emptyrec p A t) =
cong₂ (emptyrec _) (inline-glassifyᵉ A) (inline-glassifyᵉ t)
inline-glassifyᵉ (Unit _) =
refl
inline-glassifyᵉ (star _) =
refl
inline-glassifyᵉ (unitrec _ _ A t u) =
cong₃ (unitrec _ _) (inline-glassifyᵉ A) (inline-glassifyᵉ t)
(inline-glassifyᵉ u)
inline-glassifyᵉ (ΠΣ⟨ _ ⟩ _ , _ ▷ A ▹ B) =
cong₂ (ΠΣ⟨ _ ⟩ _ , _ ▷_▹_) (inline-glassifyᵉ A) (inline-glassifyᵉ B)
inline-glassifyᵉ (lam p t) =
cong (lam _) (inline-glassifyᵉ t)
inline-glassifyᵉ (t ∘⟨ p ⟩ u) =
cong₂ (_∘⟨ _ ⟩_) (inline-glassifyᵉ t) (inline-glassifyᵉ u)
inline-glassifyᵉ (prod s p t u) =
cong₂ (prod _ _) (inline-glassifyᵉ t) (inline-glassifyᵉ u)
inline-glassifyᵉ (fst p t) =
cong (fst _) (inline-glassifyᵉ t)
inline-glassifyᵉ (snd p t) =
cong (snd _) (inline-glassifyᵉ t)
inline-glassifyᵉ (prodrec r p q A t u) =
cong₃ (prodrec _ _ _) (inline-glassifyᵉ A) (inline-glassifyᵉ t)
(inline-glassifyᵉ u)
inline-glassifyᵉ ℕ =
refl
inline-glassifyᵉ zero =
refl
inline-glassifyᵉ (suc t) =
cong suc (inline-glassifyᵉ t)
inline-glassifyᵉ (natrec p q r A t u v) =
cong₄ (natrec _ _ _) (inline-glassifyᵉ A) (inline-glassifyᵉ t)
(inline-glassifyᵉ u) (inline-glassifyᵉ v)
inline-glassifyᵉ (Id A t u) =
cong₃ Id (inline-glassifyᵉ A) (inline-glassifyᵉ t)
(inline-glassifyᵉ u)
inline-glassifyᵉ rfl =
refl
inline-glassifyᵉ (J p q A t B u v w) =
cong₆ (J _ _) (inline-glassifyᵉ A) (inline-glassifyᵉ t)
(inline-glassifyᵉ B) (inline-glassifyᵉ u) (inline-glassifyᵉ v)
(inline-glassifyᵉ w)
inline-glassifyᵉ (K p A t B u v) =
cong₅ (K _) (inline-glassifyᵉ A) (inline-glassifyᵉ t)
(inline-glassifyᵉ B) (inline-glassifyᵉ u) (inline-glassifyᵉ v)
inline-glassifyᵉ ([]-cong _ l A t u v) =
cong₅ ([]-cong _) (inline-glassifyᵉ l) (inline-glassifyᵉ A)
(inline-glassifyᵉ t) (inline-glassifyᵉ u) (inline-glassifyᵉ v)
inline-glassifyᵉ (Quot A B) =
cong₂ Quot (inline-glassifyᵉ A) (inline-glassifyᵉ B)
inline-glassifyᵉ (class t) =
cong class (inline-glassifyᵉ t)
inline-glassifyᵉ (resp A B t u v) =
cong₅ resp (inline-glassifyᵉ A) (inline-glassifyᵉ B)
(inline-glassifyᵉ t) (inline-glassifyᵉ u) (inline-glassifyᵉ v)
inline-glassifyᵉ (set A B t u v w) =
cong₆ set (inline-glassifyᵉ A) (inline-glassifyᵉ B)
(inline-glassifyᵉ t) (inline-glassifyᵉ u) (inline-glassifyᵉ v)
(inline-glassifyᵉ w)
inline-glassifyᵉ (qrec C t u v w) =
cong₅ qrec (inline-glassifyᵉ C) (inline-glassifyᵉ t)
(inline-glassifyᵉ u) (inline-glassifyᵉ v) (inline-glassifyᵉ w)
opaque
unfolding inlineᵈ
inlineᵈ-glassify : inlineᵈ (glassify ∇) t ≡ inlineᵈ ∇ t
inlineᵈ-glassify {∇} {t} =
inline (as-DExt (glassify ∇)) t ≡˘⟨ cong (flip inline t) glassifyᵉ-as-DExt ⟩
inline (glassifyᵉ (as-DExt ∇)) t ≡⟨ inline-glassifyᵉ t ⟩
inline (as-DExt ∇) t ∎
opaque
unfolding inline-Con
inline-Con-glassifyᵉ :
(Γ : Con Term n) → inline-Con (glassifyᵉ ξ) Γ ≡ inline-Con ξ Γ
inline-Con-glassifyᵉ ε = refl
inline-Con-glassifyᵉ (Γ ∙ A) =
cong₂ _∙_ (inline-Con-glassifyᵉ _) (inline-glassifyᵉ A)
opaque
unfolding inline-Conᵈ
inline-Conᵈ-glassify : inline-Conᵈ (glassify ∇) Γ ≡ inline-Conᵈ ∇ Γ
inline-Conᵈ-glassify {∇} {Γ} =
inline-Con (as-DExt (glassify ∇)) Γ ≡˘⟨ cong (flip inline-Con _) glassifyᵉ-as-DExt ⟩
inline-Con (glassifyᵉ (as-DExt ∇)) Γ ≡⟨ inline-Con-glassifyᵉ _ ⟩
inline-Con (as-DExt ∇) Γ ∎
opaque
⟨≔⟩≡⟨≔⟩↑ :
(y : Fin n) →
wk (step-at x) (⟨ x ≔ t ⟩ y) ≡ ⟨ x ≔ wk (step-at′ x) t ⟩↑ y
⟨≔⟩≡⟨≔⟩↑ {x = x0} x0 =
refl
⟨≔⟩≡⟨≔⟩↑ {x = x0} (_ +1) =
refl
⟨≔⟩≡⟨≔⟩↑ {x = _+1 {n = 0} ()}
⟨≔⟩≡⟨≔⟩↑ {x = _+1 {n = 1+ _} _} x0 =
refl
⟨≔⟩≡⟨≔⟩↑ {x = _+1 {n = 1+ _} x} {t} (y +1) =
wk (lift (step-at x)) (wk1 (⟨ x ≔ t ⟩ y)) ≡˘⟨ wk1-wk≡lift-wk1 _ _ ⟩
wk1 (wk (step-at x) (⟨ x ≔ t ⟩ y)) ≡⟨ cong wk1 $ ⟨≔⟩≡⟨≔⟩↑ y ⟩
wk1 (⟨ x ≔ wk (step-at′ x) t ⟩↑ y) ∎
data Is-var? {n} : Term n → Set a where
var : ∀ x → Is-var? (var x)
not-var : (∀ {x} → ¬ t ≡ var x) → Is-var? t
opaque
is-var? : (t : Term n) → Is-var? t
is-var? (var x) = var x
is-var? (defn _) = not-var (λ ())
is-var? Level = not-var (λ ())
is-var? zeroᵘ = not-var (λ ())
is-var? (sucᵘ _) = not-var (λ ())
is-var? (_ supᵘ _) = not-var (λ ())
is-var? (U _) = not-var (λ ())
is-var? (Lift _ _) = not-var (λ ())
is-var? (lift _) = not-var (λ ())
is-var? (lower _) = not-var (λ ())
is-var? Empty = not-var (λ ())
is-var? (emptyrec _ _ _) = not-var (λ ())
is-var? (Unit _) = not-var (λ ())
is-var? (star _) = not-var (λ ())
is-var? (unitrec _ _ _ _ _) = not-var (λ ())
is-var? (ΠΣ⟨ _ ⟩ _ , _ ▷ _ ▹ _) = not-var (λ ())
is-var? (lam _ _) = not-var (λ ())
is-var? (_ ∘⟨ _ ⟩ _) = not-var (λ ())
is-var? (prod _ _ _ _) = not-var (λ ())
is-var? (fst _ _) = not-var (λ ())
is-var? (snd _ _) = not-var (λ ())
is-var? (prodrec _ _ _ _ _ _) = not-var (λ ())
is-var? ℕ = not-var (λ ())
is-var? zero = not-var (λ ())
is-var? (suc _) = not-var (λ ())
is-var? (natrec _ _ _ _ _ _ _) = not-var (λ ())
is-var? (Id _ _ _) = not-var (λ ())
is-var? rfl = not-var (λ ())
is-var? (J _ _ _ _ _ _ _ _) = not-var (λ ())
is-var? (K _ _ _ _ _ _) = not-var (λ ())
is-var? ([]-cong _ _ _ _ _ _) = not-var (λ ())
is-var? (Quot _ _) = not-var (λ ())
is-var? (class _) = not-var (λ ())
is-var? (resp _ _ _ _ _) = not-var (λ ())
is-var? (set _ _ _ _ _ _) = not-var (λ ())
is-var? (qrec _ _ _ _ _) = not-var (λ ())
opaque
unfolding _ᵈ•_
ᵈ•-PE-injectivity :
{∇₁ : DCon (Term 0) m} {ξ₁ : DExt (Term 0) n m}
{∇₂ : DCon (Term 0) m} {ξ₂ : DExt (Term 0) n m} →
∇₁ ᵈ• ξ₁ ≡ ∇₂ ᵈ• ξ₂ →
∇₁ ≡ ∇₂ × ξ₁ ≡ ξ₂
ᵈ•-PE-injectivity {ξ₁ = idᵉ} {∇₂} {ξ₂ = id eq} refl =
subst (λ eq → ∇₂ ᵈ• id eq ≡ ∇₂ × idᵉ ≡ id eq) Nat-set
(refl , refl)
ᵈ•-PE-injectivity {ξ₁ = idᵉ} {ξ₂ = step ξ₂ _ _ _} _ =
⊥-elim $ n≮n _ (DExt→≤ ξ₂)
ᵈ•-PE-injectivity {ξ₁ = step ξ₁ _ _ _} {ξ₂ = idᵉ} _ =
⊥-elim $ n≮n _ (DExt→≤ ξ₁)
ᵈ•-PE-injectivity {ξ₁ = step _ _ _ _} {ξ₂ = step _ _ _ _} eq =
case ∙-PE-injectivity eq of λ {
(eq , refl , refl , refl) →
Σ.map idᶠ (cong (λ ξ → step ξ _ _ _)) (ᵈ•-PE-injectivity eq) }
opaque
map-Cons-id : map-Cons idᶠ Δ ≡ Δ
map-Cons-id = cong₂ _»_ map-DCon-id map-Con-id
opaque
map-Cons-cong :
{f g : ∀ {n} → Term n → Term n} →
(∀ {n} (x : Term n) → f x ≡ g x) → map-Cons f Δ ≡ map-Cons g Δ
map-Cons-cong f≡g = cong₂ _»_ (map-DCon-cong f≡g) (map-Con-cong f≡g)
opaque
infix 4 _≟L_
_≟L_ :
Level-literal t₁ → Level-literal t₂ →
Dec (t₁ ≡ t₂)
zeroᵘ ≟L zeroᵘ = yes refl
zeroᵘ ≟L sucᵘ _ = no (λ ())
sucᵘ _ ≟L zeroᵘ = no (λ ())
sucᵘ t₁ ≟L sucᵘ t₂ =
Dec-map (cong sucᵘ , sucᵘ-PE-injectivity) (t₁ ≟L t₂)
ωᵘ+ {m = m₁} ≟L ωᵘ+ {m = m₂} =
Dec-map (cong ωᵘ+ , ωᵘ+-PE-injectivity) (m₁ Nat.≟ m₂)
ωᵘ+ ≟L level _ = no (λ ())
level _ ≟L ωᵘ+ = no (λ ())
level t₁ ≟L level t₂ =
Dec-map (cong level , level-PE-injectivity) (t₁ ≟L t₂)
opaque
Level-literal-propositional : Is-proposition (Level-literal t)
Level-literal-propositional {x = zeroᵘ} {y = zeroᵘ} = refl
Level-literal-propositional {x = sucᵘ _} {y = sucᵘ _} =
cong sucᵘ Level-literal-propositional
Level-literal-propositional {x = ωᵘ+} {y = ωᵘ+} = refl
Level-literal-propositional {x = level _} {y = level _} =
cong level Level-literal-propositional
opaque
unfolding size-of-Level ↓ᵘ_
↓ᵘ-size-of-Level :
{t : Term n} {t-lit : Level-literal t} →
↓ᵘ (size-of-Level t-lit) ≡ t
↓ᵘ-size-of-Level {t-lit = zeroᵘ} = refl
↓ᵘ-size-of-Level {t-lit = sucᵘ t} =
cong sucᵘ (↓ᵘ-size-of-Level {t-lit = t})
opaque
unfolding ↓ᵘ_
Level-literal⇔ :
{t : Term n} →
Level-literal t ⇔ ∃ λ n → t ≡ ↓ᵘ n
Level-literal⇔ =
(λ t-lit → size-of-Level t-lit , sym (↓ᵘ-size-of-Level)) , from
where
from : (∃ λ n → t ≡ ↓ᵘ n) → Level-literal t
from (0 , refl) = zeroᵘ
from (1+ n , refl) = sucᵘ (from (n , refl))
opaque
Level-literal-↓ᵘ : Level-literal {n = n} (↓ᵘ m)
Level-literal-↓ᵘ = Level-literal⇔ .proj₂ (_ , refl)
opaque
Level-literal-level-⇔ : Level-literal (level t) ⇔ Level-literal t
Level-literal-level-⇔ =
(λ { (level t-lit) → t-lit }) , level
opaque
unfolding Level-literal→Universe-level
Level-literal→Universe-level<ᵘωᵘ·2 :
{l-lit : Level-literal l} →
Level-literal→Universe-level l-lit <ᵘ ωᵘ·2
Level-literal→Universe-level<ᵘωᵘ·2 {l-lit = ωᵘ+} = ωᵘ+<ᵘωᵘ·2
Level-literal→Universe-level<ᵘωᵘ·2 {l-lit = level _} = 0ᵘ+<ᵘωᵘ·2
opaque
wk-1ᵘ+ : {l : Term[ k ] n} → wk ρ (1ᵘ+ l) ≡ 1ᵘ+ (wk ρ l)
wk-1ᵘ+ {k = tm} = refl
wk-1ᵘ+ {k = lvl} {l = ωᵘ+ _} = refl
wk-1ᵘ+ {k = lvl} {l = level _} = refl
opaque
1ᵘ+-[] : (l : Term[ k ] n) → 1ᵘ+ l [ σ ] ≡ 1ᵘ+ (l [ σ ])
1ᵘ+-[] {k = tm} _ = refl
1ᵘ+-[] {k = lvl} (ωᵘ+ _) = refl
1ᵘ+-[] {k = lvl} (level _) = refl
opaque
1ᵘ+ⁿ-[] : ∀ n → 1ᵘ+ⁿ n t [ σ ] ≡ 1ᵘ+ⁿ n (t [ σ ])
1ᵘ+ⁿ-[] 0 = refl
1ᵘ+ⁿ-[] {t} {σ} (1+ n) =
1ᵘ+ (1ᵘ+ⁿ n t) [ σ ] ≡⟨ 1ᵘ+-[] (1ᵘ+ⁿ n t) ⟩
1ᵘ+ (1ᵘ+ⁿ n t [ σ ]) ≡⟨ cong 1ᵘ+ (1ᵘ+ⁿ-[] n) ⟩
1ᵘ+ (1ᵘ+ⁿ n (t [ σ ])) ∎
opaque
wk-1ᵘ+ⁿ : ∀ n → wk ρ (1ᵘ+ⁿ n t) ≡ 1ᵘ+ⁿ n (wk ρ t)
wk-1ᵘ+ⁿ {ρ} {t} n =
wk ρ (1ᵘ+ⁿ n t) ≡⟨ wk≡subst _ _ ⟩
1ᵘ+ⁿ n t [ toSubst ρ ] ≡⟨ 1ᵘ+ⁿ-[] n ⟩
1ᵘ+ⁿ n (t [ toSubst ρ ]) ≡˘⟨ cong (1ᵘ+ⁿ n) $ wk≡subst _ _ ⟩
1ᵘ+ⁿ n (wk ρ t) ∎
opaque
unfolding ↓ᵘ_
↓ᵘ-[] : (↓ᵘ n) [ σ ] ≡ ↓ᵘ n
↓ᵘ-[] {n} = 1ᵘ+ⁿ-[] n
opaque
wk-↓ᵘ : wk ρ (↓ᵘ n) ≡ ↓ᵘ n
wk-↓ᵘ {ρ} {n} =
wk ρ (↓ᵘ n) ≡⟨ wk≡subst _ _ ⟩
(↓ᵘ n) [ toSubst ρ ] ≡⟨ ↓ᵘ-[] ⟩
↓ᵘ n ∎
opaque
1ᵘ+ⁿ-level≡ : ∀ n → 1ᵘ+ⁿ n (level t) ≡ level (1ᵘ+ⁿ n t)
1ᵘ+ⁿ-level≡ 0 = refl
1ᵘ+ⁿ-level≡ (1+ n) = cong 1ᵘ+ (1ᵘ+ⁿ-level≡ n)
opaque
Level-literal-1ᵘ+-⇔ :
{l : Term[ k ] n} →
Level-literal (1ᵘ+ l) ⇔ Level-literal l
Level-literal-1ᵘ+-⇔ {k = tm} =
(λ { (sucᵘ t) → t }) , sucᵘ
Level-literal-1ᵘ+-⇔ {l = ωᵘ+ _} =
(λ _ → ωᵘ+) , (λ _ → ωᵘ+)
Level-literal-1ᵘ+-⇔ {l = level _} =
(λ { (level (sucᵘ t)) → level t }) ,
(λ { (level t) → level (sucᵘ t) })
opaque
Infinite-1ᵘ+-⇔ : Infinite (1ᵘ+ l) ⇔ Infinite l
Infinite-1ᵘ+-⇔ = to _ , (λ { ωᵘ+ → ωᵘ+ })
where
to : (l : Term[ k ] n) → Infinite (1ᵘ+ l) → Infinite l
to {k = tm} _ ()
to (ωᵘ+ _) _ = ωᵘ+
to (level _) ()
opaque
unfolding inline
inline-1ᵘ+ : (l : Lvl n) → inline ξ (1ᵘ+ l) ≡ 1ᵘ+ (inline ξ l)
inline-1ᵘ+ (ωᵘ+ _) = refl
inline-1ᵘ+ (level _) = refl
opaque
Level-literal→[]≡[] :
{t : Term[ k ] n} → Level-literal t → t [ σ₁ ] ≡ t [ σ₂ ]
Level-literal→[]≡[] {k = tm} {σ₁} {σ₂} {t} t-lit =
let n , eq = Level-literal⇔ .proj₁ t-lit in
t [ σ₁ ] ≡⟨ cong _[ _ ] eq ⟩
(↓ᵘ n) [ σ₁ ] ≡⟨ ↓ᵘ-[] ⟩
↓ᵘ n ≡˘⟨ ↓ᵘ-[] ⟩
(↓ᵘ n) [ σ₂ ] ≡˘⟨ cong _[ _ ] eq ⟩
t [ σ₂ ] ∎
Level-literal→[]≡[] {k = lvl} ωᵘ+ = refl
Level-literal→[]≡[] {k = lvl} (level t-lit) =
cong level (Level-literal→[]≡[] t-lit)
opaque
Level-literal-[] :
{t : Term[ k ] n} → Level-literal t → Level-literal (t [ σ ])
Level-literal-[] {k = tm} {σ} {t} =
Level-literal t ⇔⟨ Level-literal⇔ ⟩→
(∃ λ n → t ≡ ↓ᵘ n) →⟨ Σ.map idᶠ (λ { refl → ↓ᵘ-[] }) ⟩
(∃ λ n → t [ σ ] ≡ ↓ᵘ n) ⇔˘⟨ Level-literal⇔ ⟩→
Level-literal (t [ σ ]) □
Level-literal-[] {k = lvl} ωᵘ+ = ωᵘ+
Level-literal-[] {k = lvl} (level t-lit) =
level (Level-literal-[] t-lit)
opaque
wk-Level-literal : Level-literal t ⇔ Level-literal (wk ρ t)
wk-Level-literal = to , flip from refl
where
to : Level-literal t → Level-literal (wk ρ t)
to = subst Level-literal (sym $ wk≡subst _ _) ∘→ Level-literal-[]
from : Level-literal u → wk ρ t ≡ u → Level-literal t
from zeroᵘ eq =
case wk-zeroᵘ eq of λ {
refl →
zeroᵘ }
from (sucᵘ u-lit) eq =
case wk-sucᵘ eq of λ {
(_ , refl , refl) →
sucᵘ (from u-lit refl) }
from ωᵘ+ eq rewrite wk-ωᵘ+ eq =
ωᵘ+
from (level u-lit) eq with wk-level eq
… | _ , refl , eq =
level (from u-lit eq)
opaque
unfolding _supᵘₗ′_
supᵘₗ′≡↓ᵘ⊔ :
(t₁-lit : Level-literal t₁) (t₂-lit : Level-literal t₂) →
t₁ supᵘₗ′ t₂ ≡
↓ᵘ (size-of-Level t₁-lit ⊔ size-of-Level t₂-lit)
supᵘₗ′≡↓ᵘ⊔ {t₁} {t₂} t₁-lit t₂-lit
with Level-literal? t₁ ×-dec Level-literal? t₂
… | yes _ =
cong₂ (λ t₁ t₂ → ↓ᵘ (size-of-Level t₁ ⊔ size-of-Level t₂))
Level-literal-propositional Level-literal-propositional
… | no not-both = ⊥-elim (not-both (t₁-lit , t₂-lit))
opaque
unfolding _supᵘₗ′_
supᵘₗ′≡supᵘ :
¬ (Level-literal t₁ × Level-literal t₂) →
t₁ supᵘₗ′ t₂ ≡ t₁ supᵘ t₂
supᵘₗ′≡supᵘ {t₁} {t₂} not-both
with Level-literal? t₁ ×-dec Level-literal? t₂
… | yes (t₁-lit , t₂-lit) = ⊥-elim (not-both (t₁-lit , t₂-lit))
… | no _ = refl
opaque
unfolding _supᵘₗ′_
Level-literal-supᵘₗ′⇔ :
Level-literal (t₁ supᵘₗ′ t₂) ⇔
(Level-literal t₁ × Level-literal t₂)
Level-literal-supᵘₗ′⇔ =
to ,
(λ (t₁-lit , t₂-lit) →
subst Level-literal (sym $ supᵘₗ′≡↓ᵘ⊔ t₁-lit t₂-lit)
Level-literal-↓ᵘ)
where
to :
Level-literal (t₁ supᵘₗ′ t₂) →
Level-literal t₁ × Level-literal t₂
to {t₁} {t₂} supᵘₗ′-lit
with Level-literal? t₁ ×-dec Level-literal? t₂
… | yes (t₁-lit , t₂-lit) = t₁-lit , t₂-lit
… | no _ = case supᵘₗ′-lit of λ ()
opaque
inline-supᵘₗ′ :
Level-literal t₁ → Level-literal t₂ →
inline ξ (t₁ supᵘₗ′ t₂) PE.≡ inline ξ t₁ supᵘₗ′ inline ξ t₂
inline-supᵘₗ′ {t₁} {t₂} {ξ} t₁-lit t₂-lit =
inline ξ (t₁ supᵘₗ′ t₂) ≡⟨ inline-Level-literal (Level-literal-supᵘₗ′⇔ .proj₂ (t₁-lit , t₂-lit)) ⟩
t₁ supᵘₗ′ t₂ ≡˘⟨ cong₂ _supᵘₗ′_ (inline-Level-literal t₁-lit) (inline-Level-literal t₂-lit) ⟩
inline ξ t₁ supᵘₗ′ inline ξ t₂ ∎
opaque
unfolding Level-literal⇔ size-of-Level
size-of-Level-Level-literal⇔ :
{eq : t ≡ ↓ᵘ n} →
size-of-Level (Level-literal⇔ .proj₂ (n , eq)) ≡ n
size-of-Level-Level-literal⇔ {n = 0} {eq = refl} = refl
size-of-Level-Level-literal⇔ {n = 1+ _} {eq = refl} =
cong 1+ size-of-Level-Level-literal⇔
opaque
unfolding Level-literal-↓ᵘ
size-of-Level-Level-literal-↓ᵘ :
size-of-Level (Level-literal-↓ᵘ {n = n} {m = m}) ≡ m
size-of-Level-Level-literal-↓ᵘ = size-of-Level-Level-literal⇔
opaque
unfolding Level-literal→Universe-level
Level-literal→Universe-level-ωᵘ+ :
{lit : Level-literal {n = n} (ωᵘ+ m)} →
Level-literal→Universe-level lit ≡ ωᵘ+ m
Level-literal→Universe-level-ωᵘ+ {lit = ωᵘ+} = refl
opaque
unfolding Level-literal→Universe-level Level-literal-level-⇔
Level-literal→Universe-level-level :
{lit : Level-literal (level t)} →
Level-literal→Universe-level lit ≡
0ᵘ+ (size-of-Level (Level-literal-level-⇔ .proj₁ lit))
Level-literal→Universe-level-level {lit = level _} = refl
opaque
unfolding Level-literal-[] Level-literal⇔
size-of-Level-Level-literal-[] :
{t-lit : Level-literal t} →
size-of-Level (Level-literal-[] {σ = σ} t-lit) ≡
size-of-Level t-lit
size-of-Level-Level-literal-[] = size-of-Level-Level-literal⇔
opaque
unfolding Level-literal→Universe-level Level-literal-[]
Level-literal→Universe-level-Level-literal-[] :
{l-lit : Level-literal l} →
Level-literal→Universe-level (Level-literal-[] {σ = σ} l-lit) ≡
Level-literal→Universe-level l-lit
Level-literal→Universe-level-Level-literal-[] {l-lit = ωᵘ+} =
refl
Level-literal→Universe-level-Level-literal-[] {l-lit = level _} =
cong 0ᵘ+ size-of-Level-Level-literal-[]
opaque
size-of-Level-subst :
{eq : t₁ ≡ t₂} {t₁-lit : Level-literal t₁} →
size-of-Level (subst Level-literal eq t₁-lit) ≡
size-of-Level t₁-lit
size-of-Level-subst {eq = refl} = refl
opaque
Level-literal→Universe-level-subst :
{eq : l₁ ≡ l₂} {l₁-lit : Level-literal l₁} →
Level-literal→Universe-level (subst Level-literal eq l₁-lit) ≡
Level-literal→Universe-level l₁-lit
Level-literal→Universe-level-subst {eq = refl} = refl
opaque
unfolding wk-Level-literal
size-of-Level-wk-Level-literal :
{t-lit : Level-literal t} →
size-of-Level (wk-Level-literal {ρ = ρ} .proj₁ t-lit) ≡
size-of-Level t-lit
size-of-Level-wk-Level-literal {t} {ρ} {t-lit} =
size-of-Level
(subst Level-literal (sym $ wk≡subst _ _) $
Level-literal-[] t-lit) ≡⟨ size-of-Level-subst ⟩
size-of-Level (Level-literal-[] t-lit) ≡⟨ size-of-Level-Level-literal-[] ⟩
size-of-Level t-lit ∎
opaque
unfolding wk-Level-literal
Level-literal→Universe-level-wk-Level-literal :
{t-lit : Level-literal t} →
Level-literal→Universe-level
(wk-Level-literal {ρ = ρ} .proj₁ t-lit) ≡
Level-literal→Universe-level t-lit
Level-literal→Universe-level-wk-Level-literal {t} {ρ} {t-lit} =
Level-literal→Universe-level
(subst Level-literal (sym $ wk≡subst _ _) $
Level-literal-[] t-lit) ≡⟨ Level-literal→Universe-level-subst ⟩
Level-literal→Universe-level (Level-literal-[] t-lit) ≡⟨ Level-literal→Universe-level-Level-literal-[] ⟩
Level-literal→Universe-level t-lit ∎
opaque
unfolding Level-literal-supᵘₗ′⇔
size-of-Level-Level-literal-supᵘₗ′⇔ :
{t₁-lit : Level-literal t₁}
{t₂-lit : Level-literal t₂} →
size-of-Level (Level-literal-supᵘₗ′⇔ .proj₂ (t₁-lit , t₂-lit)) ≡
size-of-Level t₁-lit ⊔ size-of-Level t₂-lit
size-of-Level-Level-literal-supᵘₗ′⇔ {t₁-lit} {t₂-lit} =
size-of-Level
(PE.subst Level-literal (PE.sym (supᵘₗ′≡↓ᵘ⊔ t₁-lit t₂-lit))
Level-literal-↓ᵘ) ≡⟨ size-of-Level-subst ⟩
size-of-Level
(Level-literal-↓ᵘ
{m = size-of-Level t₁-lit ⊔ size-of-Level t₂-lit}) ≡⟨ size-of-Level-Level-literal-↓ᵘ ⟩
size-of-Level t₁-lit ⊔ size-of-Level t₂-lit ∎
opaque
supᵘₗ′-[] :
Level-literal t₁ → Level-literal t₂ →
t₁ supᵘₗ′ t₂ [ σ ] ≡ (t₁ [ σ ]) supᵘₗ′ (t₂ [ σ ])
supᵘₗ′-[] {t₁} {t₂} {σ} t₁-lit t₂-lit =
t₁ supᵘₗ′ t₂ [ σ ] ≡⟨ cong _[ _ ] $ supᵘₗ′≡↓ᵘ⊔ _ _ ⟩
(↓ᵘ (size-of-Level t₁-lit ⊔ size-of-Level t₂-lit)) [ σ ] ≡⟨ ↓ᵘ-[] ⟩
↓ᵘ (size-of-Level t₁-lit ⊔ size-of-Level t₂-lit) ≡˘⟨ cong₂ (λ t₁ t₂ → ↓ᵘ (t₁ ⊔ t₂))
size-of-Level-Level-literal-[]
size-of-Level-Level-literal-[] ⟩
↓ᵘ
(size-of-Level (Level-literal-[] t₁-lit) ⊔
size-of-Level (Level-literal-[] t₂-lit)) ≡˘⟨ supᵘₗ′≡↓ᵘ⊔ _ _ ⟩
(t₁ [ σ ]) supᵘₗ′ (t₂ [ σ ]) ∎
opaque
unfolding _supᵘₗ′_
wk-supᵘₗ′ : wk ρ (t₁ supᵘₗ′ t₂) ≡ wk ρ t₁ supᵘₗ′ wk ρ t₂
wk-supᵘₗ′ {ρ} {t₁} {t₂}
with Level-literal? t₁ ×-dec Level-literal? t₂
… | yes (t₁-lit , t₂-lit) =
wk ρ (↓ᵘ (size-of-Level t₁-lit ⊔ size-of-Level t₂-lit)) ≡˘⟨ cong (wk _) $ supᵘₗ′≡↓ᵘ⊔ _ _ ⟩
wk ρ (t₁ supᵘₗ′ t₂) ≡⟨ wk≡subst _ _ ⟩
t₁ supᵘₗ′ t₂ [ toSubst ρ ] ≡⟨ supᵘₗ′-[] t₁-lit t₂-lit ⟩
(t₁ [ toSubst ρ ]) supᵘₗ′ (t₂ [ toSubst ρ ]) ≡˘⟨ cong₂ _supᵘₗ′_ (wk≡subst _ _) (wk≡subst _ _) ⟩
wk ρ t₁ supᵘₗ′ wk ρ t₂ ∎
… | no not-both =
wk ρ t₁ supᵘ wk ρ t₂ ≡˘⟨ supᵘₗ′≡supᵘ (not-both ∘→ Σ.map (wk-Level-literal .proj₂) (wk-Level-literal .proj₂)) ⟩
wk ρ t₁ supᵘₗ′ wk ρ t₂ ∎
opaque
Infinite-wk-⇔ : Infinite (wk ρ l) ⇔ Infinite l
Infinite-wk-⇔ = flip to refl , (λ { ωᵘ+ → ωᵘ+ })
where
to : Infinite l′ → wk ρ l ≡ l′ → Infinite l
to ωᵘ+ eq rewrite wk-ωᵘ+ eq = ωᵘ+
opaque
Infinite-[]-⇔ : Infinite (l [ σ ]) ⇔ Infinite l
Infinite-[]-⇔ = flip to refl , (λ { ωᵘ+ → ωᵘ+ })
where
to : Infinite l′ → l [ σ ] ≡ l′ → Infinite l
to {l} ωᵘ+ eq rewrite subst-ωᵘ+ {l = l} eq = ωᵘ+
opaque
Infinite→Level-literal : Infinite l → Level-literal l
Infinite→Level-literal ωᵘ+ = ωᵘ+
opaque
mapJ-cong :
{f g : ∀ {k} → Term[ k ] n → Term[ k ] n} →
(∀ {k} (t : Term[ k ] n) → f t ≡ g t) →
mapJ f 𝓙 ≡ mapJ g 𝓙
mapJ-cong {𝓙 = [ctxt]} f≡g = refl
mapJ-cong {𝓙 = [ _ type]} f≡g = cong [_type] (f≡g _)
mapJ-cong {𝓙 = [ _ ≡ _ type]} f≡g = cong₂ [_≡_type] (f≡g _) (f≡g _)
mapJ-cong {𝓙 = [ _ ∷ _ ]} f≡g = cong₂ [_∷_] (f≡g _) (f≡g _)
mapJ-cong {𝓙 = [ _ ≡ _ ∷ _ ]} f≡g = cong₃ [_≡_∷_] (f≡g _) (f≡g _)
(f≡g _)
mapJ-cong {𝓙 = [ _ ∷Level]} f≡g = cong [_∷Level] (f≡g _)
mapJ-cong {𝓙 = [ _ ≡ _ ∷Level]} f≡g = cong₂ [_≡_∷Level] (f≡g _)
(f≡g _)
opaque
mapJ-id : mapJ idᶠ 𝓙 ≡ 𝓙
mapJ-id {𝓙 = [ctxt]} = refl
mapJ-id {𝓙 = [ _ type]} = refl
mapJ-id {𝓙 = [ _ ≡ _ type]} = refl
mapJ-id {𝓙 = [ _ ∷ _ ]} = refl
mapJ-id {𝓙 = [ _ ≡ _ ∷ _ ]} = refl
mapJ-id {𝓙 = [ _ ∷Level]} = refl
mapJ-id {𝓙 = [ _ ≡ _ ∷Level]} = refl
opaque
mapJ-wk-id : mapJ (wk id) 𝓙 ≡ 𝓙
mapJ-wk-id {𝓙} =
mapJ (wk id) 𝓙 ≡⟨ mapJ-cong wk-id ⟩
mapJ idᶠ 𝓙 ≡⟨ mapJ-id ⟩
𝓙 ∎