------------------------------------------------------------------------ -- The Agda standard library -- -- Function setoids and related constructions ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Function.Indexed.Relation.Binary.Equality where open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid) -- A variant of setoid which uses the propositional equality setoid -- for the domain, and a more convenient definition of _≈_. ≡-setoid : ∀ {f t₁ t₂} (From : Set f) → IndexedSetoid From t₁ t₂ → Setoid _ _ ≡-setoid From To = record { Carrier = (x : From) → Carrier x ; _≈_ = λ f g → ∀ x → f x ≈ g x ; isEquivalence = record { refl = λ {f} x → refl ; sym = λ f∼g x → sym (f∼g x) ; trans = λ f∼g g∼h x → trans (f∼g x) (g∼h x) } } where open IndexedSetoid To