blob: 4f85b3d6e5ca23fcb7a92cd65643bd34f46cb395 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
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
|
