```------------------------------------------------------------------------
-- A class of algebraic structures, based on non-recursive simple
-- types, satisfies the property that isomorphic instances of a
-- structure are equal (assuming univalence)
------------------------------------------------------------------------

-- In fact, isomorphism and equality are basically the same thing, and
-- the main theorem can be instantiated with several different
-- "universes", not only the one based on simple types.

-- This module has been developed in collaboration with Thierry
-- Coquand.

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

open import Equality

module Univalence-axiom.Isomorphism-is-equality.Simple
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq
hiding (id; _∘_; inverse; _↔⟨_⟩_; finally-↔)
open Derived-definitions-and-properties eq
renaming (lower-extensionality to lower-ext)
open import Equality.Decidable-UIP eq
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq hiding (id; _∘_; inverse)
open import Function-universe eq hiding (id) renaming (_∘_ to _⊚_)
open import H-level eq
open import H-level.Closure eq
open import Injection eq using (Injective)
open import Logical-equivalence using (_⇔_; module _⇔_)
open import Nat eq
open import Preimage eq
open import Prelude as P hiding (id)
open import Univalence-axiom eq

------------------------------------------------------------------------
-- Universes with some extra stuff

-- A record type packing up some assumptions.

record Assumptions : Set₃ where
field

-- Univalence at three different levels.

univ  : Univalence (# 0)
univ₁ : Univalence (# 1)
univ₂ : Univalence (# 2)

abstract

-- Extensionality.

ext : ∀ {ℓ} → Extensionality ℓ (# 1)
ext = dependent-extensionality univ₂ (λ _ → univ₁)

ext₁ : Extensionality (# 1) (# 1)
ext₁ = ext

-- Universes with some extra stuff.

record Universe : Set₃ where

-- Parameters.

field

-- Codes for something.

U : Set₂

-- Interpretation of codes.

El : U → Set₁ → Set₁

-- El a, seen as a predicate, respects equivalences.

resp : ∀ a {B C} → B ≃ C → El a B → El a C

-- The resp function respects identities (assuming univalence).

resp-id : Assumptions → ∀ a {B} (x : El a B) → resp a Eq.id x ≡ x

-- Derived definitions.

-- A predicate that specifies what it means for an equivalence to be
-- an isomorphism between two elements.

Is-isomorphism : ∀ a {B C} → B ≃ C → El a B → El a C → Set₁
Is-isomorphism a eq x y = resp a eq x ≡ y

-- An alternative definition of Is-isomorphism, defined using
-- univalence.

Is-isomorphism′ : Assumptions →
∀ a {B C} → B ≃ C → El a B → El a C → Set₁
Is-isomorphism′ ass a eq x y = subst (El a) (≃⇒≡ univ₁ eq) x ≡ y
where open Assumptions ass

-- Every element is isomorphic to itself, transported along the
-- isomorphism.

isomorphic-to-itself :
(ass : Assumptions) → let open Assumptions ass in
∀ a {B C} (eq : B ≃ C) x →
Is-isomorphism a eq x (subst (El a) (≃⇒≡ univ₁ eq) x)
isomorphic-to-itself ass a eq x =
transport-theorem (El a) (resp a) (resp-id ass a) univ₁ eq x
where open Assumptions ass

-- Is-isomorphism and Is-isomorphism′ are isomorphic (assuming
-- univalence).

isomorphism-definitions-isomorphic :
(ass : Assumptions) →
∀ a {B C} (eq : B ≃ C) {x y} →
Is-isomorphism a eq x y ↔ Is-isomorphism′ ass a eq x y
isomorphism-definitions-isomorphic ass a eq {x} {y} =
Is-isomorphism      a eq x y  ↝⟨ ≡⇒↝ _ \$ cong (λ z → z ≡ y) \$ isomorphic-to-itself ass a eq x ⟩□
Is-isomorphism′ ass a eq x y  □

------------------------------------------------------------------------
-- A universe-indexed family of classes of structures

module Class (Univ : Universe) where

open Universe Univ

-- Codes for structures.

Code : Set₃
Code =
-- A code.
Σ U λ a →

-- A proposition.
(C : Set₁) → El a C → Σ Set₁ λ P →
-- The proposition should be propositional (assuming
-- univalence).
Assumptions → Is-proposition P

-- Interpretation of the codes. The elements of "Instance c" are
-- instances of the structure encoded by c.

Instance : Code → Set₂
Instance (a , P) =
-- A carrier type.
Σ Set₁ λ C →

-- An element.
Σ (El a C) λ x →

-- The element should satisfy the proposition.
proj₁ (P C x)

-- The carrier type.

Carrier : ∀ c → Instance c → Set₁
Carrier _ X = proj₁ X

-- The "element".

element : ∀ c (X : Instance c) → El (proj₁ c) (Carrier c X)
element _ X = proj₁ (proj₂ X)

abstract

-- One can prove that two instances of a structure are equal by
-- proving that the carrier types and "elements" (suitably
-- transported) are equal (assuming univalence).

equality-pair-lemma :
Assumptions →
∀ c {X Y : Instance c} →
(X ≡ Y) ↔
∃ λ (eq : Carrier c X ≡ Carrier c Y) →
subst (El (proj₁ c)) eq (element c X) ≡ element c Y
equality-pair-lemma ass (a , P) {C , x , p} {D , y , q} =

((C , x , p) ≡ (D , y , q))                 ↔⟨ inverse \$ ≃-≡ \$ ↔⇒≃ Σ-assoc ⟩

(((C , x) , p) ≡ ((D , y) , q))             ↝⟨ inverse \$ ignore-propositional-component (proj₂ (P D y) ass) ⟩

((C , x) ≡ (D , y))                         ↝⟨ inverse Σ-≡,≡↔≡ ⟩□

(∃ λ (eq : C ≡ D) → subst (El a) eq x ≡ y)  □

-- Structure isomorphisms.

Isomorphic : ∀ c → Instance c → Instance c → Set₁
Isomorphic (a , _) (C , x , _) (D , y , _) =
Σ (C ≃ D) λ eq → Is-isomorphism a eq x y

-- The type of isomorphisms between two instances of a structure
-- is isomorphic to the type of equalities between the same
-- instances (assuming univalence).
--
-- In short, isomorphism is isomorphic to equality.

isomorphism-is-equality :
Assumptions →
∀ c X Y → Isomorphic c X Y ↔ (X ≡ Y)
isomorphism-is-equality ass (a , P) (C , x , p) (D , y , q) =

(∃ λ (eq : C ≃ D) → resp a eq x ≡ y)                    ↝⟨ ∃-cong (λ eq → isomorphism-definitions-isomorphic ass a eq) ⟩

(∃ λ (eq : C ≃ D) → subst (El a) (≃⇒≡ univ₁ eq) x ≡ y)  ↝⟨ inverse \$
Σ-cong (≡≃≃ univ₁) (λ eq → ≡⇒↝ _ \$ sym \$
cong (λ eq → subst (El a) eq x ≡ y)
(_≃_.left-inverse-of (≡≃≃ univ₁) eq)) ⟩
(∃ λ (eq : C ≡ D) → subst (El a) eq x ≡ y)              ↝⟨ inverse \$ equality-pair-lemma ass c ⟩□

(X ≡ Y)                                                 □

where
open Assumptions ass

c : Code
c = a , P

X : Instance c
X = C , x , p

Y : Instance c
Y = D , y , q

abstract

-- The type of (lifted) isomorphisms between two instances of a
-- structure is equal to the type of equalities between the same
-- instances (assuming univalence).
--
-- In short, isomorphism is equal to equality.

isomorphic≡≡ :
Assumptions →
∀ c {X Y} → ↑ (# 2) (Isomorphic c X Y) ≡ (X ≡ Y)
isomorphic≡≡ ass c {X} {Y} =
≃⇒≡ univ₂ \$ ↔⇒≃ (
↑ _ (Isomorphic c X Y)  ↝⟨ ↑↔ ⟩
Isomorphic c X Y        ↝⟨ isomorphism-is-equality ass c X Y ⟩□
(X ≡ Y)                 □)
where open Assumptions ass

-- The "first part" of the from component of
-- isomorphism-is-equality is equal to a simple function.

proj₁-from-isomorphism-is-equality :
∀ ass c X Y →
proj₁ ∘ _↔_.from (isomorphism-is-equality ass c X Y) ≡
elim (λ {X Y} _ → proj₁ X ≃ proj₁ Y) (λ _ → Eq.id)
proj₁-from-isomorphism-is-equality ass _ _ _ = ext λ eq →

≡⇒≃ (proj₁ (Σ-≡,≡←≡ (proj₁ (Σ-≡,≡←≡
(cong (λ { (x , (y , z)) → (x , y) , z }) eq)))))            ≡⟨ cong (≡⇒≃ ∘ proj₁ ∘ Σ-≡,≡←≡) \$ proj₁-Σ-≡,≡←≡ _ ⟩

≡⇒≃ (proj₁ (Σ-≡,≡←≡ (cong proj₁
(cong (λ { (x , (y , z)) → (x , y) , z }) eq))))             ≡⟨ cong (≡⇒≃ ∘ proj₁ ∘ Σ-≡,≡←≡) \$
cong-∘ proj₁ (λ { (x , (y , z)) → (x , y) , z }) _ ⟩
≡⇒≃ (proj₁ (Σ-≡,≡←≡ (cong (λ { (x , (y , z)) → x , y }) eq)))  ≡⟨ cong ≡⇒≃ \$ proj₁-Σ-≡,≡←≡ _ ⟩

≡⇒≃ (cong proj₁ (cong (λ { (x , (y , z)) → x , y }) eq))       ≡⟨ cong ≡⇒≃ \$ cong-∘ proj₁ (λ { (x , (y , z)) → x , y }) _ ⟩

≡⇒≃ (cong proj₁ eq)                                            ≡⟨ elim-cong _≃_ proj₁ _ ⟩∎

elim (λ {X Y} _ → proj₁ X ≃ proj₁ Y) (λ _ → Eq.id) eq          ∎

where open Assumptions ass

-- In fact, the entire from component of isomorphism-is-equality
-- is equal to a simple function.
--
-- The proof of this lemma is somewhat complicated. A much shorter
-- proof can be constructed if El (proj₁ c) (proj₁ J) is a set
-- (see
-- Structure-identity-principle.from-isomorphism-is-equality′).

from-isomorphism-is-equality :
∀ ass c X Y →
_↔_.from (isomorphism-is-equality ass c X Y) ≡
elim (λ {X Y} _ → Isomorphic c X Y)
(λ { (_ , x , _) → Eq.id , resp-id ass (proj₁ c) x })
from-isomorphism-is-equality ass (a , P) (C , x , p) _ =
ext (elim¹
(λ eq → Σ-map ≡⇒≃ f (Σ-≡,≡←≡ (proj₁ (Σ-≡,≡←≡
(cong (λ { (C , (x , p)) → (C , x) , p }) eq)))) ≡
elim (λ {X Y} _ → Isomorphic (a , P) X Y)
(λ { (_ , x , _) → Eq.id , resp-id ass a x })
eq)

(Σ-map ≡⇒≃ f (Σ-≡,≡←≡ (proj₁ (Σ-≡,≡←≡ {A = ∃ (El a)}
(cong (λ { (C , (x , p)) → (C , x) , p })
(refl (C , x , p))))))               ≡⟨ cong (Σ-map ≡⇒≃ f ∘ Σ-≡,≡←≡ ∘ proj₁ ∘ Σ-≡,≡←≡) \$
cong-refl {A = Instance (a , P)}
(λ { (C , (x , p)) → (C , x) , p }) ⟩
Σ-map ≡⇒≃ f (Σ-≡,≡←≡ (proj₁ (Σ-≡,≡←≡ {A = ∃ (El a)}
(refl ((C , x) , p)))))    ≡⟨ cong (Σ-map ≡⇒≃ f ∘ Σ-≡,≡←≡ ∘ proj₁) (Σ-≡,≡←≡-refl {A = ∃ (El a)}) ⟩

Σ-map ≡⇒≃ f (Σ-≡,≡←≡ (refl {A = ∃ (El a)} (C , x)))       ≡⟨ cong (Σ-map ≡⇒≃ f) (Σ-≡,≡←≡-refl {B = El a}) ⟩

(≡⇒≃ (refl C) , f (subst-refl (El a) x))                  ≡⟨ Σ-≡,≡→≡ ≡⇒≃-refl lemma₄ ⟩

(Eq.id , resp-id ass a x)                                 ≡⟨ sym \$ elim-refl (λ {X Y} _ → Isomorphic (a , P) X Y) _ ⟩∎

elim (λ {X Y} _ → Isomorphic (a , P) X Y)
(λ { (_ , x , _) → Eq.id , resp-id ass a x })
(refl (C , x , p))                                   ∎))

where
open Assumptions ass

f : ∀ {D} {y : El a D} {eq : C ≡ D} →
subst (El a) eq x ≡ y →
resp a (≡⇒≃ eq) x ≡ y
f {y = y} {eq} eq′ =
_↔_.from (≡⇒↝ _ \$ cong (λ z → z ≡ y) \$
transport-theorem (El a) (resp a) (resp-id ass a)
univ₁ (≡⇒≃ eq) x)
(_↔_.to (≡⇒↝ _ \$ sym \$ cong (λ eq → subst (El a) eq x ≡ y)
(_≃_.left-inverse-of (≡≃≃ univ₁) eq)) eq′)

lemma₁ : ∀ {ℓ} {A B C : Set ℓ} {x} (eq₁ : B ≡ A) (eq₂ : C ≡ B) →
_↔_.from (≡⇒↝ _ eq₂) (_↔_.to (≡⇒↝ _ (sym eq₁)) x) ≡
_↔_.to (≡⇒↝ _ (sym (trans eq₂ eq₁))) x
lemma₁ {x = x} eq₁ eq₂ =
_↔_.from (≡⇒↝ _ eq₂) (_↔_.to (≡⇒↝ _ (sym eq₁)) x)      ≡⟨ sym \$ cong (λ f → f (_↔_.to (≡⇒↝ _ (sym eq₁)) x)) \$ ≡⇒↝-sym bijection ⟩
_↔_.to (≡⇒↝ _ (sym eq₂)) (_↔_.to (≡⇒↝ _ (sym eq₁)) x)  ≡⟨ sym \$ cong (λ f → f x) \$ ≡⇒↝-trans bijection ⟩
_↔_.to (≡⇒↝ _ (trans (sym eq₁) (sym eq₂))) x           ≡⟨ sym \$ cong (λ eq → _↔_.to (≡⇒↝ _ eq) x) \$ sym-trans _ _ ⟩∎
_↔_.to (≡⇒↝ _ (sym (trans eq₂ eq₁))) x                 ∎

lemma₂ : ∀ {a} {A : Set a} {x y z : A}
(x≡y : x ≡ y) (y≡z : y ≡ z) →
_↔_.to (≡⇒↝ _ (cong (λ x → x ≡ z) (sym x≡y))) y≡z ≡
trans x≡y y≡z
lemma₂ {y = y} {z} x≡y y≡z = elim₁
(λ x≡y → _↔_.to (≡⇒↝ _ (cong (λ x → x ≡ z) (sym x≡y))) y≡z ≡
trans x≡y y≡z)
(_↔_.to (≡⇒↝ _ (cong (λ x → x ≡ z) (sym (refl y)))) y≡z  ≡⟨ cong (λ eq → _↔_.to (≡⇒↝ _ (cong (λ x → x ≡ z) eq)) y≡z) sym-refl ⟩
_↔_.to (≡⇒↝ _ (cong (λ x → x ≡ z) (refl y))) y≡z        ≡⟨ cong (λ eq → _↔_.to (≡⇒↝ _ eq) y≡z) \$ cong-refl (λ x → x ≡ z) ⟩
_↔_.to (≡⇒↝ _ (refl (y ≡ z))) y≡z                       ≡⟨ cong (λ f → _↔_.to f y≡z) ≡⇒↝-refl ⟩
y≡z                                                     ≡⟨ sym \$ trans-reflˡ _ ⟩∎
trans (refl y) y≡z                                      ∎)
x≡y

lemma₃ :
sym (trans (cong (λ z → z ≡ x) \$
transport-theorem (El a) (resp a) (resp-id ass a)
univ₁ (≡⇒≃ (refl C)) x)
(cong (λ eq → subst (El a) eq x ≡ x)
(_≃_.left-inverse-of (≡≃≃ univ₁) (refl C)))) ≡
cong (λ z → z ≡ x) (sym \$
trans (trans (cong (λ eq → resp a eq x) ≡⇒≃-refl)
(resp-id ass a x))
(sym \$ subst-refl (El a) x))
lemma₃ =
sym (trans (cong (λ z → z ≡ x) _)
(cong (λ eq → subst (El a) eq x ≡ x) _))           ≡⟨ cong (λ eq → sym (trans (cong (λ z → z ≡ x)
(transport-theorem (El a) (resp a) (resp-id ass a)
univ₁ (≡⇒≃ (refl C)) x))
eq)) \$ sym \$
cong-∘ (λ z → z ≡ x) (λ eq → subst (El a) eq x) _ ⟩
sym (trans (cong (λ z → z ≡ x) _)
(cong (λ z → z ≡ x)
(cong (λ eq → subst (El a) eq x) _)))           ≡⟨ cong sym \$ sym \$ cong-trans (λ z → z ≡ x) _ _ ⟩

sym (cong (λ z → z ≡ x)
(trans _ (cong (λ eq → subst (El a) eq x) _)))          ≡⟨ sym \$ cong-sym (λ z → z ≡ x) _ ⟩

cong (λ z → z ≡ x) (sym \$
trans (transport-theorem (El a) (resp a)
(resp-id ass a) univ₁ (≡⇒≃ (refl C)) x)
(cong (λ eq → subst (El a) eq x) _))                  ≡⟨ cong (λ eq → cong (λ z → z ≡ x) (sym \$
trans eq (cong (λ eq → subst (El a) eq x)
(_≃_.left-inverse-of (≡≃≃ univ₁) (refl C)))))
(transport-theorem-≡⇒≃-refl (El a) (resp a) (resp-id ass a) univ₁ _) ⟩
cong (λ z → z ≡ x) (sym \$
trans (trans (trans (trans (cong (λ eq → resp a eq x)
≡⇒≃-refl)
(resp-id ass a x))
(sym \$ subst-refl (El a) x))
(sym \$ cong (λ eq → subst (El a) eq x)
(_≃_.left-inverse-of
(≡≃≃ univ₁) (refl C))))
(cong (λ eq → subst (El a) eq x)
(_≃_.left-inverse-of (≡≃≃ univ₁) (refl C))))    ≡⟨ cong (cong (λ z → z ≡ x) ∘ sym) \$
trans-[trans-sym]- _ _ ⟩∎
cong (λ z → z ≡ x) (sym \$
trans (trans (cong (λ eq → resp a eq x) ≡⇒≃-refl)
(resp-id ass a x))
(sym \$ subst-refl (El a) x))                         ∎

lemma₄ : subst (λ eq → Is-isomorphism a eq x x) ≡⇒≃-refl
(f (subst-refl (El a) x)) ≡
resp-id ass a x
lemma₄ =
subst (λ eq → Is-isomorphism a eq x x) ≡⇒≃-refl
(f (subst-refl (El a) x))                                      ≡⟨ cong (subst (λ eq → Is-isomorphism a eq x x) ≡⇒≃-refl) \$ lemma₁ _ _ ⟩

subst (λ eq → Is-isomorphism a eq x x) ≡⇒≃-refl
(_↔_.to (≡⇒↝ _ (sym (trans (cong (λ z → z ≡ x) \$
transport-theorem (El a)
(resp a) (resp-id ass a)
univ₁ (≡⇒≃ (refl C)) x)
(cong (λ eq → subst (El a) eq x ≡ x)
(_≃_.left-inverse-of
(≡≃≃ univ₁) (refl C))))))
(subst-refl (El a) x))                                 ≡⟨ cong (λ eq → subst (λ eq → Is-isomorphism a eq x x) ≡⇒≃-refl
(_↔_.to (≡⇒↝ _ eq) (subst-refl (El a) x)))
lemma₃ ⟩
subst (λ eq → Is-isomorphism a eq x x) ≡⇒≃-refl
(_↔_.to (≡⇒↝ _
(cong (λ z → z ≡ x) \$ sym
(trans (trans (cong (λ eq → resp a eq x)
≡⇒≃-refl)
(resp-id ass a x))
(sym \$ subst-refl (El a) x))))
(subst-refl (El a) x))                                 ≡⟨ cong (subst (λ eq → Is-isomorphism a eq x x) ≡⇒≃-refl) \$ lemma₂ _ _ ⟩

subst (λ eq → Is-isomorphism a eq x x) ≡⇒≃-refl
(trans (trans (trans (cong (λ eq → resp a eq x) ≡⇒≃-refl)
(resp-id ass a x))
(sym \$ subst-refl (El a) x))
(subst-refl (El a) x))                                      ≡⟨ cong (λ eq → subst (λ eq → Is-isomorphism a eq x x) ≡⇒≃-refl eq)
(trans-[trans-sym]- _ _) ⟩
subst (λ eq → resp a eq x ≡ x) ≡⇒≃-refl
(trans (cong (λ eq → resp a eq x) ≡⇒≃-refl)
(resp-id ass a x))                                          ≡⟨ subst-∘ (λ z → z ≡ x) (λ eq → resp a eq x) _ ⟩

subst (λ z → z ≡ x)
(cong (λ eq → resp a eq x) ≡⇒≃-refl)
(trans (cong (λ eq → resp a eq x) ≡⇒≃-refl)
(resp-id ass a x))                                          ≡⟨ cong (λ eq → subst (λ z → z ≡ x) eq
(trans (cong (λ eq → resp a eq x) ≡⇒≃-refl)
(resp-id ass a x))) \$
sym \$ sym-sym _ ⟩
subst (λ z → z ≡ x)
(sym \$ sym \$ cong (λ eq → resp a eq x) ≡⇒≃-refl)
(trans (cong (λ eq → resp a eq x) ≡⇒≃-refl)
(resp-id ass a x))                                          ≡⟨ subst-trans (sym \$ cong (λ eq → resp a eq x) ≡⇒≃-refl) ⟩

trans (sym \$ cong (λ eq → resp a eq x) ≡⇒≃-refl)
(trans (cong (λ eq → resp a eq x) ≡⇒≃-refl)
(resp-id ass a x))                                          ≡⟨ sym \$ trans-assoc _ _ _ ⟩

trans (trans (sym \$ cong (λ eq → resp a eq x) ≡⇒≃-refl)
(cong (λ eq → resp a eq x) ≡⇒≃-refl))
(resp-id ass a x)                                              ≡⟨ cong (λ eq → trans eq _) \$ trans-symˡ _ ⟩

trans (refl (resp a Eq.id x)) (resp-id ass a x)                  ≡⟨ trans-reflˡ _ ⟩∎

resp-id ass a x                                                  ∎

------------------------------------------------------------------------
-- A universe of non-recursive, simple types

-- Codes for types.

infixr 20 _⊗_
infixr 15 _⊕_
infixr 10 _⇾_

data U : Set₂ where
id set      : U
k           : Set₁ → U
_⇾_ _⊗_ _⊕_ : U → U → U

-- Interpretation of types.

El : U → Set₁ → Set₁
El id      C = C
El set     C = Set
El (k A)   C = A
El (a ⇾ b) C = El a C → El b C
El (a ⊗ b) C = El a C × El b C
El (a ⊕ b) C = El a C ⊎ El b C

-- El a preserves logical equivalences.

cast : ∀ a {B C} → B ⇔ C → El a B ⇔ El a C
cast id      eq = eq
cast set     eq = Logical-equivalence.id
cast (k A)   eq = Logical-equivalence.id
cast (a ⇾ b) eq = →-cong-⇔ (cast a eq) (cast b eq)
cast (a ⊗ b) eq = cast a eq ×-cong cast b eq
cast (a ⊕ b) eq = cast a eq ⊎-cong cast b eq

-- El a respects equivalences.

resp : ∀ a {B C} → B ≃ C → El a B → El a C
resp a eq = _⇔_.to (cast a (_≃_.logical-equivalence eq))

resp⁻¹ : ∀ a {B C} → B ≃ C → El a C → El a B
resp⁻¹ a eq = _⇔_.from (cast a (_≃_.logical-equivalence eq))

abstract

-- The cast function respects identities (assuming extensionality).

cast-id : Extensionality (# 1) (# 1) →
∀ a {B} → cast a (Logical-equivalence.id {A = B}) ≡
Logical-equivalence.id
cast-id ext id      = refl _
cast-id ext set     = refl _
cast-id ext (k A)   = refl _
cast-id ext (a ⇾ b) = cong₂ →-cong-⇔ (cast-id ext a) (cast-id ext b)
cast-id ext (a ⊗ b) = cong₂ _×-cong_ (cast-id ext a) (cast-id ext b)
cast-id ext (a ⊕ b) =
cast a Logical-equivalence.id ⊎-cong cast b Logical-equivalence.id  ≡⟨ cong₂ _⊎-cong_ (cast-id ext a) (cast-id ext b) ⟩
Logical-equivalence.id ⊎-cong Logical-equivalence.id                ≡⟨ cong₂ (λ f g → record { to = f; from = g })
(ext [ refl ∘ inj₁ , refl ∘ inj₂ ])
(ext [ refl ∘ inj₁ , refl ∘ inj₂ ]) ⟩∎
Logical-equivalence.id                                              ∎

resp-id : Extensionality (# 1) (# 1) →
∀ a {B} x → resp a (Eq.id {A = B}) x ≡ x
resp-id ext a x = cong (λ eq → _⇔_.to eq x) \$ cast-id ext a

-- The universe above is a "universe with some extra stuff".

simple : Universe
simple = record
{ U       = U
; El      = El
; resp    = resp
; resp-id = resp-id ∘ Assumptions.ext₁
}

-- Let us use this universe below.

open Universe simple using (Is-isomorphism)
open Class simple

-- An alternative definition of "being an isomorphism".
--
-- This definition is in bijective correspondence with Is-isomorphism
-- (see below).

Is-isomorphism′ : ∀ a {B C} → B ≃ C → El a B → El a C → Set₁
Is-isomorphism′ id      eq = λ x y → _≃_.to eq x ≡ y
Is-isomorphism′ set     eq = λ X Y → ↑ _ (X ≃ Y)
Is-isomorphism′ (k A)   eq = λ x y → x ≡ y
Is-isomorphism′ (a ⇾ b) eq = Is-isomorphism′ a eq →-rel
Is-isomorphism′ b eq
Is-isomorphism′ (a ⊗ b) eq = Is-isomorphism′ a eq ×-rel
Is-isomorphism′ b eq
Is-isomorphism′ (a ⊕ b) eq = Is-isomorphism′ a eq ⊎-rel
Is-isomorphism′ b eq

-- An alternative definition of Isomorphic, using Is-isomorphism′

Isomorphic′ : ∀ c → Instance c → Instance c → Set₁
Isomorphic′ (a , _) (C , x , _) (D , y , _) =
Σ (C ≃ D) λ eq → Is-isomorphism′ a eq x y

-- El a preserves equivalences (assuming extensionality).
--
-- Note that _≃_.logical-equivalence (cast≃ ext a eq) is
-- (definitionally) equal to cast a (_≃_.logical-equivalence eq); this
-- property is used below.

cast≃ : Extensionality (# 1) (# 1) →
∀ a {B C} → B ≃ C → El a B ≃ El a C
cast≃ ext a {B} {C} B≃C = ↔⇒≃ record
{ surjection = record
{ logical-equivalence = cast a B⇔C
; right-inverse-of    = to∘from
}
; left-inverse-of = from∘to
}
where
B⇔C = _≃_.logical-equivalence B≃C

cst : ∀ a → El a B ≃ El a C
cst id      = B≃C
cst set     = Eq.id
cst (k A)   = Eq.id
cst (a ⇾ b) = →-cong ext (cst a) (cst b)
cst (a ⊗ b) = cst a ×-cong cst b
cst (a ⊕ b) = cst a ⊎-cong cst b

abstract

-- The projection _≃_.logical-equivalence is homomorphic with
-- respect to cast a/cst a.

casts-related : ∀ a →
cast a (_≃_.logical-equivalence B≃C) ≡
_≃_.logical-equivalence (cst a)
casts-related id      = refl _
casts-related set     = refl _
casts-related (k A)   = refl _
casts-related (a ⇾ b) = cong₂ →-cong-⇔ (casts-related a)
(casts-related b)
casts-related (a ⊗ b) = cong₂ _×-cong_ (casts-related a)
(casts-related b)
casts-related (a ⊕ b) = cong₂ _⊎-cong_ (casts-related a)
(casts-related b)

to∘from : ∀ x → _⇔_.to (cast a B⇔C) (_⇔_.from (cast a B⇔C) x) ≡ x
to∘from x =
_⇔_.to (cast a B⇔C) (_⇔_.from (cast a B⇔C) x)  ≡⟨ cong₂ (λ f g → f (g x)) (cong _⇔_.to \$ casts-related a)
(cong _⇔_.from \$ casts-related a) ⟩
_≃_.to (cst a) (_≃_.from (cst a) x)            ≡⟨ _≃_.right-inverse-of (cst a) x ⟩∎
x                                              ∎

from∘to : ∀ x → _⇔_.from (cast a B⇔C) (_⇔_.to (cast a B⇔C) x) ≡ x
from∘to x =
_⇔_.from (cast a B⇔C) (_⇔_.to (cast a B⇔C) x)  ≡⟨ cong₂ (λ f g → f (g x)) (cong _⇔_.from \$ casts-related a)
(cong _⇔_.to \$ casts-related a) ⟩
_≃_.from (cst a) (_≃_.to (cst a) x)            ≡⟨ _≃_.left-inverse-of (cst a) x ⟩∎
x                                              ∎

private

logical-equivalence-cast≃ :
(ext : Extensionality (# 1) (# 1)) →
∀ a {B C} (eq : B ≃ C) →
_≃_.logical-equivalence (cast≃ ext a eq) ≡
cast a (_≃_.logical-equivalence eq)
logical-equivalence-cast≃ _ _ _ = refl _

-- Alternative, shorter definition of cast≃, based on univalence.
--
-- This proof does not (at the time of writing) have the property that
-- _≃_.logical-equivalence (cast≃′ ass a eq) is definitionally equal
-- to cast a (_≃_.logical-equivalence eq).

cast≃′ : Assumptions → ∀ a {B C} → B ≃ C → El a B ≃ El a C
cast≃′ ass a eq =
⟨ resp a eq
, resp-is-equivalence (El a) (resp a) (resp-id ext₁ a) univ₁ eq
⟩
where open Assumptions ass

abstract

-- The two definitions of "being an isomorphism" are "isomorphic"
-- (in bijective correspondence), assuming univalence.

is-isomorphism-isomorphic :
Assumptions →
∀ a {B C x y} (eq : B ≃ C) →
Is-isomorphism a eq x y ↔ Is-isomorphism′ a eq x y

is-isomorphism-isomorphic ass id {x = x} {y} eq =

(_≃_.to eq x ≡ y)  □

is-isomorphism-isomorphic ass set {x = X} {Y} eq =

(X ≡ Y)      ↔⟨ ≡≃≃ univ ⟩

(X ≃ Y)      ↝⟨ inverse ↑↔ ⟩□

↑ _ (X ≃ Y)  □

where open Assumptions ass

is-isomorphism-isomorphic ass (k A) {x = x} {y} eq =

(x ≡ y) □

is-isomorphism-isomorphic ass (a ⇾ b) {x = f} {g} eq =

(resp b eq ∘ f ∘ resp⁻¹ a eq ≡ g)                  ↝⟨ ∘from≡↔≡∘to ext₁ (cast≃ ext₁ a eq) ⟩

(resp b eq ∘ f ≡ g ∘ resp a eq)                    ↔⟨ inverse \$ extensionality-isomorphism ext₁ ⟩

(∀ x → resp b eq (f x) ≡ g (resp a eq x))          ↔⟨ ∀-preserves ext₁ (λ x → ↔⇒≃ \$
∀-intro ext₁ (λ y _ → resp b eq (f x) ≡ g y)) ⟩
(∀ x y → resp a eq x ≡ y → resp b eq (f x) ≡ g y)  ↔⟨ ∀-preserves ext₁ (λ _ → ∀-preserves ext₁ λ _ → ↔⇒≃ \$
→-cong ext₁ (is-isomorphism-isomorphic ass a eq)
(is-isomorphism-isomorphic ass b eq)) ⟩□
(∀ x y → Is-isomorphism′ a eq x y →
Is-isomorphism′ b eq (f x) (g y))         □

where open Assumptions ass

is-isomorphism-isomorphic ass (a ⊗ b) {x = x , u} {y , v} eq =

((resp a eq x , resp b eq u) ≡ (y , v))              ↝⟨ inverse ≡×≡↔≡ ⟩

(resp a eq x ≡ y × resp b eq u ≡ v)                  ↝⟨ is-isomorphism-isomorphic ass a eq ×-cong
is-isomorphism-isomorphic ass b eq ⟩□
Is-isomorphism′ a eq x y × Is-isomorphism′ b eq u v  □

where open Assumptions ass

is-isomorphism-isomorphic ass (a ⊕ b) {x = inj₁ x} {inj₁ y} eq =

(inj₁ (resp a eq x) ≡ inj₁ y)  ↝⟨ inverse ≡↔inj₁≡inj₁ ⟩

(resp a eq x ≡ y)              ↝⟨ is-isomorphism-isomorphic ass a eq ⟩□

Is-isomorphism′ a eq x y       □

where open Assumptions ass

is-isomorphism-isomorphic ass (a ⊕ b) {x = inj₂ x} {inj₂ y} eq =

(inj₂ (resp b eq x) ≡ inj₂ y)  ↝⟨ inverse ≡↔inj₂≡inj₂ ⟩

(resp b eq x ≡ y)              ↝⟨ is-isomorphism-isomorphic ass b eq ⟩□

Is-isomorphism′ b eq x y       □

where open Assumptions ass

is-isomorphism-isomorphic ass (a ⊕ b) {x = inj₁ x} {inj₂ y} eq =

(inj₁ _ ≡ inj₂ _)  ↝⟨ inverse \$ ⊥↔uninhabited ⊎.inj₁≢inj₂ ⟩□

⊥                  □

is-isomorphism-isomorphic ass (a ⊕ b) {x = inj₂ x} {inj₁ y} eq =

(inj₂ _ ≡ inj₁ _)  ↝⟨ inverse \$ ⊥↔uninhabited (⊎.inj₁≢inj₂ ∘ sym) ⟩□

⊥                  □

-- The two definitions of isomorphism are "isomorphic" (in bijective
-- correspondence), assuming univalence.

isomorphic-isomorphic :
Assumptions →
∀ c X Y →
Isomorphic c X Y ↔ Isomorphic′ c X Y
isomorphic-isomorphic ass (a , _) (C , x , _) (D , y , _) =
Σ (C ≃ D) (λ eq → Is-isomorphism  a eq x y)  ↝⟨ ∃-cong (λ eq → is-isomorphism-isomorphic ass a eq) ⟩
Σ (C ≃ D) (λ eq → Is-isomorphism′ a eq x y)  □

------------------------------------------------------------------------
-- An example: monoids

monoid : Code
monoid =
-- Binary operation.
(id ⇾ id ⇾ id) ⊗

-- Identity.
id ,

λ { C (_∙_ , e) →

-- The carrier type is a set.
(Is-set C ×

-- Left and right identity laws.
(∀ x → (e ∙ x) ≡ x) ×
(∀ x → (x ∙ e) ≡ x) ×

-- Associativity.
(∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z))) ,

-- The laws are propositional (assuming extensionality).
λ ass → let open Assumptions ass in
[inhabited⇒+]⇒+ 0 λ { (C-set , _) →
×-closure 1  (H-level-propositional ext₁ 2)
(×-closure 1 (Π-closure ext₁ 1 λ _ →
C-set _ _)
(×-closure 1 (Π-closure ext₁ 1 λ _ →
C-set _ _)
(Π-closure ext₁ 1 λ _ →
Π-closure ext₁ 1 λ _ →
Π-closure ext₁ 1 λ _ →
C-set _ _))) }}

-- The interpretation of the code is reasonable.

Instance-monoid :

Instance monoid
≡
Σ Set₁ λ C →
Σ ((C → C → C) × C) λ { (_∙_ , e) →
Is-set C ×
(∀ x → (e ∙ x) ≡ x) ×
(∀ x → (x ∙ e) ≡ x) ×
(∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z)) }

Instance-monoid = refl _

-- The notion of isomorphism that we get is also reasonable.

Isomorphic-monoid :
∀ {C₁ _∙₁_ e₁ laws₁ C₂ _∙₂_ e₂ laws₂} →

Isomorphic monoid (C₁ , (_∙₁_ , e₁) , laws₁)
(C₂ , (_∙₂_ , e₂) , laws₂)
≡
Σ (C₁ ≃ C₂) λ eq → let open _≃_ eq in
((λ x y → to (from x ∙₁ from y)) , to e₁) ≡ (_∙₂_ , e₂)

Isomorphic-monoid = refl _

-- Note that this definition of isomorphism is isomorphic to a more
-- standard one (assuming extensionality).

Isomorphism-monoid-isomorphic-to-standard :
Extensionality (# 1) (# 1) →
∀ {C₁ _∙₁_ e₁ laws₁ C₂ _∙₂_ e₂ laws₂} →

Isomorphic monoid (C₁ , (_∙₁_ , e₁) , laws₁)
(C₂ , (_∙₂_ , e₂) , laws₂)
↔
Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(∀ x y → to (x ∙₁ y) ≡ (to x ∙₂ to y)) ×
to e₁ ≡ e₂

Isomorphism-monoid-isomorphic-to-standard ext
{C₁} {_∙₁_} {e₁} {laws₁} {C₂} {_∙₂_} {e₂} =

(Σ (C₁ ≃ C₂) λ eq → let open _≃_ eq in
((λ x y → to (from x ∙₁ from y)) , to e₁) ≡ (_∙₂_ , e₂))  ↝⟨ inverse \$ Σ-cong (↔↔≃ ext (proj₁ laws₁)) (λ _ → _ □) ⟩

(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
((λ x y → to (from x ∙₁ from y)) , to e₁) ≡ (_∙₂_ , e₂))  ↝⟨ inverse \$ ∃-cong (λ _ → ≡×≡↔≡) ⟩

(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(λ x y → to (from x ∙₁ from y)) ≡ _∙₂_ ×
to e₁ ≡ e₂)                                               ↔⟨ inverse \$ ∃-cong (λ _ → extensionality-isomorphism ext ×-cong (_ □)) ⟩

(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(∀ x → (λ y → to (from x ∙₁ from y)) ≡ _∙₂_ x) ×
to e₁ ≡ e₂)                                               ↔⟨ inverse \$ ∃-cong (λ _ →
∀-preserves ext (λ _ → extensionality-isomorphism ext)
×-cong
(_ □)) ⟩
(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(∀ x y → to (from x ∙₁ from y) ≡ (x ∙₂ y)) ×
to e₁ ≡ e₂)                                               ↔⟨ inverse \$ ∃-cong (λ eq →
Π-preserves ext (↔⇒≃ eq) (λ x → Π-preserves ext (↔⇒≃ eq) (λ y →
≡⇒≃ \$ sym \$ cong₂ (λ u v → _↔_.to eq (u ∙₁ v) ≡
(_↔_.to eq x ∙₂ _↔_.to eq y))
(_↔_.left-inverse-of eq x)
(_↔_.left-inverse-of eq y)))
×-cong
(_ □)) ⟩□
(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(∀ x y → to (x ∙₁ y) ≡ (to x ∙₂ to y)) ×
to e₁ ≡ e₂)                                               □

------------------------------------------------------------------------
-- An example: posets

poset : Code
poset =
-- The ordering relation.
(id ⇾ id ⇾ set) ,

λ C _≤_ →

-- The carrier type is a set.
(Is-set C ×

-- The ordering relation is (pointwise) propositional.
(∀ x y → Is-proposition (x ≤ y)) ×

-- Reflexivity.
(∀ x → x ≤ x) ×

-- Transitivity.
(∀ x y z → x ≤ y → y ≤ z → x ≤ z) ×

-- Antisymmetry.
(∀ x y → x ≤ y → y ≤ x → x ≡ y)) ,

λ ass → let open Assumptions ass in
[inhabited⇒+]⇒+ 0 λ { (C-set , ≤-prop , _) →
×-closure 1  (H-level-propositional ext₁ 2)
(×-closure 1 (Π-closure ext₁                     1 λ _ →
Π-closure (lower-ext (# 0) _ ext₁) 1 λ _ →
H-level-propositional (lower-ext _ _ ext₁) 1)
(×-closure 1 (Π-closure (lower-ext (# 0) _ ext₁) 1 λ _ →
≤-prop _ _)
(×-closure 1 (Π-closure ext₁                     1 λ _ →
Π-closure ext₁                     1 λ _ →
Π-closure (lower-ext (# 0) _ ext₁) 1 λ _ →
Π-closure (lower-ext _ _ ext₁)     1 λ _ →
Π-closure (lower-ext _ _ ext₁)     1 λ _ →
≤-prop _ _)
(Π-closure ext₁                     1 λ _ →
Π-closure ext₁                     1 λ _ →
Π-closure ext                      1 λ _ →
Π-closure ext                      1 λ _ →
C-set _ _)))) }

-- The interpretation of the code is reasonable. (Except, perhaps,
-- that the carrier type lives in Set₁ but the codomain of the
-- ordering relation is Set. In the corresponding example in
-- Univalence-axiom.Isomorphism-is-equality.Simple.Variant the carrier
-- type lives in Set.)

Instance-poset :

Instance poset
≡
Σ Set₁ λ C →
Σ (C → C → Set) λ _≤_ →
Is-set C ×
(∀ x y → Is-proposition (x ≤ y)) ×
(∀ x → x ≤ x) ×
(∀ x y z → x ≤ y → y ≤ z → x ≤ z) ×
(∀ x y → x ≤ y → y ≤ x → x ≡ y)

Instance-poset = refl _

-- The notion of isomorphism that we get is also reasonable. It is the
-- usual notion of "order isomorphism", with two (main) differences:
--
-- * Equivalences are used instead of bijections. However,
--   equivalences and bijections coincide for sets (assuming
--   extensionality).
--
-- * We use equality, (λ a b → from a ≤₁ from b) ≡ _≤₂_, instead of
--   "iff", ∀ a b → (a ≤₁ b) ⇔ (to a ≤₂ to b). However, the ordering
--   relation is pointwise propositional, so these two expressions are
--   equal (assuming univalence).

Isomorphic-poset :
∀ {C₁ _≤₁_ laws₁ C₂ _≤₂_ laws₂} →

Isomorphic poset (C₁ , _≤₁_ , laws₁) (C₂ , _≤₂_ , laws₂)
≡
Σ (C₁ ≃ C₂) λ eq → let open _≃_ eq in
(λ a b → from a ≤₁ from b) ≡ _≤₂_

Isomorphic-poset = refl _

-- We can prove that this notion of isomorphism is isomorphic to the
-- usual notion of order isomorphism (assuming univalence).

Isomorphism-poset-isomorphic-to-order-isomorphism :
Assumptions →
∀ {C₁ _≤₁_ laws₁ C₂ _≤₂_ laws₂} →

Isomorphic poset (C₁ , _≤₁_ , laws₁) (C₂ , _≤₂_ , laws₂)
↔
Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
∀ x y → (x ≤₁ y) ⇔ (to x ≤₂ to y)

Isomorphism-poset-isomorphic-to-order-isomorphism ass
{C₁} {_≤₁_} {laws₁} {C₂} {_≤₂_} {laws₂} =

(Σ (C₁ ≃ C₂) λ eq → let open _≃_ eq in
(λ a b → from a ≤₁ from b) ≡ _≤₂_)           ↝⟨ inverse \$ Σ-cong (↔↔≃ ext₁ (proj₁ laws₁)) (λ _ → _ □) ⟩

(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(λ a b → from a ≤₁ from b) ≡ _≤₂_)           ↔⟨ inverse \$ ∃-cong (λ _ → extensionality-isomorphism ext₁) ⟩

(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(∀ a → (λ b → from a ≤₁ from b) ≡ _≤₂_ a))   ↔⟨ inverse \$ ∃-cong (λ _ → ∀-preserves ext₁ λ _ → extensionality-isomorphism ext₁) ⟩

(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(∀ a b → (from a ≤₁ from b) ≡ (a ≤₂ b)))     ↔⟨ inverse \$ ∃-cong (λ eq →
Π-preserves ext₁ (↔⇒≃ eq) λ a → Π-preserves ext₁ (↔⇒≃ eq) λ b →
≡⇒≃ \$ sym \$ cong₂ (λ x y → (x ≤₁ y) ≡ (_↔_.to eq a ≤₂ _↔_.to eq b))
(_↔_.left-inverse-of eq a)
(_↔_.left-inverse-of eq b)) ⟩
(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(∀ a b → (a ≤₁ b) ≡ (to a ≤₂ to b)))         ↔⟨ ∃-cong (λ _ → ∀-preserves ext₁ λ _ → ∀-preserves ext₁ λ _ → ≡≃≃ univ) ⟩

(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(∀ a b → (a ≤₁ b) ≃ (to a ≤₂ to b)))         ↔⟨ inverse \$ ∃-cong (λ _ → ∀-preserves ext₁ λ _ → ∀-preserves (lower-ext (# 0) _ ext₁) λ _ → ↔⇒≃ \$
⇔↔≃ (lower-ext _ _ ext₁) (proj₁ (proj₂ laws₁) _ _)
(proj₁ (proj₂ laws₂) _ _)) ⟩□
(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
(∀ a b → (a ≤₁ b) ⇔ (to a ≤₂ to b)))         □

where open Assumptions ass

-- The previous lemma implies that we can prove that the notion of
-- isomorphism that we get is /equal/ to the usual notion of order
-- isomorphism (assuming univalence).

Isomorphism-poset-equal-to-order-isomorphism :
Assumptions →
∀ {C₁ _≤₁_ laws₁ C₂ _≤₂_ laws₂} →

Isomorphic poset (C₁ , _≤₁_ , laws₁) (C₂ , _≤₂_ , laws₂)
≡
Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
∀ x y → (x ≤₁ y) ⇔ (to x ≤₂ to y)
Isomorphism-poset-equal-to-order-isomorphism ass
{laws₁ = laws₁} {laws₂ = laws₂} =
≃⇒≡ univ₁ \$ ↔⇒≃ \$
Isomorphism-poset-isomorphic-to-order-isomorphism ass
{laws₁ = laws₁} {laws₂ = laws₂}
where open Assumptions ass

-- The notion of isomorphism that we get if we use Is-isomorphism′
-- instead of Is-isomorphism is also reasonable.

Isomorphic′-poset :
∀ {C₁ _≤₁_ laws₁ C₂ _≤₂_ laws₂} →

Isomorphic′ poset (C₁ , _≤₁_ , laws₁) (C₂ , _≤₂_ , laws₂)
≡
Σ (C₁ ≃ C₂) λ eq → let open _≃_ eq in
∀ a b → to a ≡ b → ∀ c d → to c ≡ d → ↑ _ ((a ≤₁ c) ≃ (b ≤₂ d))

Isomorphic′-poset = refl _

-- Is-isomorphism, then we could have proved
-- Isomorphism-poset-isomorphic-to-order-isomorphism without assuming
-- univalence, but instead assuming extensionality.

Isomorphism′-poset-isomorphic-to-order-isomorphism :
Extensionality (# 1) (# 1) →
∀ {C₁ _≤₁_ laws₁ C₂ _≤₂_ laws₂} →

Isomorphic′ poset (C₁ , _≤₁_ , laws₁) (C₂ , _≤₂_ , laws₂)
↔
Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
∀ x y → (x ≤₁ y) ⇔ (to x ≤₂ to y)

Isomorphism′-poset-isomorphic-to-order-isomorphism ext
{C₁} {_≤₁_} {laws₁} {C₂} {_≤₂_} {laws₂} =

(Σ (C₁ ≃ C₂) λ eq → let open _≃_ eq in
∀ a b → to a ≡ b → ∀ c d → to c ≡ d → ↑ _ ((a ≤₁ c) ≃ (b ≤₂ d)))  ↝⟨ inverse \$ Σ-cong (↔↔≃ ext (proj₁ laws₁)) (λ _ → _ □) ⟩

(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
∀ a b → to a ≡ b → ∀ c d → to c ≡ d → ↑ _ ((a ≤₁ c) ≃ (b ≤₂ d)))  ↔⟨ inverse \$ ∃-cong (λ _ → ∀-preserves ext λ _ → ↔⇒≃ \$
∀-intro ext λ _ _ → _) ⟩
(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
∀ a c d → to c ≡ d → ↑ _ ((a ≤₁ c) ≃ (to a ≤₂ d)))                ↔⟨ inverse \$ ∃-cong (λ _ → ∀-preserves ext λ _ → ∀-preserves ext λ _ → ↔⇒≃ \$
∀-intro ext λ _ _ → _) ⟩
(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
∀ a c → ↑ _ ((a ≤₁ c) ≃ (to a ≤₂ to c)))                          ↔⟨ ∃-cong (λ _ → ∀-preserves ext λ _ → ∀-preserves ext λ _ → ↔⇒≃
↑↔) ⟩
(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
∀ a c → (a ≤₁ c) ≃ (to a ≤₂ to c))                                ↔⟨ inverse \$ ∃-cong (λ _ →
∀-preserves ext λ _ → ∀-preserves (lower-ext (# 0) _ ext) λ _ → ↔⇒≃ \$
⇔↔≃ (lower-ext _ _ ext) (proj₁ (proj₂ laws₁) _ _)
(proj₁ (proj₂ laws₂) _ _)) ⟩□
(Σ (C₁ ↔ C₂) λ eq → let open _↔_ eq in
∀ a c → (a ≤₁ c) ⇔ (to a ≤₂ to c))                                □

------------------------------------------------------------------------
-- An example: discrete fields

private

-- Some lemmas used below.

0* :
{C : Set₁}
(_+_ : C → C → C)
(0# : C)
(_*_ : C → C → C)
(1# : C)
(-_ : C → C) →
(∀ x y z → (x + (y + z)) ≡ ((x + y) + z)) →
(∀ x y → (x + y) ≡ (y + x)) →
(∀ x y → (x * y) ≡ (y * x)) →
(∀ x y z → (x * (y + z)) ≡ ((x * y) + (x * z))) →
(∀ x → (x + 0#) ≡ x) →
(∀ x → (x * 1#) ≡ x) →
(∀ x → (x + (- x)) ≡ 0#) →
∀ x → (0# * x) ≡ 0#
0* _+_ 0# _*_ 1# -_ +-assoc +-comm *-comm *+ +0 *1 +- x =
(0# * x)                  ≡⟨ sym \$ +0 _ ⟩
((0# * x) + 0#)           ≡⟨ cong (_+_ _) \$ sym \$ +- _ ⟩
((0# * x) + (x + (- x)))  ≡⟨ +-assoc _ _ _ ⟩
(((0# * x) + x) + (- x))  ≡⟨ cong (λ y → y + _) lemma ⟩
(x + (- x))               ≡⟨ +- x ⟩∎
0#                        ∎
where
lemma =
((0# * x) + x)         ≡⟨ cong (_+_ _) \$ sym \$ *1 _ ⟩
((0# * x) + (x * 1#))  ≡⟨ cong (λ y → y + (x * 1#)) \$ *-comm _ _ ⟩
((x * 0#) + (x * 1#))  ≡⟨ sym \$ *+ _ _ _ ⟩
(x * (0# + 1#))        ≡⟨ cong (_*_ _) \$ +-comm _ _ ⟩
(x * (1# + 0#))        ≡⟨ cong (_*_ _) \$ +0 _ ⟩
(x * 1#)               ≡⟨ *1 _ ⟩∎
x                      ∎

dec-lemma₁ :
{C : Set₁}
(_+_ : C → C → C)
(0# : C)
(-_ : C → C) →
(∀ x y z → (x + (y + z)) ≡ ((x + y) + z)) →
(∀ x y → (x + y) ≡ (y + x)) →
(∀ x → (x + 0#) ≡ x) →
(∀ x → (x + (- x)) ≡ 0#) →
(∀ x → Dec (x ≡ 0#)) →
Decidable (_≡_ {A = C})
dec-lemma₁ _+_ 0# -_ +-assoc +-comm +0 +- dec-0 x y =
⊎-map (λ x-y≡0 → x                  ≡⟨ sym \$ +0 _ ⟩
(x + 0#)           ≡⟨ cong (_+_ _) \$ sym \$ +- _ ⟩
(x + (y + (- y)))  ≡⟨ cong (_+_ _) \$ +-comm _ _ ⟩
(x + ((- y) + y))  ≡⟨ +-assoc _ _ _ ⟩
((x + (- y)) + y)  ≡⟨ cong (λ x → x + _) x-y≡0 ⟩
(0# + y)           ≡⟨ +-comm _ _ ⟩
(y + 0#)           ≡⟨ +0 _ ⟩∎
y                  ∎)
(λ x-y≢0 x≡y → x-y≢0 ((x + (- y))  ≡⟨ cong (_+_ _ ∘ -_) \$ sym x≡y ⟩
(x + (- x))  ≡⟨ +- _ ⟩∎
0#           ∎))
(dec-0 (x + (- y)))

dec-lemma₂ :
{C : Set₁}
(_+_ : C → C → C)
(0# : C)
(_*_ : C → C → C)
(1# : C)
(-_ : C → C) →
(_⁻¹ : C → ↑ (# 1) ⊤ ⊎ C) →
(∀ x y z → (x + (y + z)) ≡ ((x + y) + z)) →
(∀ x y → (x + y) ≡ (y + x)) →
(∀ x y → (x * y) ≡ (y * x)) →
(∀ x y z → (x * (y + z)) ≡ ((x * y) + (x * z))) →
(∀ x → (x + 0#) ≡ x) →
(∀ x → (x * 1#) ≡ x) →
(∀ x → (x + (- x)) ≡ 0#) →
0# ≢ 1# →
(∀ x → (x ⁻¹) ≡ inj₁ (lift tt) → x ≡ 0#) →
(∀ x y → (x ⁻¹) ≡ inj₂ y → (x * y) ≡ 1#) →
Decidable (_≡_ {A = C})
dec-lemma₂ _+_ 0# _*_ 1# -_ _⁻¹ +-assoc +-comm *-comm
*+ +0 *1 +- 0≢1 ⁻¹₁ ⁻¹₂ =
dec-lemma₁ _+_ 0# -_ +-assoc +-comm +0 +- dec-0
where
dec-0 : ∀ z → Dec (z ≡ 0#)
dec-0 z with z ⁻¹ | ⁻¹₁ z | ⁻¹₂ z
... | inj₁ _   | hyp | _   = inj₁ (hyp (refl _))
... | inj₂ z⁻¹ | _   | hyp = inj₂ (λ z≡0 →
0≢1 (0#          ≡⟨ sym \$ 0* _+_ 0# _*_ 1# -_ +-assoc +-comm *-comm *+ +0 *1 +- _ ⟩
(0# * z⁻¹)  ≡⟨ cong (λ x → x * _) \$ sym z≡0 ⟩
(z * z⁻¹)   ≡⟨ hyp z⁻¹ (refl _) ⟩∎
1#          ∎))

dec-lemma₃ :
{C : Set₁}
(_+_ : C → C → C)
(0# : C)
(-_ : C → C) →
(_*_ : C → C → C)
(1# : C) →
(∀ x y z → (x + (y + z)) ≡ ((x + y) + z)) →
(∀ x y z → (x * (y * z)) ≡ ((x * y) * z)) →
(∀ x y → (x + y) ≡ (y + x)) →
(∀ x y → (x * y) ≡ (y * x)) →
(∀ x → (x + 0#) ≡ x) →
(∀ x → (x * 1#) ≡ x) →
(∀ x → (x + (- x)) ≡ 0#) →
(∀ x → (∃ λ y → (x * y) ≡ 1#) Xor (x ≡ 0#)) →
Decidable (_≡_ {A = C})
dec-lemma₃ _+_ 0# -_ _*_ 1# +-assoc *-assoc +-comm *-comm +0 *1 +-
inv-xor =
dec-lemma₁ _+_ 0# -_ +-assoc +-comm +0 +-
(λ x → [ inj₂ ∘ proj₂ , inj₁ ∘ proj₂ ] (inv-xor x))

*-injective :
{C : Set₁}
(_*_ : C → C → C)
(1# : C) →
(∀ x y z → (x * (y * z)) ≡ ((x * y) * z)) →
(∀ x y → (x * y) ≡ (y * x)) →
(∀ x → (x * 1#) ≡ x) →
∀ x → ∃ (λ ```