From 11c125940cc7efac5a782f0c4ea4ea695d0615e5 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sun, 25 Feb 2024 23:03:53 +0100 Subject: [PATCH] One direction of translation preservation is enough One other half of a preservation proof can be constructed if given one direction of a translation preservation proof and a proof that the configuration translations are inverses to each other. However, this is only useful if the translation functions are extensionally equal to each other. Hence, in most cases, using this theorem will require function extensionally. --- src/Data/IndexedSet.lagda.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Data/IndexedSet.lagda.md b/src/Data/IndexedSet.lagda.md index b84142be..3076dc23 100644 --- a/src/Data/IndexedSet.lagda.md +++ b/src/Data/IndexedSet.lagda.md @@ -30,7 +30,7 @@ open import Data.Empty.Polymorphic using (⊥) open import Data.Unit.Polymorphic using (⊤; tt) open import Data.Product using (_×_; _,_; ∃-syntax; Σ-syntax; proj₁; proj₂) -open import Relation.Binary.PropositionalEquality using (_≗_) +open import Relation.Binary.PropositionalEquality using (_≗_; subst) open import Relation.Nullary using (¬_) open import Function using (id; _∘_; Congruent; Surjective) --IsSurjection) @@ -254,6 +254,9 @@ irrelevant-index-≅ x const-A const-B = ≅[]-trans {A = A} {C = C} (A⊆B , B⊆A) (B⊆C , C⊆B) = ⊆[]-trans {C = C} A⊆B B⊆C , ⊆[]-trans {C = A} C⊆B B⊆A + +⊆→≅ : ∀ {I J} {A : IndexedSet I} {B : IndexedSet J} → (f : I → J) → (f⁻¹ : J → I) → f ∘ f⁻¹ ≗ id → A ⊆[ f ] B → A ≅[ f ][ f⁻¹ ] B +⊆→≅ {A = A} {B = B} f f⁻¹ f∘f⁻¹ A⊆B = A⊆B , (λ i → Eq.sym (subst (λ j → A (f⁻¹ i) ≈ B j) (f∘f⁻¹ i) (A⊆B (f⁻¹ i)))) ``` ## Equational Reasoning