add irefl, icong and icong' (#1224)

Author: JacquesCarette

CHANGELOG.md

@@ -565,3 +565,12 @@ Other minor additions
   cong₂-reflˡ : cong₂ _∙_ refl p ≡ cong (x ∙_) p
   cong₂-reflʳ : cong₂ _∙_ p refl ≡ cong (_∙ u) p
   ```
+
+* Added new combinators to `Relation.Binary.PropositionalEquality.Core`:
+  ```agda
+  pattern erefl x = refl {x = x}
+
+  cong′  : {f : A → B} x → f x ≡ f x
+  icong  : {f : A → B} {x y} → x ≡ y → f x ≡ f y
+  icong′ : {f : A → B} x → f x ≡ f x
+  ```

src/Relation/Binary/PropositionalEquality/Core.agda

@@ -32,6 +32,33 @@ infix 4 _≢_
 _≢_ : {A : Set a} → Rel A a
 x ≢ y = ¬ x ≡ y
 
+------------------------------------------------------------------------
+-- A variant of `refl` where the argument is explicit
+
+pattern erefl x = refl {x = x}
+
+------------------------------------------------------------------------
+-- Congruence lemmas
+
+cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
+cong f refl = refl
+
+cong′ : ∀ {f : A → B} x → f x ≡ f x
+cong′ _ = refl
+
+icong : ∀ {f : A → B} {x y} → x ≡ y → f x ≡ f y
+icong = cong _
+
+icong′ : ∀ {f : A → B} x → f x ≡ f x
+icong′ _ = refl
+
+cong₂ : ∀ (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
+cong₂ f refl refl = refl
+
+cong-app : ∀ {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
+           f ≡ g → (x : A) → f x ≡ g x
+cong-app refl x = refl
+
 ------------------------------------------------------------------------
 -- Properties of _≡_
 
@@ -44,19 +71,9 @@ trans refl eq = eq
 subst : Substitutive {A = A} _≡_ ℓ
 subst P refl p = p
 
-cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
-cong f refl = refl
-
 subst₂ : ∀ (_∼_ : REL A B ℓ) {x y u v} → x ≡ y → u ≡ v → x ∼ u → y ∼ v
 subst₂ _ refl refl p = p
 
-cong-app : ∀ {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
-           f ≡ g → (x : A) → f x ≡ g x
-cong-app refl x = refl
-
-cong₂ : ∀ (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
-cong₂ f refl refl = refl
-
 respˡ : ∀ (∼ : Rel A ℓ) → ∼ Respectsˡ _≡_
 respˡ _∼_ refl x∼y = x∼y