diff options
Diffstat (limited to 'Data/Castable.agda')
| -rw-r--r-- | Data/Castable.agda | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/Data/Castable.agda b/Data/Castable.agda index 2c6932e..4f85b3d 100644 --- a/Data/Castable.agda +++ b/Data/Castable.agda @@ -3,7 +3,8 @@ module Data.Castable where open import Level using (Level; suc; _⊔_) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; subst) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; cong; module ≡-Reasoning) +open import Relation.Binary using (Sym; Trans; _⇒_) record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where @@ -18,6 +19,31 @@ record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂ cast-is-id : {m : A} .(eq : m ≡ m) (x : B m) → cast eq x ≡ x subst-is-cast : {m n : A} (eq : m ≡ n) (x : B m) → subst B eq x ≡ cast eq x + infix 3 _≈[_]_ + _≈[_]_ : {n m : A} → B n → .(eq : n ≡ m) → B m → Set ℓ₂ + _≈[_]_ x eq y = cast eq x ≡ y + + ≈-reflexive : {n : A} → _≡_ ⇒ (λ xs ys → _≈[_]_ {n} xs refl ys) + ≈-reflexive {n} {x} {y} eq = trans (cast-is-id refl x) eq + + ≈-sym : {m n : A} .{m≡n : m ≡ n} → Sym _≈[ m≡n ]_ _≈[ sym m≡n ]_ + ≈-sym {m} {n} {m≡n} {x} {y} x≡y = begin + cast (sym m≡n) y ≡⟨ cong (cast (sym m≡n)) x≡y ⟨ + cast (sym m≡n) (cast m≡n x) ≡⟨ cast-trans m≡n (sym m≡n) x ⟩ + cast (trans m≡n (sym m≡n)) x ≡⟨ cast-is-id (trans m≡n (sym m≡n)) x ⟩ + x ∎ + where + open ≡-Reasoning + + ≈-trans : {m n o : A} .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_ + ≈-trans {m} {n} {o} {m≡n} {n≡o} {x} {y} {z} x≡y y≡z = begin + cast (trans m≡n n≡o) x ≡⟨ cast-trans m≡n n≡o x ⟨ + cast n≡o (cast m≡n x) ≡⟨ cong (cast n≡o) x≡y ⟩ + cast n≡o y ≡⟨ y≡z ⟩ + z ∎ + where + open ≡-Reasoning + record Castable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} : Set (suc (ℓ₁ ⊔ ℓ₂)) where field B : A → Set ℓ₂ |