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

open import MGS.Powerset                public
open import MGS.Universe-Lifting        public
open import MGS.Subsingleton-Truncation public

_has-size_ : 𝓀 Μ‡ β†’ (π“₯ : Universe) β†’ π“₯ ⁺ βŠ” 𝓀 Μ‡
X has-size π“₯ = Ξ£ Y κž‰ π“₯ Μ‡ , X ≃ Y

propositional-resizing : (𝓀 π“₯ : Universe) β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
propositional-resizing 𝓀 π“₯ = (P : 𝓀 Μ‡ ) β†’ is-subsingleton P β†’ P has-size π“₯

resize-up : (X : 𝓀 Μ‡ ) β†’ X has-size (𝓀 βŠ” π“₯)
resize-up {𝓀} {π“₯} X = (Lift π“₯ X , ≃-Lift X)

resize-up-subsingleton : propositional-resizing 𝓀 (𝓀 βŠ” π“₯)
resize-up-subsingleton {𝓀} {π“₯} P i = resize-up {𝓀} {π“₯} P

resize : propositional-resizing 𝓀 π“₯
       β†’ (P : 𝓀 Μ‡ ) (i : is-subsingleton P) β†’ π“₯ Μ‡

resize ρ P i = pr₁ (ρ P i)

resize-is-subsingleton : (ρ : propositional-resizing 𝓀 π“₯)
                         (P : 𝓀 Μ‡ ) (i : is-subsingleton P)
                       β†’ is-subsingleton (resize ρ P i)

resize-is-subsingleton ρ P i = equiv-to-subsingleton (≃-sym (prβ‚‚ (ρ P i))) i

to-resize : (ρ : propositional-resizing 𝓀 π“₯)
            (P : 𝓀 Μ‡ ) (i : is-subsingleton P)
          β†’ P β†’ resize ρ P i

to-resize ρ P i = ⌜ prβ‚‚ (ρ P i) ⌝

from-resize : (ρ : propositional-resizing 𝓀 π“₯)
              (P : 𝓀 Μ‡ ) (i : is-subsingleton P)
            β†’ resize ρ P i β†’ P

from-resize ρ P i = ⌜ ≃-sym (prβ‚‚ (ρ P i)) ⌝

Propositional-resizing : 𝓀ω
Propositional-resizing = {𝓀 π“₯ : Universe} β†’ propositional-resizing 𝓀 π“₯

EM-gives-PR : EM 𝓀 β†’ propositional-resizing 𝓀 π“₯
EM-gives-PR {𝓀} {π“₯} em P i = Q (em P i) , e
 where
   Q : P + Β¬ P β†’ π“₯ Μ‡
   Q (inl p) = Lift π“₯ πŸ™
   Q (inr n) = Lift π“₯ 𝟘

   j : (d : P + Β¬ P) β†’ is-subsingleton (Q d)
   j (inl p) = equiv-to-subsingleton (Lift-≃ πŸ™) πŸ™-is-subsingleton
   j (inr n) = equiv-to-subsingleton (Lift-≃ 𝟘) 𝟘-is-subsingleton

   f : (d : P + Β¬ P) β†’ P β†’ Q d
   f (inl p) p' = lift ⋆
   f (inr n) p  = !𝟘 (Lift π“₯ 𝟘) (n p)

   g : (d : P + Β¬ P) β†’ Q d β†’ P
   g (inl p) q = p
   g (inr n) q = !𝟘 P (lower q)

   e : P ≃ Q (em P i)
   e = logically-equivalent-subsingletons-are-equivalent
        P (Q (em P i)) i (j (em P i)) (f (em P i) , g (em P i))

has-size-is-subsingleton : Univalence
                         β†’ (X : 𝓀 Μ‡ ) (π“₯ :  Universe)
                         β†’ is-subsingleton (X has-size π“₯)

has-size-is-subsingleton {𝓀} ua X π“₯ = univalenceβ†’' (ua π“₯) (ua (𝓀 βŠ” π“₯)) X

PR-is-subsingleton : Univalence β†’ is-subsingleton (propositional-resizing 𝓀 π“₯)
PR-is-subsingleton {𝓀} {π“₯} ua =
 Ξ -is-subsingleton (univalence-gives-global-dfunext ua)
  (Ξ» P β†’ Ξ -is-subsingleton (univalence-gives-global-dfunext ua)
  (Ξ» i β†’ has-size-is-subsingleton ua P π“₯))

Impredicativity : (𝓀 π“₯ : Universe) β†’ (𝓀 βŠ” π“₯ )⁺ Μ‡
Impredicativity 𝓀 π“₯ = (Ξ© 𝓀) has-size π“₯

