module Relation.Binary.PropositionalEquality where
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.FunctionLifting
open import Data.Function
open import Data.Product
open import Relation.Binary.Core public using (_≡_; ≡-refl; _≢_)
open import Relation.Binary.PropositionalEquality.Core public
≡-subst₁ : ∀ {a} (P : a → Set1) → ∀ {x y} → x ≡ y → P x → P y
≡-subst₁ P ≡-refl p = p
≡-cong : Congruential _≡_
≡-cong = subst⟶cong ≡-refl ≡-subst
≡-cong₂ : Congruential₂ _≡_
≡-cong₂ = cong+trans⟶cong₂ ≡-cong ≡-trans
≡-setoid : Set → Setoid
≡-setoid a = record
{ carrier = a
; _≈_ = _≡_
; isEquivalence = ≡-isEquivalence
}
≡-decSetoid : ∀ {a} → Decidable (_≡_ {a}) → DecSetoid
≡-decSetoid ≡-dec = record
{ carrier = _
; _≈_ = _≡_
; isDecEquivalence = record
{ isEquivalence = ≡-isEquivalence
; _≟_ = ≡-dec
}
}
≡-isPreorder : ∀ {a} → IsPreorder {a} _≡_ _≡_
≡-isPreorder = record
{ isEquivalence = ≡-isEquivalence
; reflexive = id
; trans = ≡-trans
; ≈-resp-∼ = ≡-resp _≡_
}
≡-preorder : Set → Preorder
≡-preorder a = record
{ carrier = a
; _≈_ = _≡_
; _∼_ = _≡_
; isPreorder = ≡-isPreorder
}
infix 4 _≗_
_→-setoid_ : (a b : Set) → Setoid
a →-setoid b = record
{ carrier = a → b
; _≈_ = λ f g → ∀ x → f x ≡ g x
; isEquivalence = record
{ refl = λ _ → ≡-refl
; sym = λ f≗g x → ≡-sym (f≗g x)
; trans = λ f≗g g≗h x → ≡-trans (f≗g x) (g≗h x)
}
}
_≗_ : ∀ {a b} (f g : a → b) → Set
_≗_ {a} {b} = Setoid._≈_ (a →-setoid b)
data Inspect {a : Set} (x : a) : Set where
_with-≡_ : (y : a) (eq : y ≡ x) → Inspect x
inspect : ∀ {a} (x : a) → Inspect x
inspect x = x with-≡ ≡-refl
import Relation.Binary.EqReasoning as EqR
module ≡-Reasoning where
private
module Dummy {a : Set} where
open EqR (≡-setoid a) public
hiding (_≡⟨_⟩_; ≡-byDef)
renaming (_≈⟨_⟩_ to _≡⟨_⟩_)
open Dummy public