------------------------------------------------------------------------
-- 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 is similar to
-- Univalence-axiom.Isomorphism-is-equality.Simple, but the
-- definitions of isomorphism used below are perhaps closer to the
-- "standard" ones. Carrier types also live in Type rather than Type₁
-- (at the cost of quite a bit of lifting).

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

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

open import Equality

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

open import Bijection eq as B using (_↔_)
open Derived-definitions-and-properties eq
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq using (_≃_)
open import Extensionality eq
  renaming (lower-extensionality to lower-ext)
open import Function-universe eq hiding (id; _∘_)
open import H-level eq
open import H-level.Closure eq
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 : Type₃ where
  field

    -- Univalence at three different levels.

    univ  : Univalence (# )
    univ₁ : Univalence (# )
    univ₂ : Univalence (# )

  opaque

    -- Extensionality.

    ext : Extensionality (# ) (# )
    ext = dependent-extensionality univ₂ univ₁

    ext₀ : Extensionality (# ) (# )
    ext₀ = dependent-extensionality univ₁ univ

-- Universes with some extra stuff.

record Universe : Type₃ where
  field

    -- Codes for something.

    U : Type₁

    -- Interpretation of codes.

    El : U → Type → Type₁

    -- A predicate, possibly specifying what it means for a bijection
    -- to be an isomorphism between two elements.

    Is-isomorphism : ∀ a {B C} → B ↔ C → El a B → El a C → Type₁

    -- El a, seen as a predicate, respects equivalences (assuming
    -- univalence).

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

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

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

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

  Is-isomorphism′ : Assumptions →
                    ∀ a {B C} → B ↔ C → El a B → El a C → Type₁
  Is-isomorphism′ ass a B↔C x y = resp ass a (Eq.↔⇒≃ B↔C) x ≡ y

  field

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

    isomorphism-definitions-isomorphic :
      (ass : Assumptions) →
      ∀ a {B C} (B↔C : B ↔ C) {x y} →
      Is-isomorphism a B↔C x y ↔ Is-isomorphism′ ass a B↔C x y

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

  Is-isomorphism″ : Assumptions →
                    ∀ a {B C} → B ↔ C → El a B → El a C → Type₁
  Is-isomorphism″ ass a B↔C x y =
    subst (El a) (≃⇒≡ univ (Eq.↔⇒≃ B↔C)) x ≡ y
    where open Assumptions ass

  opaque

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

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

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

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

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

module Class (Univ : Universe) where

  open Universe Univ

  -- Codes for structures.

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

    -- A proposition.
    (C : Set (# )) → El a ⌞ C ⌟ → Σ Type₁ λ 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 → Type₁
  Instance (a , P) =
    -- A carrier set.
    Σ (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 → Type
  Carrier _ I = ⌞ proj₁ I ⌟

  -- The "element".

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

  -- 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).

  instances-equal↔ :
    Assumptions →
    ∀ c {I₁ I₂} →
    (I₁ ≡ I₂) ↔
    ∃ λ (C-eq : Carrier c I₁ ≡ Carrier c I₂) →
      subst (El (proj₁ c)) C-eq (element c I₁) ≡ element c I₂
  instances-equal↔ ass (a , P)
                   {(C₁ , S₁) , x₁ , p₁} {(C₂ , S₂) , x₂ , p₂} =

    ((C₁ , λ {_ _} → S₁) , x₁ , p₁) ≡ ((C₂ , λ {_ _} → S₂) , x₂ , p₂)  ↔⟨ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ bij ⟩

    ((C₁ , x₁) , ((λ {_ _} → S₁) , p₁)) ≡
    ((C₂ , x₂) , ((λ {_ _} → S₂) , p₂))                                ↝⟨ inverse $ ignore-propositional-component prop ⟩

    ((C₁ , x₁) ≡ (C₂ , x₂))                                            ↝⟨ inverse B.Σ-≡,≡↔≡ ⟩□

    (∃ λ (C-eq : C₁ ≡ C₂) → subst (El a) C-eq x₁ ≡ x₂)                 □

    where
    bij : Instance (a , P) ↔
          Σ (Σ Type (El a)) λ { (C , x) →
          Σ (Is-set C) λ S → proj₁ (P (C , S) x) }
    bij =
      (Σ (Σ Type Is-set) λ { (C , S) →
         Σ (El a C) λ x → proj₁ (P (C , S) x) })    ↝⟨ inverse Σ-assoc ⟩

      (Σ Type λ C → Σ (Is-set C) λ S →
         Σ (El a C) λ x → proj₁ (P (C , S) x))      ↝⟨ ∃-cong (λ _ → ∃-comm) ⟩

      (Σ Type λ C → Σ (El a C) λ x →
         Σ (Is-set C) λ S → proj₁ (P (C , S) x))    ↝⟨ Σ-assoc ⟩□

      (Σ (Σ Type (El a)) λ { (C , x) →
         Σ (Is-set C) λ S → proj₁ (P (C , S) x) })  □

    prop : Is-proposition
             (Σ (Is-set C₂) λ S₂ → proj₁ (P (C₂ , S₂) x₂))
    prop =
      Σ-closure 
        (H-level-propositional (Assumptions.ext₀ ass) )
        (λ S₂ → proj₂ (P (C₂ , S₂) x₂) ass)

  -- Structure isomorphisms.

  Isomorphic : ∀ c → Instance c → Instance c → Type₁
  Isomorphic (a , _) ((C₁ , _) , x₁ , _) ((C₂ , _) , x₂ , _) =
    Σ (C₁ ↔ C₂) λ C₁↔C₂ → Is-isomorphism a C₁↔C₂ x₁ x₂

  opaque

    -- 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.

    isomorphic↔equal :
      Assumptions →
      ∀ c {I₁ I₂} → Isomorphic c I₁ I₂ ↔ (I₁ ≡ I₂)
    isomorphic↔equal ass c {I₁} {I₂} =

      (∃ λ (C-eq : Carrier c I₁ ↔ Carrier c I₂) →
         Is-isomorphism (proj₁ c) C-eq (element c I₁) (element c I₂))    ↝⟨ ∃-cong (λ C-eq → isomorphism-definitions-isomorphic₂
                                                                                               ass (proj₁ c) C-eq) ⟩
      (∃ λ (C-eq : Carrier c I₁ ↔ Carrier c I₂) →
         subst (El (proj₁ c)) (≃⇒≡ univ (Eq.↔⇒≃ C-eq)) (element c I₁) ≡
         element c I₂)                                                   ↝⟨ Σ-cong (Eq.↔↔≃ ext₀ (proj₂ (proj₁ I₁))) (λ _ → _ □) ⟩

      (∃ λ (C-eq : Carrier c I₁ ≃ Carrier c I₂) →
         subst (El (proj₁ c)) (≃⇒≡ univ C-eq) (element c I₁) ≡
         element c I₂)                                                   ↝⟨ inverse $
                                                                              Σ-cong (≡≃≃ univ) (λ C-eq → ≡⇒↝ _ $ sym $
                                                                                cong (λ eq → subst (El (proj₁ c)) eq (element c I₁) ≡
                                                                                             element c I₂)
                                                                                     (_≃_.left-inverse-of (≡≃≃ univ) C-eq)) ⟩
      (∃ λ (C-eq : Carrier c I₁ ≡ Carrier c I₂) →
         subst (El (proj₁ c)) C-eq (element c I₁) ≡ element c I₂)        ↝⟨ inverse $ instances-equal↔ ass c ⟩□

      (I₁ ≡ I₂)                                                          □

      where open Assumptions ass

    -- The first part of the from component of the preceding lemma is
    -- extensionally equal to a simple function. (The codomain of the
    -- second part is propositional whenever El (proj₁ c) applied to
    -- either carrier type is a set.)

    proj₁-from-isomorphic↔equal :
      ∀ ass c {I J} (I≡J : I ≡ J) →
      proj₁ (_↔_.from (isomorphic↔equal ass c) I≡J) ≡
      _≃_.bijection (≡⇒≃ (cong (proj₁ ∘ proj₁) I≡J))
    proj₁-from-isomorphic↔equal ass (a , P) I≡J =
      let A = Instance (a , P)
          B = Σ (∃ (El a)) λ { (C , x) →
                ∃ λ (S : Is-set C) → proj₁ (P (C , S) x) }
      in

      cong (_≃_.bijection ∘ ≡⇒≃) (
        proj₁ (Σ-≡,≡←≡ (proj₁ (Σ-≡,≡←≡ (cong {B = B}
          (λ { ((C , S) , x , p) → (C , x) , S , p }) I≡J))))            ≡⟨ cong (proj₁ ∘ Σ-≡,≡←≡) $ proj₁-Σ-≡,≡←≡ _ ⟩
        proj₁ (Σ-≡,≡←≡ (cong proj₁ (cong {B = B}
          (λ { ((C , S) , x , p) → (C , x) , S , p }) I≡J)))             ≡⟨ cong (proj₁ ∘ Σ-≡,≡←≡) $
                                                                              cong-∘ {B = B} proj₁
                                                                                     (λ { ((C , S) , x , p) → (C , x) , S , p }) _ ⟩
        proj₁ (Σ-≡,≡←≡ (cong {A = A}
          (λ { ((C , S) , x , p) → C , x }) I≡J))                        ≡⟨ proj₁-Σ-≡,≡←≡ _ ⟩
        cong proj₁ (cong {A = A} (λ { ((C , S) , x , p) → C , x }) I≡J)  ≡⟨ cong-∘ {A = A} proj₁ (λ { ((C , S) , x , p) → C , x }) _ ⟩∎
        cong (proj₁ ∘ proj₁) I≡J                                         ∎)

    -- 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≡equal :
      Assumptions →
      ∀ c {I₁ I₂} → Isomorphic c I₁ I₂ ≡ (I₁ ≡ I₂)
    isomorphic≡equal ass c {I₁} {I₂} =
      ≃⇒≡ univ₁ $ Eq.↔⇒≃ (isomorphic↔equal ass c)
      where open Assumptions ass

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

-- Codes for types.

infixr  _⊗_
infixr  _⊕_
infixr  _⇾_

data U : Type₁ where
  id prop     : U
  k           : Type → U
  _⇾_ _⊕_ _⊗_ : U → U → U

-- Interpretation of types.

El : U → Type₁ → Type₁
El id      B = B
El prop    B = Proposition (# )
El (k A)   B = ↑ _ A
El (a ⇾ b) B = El a B → El b B
El (a ⊕ b) B = El a B ⊎ El b B
El (a ⊗ b) B = El a B × El b B

-- El a preserves equivalences (assuming extensionality).

cast : Extensionality (# ) (# ) →
       ∀ a {B C} → B ≃ C → El a B ≃ El a C
cast ext id      B≃C = B≃C
cast ext prop    B≃C = Eq.id
cast ext (k A)   B≃C = Eq.id
cast ext (a ⇾ b) B≃C = →-cong ext (cast ext a B≃C) (cast ext b B≃C)
cast ext (a ⊕ b) B≃C = cast ext a B≃C ⊎-cong cast ext b B≃C
cast ext (a ⊗ b) B≃C = cast ext a B≃C ×-cong cast ext b B≃C

opaque

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

  cast-id : (ext : Extensionality (# ) (# )) →
            ∀ a {B} → cast ext a (Eq.id {A = B}) ≡ Eq.id
  cast-id ext id      = refl _
  cast-id ext prop    = refl _
  cast-id ext (k A)   = refl _
  cast-id ext (a ⇾ b) = Eq.lift-equality ext $ cong _≃_.to $
                          cong₂ (→-cong ext) (cast-id ext a) (cast-id ext b)
  cast-id ext (a ⊗ b) = Eq.lift-equality ext $ cong _≃_.to $
                          cong₂ _×-cong_ (cast-id ext a) (cast-id ext b)
  cast-id ext (a ⊕ b) =
    cast ext a Eq.id ⊎-cong cast ext b Eq.id  ≡⟨ cong₂ _⊎-cong_ (cast-id ext a) (cast-id ext b) ⟩
    Eq.⟨ [ inj₁ , inj₂ ] , _ ⟩                ≡⟨ Eq.lift-equality ext (apply-ext ext [ refl ∘ inj₁ , refl ∘ inj₂ ]) ⟩∎
    Eq.id                                     ∎

-- The property of being an isomorphism between two elements.

Is-isomorphism : ∀ a {B C} → B ↔ C → El a B → El a C → Type₁
Is-isomorphism id      B↔C = λ x y → _↔_.to B↔C x ≡ y
Is-isomorphism prop    B↔C = λ { (P , _) (Q , _) → ↑ _ (P ⇔ Q) }
Is-isomorphism (k A)   B↔C = λ x y → x ≡ y
Is-isomorphism (a ⇾ b) B↔C = Is-isomorphism a B↔C →-rel
                             Is-isomorphism b B↔C
Is-isomorphism (a ⊕ b) B↔C = Is-isomorphism a B↔C ⊎-rel
                             Is-isomorphism b B↔C
Is-isomorphism (a ⊗ b) B↔C = Is-isomorphism a B↔C ×-rel
                             Is-isomorphism b B↔C

-- Another definition of "being an isomorphism" (defined using
-- extensionality).

Is-isomorphism′ : Extensionality (# ) (# ) →
                  ∀ a {B C} → B ↔ C → El a B → El a C → Type₁
Is-isomorphism′ ext a B↔C x y = _≃_.to (cast ext a (Eq.↔⇒≃ B↔C)) x ≡ y

opaque

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

  isomorphism-definitions-isomorphic :
    (ass : Assumptions) → let open Assumptions ass in
    ∀ a {B C} (B↔C : B ↔ C) {x y} →
    Is-isomorphism a B↔C x y ↔ Is-isomorphism′ ext a B↔C x y

  isomorphism-definitions-isomorphic ass id B↔C {x} {y} =

    (_↔_.to B↔C x ≡ y)  □

  isomorphism-definitions-isomorphic ass prop B↔C {x = P} {y = Q} =

    ↑ _ (proj₁ P ⇔ proj₁ Q)  ↝⟨ B.↑↔ ⟩

    (proj₁ P ⇔ proj₁ Q)      ↝⟨ Eq.⇔↔≃ ext₀ (proj₂ P) (proj₂ Q) ⟩

    (proj₁ P ≃ proj₁ Q)      ↔⟨ inverse $ ≡≃≃ univ ⟩

    (proj₁ P ≡ proj₁ Q)      ↝⟨ ignore-propositional-component (H-level-propositional ext₀ ) ⟩□

    (P ≡ Q)                □

    where open Assumptions ass

  isomorphism-definitions-isomorphic ass (k A) B↔C {x} {y} =

    (x ≡ y) □

  isomorphism-definitions-isomorphic ass (a ⇾ b) B↔C {x = f} {y = g} =
    let B≃C = Eq.↔⇒≃ B↔C in

    (∀ x y → Is-isomorphism a B↔C x y →
             Is-isomorphism b B↔C (f x) (g y))                     ↝⟨ ∀-cong ext (λ _ → ∀-cong ext λ _ →
                                                                        →-cong ext (isomorphism-definitions-isomorphic ass a B↔C)
                                                                                   (isomorphism-definitions-isomorphic ass b B↔C)) ⟩
    (∀ x y → to (cast ext a B≃C) x ≡ y →
             to (cast ext b B≃C) (f x) ≡ g y)                      ↝⟨ inverse $ ∀-cong ext (λ x →
                                                                        ∀-intro (λ y _ → to (cast ext b B≃C) (f x) ≡ g y) ext) ⟩
    (∀ x → to (cast ext b B≃C) (f x) ≡ g (to (cast ext a B≃C) x))  ↔⟨ Eq.extensionality-isomorphism ext ⟩

    (to (cast ext b B≃C) ∘ f ≡ g ∘ to (cast ext a B≃C))            ↝⟨ inverse $ ∘from≡↔≡∘to ext (cast ext a B≃C) ⟩□

    (to (cast ext b B≃C) ∘ f ∘ from (cast ext a B≃C) ≡ g)          □

    where
    open _≃_
    open Assumptions ass

  isomorphism-definitions-isomorphic
    ass (a ⊕ b) B↔C {x = inj₁ x} {y = inj₁ y} =
    let B≃C = Eq.↔⇒≃ B↔C in

    Is-isomorphism a B↔C x y                 ↝⟨ isomorphism-definitions-isomorphic ass a B↔C ⟩

    (to (cast ext a B≃C) x ≡ y)              ↝⟨ B.≡↔inj₁≡inj₁ ⟩□

    (inj₁ (to (cast ext a B≃C) x) ≡ inj₁ y)  □

    where
    open _≃_
    open Assumptions ass

  isomorphism-definitions-isomorphic
    ass (a ⊕ b) B↔C {x = inj₂ x} {y = inj₂ y} =
    let B≃C = Eq.↔⇒≃ B↔C in

    Is-isomorphism b B↔C x y                 ↝⟨ isomorphism-definitions-isomorphic ass b B↔C ⟩

    (to (cast ext b B≃C) x ≡ y)              ↝⟨ B.≡↔inj₂≡inj₂ ⟩□

    (inj₂ (to (cast ext b B≃C) x) ≡ inj₂ y)  □

    where
    open _≃_
    open Assumptions ass

  isomorphism-definitions-isomorphic
    ass (a ⊕ b) B↔C {x = inj₁ x} {y = inj₂ y} =

    ⊥                  ↝⟨ B.⊥↔uninhabited ⊎.inj₁≢inj₂ ⟩□

    (inj₁ _ ≡ inj₂ _)  □

  isomorphism-definitions-isomorphic
    ass (a ⊕ b) B↔C {x = inj₂ x} {y = inj₁ y} =

    ⊥                  ↝⟨ B.⊥↔uninhabited (⊎.inj₁≢inj₂ ∘ sym) ⟩□

    (inj₂ _ ≡ inj₁ _)  □

  isomorphism-definitions-isomorphic
    ass (a ⊗ b) B↔C {x = x , u} {y = y , v} =
    let B≃C = Eq.↔⇒≃ B↔C in

    Is-isomorphism  a B↔C x y × Is-isomorphism  b B↔C u v        ↝⟨ isomorphism-definitions-isomorphic ass a B↔C ×-cong
                                                                    isomorphism-definitions-isomorphic ass b B↔C ⟩
    (to (cast ext a B≃C) x ≡ y × to (cast ext b B≃C) u ≡ v)      ↝⟨ ≡×≡↔≡ ⟩□

    ((to (cast ext a B≃C) x , to (cast ext b B≃C) u) ≡ (y , v))  □

    where
    open _≃_
    open Assumptions ass

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

simple : Universe
simple = record
  { U              = U
  ; El             = λ a → El a ∘ ↑ _
  ; Is-isomorphism = λ a B↔C → Is-isomorphism a (↑-cong B↔C)
  ; resp           = λ ass a → _≃_.to ∘ cast (ext ass) a ∘ ↑-cong
  ; resp-id        = λ ass a x → cong (λ f → _≃_.to f x) (
                       cast (ext ass) a (↑-cong Eq.id)  ≡⟨ cong (cast (ext ass) a) $ Eq.lift-equality (ext ass) (refl _) ⟩
                       cast (ext ass) a Eq.id           ≡⟨ cast-id (ext ass) a ⟩∎
                       Eq.id                            ∎)
  ; isomorphism-definitions-isomorphic = λ ass a B↔C {x y} →
      Is-isomorphism a (↑-cong B↔C) x y                        ↝⟨ isomorphism-definitions-isomorphic ass a (↑-cong B↔C) ⟩
      (_≃_.to (cast (ext ass) a (Eq.↔⇒≃ (↑-cong B↔C))) x ≡ y)  ↝⟨ ≡⇒↝ _ $ cong (λ eq → _≃_.to (cast (ext ass) a eq) x ≡ y) $
                                                                    Eq.lift-equality (ext ass) (refl _) ⟩□
      (_≃_.to (cast (ext ass) a (↑-cong (Eq.↔⇒≃ B↔C))) x ≡ y)  □
  }
  where open Assumptions

-- Let us use this universe in the examples below.

open Class simple

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

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

  -- Identity.
  id ,

  λ { (_ , M-set) (_∙_ , e) →

      (-- 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
        ×-closure   (Π-closure ext  λ _ →
                      ↑-closure  M-set)
        (×-closure  (Π-closure ext  λ _ →
                      ↑-closure  M-set)
                     (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  M-set)) }

-- The interpretation of the code is reasonable.

Instance-monoid :

  Instance monoid
    ≡
  Σ (Set (# )) λ { (M , _) →
  Σ ((↑ _ M → ↑ _ M → ↑ _ M) × ↑ _ M) λ { (_∙_ , e) →
  (∀ 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 :
  ∀ {M₁} {S₁ : Is-set M₁} {_∙₁_ e₁ laws₁}
    {M₂} {S₂ : Is-set M₂} {_∙₂_ e₂ laws₂} →

  Isomorphic monoid ((M₁ , S₁) , (_∙₁_ , e₁) , laws₁)
                    ((M₂ , S₂) , (_∙₂_ , e₂) , laws₂)
    ≡
  Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
  (∀ x y → to x ≡ y → ∀ u v → to u ≡ v → to (x ∙₁ u) ≡ (y ∙₂ v)) ×
  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 (# ) (# ) →
  ∀ {M₁} {S₁ : Is-set M₁} {_∙₁_ e₁ laws₁}
    {M₂} {S₂ : Is-set M₂} {_∙₂_ e₂ laws₂} →

  Isomorphic monoid ((M₁ , S₁) , (_∙₁_ , e₁) , laws₁)
                    ((M₂ , S₂) , (_∙₂_ , e₂) , laws₂)
    ↔
  Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
  (∀ x y → to (x ∙₁ y) ≡ (to x ∙₂ to y)) ×
  to e₁ ≡ e₂

Isomorphism-monoid-isomorphic-to-standard ext
  {M₁} {S₁} {_∙₁_} {e₁} {M₂} {_∙₂_} {e₂} =

  (Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
   (∀ x y → to x ≡ y → ∀ u v → to u ≡ v → to (x ∙₁ u) ≡ (y ∙₂ v)) ×
   to e₁ ≡ e₂)                                                       ↝⟨ inverse $ ∃-cong (λ _ →
                                                                          (∀-cong ext λ _ → ∀-intro (λ _ _ → _) ext) ×-cong (_ □)) ⟩
  (Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
   (∀ x u v → to u ≡ v → to (x ∙₁ u) ≡ (to x ∙₂ v)) ×
   to e₁ ≡ e₂)                                                       ↝⟨ inverse $ ∃-cong (λ _ →
                                                                          (∀-cong ext λ _ → ∀-cong ext λ _ → ∀-intro (λ _ _ → _) ext)
                                                                            ×-cong
                                                                          (_ □)) ⟩□
  (Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
   (∀ x u → to (x ∙₁ u) ≡ (to x ∙₂ to u)) ×
   to e₁ ≡ e₂)                                                       □

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

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

  λ { (P , P-set) Le →

    let _≤_ : ↑ _ P → ↑ _ P → Type
        _≤_ x y = proj₁ (Le x y)
    in

     -- 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
      ×-closure   (Π-closure (lower-ext (# ) _ ext)  λ _ →
                    proj₂ (Le _ _))
      (×-closure  (Π-closure ext                      λ _ →
                    Π-closure ext                      λ _ →
                    Π-closure (lower-ext (# ) _ ext)  λ _ →
                    Π-closure ext₀                     λ _ →
                    Π-closure ext₀                     λ _ →
                    proj₂ (Le _ _))
                   (Π-closure ext                      λ _ →
                    Π-closure ext                      λ _ →
                    Π-closure (lower-ext _ (# ) ext)  λ _ →
                    Π-closure (lower-ext _ (# ) ext)  λ _ →
                    ↑-closure  P-set)) }

-- The interpretation of the code is reasonable.

Instance-poset :

  Instance poset
    ≡
  Σ (Set (# )) λ { (P , _) →
  Σ (↑ _ P → ↑ _ P → Proposition (# )) λ Le →
  let _≤_ : ↑ _ P → ↑ _ P → Type
      _≤_ x y = proj₁ (Le x y)
  in
  (∀ 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".

Isomorphic-poset :
  ∀ {P₁} {S₁ : Is-set P₁} {Le₁ laws₁}
    {P₂} {S₂ : Is-set P₂} {Le₂ laws₂} →
  let _≤₁_ : ↑ _ P₁ → ↑ _ P₁ → Type
      _≤₁_ x y = proj₁ (Le₁ x y)

      _≤₂_ : ↑ _ P₂ → ↑ _ P₂ → Type
      _≤₂_ x y = proj₁ (Le₂ x y)
  in

  Isomorphic poset ((P₁ , S₁) , Le₁ , laws₁) ((P₂ , S₂) , Le₂ , laws₂)
    ≡
  Σ (P₁ ↔ P₂) λ P₁↔P₂ → let open _↔_ (↑-cong P₁↔P₂) in
  ∀ a b → to a ≡ b → ∀ c d → to c ≡ d → ↑ _ ((a ≤₁ c) ⇔ (b ≤₂ d))

Isomorphic-poset = refl _

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

-- Discrete fields.

discrete-field : Code
discrete-field =
  -- Addition.
  (id ⇾ id ⇾ id) ⊗

  -- Zero.
  id ⊗

  -- Multiplication.
  (id ⇾ id ⇾ id) ⊗

  -- One.
  id ⊗

  -- Minus.
  (id ⇾ id) ⊗

  -- Multiplicative inverse (a partial operation).
  (id ⇾ k ⊤ ⊕ id) ,

  λ { (_ , F-set) (_+_ , 0# , _*_ , 1# , -_ , _⁻¹) →

       -- Associativity.
      ((∀ x y z → (x + (y + z)) ≡ ((x + y) + z)) ×
       (∀ x y z → (x * (y * z)) ≡ ((x * y) * z)) ×

       -- Commutativity.
       (∀ x y → (x + y) ≡ (y + x)) ×
       (∀ x y → (x * y) ≡ (y * x)) ×

       -- Distributivity.
       (∀ x y z → (x * (y + z)) ≡ ((x * y) + (x * z))) ×

       -- Identity laws.
       (∀ x → (x + 0#) ≡ x) ×
       (∀ x → (x * 1#) ≡ x) ×

       -- Zero and one are distinct.
       0# ≢ 1# ×

       -- Inverse laws.
       (∀ x → (x + (- x)) ≡ 0#) ×
       (∀ x → (x ⁻¹) ≡ inj₁ (lift tt) → x ≡ 0#) ×
       (∀ x y → (x ⁻¹) ≡ inj₂ y → (x * y) ≡ 1#)) ,

      λ ass → let open Assumptions ass in
        ×-closure   (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  F-set)
        (×-closure  (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  F-set)
        (×-closure  (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  F-set)
        (×-closure  (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  F-set)
        (×-closure  (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  F-set)
        (×-closure  (Π-closure ext  λ _ →
                      ↑-closure  F-set)
        (×-closure  (Π-closure ext  λ _ →
                      ↑-closure  F-set)
        (×-closure  (Π-closure (lower-ext (# ) (# ) ext)  λ _ →
                      ⊥-propositional)
        (×-closure  (Π-closure ext  λ _ →
                      ↑-closure  F-set)
        (×-closure  (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  F-set)
                     (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  F-set)))))))))) }

-- The interpretation of the code is reasonable.

Instance-discrete-field :

  Instance discrete-field
    ≡
  Σ (Set (# )) λ { (F , _) →
  Σ ((↑ _ F → ↑ _ F → ↑ _ F) × ↑ _ F × (↑ _ F → ↑ _ F → ↑ _ F) ×
     ↑ _ F × (↑ _ F → ↑ _ F) × (↑ _ F → ↑ (# ) ⊤ ⊎ ↑ _ F))
    λ { (_+_ , 0# , _*_ , 1# , -_ , _⁻¹) →
  (∀ 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 y z → (x * (y + z)) ≡ ((x * y) + (x * z))) ×
  (∀ x → (x + 0#) ≡ x) ×
  (∀ x → (x * 1#) ≡ x) ×
  0# ≢ 1# ×
  (∀ x → (x + (- x)) ≡ 0#) ×
  (∀ x → (x ⁻¹) ≡ inj₁ (lift tt) → x ≡ 0#) ×
  (∀ x y → (x ⁻¹) ≡ inj₂ y → (x * y) ≡ 1#) }}

Instance-discrete-field = refl _

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

Isomorphic-discrete-field :
  ∀ {F₁} {S₁ : Is-set F₁} {_+₁_ 0₁ _*₁_ 1₁ -₁_ _⁻¹₁ laws₁}
    {F₂} {S₂ : Is-set F₂} {_+₂_ 0₂ _*₂_ 1₂ -₂_ _⁻¹₂ laws₂} →

  Isomorphic discrete-field
    ((F₁ , S₁) , (_+₁_ , 0₁ , _*₁_ , 1₁ , -₁_ , _⁻¹₁) , laws₁)
    ((F₂ , S₂) , (_+₂_ , 0₂ , _*₂_ , 1₂ , -₂_ , _⁻¹₂) , laws₂)
    ≡
  Σ (F₁ ↔ F₂) λ F₁↔F₂ → let open _↔_ (↑-cong F₁↔F₂) in
  (∀ x y → to x ≡ y → ∀ u v → to u ≡ v → to (x +₁ u) ≡ (y +₂ v)) ×
  to 0₁ ≡ 0₂ ×
  (∀ x y → to x ≡ y → ∀ u v → to u ≡ v → to (x *₁ u) ≡ (y *₂ v)) ×
  to 1₁ ≡ 1₂ ×
  (∀ x y → to x ≡ y → to (-₁ x) ≡ (-₂ y)) ×
  (∀ x y → to x ≡ y →
     ((λ _ _ → lift tt ≡ lift tt) ⊎-rel (λ u v → to u ≡ v))
       (x ⁻¹₁) (y ⁻¹₂))

Isomorphic-discrete-field = refl _

------------------------------------------------------------------------
-- An example: vector spaces over discrete fields

-- Vector spaces over a particular discrete field.

vector-space : Instance discrete-field → Code
vector-space ((F , _) , (_+F_ , _ , _*F_ , 1F , _ , _) , _) =
  -- Addition.
  (id ⇾ id ⇾ id) ⊗

  -- Scalar multiplication.
  (k F ⇾ id ⇾ id) ⊗

  -- Zero vector.
  id ⊗

  -- Additive inverse.
  (id ⇾ id) ,

  λ { (_ , V-set) (_+_ , _*_ , 0V , -_) →

       -- Associativity.
      ((∀ u v w → (u + (v + w)) ≡ ((u + v) + w)) ×
       (∀ x y v → (x * (y * v)) ≡ ((x *F y) * v)) ×

       -- Commutativity.
       (∀ u v → (u + v) ≡ (v + u)) ×

       -- Distributivity.
       (∀ x u v → (x * (u + v)) ≡ ((x * u) + (x * v))) ×
       (∀ x y v → ((x +F y) * v) ≡ ((x * v) + (y * v))) ×

       -- Identity laws.
       (∀ v → (v + 0V) ≡ v) ×
       (∀ v → (1F * v) ≡ v) ×

       -- Inverse law.
       (∀ v → (v + (- v)) ≡ 0V)) ,

      λ ass → let open Assumptions ass in
        ×-closure   (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  V-set)
        (×-closure  (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  V-set)
        (×-closure  (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  V-set)
        (×-closure  (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  V-set)
        (×-closure  (Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      Π-closure ext  λ _ →
                      ↑-closure  V-set)
        (×-closure  (Π-closure ext  λ _ →
                      ↑-closure  V-set)
        (×-closure  (Π-closure ext  λ _ →
                      ↑-closure  V-set)
                     (Π-closure ext  λ _ →
                      ↑-closure  V-set))))))) }

-- The interpretation of the code is reasonable.

Instance-vector-space :
  ∀ {F} {S : Is-set F} {_+F_ 0F _*F_ 1F -F_ _⁻¹F laws} →

  Instance (vector-space
              ((F , S) , (_+F_ , 0F , _*F_ , 1F , -F_ , _⁻¹F) , laws))
    ≡
  Σ (Set (# )) λ { (V , _) →
  Σ ((↑ _ V → ↑ _ V → ↑ _ V) × (↑ _ F → ↑ _ V → ↑ _ V) × ↑ _ V ×
     (↑ _ V → ↑ _ V))
    λ { (_+_ , _*_ , 0V , -_) →
  (∀ u v w → (u + (v + w)) ≡ ((u + v) + w)) ×
  (∀ x y v → (x * (y * v)) ≡ ((x *F y) * v)) ×
  (∀ u v → (u + v) ≡ (v + u)) ×
  (∀ x u v → (x * (u + v)) ≡ ((x * u) + (x * v))) ×
  (∀ x y v → ((x +F y) * v) ≡ ((x * v) + (y * v))) ×
  (∀ v → (v + 0V) ≡ v) ×
  (∀ v → (1F * v) ≡ v) ×
  (∀ v → (v + (- v)) ≡ 0V) }}

Instance-vector-space = refl _

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

Isomorphic-vector-space :
  ∀ {F V₁} {S₁ : Is-set V₁} {_+₁_ _*₁_ 0₁ -₁_ laws₁}
      {V₂} {S₂ : Is-set V₂} {_+₂_ _*₂_ 0₂ -₂_ laws₂} →

  Isomorphic (vector-space F)
             ((V₁ , S₁) , (_+₁_ , _*₁_ , 0₁ , -₁_) , laws₁)
             ((V₂ , S₂) , (_+₂_ , _*₂_ , 0₂ , -₂_) , laws₂)
    ≡
  Σ (V₁ ↔ V₂) λ V₁↔V₂ → let open _↔_ (↑-cong V₁↔V₂) in
  (∀ a b → to a ≡ b → ∀ u v → to u ≡ v → to (a +₁ u) ≡ (b +₂ v)) ×
  (∀ x y →    x ≡ y → ∀ u v → to u ≡ v → to (x *₁ u) ≡ (y *₂ v)) ×
  to 0₁ ≡ 0₂ ×
  (∀ u v → to u ≡ v → to (-₁ u) ≡ (-₂ v))

Isomorphic-vector-space = refl _

------------------------------------------------------------------------
-- An example: sets equipped with fixpoint operators

set-with-fixpoint-operator : Code
set-with-fixpoint-operator =
  (id ⇾ id) ⇾ id ,

  λ { (_ , F-set) fix →

     -- The fixpoint operator property.
    (∀ f → f (fix f) ≡ fix f) ,

    λ ass → let open Assumptions ass in
      Π-closure ext  λ _ →
      ↑-closure  F-set }

-- The usual unfolding lemmas.

Instance-set-with-fixpoint-operator :

  Instance set-with-fixpoint-operator
    ≡
  Σ (Set (# )) λ { (F , _) →
  Σ ((↑ _ F → ↑ _ F) → ↑ _ F) λ fix →
  ∀ f → f (fix f) ≡ fix f }

Instance-set-with-fixpoint-operator = refl _

Isomorphic-set-with-fixpoint-operator :
  ∀ {F₁} {S₁ : Is-set F₁} {fix₁ law₁}
    {F₂} {S₂ : Is-set F₂} {fix₂ law₂} →

  Isomorphic set-with-fixpoint-operator
             ((F₁ , S₁) , fix₁ , law₁) ((F₂ , S₂) , fix₂ , law₂)
    ≡
  Σ (F₁ ↔ F₂) λ F₁↔F₂ → let open _↔_ (↑-cong F₁↔F₂) in
  ∀ f g → (∀ x y → to x ≡ y → to (f x) ≡ g y) → to (fix₁ f) ≡ fix₂ g

Isomorphic-set-with-fixpoint-operator = refl _