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

\begin{code}

{-# 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β‚€) Ο„


 variable
  π“₯β‚€ π“₯₁ 𝓦₀ 𝓦₁ : Universe

 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 42 _Β·_

  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

\end{code}