blob: 2c6932ebdc04a4dc3bc8ec71b6afc154b617efb9 (
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
|
{-# OPTIONS --without-K --safe #-}
module Data.Castable where
open import Level using (Level; suc; _⊔_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; subst)
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
record Castable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} : Set (suc (ℓ₁ ⊔ ℓ₂)) where
field
B : A → Set ℓ₂
isCastable : IsCastable B
|