is-impredicative : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
is-impredicative 𝓀 = Impredicativity 𝓀 𝓀

PR-gives-Impredicativity⁺ : global-propext
                          β†’ global-dfunext
                          β†’ propositional-resizing π“₯ 𝓀
                          β†’ propositional-resizing 𝓀 π“₯
                          β†’ Impredicativity 𝓀 (π“₯ ⁺)

PR-gives-Impredicativity⁺ {π“₯} {𝓀} pe fe ρ Οƒ = Ξ³
 where
  Ο† : Ξ© π“₯ β†’ Ξ© 𝓀
  Ο† (Q , j) = resize ρ Q j , resize-is-subsingleton ρ Q j

  ψ : Ξ© 𝓀 β†’ Ξ© π“₯
  ψ (P , i) = resize Οƒ P i , resize-is-subsingleton Οƒ P i

  Ξ· : (p : Ξ© 𝓀) β†’ Ο† (ψ p) ＝ p
  Ξ· (P , i) = Ξ©-ext fe pe a b
   where
    Q : π“₯ Μ‡
    Q = resize Οƒ P i

    j : is-subsingleton Q
    j = resize-is-subsingleton Οƒ P i

    a : resize ρ Q j β†’ P
    a = from-resize Οƒ P i ∘ from-resize ρ Q j

    b : P β†’ resize ρ Q j
    b = to-resize ρ Q j ∘ to-resize Οƒ P i

  Ξ΅ : (q : Ξ© π“₯) β†’ ψ (Ο† q) ＝ q
  Ξ΅ (Q , j) = Ξ©-ext fe pe a b
   where
    P : 𝓀 Μ‡
    P = resize ρ Q j

    i : is-subsingleton P
    i = resize-is-subsingleton ρ Q j

    a : resize Οƒ P i β†’ Q
    a = from-resize ρ Q j ∘ from-resize Οƒ P i

    b : Q β†’ resize Οƒ P i
    b = to-resize Οƒ P i ∘ to-resize ρ Q j

  Ξ³ : (Ξ© 𝓀) has-size (π“₯ ⁺)
  Ξ³ = Ξ© π“₯ , invertibility-gives-≃ ψ (Ο† , Ξ· , Ξ΅)

PR-gives-impredicativity⁺ : global-propext
                          β†’ global-dfunext
                          β†’ propositional-resizing (𝓀 ⁺) 𝓀
                          β†’ is-impredicative (𝓀 ⁺)

PR-gives-impredicativity⁺ pe fe = PR-gives-Impredicativity⁺
                                   pe fe (Ξ» P i β†’ resize-up P)

PR-gives-impredicativity₁ : global-propext
                          β†’ global-dfunext
                          β†’ propositional-resizing 𝓀 𝓀₀
                          β†’ Impredicativity 𝓀 𝓀₁

PR-gives-impredicativity₁ pe fe = PR-gives-Impredicativity⁺
                                   pe fe (Ξ» P i β†’ resize-up P)

Impredicativity-gives-PR : propext 𝓀
                         β†’ dfunext 𝓀 𝓀
                         β†’ Impredicativity 𝓀 π“₯
                         β†’ propositional-resizing 𝓀 π“₯

Impredicativity-gives-PR {𝓀} {π“₯} pe fe (O , e) P i = Q , Ξ΅
 where
  πŸ™'' : 𝓀 Μ‡
  πŸ™'' = Lift 𝓀 πŸ™

  k : is-subsingleton πŸ™''
  k (lift ⋆) (lift ⋆) = refl (lift ⋆)

  down : Ξ© 𝓀 β†’ O
  down = ⌜ e ⌝

  O-is-set : is-set O
  O-is-set = equiv-to-set (≃-sym e) (Ξ©-is-set fe pe)

  Q : π“₯ Μ‡
  Q = down (πŸ™'' , k) ＝ down (P , i)

  j : is-subsingleton Q
  j = O-is-set (down (Lift 𝓀 πŸ™ , k)) (down (P , i))

  Ο† : Q β†’ P
  φ q = Id→fun
         (ap _holds (equivs-are-lc down (⌜⌝-is-equiv e) q))
         (lift ⋆)

  Ξ³ : P β†’ Q
  γ p = ap down (to-subtype-＝
                    (Ξ» _ β†’ being-subsingleton-is-subsingleton fe)
                    (pe k i (Ξ» _ β†’ p) (Ξ» _ β†’ lift ⋆)))

  Ξ΅ : P ≃ Q
  Ξ΅ = logically-equivalent-subsingletons-are-equivalent P Q i j (Ξ³ , Ο†)

