{-# OPTIONS --with-K --safe #-}
module Relation.Binary.HeterogeneousEquality where
import Axiom.Extensionality.Heterogeneous as Ext
open import Data.Product
open import Data.Unit.NonEta
open import Function
open import Function.Inverse using (Inverse)
open import Level
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.Indexed.Heterogeneous
using (IndexedSetoid)
open import Relation.Binary.Indexed.Heterogeneous.Construct.At
using (_atₛ_)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
import Relation.Binary.HeterogeneousEquality.Core as Core
infix 4 _≇_
open Core public using (_≅_; refl)
_≇_ : ∀ {ℓ} {A : Set ℓ} → A → {B : Set ℓ} → B → Set ℓ
x ≇ y = ¬ x ≅ y
open Core public using (≅-to-≡; ≡-to-≅)
≅-to-type-≡ : ∀ {a} {A B : Set a} {x : A} {y : B} →
x ≅ y → A ≡ B
≅-to-type-≡ refl = refl
≅-to-subst-≡ : ∀ {a} {A B : Set a} {x : A} {y : B} → (p : x ≅ y) →
P.subst (λ x → x) (≅-to-type-≡ p) x ≡ y
≅-to-subst-≡ refl = refl
reflexive : ∀ {a} {A : Set a} → _⇒_ {A = A} _≡_ (λ x y → x ≅ y)
reflexive refl = refl
sym : ∀ {ℓ} {A B : Set ℓ} {x : A} {y : B} → x ≅ y → y ≅ x
sym refl = refl
trans : ∀ {ℓ} {A B C : Set ℓ} {x : A} {y : B} {z : C} →
x ≅ y → y ≅ z → x ≅ z
trans refl eq = eq
subst : ∀ {a} {A : Set a} {p} → Substitutive {A = A} (λ x y → x ≅ y) p
subst P refl p = p
subst₂ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
∀ {x₁ x₂ y₁ y₂} → x₁ ≅ x₂ → y₁ ≅ y₂ → P x₁ y₁ → P x₂ y₂
subst₂ P refl refl p = p
subst-removable : ∀ {a p} {A : Set a}
(P : A → Set p) {x y} (eq : x ≅ y) z →
subst P eq z ≅ z
subst-removable P refl z = refl
≡-subst-removable : ∀ {a p} {A : Set a}
(P : A → Set p) {x y} (eq : x ≡ y) z →
P.subst P eq z ≅ z
≡-subst-removable P refl z = refl
cong : ∀ {a b} {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 b} {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 b c} {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₂ : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) → ∼ Respects₂ (λ x y → x ≅ y)
resp₂ _∼_ = subst⟶resp₂ _∼_ subst
icong : ∀ {a b ℓ} {I : Set ℓ}
(A : I → Set a) {B : {k : I} → A k → Set b}
{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₂ : ∀ {a b c ℓ} {I : Set ℓ}
(A : I → Set a)
{B : {k : I} → A k → Set b}
{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 : ∀ {a b ℓ}
{I : Set ℓ}
(A : I → Set a) {B : {k : I} → A k → Set b}
{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 : ∀ {a b ℓ}
{I : Set ℓ}
(A : I → Set a) {B : {k : I} → A k → Set b}
{i j : I} (eq : i ≡ j)
(f : {k : I} → (z : A k) → B z)
(x : A i) →
f (P.subst A eq x) ≅ f x
icong-≡-subst-removable _ refl _ _ = refl
≅-irrelevant : ∀ {ℓ} {A B : Set ℓ} → Irrelevant ((A → B → Set ℓ) ∋ λ a → a ≅_)
≅-irrelevant refl refl = refl
module _ {ℓ} {A₁ A₂ A₃ A₄ : Set ℓ} {a₁ : A₁} {a₂ : A₂} {a₃ : A₃} {a₄ : A₄} where
≅-heterogeneous-irrelevant : (p : a₁ ≅ a₂) (q : a₃ ≅ a₄) → a₂ ≅ a₃ → p ≅ q
≅-heterogeneous-irrelevant refl refl refl = refl
≅-heterogeneous-irrelevantˡ : (p : a₁ ≅ a₂) (q : a₃ ≅ a₄) → a₁ ≅ a₃ → p ≅ q
≅-heterogeneous-irrelevantˡ refl refl refl = refl
≅-heterogeneous-irrelevantʳ : (p : a₁ ≅ a₂) (q : a₃ ≅ a₄) → a₂ ≅ a₄ → p ≅ q
≅-heterogeneous-irrelevantʳ refl refl refl = refl
isEquivalence : ∀ {a} {A : Set a} →
IsEquivalence {A = A} (λ x y → x ≅ y)
isEquivalence = record
{ refl = refl
; sym = sym
; trans = trans
}
setoid : ∀ {a} → Set a → Setoid _ _
setoid A = record
{ Carrier = A
; _≈_ = λ x y → x ≅ y
; isEquivalence = isEquivalence
}
indexedSetoid : ∀ {a b} {A : Set a} → (A → Set b) → IndexedSetoid A _ _
indexedSetoid B = record
{ Carrier = B
; _≈_ = λ x y → x ≅ y
; isEquivalence = record
{ refl = refl
; sym = sym
; trans = trans
}
}
≡↔≅ : ∀ {a b} {A : Set a} (B : A → Set b) {x : A} →
Inverse (P.setoid (B x)) ((indexedSetoid B) atₛ x)
≡↔≅ B = record
{ to = record { _⟨$⟩_ = id; cong = ≡-to-≅ }
; from = record { _⟨$⟩_ = id; cong = ≅-to-≡ }
; inverse-of = record
{ left-inverse-of = λ _ → refl
; right-inverse-of = λ _ → refl
}
}
decSetoid : ∀ {a} {A : Set a} →
Decidable {A = A} {B = A} (λ x y → x ≅ y) →
DecSetoid _ _
decSetoid dec = record
{ _≈_ = λ x y → x ≅ y
; isDecEquivalence = record
{ isEquivalence = isEquivalence
; _≟_ = dec
}
}
isPreorder : ∀ {a} {A : Set a} →
IsPreorder {A = A} (λ x y → x ≅ y) (λ x y → x ≅ y)
isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = id
; trans = trans
}
isPreorder-≡ : ∀ {a} {A : Set a} →
IsPreorder {A = A} _≡_ (λ x y → x ≅ y)
isPreorder-≡ = record
{ isEquivalence = P.isEquivalence
; reflexive = reflexive
; trans = trans
}
preorder : ∀ {a} → Set a → Preorder _ _ _
preorder A = record
{ Carrier = A
; _≈_ = _≡_
; _∼_ = λ x y → x ≅ y
; isPreorder = isPreorder-≡
}
module ≅-Reasoning where
infix 4 _IsRelatedTo_
infix 3 _∎
infixr 2 _≅⟨_⟩_ _≅˘⟨_⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_ _≡⟨⟩_
infix 1 begin_
data _IsRelatedTo_ {ℓ} {A : Set ℓ} (x : A) {B : Set ℓ} (y : B) :
Set ℓ where
relTo : (x≅y : x ≅ y) → x IsRelatedTo y
begin_ : ∀ {ℓ} {A : Set ℓ} {x : A} {B} {y : B} →
x IsRelatedTo y → x ≅ y
begin relTo x≅y = x≅y
_≅⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} {C} {z : C} →
x ≅ y → y IsRelatedTo z → x IsRelatedTo z
_ ≅⟨ x≅y ⟩ relTo y≅z = relTo (trans x≅y y≅z)
_≅˘⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} {C} {z : C} →
y ≅ x → y IsRelatedTo z → x IsRelatedTo z
_ ≅˘⟨ y≅x ⟩ relTo y≅z = relTo (trans (sym y≅x) y≅z)
_≡⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {y C} {z : C} →
x ≡ y → y IsRelatedTo z → x IsRelatedTo z
_ ≡⟨ x≡y ⟩ relTo y≅z = relTo (trans (reflexive x≡y) y≅z)
_≡˘⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {y C} {z : C} →
y ≡ x → y IsRelatedTo z → x IsRelatedTo z
_ ≡˘⟨ y≡x ⟩ relTo y≅z = relTo (trans (sym (reflexive y≡x)) y≅z)
_≡⟨⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} →
x IsRelatedTo y → x IsRelatedTo y
_ ≡⟨⟩ x≅y = x≅y
_∎ : ∀ {a} {A : Set a} (x : A) → x IsRelatedTo x
_∎ _ = relTo refl
record Reveal_·_is_ {a b} {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 b} {A : Set a} {B : A → Set b}
(f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]
proof-irrelevance = ≅-irrelevant
{-# WARNING_ON_USAGE proof-irrelevance
"Warning: proof-irrelevance was deprecated in v0.15.
Please use ≅-irrelevant instead."
#-}
≅-irrelevance = ≅-irrelevant
{-# WARNING_ON_USAGE ≅-irrelevance
"Warning: ≅-irrelevance was deprecated in v1.0.
Please use ≅-irrelevant instead."
#-}
≅-heterogeneous-irrelevance = ≅-heterogeneous-irrelevant
{-# WARNING_ON_USAGE ≅-heterogeneous-irrelevance
"Warning: ≅-heterogeneous-irrelevance was deprecated in v1.0.
Please use ≅-heterogeneous-irrelevant instead."
#-}
≅-heterogeneous-irrelevanceˡ = ≅-heterogeneous-irrelevantˡ
{-# WARNING_ON_USAGE ≅-heterogeneous-irrelevanceˡ
"Warning: ≅-heterogeneous-irrelevanceˡ was deprecated in v1.0.
Please use ≅-heterogeneous-irrelevantˡ instead."
#-}
≅-heterogeneous-irrelevanceʳ = ≅-heterogeneous-irrelevantʳ
{-# WARNING_ON_USAGE ≅-heterogeneous-irrelevanceʳ
"Warning: ≅-heterogeneous-irrelevanceʳ was deprecated in v1.0.
Please use ≅-heterogeneous-irrelevantʳ instead."
#-}
Extensionality = Ext.Extensionality
{-# WARNING_ON_USAGE Extensionality
"Warning: Extensionality was deprecated in v1.0.
Please use Extensionality from `Axiom.Extensionality.Heterogeneous` instead."
#-}
≡-ext-to-≅-ext = Ext.≡-ext⇒≅-ext
{-# WARNING_ON_USAGE ≡-ext-to-≅-ext
"Warning: ≡-ext-to-≅-ext was deprecated in v1.0.
Please use ≡-ext⇒≅-ext from `Axiom.Extensionality.Heterogeneous` instead."
#-}