------------------------------------------------------------------------ -- Context extensions ------------------------------------------------------------------------ module SimplyTyped.ContextExtension where open import SimplyTyped.TypeSystem open import Relation.Binary.PropositionalEquality infixl 20 _▻▻_ -- Extending a context. _▻▻_ : Ctxt → Ctxt → Ctxt Γ ▻▻ ε = Γ Γ ▻▻ (Γ⁺ ▻ τ) = Γ ▻▻ Γ⁺ ▻ τ -- Context extension is associative. ▻▻-assoc : ∀ Γ Γ⁺ Γ⁺⁺ → Γ ▻▻ (Γ⁺ ▻▻ Γ⁺⁺) ≡ (Γ ▻▻ Γ⁺) ▻▻ Γ⁺⁺ ▻▻-assoc Γ Γ⁺ ε = refl ▻▻-assoc Γ Γ⁺ (Γ⁺⁺ ▻ τ) = cong (λ Γ → Γ ▻ τ) (▻▻-assoc Γ Γ⁺ Γ⁺⁺)