PR-gives-existence-of-truncations : global-dfunext
                                  β†’ Propositional-resizing
                                  β†’ subsingleton-truncations-exist

PR-gives-existence-of-truncations fe R =
 record
 {
   βˆ₯_βˆ₯ =

    Ξ» {𝓀} X β†’ resize R
               (is-inhabited X)
               (inhabitation-is-subsingleton fe X) ;

   βˆ₯βˆ₯-is-subsingleton =

    Ξ» {𝓀} {X} β†’ resize-is-subsingleton R
                 (is-inhabited X)
                 (inhabitation-is-subsingleton fe X) ;

   ∣_∣ =

    Ξ» {𝓀} {X} x β†’ to-resize R
                   (is-inhabited X)
                   (inhabitation-is-subsingleton fe X)
                   (inhabited-intro x) ;

   βˆ₯βˆ₯-recursion =

    Ξ» {𝓀} {π“₯} {X} {P} i u s β†’ from-resize R P i
                                (inhabited-recursion
                                  (resize-is-subsingleton R P i)
                                  (to-resize R P i ∘ u)
                                  (from-resize R
                                    (is-inhabited X)
                                    (inhabitation-is-subsingleton fe X) s))
 }

module powerset-union-existence
        (pt  : subsingleton-truncations-exist)
        (hfe : global-hfunext)
       where

 open basic-truncation-development pt hfe

 family-union : {X : 𝓀 βŠ” π“₯ Μ‡ } {I : π“₯ Μ‡ } β†’ (I β†’ π“Ÿ X) β†’ π“Ÿ X
 family-union {𝓀} {π“₯} {X} {I} A = Ξ» x β†’ (βˆƒ i κž‰ I , x ∈ A i) , βˆƒ-is-subsingleton

 π“Ÿπ“Ÿ : 𝓀 Μ‡ β†’ 𝓀 ⁺⁺ Μ‡
 π“Ÿπ“Ÿ X = π“Ÿ (π“Ÿ X)

 existence-of-unions : (𝓀 : Universe) β†’ 𝓀 ⁺⁺ Μ‡
 existence-of-unions 𝓀 =
  (X : 𝓀 Μ‡ ) (𝓐 : π“Ÿπ“Ÿ X) β†’ Ξ£ B κž‰ π“Ÿ X , ((x : X) β†’ (x ∈ B) ↔ (βˆƒ A κž‰ π“Ÿ X , (A ∈ 𝓐) Γ— (x ∈ A)))

 existence-of-unions₁ : (𝓀 :  Universe) β†’ _ Μ‡
 existence-of-unions₁ 𝓀 =
  (X : 𝓀 Μ‡ )
  (𝓐 : (X β†’ Ξ© _) β†’ Ξ© _)
     β†’ Ξ£ B κž‰ (X β†’ Ξ© _) , ((x : X) β†’ (x ∈ B) ↔ (βˆƒ A κž‰ (X β†’ Ξ© _) , (A ∈ 𝓐) Γ— (x ∈ A)))

 existence-of-unionsβ‚‚ : (𝓀 :  Universe) β†’ 𝓀 ⁺⁺ Μ‡
 existence-of-unionsβ‚‚ 𝓀 =
  (X : 𝓀 Μ‡ )
  (𝓐 : (X β†’ Ξ© 𝓀) β†’ Ξ© (𝓀 ⁺))
     β†’ Ξ£ B κž‰ (X β†’ Ξ© 𝓀) , ((x : X) β†’ (x ∈ B) ↔ (βˆƒ A κž‰ (X β†’ Ξ© 𝓀) , (A ∈ 𝓐) Γ— (x ∈ A)))

 existence-of-unions-agreement : existence-of-unions 𝓀 ＝ existence-of-unionsβ‚‚ 𝓀
 existence-of-unions-agreement = refl _

 existence-of-unions-gives-PR : existence-of-unions 𝓀
                              β†’ propositional-resizing (𝓀 ⁺) 𝓀

 existence-of-unions-gives-PR {𝓀} Ξ± = Ξ³
  where
   Ξ³ : (P : 𝓀 ⁺ Μ‡ ) β†’ (i : is-subsingleton P) β†’ P has-size 𝓀
   Ξ³ P i = Q , e
    where
    πŸ™α΅€ : 𝓀 Μ‡
    πŸ™α΅€ = Lift 𝓀 πŸ™

    ⋆ᡀ : πŸ™α΅€
    ⋆ᡀ = lift ⋆

    πŸ™α΅€-is-subsingleton : is-subsingleton πŸ™α΅€
    πŸ™α΅€-is-subsingleton = equiv-to-subsingleton (Lift-≃ πŸ™) πŸ™-is-subsingleton

    𝓐 : π“Ÿπ“Ÿ πŸ™α΅€
    𝓐 = Ξ» (A : π“Ÿ πŸ™α΅€) β†’ P , i

    B : π“Ÿ πŸ™α΅€
    B = pr₁ (Ξ± πŸ™α΅€ 𝓐)

    Ο† : (x : πŸ™α΅€) β†’ (x ∈ B) ↔ (βˆƒ A κž‰ π“Ÿ πŸ™α΅€ , (A ∈ 𝓐) Γ— (x ∈ A))
    Ο† = prβ‚‚ (Ξ± πŸ™α΅€ 𝓐)

    Q : 𝓀 Μ‡
    Q = ⋆ᡀ ∈ B

    j : is-subsingleton Q
    j = ∈-is-subsingleton B ⋆ᡀ

    f : P β†’ Q
    f p = b
     where
      a : Ξ£ A κž‰ π“Ÿ πŸ™α΅€ , (A ∈ 𝓐) Γ— (⋆ᡀ ∈ A)
      a = (Ξ» (x : πŸ™α΅€) β†’ πŸ™α΅€ , πŸ™α΅€-is-subsingleton) , p , ⋆ᡀ

      b : ⋆ᡀ ∈ B
      b = rl-implication (Ο† ⋆ᡀ) ∣ a ∣

    g : Q β†’ P
    g q = βˆ₯βˆ₯-recursion i b a
     where
      a : βˆƒ A κž‰ π“Ÿ πŸ™α΅€ , (A ∈ 𝓐) Γ— (⋆ᡀ ∈ A)
      a = lr-implication (Ο† ⋆ᡀ) q

      b : (Ξ£ A κž‰ π“Ÿ πŸ™α΅€ , (A ∈ 𝓐) Γ— (⋆ᡀ ∈ A)) β†’ P
      b (A , m , _) = m

    e : P ≃ Q
    e = logically-equivalent-subsingletons-are-equivalent P Q i j (f , g)

 PR-gives-existence-of-unions : propositional-resizing (𝓀 ⁺) 𝓀
                              β†’ existence-of-unions 𝓀

 PR-gives-existence-of-unions {𝓀} ρ X 𝓐 = B , (Ξ» x β†’ lr x , rl x)
  where
   Ξ² : X β†’ 𝓀 ⁺ Μ‡
   Ξ² x = βˆƒ A κž‰ π“Ÿ X , (A ∈ 𝓐) Γ— (x ∈ A)

   i : (x : X) β†’ is-subsingleton (Ξ² x)
   i x = βˆƒ-is-subsingleton

   B : π“Ÿ X
   B x = (resize ρ (β x) (i x) , resize-is-subsingleton ρ (β x) (i x))

   lr : (x : X) β†’ x ∈ B β†’ βˆƒ A κž‰ π“Ÿ X , (A ∈ 𝓐) Γ— (x ∈ A)
   lr x = from-resize ρ (β x) (i x)

   rl : (x : X) β†’ (βˆƒ A κž‰ π“Ÿ X , (A ∈ 𝓐) Γ— (x ∈ A)) β†’ x ∈ B
   rl x = to-resize ρ (β x) (i x)

