Cong.agda

open import Agda.Builtin.Equality using (_≡_ ; refl)

infixl 9 _&_
_&_ : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x x′} → x ≡ x′ → f x ≡ f x′
f & refl = refl

infixl 8 _⊗_
_⊗_ : ∀ {a b} {A : Set a} {B : Set b} {f f′ : A → B} {x x′} →
      f ≡ f′ → x ≡ x′ → f x ≡ f′ x′
refl ⊗ refl = refl

cong = _&_

cong₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
          (f : A → B → C) {x x′ y y′} → x ≡ x′ → y ≡ y′ → f x y ≡ f x′ y′
cong₂ f p q = f & p ⊗ q