Agda UALib ↑

MartΓ­n EscardΓ³ 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes, which are available online from the following links.

html lecture notes

Source code repository


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

module MGS-Powerset where

open import MGS-More-FunExt-Consequences public

propext : βˆ€ 𝓀  β†’ 𝓀 ⁺ Μ‡
propext 𝓀 = {P Q : 𝓀 Μ‡ } β†’ is-prop P β†’ is-prop Q β†’ (P β†’ Q) β†’ (Q β†’ P) β†’ P ≑ Q

global-propext : 𝓀ω
global-propext = βˆ€ {𝓀} β†’ propext 𝓀

univalence-gives-propext : is-univalent 𝓀 β†’ propext 𝓀
univalence-gives-propext ua {P} {Q} i j f g = Eq→Id ua P Q γ
 where
  Ξ³ : P ≃ Q
  Ξ³ = logically-equivalent-subsingletons-are-equivalent P Q i j (f , g)

Id-from-subsingleton : propext 𝓀 β†’ dfunext 𝓀 𝓀
                     β†’ (P : 𝓀 Μ‡ )
                     β†’ is-subsingleton P
                     β†’ (X : 𝓀 Μ‡ ) β†’ is-subsingleton (P ≑ X)

Id-from-subsingleton {𝓀} pe fe P i = Hedberg P (Ξ» X β†’ h X , k X)
 where
  module _ (X : 𝓀 Μ‡ ) where
   f : P ≑ X β†’ is-subsingleton X Γ— (P ⇔ X)
   f p = transport is-subsingleton p i , Idβ†’fun p , (Idβ†’fun (p ⁻¹))

   g : is-subsingleton X Γ— (P ⇔ X) β†’ P ≑ X
   g (l , Ο† , ψ) = pe i l Ο† ψ

   h : P ≑ X β†’ P ≑ X
   h = g ∘ f

   j : is-subsingleton (is-subsingleton X Γ— (P ⇔ X))
   j = Γ—-is-subsingleton'
        ((Ξ» (_ : P ⇔ X) β†’ being-subsingleton-is-subsingleton fe) ,
         (Ξ» (l : is-subsingleton X) β†’ Γ—-is-subsingleton
                                       (Ξ -is-subsingleton fe (Ξ» p β†’ l))
                                       (Ξ -is-subsingleton fe (Ξ» x β†’ i))))

   k : wconstant h
   k p q = ap g (j (f p) (f q))

subsingleton-univalence : propext 𝓀 β†’ dfunext 𝓀 𝓀
                        β†’ (P : 𝓀 Μ‡ )
                        β†’ is-subsingleton P
                        β†’ (X : 𝓀 Μ‡ ) β†’ is-equiv (Idβ†’Eq P X)

