```------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous equality
------------------------------------------------------------------------

{-# 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.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 as P using (_≡_; refl)

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) →
P.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) →
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

------------------------------------------------------------------------
--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 (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-≡
}

------------------------------------------------------------------------
-- 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_
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

------------------------------------------------------------------------
-- 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 ] = ...
```