Type Equality
module Type.Equality where
Fixity
infix 1 _≡β_
Imports
open import Type open import Type.RenamingSubstitution open import Builtin.Constant.Type open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂; trans; sym)
Beta equality relation for types
This serves as a declaritive specification of the semantics of types.
We need to give constructors for reflexivity, symmetry and transitivity as the presence of the beta-rule prevents these properties from being derivable. We have congruence rules for all constructors of type (except variables as this is subsumed by reflexivity). Finally, we have one computation rule: the beta-rule for application.
data _≡β_ : Φ ⊢⋆ J → Φ ⊢⋆ J → Set where -- structural rules refl≡β : (A : Φ ⊢⋆ J) ------------ → A ≡β A sym≡β : A ≡β B ------ → B ≡β A trans≡β : A ≡β B → B ≡β C ------ → A ≡β C -- congruence rules -- (no variable rule is needed) ⇒≡β : A ≡β A' → B ≡β B' ----------------- → A ⇒ B ≡β A' ⇒ B' Π≡β : B ≡β B' ----------- → Π B ≡β Π B' ƛ≡β : B ≡β B' ----------- → ƛ B ≡β ƛ B' ·≡β : A ≡β A' → B ≡β B' -------------------- → A · B ≡β A' · B' μ≡β : A ≡β A' → B ≡β B' ---------------- → μ A B ≡β μ A' B' -- computation rule β≡β : (B : Φ ,⋆ J ⊢⋆ K) → (A : Φ ⊢⋆ J) ------------------ → ƛ B · A ≡β B [ A ]
≡2β : A ≡ A' → A ≡β A' ≡2β refl = refl≡β _
Renaming for proofs of type equality
ren≡β : (ρ : Ren Φ Ψ) → A ≡β B ------------------ → ren ρ A ≡β ren ρ B ren≡β ρ (refl≡β A) = refl≡β (ren ρ A) ren≡β ρ (sym≡β p) = sym≡β (ren≡β ρ p) ren≡β ρ (trans≡β p q) = trans≡β (ren≡β ρ p) (ren≡β ρ q) ren≡β ρ (⇒≡β p q) = ⇒≡β (ren≡β ρ p) (ren≡β ρ q) ren≡β ρ (Π≡β p) = Π≡β (ren≡β (ext ρ) p) ren≡β ρ (ƛ≡β p) = ƛ≡β (ren≡β (ext ρ) p) ren≡β ρ (·≡β p q) = ·≡β (ren≡β ρ p) (ren≡β ρ q) ren≡β ρ (μ≡β p q) = μ≡β (ren≡β ρ p) (ren≡β ρ q) ren≡β ρ (β≡β B A) = trans≡β (β≡β _ _) (≡2β (trans (sym (sub-ren B)) (trans (sub-cong (ren-sub-cons ρ A) B) (ren-sub B))))
Substitution for proofs of type equality
sub≡β : (σ : Sub Φ Ψ) → A ≡β B ------------------ → sub σ A ≡β sub σ B sub≡β σ (refl≡β A) = refl≡β (sub σ A) sub≡β σ (sym≡β p) = sym≡β (sub≡β σ p) sub≡β σ (trans≡β p q) = trans≡β (sub≡β σ p) (sub≡β σ q) sub≡β σ (⇒≡β p q) = ⇒≡β (sub≡β σ p) (sub≡β σ q) sub≡β σ (Π≡β p) = Π≡β (sub≡β (exts σ) p) sub≡β σ (ƛ≡β p) = ƛ≡β (sub≡β (exts σ) p) sub≡β σ (·≡β p q) = ·≡β (sub≡β σ p) (sub≡β σ q) sub≡β σ (μ≡β p q) = μ≡β (sub≡β σ p) (sub≡β σ q) sub≡β σ (β≡β B A) = trans≡β (β≡β _ _) (≡2β (trans (trans (sym (sub-comp B)) (sub-cong (sub-sub-cons σ A) B)) (sub-comp B)))