MGS.SIP

This is ported from the Midlands Graduate School 2019 lecture notes

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


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

module MGS.SIP where

open import MGS.More-FunExt-Consequences public
open import MGS.Yoneda                   public
open import MGS.Powerset                 public
open import MGS.Classifiers              public
open import MGS.Subsingleton-Truncation  public

module sip where

 ⟨_⟩ : {S : 𝓤 ̇ → 𝓥 ̇ } → Σ S → 𝓤 ̇
 ⟨ X , s ⟩ = X

 structure : {S : 𝓤 ̇ → 𝓥 ̇ } (A : Σ S) → S ⟨ A ⟩
 structure (X , s) = s

 canonical-map : {S : 𝓤 ̇ → 𝓥 ̇ }
                 (ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦 ̇ )
                 (ρ : (A : Σ S) → ι A A (id-≃ ⟨ A ⟩))
                 {X : 𝓤 ̇ }
                 (s t : S X)

               → s ＝ t → ι (X , s) (X , t) (id-≃ X)

 canonical-map ι ρ {X} s s (refl s) = ρ (X , s)

 SNS : (𝓤 ̇ → 𝓥 ̇ ) → (𝓦 : Universe) → 𝓤 ⁺ ⊔ 𝓥 ⊔ (𝓦 ⁺) ̇

 SNS {𝓤} {𝓥} S 𝓦 = Σ ι ꞉ ((A B : Σ S) → (⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦 ̇ ))
                  , Σ ρ ꞉ ((A : Σ S) → ι A A (id-≃ ⟨ A ⟩))
                  , ({X : 𝓤 ̇ } (s t : S X) → is-equiv (canonical-map ι ρ s t))

 homomorphic : {S : 𝓤 ̇ → 𝓥 ̇ } → SNS S 𝓦
             → (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦 ̇

 homomorphic (ι , ρ , θ) = ι

 _≃[_]_ : {S : 𝓤 ̇ → 𝓥 ̇ } → Σ S → SNS S 𝓦 → Σ S → 𝓤 ⊔ 𝓦 ̇

 A ≃[ σ ] B = Σ f ꞉ (⟨ A ⟩ → ⟨ B ⟩)
            , Σ i ꞉ is-equiv f
            , homomorphic σ A B (f , i)

 Id→homEq : {S : 𝓤 ̇ → 𝓥 ̇ } (σ : SNS S 𝓦)
          → (A B : Σ S) → (A ＝ B) → (A ≃[ σ ] B)

 Id→homEq (_ , ρ , _) A A (refl A) = id , id-is-equiv ⟨ A ⟩ , ρ A

 homomorphism-lemma : {S : 𝓤 ̇ → 𝓥 ̇ } (σ : SNS S 𝓦)
                      (A B : Σ S) (p : ⟨ A ⟩ ＝ ⟨ B ⟩)
                    →
                      (transport S p (structure A) ＝ structure B)
                    ≃  homomorphic σ A B (Id→Eq ⟨ A ⟩ ⟨ B ⟩ p)

 homomorphism-lemma (ι , ρ , θ) (X , s) (X , t) (refl X) = γ
  where
   γ : (s ＝ t) ≃ ι (X , s) (X , t) (id-≃ X)
   γ = (canonical-map ι ρ s t , θ s t)

 characterization-of-＝ : is-univalent 𝓤
                       → {S : 𝓤 ̇ → 𝓥 ̇ } (σ : SNS S 𝓦)
                       → (A B : Σ S)

                       → (A ＝ B) ≃ (A ≃[ σ ] B)

 characterization-of-＝ ua {S} σ A B =

    (A ＝ B)                                                           ≃⟨ i ⟩
    (Σ p ꞉ ⟨ A ⟩ ＝ ⟨ B ⟩ , transport S p (structure A) ＝ structure B) ≃⟨ ii ⟩
    (Σ p ꞉ ⟨ A ⟩ ＝ ⟨ B ⟩ , ι A B (Id→Eq ⟨ A ⟩ ⟨ B ⟩ p))               ≃⟨ iii ⟩
    (Σ e ꞉ ⟨ A ⟩ ≃ ⟨ B ⟩ , ι A B e)                                   ≃⟨ iv ⟩
    (A ≃[ σ ] B)                                                      ■

  where
   ι   = homomorphic σ

   i   = Σ-＝-≃ A B
   ii  = Σ-cong (homomorphism-lemma σ A B)
   iii = ≃-sym (Σ-change-of-variable (ι A B) (Id→Eq ⟨ A ⟩ ⟨ B ⟩) (ua ⟨ A ⟩ ⟨ B ⟩))
   iv  = Σ-assoc

 Id→homEq-is-equiv : (ua : is-univalent 𝓤) {S : 𝓤 ̇ → 𝓥 ̇ } (σ : SNS S 𝓦)
                   → (A B : Σ S) → is-equiv (Id→homEq σ A B)

 Id→homEq-is-equiv ua {S} σ A B = γ
  where
   h : (A B : Σ S) → Id→homEq σ A B ∼ ⌜ characterization-of-＝ ua σ A B ⌝
   h A A (refl A) = refl _

   γ : is-equiv (Id→homEq σ A B)
   γ = equivs-closed-under-∼
       (⌜⌝-is-equiv (characterization-of-＝ ua σ A B))
       (h A B)

 module _ {S : 𝓤 ̇ → 𝓥 ̇ }
          (ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦 ̇ )
          (ρ : (A : Σ S) → ι A A (id-≃ ⟨ A ⟩))
          {X : 𝓤 ̇ }

        where

  canonical-map-charac : (s t : S X) (p : s ＝ t)

                       → canonical-map ι ρ s t p
                       ＝ transport (λ - → ι (X , s) (X , -) (id-≃ X)) p (ρ (X , s))

  canonical-map-charac s = transport-lemma (λ t → ι (X , s) (X , t) (id-≃ X)) s
                            (canonical-map ι ρ s)

  when-canonical-map-is-equiv : ((s t : S X) → is-equiv (canonical-map ι ρ s t))
                              ↔ ((s : S X) → ∃! t ꞉ S X , ι (X , s) (X , t) (id-≃ X))

  when-canonical-map-is-equiv = (λ e s → fiberwise-equiv-universal (A s) s (τ s) (e s)) ,
                                (λ φ s → universal-fiberwise-equiv (A s) (φ s) s (τ s))
   where
    A = λ s t → ι (X , s) (X , t) (id-≃ X)
    τ = canonical-map ι ρ

  canonical-map-equiv-criterion : ((s t : S X) → (s ＝ t) ≃ ι (X , s) (X , t) (id-≃ X))
                                → (s t : S X) → is-equiv (canonical-map ι ρ s t)

  canonical-map-equiv-criterion φ s = fiberwise-equiv-criterion'
                                       (λ t → ι (X , s) (X , t) (id-≃ X))
                                       s (φ s) (canonical-map ι ρ s)

  canonical-map-equiv-criterion' : ((s t : S X) → ι (X , s) (X , t) (id-≃ X) ◁ (s ＝ t))
                                 → (s t : S X) → is-equiv (canonical-map ι ρ s t)

  canonical-map-equiv-criterion' φ s = fiberwise-equiv-criterion
                                        (λ t → ι (X , s) (X , t) (id-≃ X))
                                        s (φ s) (canonical-map ι ρ s)

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 (id-≃ ⟨ A ⟩)
   ρ (X , _·_) = refl _·_

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

   h (refl _·_) = refl (refl _·_)

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

   θ _·_ _*_ = equivs-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 ⌝ (refl A)
  ＝
    (𝑖𝑑 ⟨ A ⟩ , id-is-equiv ⟨ A ⟩ , refl _)

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

module sip-with-axioms where

 open sip

 [_] : {S : 𝓤 ̇ → 𝓥 ̇ } {axioms : (X : 𝓤 ̇ ) → S X → 𝓦 ̇ }
     → (Σ X ꞉ 𝓤 ̇ , Σ s ꞉ S X , axioms X s) → Σ S

 [ X , s , _ ] = (X , s)

 ⟪_⟫ : {S : 𝓤 ̇ → 𝓥 ̇ } {axioms : (X : 𝓤 ̇ ) → S X → 𝓦 ̇ }
     → (Σ X ꞉ 𝓤 ̇ , Σ s ꞉ S X , axioms X s) → 𝓤 ̇

 ⟪ X , _ , _ ⟫ = X

 add-axioms : {S : 𝓤 ̇ → 𝓥 ̇ }
              (axioms : (X : 𝓤 ̇ ) → S X → 𝓦 ̇ )
            → ((X : 𝓤 ̇ ) (s : S X) → is-subsingleton (axioms X s))

            → SNS S 𝓣
            → SNS (λ X → Σ s ꞉ S X , axioms X s) 𝓣

 add-axioms {𝓤} {𝓥} {𝓦} {𝓣} {S} axioms i (ι , ρ , θ) = ι' , ρ' , θ'
  where
   S' : 𝓤 ̇ → 𝓥 ⊔ 𝓦 ̇
   S' X = Σ s ꞉ S X , axioms X s

   ι' : (A B : Σ S') → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓣 ̇
   ι' A B = ι [ A ] [ B ]

   ρ' : (A : Σ S') → ι' A A (id-≃ ⟨ A ⟩)
   ρ' A = ρ [ A ]

   θ' : {X : 𝓤 ̇ } (s' t' : S' X) → is-equiv (canonical-map ι' ρ' s' t')
   θ' {X} (s , a) (t , b) = γ
    where
     π : S' X → S X
     π (s , _) = s

     j : is-embedding π
     j = pr₁-embedding (i X)

     k : {s' t' : S' X} → is-equiv (ap π {s'} {t'})
     k {s'} {t'} = embedding-gives-ap-is-equiv π j s' t'

     l : canonical-map ι' ρ' (s , a) (t , b)
       ∼ canonical-map ι ρ s t ∘ ap π {s , a} {t , b}

     l (refl (s , a)) = refl (ρ (X , s))

     e : is-equiv (canonical-map ι ρ s t ∘ ap π {s , a} {t , b})
     e = ∘-is-equiv (θ s t) k

     γ : is-equiv (canonical-map ι' ρ' (s , a) (t , b))
     γ = equivs-closed-under-∼ e l

 characterization-of-＝-with-axioms :

     is-univalent 𝓤
   → {S : 𝓤 ̇ → 𝓥 ̇ }
     (σ : SNS S 𝓣)
     (axioms : (X : 𝓤 ̇ ) → S X → 𝓦 ̇ )
   → ((X : 𝓤 ̇ ) (s : S X) → is-subsingleton (axioms X s))
   → (A B : Σ X ꞉ 𝓤 ̇ , Σ s ꞉ S X , axioms X s)

   → (A ＝ B) ≃ ([ A ] ≃[ σ ] [ B ])

 characterization-of-＝-with-axioms ua σ axioms i =
   characterization-of-＝ ua (add-axioms axioms i σ)

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-subsingleton (univalence-gives-dfunext 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 (id-≃ ⟨ A ⟩)
   ρ (X , x₀) = refl x₀

   θ : {X : 𝓤 ̇ } (x₀ x₁ : Pointed X) → is-equiv (canonical-map ι ρ x₀ x₁)
   θ x₀ x₁ = equivs-closed-under-∼ (id-is-equiv (x₀ ＝ x₁)) h
    where
     h : canonical-map ι ρ x₀ x₁ ∼ 𝑖𝑑 (x₀ ＝ x₁)
     h (refl x₀) = refl (refl 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 sip-join where

 technical-lemma :
     {X : 𝓤 ̇ } {A : X → X → 𝓥 ̇ }
     {Y : 𝓦 ̇ } {B : Y → Y → 𝓣 ̇ }
     (f : (x₀ x₁ : X) → x₀ ＝ x₁ → A x₀ x₁)
     (g : (y₀ y₁ : Y) → y₀ ＝ y₁ → B y₀ y₁)
   → ((x₀ x₁ : X) → is-equiv (f x₀ x₁))
   → ((y₀ y₁ : Y) → is-equiv (g y₀ y₁))

   → ((x₀ , y₀) (x₁ , y₁) : X × Y) → is-equiv (λ (p : (x₀ , y₀) ＝ (x₁ , y₁)) → f x₀ x₁ (ap pr₁ p) ,
                                                                               g y₀ y₁ (ap pr₂ p))
 technical-lemma {𝓤} {𝓥} {𝓦} {𝓣} {X} {A} {Y} {B} f g i j (x₀ , y₀) = γ
  where
   u : ∃! x₁ ꞉ X , A x₀ x₁
   u = fiberwise-equiv-universal (A x₀) x₀ (f x₀) (i x₀)

   v : ∃! y₁ ꞉ Y , B y₀ y₁
   v = fiberwise-equiv-universal (B y₀) y₀ (g y₀) (j y₀)

   C : X × Y → 𝓥 ⊔ 𝓣 ̇
   C (x₁ , y₁) = A x₀ x₁ × B y₀ y₁

   w : (∃! x₁ ꞉ X , A x₀ x₁)
     → (∃! y₁ ꞉ Y , B y₀ y₁)
     →  ∃! (x₁ , y₁) ꞉ X × Y , C (x₁ , y₁)
   w ((x₁ , a₁) , φ) ((y₁ , b₁) , ψ) = ((x₁ , y₁) , (a₁ , b₁)) , δ
    where
     p : ∀ x y a b
       → (x₁ , a₁) ＝ (x , a)
       → (y₁ , b₁) ＝ (y , b)
       → (x₁ , y₁) , (a₁ , b₁) ＝ (x , y) , (a , b)
     p .x₁ .y₁ .a₁ .b₁ (refl .(x₁ , a₁)) (refl .(y₁ , b₁)) = refl ((x₁ , y₁) , (a₁ , b₁))

     δ : (((x , y) , (a , b)) : Σ C) → (x₁ , y₁) , (a₁ , b₁) ＝ ((x , y) , (a , b))
     δ ((x , y) , (a , b)) = p x y a b (φ (x , a)) (ψ (y , b))

   τ : Nat (𝓨 (x₀ , y₀)) C
   τ (x₁ , y₁) p = f x₀ x₁ (ap pr₁ p) , g y₀ y₁ (ap pr₂ p)

   γ : is-fiberwise-equiv τ
   γ = universal-fiberwise-equiv C (w u v) (x₀ , y₀) τ


 open sip

 ⟪_⟫ : {S₀ : 𝓤 ̇ → 𝓥₀ ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
     → (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X) → 𝓤 ̇

 ⟪ X , s₀ , s₁ ⟫ = X

 [_]₀ : {S₀ : 𝓤 ̇ → 𝓥₀ ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
      → (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X) → Σ S₀

 [ X , s₀ , s₁ ]₀ = (X , s₀)

 [_]₁ : {S₀ : 𝓤 ̇ → 𝓥₀ ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
      → (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X) → Σ S₁

 [ X , s₀ , s₁ ]₁ = (X , s₁)

 join : {S₀ : 𝓤 ̇ → 𝓥₀ ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
      → SNS S₀ 𝓦₀
      → SNS S₁ 𝓦₁
      → SNS (λ X → S₀ X × S₁ X) (𝓦₀ ⊔ 𝓦₁)

 join {𝓤} {𝓥₀} {𝓥₁} {𝓦₀} {𝓦₁} {S₀} {S₁} (ι₀ , ρ₀ , θ₀) (ι₁ , ρ₁ , θ₁) = ι , ρ , θ
  where
   S : 𝓤 ̇ → 𝓥₀ ⊔ 𝓥₁ ̇
   S X = S₀ X × S₁ X

   ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦₀ ⊔ 𝓦₁ ̇
   ι A B e = ι₀ [ A ]₀ [ B ]₀ e  ×  ι₁ [ A ]₁ [ B ]₁ e

   ρ : (A : Σ S) → ι A A (id-≃ ⟨ A ⟩)
   ρ A = (ρ₀ [ A ]₀ , ρ₁ [ A ]₁)

   θ : {X : 𝓤 ̇ } (s t : S X) → is-equiv (canonical-map ι ρ s t)
   θ {X} (s₀ , s₁) (t₀ , t₁) = γ
    where
     c : (p : s₀ , s₁ ＝ t₀ , t₁) → ι₀ (X , s₀) (X , t₀) (id-≃ X)
                                 × ι₁ (X , s₁) (X , t₁) (id-≃ X)

     c p = (canonical-map ι₀ ρ₀ s₀ t₀ (ap pr₁ p) ,
            canonical-map ι₁ ρ₁ s₁ t₁ (ap pr₂ p))

     i : is-equiv c
     i = technical-lemma
          (canonical-map ι₀ ρ₀)
          (canonical-map ι₁ ρ₁)
          θ₀ θ₁ (s₀ , s₁) (t₀ , t₁)

     e : canonical-map ι ρ (s₀ , s₁) (t₀ , t₁) ∼ c
     e (refl (s₀ , s₁)) = refl (ρ₀ (X , s₀) , ρ₁ (X , s₁))

     γ : is-equiv (canonical-map ι ρ (s₀ , s₁) (t₀ , t₁))
     γ = equivs-closed-under-∼ i e

 _≃⟦_,_⟧_ : {S₀ : 𝓤 ̇ → 𝓥 ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }

          → (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X)
          → SNS S₀ 𝓦₀
          → SNS S₁ 𝓦₁
          → (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X)

          → 𝓤 ⊔ 𝓦₀ ⊔ 𝓦₁ ̇

 A ≃⟦ σ₀ , σ₁ ⟧ B = Σ f ꞉ (⟪ A ⟫ → ⟪ B ⟫)
                  , Σ i ꞉ is-equiv f , homomorphic σ₀ [ A ]₀ [ B ]₀ (f , i)
                                     × homomorphic σ₁ [ A ]₁ [ B ]₁ (f , i)

 characterization-of-join-＝ : is-univalent 𝓤
                            → {S₀ : 𝓤 ̇ → 𝓥 ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
                              (σ₀ : SNS S₀ 𝓦₀)  (σ₁ : SNS S₁ 𝓦₁)
                              (A B : Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X)

                            → (A ＝ B) ≃ (A ≃⟦ σ₀ , σ₁ ⟧ B)

 characterization-of-join-＝ ua σ₀ σ₁ = characterization-of-＝ ua (join σ₀ σ₁)

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} (ua : is-univalent 𝓤) where

 dfe : dfunext 𝓤 𝓤
 dfe = univalence-gives-dfunext ua

 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
                           × monoids.left-neutral  e _·_
                           × monoids.right-neutral e _·_
                           × monoids.associative     _·_

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

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

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

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

 sns-data : SNS (λ X → Σ s ꞉ monoid-structure X , monoid-axioms X s) 𝓤
 sns-data = add-axioms
              monoid-axioms monoid-axioms-subsingleton
              (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

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

 fe : dfunext 𝓤 𝓤
 fe = univalence-gives-dfunext ua

 associative : {X : 𝓤 ̇ } → (X → X → X) → 𝓤 ̇
 associative _·_ = ∀ x y z → (x · y) · z ＝ x · (y · z)

 ∞-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 (refl _·_)
        ＝ ((λ x y z → refl ((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) → ι 𝓧 𝓧 (id-≃ ⟨ 𝓧 ⟩)
   ρ (X , _·_ , α) = h , p
    where
     h : homomorphic _·_ _·_ id
     h = refl _·_

     p : (λ x y z → refl ((x · y) · z) ∙ ap id (α x y z)) ＝ α
     p = fe (λ x → fe (λ y → fe (λ z → refl-left ∙ ap-id (α x y z))))

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

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

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

       i : is-subsingleton (singleton-type' a)
       i = singletons-are-subsingletons _ (singleton-types'-are-singletons _ a)

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

       γ : c ＝ (_·_ , β) , refl _·_ , k
       γ = ap g q

   θ : {X : 𝓤 ̇ } (s t : ∞-amagma-structure X) → is-equiv (canonical-map ι ρ s t)
   θ {X} s = universal-fiberwise-equiv (λ t → ι (X , s) (X , t) (id-≃ X))
              (u X s) s (canonical-map ι ρ 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} (ua : is-univalent 𝓤) where

 hfe : hfunext 𝓤 𝓤
 hfe = univalence-gives-hfunext ua

 open sip
 open sip-with-axioms
 open monoid {𝓤} ua 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-subsingleton : (X : 𝓤 ̇ )
                             → (s : group-structure X)
                             → is-subsingleton (group-axiom X (pr₁ s))

 group-axiom-is-subsingleton X ((_·_ , e) , (s , l , r , a)) = γ
  where
   i : (x : X) → is-subsingleton (Σ 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-subsingleton (s (x · x') e) (s (x' · x) e)) t

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

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

 _≅_ : 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-＝ : (A B : Group) → (A ＝ B) ≃ (A ≅ B)
 characterization-of-group-＝ = characterization-of-＝ ua sns-data

 _≅'_ : 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-subsingleton : (G H : Group) (f : ⟨ G ⟩ → ⟨ H ⟩)
                                      → is-subsingleton (preserves-multiplication G H f)
 preservation-of-mult-is-subsingleton G H f = j
  where
   j : is-subsingleton (preserves-multiplication G H f)
   j = Π-is-set hfe
        (λ _ → Π-is-set hfe
        (λ _ → group-is-set H))
        (λ (x y : ⟨ G ⟩) → f (x ·⟨ G ⟩ y))
        (λ (x y : ⟨ G ⟩) → f x ·⟨ H ⟩ f y)

 being-homomorphism-is-subsingleton : (G H : Group) (f : ⟨ G ⟩ → ⟨ H ⟩)
                                    → is-subsingleton (is-homomorphism G H f)
 being-homomorphism-is-subsingleton G H f = i
  where

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

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

 notions-of-homomorphism-agree 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-subsingletons-are-equivalent _ _
        (being-homomorphism-is-subsingleton G H f)
        (preservation-of-mult-is-subsingleton G H f)
        (α , β)

 ≅-agreement : (G H : Group) → (G ≅ H) ≃ (G ≅' H)
 ≅-agreement G H = Σ-cong (λ f → Σ-cong (λ _ → notions-of-homomorphism-agree 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 : (G H : Group) → ⌜ ≅-agreement G H ⌝ ＝ forget-unit-preservation G H
 NB G H = refl _

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

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

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

 gfe : global-dfunext
 gfe = univalence-gives-global-dfunext ua

 open sip
 open monoid {𝓤} (ua 𝓤) hiding (sns-data ; _≅_)
 open group {𝓤} (ua 𝓤)

 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-subsingleton : (A : 𝓟 ⟨ G ⟩) → is-subsingleton (group-closed (_∈ A))
  being-group-closed-subset-is-subsingleton A = ×-is-subsingleton
                                                  (∈-is-subsingleton A (unit G))
                                               (×-is-subsingleton
                                                  (Π-is-subsingleton dfe
                                                     (λ x → Π-is-subsingleton dfe
                                                     (λ y → Π-is-subsingleton dfe
                                                     (λ _ → Π-is-subsingleton dfe
                                                     (λ _ → ∈-is-subsingleton A (x · y))))))
                                                  (Π-is-subsingleton dfe
                                                     (λ x → Π-is-subsingleton dfe
                                                     (λ _ → ∈-is-subsingleton A (inv G x)))))

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

  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-gives-ap-is-equiv ⟪_⟫ ⟪⟫-is-embedding

  subgroups-form-a-set : is-set Subgroups
  subgroups-form-a-set S T = equiv-to-subsingleton
                              (ap-⟪⟫ S T , ap-⟪⟫-is-equiv S T)
                              (powersets-are-sets' ua ⟪ S ⟫ ⟪ T ⟫)

  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-subsingletons-are-equivalent _ _
          (subgroups-form-a-set S T)
          (Π-is-subsingleton dfe
             (λ x → ×-is-subsingleton
                      (Π-is-subsingleton dfe (λ _ → ∈-is-subsingleton ⟪ T ⟫ x))
                      (Π-is-subsingleton dfe (λ _ → ∈-is-subsingleton ⟪ 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-subsingleton : is-subsingleton (group-closed (fiber h))
   having-group-closed-fiber-is-subsingleton = being-group-closed-subset-is-subsingleton
                                                (λ x → (fiber h x , e x))

   at-most-one-homomorphic-structure : is-subsingleton (Σ τ ꞉ 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 = gfe (λ x → gfe (λ 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-subsingleton X)
           (to-subtype-＝
              (monoid-axioms-subsingleton X)
              r)

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

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

   group-closed-fiber-gives-homomorphic-structure (unitc , mulc , invc) = τ , i
    where
     φ : (x : X) → fiber h (h x)
     φ x = (x , refl (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 = gfe (λ x → gfe (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 : group-closed (fiber h)
                         ≃ (Σ τ ꞉ T X , is-homomorphism (X , τ) G h)

   fiber-structure-lemma = logically-equivalent-subsingletons-are-equivalent _ _
                             having-group-closed-fiber-is-subsingleton
                             at-most-one-homomorphic-structure
                             (group-closed-fiber-gives-homomorphic-structure ,
                              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
       φ : Subtypes ⟨ G ⟩ → 𝓟 ⟨ G ⟩
       φ = χ-special is-subsingleton ⟨ G ⟩

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

       i    = id-≃ Subgroups
       ii   = Σ-change-of-variable (λ (A : 𝓟 ⟨ G ⟩) → group-closed (_∈ A)) φ j
       iii  = Σ-assoc
       iv   = Σ-cong (λ X → Σ-cong (λ (h , e) → fiber-structure-lemma h e))
       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 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 (id-≃ ⟨ A ⟩)
   ρ (X , g) = refl g

   k : {X : 𝓤 ̇ } {g h : S X} → canonical-map ι ρ g h ∼ 𝑖𝑑 (g ＝ h)
   k (refl g) = refl (refl g)

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

 _≅_  : 𝓤 / 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 generalized-metric-space
        {𝓤 𝓥 : Universe}
        (R : 𝓥 ̇ )
        (axioms  : (X : 𝓤 ̇ ) → (X → X → R) → 𝓤 ⊔ 𝓥 ̇ )
        (axiomss : (X : 𝓤 ̇ ) (d : X → X → R) → is-subsingleton (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 (id-≃ ⟨ A ⟩)
   ρ (X , d) = refl d

   h : {X : 𝓤 ̇ } {d e : S X} → canonical-map ι ρ d e ∼ 𝑖𝑑 (d ＝ e)
   h (refl d) = refl (refl d)

   θ : {X : 𝓤 ̇ } (d e : S X) → is-equiv (canonical-map ι ρ d e)
   θ d e = equivs-closed-under-∼ (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

module generalized-topological-space
        (𝓤 𝓥 : Universe)
        (R : 𝓥 ̇ )
        (axioms  : (X : 𝓤 ̇ ) → ((X → R) → R) → 𝓤 ⊔ 𝓥 ̇ )
        (axiomss : (X : 𝓤 ̇ ) (𝓞 : (X → R) → R) → is-subsingleton (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 (id-≃ ⟨ A ⟩)
   ρ (X , 𝓞) = refl 𝓞

   h : {X : 𝓤 ̇ } {𝓞 𝓞' : ℙℙ X} → canonical-map ι ρ 𝓞 𝓞' ∼ 𝑖𝑑 (𝓞 ＝ 𝓞')
   h (refl 𝓞) = refl (refl 𝓞)

   θ : {X : 𝓤 ̇ } (𝓞 𝓞' : ℙℙ X) → is-equiv (canonical-map ι ρ 𝓞 𝓞')
   θ {X} 𝓞 𝓞' = equivs-closed-under-∼ (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-subsingleton (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 (id-≃ ⟨ A ⟩)
   ρ (X , ε) = refl ε

   θ : {X : 𝓤 ̇ } (ε δ : S X) → is-equiv (canonical-map ι ρ ε δ)
   θ {X} ε δ = γ
    where
     h : canonical-map ι ρ ε δ ∼ 𝑖𝑑 (ε ＝ δ)
     h (refl ε) = refl (refl ε)

     γ : is-equiv (canonical-map ι ρ ε δ)
     γ = equivs-closed-under-∼ (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 , φ) → refl φ) ,
     (λ φ γ → equivs-closed-under-∼ (id-is-equiv (φ ＝ γ)) (λ {(refl φ) → refl (refl φ)})))
    (X , φ) (Y , γ)

module generalized-functor-algebra
         {𝓤 𝓥 : Universe}
         (F : 𝓤 ̇ → 𝓥 ̇ )
         (𝓕 : {X Y : 𝓤 ̇ } → (X → Y) → F X → F Y)
         (𝓕-id : {X : 𝓤 ̇ } → 𝓕 (𝑖𝑑 X) ＝ 𝑖𝑑 (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 (id-≃ ⟨ A ⟩)
   ρ (X , α) = α        ＝⟨ ap (α ∘_) (𝓕-id ⁻¹) ⟩
               α ∘ 𝓕 id ∎

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

     i : is-equiv c
     i = transport-is-equiv (α ＝_) (ρ (X , β))

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

     γ : is-equiv (canonical-map ι ρ α β)
     γ = equivs-closed-under-∼ 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 : global-dfunext
 fe = univalence-gives-global-dfunext ua

 hfe : global-hfunext
 hfe = univalence-gives-global-hfunext 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) → ι 𝓧 𝓧 (id-≃ ⟨ 𝓧 ⟩)
   ρ 𝓧 = refl (hom 𝓧) , refl (𝒾𝒹 𝓧) , refl (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 = invertibles-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   = hfunext₂-≃ hfe hfe (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 _) = id-≃ _

   γ =

    (Σ 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  = ≃-sym (Σ-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-subsingleton (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 : global-dfunext
 fe = univalence-gives-global-dfunext 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-subsingleton : (X : 𝓤 ̇ ) (s : S X) → is-subsingleton (category-axioms X s)
 category-axioms-subsingleton X (homX , idX , compX) ca = γ ca
  where
   i : ∀ x y → is-set (homX x y)
   i = pr₁ ca

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

     ls = Π-is-subsingleton fe
           (λ x → Π-is-subsingleton fe
           (λ y → Π-is-subsingleton fe
           (λ f → i x y (compX x x y (idX x) f) f)))

     rs = Π-is-subsingleton fe
           (λ x → Π-is-subsingleton fe
           (λ y → Π-is-subsingleton fe
           (λ f → i x y (compX x y y f (idX y)) f)))

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

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

 Id→EqCat : (𝓧 𝓐 : Cat) → 𝓧 ＝ 𝓐 → 𝓧 ⋍ 𝓐
 Id→EqCat 𝓧 𝓧 (refl 𝓧) = 𝑖𝑑 (Ob 𝓧 ) ,
                         id-is-equiv (Ob 𝓧 ) ,
                         (λ x y → 𝑖𝑑 (hom 𝓧 x y)) ,
                         (λ x y → id-is-equiv (hom 𝓧 x y)) ,
                         refl (𝒾𝒹 𝓧) ,
                         refl (comp 𝓧)

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

 Id→EqCat-is-equiv : (𝓧 𝓐 : Cat) → is-equiv (Id→EqCat 𝓧 𝓐)
 Id→EqCat-is-equiv 𝓧 𝓐 = equivs-closed-under-∼
                           (⌜⌝-is-equiv (characterization-of-category-＝ 𝓧 𝓐))
                           (γ 𝓧 𝓐)
  where
   γ : (𝓧 𝓐 : Cat) → Id→EqCat 𝓧 𝓐 ∼ ⌜ characterization-of-category-＝ 𝓧 𝓐 ⌝
   γ 𝓧 𝓧 (refl 𝓧) = refl _

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

 fe : global-dfunext
 fe = univalence-gives-global-dfunext ua

 hfe : global-hfunext
 hfe = univalence-gives-global-hfunext 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-subsingleton : (R : 𝓤 ̇ ) (s : rng-structure R)
                            → is-subsingleton (rng-axioms R s)

 rng-axioms-is-subsingleton 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-subsingleton ((x : R) → x + O ＝ x)
    b O = Π-is-subsingleton fe (λ x → i (x + O) x)

    c : (O : R)
      → ((x : R) → x + O ＝ x)
      → (x : R) → is-subsingleton (Σ x' ꞉ R , x + x' ＝ O)
    c O f x (x' , p') (x'' , p'') = to-subtype-＝ (λ x' → i (x + x') 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-subsingleton (A O)
    d O (f , g) = φ (f , g)
     where
      φ : is-subsingleton (A O)
      φ = ×-is-subsingleton (b O) (Π-is-subsingleton fe (λ x → c O f x))

    IV-is-subsingleton : is-subsingleton IV
    IV-is-subsingleton (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-subsingleton (rng-axioms R (_+_ , _·_))
    γ = ×-is-subsingleton
          (being-set-is-subsingleton fe)
       (×-is-subsingleton
          (Π-is-subsingleton fe
          (λ x → Π-is-subsingleton fe
          (λ y → Π-is-subsingleton fe
          (λ z → i ((x + y) + z) (x + (y + z))))))
       (×-is-subsingleton
          (Π-is-subsingleton fe
          (λ x → Π-is-subsingleton fe
          (λ y → i (x + y) (y + x))))
       (×-is-subsingleton
          IV-is-subsingleton
       (×-is-subsingleton
          (Π-is-subsingleton fe
          (λ x → Π-is-subsingleton fe
          (λ y → Π-is-subsingleton fe
          (λ z → i ((x · y) · z) (x · (y · z))))))
       (×-is-subsingleton
          (Π-is-subsingleton fe
          (λ x → Π-is-subsingleton fe
          (λ y → Π-is-subsingleton fe
          (λ z → i (x · (y + z)) ((x · y) + (x · z))))))

          (Π-is-subsingleton fe
          (λ x → Π-is-subsingleton fe
          (λ y → Π-is-subsingleton fe
          (λ z → i ((y + z) · x) ((y · x) + (z · x)))))))))))

    δ : (α : rng-axioms R (_+_ , _·_)) → (i , ii , iii , iv-vii) ＝ α
    δ = γ (i , ii , iii , iv-vii)

 _≅[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-subsingleton
                                (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-subsingleton : (R : 𝓤 ̇ ) (s : ring-structure R)
                             → is-subsingleton (ring-axioms R s)

 ring-axioms-is-subsingleton R (𝟏 , _+_ , _·_) ((i , ii-vii) , viii) = γ ((i , ii-vii) , viii)
  where
   γ : is-subsingleton (ring-axioms R (𝟏 , _+_ , _·_))
   γ = ×-is-subsingleton
         (rng-axioms-is-subsingleton R (_+_ , _·_))
         (Π-is-subsingleton fe (λ x → ×-is-subsingleton (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-subsingleton
                                  (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-subsingleton : (𝓡 : Rng) → is-subsingleton (is-commutative 𝓡)
 being-commutative-is-subsingleton (R , (_+_ , _·_) , i , ii-vii) =

   Π-is-subsingleton fe
   (λ x → Π-is-subsingleton fe
   (λ y → i (x · y) (y · x)))

 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-subsingleton : (𝓡 : Rng) → is-subsingleton (is-local 𝓡)
 being-local-is-subsingleton 𝓡 = ∃!-is-subsingleton _ fe

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

  open basic-truncation-development pt hfe
  open ℕ-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-subsingleton : (𝓡 : Rng) → is-subsingleton (is-noetherian 𝓡)

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

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

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

  _≅[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 = ⌜ ≃-sym (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-subsingleton : (𝓡 : Ring) → is-subsingleton (is-CNL 𝓡)
  being-CNL-is-subsingleton (R , (𝟏 , _+_ , _·_) , i-vii , viii) =

     ×-is-subsingleton (being-commutative-is-subsingleton 𝓡)
    (×-is-subsingleton (being-noetherian-is-subsingleton 𝓡)
                       (being-local-is-subsingleton 𝓡))
   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₁-embedding being-CNL-is-subsingleton

  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 = ⌜ ≃-sym (characterization-of-CNL-ring-＝ 𝓡 𝓡') ⌝ i

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