------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous equality
------------------------------------------------------------------------
{-# OPTIONS --with-K --safe #-}
module Relation.Binary.HeterogeneousEquality where
open import Data.Product.Base using (_,_)
open import Function.Base using (case_of_; _∋_; id)
open import Function.Bundles using (Inverse)
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (Rel; REL; _⇒_)
open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder)
open import Relation.Binary.Structures using (IsEquivalence; IsPreorder)
open import Relation.Binary.Definitions using (Substitutive; Irrelevant
; Decidable; _Respects₂_; Trans; Reflexive)
open import Relation.Binary.Consequences using (subst⇒resp₂)
open import Relation.Binary.Indexed.Heterogeneous
using (IndexedSetoid)
open import Relation.Binary.Indexed.Heterogeneous.Construct.At
using (_atₛ_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
open import Relation.Binary.Reasoning.Syntax
open import Relation.Nullary.Decidable.Core using (yes; no)
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Unary using (Pred)
import Relation.Binary.PropositionalEquality.Properties as ≡
import Relation.Binary.HeterogeneousEquality.Core as Core
private
variable
a b c p r ℓ : Level
A : Set a
B : Set b
C : Set c
------------------------------------------------------------------------
-- Heterogeneous equality
infix 4 _≇_
open Core public using (_≅_; refl)
-- Nonequality.
_≇_ : ∀ {A : Set a} → A → {B : Set b} → B → Set a
x ≇ y = ¬ x ≅ y
------------------------------------------------------------------------
-- Conversion
open Core public using (≅-to-≡; ≡-to-≅)
≅-to-type-≡ : ∀ {A B : Set a} {x : A} {y : B} → x ≅ y → A ≡ B
≅-to-type-≡ refl = refl
≅-to-subst-≡ : ∀ {A B : Set a} {x : A} {y : B} → (p : x ≅ y) →
≡.subst (λ x → x) (≅-to-type-≡ p) x ≡ y
≅-to-subst-≡ refl = refl
------------------------------------------------------------------------
-- Some properties
reflexive : _⇒_ {A = A} _≡_ (λ x y → x ≅ y)
reflexive refl = refl
sym : ∀ {x : A} {y : B} → x ≅ y → y ≅ x
sym refl = refl
trans : ∀ {x : A} {y : B} {z : C} → x ≅ y → y ≅ z → x ≅ z
trans refl eq = eq
subst : Substitutive {A = A} (λ x y → x ≅ y) ℓ
subst P refl p = p
subst₂ : ∀ (_∼_ : REL A B r) {x y u v} → x ≅ y → u ≅ v → x ∼ u → y ∼ v
subst₂ _∼_ refl refl z = z
subst-removable : ∀ (P : Pred A p) {x y} (eq : x ≅ y) (z : P x) →
subst P eq z ≅ z
subst-removable P refl z = refl
subst₂-removable : ∀ (_∼_ : REL A B r) {x y u v} (eq₁ : x ≅ y) (eq₂ : u ≅ v) (z : x ∼ u) →
subst₂ _∼_ eq₁ eq₂ z ≅ z
subst₂-removable _∼_ refl refl z = refl
≡-subst-removable : ∀ (P : Pred A p) {x y} (eq : x ≡ y) (z : P x) →
≡.subst P eq z ≅ z
≡-subst-removable P refl z = refl
cong : ∀ {A : Set a} {B : A → Set b} {x y}
(f : (x : A) → B x) → x ≅ y → f x ≅ f y
cong f 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
cong₂ : ∀ {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c} {x y u v}
(f : (x : A) (y : B x) → C x y) → x ≅ y → u ≅ v → f x u ≅ f y v
cong₂ f refl refl = refl
resp₂ : ∀ (∼ : Rel A ℓ) → ∼ Respects₂ (λ x y → x ≅ y)
resp₂ _∼_ = subst⇒resp₂ _∼_ subst
module _ {I : Set ℓ} (A : I → Set a) {B : {k : I} → A k → Set b} where
icong : {i j : I} {x : A i} {y : A j} →
i ≡ j →
(f : {k : I} → (z : A k) → B z) →
x ≅ y →
f x ≅ f y
icong refl _ refl = refl
icong₂ : {C : {k : I} → (a : A k) → B a → Set c}
{i j : I} {x : A i} {y : A j} {u : B x} {v : B y} →
i ≡ j →
(f : {k : I} → (z : A k) → (w : B z) → C z w) →
x ≅ y → u ≅ v →
f x u ≅ f y v
icong₂ refl _ refl refl = refl
icong-subst-removable : {i j : I} (eq : i ≅ j)
(f : {k : I} → (z : A k) → B z)
(x : A i) →
f (subst A eq x) ≅ f x
icong-subst-removable refl _ _ = refl
icong-≡-subst-removable : {i j : I} (eq : i ≡ j)
(f : {k : I} → (z : A k) → B z)
(x : A i) →
f (≡.subst A eq x) ≅ f x
icong-≡-subst-removable refl _ _ = refl
------------------------------------------------------------------------
--Proof irrelevance
≅-irrelevant : {A B : Set ℓ} → Irrelevant ((A → B → Set ℓ) ∋ λ a → a ≅_)
≅-irrelevant refl refl = refl
module _ {A C : Set a} {B D : Set ℓ}
{w : A} {x : B} {y : C} {z : D} where
≅-heterogeneous-irrelevant : (p : w ≅ x) (q : y ≅ z) → x ≅ y → p ≅ q
≅-heterogeneous-irrelevant refl refl refl = refl
≅-heterogeneous-irrelevantˡ : (p : w ≅ x) (q : y ≅ z) → w ≅ y → p ≅ q
≅-heterogeneous-irrelevantˡ refl refl refl = refl
≅-heterogeneous-irrelevantʳ : (p : w ≅ x) (q : y ≅ z) → x ≅ z → p ≅ q
≅-heterogeneous-irrelevantʳ refl refl refl = refl
------------------------------------------------------------------------
-- Structures
isEquivalence : IsEquivalence {A = A} (λ x y → x ≅ y)
isEquivalence = record
{ refl = refl
; sym = sym
; trans = trans
}
setoid : Set ℓ → Setoid ℓ ℓ
setoid A = record
{ Carrier = A
; _≈_ = λ x y → x ≅ y
; isEquivalence = isEquivalence
}
indexedSetoid : (A → Set b) → IndexedSetoid A _ _
indexedSetoid B = record
{ Carrier = B
; _≈_ = λ x y → x ≅ y
; isEquivalence = record
{ refl = refl
; sym = sym
; trans = trans
}
}
≡↔≅ : ∀ {A : Set a} (B : A → Set b) {x : A} →
Inverse (≡.setoid (B x)) ((indexedSetoid B) atₛ x)
≡↔≅ B = record
{ to = id
; to-cong = ≡-to-≅
; from = id
; from-cong = ≅-to-≡
; inverse = (λ { ≡.refl → refl }) , λ { refl → ≡.refl }
}
decSetoid : Decidable {A = A} {B = A} (λ x y → x ≅ y) →
DecSetoid _ _
decSetoid dec = record
{ _≈_ = λ x y → x ≅ y
; isDecEquivalence = record
{ isEquivalence = isEquivalence
; _≟_ = dec
}
}
isPreorder : IsPreorder {A = A} (λ x y → x ≅ y) (λ x y → x ≅ y)
isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = id
; trans = trans
}
isPreorder-≡ : IsPreorder {A = A} _≡_ (λ x y → x ≅ y)
isPreorder-≡ = record
{ isEquivalence = ≡.isEquivalence
; reflexive = reflexive
; trans = trans
}
preorder : Set ℓ → Preorder ℓ ℓ ℓ
preorder A = record
{ Carrier = A
; _≈_ = _≡_
; _≲_ = λ x y → x ≅ y
; isPreorder = isPreorder-≡
}
------------------------------------------------------------------------
-- Convenient syntax for equational reasoning
module ≅-Reasoning where
-- The code in `Relation.Binary.Reasoning.Setoid` cannot handle
-- heterogeneous equalities, hence the code duplication here.
infix 4 _IsRelatedTo_
data _IsRelatedTo_ {A : Set a} {B : Set b} (x : A) (y : B) : Set a where
relTo : (x≅y : x ≅ y) → x IsRelatedTo y
start : ∀ {x : A} {y : B} → x IsRelatedTo y → x ≅ y
start (relTo x≅y) = x≅y
≡-go : ∀ {A : Set a} {B : Set b} → Trans {A = A} {C = B} _≡_ _IsRelatedTo_ _IsRelatedTo_
≡-go x≡y (relTo y≅z) = relTo (trans (reflexive x≡y) y≅z)
-- Combinators with one heterogeneous relation
module _ {A : Set a} {B : Set b} where
open begin-syntax (_IsRelatedTo_ {A = A} {B}) start public
open ≡-syntax (_IsRelatedTo_ {A = A} {B}) ≡-go public
-- Combinators with homogeneous relations
module _ {A : Set a} where
open end-syntax (_IsRelatedTo_ {A = A}) (relTo refl) public
-- Can't create syntax in the standard `Syntax` module for
-- heterogeneous steps because it would force that module to use
-- the `--with-k` option.
infixr 2 _≅⟨_⟩_ _≅⟨_⟨_
_≅⟨_⟩_ : ∀ (x : A) {y : B} {z : C} →
x ≅ y → y IsRelatedTo z → x IsRelatedTo z
_ ≅⟨ x≅y ⟩ relTo y≅z = relTo (trans x≅y y≅z)
_≅⟨_⟨_ : ∀ (x : A) {y : B} {z : C} →
y ≅ x → y IsRelatedTo z → x IsRelatedTo z
_ ≅⟨ y≅x ⟨ relTo y≅z = relTo (trans (sym y≅x) y≅z)
-- Deprecated
infixr 2 _≅˘⟨_⟩_
_≅˘⟨_⟩_ = _≅⟨_⟨_
{-# WARNING_ON_USAGE _≅˘⟨_⟩_
"Warning: _≅˘⟨_⟩_ was deprecated in v2.0.
Please use _≅⟨_⟨_ instead."
#-}
------------------------------------------------------------------------
-- Inspect
-- Inspect can be used when you want to pattern match on the result r
-- of some expression e, and you also need to "remember" that r ≡ e.
record Reveal_·_is_ {A : Set a} {B : A → Set b}
(f : (x : A) → B x) (x : A) (y : B x) :
Set (a ⊔ b) where
constructor [_]
field eq : f x ≅ y
inspect : ∀ {A : Set a} {B : A → Set b}
(f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]
-- Example usage:
-- f x y with g x | inspect g x
-- f x y | c z | [ eq ] = ...
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