------------------------------------------------------------------------
-- Results relating different instances of certain axioms related to
-- equality
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Equality.Instances-related where

import Bijection
open import Equality
import Equivalence
import Extensionality
import Function-universe
import H-level
import H-level.Closure
open import Logical-equivalence using (_⇔_)
open import Prelude
import Surjection

private
module E (e⁺ :  e  Equivalence-relation⁺ e) where
open Reflexive-relation′
e  Equivalence-relation⁺.reflexive-relation (e⁺ e))
public

-- All families of equality types that satisfy certain axioms are
-- pointwise isomorphic. One of the families are used to define what
-- "isomorphic" means.
--
-- The isomorphisms map reflexivity to reflexivity in both directions.
--
-- Hofmann and Streicher prove something similar in "The groupoid
-- interpretation of type theory".

all-equality-types-isomorphic :
{e₁ e₂}
(eq₁ :  {a p}  Equality-with-J a p e₁)
(eq₂ :  {a p}  Equality-with-J a p e₂)
let open Bijection eq₁ in
{a} {A : Type a}
λ (iso : {x y : A}  E._≡_ e₁ x y  E._≡_ e₂ x y)
(∀ {x}  E._≡_ e₂ (_↔_.to   iso (E.refl e₁ x)) (E.refl e₂ x)) ×
(∀ {x}  E._≡_ e₁ (_↔_.from iso (E.refl e₂ x)) (E.refl e₁ x))
all-equality-types-isomorphic {c₁} {c₂} eq₁ eq₂ =
record
{ surjection = record
{ logical-equivalence = record
{ to   = to c₂ eq₁
; from = to c₁ eq₂
}
; right-inverse-of = to c₁ eq₂  to∘to _ _ eq₂ eq₁
}
; left-inverse-of = to∘to _ _ eq₁ eq₂
}
, to-refl c₂ eq₁
, to-refl c₁ eq₂
where
open E
open module Eq {c} (eq :  {a p}  Equality-with-J a p c) =
Equality-with-J′ eq hiding (_≡_; refl)

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

to-refl :
{c₁} c₂ (eq₁ :  {a p}  Equality-with-J a p c₁)
{a} {A : Type a} {x : A}
_≡_ c₂ (to c₂ eq₁ (refl c₁ x)) (refl c₂ x)
to-refl c₂ eq₁ = to c₂ eq₁ \$ subst-refl eq₁ (_≡_ c₂ _) _

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

module _ {congruence⁺}
(eq :  {a p}  Equality-with-J a p congruence⁺)
where

open Derived-definitions-and-properties eq
open Extensionality eq
open Function-universe eq hiding (_∘_) renaming (id to ⟨id⟩)
open H-level.Closure eq
open Surjection eq using (_↠_)

private
open module Eq = Equivalence eq using (_≃_)

abstract

-- The type Equality-with-J₀ a p reflexive-relation is
-- contractible (given the assumptions in the telescope above, and
-- assuming extensionality). A slight variant of this observation
-- came up in a discussion between Thierry Coquand, Simon Huber
-- and Nicolai Kraus. The proof is based on one due to Nicolai
-- Kraus.

Equality-with-J-contractible :
{a p}
Extensionality (lsuc (a  p)) (a  lsuc p)
Contractible (Equality-with-J₀ a p  _  reflexive-relation))
Equality-with-J-contractible {a} {p} ext =                        \$⟨ contr
Contractible ((A : Type a) (P : I A  Type p)
(d :  x  P (to x))  Singleton d)               ↝⟨ H-level.respects-surjection eq surj 0

Contractible (Equality-with-J₀ a p  _  reflexive-relation))
where
I : Type a  Type a
I A =  λ (x : A)   λ (y : A)  x  y

to :  {A}  A  I A
to x = x , x , refl x

≃I :  {A}  A  I A
≃I = Eq.↔⇒≃ (record
{ surjection = record
{ logical-equivalence = record
{ to   = to
; from = proj₁
}
; right-inverse-of = λ q
let x , y , x≡y = q in
cong (x ,_) \$
Σ-≡,≡→≡ x≡y
(subst (x ≡_) x≡y (refl x)  ≡⟨ sym trans-subst
trans (refl x) x≡y         ≡⟨ trans-reflˡ x≡y ⟩∎
x≡y                        )
}
; left-inverse-of = refl
})

contr :
Contractible ((A : Type a) (P : I A  Type p)
(d :  x  P (to x))  Singleton d)
contr =
Π-closure          (lower-extensionality (lsuc p) lzero    ext) 0 λ _
Π-closure          (lower-extensionality (lsuc a) (lsuc p) ext) 0 λ _
Π-closure          (lower-extensionality _        (lsuc p) ext) 0 λ _
singleton-contractible _

surj :
((A : Type a) (P : I A  Type p)
(d :  x  P (to x))  Singleton d)
Equality-with-J₀ a p  _  reflexive-relation)
surj =
((A : Type a) (P : I A  Type p)
(d :  x  P (to x))  Singleton d)                    ↔⟨⟩

((A : Type a) (P : I A  Type p)
(d :  x  P (to x))
λ (j : (x : A)  P (to x))  j  d)                  ↔⟨ (∀-cong (lower-extensionality (lsuc p) lzero ext) λ _
∀-cong (lower-extensionality (lsuc a) (lsuc p) ext) λ _
∀-cong (lower-extensionality _ (lsuc p) ext) λ _
∃-cong λ _  inverse \$
Eq.extensionality-isomorphism (lower-extensionality _ _ ext))
((A : Type a) (P : I A  Type p)
(d :  x  P (to x))
λ (j : (x : A)  P (to x))  (x : A)  j x  d x)    ↔⟨ (∀-cong (lower-extensionality (lsuc p) lzero ext) λ _
∀-cong (lower-extensionality (lsuc a) (lsuc p) ext) λ _
∀-cong (lower-extensionality _ (lsuc p) ext) λ _  inverse \$
Σ-cong (inverse \$ Π-cong (lower-extensionality _ _ ext)
≃I λ _  ⟨id⟩ {k = equivalence}) λ _
⟨id⟩ {k = equivalence})
((A : Type a) (P : I A  Type p)
(d :  x  P (to x))
λ (j : (q : I A)  P q)  (x : A)  j (to x)  d x)  ↔⟨ (∀-cong (lower-extensionality (lsuc p) lzero ext) λ _
∀-cong (lower-extensionality (lsuc a) (lsuc p) ext) λ _
ΠΣ-comm)
((A : Type a) (P : I A  Type p)
λ (j : (d :  x  P (to x))
(q : I A)  P q)
(d :  x  P (to x))
(x : A)  j d (to x)  d x)                        ↔⟨ (∀-cong (lower-extensionality (lsuc p) lzero ext) λ _
ΠΣ-comm)
((A : Type a)
λ (j : (P : I A  Type p) (d :  x  P (to x))
(q : I A)  P q)
(P : I A  Type p) (d :  x  P (to x))
(x : A)  j P d (to x)  d x)                      ↔⟨ ΠΣ-comm

( λ (J : (A : Type a) (P : I A  Type p)
(d :  x  P (to x))
(q : I A)  P q)
(A : Type a) (P : I A  Type p)
(d :  x  P (to x))
(x : A)  J A P d (to x)  d x)                    ↝⟨ record
{ logical-equivalence = record
{ to   = uncurry λ J   record
{ elim      = λ P r x≡y
J _ (P  proj₂  proj₂) r (_ , _ , x≡y)
; elim-refl = λ P r   _ (P  proj₂  proj₂) r _
}
; from = λ eq
A P d q  Equality-with-J₀.elim eq
x≡y  P (_ , _ , x≡y)) d (proj₂ (proj₂ q)))
,  A P d x  Equality-with-J₀.elim-refl eq
x≡y  P (_ , _ , x≡y)) d)
}
; right-inverse-of = refl
} ⟩□
Equality-with-J₀ a p  _  reflexive-relation)

private

-- A related example. It had been suggested that the two proofs
-- proof₁ and proof₂ below might not be provably equal, but Simon
-- Huber managed to prove that they are (using a slightly
-- different type for elim-refl).

module _ {a p} {A : Type a}
(P : A  Type p)
{x : A} (y : P x) where

subst′ : {x y : A} (P : A  Type p)  x  y  P x  P y
subst′ P = elim  {u v} _  P u  P v)  _ p  p)

subst′-refl≡id : {x : A} (P : A  Type p)  subst′ P (refl x)  id
subst′-refl≡id P = elim-refl  {u v} _  P u  P v)  _ p  p)

proof₁ proof₂ :
subst′ P (refl x) (subst′ P (refl x) y)  subst′ P (refl x) y

proof₁ = cong (_\$ subst′ P (refl x) y) (subst′-refl≡id P)

proof₂ = cong (subst′ P (refl x)) (cong (_\$ y) (subst′-refl≡id P))

proof₁≡proof₂ : proof₁  proof₂
proof₁≡proof₂ =
subst  (s : Singleton id)
y  cong (_\$ proj₁ s y) (proj₂ s)
cong (proj₁ s) (cong (_\$ y) (proj₂ s)))

(id                , refl id           ≡⟨ proj₂ (singleton-contractible _) _ ⟩∎
subst′ P (refl x) , subst′-refl≡id P  )

y
cong (_\$ y) (refl id)            ≡⟨ cong-id _ ⟩∎
cong id (cong (_\$ y) (refl id))  )

y