module basic-powerset-development
        (hfe : global-hfunext)
        (ρ   : Propositional-resizing)
       where

  pt : subsingleton-truncations-exist
  pt = PR-gives-existence-of-truncations (hfunext-gives-dfunext hfe) ρ

  open basic-truncation-development pt hfe
  open powerset-union-existence pt hfe

  ⋃ : {X : 𝓀 Μ‡ } β†’ π“Ÿπ“Ÿ X β†’ π“Ÿ X
  ⋃ 𝓐 = pr₁ (PR-gives-existence-of-unions ρ _ 𝓐)

  ⋃-property : {X : 𝓀 Μ‡ } (𝓐 : π“Ÿπ“Ÿ X)
             β†’ (x : X) β†’ (x ∈ ⋃ 𝓐) ↔ (βˆƒ A κž‰ π“Ÿ X , (A ∈ 𝓐) Γ— (x ∈ A))

  ⋃-property 𝓐 = prβ‚‚ (PR-gives-existence-of-unions ρ _ 𝓐)

  intersections-exist :
    (X : 𝓀 Μ‡ )
    (𝓐 : π“Ÿπ“Ÿ X)
       β†’ Ξ£ B κž‰ π“Ÿ X , ((x : X) β†’ (x ∈ B) ↔ ((A : π“Ÿ X) β†’ A ∈ 𝓐 β†’ x ∈ A))

  intersections-exist {𝓀} X 𝓐 = B , (Ξ» x β†’ lr x , rl x)
   where
    Ξ² : X β†’ 𝓀 ⁺ Μ‡
    Ξ² x = (A : π“Ÿ X) β†’ A ∈ 𝓐 β†’ x ∈ A

    i : (x : X) β†’ is-subsingleton (Ξ² x)
    i x = Ξ -is-subsingleton hunapply
           (Ξ» A β†’ Ξ -is-subsingleton hunapply
           (Ξ» _ β†’ ∈-is-subsingleton A x))

    B : π“Ÿ X
    B x = (resize ρ (β x) (i x) , resize-is-subsingleton ρ (β x) (i x))

    lr : (x : X) β†’ x ∈ B β†’ (A : π“Ÿ X) β†’ A ∈ 𝓐 β†’ x ∈ A
    lr x = from-resize ρ (β x) (i x)

    rl : (x : X) β†’ ((A : π“Ÿ X) β†’ A ∈ 𝓐 β†’ x ∈ A) β†’ x ∈ B
    rl x = to-resize ρ (β x) (i x)

  β‹‚ : {X : 𝓀 Μ‡ } β†’ π“Ÿπ“Ÿ X β†’ π“Ÿ X
  β‹‚ {𝓀} {X} 𝓐 = pr₁ (intersections-exist X 𝓐)

  β‹‚-property : {X : 𝓀 Μ‡ } (𝓐 : π“Ÿπ“Ÿ X)
             β†’ (x : X) β†’ (x ∈ β‹‚ 𝓐) ↔ ((A : π“Ÿ X) β†’ A ∈ 𝓐 β†’ x ∈ A)

  β‹‚-property {𝓀} {X} 𝓐 = prβ‚‚ (intersections-exist X 𝓐)

  βˆ… full : {X : 𝓀 Μ‡ } β†’ π“Ÿ X

  βˆ…    = Ξ» x β†’ (Lift _ 𝟘 , equiv-to-subsingleton (Lift-≃ 𝟘) 𝟘-is-subsingleton)

  full = Ξ» x β†’ (Lift _ πŸ™ , equiv-to-subsingleton (Lift-≃ πŸ™) πŸ™-is-subsingleton)

  βˆ…-property : (X : 𝓀 Μ‡ ) β†’ (x : X) β†’ Β¬ (x ∈ βˆ…)
  βˆ…-property X x = lower

  full-property : (X : 𝓀 Μ‡ ) β†’ (x : X) β†’ x ∈ full
  full-property X x = lift ⋆

  _∩_ _βˆͺ_ : {X : 𝓀 Μ‡ } β†’ π“Ÿ X β†’ π“Ÿ X β†’ π“Ÿ X

  (A βˆͺ B) = Ξ» x β†’ ((x ∈ A) ∨ (x ∈ B)) , ∨-is-subsingleton

  (A ∩ B) = Ξ» x β†’ ((x ∈ A) Γ— (x ∈ B)) ,
                  Γ—-is-subsingleton
                    (∈-is-subsingleton A x)
                    (∈-is-subsingleton B x)

  βˆͺ-property : {X : 𝓀 Μ‡ } (A B : π“Ÿ X)
             β†’ (x : X) β†’ x ∈ (A βˆͺ B) ↔ (x ∈ A) ∨ (x ∈ B)

  βˆͺ-property {𝓀} {X} A B x = id , id

  ∩-property : {X : 𝓀 Μ‡ } (A B : π“Ÿ X)
             β†’ (x : X) β†’ x ∈ (A ∩ B) ↔ (x ∈ A) Γ— (x ∈ B)

  ∩-property {𝓀} {X} A B x = id , id

  infix  20 _∩_
  infix  20 _βˆͺ_

  Top : (𝓀 : Universe) β†’ 𝓀 ⁺⁺ Μ‡
  Top 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , is-set X
                     Γ— (Ξ£ π“ž κž‰ π“Ÿπ“Ÿ X , full ∈ π“ž
                                   Γ— ((U V : π“Ÿ X) β†’ U ∈ π“ž β†’ V ∈ π“ž β†’ (U ∩ V) ∈ π“ž)
                                   Γ— ((𝓖 : π“Ÿπ“Ÿ X) β†’ 𝓖 βŠ† π“ž β†’ ⋃ 𝓖 ∈ π“ž))

\end{code}