------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of products ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.Product.Properties where open import Data.Product open import Function using (_∘_) open import Relation.Binary using (Decidable) open import Relation.Binary.PropositionalEquality open import Relation.Nullary using (yes; no) ------------------------------------------------------------------------ -- Equality 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 -- See also Data.Product.Properties.WithK.,-injectiveʳ.