subsingleton-univalence pe fe P i X = Ξ³
 where
  l : P ≃ X β†’ is-subsingleton X
  l e = equiv-to-subsingleton (≃-sym e) i

  eqtoid : P ≃ X β†’ P ≑ X
  eqtoid e = pe i (equiv-to-subsingleton (≃-sym e) i)
                  ⌜ e ⌝ ⌜ ≃-sym e ⌝

  m : is-subsingleton (P ≃ X)
  m (f , k) (f' , k') = to-subtype-≑
                          (being-equiv-is-subsingleton fe fe)
                          (fe (Ξ» x β†’ j (f x) (f' x)))
    where
     j : is-subsingleton X
     j = equiv-to-subsingleton (≃-sym (f , k)) i

  Ξ΅ : (e : P ≃ X) β†’ Idβ†’Eq P X (eqtoid e) ≑ e
  Ρ e = m (Id→Eq P X (eqtoid e)) e

  Ξ· : (q : P ≑ X) β†’ eqtoid (Idβ†’Eq P X q) ≑ q
  η q = Id-from-subsingleton pe fe P i X (eqtoid (Id→Eq P X q)) q

  γ : is-equiv (Id→Eq P X)
  γ = invertibles-are-equivs (Id→Eq P X) (eqtoid , η , Ρ)

subsingleton-univalence-≃ : propext 𝓀 β†’ dfunext 𝓀 𝓀
                          β†’ (X P : 𝓀 Μ‡ ) β†’ is-subsingleton P β†’ (P ≑ X) ≃ (P ≃ X)

subsingleton-univalence-≃ pe fe X P i = Idβ†’Eq P X ,
                                        subsingleton-univalence pe fe P i X

Ξ© : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
Ξ© 𝓀 = Ξ£ P κž‰ 𝓀 Μ‡ , is-subsingleton P

_holds : Ξ© 𝓀 β†’ 𝓀 Μ‡
_holds (P , i) = P

holds-is-subsingleton : (p : Ξ© 𝓀) β†’ is-subsingleton (p holds)
holds-is-subsingleton (P , i) = i

Ξ©-ext : dfunext 𝓀 𝓀 β†’ propext 𝓀 β†’ {p q : Ξ© 𝓀}
      β†’ (p holds β†’ q holds) β†’ (q holds β†’ p holds) β†’ p ≑ q

Ξ©-ext {𝓀} fe pe {p} {q} f g = to-subtype-≑
                                 (Ξ» _ β†’ being-subsingleton-is-subsingleton fe)
                                 (pe (holds-is-subsingleton p) (holds-is-subsingleton q) f g)

Ξ©-is-set : dfunext 𝓀 𝓀 β†’ propext 𝓀 β†’ is-set (Ξ© 𝓀)
Ξ©-is-set {𝓀} fe pe = types-with-wconstant-≑-endomaps-are-sets (Ξ© 𝓀) c
 where
  A : (p q : Ξ© 𝓀) β†’ 𝓀 Μ‡
  A p q = (p holds β†’ q holds) Γ— (q holds β†’ p holds)

  i : (p q : Ξ© 𝓀) β†’ is-subsingleton (A p q)
  i p q = Ξ£-is-subsingleton
           (Ξ -is-subsingleton fe
             (Ξ» _ β†’ holds-is-subsingleton q))
             (Ξ» _ β†’ Ξ -is-subsingleton fe (Ξ» _ β†’ holds-is-subsingleton p))

  g : (p q : Ξ© 𝓀) β†’ p ≑ q β†’ A p q
  g p q e = (u , v)
   where
    a : p holds ≑ q holds
    a = ap _holds e

    u : p holds β†’ q holds
    u = Id→fun a

    v : q holds β†’ p holds
    v = Idβ†’fun (a ⁻¹)

  h : (p q : Ξ© 𝓀) β†’ A p q β†’ p ≑ q
  h p q (u , v) = Ξ©-ext fe pe u v

  f : (p q : Ξ© 𝓀) β†’ p ≑ q β†’ p ≑ q
  f p q e = h p q (g p q e)

  k : (p q : Ξ© 𝓀) (d e : p ≑ q) β†’ f p q d ≑ f p q e
  k p q d e = ap (h p q) (i p q (g p q d) (g p q e))

  c : (p q : Ξ© 𝓀) β†’ Ξ£ f κž‰ (p ≑ q β†’ p ≑ q), wconstant f
  c p q = (f p q , k p q)

powersets-are-sets : hfunext 𝓀 (π“₯ ⁺) β†’ dfunext π“₯ π“₯ β†’ propext π“₯
                   β†’ {X : 𝓀 Μ‡ } β†’ is-set (X β†’ Ξ© π“₯)

powersets-are-sets fe fe' pe = Ξ -is-set fe (Ξ» x β†’ Ξ©-is-set fe' pe)

π“Ÿ : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
π“Ÿ {𝓀} X = X β†’ Ξ© 𝓀

powersets-are-sets' : Univalence
                    β†’ {X : 𝓀 Μ‡ } β†’ is-set (π“Ÿ X)

powersets-are-sets' {𝓀} ua = powersets-are-sets
                               (univalence-gives-hfunext' (ua 𝓀) (ua (𝓀 ⁺)))
                               (univalence-gives-dfunext (ua 𝓀))
                               (univalence-gives-propext (ua 𝓀))

_∈_ : {X : 𝓀 Μ‡ } β†’ X β†’ π“Ÿ X β†’ 𝓀 Μ‡
x ∈ A = A x holds

_βŠ†_ : {X : 𝓀 Μ‡ } β†’ π“Ÿ X β†’ π“Ÿ X β†’ 𝓀 Μ‡
A βŠ† B = βˆ€ x β†’ x ∈ A β†’ x ∈ B

∈-is-subsingleton : {X : 𝓀 Μ‡ } (A : π“Ÿ X) (x : X) β†’ is-subsingleton (x ∈ A)
∈-is-subsingleton A x = holds-is-subsingleton (A x)

βŠ†-is-subsingleton : dfunext 𝓀 𝓀
                  β†’ {X : 𝓀 Μ‡ } (A B : π“Ÿ X) β†’ is-subsingleton (A βŠ† B)

βŠ†-is-subsingleton fe A B = Ξ -is-subsingleton fe
                            (Ξ» x β†’ Ξ -is-subsingleton fe
                            (Ξ» _ β†’ ∈-is-subsingleton B x))

βŠ†-refl : {X : 𝓀 Μ‡ } (A : π“Ÿ X) β†’ A βŠ† A
βŠ†-refl A x = 𝑖𝑑 (x ∈ A)

βŠ†-refl-consequence : {X : 𝓀 Μ‡ } (A B : π“Ÿ X)
                   β†’ A ≑ B β†’ (A βŠ† B) Γ— (B βŠ† A)

βŠ†-refl-consequence {X} A A (refl A) = βŠ†-refl A , βŠ†-refl A

subset-extensionality : propext 𝓀 β†’ dfunext 𝓀 𝓀 β†’ dfunext 𝓀 (𝓀 ⁺)
                      β†’ {X : 𝓀 Μ‡ } {A B : π“Ÿ X}
                      β†’ A βŠ† B β†’ B βŠ† A β†’ A ≑ B

subset-extensionality pe fe fe' {X} {A} {B} h k = fe' Ο†
 where
  Ο† : (x : X) β†’ A x ≑ B x
  Ο† x = to-subtype-≑
           (Ξ» _ β†’ being-subsingleton-is-subsingleton fe)
           (pe (holds-is-subsingleton (A x)) (holds-is-subsingleton (B x))
               (h x) (k x))

subset-extensionality' : Univalence
                       β†’ {X : 𝓀 Μ‡ } {A B : π“Ÿ X}
                       β†’ A βŠ† B β†’ B βŠ† A β†’ A ≑ B

subset-extensionality' {𝓀} ua = subset-extensionality
                                 (univalence-gives-propext (ua 𝓀))
                                 (univalence-gives-dfunext (ua 𝓀))
                                 (univalence-gives-dfunext' (ua 𝓀) (ua (𝓀 ⁺)))
infix  40 _∈_