------------------------------------------------------------------------ -- The Agda standard library -- -- Sum combinators for propositional equality preserving functions ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Sum.Function.Propositional where open import Data.Sum.Base open import Data.Sum.Function.Setoid open import Data.Sum.Relation.Binary.Pointwise using (Pointwise-≡↔≡; _⊎ₛ_) open import Function.Construct.Composition as Compose open import Function.Related.Propositional open import Function open import Function.Properties.Inverse as Inv open import Level using (Level; _⊔_) open import Relation.Binary using (REL; Setoid) open import Relation.Binary.PropositionalEquality using (setoid) private variable a b c d : Level A B C D : Set a ------------------------------------------------------------------------ -- Helper lemma private liftViaInverse : {R : ∀ {a b ℓ₁ ℓ₂} → REL (Setoid a ℓ₁) (Setoid b ℓ₂) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)} → (∀ {a b c ℓ₁ ℓ₂ ℓ₃} {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} {U : Setoid c ℓ₃} → R S T → R T U → R S U) → (∀ {a b ℓ₁ ℓ₂} {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} → Inverse S T → R S T) → (R (setoid A) (setoid C) → R (setoid B) (setoid D) → R (setoid A ⊎ₛ setoid B) (setoid C ⊎ₛ setoid D)) → R (setoid A) (setoid C) → R (setoid B) (setoid D) → R (setoid (A ⊎ B)) (setoid (C ⊎ D)) liftViaInverse trans inv⇒R lift RAC RBD = Inv.transportVia trans inv⇒R (Inv.sym (Pointwise-≡↔≡ _ _)) (lift RAC RBD) (Pointwise-≡↔≡ _ _) ------------------------------------------------------------------------ -- Combinators for various function types infixr 1 _⊎-⟶_ _⊎-⇔_ _⊎-↣_ _⊎-↩_ _⊎-↪_ _⊎-↔_ _⊎-⟶_ : A ⟶ B → C ⟶ D → (A ⊎ C) ⟶ (B ⊎ D) _⊎-⟶_ = liftViaInverse Compose.function Inv.toFunction _⊎-function_ _⊎-⇔_ : A ⇔ B → C ⇔ D → (A ⊎ C) ⇔ (B ⊎ D) _⊎-⇔_ = liftViaInverse Compose.equivalence Inverse⇒Equivalence _⊎-equivalence_ _⊎-↣_ : A ↣ B → C ↣ D → (A ⊎ C) ↣ (B ⊎ D) _⊎-↣_ = liftViaInverse Compose.injection Inverse⇒Injection _⊎-injection_ _⊎-↠_ : A ↠ B → C ↠ D → (A ⊎ C) ↠ (B ⊎ D) _⊎-↠_ = liftViaInverse Compose.surjection Inverse⇒Surjection _⊎-surjection_ _⊎-↩_ : A ↩ B → C ↩ D → (A ⊎ C) ↩ (B ⊎ D) _⊎-↩_ = liftViaInverse Compose.leftInverse Inverse.leftInverse _⊎-leftInverse_ _⊎-↪_ : A ↪ B → C ↪ D → (A ⊎ C) ↪ (B ⊎ D) _⊎-↪_ = liftViaInverse Compose.rightInverse Inverse.rightInverse _⊎-rightInverse_ _⊎-⤖_ : A ⤖ B → C ⤖ D → (A ⊎ C) ⤖ (B ⊎ D) _⊎-⤖_ = liftViaInverse Compose.bijection Inverse⇒Bijection _⊎-bijection_ _⊎-↔_ : A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D) _⊎-↔_ = liftViaInverse Compose.inverse id _⊎-inverse_ infixr 1 _⊎-cong_ _⊎-cong_ : ∀ {k} → A ∼[ k ] B → C ∼[ k ] D → (A ⊎ C) ∼[ k ] (B ⊎ D) _⊎-cong_ {k = implication} = _⊎-⟶_ _⊎-cong_ {k = reverseImplication} = _⊎-⟶_ _⊎-cong_ {k = equivalence} = _⊎-⇔_ _⊎-cong_ {k = injection} = _⊎-↣_ _⊎-cong_ {k = reverseInjection} = _⊎-↣_ _⊎-cong_ {k = leftInverse} = _⊎-↪_ _⊎-cong_ {k = surjection} = _⊎-↠_ _⊎-cong_ {k = bijection} = _⊎-↔_