1 files changed, 50 insertions, 0 deletions
diff --git a/Data/Castable.agda b/Data/Castable.agda
new file mode 100644
index 0000000..4f85b3d
--- /dev/null
+++ b/Data/Castable.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Castable where
+
+open import Level using (Level; suc; _⊔_)
+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
+
+  field
+    cast : {e e′ : A} → .(e ≡ e′) → B e → B e′
+    cast-trans
+        : {m n o : A}
+        → .(eq₁ : m ≡ n)
+          .(eq₂ : n ≡ o)
+          (x : B m)
+        → cast eq₂ (cast eq₁ x) ≡ cast (trans eq₁ eq₂) x
+    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 ℓ₂
+    isCastable : IsCastable B