------------------------------------------------------------------------
-- 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  _≇_
 
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  _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  _≅⟨_⟩_ _≅⟨_⟨_
 
  _≅⟨_⟩_ : ∀ (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  _≅˘⟨_⟩_
  _≅˘⟨_⟩_ = _≅⟨_⟨_
  {-# 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 ] = ...