------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of products ------------------------------------------------------------------------ module Data.Product.Properties where open import Data.Product open import Function open import Relation.Binary.PropositionalEquality module _ {a b} {A : Set a} {B : A → Set b} where ,-injectiveˡ : ∀ {a c} {b : B a} {d : B c} → (a , b) ≡ (c , d) → a ≡ c ,-injectiveˡ refl = refl ,-injectiveʳ : ∀ {a} {b c : B a} → (Σ A B ∋ (a , b)) ≡ (a , c) → b ≡ c ,-injectiveʳ refl = refl