------------------------------------------------------------------------
-- The Agda standard library
--
-- Substituting equalities for binary relations
------------------------------------------------------------------------
-- For more general transformations between binary relations
-- see `Relation.Binary.Morphisms`.
{-# OPTIONS --cubical-compatible --safe #-}
open import Data.Product.Base using (_,_)
open import Relation.Binary.Core using (Rel; _⇔_)
module Relation.Binary.Construct.Subst.Equality
{a ℓ₁ ℓ₂} {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂}
(equiv@(to , from) : ≈₁ ⇔ ≈₂)
where
open import Function.Base using (_∘_; _∘′_)
open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
------------------------------------------------------------------------
-- Definitions
refl : Reflexive ≈₁ → Reflexive ≈₂
refl refl = to refl
sym : Symmetric ≈₁ → Symmetric ≈₂
sym sym = to ∘′ sym ∘′ from
trans : Transitive ≈₁ → Transitive ≈₂
trans trans x≈y y≈z = to (trans (from x≈y) (from y≈z))
------------------------------------------------------------------------
-- Structures
isEquivalence : IsEquivalence ≈₁ → IsEquivalence ≈₂
isEquivalence E = record
{ refl = refl E.refl
; sym = sym E.sym
; trans = trans E.trans
} where module E = IsEquivalence E
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4