Skip to content

Instantly share code, notes, and snippets.

@mietek

mietek/Cong.agda

Last active July 17, 2021 10:10
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mietek/71a91613058970a9878dc99aeea6640c to your computer and use it in GitHub Desktop.
Save mietek/71a91613058970a9878dc99aeea6640c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment