------------------------------------------------------------------------
-- All instances of the equality axioms are isomorphic
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Equality.Instances-isomorphic where

import Bijection
open import Equality
open import Prelude

-- One of the instances is used to define what "isomorphic" means.

all-instances-isomorphic :
  ∀ {refl₁ refl₂}
  (eq₁ : ∀ {a p} → Equality-with-J a p refl₁)
  (eq₂ : ∀ {a p} → Equality-with-J a p refl₂) →
  let open Bijection eq₁ in
  ∀ {a} {A : Set a} {x y : A} →
  Reflexive′._≡_ refl₁ x y ↔ Reflexive′._≡_ refl₂ x y
all-instances-isomorphic {refl₁} {refl₂} eq₁ eq₂ = record
  { surjection = record
    { equivalence = record
      { to   = to refl₂ eq₁
      ; from = to refl₁ eq₂
      }
    ; right-inverse-of = λ x≡y → to refl₁ eq₂ (to∘to _ _ eq₂ eq₁ x≡y)
    }
  ; left-inverse-of = to∘to _ _ eq₁ eq₂
  }
  where
  open Reflexive′
  open Equality-with-J′ hiding (_≡_; refl)

  to : ∀ {refl₁} refl₂ (eq₁ : ∀ {a p} → Equality-with-J a p refl₁)
       {a} {A : Set a} {x y : A} →
       _≡_ refl₁ x y → _≡_ refl₂ x y
  to refl₂ eq₁ {x = x} x≡y = subst eq₁ (_≡_ refl₂ x) x≡y (refl refl₂ x)

  to∘to : ∀ refl₁ refl₂
          (eq₁ : ∀ {a p} → Equality-with-J a p refl₁)
          (eq₂ : ∀ {a p} → Equality-with-J a p refl₂) →
          ∀ {a} {A : Set a} {x y : A} (x≡y : _≡_ refl₁ x y) →
          _≡_ refl₁ (to refl₁ eq₂ (to refl₂ eq₁ x≡y)) x≡y
  to∘to refl₁ refl₂ eq₁ eq₂ = elim eq₁
    (λ {x y} x≡y → _≡_ refl₁ (to refl₁ eq₂ (to refl₂ eq₁ x≡y)) x≡y)
    (λ x → to refl₁ eq₂ (to refl₂ eq₁ (refl refl₁ x))  ≡⟨ cong eq₁ (to refl₁ eq₂) (subst-refl eq₁ (_≡_ refl₂ x) (refl refl₂ x)) ⟩
           to refl₁ eq₂ (refl refl₂ x)                 ≡⟨ to refl₁ eq₂ $ subst-refl eq₂ (_≡_ refl₁ x) (refl refl₁ x) ⟩∎
           refl refl₁ x                                ∎)
    where
    open Derived-definitions-and-properties eq₁
      using (_≡⟨_⟩_; finally)