From 02a7c2e196435b6b60a1164ff75a805685d2d151 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 19 Jun 2025 20:11:18 -0500 Subject: Add new hypergraph definitions --- Data/Castable.agda | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 Data/Castable.agda (limited to 'Data/Castable.agda') diff --git a/Data/Castable.agda b/Data/Castable.agda new file mode 100644 index 0000000..2c6932e --- /dev/null +++ b/Data/Castable.agda @@ -0,0 +1,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 -- cgit v1.2.3