------------------------------------------------------------------------
-- 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.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 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′
-- instead of 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 _

-- If we had defined isomorphism using Is-isomorphism′ instead of
-- 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    y  x * y  1#)  Injective (_*_ x)
  *-injective _*_ 1# *-assoc *-comm *1 x (x⁻¹ , xx⁻¹≡1)
             {y₁} {y₂} xy₁≡xy₂ =
    y₁              ≡⟨ lemma y₁ 
    x⁻¹ *