------------------------------------------------------------------------ -- The Agda standard library -- -- Propositional equality -- -- This file contains some core definitions which are re-exported by -- Relation.Binary.PropositionalEquality. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Relation.Binary.PropositionalEquality.Core where open import Data.Product using (_,_) open import Function.Base using (_∘_) open import Level open import Relation.Binary.Core open import Relation.Binary.Definitions open import Relation.Nullary using (¬_) private variable a b : Level A B C : Set a ------------------------------------------------------------------------ -- Propositional equality open import Agda.Builtin.Equality public 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 _≡_ sym : Symmetric {A = A} _≡_ sym refl = refl trans : Transitive {A = A} _≡_ trans refl eq = eq subst : Substitutive {A = A} _≡_ subst P refl p = p subst₂ : (_∼_ : REL A B ) {x y u v} x y u v x u y v subst₂ _ refl refl p = p resp : (P : A Set ) P Respects _≡_ resp P refl p = p respˡ : ( : Rel A ) Respectsˡ _≡_ respˡ _∼_ refl x∼y = x∼y respʳ : ( : Rel A ) Respectsʳ _≡_ respʳ _∼_ refl x∼y = x∼y resp₂ : ( : Rel A ) Respects₂ _≡_ resp₂ _∼_ = respʳ _∼_ , respˡ _∼_ ------------------------------------------------------------------------ -- Properties of _≢_ ≢-sym : Symmetric {A = A} _≢_ ≢-sym x≢y = x≢y sym ------------------------------------------------------------------------ -- Convenient syntax for equational reasoning -- This is a special instance of `Relation.Binary.Reasoning.Setoid`. -- Rather than instantiating the latter with (setoid A), we reimplement -- equation chains from scratch since then goals are printed much more -- readably. module ≡-Reasoning {A : Set a} where infix 3 _∎ infixr 2 _≡⟨⟩_ step-≡ step-≡˘ infix 1 begin_ begin_ : ∀{x y : A} x y x y begin_ x≡y = x≡y _≡⟨⟩_ : (x {y} : A) x y x y _ ≡⟨⟩ x≡y = x≡y step-≡ : (x {y z} : A) y z x y x z step-≡ _ y≡z x≡y = trans x≡y y≡z step-≡˘ : (x {y z} : A) y z y x x z step-≡˘ _ y≡z y≡x = trans (sym y≡x) y≡z _∎ : (x : A) x x _∎ _ = refl syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y y≡z syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x y≡z