From 33357ea0c2227e09953c42d00373115f0bbe9bca Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Mon, 24 Jun 2024 16:31:34 +0200 Subject: [PATCH] Remove the extensionality axiom module --- src/Axioms/Extensionality.agda | 28 ---------------------------- 1 file changed, 28 deletions(-) delete mode 100644 src/Axioms/Extensionality.agda diff --git a/src/Axioms/Extensionality.agda b/src/Axioms/Extensionality.agda deleted file mode 100644 index 80929e3e..00000000 --- a/src/Axioms/Extensionality.agda +++ /dev/null @@ -1,28 +0,0 @@ -module Axioms.Extensionality where - --- We use extensionality because --- the semantic domain of variability languages is a function --- and we want to prove these functions equivalent. - -open import Axiom.Extensionality.Propositional using (Extensionality) - -open import Data.List using (map) -open import Data.List.Properties using (map-cong) -open import Function using (_∘_; id) -open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl) - -postulate - extensionality : ∀ {a b} → Extensionality a b - -≗→≡ : ∀ {A B : Set} {f g : A → B} → f ≗ g → f ≡ g -≗→≡ = extensionality - -≡→≗ : ∀ {A B : Set} {f g : A → B} → f ≡ g → f ≗ g -≡→≗ f≡g rewrite f≡g = λ x → refl - -map-cong-≗-≡ : ∀ {A B : Set} {f g : A → B} → f ≗ g → map f ≡ map g -map-cong-≗-≡ = ≗→≡ ∘ map-cong - -map-cong-≡ : ∀ {A B : Set} {f g : A → B} → f ≡ g → map f ≡ map g -map-cong-≡ = map-cong-≗-≡ ∘ ≡→≗ -