Martin Escardo, 30 April 2020

This ports the structure identity principle examples formulated and proved in

 https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/index.html
 https://arxiv.org/abs/1911.00580
 https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

Each example is in a submodule:

  * ∞-magma
  * magma
  * pointed type
  * pointed-∞-magma
  * monoid
  * associative ∞-magma
  * group
  * subgroups of an ambient group
  * ring
  * slice
  * generalized metric space
  * generalized topological space
  * selection space
  * contrived example
  * generalized functor algebra
  * type-valued preorder
  * type-valued preorder with- xioms
  * category

We also consider the following, which are not in the above lecture
notes:

  * universe à la Tarski
  * ∞-bigmagma
  * ∞-hugemagma

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

module UF.SIP-Examples where

open import MLTT.Spartan
open import Notation.Order

open import UF.Base
open import UF.SIP
open import UF.Equiv hiding (_≅_)
open import UF.Univalence
open import UF.EquivalenceExamples
open import UF.Subsingletons
open import UF.Embeddings
open import UF.Subsingletons-FunExt
open import UF.FunExt
open import UF.UA-FunExt
open import UF.Retracts
open import UF.Yoneda

module ∞-magma {𝓤 : Universe} where

 open sip

 ∞-magma-structure : 𝓤 ̇ → 𝓤 ̇
 ∞-magma-structure X = X → X → X

 ∞-Magma : 𝓤 ⁺ ̇
 ∞-Magma = Σ X ꞉ 𝓤 ̇ , ∞-magma-structure X

 sns-data : SNS ∞-magma-structure 𝓤
 sns-data = (ι , ρ , θ)
  where
   ι : (A B : ∞-Magma) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓤 ̇
   ι (X , _·_) (Y , _*_) (f , _) = (λ x x' → f (x · x')) ＝ (λ x x' → f x * f x')

   ρ : (A : ∞-Magma) → ι A A (≃-refl ⟨ A ⟩)
   ρ (X , _·_) = 𝓻𝓮𝒻𝓵  _·_

   h : {X : 𝓤 ̇ } {_·_ _*_ : ∞-magma-structure X}
     → canonical-map ι ρ _·_ _*_ ∼ -id (_·_ ＝ _*_)

   h (refl {_·_}) = 𝓻𝓮𝒻𝓵 (𝓻𝓮𝒻𝓵 _·_)

   θ : {X : 𝓤 ̇ } (_·_ _*_ : ∞-magma-structure X)
     → is-equiv (canonical-map ι ρ _·_ _*_)

   θ _·_ _*_ = equiv-closed-under-∼ _ _ (id-is-equiv (_·_ ＝ _*_)) h

 _≅_ : ∞-Magma → ∞-Magma → 𝓤 ̇

 (X , _·_) ≅ (Y , _*_) =

           Σ f ꞉ (X → Y) , is-equiv f
                         × ((λ x x' → f (x · x')) ＝ (λ x x' → f x * f x'))

 characterization-of-∞-Magma-＝ : is-univalent 𝓤 → (A B : ∞-Magma) → (A ＝ B) ≃ (A ≅ B)
 characterization-of-∞-Magma-＝ ua = characterization-of-＝ ua sns-data

 characterization-of-characterization-of-∞-Magma-＝ :

    (ua : is-univalent 𝓤) (A : ∞-Magma)
  →
    ⌜ characterization-of-∞-Magma-＝ ua A A ⌝ (𝓻𝓮𝒻𝓵 A)
  ＝
    (-id ⟨ A ⟩ , id-is-equiv ⟨ A ⟩ , refl)

 characterization-of-characterization-of-∞-Magma-＝ ua A = refl


module magma {𝓤 : Universe} where

 open sip-with-axioms

 Magma : 𝓤 ⁺ ̇
 Magma = Σ X ꞉ 𝓤 ̇ , (X → X → X) × is-set X

 _≅_ : Magma → Magma → 𝓤 ̇

 (X , _·_ , _) ≅ (Y , _*_ , _) =

               Σ f ꞉ (X → Y), is-equiv f
                            × ((λ x x' → f (x · x')) ＝ (λ x x' → f x * f x'))

 characterization-of-Magma-＝ : is-univalent 𝓤 → (A B : Magma ) → (A ＝ B) ≃ (A ≅ B)
 characterization-of-Magma-＝ ua =
   characterization-of-＝-with-axioms ua
     ∞-magma.sns-data
     (λ X s → is-set X)
     (λ X s → being-set-is-prop (univalence-gives-funext ua))

module pointed-type {𝓤 : Universe} where
 open sip

 Pointed : 𝓤 ̇ → 𝓤 ̇
 Pointed X = X

 sns-data : SNS Pointed 𝓤
 sns-data = (ι , ρ , θ)
  where
   ι : (A B : Σ Pointed) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓤 ̇
   ι (X , x₀) (Y , y₀) (f , _) = (f x₀ ＝ y₀)

   ρ : (A : Σ Pointed) → ι A A (≃-refl ⟨ A ⟩)
   ρ (X , x₀) = 𝓻𝓮𝒻𝓵 x₀

   θ : {X : 𝓤 ̇ } (x₀ x₁ : Pointed X) → is-equiv (canonical-map ι ρ x₀ x₁)
   θ x₀ x₁ = equiv-closed-under-∼ _ _ (id-is-equiv (x₀ ＝ x₁)) h
    where
     h : canonical-map ι ρ x₀ x₁ ∼ -id (x₀ ＝ x₁)
     h (refl {x₀}) = 𝓻𝓮𝒻𝓵 (𝓻𝓮𝒻𝓵 x₀)

 _≅_ : Σ Pointed → Σ Pointed → 𝓤 ̇
 (X , x₀) ≅ (Y , y₀) = Σ f ꞉ (X → Y), is-equiv f × (f x₀ ＝ y₀)

 characterization-of-pointed-type-＝ : is-univalent 𝓤
                                    → (A B : Σ Pointed)

                                    → (A ＝ B) ≃ (A ≅ B)

 characterization-of-pointed-type-＝ ua = characterization-of-＝ ua sns-data

module pointed-∞-magma {𝓤 : Universe} where

 open sip-join

 ∞-Magma· : 𝓤 ⁺ ̇
 ∞-Magma· = Σ X ꞉ 𝓤 ̇ , (X → X → X) × X

 _≅_ : ∞-Magma· → ∞-Magma· → 𝓤 ̇

 (X ,  _·_ , x₀) ≅ (Y ,  _*_ , y₀) =

                 Σ f ꞉ (X → Y), is-equiv f
                              × ((λ x x' → f (x · x')) ＝ (λ x x' → f x * f x'))
                              × (f x₀ ＝ y₀)

 characterization-of-pointed-magma-＝ : is-univalent 𝓤
                                     → (A B : ∞-Magma·)

                                     → (A ＝ B) ≃ (A ≅ B)

 characterization-of-pointed-magma-＝ ua = characterization-of-join-＝ ua
                                            ∞-magma.sns-data
                                            pointed-type.sns-data

module monoid {𝓤 : Universe} where

 open sip
 open sip-join
 open sip-with-axioms

 monoid-structure : 𝓤 ̇ → 𝓤 ̇
 monoid-structure X = (X → X → X) × X

 monoid-axioms : (X : 𝓤 ̇ ) → monoid-structure X → 𝓤 ̇
 monoid-axioms X (_·_ , e) = is-set X
                           × left-neutral  e _·_
                           × right-neutral e _·_
                           × associative     _·_

 Monoid : 𝓤 ⁺ ̇
 Monoid = Σ X ꞉ 𝓤 ̇ , Σ s ꞉ monoid-structure X , monoid-axioms X s

 monoid-axioms-is-prop : funext 𝓤 𝓤
                       → (X : 𝓤 ̇ ) (s : monoid-structure X)
                       → is-prop (monoid-axioms X s)

 monoid-axioms-is-prop fe X (_·_ , e) s = γ s
  where
   i : is-set X
   i = pr₁ s

   γ : is-prop (monoid-axioms X (_·_ , e))
   γ = ×-is-prop
         (being-set-is-prop fe)
      (×-is-prop
         (Π-is-prop fe
           (λ x → i {e · x} {x}))
      (×-is-prop
         (Π-is-prop fe
           (λ x → i {x · e} {x}))
         (Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → Π-is-prop fe
           (λ z → i {(x · y) · z} {x · (y · z)}))))))

 sns-data : funext 𝓤 𝓤
          → SNS (λ X → Σ s ꞉ monoid-structure X , monoid-axioms X s) 𝓤
 sns-data fe = add-axioms
                monoid-axioms (monoid-axioms-is-prop fe)
                (join
                   ∞-magma.sns-data
                   pointed-type.sns-data)

 _≅_ : Monoid → Monoid → 𝓤 ̇

 (X , (_·_ , d) , _) ≅ (Y , (_*_ , e) , _) =

                     Σ f ꞉ (X → Y), is-equiv f
                                  × ((λ x x' → f (x · x')) ＝ (λ x x' → f x * f x'))
                                  × (f d ＝ e)

 characterization-of-monoid-＝ : is-univalent 𝓤
                              → (A B : Monoid)

                              → (A ＝ B) ≃ (A ≅ B)

 characterization-of-monoid-＝ ua = characterization-of-＝ ua
                                    (sns-data (univalence-gives-funext ua))

module associative-∞-magma
        {𝓤 : Universe}
        (ua : is-univalent 𝓤)
       where

 abstract
  fe : funext 𝓤 𝓤
  fe = univalence-gives-funext ua

 ∞-amagma-structure : 𝓤 ̇ → 𝓤 ̇
 ∞-amagma-structure X = Σ _·_ ꞉ (X → X → X), (associative _·_)

 ∞-aMagma : 𝓤 ⁺ ̇
 ∞-aMagma = Σ X ꞉ 𝓤 ̇ , ∞-amagma-structure X

 homomorphic : {X Y : 𝓤 ̇ } → (X → X → X) → (Y → Y → Y) → (X → Y) → 𝓤 ̇
 homomorphic _·_ _*_ f = (λ x y → f (x · y)) ＝ (λ x y → f x * f y)

 respect-assoc : {X A : 𝓤 ̇ } (_·_ : X → X → X) (_*_ : A → A → A)
               → associative _·_ → associative _*_
               → (f : X → A) → homomorphic _·_ _*_ f → 𝓤 ̇

 respect-assoc _·_ _*_ α β f h  =  fα ＝ βf
  where
   l = λ x y z → f ((x · y) · z)   ＝⟨ ap (λ - → - (x · y) z) h ⟩
                 f (x · y) * f z   ＝⟨ ap (λ - → - x y * f z) h ⟩
                 (f x * f y) * f z ∎

   r = λ x y z → f (x · (y · z))   ＝⟨ ap (λ - → - x (y · z)) h ⟩
                 f x * f (y · z)   ＝⟨ ap (λ - → f x * - y z) h ⟩
                 f x * (f y * f z) ∎

   fα βf : ∀ x y z → (f x * f y) * f z ＝ f x * (f y * f z)
   fα x y z = (l x y z)⁻¹ ∙ ap f (α x y z) ∙ r x y z
   βf x y z = β (f x) (f y) (f z)

 remark : {X : 𝓤 ̇ } (_·_ : X → X → X) (α β : associative _·_ )
        → respect-assoc _·_ _·_ α β id (𝓻𝓮𝒻𝓵 _·_)
        ＝ ((λ x y z → 𝓻𝓮𝒻𝓵 ((x · y) · z) ∙ ap id (α x y z)) ＝ β)

 remark _·_ α β = refl

 open sip hiding (homomorphic)

 sns-data : SNS ∞-amagma-structure 𝓤
 sns-data = (ι , ρ , θ)
  where
   ι : (𝓧 𝓐 : ∞-aMagma) → ⟨ 𝓧 ⟩ ≃ ⟨ 𝓐 ⟩ → 𝓤 ̇
   ι (X , _·_ , α) (A , _*_ , β) (f , i) = Σ h ꞉ homomorphic _·_ _*_ f
                                               , respect-assoc _·_ _*_ α β f h

   ρ : (𝓧 : ∞-aMagma) → ι 𝓧 𝓧 (≃-refl ⟨ 𝓧 ⟩)
   ρ (X , _·_ , α) = h , p
    where
     h : homomorphic _·_ _·_ id
     h = 𝓻𝓮𝒻𝓵 _·_

     q : ∀ x y z → 𝓻𝓮𝒻𝓵 ((x · y) · z) ∙ ap id (α x y z) ＝ α x y z
     q x y z = refl-left-neutral ∙ ap-id-is-id (α x y z)

     p : (λ x y z → 𝓻𝓮𝒻𝓵 ((x · y) · z) ∙ ap id (α x y z)) ＝ α
     p =  dfunext fe (λ x → dfunext fe (λ y → dfunext fe (λ z → q x y z)))

   u : (X : 𝓤 ̇ ) → ∀ s → ∃! t ꞉ ∞-amagma-structure X , ι (X , s) (X , t) (≃-refl X)
   u X (_·_ , α) = c , φ
    where
     c : Σ t ꞉ ∞-amagma-structure X , ι (X , _·_ , α) (X , t) (≃-refl X)
     c = (_·_ , α) , ρ (X , _·_ , α)

     φ : (σ : Σ t ꞉ ∞-amagma-structure X , ι (X , _·_ , α) (X , t) (≃-refl X)) → c ＝ σ
     φ ((_·_ , β) , refl {_·_} , k) = γ
      where
       a : associative _·_
       a x y z = 𝓻𝓮𝒻𝓵 ((x · y) · z) ∙ ap id (α x y z)

       g : singleton-type a → Σ t ꞉ ∞-amagma-structure X , ι (X , _·_ , α) (X , t) (≃-refl X)
       g (β , k) = (_·_ , β) , (𝓻𝓮𝒻𝓵 _·_) , k

       i : is-prop (singleton-type a)
       i = singletons-are-props (singleton-types-are-singletons a)

       q : α , pr₂ (ρ (X , _·_ , α)) ＝ β , k
       q = i _ _

       γ : c ＝ (_·_ , β) , 𝓻𝓮𝒻𝓵 _·_ , k
       γ = ap g q

   θ : {X : 𝓤 ̇ } (s t : ∞-amagma-structure X) → is-equiv (canonical-map ι ρ s t)
   θ {X} s = Yoneda-Theorem-forth s (canonical-map ι ρ s) (u X s)

 _≅_ : ∞-aMagma → ∞-aMagma → 𝓤 ̇
 (X , _·_ , α) ≅ (Y , _*_ , β) = Σ f ꞉ (X → Y)
                                     , is-equiv f
                                     × (Σ h ꞉ homomorphic _·_ _*_ f
                                            , respect-assoc _·_ _*_ α β f h)

 characterization-of-∞-aMagma-＝ : (A B : ∞-aMagma) → (A ＝ B) ≃ (A ≅ B)
 characterization-of-∞-aMagma-＝ = characterization-of-＝ ua sns-data

module group {𝓤 : Universe} where
 open sip
 open sip-with-axioms
 open monoid {𝓤} hiding (sns-data ; _≅_)

 group-structure : 𝓤 ̇ → 𝓤 ̇
 group-structure X = Σ s ꞉ monoid-structure X , monoid-axioms X s

 group-axiom : (X : 𝓤 ̇ ) → monoid-structure X → 𝓤 ̇
 group-axiom X (_·_ , e) = (x : X) → Σ x' ꞉ X , (x · x' ＝ e) × (x' · x ＝ e)

 Group : 𝓤 ⁺ ̇
 Group = Σ X ꞉ 𝓤 ̇ , Σ ((_·_ , e) , a) ꞉ group-structure X , group-axiom X (_·_ , e)

 inv-lemma : (X : 𝓤 ̇ ) (_·_ : X → X → X) (e : X)
           → monoid-axioms X (_·_ , e)
           → (x y z : X)
           → (y · x) ＝ e
           → (x · z) ＝ e
           → y ＝ z

 inv-lemma X _·_  e (s , l , r , a) x y z q p =

    y             ＝⟨ (r y)⁻¹ ⟩
    (y · e)       ＝⟨ ap (y ·_) (p ⁻¹) ⟩
    (y · (x · z)) ＝⟨ (a y x z)⁻¹ ⟩
    ((y · x) · z) ＝⟨ ap (_· z) q ⟩
    (e · z)       ＝⟨ l z ⟩
    z             ∎

 group-axiom-is-prop : funext 𝓤 𝓤
                     → (X : 𝓤 ̇ )
                     → (s : group-structure X)
                     → is-prop (group-axiom X (pr₁ s))

 group-axiom-is-prop fe X ((_·_ , e) , (s , l , r , a)) = γ
  where
   i : (x : X) → is-prop (Σ x' ꞉ X , (x · x' ＝ e) × (x' · x ＝ e))
   i x (y , _ , q) (z , p , _) = u
    where
     t : y ＝ z
     t = inv-lemma X _·_ e (s , l , r , a) x y z q p

     u : (y , _ , q) ＝ (z , p , _)
     u = to-subtype-＝ (λ x' → ×-is-prop s s) t

   γ : is-prop (group-axiom X (_·_ , e))
   γ = Π-is-prop fe i

 sns-data : funext 𝓤 𝓤
          → SNS (λ X → Σ s ꞉ group-structure X , group-axiom X (pr₁ s)) 𝓤
 sns-data fe = add-axioms
                (λ X s → group-axiom X (pr₁ s)) (group-axiom-is-prop fe)
                (monoid.sns-data fe)

 _≅_ : Group → Group → 𝓤 ̇

 (X , ((_·_ , d) , _) , _) ≅ (Y , ((_*_ , e) , _) , _) =

            Σ f ꞉ (X → Y), is-equiv f
                         × ((λ x x' → f (x · x')) ＝ (λ x x' → f x * f x'))
                         × (f d ＝ e)

 characterization-of-group-＝ : is-univalent 𝓤 → (A B : Group) → (A ＝ B) ≃ (A ≅ B)
 characterization-of-group-＝ ua = characterization-of-＝ ua
                                   (sns-data (univalence-gives-funext ua))

 _≅'_ : Group → Group → 𝓤 ̇

 (X , ((_·_ , d) , _) , _) ≅' (Y , ((_*_ , e) , _) , _) =

            Σ f ꞉ (X → Y), is-equiv f
                         × ((λ x x' → f (x · x')) ＝ (λ x x' → f x * f x'))

 group-structure-of : (G : Group) → group-structure ⟨ G ⟩
 group-structure-of (X , ((_·_ , e) , i , l , r , a) , γ) = (_·_ , e) , i , l , r , a

 monoid-structure-of : (G : Group) → monoid-structure ⟨ G ⟩
 monoid-structure-of (X , ((_·_ , e) , i , l , r , a) , γ) = (_·_ , e)

 monoid-axioms-of : (G : Group) → monoid-axioms ⟨ G ⟩ (monoid-structure-of G)
 monoid-axioms-of (X , ((_·_ , e) , i , l , r , a) , γ) = i , l , r , a

 multiplication : (G : Group) → ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
 multiplication (X , ((_·_ , e) , i , l , r , a) , γ) = _·_

 syntax multiplication G x y = x ·⟨ G ⟩ y

 unit : (G : Group) → ⟨ G ⟩
 unit (X , ((_·_ , e) , i , l , r , a) , γ) = e

 group-is-set : (G : Group)
              → is-set ⟨ G ⟩

 group-is-set (X , ((_·_ , e) , i , l , r , a) , γ) = i

 unit-left : (G : Group) (x : ⟨ G ⟩)
           → unit G ·⟨ G ⟩ x ＝ x

 unit-left (X , ((_·_ , e) , i , l , r , a) , γ) x = l x

 unit-right : (G : Group) (x : ⟨ G ⟩)
            → x ·⟨ G ⟩ unit G ＝ x

 unit-right (X , ((_·_ , e) , i , l , r , a) , γ) x = r x

 assoc : (G : Group) (x y z : ⟨ G ⟩)
       → (x ·⟨ G ⟩ y) ·⟨ G ⟩ z ＝ x ·⟨ G ⟩ (y ·⟨ G ⟩ z)

 assoc (X , ((_·_ , e) , i , l , r , a) , γ) = a

 inv : (G : Group) → ⟨ G ⟩ → ⟨ G ⟩
 inv (X , ((_·_ , e) , i , l , r , a) , γ) x = pr₁ (γ x)

 inv-left : (G : Group) (x : ⟨ G ⟩)
          → inv G x ·⟨ G ⟩ x ＝ unit G

 inv-left (X , ((_·_ , e) , i , l , r , a) , γ) x = pr₂ (pr₂ (γ x))

 inv-right : (G : Group) (x : ⟨ G ⟩)
           → x ·⟨ G ⟩ inv G x ＝ unit G

 inv-right (X , ((_·_ , e) , i , l , r , a) , γ) x = pr₁ (pr₂ (γ x))

 preserves-multiplication : (G H : Group) → (⟨ G ⟩ → ⟨ H ⟩) → 𝓤 ̇
 preserves-multiplication G H f = (λ (x y : ⟨ G ⟩) → f (x ·⟨ G ⟩ y))
                                ＝ (λ (x y : ⟨ G ⟩) → f x ·⟨ H ⟩ f y)

 preserves-unit : (G H : Group) → (⟨ G ⟩ → ⟨ H ⟩) → 𝓤 ̇
 preserves-unit G H f = f (unit G) ＝ unit H

 idempotent-is-unit : (G : Group) (x : ⟨ G ⟩)
                    → x ·⟨ G ⟩ x ＝ x
                    → x ＝ unit G

 idempotent-is-unit G x p = γ
  where
   x' = inv G x
   γ = x                        ＝⟨ (unit-left G x)⁻¹ ⟩
       unit G ·⟨ G ⟩ x          ＝⟨ (ap (λ - → - ·⟨ G ⟩ x) (inv-left G x))⁻¹ ⟩
       (x' ·⟨ G ⟩ x) ·⟨ G ⟩ x   ＝⟨ assoc G x' x x ⟩
       x' ·⟨ G ⟩ (x ·⟨ G ⟩ x)   ＝⟨ ap (λ - → x' ·⟨ G ⟩ -) p ⟩
       x' ·⟨ G ⟩ x              ＝⟨ inv-left G x ⟩
       unit G                   ∎

 unit-preservation-lemma : (G H : Group) (f : ⟨ G ⟩ → ⟨ H ⟩)
                         → preserves-multiplication G H f
                         → preserves-unit G H f

 unit-preservation-lemma G H f m = idempotent-is-unit H e p
  where
   e  = f (unit G)

   p = e ·⟨ H ⟩ e               ＝⟨ ap (λ - → - (unit G) (unit G)) (m ⁻¹) ⟩
       f (unit G ·⟨ G ⟩ unit G) ＝⟨ ap f (unit-left G (unit G)) ⟩
       e                        ∎

 inv-Lemma : (G : Group) (x y z : ⟨ G ⟩)
           → (y ·⟨ G ⟩ x) ＝ unit G
           → (x ·⟨ G ⟩ z) ＝ unit G
           → y ＝ z

 inv-Lemma G = inv-lemma ⟨ G ⟩ (multiplication G) (unit G) (monoid-axioms-of G)

 one-left-inv : (G : Group) (x x' : ⟨ G ⟩)
              → (x' ·⟨ G ⟩ x) ＝ unit G
              → x' ＝ inv G x

 one-left-inv G x x' p = inv-Lemma G x x' (inv G x) p (inv-right G x)

 one-right-inv : (G : Group) (x x' : ⟨ G ⟩)
               → (x ·⟨ G ⟩ x') ＝ unit G
               → x' ＝ inv G x

 one-right-inv G x x' p = (inv-Lemma G x (inv G x) x' (inv-left G x) p)⁻¹

 preserves-inv : (G H : Group) → (⟨ G ⟩ → ⟨ H ⟩) → 𝓤 ̇
 preserves-inv G H f = (x : ⟨ G ⟩) → f (inv G x) ＝ inv H (f x)

 inv-preservation-lemma : (G H : Group) (f : ⟨ G ⟩ → ⟨ H ⟩)
                        → preserves-multiplication G H f
                        → preserves-inv G H f

 inv-preservation-lemma G H f m x = γ
  where
   p = f (inv G x) ·⟨ H ⟩ f x ＝⟨ (ap (λ - → - (inv G x) x) m)⁻¹ ⟩
       f (inv G x ·⟨ G ⟩ x)   ＝⟨ ap f (inv-left G x) ⟩
       f (unit G)             ＝⟨ unit-preservation-lemma G H f m ⟩
       unit H                 ∎

   γ : f (inv G x) ＝ inv H (f x)
   γ = one-left-inv H (f x) (f (inv G x)) p

 is-homomorphism : (G H : Group) → (⟨ G ⟩ → ⟨ H ⟩) → 𝓤 ̇
 is-homomorphism G H f = preserves-multiplication G H f
                       × preserves-unit G H f

 preservation-of-mult-is-prop : funext 𝓤 𝓤
                              → (G H : Group) (f : ⟨ G ⟩ → ⟨ H ⟩)
                              → is-prop (preserves-multiplication G H f)
 preservation-of-mult-is-prop fe G H f = j
  where
   j : is-prop (preserves-multiplication G H f)
   j = Π-is-set fe (λ _ → Π-is-set fe (λ _ → group-is-set H))

 being-homomorphism-is-prop : funext 𝓤 𝓤
                            → (G H : Group) (f : ⟨ G ⟩ → ⟨ H ⟩)
                            → is-prop (is-homomorphism G H f)
 being-homomorphism-is-prop fe G H f = i
  where

   i : is-prop (is-homomorphism G H f)
   i = ×-is-prop
        (preservation-of-mult-is-prop fe G H f)
        (group-is-set H)

 notions-of-homomorphism-agree : funext 𝓤 𝓤
                               → (G H : Group) (f : ⟨ G ⟩ → ⟨ H ⟩)
                               → is-homomorphism G H f
                               ≃ preserves-multiplication G H f

 notions-of-homomorphism-agree fe G H f = γ
  where
   α : is-homomorphism G H f → preserves-multiplication G H f
   α = pr₁

   β : preserves-multiplication G H f → is-homomorphism G H f
   β m = m , unit-preservation-lemma G H f m

   γ : is-homomorphism G H f ≃ preserves-multiplication G H f
   γ = logically-equivalent-props-are-equivalent
        (being-homomorphism-is-prop fe G H f)
        (preservation-of-mult-is-prop fe G H f)
        α
        β

 ≅-agreement : funext 𝓤 𝓤 → (G H : Group) → (G ≅ H) ≃ (G ≅' H)
 ≅-agreement fe G H = Σ-cong (λ f → Σ-cong (λ _ → notions-of-homomorphism-agree fe G H f))

 forget-unit-preservation : (G H : Group) → (G ≅ H) → (G ≅' H)
 forget-unit-preservation G H (f , e , m , _) = f , e , m

 NB : (fe : funext 𝓤 𝓤)
    → (G H : Group) → ⌜ ≅-agreement fe G H ⌝ ＝ forget-unit-preservation G H
 NB fe G H = refl

 forget-unit-preservation-is-equiv : funext 𝓤 𝓤
                                   → (G H : Group)
                                   → is-equiv (forget-unit-preservation G H)

 forget-unit-preservation-is-equiv fe G H = ⌜⌝-is-equiv (≅-agreement fe G H)

module subgroup
        (𝓤  : Universe)
        (ua : Univalence)
       where

 fe : ∀ {𝓥} {𝓦} → funext 𝓥 𝓦
 fe {𝓥} {𝓦} = univalence-gives-funext' 𝓥 𝓦 (ua 𝓥) (ua (𝓥 ⊔ 𝓦))

 open sip
 open monoid {𝓤} hiding (sns-data ; _≅_)
 open group {𝓤}
 open import UF.Powerset
 open import UF.Classifiers

 module ambient (G : Group) where

  _·_ : ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
  x · y = x ·⟨ G ⟩ y

  infixl  _·_

  group-closed : (⟨ G ⟩ → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
  group-closed 𝓐 = 𝓐 (unit G)
                 × ((x y : ⟨ G ⟩) → 𝓐 x → 𝓐 y → 𝓐 (x · y))
                 × ((x : ⟨ G ⟩) → 𝓐 x → 𝓐 (inv G x))

  Subgroups : 𝓤 ⁺ ̇
  Subgroups = Σ A ꞉ 𝓟 ⟨ G ⟩ , group-closed (_∈ A)

  ⟪_⟫ : Subgroups → 𝓟 ⟨ G ⟩
  ⟪ A , u , c , ι ⟫ = A

  being-group-closed-subset-is-prop : (A : 𝓟 ⟨ G ⟩)
                                    → is-prop (group-closed (_∈ A))
  being-group-closed-subset-is-prop A = ×-is-prop
                                            (∈-is-prop A (unit G))
                                         (×-is-prop
                                            (Π-is-prop fe
                                               (λ x → Π-is-prop fe
                                               (λ y → Π-is-prop fe
                                               (λ _ → Π-is-prop fe
                                               (λ _ → ∈-is-prop A (x · y))))))
                                            (Π-is-prop fe
                                               (λ x → Π-is-prop fe
                                               (λ _ → ∈-is-prop A (inv G x)))))

  ⟪⟫-is-embedding : is-embedding ⟪_⟫
  ⟪⟫-is-embedding = pr₁-is-embedding being-group-closed-subset-is-prop

  ap-⟪⟫ : (S T : Subgroups) → S ＝ T → ⟪ S ⟫ ＝ ⟪ T ⟫
  ap-⟪⟫ S T = ap ⟪_⟫

  ap-⟪⟫-is-equiv : (S T : Subgroups) → is-equiv (ap-⟪⟫ S T)
  ap-⟪⟫-is-equiv = embedding-embedding' ⟪_⟫ ⟪⟫-is-embedding

  subgroups-form-a-set : is-set Subgroups
  subgroups-form-a-set {S} {T} = equiv-to-prop
                                  (ap-⟪⟫ S T , ap-⟪⟫-is-equiv S T)
                                  (𝓟-is-set ua)

  subgroup-equality : (S T : Subgroups)
                    → (S ＝ T)
                    ≃ ((x : ⟨ G ⟩) → (x ∈ ⟪ S ⟫) ⇔ (x ∈ ⟪ T ⟫))

  subgroup-equality S T = γ
   where
    f : S ＝ T → (x : ⟨ G ⟩) → x ∈ ⟪ S ⟫ ⇔ x ∈ ⟪ T ⟫
    f p x = transport (λ - → x ∈ ⟪ - ⟫) p , transport (λ - → x ∈ ⟪ - ⟫) (p ⁻¹)

    h : ((x : ⟨ G ⟩) → x ∈ ⟪ S ⟫ ⇔ x ∈ ⟪ T ⟫) → ⟪ S ⟫ ＝ ⟪ T ⟫
    h φ = subset-extensionality' ua α β
     where
      α : ⟪ S ⟫ ⊆ ⟪ T ⟫
      α x = lr-implication (φ x)

      β : ⟪ T ⟫ ⊆ ⟪ S ⟫
      β x = rl-implication (φ x)

    g : ((x : ⟨ G ⟩) → x ∈ ⟪ S ⟫ ⇔ x ∈ ⟪ T ⟫) → S ＝ T
    g = inverse (ap-⟪⟫ S T) (ap-⟪⟫-is-equiv S T) ∘ h

    γ : (S ＝ T) ≃ ((x : ⟨ G ⟩) → x ∈ ⟪ S ⟫ ⇔ x ∈ ⟪ T ⟫)
    γ = logically-equivalent-props-are-equivalent
         subgroups-form-a-set
         (Π-is-prop fe
           (λ x → ×-is-prop
                   (Π-is-prop fe (λ _ → ∈-is-prop ⟪ T ⟫ x))
                   (Π-is-prop fe (λ _ → ∈-is-prop ⟪ S ⟫ x)))) f g

  T : 𝓤 ̇ → 𝓤 ̇
  T X = Σ ((_·_ , e) , a) ꞉ group-structure X , group-axiom X (_·_ , e)

  module _ {X : 𝓤 ̇ } (h : X → ⟨ G ⟩) (e : is-embedding h) where

   private
    h-lc : left-cancellable h
    h-lc = embeddings-are-lc h e

   having-group-closed-fiber-is-prop : is-prop (group-closed (fiber h))
   having-group-closed-fiber-is-prop = being-group-closed-subset-is-prop
                                        (λ x → (fiber h x , e x))

   at-most-one-homomorphic-structure : is-prop (Σ τ ꞉ T X , is-homomorphism (X , τ) G h)
   at-most-one-homomorphic-structure
      ((((_*_ ,  unitH) ,  maxioms) ,  gaxiom) ,  (pmult ,  punit))
      ((((_*'_ , unitH') , maxioms') , gaxiom') , (pmult' , punit'))
    = γ
    where
     τ τ' : T X
     τ  = ((_*_ ,  unitH) ,  maxioms) ,  gaxiom
     τ' = ((_*'_ , unitH') , maxioms') , gaxiom'

     i :  is-homomorphism (X , τ)  G h
     i  = (pmult ,  punit)

     i' : is-homomorphism (X , τ') G h
     i' = (pmult' , punit')

     p : _*_ ＝ _*'_
     p = dfunext fe (λ x → dfunext fe (λ y → h-lc (h (x * y)  ＝⟨  ap (λ - → - x y) pmult ⟩
                                                   h x · h y  ＝⟨ (ap (λ - → - x y) pmult')⁻¹ ⟩
                                                   h (x *' y) ∎)))
     q : unitH ＝ unitH'
     q = h-lc (h unitH  ＝⟨  punit ⟩
               unit G   ＝⟨  punit' ⁻¹ ⟩
               h unitH' ∎)

     r : (_*_ , unitH) ＝ (_*'_ , unitH')
     r = to-×-＝ p q

     δ : τ ＝ τ'
     δ = to-subtype-＝
           (group-axiom-is-prop fe X)
           (to-subtype-＝ (monoid-axioms-is-prop fe X) r)

     γ : (τ  , i) ＝ (τ' , i')
     γ = to-subtype-＝ (λ τ → being-homomorphism-is-prop fe (X , τ) G h) δ

   group-closed-fiber-gives-homomorphic-structure : funext 𝓤 𝓤
                                                  → group-closed (fiber h)
                                                  → (Σ τ ꞉ T X , is-homomorphism (X , τ) G h)

   group-closed-fiber-gives-homomorphic-structure fe (unitc , mulc , invc) = τ , i
    where
     φ : (x : X) → fiber h (h x)
     φ x = (x , 𝓻𝓮𝒻𝓵 (h x))

     unitH : X
     unitH = fiber-point unitc

     _*_ : X → X → X
     x * y = fiber-point (mulc (h x) (h y) (φ x) (φ y))

     invH : X → X
     invH x = fiber-point (invc (h x) (φ x))

     pmul : (x y : X) → h (x * y) ＝ h x · h y
     pmul x y = fiber-identification (mulc (h x) (h y) (φ x) (φ y))

     punit : h unitH ＝ unit G
     punit = fiber-identification unitc

     pinv : (x : X) → h (invH x) ＝ inv G (h x)
     pinv x = fiber-identification (invc (h x) (φ x))

     unitH-left : (x : X) → unitH * x ＝ x
     unitH-left x = h-lc (h (unitH * x) ＝⟨ pmul unitH x ⟩
                          h unitH · h x ＝⟨ ap (_· h x) punit ⟩
                          unit G · h x  ＝⟨ unit-left G (h x) ⟩
                          h x           ∎)

     unitH-right : (x : X) → x * unitH ＝ x
     unitH-right x = h-lc (h (x * unitH) ＝⟨ pmul x unitH ⟩
                           h x · h unitH ＝⟨ ap (h x ·_) punit ⟩
                           h x · unit G  ＝⟨ unit-right G (h x) ⟩
                           h x           ∎)

     assocH : (x y z : X) → ((x * y) * z) ＝ (x * (y * z))
     assocH x y z = h-lc (h ((x * y) * z)   ＝⟨ pmul (x * y) z ⟩
                          h (x * y) · h z   ＝⟨ ap (_· h z) (pmul x y) ⟩
                          (h x · h y) · h z ＝⟨ assoc G (h x) (h y) (h z) ⟩
                          h x · (h y · h z) ＝⟨ (ap (h x ·_) (pmul y z))⁻¹ ⟩
                          h x · h (y * z)   ＝⟨ (pmul x (y * z))⁻¹ ⟩
                          h (x * (y * z))   ∎)

     group-axiomH : (x : X) → Σ x' ꞉ X , (x * x' ＝ unitH) × (x' * x ＝ unitH)
     group-axiomH x = invH x ,

                      h-lc (h (x * invH x)     ＝⟨ pmul x (invH x) ⟩
                            h x · h (invH x)   ＝⟨ ap (h x ·_) (pinv x) ⟩
                            h x · inv G (h x)  ＝⟨ inv-right G (h x) ⟩
                            unit G             ＝⟨ punit ⁻¹ ⟩
                            h unitH            ∎),

                      h-lc ((h (invH x * x)    ＝⟨ pmul (invH x) x ⟩
                             h (invH x) · h x  ＝⟨ ap (_· h x) (pinv x) ⟩
                             inv G (h x) · h x ＝⟨ inv-left G (h x) ⟩
                             unit G            ＝⟨ punit ⁻¹ ⟩
                             h unitH           ∎))

     j : is-set X
     j = subtypes-of-sets-are-sets h h-lc (group-is-set G)

     τ : T X
     τ = ((_*_ , unitH) , (j , unitH-left , unitH-right , assocH)) , group-axiomH

     i : is-homomorphism (X , τ) G h
     i = dfunext fe (λ x → dfunext fe (pmul x)) , punit

   homomorphic-structure-gives-group-closed-fiber : (Σ τ ꞉ T X , is-homomorphism (X , τ) G h)
                                                  → group-closed (fiber h)

   homomorphic-structure-gives-group-closed-fiber
       ((((_*_ , unitH) , maxioms) , gaxiom) , (pmult , punit))
     = (unitc , mulc , invc)
    where
     H : Group
     H = X , ((_*_ , unitH) , maxioms) , gaxiom

     unitc : fiber h (unit G)
     unitc = unitH , punit

     mulc : ((x y : ⟨ G ⟩) → fiber h x → fiber h y → fiber h (x · y))
     mulc x y (a , p) (b , q) = (a * b) ,
                                (h (a * b) ＝⟨ ap (λ - → - a b) pmult ⟩
                                 h a · h b ＝⟨ ap₂ (λ - -' → - · -') p q ⟩
                                 x · y     ∎)

     invc : ((x : ⟨ G ⟩) → fiber h x → fiber h (inv G x))
     invc x (a , p) = inv H a ,
                      (h (inv H a) ＝⟨ inv-preservation-lemma H G h pmult a ⟩
                       inv G (h a) ＝⟨ ap (inv G) p ⟩
                       inv G x     ∎)

   fiber-structure-lemma : funext 𝓤 𝓤
                         → group-closed (fiber h)
                         ≃ (Σ τ ꞉ T X , is-homomorphism (X , τ) G h)

   fiber-structure-lemma fe = logically-equivalent-props-are-equivalent
                               having-group-closed-fiber-is-prop
                               at-most-one-homomorphic-structure
                               (group-closed-fiber-gives-homomorphic-structure fe)
                               homomorphic-structure-gives-group-closed-fiber

  characterization-of-the-type-of-subgroups : Subgroups ≃ (Σ H ꞉ Group
                                                         , Σ h ꞉ (⟨ H ⟩ → ⟨ G ⟩)
                                                         , is-embedding h
                                                         × is-homomorphism H G h)
  characterization-of-the-type-of-subgroups =

   Subgroups                                                                                       ≃⟨ i ⟩
   (Σ A ꞉ 𝓟 ⟨ G ⟩ , group-closed (_∈ A))                                                           ≃⟨ ii ⟩
   (Σ (X , h , e) ꞉ Subtypes ⟨ G ⟩ , group-closed (fiber h))                                       ≃⟨ iii ⟩
   (Σ X ꞉ 𝓤 ̇ , Σ (h , e) ꞉ X ↪ ⟨ G ⟩ , group-closed (fiber h))                                     ≃⟨ iv ⟩
   (Σ X ꞉ 𝓤 ̇ , Σ (h , e) ꞉ X ↪ ⟨ G ⟩ , Σ τ ꞉ T X , is-homomorphism (X , τ) G h)                    ≃⟨ v ⟩
   (Σ X ꞉ 𝓤 ̇ , Σ h ꞉ (X → ⟨ G ⟩) , Σ e ꞉ is-embedding h , Σ τ ꞉ T X , is-homomorphism (X , τ) G h) ≃⟨ vi ⟩
   (Σ X ꞉ 𝓤 ̇ , Σ h ꞉ (X → ⟨ G ⟩) , Σ τ ꞉ T X , Σ e ꞉ is-embedding h , is-homomorphism (X , τ) G h) ≃⟨ vii ⟩
   (Σ X ꞉ 𝓤 ̇ , Σ τ ꞉ T X , Σ h ꞉ (X → ⟨ G ⟩) , is-embedding h × is-homomorphism (X , τ) G h)       ≃⟨ viii ⟩
   (Σ H ꞉ Group , Σ h ꞉ (⟨ H ⟩ → ⟨ G ⟩) , is-embedding h × is-homomorphism H G h)                  ■

      where
       open special-classifier-single-universe 𝓤

       φ : Subtypes ⟨ G ⟩ → 𝓟 ⟨ G ⟩
       φ = χ-special is-prop ⟨ G ⟩

       j : is-equiv φ
       j = χ-special-is-equiv (ua 𝓤) fe is-prop ⟨ G ⟩

       i    = ≃-refl Subgroups
       ii   = ≃-sym (Σ-change-of-variable (λ (A : 𝓟 ⟨ G ⟩) → group-closed (_∈ A)) φ j)
       iii  = Σ-assoc
       iv   = Σ-cong (λ X → Σ-cong (λ (h , e) → fiber-structure-lemma h e fe))
       v    = Σ-cong (λ X → Σ-assoc)
       vi   = Σ-cong (λ X → Σ-cong (λ h → Σ-flip))
       vii  = Σ-cong (λ X → Σ-flip)
       viii = ≃-sym Σ-assoc

  induced-group : Subgroups → Group
  induced-group S = pr₁ (⌜ characterization-of-the-type-of-subgroups ⌝ S)

module ring {𝓤 : Universe} (ua : Univalence) where
 open sip hiding (⟨_⟩)
 open sip-with-axioms
 open sip-join

 fe : ∀ {𝓥} {𝓦} → funext 𝓥 𝓦
 fe {𝓥} {𝓦} = univalence-gives-funext' 𝓥 𝓦 (ua 𝓥) (ua (𝓥 ⊔ 𝓦))

 rng-structure : 𝓤 ̇ → 𝓤 ̇
 rng-structure X = (X → X → X) × (X → X → X)

 rng-axioms : (R : 𝓤 ̇ ) → rng-structure R → 𝓤 ̇
 rng-axioms R (_+_ , _·_) = I × II × III × IV × V × VI × VII
  where
    I   = is-set R
    II  = (x y z : R) → (x + y) + z ＝ x + (y + z)
    III = (x y : R) → x + y ＝ y + x
    IV  = Σ O ꞉ R , ((x : R) → x + O ＝ x) × ((x : R) → Σ x' ꞉ R , x + x' ＝ O)
    V   = (x y z : R) → (x · y) · z ＝ x · (y · z)
    VI  = (x y z : R) → x · (y + z) ＝ (x · y) + (x · z)
    VII = (x y z : R) → (y + z) · x ＝ (y · x) + (z · x)

 Rng : 𝓤 ⁺ ̇
 Rng = Σ R ꞉ 𝓤 ̇ , Σ s ꞉ rng-structure R , rng-axioms R s

 rng-axioms-is-prop : (R : 𝓤 ̇ ) (s : rng-structure R)
                    → is-prop (rng-axioms R s)

 rng-axioms-is-prop R (_+_ , _·_) = prop-criterion δ
  where
   δ : rng-axioms R (_+_ , _·_) → is-prop (rng-axioms R (_+_ , _·_))
   δ (i , ii , iii , iv-vii) = γ
    where
     A   = λ (O : R) → ((x : R) → x + O ＝ x)
                     × ((x : R) → Σ x' ꞉ R , x + x' ＝ O)

     IV  = Σ A

     a : (O O' : R) → ((x : R) → x + O ＝ x) → ((x : R) → x + O' ＝ x) → O ＝ O'
     a O O' f f' = O       ＝⟨ (f' O)⁻¹ ⟩
                  (O + O') ＝⟨ iii O O' ⟩
                  (O' + O) ＝⟨ f O' ⟩
                   O'      ∎

     b : (O : R) → is-prop ((x : R) → x + O ＝ x)
     b O = Π-is-prop fe (λ x → i {x + O} {x})

     c : (O : R)
       → ((x : R) → x + O ＝ x)
       → (x : R) → is-prop (Σ x' ꞉ R , x + x' ＝ O)
     c O f x (x' , p') (x'' , p'') = to-subtype-＝ (λ y → i {x + y} {O}) r
      where
       r : x' ＝ x''
       r = x'               ＝⟨ (f x')⁻¹ ⟩
           (x' + O)         ＝⟨ ap (x' +_) (p'' ⁻¹) ⟩
           (x' + (x + x'')) ＝⟨ (ii x' x x'')⁻¹ ⟩
           ((x' + x) + x'') ＝⟨ ap (_+ x'') (iii x' x) ⟩
           ((x + x') + x'') ＝⟨ ap (_+ x'') p' ⟩
           (O + x'')        ＝⟨ iii O x'' ⟩
           (x'' + O)        ＝⟨ f x'' ⟩
           x''              ∎

     d : (O : R) → is-prop (A O)
     d O (f , g) = φ (f , g)
      where
       φ : is-prop (A O)
       φ = ×-is-prop (b O) (Π-is-prop fe (λ x → c O f x))

     IV-is-prop : is-prop IV
     IV-is-prop (O , f , g) (O' , f' , g') = e
      where
       e : (O , f , g) ＝ (O' , f' , g')
       e = to-subtype-＝ d (a O O' f f')

     γ : is-prop (rng-axioms R (_+_ , _·_))
     γ = ×-is-prop
           (being-set-is-prop fe)
        (×-is-prop
           (Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → Π-is-prop fe
           λ z → i {(x + y) + z} {x + (y + z)})))
        (×-is-prop
           (Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → i {x + y} {y + x})))
        (×-is-prop
           IV-is-prop
        (×-is-prop
           (Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → Π-is-prop fe
           (λ z → i {(x · y) · z} {x · (y · z)}))))
        (×-is-prop
           (Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → Π-is-prop fe
           (λ z → i {x · (y + z)} {(x · y) + (x · z)}))))
           (Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → Π-is-prop fe
           (λ z → i {(y + z) · x} {(y · x) + (z · x)})))))))))

 _≅[Rng]_ : Rng → Rng → 𝓤 ̇

 (R , (_+_ , _·_) , _) ≅[Rng] (R' , (_+'_ , _·'_) , _) =

                       Σ f ꞉ (R → R')
                           , is-equiv f
                           × ((λ x y → f (x + y)) ＝ (λ x y → f x +' f y))
                           × ((λ x y → f (x · y)) ＝ (λ x y → f x ·' f y))

 characterization-of-rng-＝ : (𝓡 𝓡' : Rng) → (𝓡 ＝ 𝓡') ≃ (𝓡 ≅[Rng] 𝓡')
 characterization-of-rng-＝ = characterization-of-＝ (ua 𝓤)
                              (add-axioms
                                rng-axioms
                                rng-axioms-is-prop
                                (join
                                  ∞-magma.sns-data
                                  ∞-magma.sns-data))

 ⟨_⟩ : (𝓡 : Rng) → 𝓤 ̇
 ⟨ R , _ ⟩ = R

 ring-structure : 𝓤 ̇ → 𝓤 ̇
 ring-structure X = X × rng-structure X

 ring-axioms : (R : 𝓤 ̇ ) → ring-structure R → 𝓤 ̇
 ring-axioms R (𝟏 , _+_ , _·_) = rng-axioms R (_+_ , _·_) × VIII
  where
   VIII = (x : R) → (x · 𝟏 ＝ x) × (𝟏 · x ＝ x)

 ring-axioms-is-prop : (R : 𝓤 ̇ ) (s : ring-structure R)
                             → is-prop (ring-axioms R s)

 ring-axioms-is-prop R (𝟏 , _+_ , _·_) ((i , ii-vii) , viii) = γ ((i , ii-vii) , viii)
  where
   γ : is-prop (ring-axioms R (𝟏 , _+_ , _·_))
   γ = ×-is-prop
         (rng-axioms-is-prop R (_+_ , _·_))
         (Π-is-prop fe (λ x → ×-is-prop (i {x · 𝟏} {x}) (i {𝟏 · x} {x})))

 Ring : 𝓤 ⁺ ̇
 Ring = Σ R ꞉ 𝓤 ̇ , Σ s ꞉ ring-structure R , ring-axioms R s

 _≅[Ring]_ : Ring → Ring → 𝓤 ̇

 (R , (𝟏 , _+_ , _·_) , _) ≅[Ring] (R' , (𝟏' , _+'_ , _·'_) , _) =

                           Σ f ꞉ (R → R')
                               , is-equiv f
                               × (f 𝟏 ＝ 𝟏')
                               × ((λ x y → f (x + y)) ＝ (λ x y → f x +' f y))
                               × ((λ x y → f (x · y)) ＝ (λ x y → f x ·' f y))

 characterization-of-ring-＝ : (𝓡 𝓡' : Ring) → (𝓡 ＝ 𝓡') ≃ (𝓡 ≅[Ring] 𝓡')
 characterization-of-ring-＝ = sip.characterization-of-＝ (ua 𝓤)
                                (sip-with-axioms.add-axioms
                                  ring-axioms
                                  ring-axioms-is-prop
                                  (sip-join.join
                                    pointed-type.sns-data
                                      (join
                                        ∞-magma.sns-data
                                        ∞-magma.sns-data)))

 is-commutative : Rng → 𝓤 ̇
 is-commutative (R , (_+_ , _·_) , _) = (x y : R) → x · y ＝ y · x

 being-commutative-is-prop : (𝓡 : Rng) → is-prop (is-commutative 𝓡)
 being-commutative-is-prop (R , (_+_ , _·_) , i , ii-vii) =

   Π-is-prop fe
   (λ x → Π-is-prop fe
   (λ y → i {x · y} {y · x}))

 open import UF.Powerset

 is-ideal : (𝓡 : Rng) → 𝓟 ⟨ 𝓡 ⟩ → 𝓤 ̇
 is-ideal (R , (_+_ , _·_) , _) I = (x y : R) → (x ∈ I → y ∈ I → (x + y) ∈ I)
                                              × (x ∈ I → (x · y) ∈ I)
                                              × (y ∈ I → (x · y) ∈ I)

 is-local : Rng → 𝓤 ⁺ ̇
 is-local 𝓡 = ∃! I ꞉ 𝓟 ⟨ 𝓡 ⟩ , (is-ideal 𝓡 I → (J : 𝓟 ⟨ 𝓡 ⟩) → is-ideal 𝓡 J → J ⊆ I)

 being-local-is-prop : (𝓡 : Rng) → is-prop (is-local 𝓡)
 being-local-is-prop 𝓡 = ∃!-is-prop fe

 open import UF.PropTrunc

 module _ (pt : propositional-truncations-exist) where

  open propositional-truncations-exist pt public
  open PropositionalTruncation pt
  open import Naturals.Order

  is-noetherian : (𝓡 : Rng) → 𝓤 ⁺ ̇
  is-noetherian 𝓡 = (I : ℕ → 𝓟 ⟨ 𝓡 ⟩)
                  → ((n : ℕ) → is-ideal 𝓡 (I n))
                  → ((n : ℕ) → I n ⊆ I (succ n))
                  → ∃ m ꞉ ℕ , ((n : ℕ) → m ≤ n → I m ＝ I n)

  NoetherianRng : 𝓤 ⁺ ̇
  NoetherianRng = Σ 𝓡 ꞉ Rng , is-noetherian 𝓡

  being-noetherian-is-prop : (𝓡 : Rng) → is-prop (is-noetherian 𝓡)

  being-noetherian-is-prop 𝓡 = Π-is-prop fe
                                (λ I → Π-is-prop fe
                                (λ _ → Π-is-prop fe
                                (λ _ → ∃-is-prop)))

  forget-Noether : NoetherianRng → Rng
  forget-Noether (𝓡 , _) = 𝓡

  forget-Noether-is-embedding : is-embedding forget-Noether
  forget-Noether-is-embedding = pr₁-is-embedding being-noetherian-is-prop

  _≅[NoetherianRng]_ : NoetherianRng → NoetherianRng → 𝓤 ̇

  ((R , (_+_ , _·_) , _) , _) ≅[NoetherianRng] ((R' , (_+'_ , _·'_) , _) , _) =

                              Σ f ꞉ (R → R')
                                  , is-equiv f
                                  × ((λ x y → f (x + y)) ＝ (λ x y → f x +' f y))
                                  × ((λ x y → f (x · y)) ＝ (λ x y → f x ·' f y))

  NB : (𝓡 𝓡' : NoetherianRng)
     → (𝓡 ≅[NoetherianRng] 𝓡') ＝ (forget-Noether 𝓡 ≅[Rng] forget-Noether 𝓡')

  NB 𝓡 𝓡' = refl

  characterization-of-nrng-＝ : (𝓡 𝓡' : NoetherianRng)
                             → (𝓡 ＝ 𝓡') ≃ (𝓡 ≅[NoetherianRng] 𝓡')

  characterization-of-nrng-＝ 𝓡 𝓡' =

    (𝓡 ＝ 𝓡')                               ≃⟨ i ⟩
    (forget-Noether 𝓡 ＝ forget-Noether 𝓡') ≃⟨ ii ⟩
    (𝓡 ≅[NoetherianRng] 𝓡')                ■

    where
     i = ≃-sym (embedding-criterion-converse forget-Noether
                  forget-Noether-is-embedding 𝓡 𝓡')
     ii = characterization-of-rng-＝ (forget-Noether 𝓡) (forget-Noether 𝓡')

  isomorphic-NoetherianRng-transport :

      (A : NoetherianRng → 𝓥 ̇ )
    → (𝓡 𝓡' : NoetherianRng) → 𝓡 ≅[NoetherianRng] 𝓡' → A 𝓡 → A 𝓡'

  isomorphic-NoetherianRng-transport A 𝓡 𝓡' i a = a'
   where
    p : 𝓡 ＝ 𝓡'
    p = ⌜ characterization-of-nrng-＝ 𝓡 𝓡' ⌝⁻¹ i

    a' : A 𝓡'
    a' = transport A p a

  is-CNL : Ring → 𝓤 ⁺ ̇
  is-CNL (R , (𝟏 , _+_ , _·_) , i-vii , viii) = is-commutative 𝓡
                                              × is-noetherian 𝓡
                                              × is-local 𝓡
   where
    𝓡 : Rng
    𝓡 = (R , (_+_ , _·_) , i-vii)

  being-CNL-is-prop : (𝓡 : Ring) → is-prop (is-CNL 𝓡)
  being-CNL-is-prop (R , (𝟏 , _+_ , _·_) , i-vii , viii) =

     ×-is-prop (being-commutative-is-prop 𝓡)
    (×-is-prop (being-noetherian-is-prop 𝓡)
                       (being-local-is-prop 𝓡))
   where
    𝓡 : Rng
    𝓡 = (R , (_+_ , _·_) , i-vii)

  CNL-Ring : 𝓤 ⁺ ̇
  CNL-Ring = Σ 𝓡 ꞉ Ring , is-CNL 𝓡

  _≅[CNL]_ : CNL-Ring → CNL-Ring → 𝓤 ̇

  ((R , (𝟏 , _+_ , _·_) , _) , _) ≅[CNL] ((R' , (𝟏' , _+'_ , _·'_) , _) , _) =

                                  Σ f ꞉ (R → R')
                                      , is-equiv f
                                      × (f 𝟏 ＝ 𝟏')
                                      × ((λ x y → f (x + y)) ＝ (λ x y → f x +' f y))
                                      × ((λ x y → f (x · y)) ＝ (λ x y → f x ·' f y))

  forget-CNL : CNL-Ring → Ring
  forget-CNL (𝓡 , _) = 𝓡

  forget-CNL-is-embedding : is-embedding forget-CNL
  forget-CNL-is-embedding = pr₁-is-embedding being-CNL-is-prop

  NB' : (𝓡 𝓡' : CNL-Ring)
      → (𝓡 ≅[CNL] 𝓡') ＝ (forget-CNL 𝓡 ≅[Ring] forget-CNL 𝓡')

  NB' 𝓡 𝓡' = refl

  characterization-of-CNL-ring-＝ : (𝓡 𝓡' : CNL-Ring)
                                 → (𝓡 ＝ 𝓡') ≃ (𝓡 ≅[CNL] 𝓡')

  characterization-of-CNL-ring-＝ 𝓡 𝓡' =

     (𝓡 ＝ 𝓡')                               ≃⟨ i ⟩
     (forget-CNL 𝓡 ＝ forget-CNL 𝓡')         ≃⟨ ii ⟩
     (𝓡 ≅[CNL] 𝓡')                          ■

     where
      i = ≃-sym (embedding-criterion-converse forget-CNL
                   forget-CNL-is-embedding 𝓡 𝓡')
      ii = characterization-of-ring-＝ (forget-CNL 𝓡) (forget-CNL 𝓡')

  isomorphic-CNL-Ring-transport :

      (A : CNL-Ring → 𝓥 ̇ )
    → (𝓡 𝓡' : CNL-Ring) → 𝓡 ≅[CNL] 𝓡' → A 𝓡 → A 𝓡'

  isomorphic-CNL-Ring-transport A 𝓡 𝓡' i a = a'
   where
    p : 𝓡 ＝ 𝓡'
    p = ⌜ characterization-of-CNL-ring-＝ 𝓡 𝓡' ⌝⁻¹ i

    a' : A 𝓡'
    a' = transport A p a

module slice
        {𝓤 𝓥 : Universe}
        (R : 𝓥 ̇ )
       where

 open sip

 S : 𝓤 ̇ → 𝓤 ⊔ 𝓥 ̇
 S X = X → R

 sns-data : SNS S (𝓤 ⊔ 𝓥)
 sns-data = (ι , ρ , θ)
  where
   ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓤 ⊔ 𝓥 ̇
   ι (X , g) (Y , h) (f , _) = (g ＝ h ∘ f)

   ρ : (A : Σ S) → ι A A (≃-refl ⟨ A ⟩)
   ρ (X , g) = 𝓻𝓮𝒻𝓵 g

   k : {X : 𝓤 ̇ } {g h : S X} → canonical-map ι ρ g h ∼ -id (g ＝ h)
   k (refl {g}) = 𝓻𝓮𝒻𝓵 (𝓻𝓮𝒻𝓵 g)

   θ : {X : 𝓤 ̇ } (g h : S X) → is-equiv (canonical-map ι ρ g h)
   θ g h = equiv-closed-under-∼ id (canonical-map ι ρ g h) (id-is-equiv (g ＝ h)) k

 _/_ : (𝓤 : Universe) → 𝓥 ̇ → 𝓤 ⁺ ⊔ 𝓥 ̇
 𝓤 / Y = Σ X ꞉ 𝓤 ̇ , (X → Y)

 _≅_  : 𝓤 / R → 𝓤 / R → 𝓤 ⊔ 𝓥 ̇
 (X , g) ≅ (Y , h) = Σ f ꞉ (X → Y), is-equiv f × (g ＝ h ∘ f)

 characterization-of-/-＝ : is-univalent 𝓤 → (A B : 𝓤 / R) → (A ＝ B) ≃ (A ≅ B)
 characterization-of-/-＝ ua = characterization-of-＝ ua sns-data

module slice-variation
        {𝓤 𝓥 : Universe}
        (R : 𝓥 ̇ )
        (ua : is-univalent 𝓤)
        (fe : funext 𝓤 𝓥)
       where

 open sip

 S : 𝓤 ̇ → 𝓤 ⊔ 𝓥 ̇
 S X = X → R

 sns-data : SNS S (𝓤 ⊔ 𝓥)
 sns-data = (ι , ρ , θ)
  where
   ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓤 ⊔ 𝓥 ̇
   ι (X , g) (Y , h) (f , _) = ((x : X) → g x ＝ h (f x))

   ρ : (A : Σ S) → ι A A (≃-refl ⟨ A ⟩)
   ρ (X , g) = λ x → 𝓻𝓮𝒻𝓵 (g x)

   k : {X : 𝓤 ̇ } {g h : S X} → canonical-map ι ρ g h ∼ happly' g h
   k (refl {g}) = 𝓻𝓮𝒻𝓵 (λ x → 𝓻𝓮𝒻𝓵 (g x))

   θ : {X : 𝓤 ̇ } (g h : S X) → is-equiv (canonical-map ι ρ g h)
   θ g h = equiv-closed-under-∼ (happly' g h) (canonical-map ι ρ g h) (fe g h) k

 _/_ : (𝓤 : Universe) → 𝓥 ̇ → 𝓤 ⁺ ⊔ 𝓥 ̇
 𝓤 / Y = Σ X ꞉ 𝓤 ̇ , (X → Y)

 _≅_  : 𝓤 / R → 𝓤 / R → 𝓤 ⊔ 𝓥 ̇
 (X , g) ≅ (Y , h) = Σ f ꞉ (X → Y), is-equiv f × ((x : X) → g x ＝ h (f x))

 characterization-of-/-＝ : (A B : 𝓤 / R) → (A ＝ B) ≃ (A ≅ B)
 characterization-of-/-＝ = characterization-of-＝ ua sns-data

module universe-a-la-tarski
        (𝓤 𝓥 : Universe)
        (ua : is-univalent 𝓤)
        (fe : funext 𝓤 (𝓥 ⁺))
       where

 TarskiUniverse : (𝓤 𝓥 : Universe) → (𝓤 ⊔ 𝓥)⁺ ̇
 TarskiUniverse 𝓤 𝓥 = Σ X ꞉ 𝓤 ̇ , (X → 𝓥 ̇ )

 _≅_  : TarskiUniverse 𝓤 𝓥 → TarskiUniverse 𝓤 𝓥 → 𝓤 ⊔ (𝓥 ⁺) ̇
 (X , T) ≅ (X' , T') = Σ f ꞉ (X → X'), is-equiv f × ((x : X) → T x ＝ T' (f x) )

 characterization-of-Tarski-＝ : (A B : TarskiUniverse 𝓤 𝓥)
                              → (A ＝ B) ≃ (A ≅ B)
 characterization-of-Tarski-＝ = slice-variation.characterization-of-/-＝ (𝓥 ̇ ) ua fe

module universe-a-la-tarski-hSet-example
        (𝓤 : Universe)
        (ua : is-univalent (𝓤 ⁺))
       where

 fe : funext (𝓤 ⁺) (𝓤 ⁺)
 fe = univalence-gives-funext ua

 open universe-a-la-tarski (𝓤 ⁺) 𝓤 ua fe

 hset : TarskiUniverse (𝓤 ⁺) 𝓤
 hset = hSet 𝓤 , pr₁

 example : (X : 𝓤 ⁺ ̇ ) (T : X → 𝓤 ̇ )
         → ((X , T) ＝ hset) ≃ (Σ f ꞉ (X → hSet 𝓤) , is-equiv f
                                                  × ((x : X) → T x ＝ pr₁ (f x)))

 example X T = characterization-of-Tarski-＝ (X , T) hset

module generalized-metric-space
        {𝓤 𝓥 𝓦  : Universe}
        (R : 𝓥 ̇ )
        (axioms  : (X : 𝓤 ̇ ) → (X → X → R) → 𝓦 ̇ )
        (axiomss : (X : 𝓤 ̇ ) (d : X → X → R) → is-prop (axioms X d))
       where

 open sip
 open sip-with-axioms

 S : 𝓤 ̇ → 𝓤 ⊔ 𝓥 ̇
 S X = X → X → R

 sns-data : SNS S (𝓤 ⊔ 𝓥)
 sns-data = (ι , ρ , θ)
  where
   ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓤 ⊔ 𝓥 ̇
   ι (X , d) (Y , e) (f , _) = (d ＝ λ x x' → e (f x) (f x'))

   ρ : (A : Σ S) → ι A A (≃-refl ⟨ A ⟩)
   ρ (X , d) = 𝓻𝓮𝒻𝓵 d

   h : {X : 𝓤 ̇ } {d e : S X} → canonical-map ι ρ d e ∼ -id (d ＝ e)
   h (refl {d}) = 𝓻𝓮𝒻𝓵 (𝓻𝓮𝒻𝓵 d)

   θ : {X : 𝓤 ̇ } (d e : S X) → is-equiv (canonical-map ι ρ d e)
   θ d e = equiv-closed-under-∼ id (canonical-map ι ρ d e) (id-is-equiv (d ＝ e)) h

 M : 𝓤 ⁺ ⊔ 𝓥 ⊔ 𝓦 ̇
 M = Σ X ꞉ 𝓤 ̇ , Σ d ꞉ (X → X → R) , axioms X d

 _≅_  : M → M → 𝓤 ⊔ 𝓥 ̇
 (X , d , _) ≅ (Y , e , _) = Σ f ꞉ (X → Y), is-equiv f
                                          × (d ＝ λ x x' → e (f x) (f x'))

 characterization-of-M-＝ : is-univalent 𝓤
                         → (A B : M)

                         → (A ＝ B) ≃ (A ≅ B)

 characterization-of-M-＝ ua = characterization-of-＝-with-axioms ua
                                sns-data
                                axioms axiomss

 _≅'_  : M → M → 𝓤 ⊔ 𝓥 ̇
 (X , d , _) ≅' (Y , e , _)
             = Σ f ꞉ (X → Y), is-equiv f
                            × ((x x' : X) → d x x' ＝ e (f x) (f x'))


 characterization-of-M-＝' :

     Univalence
   → ((X , d , a) (Y , e , b) : M)
   → ((X , d , a) ＝ (Y , e , b))
                  ≃  (Σ f ꞉ (X → Y), is-equiv f
                                   × ((x x' : X) → d x x' ＝ e (f x) (f x')))

 characterization-of-M-＝' ua (X , d , a) (Y , e , b) =
     characterization-of-M-＝ (ua 𝓤) (X , d , a) (Y , e , b)
   ● Σ-cong (λ f → ×-cong (≃-refl (is-equiv f))
                         (≃-funext₂ (Univalence-gives-FunExt ua 𝓤 (𝓤 ⊔ 𝓥))
                                    (Univalence-gives-FunExt ua 𝓤 𝓥)
                                    (λ x y → d x y)
                                    (λ x x' → e (f x) (f x'))))


module generalized-topological-space
        (𝓤 𝓥 : Universe)
        (R : 𝓥 ̇ )
        (axioms  : (X : 𝓤 ̇ ) → ((X → R) → R) → 𝓤 ⊔ 𝓥 ̇ )
        (axiomss : (X : 𝓤 ̇ ) (𝓞 : (X → R) → R) → is-prop (axioms X 𝓞))
       where

 open sip
 open sip-with-axioms

 ℙ : 𝓦 ̇ → 𝓥 ⊔ 𝓦 ̇
 ℙ X = X → R

 _∊_ : {X : 𝓦 ̇ } → X → ℙ X → R
 x ∊ A = A x

 inverse-image : {X Y : 𝓤 ̇ } → (X → Y) → ℙ Y → ℙ X
 inverse-image f B = λ x → f x ∊ B

 ℙℙ : 𝓤 ̇ → 𝓤 ⊔ 𝓥 ̇
 ℙℙ X = ℙ (ℙ X)

 Space : 𝓤 ⁺ ⊔ 𝓥  ̇
 Space = Σ X ꞉ 𝓤 ̇ , Σ 𝓞 ꞉ ℙℙ X , axioms X 𝓞

 sns-data : SNS ℙℙ (𝓤 ⊔ 𝓥)
 sns-data = (ι , ρ , θ)
  where
   ι : (A B : Σ ℙℙ) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓤 ⊔ 𝓥 ̇
   ι (X , 𝓞X) (Y , 𝓞Y) (f , _) = (λ (V : ℙ Y) → inverse-image f V ∊ 𝓞X) ＝ 𝓞Y

   ρ : (A : Σ ℙℙ) → ι A A (≃-refl ⟨ A ⟩)
   ρ (X , 𝓞) = 𝓻𝓮𝒻𝓵 𝓞

   h : {X : 𝓤 ̇ } {𝓞 𝓞' : ℙℙ X} → canonical-map ι ρ 𝓞 𝓞' ∼ -id (𝓞 ＝ 𝓞')
   h (refl {𝓞}) = 𝓻𝓮𝒻𝓵 (𝓻𝓮𝒻𝓵 𝓞)

   θ : {X : 𝓤 ̇ } (𝓞 𝓞' : ℙℙ X) → is-equiv (canonical-map ι ρ 𝓞 𝓞')
   θ {X} 𝓞 𝓞' = equiv-closed-under-∼ id (canonical-map ι ρ 𝓞 𝓞') (id-is-equiv (𝓞 ＝ 𝓞')) h

 _≅_  : Space → Space → 𝓤 ⊔ 𝓥 ̇

 (X , 𝓞X , _) ≅ (Y , 𝓞Y , _) =

              Σ f ꞉ (X → Y), is-equiv f
                           × ((λ V → inverse-image f V ∊ 𝓞X) ＝ 𝓞Y)

 characterization-of-Space-＝ : is-univalent 𝓤
                             → (A B : Space)

                             → (A ＝ B) ≃ (A ≅ B)

 characterization-of-Space-＝ ua = characterization-of-＝-with-axioms ua
                                   sns-data axioms axiomss

 _≅'_  : Space → Space → 𝓤 ⊔ 𝓥 ̇

 (X , F , _) ≅' (Y , G , _) =

             Σ f ꞉ (X → Y), is-equiv f
                          × ((λ (v : Y → R) → F (v ∘ f)) ＝ G)

 characterization-of-Space-＝' : is-univalent 𝓤
                              → (A B : Space)

                              → (A ＝ B) ≃ (A ≅' B)

 characterization-of-Space-＝' = characterization-of-Space-＝

module selection-space
        (𝓤 𝓥 : Universe)
        (R : 𝓥 ̇ )
        (axioms  : (X : 𝓤 ̇ ) → ((X → R) → X) → 𝓤 ⊔ 𝓥 ̇ )
        (axiomss : (X : 𝓤 ̇ ) (ε : (X → R) → X) → is-prop (axioms X ε))
       where

 open sip
 open sip-with-axioms

 S : 𝓤 ̇ → 𝓤 ⊔ 𝓥 ̇
 S X = (X → R) → X

 SelectionSpace : 𝓤 ⁺ ⊔ 𝓥  ̇
 SelectionSpace = Σ X ꞉ 𝓤 ̇ , Σ ε ꞉ S X , axioms X ε

 sns-data : SNS S (𝓤 ⊔ 𝓥)
 sns-data = (ι , ρ , θ)
  where
   ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓤 ⊔ 𝓥 ̇
   ι (X , ε) (Y , δ) (f , _) = (λ (q : Y → R) → f (ε (q ∘ f))) ＝ δ

   ρ : (A : Σ S) → ι A A (≃-refl ⟨ A ⟩)
   ρ (X , ε) = 𝓻𝓮𝒻𝓵 ε

   θ : {X : 𝓤 ̇ } (ε δ : S X) → is-equiv (canonical-map ι ρ ε δ)
   θ {X} ε δ = γ
    where
     h : canonical-map ι ρ ε δ ∼ -id (ε ＝ δ)
     h (refl {ε}) = 𝓻𝓮𝒻𝓵 (𝓻𝓮𝒻𝓵 ε)

     γ : is-equiv (canonical-map ι ρ ε δ)
     γ = equiv-closed-under-∼ id (canonical-map ι ρ ε δ) (id-is-equiv (ε ＝ δ)) h

 _≅_  :  SelectionSpace → SelectionSpace → 𝓤 ⊔ 𝓥 ̇

 (X , ε , _) ≅ (Y , δ , _) =

             Σ f ꞉ (X → Y), is-equiv f
                          × ((λ (q : Y → R) → f (ε (q ∘ f))) ＝ δ)

 characterization-of-selection-space-＝ : is-univalent 𝓤
                                       → (A B : SelectionSpace)

                                       → (A ＝ B) ≃ (A ≅ B)

 characterization-of-selection-space-＝ ua = characterization-of-＝-with-axioms ua
                                             sns-data
                                             axioms axiomss

module contrived-example (𝓤 : Universe) where

 open sip

 contrived-＝ : is-univalent 𝓤 →

    (X Y : 𝓤 ̇ ) (φ : (X → X) → X) (γ : (Y → Y) → Y)
  →
    ((X , φ) ＝ (Y , γ)) ≃ (Σ f ꞉ (X → Y)
                         , Σ i ꞉ is-equiv f
                         , (λ (g : Y → Y) → f (φ (inverse f i ∘ g ∘ f))) ＝ γ)

 contrived-＝ ua X Y φ γ =
   characterization-of-＝ ua
    ((λ (X , φ) (Y , γ) (f , i) → (λ (g : Y → Y) → f (φ (inverse f i ∘ g ∘ f))) ＝ γ) ,
     (λ (X , φ) → 𝓻𝓮𝒻𝓵 φ) ,
     (λ φ γ → equiv-closed-under-∼ _ _ (id-is-equiv (φ ＝ γ)) (λ {(refl {φ}) → 𝓻𝓮𝒻𝓵 (𝓻𝓮𝒻𝓵 φ)})))
    (X , φ) (Y , γ)

module generalized-functor-algebra
         {𝓤 𝓥 : Universe}
         (F : 𝓤 ̇ → 𝓥 ̇ )
         (𝓕 : {X Y : 𝓤 ̇ } → (X → Y) → F X → F Y)
         (𝓕-id : {X : 𝓤 ̇ } → 𝓕 (-id X) ＝ -id (F X))
       where

 open sip

 S : 𝓤 ̇ → 𝓤 ⊔ 𝓥 ̇
 S X = F X → X

 sns-data : SNS S (𝓤 ⊔ 𝓥)
 sns-data = (ι , ρ , θ)
  where
   ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓤 ⊔ 𝓥 ̇
   ι (X , α) (Y , β) (f , _) = f ∘ α ＝ β ∘ 𝓕 f

   ρ : (A : Σ S) → ι A A (≃-refl ⟨ A ⟩)
   ρ (X , α) = α        ＝⟨ ap (α ∘_) (𝓕-id ⁻¹) ⟩
               α ∘ 𝓕 id ∎

   θ : {X : 𝓤 ̇ } (α β : S X) → is-equiv (canonical-map ι ρ α β)
   θ {X} α β = γ
    where
     c : α ＝ β → α ＝ β ∘ 𝓕 id
     c = transport (α ＝_) (ρ (X , β))

     i : is-equiv c
     i = transports-are-equivs (ρ (X , β))

     h : canonical-map ι ρ α β ∼ c
     h refl = ρ (X , α)           ＝⟨ refl-left-neutral ⁻¹ ⟩
              𝓻𝓮𝒻𝓵 α ∙ ρ (X , α) ∎

     γ : is-equiv (canonical-map ι ρ α β)
     γ = equiv-closed-under-∼ c (canonical-map ι ρ α β) i h

 characterization-of-functor-algebra-＝ : is-univalent 𝓤
   → (X Y : 𝓤 ̇ ) (α : F X → X) (β : F Y → Y)

   → ((X , α) ＝ (Y , β))  ≃  (Σ f ꞉ (X → Y), is-equiv f × (f ∘ α ＝ β ∘ 𝓕 f))

 characterization-of-functor-algebra-＝ ua X Y α β =
   characterization-of-＝ ua sns-data (X , α) (Y , β)

type-valued-preorder-S : 𝓤 ̇ → 𝓤 ⊔ (𝓥 ⁺) ̇
type-valued-preorder-S {𝓤} {𝓥} X = Σ _≤_ ꞉ (X → X → 𝓥 ̇ )
                                         , ((x : X) → x ≤ x)
                                         × ((x y z : X) → x ≤ y → y ≤ z → x ≤ z)

module type-valued-preorder
        (𝓤 𝓥 : Universe)
        (ua : Univalence)
       where

 open sip

 fe : Fun-Ext
 fe {𝓤} {𝓥} = Univalence-gives-FunExt ua 𝓤 𝓥

 S : 𝓤 ̇ → 𝓤 ⊔ (𝓥 ⁺) ̇
 S = type-valued-preorder-S {𝓤} {𝓥}

 Type-valued-preorder : (𝓤 ⊔ 𝓥) ⁺ ̇
 Type-valued-preorder = Σ S

 Ob : Σ S → 𝓤 ̇
 Ob (X , homX , idX , compX ) = X

 hom : (𝓧 : Σ S) → Ob 𝓧 → Ob 𝓧 → 𝓥 ̇
 hom (X , homX , idX , compX) = homX

 𝒾𝒹 : (𝓧 : Σ S) (x : Ob 𝓧) → hom 𝓧 x x
 𝒾𝒹 (X , homX , idX , compX) = idX

 comp : (𝓧 : Σ S) (x y z : Ob 𝓧) → hom 𝓧 x y → hom 𝓧 y z → hom 𝓧 x z
 comp (X , homX , idX , compX) = compX

 functorial : (𝓧 𝓐 : Σ S)
            → (F : Ob 𝓧 → Ob 𝓐)
            → ((x y : Ob 𝓧) → hom 𝓧 x y → hom 𝓐 (F x) (F y))
            → 𝓤 ⊔ 𝓥 ̇

 functorial 𝓧 𝓐 F 𝓕' = pidentity × pcomposition
  where

   _o_ : {x y z : Ob 𝓧} → hom 𝓧 y z → hom 𝓧 x y → hom 𝓧 x z
   g o f = comp 𝓧 _ _ _ f g

   _□_ : {a b c : Ob 𝓐} → hom 𝓐 b c → hom 𝓐 a b → hom 𝓐 a c
   g □ f = comp 𝓐 _ _ _ f g

   𝓕 : {x y : Ob 𝓧} → hom 𝓧 x y → hom 𝓐 (F x) (F y)
   𝓕 f = 𝓕' _ _ f

   pidentity = (λ x → 𝓕 (𝒾𝒹 𝓧 x)) ＝ (λ x → 𝒾𝒹 𝓐 (F x))

   pcomposition = (λ x y z (f : hom 𝓧 x y) (g : hom 𝓧 y z) → 𝓕 (g o f))
                ＝ (λ x y z (f : hom 𝓧 x y) (g : hom 𝓧 y z) → 𝓕 g □ 𝓕 f)

 sns-data : SNS S (𝓤 ⊔ (𝓥 ⁺))
 sns-data = (ι , ρ , θ)
  where
   ι : (𝓧 𝓐 : Σ S) → ⟨ 𝓧 ⟩ ≃ ⟨ 𝓐 ⟩ → 𝓤 ⊔ (𝓥 ⁺) ̇
   ι 𝓧 𝓐 (F , _) = Σ p ꞉ hom 𝓧 ＝ (λ x y → hom 𝓐 (F x) (F y))
                       , functorial 𝓧 𝓐 F (λ x y → transport (λ - → - x y) p)

   ρ : (𝓧 : Σ S) → ι 𝓧 𝓧 (≃-refl ⟨ 𝓧 ⟩)
   ρ 𝓧 = 𝓻𝓮𝒻𝓵 (hom 𝓧) , 𝓻𝓮𝒻𝓵 (𝒾𝒹 𝓧) , 𝓻𝓮𝒻𝓵 (comp 𝓧)

   θ : {X : 𝓤 ̇ } (s t : S X) → is-equiv (canonical-map ι ρ s t)
   θ {X} (homX , idX , compX) (homA , idA , compA) = g
    where
     φ = canonical-map ι ρ (homX , idX , compX) (homA , idA , compA)

     γ : codomain φ → domain φ
     γ (refl , refl , refl) = refl

     η : γ ∘ φ ∼ id
     η refl = refl

     ε : φ ∘ γ ∼ id
     ε (refl , refl , refl) = refl

     g : is-equiv φ
     g = qinvs-are-equivs φ (γ , η , ε)

 lemma : (𝓧 𝓐 : Σ S) (F : Ob 𝓧 → Ob 𝓐)
       →
         (Σ p ꞉ hom 𝓧 ＝ (λ x y → hom 𝓐 (F x) (F y))
              , functorial 𝓧 𝓐 F (λ x y → transport (λ - → - x y) p))
       ≃
         (Σ 𝓕 ꞉ ((x y : Ob 𝓧) → hom 𝓧 x y → hom 𝓐 (F x) (F y))
              , (∀ x y → is-equiv (𝓕 x y))
              × functorial 𝓧 𝓐 F 𝓕)

 lemma 𝓧 𝓐 F = γ
  where
   e = (hom 𝓧 ＝ λ x y → hom 𝓐 (F x) (F y))                            ≃⟨ i ⟩
       (∀ x y → hom 𝓧 x y ＝ hom 𝓐 (F x) (F y))                        ≃⟨ ii ⟩
       (∀ x y → hom 𝓧 x y ≃ hom 𝓐 (F x) (F y))                        ≃⟨ iii ⟩
       (∀ x → Σ φ ꞉ (∀ y → hom 𝓧 x y → hom 𝓐 (F x) (F y))
                  , ∀ y → is-equiv (φ y))                             ≃⟨ iv ⟩
       (Σ 𝓕 ꞉ ((x y : Ob 𝓧) → hom 𝓧 x y → hom 𝓐 (F x) (F y))
            , (∀ x y → is-equiv (𝓕 x y)))                             ■
    where
     i   = ≃-funext₂ fe fe (hom 𝓧 )  λ x y → hom 𝓐 (F x) (F y)
     ii  = Π-cong fe fe _ _ _
            (λ x → Π-cong fe fe _ _ _
            (λ y → univalence-≃ (ua 𝓥) (hom 𝓧 x y) (hom 𝓐 (F x) (F y))))
     iii = Π-cong fe fe _ _ _ (λ y → ΠΣ-distr-≃)
     iv  = ΠΣ-distr-≃

   v : (p : hom 𝓧 ＝ λ x y → hom 𝓐 (F x) (F y))
     → functorial 𝓧 𝓐 F (λ x y → transport (λ - → - x y) p)
     ≃ functorial 𝓧 𝓐 F (pr₁ (⌜ e ⌝ p))

   v refl = ≃-refl _

   γ =

    (Σ p ꞉ hom 𝓧 ＝ (λ x y → hom 𝓐 (F x) (F y))
         , functorial 𝓧 𝓐 F (λ x y → transport (λ - → - x y) p)) ≃⟨ vi ⟩

    (Σ p ꞉ hom 𝓧 ＝ (λ x y → hom 𝓐 (F x) (F y))
         , functorial 𝓧 𝓐 F (pr₁ (⌜ e ⌝ p)))                     ≃⟨ vii ⟩

    (Σ σ ꞉ (Σ 𝓕 ꞉ ((x y : Ob 𝓧) → hom 𝓧 x y → hom 𝓐 (F x) (F y))
                , (∀ x y → is-equiv (𝓕 x y)))
         , functorial 𝓧 𝓐 F (pr₁ σ))                             ≃⟨ viii ⟩

    (Σ 𝓕 ꞉ ((x y : Ob 𝓧) → hom 𝓧 x y → hom 𝓐 (F x) (F y))
                  , (∀ x y → is-equiv (𝓕 x y))
                  × functorial 𝓧 𝓐 F 𝓕)                          ■
    where
     vi   = Σ-cong v
     vii  = Σ-change-of-variable _ ⌜ e ⌝ (⌜⌝-is-equiv e)
     viii = Σ-assoc

 characterization-of-type-valued-preorder-＝ :

      (𝓧 𝓐 : Σ S)
    →
      (𝓧 ＝ 𝓐)
    ≃
      (Σ F ꞉ (Ob 𝓧 → Ob 𝓐)
           , is-equiv F
           × (Σ 𝓕 ꞉ ((x y : Ob 𝓧) → hom 𝓧 x y → hom 𝓐 (F x) (F y))
                  , (∀ x y → is-equiv (𝓕 x y))
                  × functorial 𝓧 𝓐 F 𝓕))

 characterization-of-type-valued-preorder-＝ 𝓧 𝓐 =

   (𝓧 ＝ 𝓐)                                                              ≃⟨ i ⟩
   (Σ F ꞉ (Ob 𝓧 → Ob 𝓐)
        , is-equiv F
        × (Σ p ꞉ hom 𝓧 ＝ (λ x y → hom 𝓐 (F x) (F y))
               , functorial 𝓧 𝓐 F (λ x y → transport (λ - → - x y) p))) ≃⟨ ii ⟩
   (Σ F ꞉ (Ob 𝓧 → Ob 𝓐)
     , is-equiv F
     × (Σ 𝓕 ꞉ ((x y : Ob 𝓧) → hom 𝓧 x y → hom 𝓐 (F x) (F y))
            , (∀ x y → is-equiv (𝓕 x y))
            × functorial 𝓧 𝓐 F 𝓕))                                      ■

  where
   i  = characterization-of-＝ (ua 𝓤) sns-data 𝓧 𝓐
   ii = Σ-cong (λ F → Σ-cong (λ _ → lemma 𝓧 𝓐 F))

module type-valued-preorder-with-axioms
        (𝓤 𝓥 𝓦 : Universe)
        (ua : Univalence)
        (axioms  : (X : 𝓤 ̇ ) → type-valued-preorder-S {𝓤} {𝓥} X → 𝓦 ̇ )
        (axiomss : (X : 𝓤 ̇ ) (s : type-valued-preorder-S X) → is-prop (axioms X s))
       where

 open sip
 open sip-with-axioms
 open type-valued-preorder 𝓤 𝓥 ua

 S' : 𝓤 ̇ → 𝓤 ⊔ (𝓥 ⁺) ⊔ 𝓦 ̇
 S' X = Σ s ꞉ S X , axioms X s

 sns-data' : SNS S' (𝓤 ⊔ (𝓥 ⁺))
 sns-data' = add-axioms axioms axiomss sns-data

 characterization-of-type-valued-preorder-＝-with-axioms :

      (𝓧' 𝓐' : Σ S')
    →
      (𝓧' ＝ 𝓐')
    ≃
      (Σ F ꞉ (Ob [ 𝓧' ] → Ob [ 𝓐' ])
           , is-equiv F
           × (Σ 𝓕 ꞉ ((x y : Ob [ 𝓧' ]) → hom [ 𝓧' ] x y → hom [ 𝓐' ] (F x) (F y))
                    , (∀ x y → is-equiv (𝓕 x y))
                    × functorial [ 𝓧' ] [ 𝓐' ] F 𝓕))

 characterization-of-type-valued-preorder-＝-with-axioms 𝓧' 𝓐' =

  (𝓧' ＝ 𝓐')                     ≃⟨ i ⟩
  ([ 𝓧' ] ≃[ sns-data ] [ 𝓐' ]) ≃⟨ ii ⟩
  _                              ■

  where
   i  = characterization-of-＝-with-axioms (ua 𝓤) sns-data axioms axiomss 𝓧' 𝓐'
   ii = Σ-cong (λ F → Σ-cong (λ _ → lemma [ 𝓧' ] [ 𝓐' ] F))

module category
        (𝓤 𝓥 : Universe)
        (ua : Univalence)
       where

 open type-valued-preorder-with-axioms 𝓤 𝓥 (𝓤 ⊔ 𝓥) ua

 fe : Fun-Ext
 fe {𝓤} {𝓥} = Univalence-gives-FunExt ua 𝓤 𝓥

 S : 𝓤 ̇ → 𝓤 ⊔ (𝓥 ⁺) ̇
 S = type-valued-preorder-S {𝓤} {𝓥}

 category-axioms : (X : 𝓤 ̇ ) → S X → 𝓤 ⊔ 𝓥 ̇
 category-axioms X (homX , idX , compX) = hom-sets × identityl × identityr × associativity
  where
   _o_ : {x y z : X} → homX y z → homX x y → homX x z
   g o f = compX _ _ _ f g

   hom-sets      = ∀ x y → is-set (homX x y)

   identityl     = ∀ x y (f : homX x y) → f o (idX x) ＝ f

   identityr     = ∀ x y (f : homX x y) → (idX y) o f ＝ f

   associativity = ∀ x y z t (f : homX x y) (g : homX y z) (h : homX z t)
                 → (h o g) o f ＝ h o (g o f)

 category-axioms-prop : (X : 𝓤 ̇ ) (s : S X) → is-prop (category-axioms X s)
 category-axioms-prop X (homX , idX , compX) ca = γ ca
  where
   i : ∀ x y → is-set (homX x y)
   i = pr₁ ca

   γ : is-prop (category-axioms X (homX , idX , compX))
   γ = ×-is-prop ss (×-is-prop ls (×-is-prop rs as))
    where
     ss = Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → being-set-is-prop fe))

     ls = Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → Π-is-prop fe
           (λ f → i x y)))

     rs = Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → Π-is-prop fe
           (λ f → i x y)))

     as = Π-is-prop fe
           (λ x → Π-is-prop fe
           (λ y → Π-is-prop fe
           (λ z → Π-is-prop fe
           (λ t → Π-is-prop fe
           (λ f → Π-is-prop fe
           (λ g → Π-is-prop fe
           (λ h → i x t)))))))

 Cat : (𝓤 ⊔ 𝓥)⁺ ̇
 Cat = Σ X ꞉ 𝓤 ̇ , Σ s ꞉ S X , category-axioms X s

 Ob : Cat → 𝓤 ̇
 Ob (X , (homX , idX , compX) , _) = X

 hom : (𝓧 : Cat) → Ob 𝓧 → Ob 𝓧 → 𝓥 ̇
 hom (X , (homX , idX , compX) , _) = homX

 𝒾𝒹 : (𝓧 : Cat) (x : Ob 𝓧) → hom 𝓧 x x
 𝒾𝒹 (X , (homX , idX , compX) , _) = idX

 comp : (𝓧 : Cat) (x y z : Ob 𝓧) (f : hom 𝓧 x y) (g : hom 𝓧 y z) → hom 𝓧 x z
 comp (X , (homX , idX , compX) , _) = compX

 is-functorial : (𝓧 𝓐 : Cat)
               → (F : Ob 𝓧 → Ob 𝓐)
               → ((x y : Ob 𝓧) → hom 𝓧 x y → hom 𝓐 (F x) (F y))
               → 𝓤 ⊔ 𝓥 ̇

 is-functorial 𝓧 𝓐 F 𝓕' = pidentity × pcomposition
  where
   _o_ : {x y z : Ob 𝓧} → hom 𝓧 y z → hom 𝓧 x y → hom 𝓧 x z
   g o f = comp 𝓧 _ _ _ f g

   _□_ : {a b c : Ob 𝓐} → hom 𝓐 b c → hom 𝓐 a b → hom 𝓐 a c
   g □ f = comp 𝓐 _ _ _ f g

   𝓕 : {x y : Ob 𝓧} → hom 𝓧 x y → hom 𝓐 (F x) (F y)
   𝓕 f = 𝓕' _ _ f

   pidentity    = (λ x → 𝓕 (𝒾𝒹 𝓧 x)) ＝ (λ x → 𝒾𝒹 𝓐 (F x))

   pcomposition = (λ x y z (f : hom 𝓧 x y) (g : hom 𝓧 y z) → 𝓕 (g o f))
                ＝ (λ x y z (f : hom 𝓧 x y) (g : hom 𝓧 y z) → 𝓕 g □ 𝓕 f)

 _⋍_ : Cat → Cat → 𝓤 ⊔ 𝓥 ̇

 𝓧 ⋍ 𝓐 = Σ F ꞉ (Ob 𝓧 → Ob 𝓐)
              , is-equiv F
              × (Σ 𝓕 ꞉ ((x y : Ob 𝓧) → hom 𝓧 x y → hom 𝓐 (F x) (F y))
                     , (∀ x y → is-equiv (𝓕 x y))
                     × is-functorial 𝓧 𝓐 F 𝓕)

 idtoeqCat : (𝓧 𝓐 : Cat) → 𝓧 ＝ 𝓐 → 𝓧 ⋍ 𝓐
 idtoeqCat 𝓧 𝓧 (refl {𝓧}) = -id (Ob 𝓧 ) ,
                              id-is-equiv (Ob 𝓧 ) ,
                              (λ x y → -id (hom 𝓧 x y)) ,
                              (λ x y → id-is-equiv (hom 𝓧 x y)) ,
                              𝓻𝓮𝒻𝓵 (𝒾𝒹 𝓧) ,
                              𝓻𝓮𝒻𝓵 (comp 𝓧)

 characterization-of-category-＝ : (𝓧 𝓐 : Cat) → (𝓧 ＝ 𝓐) ≃ (𝓧 ⋍ 𝓐)
 characterization-of-category-＝ = characterization-of-type-valued-preorder-＝-with-axioms
                                   category-axioms category-axioms-prop

 idtoeqCat-is-equiv : (𝓧 𝓐 : Cat) → is-equiv (idtoeqCat 𝓧 𝓐)
 idtoeqCat-is-equiv 𝓧 𝓐 = equiv-closed-under-∼ _ _
                           (⌜⌝-is-equiv (characterization-of-category-＝ 𝓧 𝓐))
                           (γ 𝓧 𝓐)
  where
   γ : (𝓧 𝓐 : Cat) → idtoeqCat 𝓧 𝓐 ∼ ⌜ characterization-of-category-＝ 𝓧 𝓐 ⌝
   γ 𝓧 𝓧 (refl {𝓧}) = 𝓻𝓮𝒻𝓵 (idtoeqCat 𝓧 𝓧 (𝓻𝓮𝒻𝓵 𝓧))

\end{code}

We now consider ∞-magmas with the binary operation generalized to an
operation of arbitrary arity. This is used to define σ-frames.

\begin{code}

module ∞-bigmagma {𝓤 𝓥 : Universe} (I : 𝓥 ̇ ) where

 open sip

 ∞-bigmagma-structure : 𝓤 ̇ → 𝓤 ⊔ 𝓥 ̇
 ∞-bigmagma-structure A = (I → A) → A

 ∞-Bigmagma : 𝓤 ⁺ ⊔ 𝓥 ̇
 ∞-Bigmagma = Σ A ꞉ 𝓤 ̇ , ∞-bigmagma-structure A

 sns-data : SNS ∞-bigmagma-structure (𝓤 ⊔ 𝓥)
 sns-data = (ι , ρ , θ)
  where
   ι : (𝓐 𝓐' : ∞-Bigmagma) → ⟨ 𝓐 ⟩ ≃ ⟨ 𝓐' ⟩ → 𝓤 ⊔ 𝓥 ̇
   ι (A , sup) (A' , sup') (f , _) = (λ 𝕒 → f (sup 𝕒)) ＝ (λ 𝕒 → sup' (n ↦ f (𝕒 n)))

   ρ : (𝓐 : ∞-Bigmagma) → ι 𝓐 𝓐 (≃-refl ⟨ 𝓐 ⟩)
   ρ (A , sup) = 𝓻𝓮𝒻𝓵 sup

   h : {A : 𝓤 ̇ } {sup sup' : ∞-bigmagma-structure A}
     → canonical-map ι ρ sup sup' ∼ -id (sup ＝ sup')

   h (refl {sup}) = 𝓻𝓮𝒻𝓵 (𝓻𝓮𝒻𝓵 sup)

   θ : {A : 𝓤 ̇ } (sup sup' : ∞-bigmagma-structure A)
     → is-equiv (canonical-map ι ρ sup sup')

   θ sup sup' = equiv-closed-under-∼ _ _ (id-is-equiv (sup ＝ sup')) h

 _≅[∞-Bigmagma]_ : ∞-Bigmagma → ∞-Bigmagma → 𝓤 ⊔ 𝓥 ̇
 (A , sup) ≅[∞-Bigmagma] (A' , sup') =

           Σ f ꞉ (A → A'), is-equiv f
                         × ((λ 𝕒 → f (sup 𝕒)) ＝ (λ 𝕒 → sup' (n ↦ f (𝕒 n))))

 characterization-of-∞-Bigmagma-＝ : is-univalent 𝓤
                                  → (A B : ∞-Bigmagma)
                                  → (A ＝ B) ≃ (A ≅[∞-Bigmagma] B)
 characterization-of-∞-Bigmagma-＝ ua = characterization-of-＝ ua sns-data

\end{code}

We use the above in another module to define σ-frames.

We now consider ∞-bigmagmas with all operations of all arities, which
we use in another module to define frames.

\begin{code}

module ∞-hugemagma {𝓤 𝓥 : Universe} where

 open sip

 ∞-hugemagma-structure : 𝓤 ̇ → 𝓤 ⊔ (𝓥 ⁺) ̇
 ∞-hugemagma-structure A = {N : 𝓥 ̇ } → (N → A) → A

 ∞-Hugemagma : (𝓤 ⊔ 𝓥)⁺ ̇
 ∞-Hugemagma = Σ A ꞉ 𝓤 ̇ , ∞-hugemagma-structure A

 sns-data : SNS ∞-hugemagma-structure (𝓤 ⊔ (𝓥 ⁺))
 sns-data = (ι , ρ , θ)
  where
   ι : (𝓐 𝓐' : ∞-Hugemagma) → ⟨ 𝓐 ⟩ ≃ ⟨ 𝓐' ⟩ → 𝓤 ⊔ (𝓥 ⁺) ̇
   ι (A , sup) (A' , sup') (f , _) = (λ {N} (𝕒 : N → A) → f (sup 𝕒)) ＝ (λ {N} 𝕒 → sup' (i ↦ f (𝕒 i)))

   ρ : (𝓐 : ∞-Hugemagma) → ι 𝓐 𝓐 (≃-refl ⟨ 𝓐 ⟩)
   ρ (A , sup) = refl

   h : {A : 𝓤 ̇ } {sup sup' : ∞-hugemagma-structure A}
     → canonical-map ι ρ sup sup' ∼ id

   h refl = refl

   θ : {A : 𝓤 ̇ } (sup sup' : ∞-hugemagma-structure A)
     → is-equiv (canonical-map ι ρ sup sup')

   θ sup sup' = equiv-closed-under-∼ _ _ (id-is-equiv _) h

 _≅[∞-Hugemagma]_ : ∞-Hugemagma → ∞-Hugemagma → 𝓤 ⊔ (𝓥 ⁺) ̇
 (A , sup) ≅[∞-Hugemagma] (A' , sup') =

           Σ f ꞉ (A → A'), is-equiv f
                         × ((λ {N} (𝕒 : N → A) → f (sup 𝕒)) ＝ (λ {N} (𝕒 : N → A) → sup' (i ↦ f (𝕒 i))))

 characterization-of-∞-Hugemagma-＝ : is-univalent 𝓤
                                   → (A B : ∞-Hugemagma)
                                   → (A ＝ B) ≃ (A ≅[∞-Hugemagma] B)
 characterization-of-∞-Hugemagma-＝ ua = characterization-of-＝ ua sns-data

\end{code}