{-# OPTIONS --with-K --safe #-}
module Relation.Binary.HeterogeneousEquality where
import Axiom.Extensionality.Heterogeneous as Ext
open import Data.Unit.NonEta
open import Function.Base
open import Function.Inverse using (Inverse)
open import Level
open import Relation.Nullary hiding (Irrelevant)
open import Relation.Unary using (Pred)
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.Core as P using (_≡_; refl)
import Relation.Binary.PropositionalEquality.Properties as P
import Relation.Binary.HeterogeneousEquality.Core as Core
private
variable
a b c p r ℓ : Level
A : Set a
B : Set b
C : Set c
infix 4 _≇_
open Core public using (_≅_; refl)
_≇_ : ∀ {A : Set a} → A → {B : Set b} → B → Set a
x ≇ y = ¬ x ≅ y
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) →
P.subst (λ x → x) (≅-to-type-≡ p) x ≡ y
≅-to-subst-≡ refl = refl
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) →
P.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 (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 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
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 (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 : 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 = P.isEquivalence
; reflexive = reflexive
; trans = trans
}
preorder : Set ℓ → 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_ : ∀ {x : A} {y : B} → x IsRelatedTo y → x ≅ y
begin relTo x≅y = x≅y
_≅⟨_⟩_ : ∀ (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)
_≡⟨_⟩_ : ∀ (x : A) {y : A} {z : C} →
x ≡ y → y IsRelatedTo z → x IsRelatedTo z
_ ≡⟨ x≡y ⟩ relTo y≅z = relTo (trans (reflexive x≡y) y≅z)
_≡˘⟨_⟩_ : ∀ (x : A) {y : A} {z : C} →
y ≡ x → y IsRelatedTo z → x IsRelatedTo z
_ ≡˘⟨ y≡x ⟩ relTo y≅z = relTo (trans (sym (reflexive y≡x)) y≅z)
_≡⟨⟩_ : ∀ (x : A) {y : B} → x IsRelatedTo y → x IsRelatedTo y
_ ≡⟨⟩ x≅y = x≅y
_∎ : ∀ (x : A) → x IsRelatedTo x
_∎ _ = relTo refl
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 ]