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 = LiftSetoid≡ A (λ _ → setoid B)
_≗_ : ∀ {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