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-Subsingleton-Truncation where

open import MGS-Powerset public
open import MGS-Embeddings public

is-inhabited : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
is-inhabited {𝓀} X = (P : 𝓀 Μ‡ ) β†’ is-subsingleton P β†’ (X β†’ P) β†’ P

inhabitation-is-subsingleton : global-dfunext β†’ (X : 𝓀 Μ‡ )
                             β†’ is-subsingleton (is-inhabited X)

inhabitation-is-subsingleton fe X =
 Ξ -is-subsingleton fe
   (Ξ» P β†’ Ξ -is-subsingleton fe
   (Ξ» (s : is-subsingleton P) β†’ Ξ -is-subsingleton fe
   (Ξ» (f : X β†’ P) β†’ s)))

inhabited-intro : {X : 𝓀 Μ‡ } β†’ X β†’ is-inhabited X
inhabited-intro x = Ξ» P s f β†’ f x

inhabited-recursion : {X P : 𝓀 Μ‡ } β†’ is-subsingleton P β†’ (X β†’ P) β†’ is-inhabited X β†’ P
inhabited-recursion s f Ο† = Ο† (codomain f) s f

inhabited-recursion-computation : {X P : 𝓀 Μ‡ }
                                  (i : is-subsingleton P)
                                  (f : X β†’ P)
                                  (x : X)
                                β†’ inhabited-recursion i f (inhabited-intro x) ≑ f x

inhabited-recursion-computation i f x = refl (f x)

inhabited-induction : global-dfunext
                    β†’ {X : 𝓀 Μ‡ } {P : is-inhabited X β†’ 𝓀 Μ‡ }
                      (i : (s : is-inhabited X) β†’ is-subsingleton (P s))
                      (f : (x : X) β†’ P (inhabited-intro x))
                    β†’ (s : is-inhabited X) β†’ P s

inhabited-induction fe {X} {P} i f s = Ο†' s
 where
  Ο† : X β†’ P s
  Ο† x = transport P (inhabitation-is-subsingleton fe X (inhabited-intro x) s) (f x)

  Ο†' : is-inhabited X β†’ P s
  Ο†' = inhabited-recursion (i s) Ο†

inhabited-computation : (fe : global-dfunext) {X : 𝓀 Μ‡ } {P : is-inhabited X β†’ 𝓀 Μ‡ }
                        (i : (s : is-inhabited X) β†’ is-subsingleton (P s))
                        (f : (x : X) β†’ P (inhabited-intro x))
                        (x : X)
                      β†’ inhabited-induction fe i f (inhabited-intro x) ≑ f x

inhabited-computation fe i f x = i (inhabited-intro x)
                                   (inhabited-induction fe i f (inhabited-intro x))
                                   (f x)

inhabited-subsingletons-are-pointed : (P : 𝓀 Μ‡ )
                                    β†’ is-subsingleton P β†’ is-inhabited P β†’ P

inhabited-subsingletons-are-pointed P s = inhabited-recursion s (𝑖𝑑 P)

inhabited-functorial : global-dfunext β†’ (X : 𝓀 ⁺ Μ‡ ) (Y : 𝓀 Μ‡ )
                     β†’ (X β†’ Y) β†’ is-inhabited X β†’ is-inhabited Y

inhabited-functorial fe X Y f = inhabited-recursion
                                  (inhabitation-is-subsingleton fe Y)
                                  (inhabited-intro ∘ f)

image' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
image' f = Ξ£ y κž‰ codomain f , is-inhabited (Ξ£ x κž‰ domain f , f x ≑ y)

restriction' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
             β†’ image' f β†’ Y

restriction' f (y , _) = y

corestriction' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
               β†’ X β†’ image' f

corestriction' f x = f x , inhabited-intro (x , refl (f x))

is-surjection' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
is-surjection' f = (y : codomain f) β†’ is-inhabited (Ξ£ x κž‰ domain f , f x ≑ y)

record subsingleton-truncations-exist : 𝓀ω where
 field
  βˆ₯_βˆ₯                  : {𝓀 : Universe} β†’ 𝓀 Μ‡ β†’ 𝓀 Μ‡
  βˆ₯βˆ₯-is-subsingleton   : {𝓀 : Universe} {X : 𝓀 Μ‡ } β†’ is-subsingleton βˆ₯ X βˆ₯
  ∣_∣                  : {𝓀 : Universe} {X : 𝓀 Μ‡ } β†’ X β†’ βˆ₯ X βˆ₯
  βˆ₯βˆ₯-recursion         : {𝓀 π“₯ : Universe} {X : 𝓀 Μ‡ } {P : π“₯ Μ‡ }
                       β†’ is-subsingleton P β†’ (X β†’ P) β†’ βˆ₯ X βˆ₯ β†’ P
 infix 0 βˆ₯_βˆ₯

module basic-truncation-development
        (pt  : subsingleton-truncations-exist)
        (hfe : global-hfunext)
       where

  open subsingleton-truncations-exist pt public

  hunapply : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {f g : Ξ  A} β†’ f ∼ g β†’ f ≑ g
  hunapply = hfunext-gives-dfunext hfe

  βˆ₯βˆ₯-recursion-computation : {X : 𝓀 Μ‡ } {P :  π“₯ Μ‡ }
                           β†’ (i : is-subsingleton P)
                           β†’ (f : X β†’ P)
                           β†’ (x : X)
                           β†’ βˆ₯βˆ₯-recursion i f ∣ x ∣ ≑ f x

  βˆ₯βˆ₯-recursion-computation i f x = i (βˆ₯βˆ₯-recursion i f ∣ x ∣) (f x)

  βˆ₯βˆ₯-induction : {X : 𝓀 Μ‡ } {P : βˆ₯ X βˆ₯ β†’ π“₯ Μ‡ }
              β†’ ((s : βˆ₯ X βˆ₯) β†’ is-subsingleton (P s))
              β†’ ((x : X) β†’ P ∣ x ∣)
              β†’ (s : βˆ₯ X βˆ₯) β†’ P s

  βˆ₯βˆ₯-induction {𝓀} {π“₯} {X} {P} i f s = Ο†' s
   where
    Ο† : X β†’ P s
    Ο† x = transport P (βˆ₯βˆ₯-is-subsingleton ∣ x ∣ s) (f x)
    Ο†' : βˆ₯ X βˆ₯ β†’ P s
    Ο†' = βˆ₯βˆ₯-recursion (i s) Ο†

  βˆ₯βˆ₯-computation : {X : 𝓀 Μ‡ } {P : βˆ₯ X βˆ₯ β†’ π“₯ Μ‡ }
                 β†’ (i : (s : βˆ₯ X βˆ₯) β†’ is-subsingleton (P s))
                 β†’ (f : (x : X) β†’ P ∣ x ∣)
                 β†’ (x : X)
                 β†’ βˆ₯βˆ₯-induction i f ∣ x ∣ ≑ f x

  βˆ₯βˆ₯-computation i f x = i ∣ x ∣ (βˆ₯βˆ₯-induction i f ∣ x ∣) (f x)

  βˆ₯βˆ₯-functor : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ βˆ₯ X βˆ₯ β†’ βˆ₯ Y βˆ₯
  βˆ₯βˆ₯-functor f = βˆ₯βˆ₯-recursion βˆ₯βˆ₯-is-subsingleton (Ξ» x β†’ ∣ f x ∣)

  βˆ₯βˆ₯-agrees-with-inhabitation : (X : 𝓀 Μ‡ ) β†’ βˆ₯ X βˆ₯ ⇔ is-inhabited X
  βˆ₯βˆ₯-agrees-with-inhabitation X = a , b
   where
    a : βˆ₯ X βˆ₯ β†’ is-inhabited X
    a = βˆ₯βˆ₯-recursion (inhabitation-is-subsingleton hunapply X) inhabited-intro

    b : is-inhabited X β†’ βˆ₯ X βˆ₯
    b = inhabited-recursion βˆ₯βˆ₯-is-subsingleton ∣_∣

  _∨_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
  A ∨ B = βˆ₯ A + B βˆ₯

  infixl 20 _∨_

  βˆƒ : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
  βˆƒ A = (βˆ₯ Ξ£ A βˆ₯)

  -βˆƒ : {𝓀 π“₯ : Universe} (X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
  -βˆƒ X Y = βˆƒ Y

  syntax -βˆƒ A (Ξ» x β†’ b) = βˆƒ x κž‰ A , b

  infixr -1 -βˆƒ

  ∨-is-subsingleton : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ } β†’ is-subsingleton (A ∨ B)
  ∨-is-subsingleton = βˆ₯βˆ₯-is-subsingleton

  βˆƒ-is-subsingleton : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } β†’ is-subsingleton (βˆƒ A)
  βˆƒ-is-subsingleton = βˆ₯βˆ₯-is-subsingleton

  image : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
  image f = Ξ£ y κž‰ codomain f , βˆƒ x κž‰ domain f , f x ≑ y

  -- inv : {X : 𝓀 Μ‡ }{Y : π“₯ Μ‡ }(f : X β†’ Y) β†’ image f  β†’  {!!}
  -- inv f imgf = prβ‚‚ imgf

  restriction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
              β†’ image f β†’ Y

  restriction f (y , _) = y

  corestriction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                β†’ X β†’ image f

  corestriction f x = f x , ∣ (x , refl (f x)) ∣

  is-surjection : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
  is-surjection f = (y : codomain f) β†’ βˆƒ x κž‰ domain f , f x ≑ y

  being-surjection-is-subsingleton : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                   β†’ is-subsingleton (is-surjection f)

  being-surjection-is-subsingleton f = Ξ -is-subsingleton hunapply
                                        (Ξ» y β†’ βˆƒ-is-subsingleton)

  corestriction-surjection : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                           β†’ is-surjection (corestriction f)

  corestriction-surjection f (y , s) = βˆ₯βˆ₯-functor g s
   where
    g : (Ξ£ x κž‰ domain f , f x ≑ y) β†’ Ξ£ x κž‰ domain f , corestriction f x ≑ (y , s)
    g (x , p) = x , to-subtype-≑ (Ξ» _ β†’ βˆƒ-is-subsingleton) p

  surjection-induction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                       β†’ is-surjection f
                       β†’ (P : Y β†’ 𝓦 Μ‡ )
                       β†’ ((y : Y) β†’ is-subsingleton (P y))
                       β†’ ((x : X) β†’ P (f x))
                       β†’ (y : Y) β†’ P y

  surjection-induction f i P j Ξ± y = βˆ₯βˆ₯-recursion (j y) Ο† (i y)
   where
    Ο† : fiber f y β†’ P y
    Ο† (x , r) = transport P r (Ξ± x)

  ∣∣-is-surjection : (X : 𝓀 Μ‡ ) β†’ is-surjection (Ξ» (x : X) β†’ ∣ x ∣)
  ∣∣-is-surjection X s = γ
   where
    f : X β†’ βˆƒ x κž‰ X , ∣ x ∣ ≑ s
    f x = ∣ (x , βˆ₯βˆ₯-is-subsingleton ∣ x ∣ s) ∣

    Ξ³ : βˆƒ x κž‰ X , ∣ x ∣ ≑ s
    Ξ³ = βˆ₯βˆ₯-recursion βˆ₯βˆ₯-is-subsingleton f s

  singletons-are-inhabited : (X : 𝓀 Μ‡ )
                           β†’ is-singleton X
                           β†’ βˆ₯ X βˆ₯

  singletons-are-inhabited X s = ∣ center X s ∣

  inhabited-subsingletons-are-singletons : (X : 𝓀 Μ‡ )
                                         β†’ βˆ₯ X βˆ₯
                                         β†’ is-subsingleton X
                                         β†’ is-singleton X

  inhabited-subsingletons-are-singletons X t i = c , Ο†
   where
    c : X
    c = βˆ₯βˆ₯-recursion i (𝑖𝑑 X) t

    Ο† : (x : X) β†’ c ≑ x
    Ο† = i c

  singleton-iff-inhabited-subsingleton : (X : 𝓀 Μ‡ )
                                       β†’ is-singleton X
                                       ⇔ (βˆ₯ X βˆ₯ Γ— is-subsingleton X)

  singleton-iff-inhabited-subsingleton X =

    (Ξ» (s : is-singleton X) β†’ singletons-are-inhabited     X s ,
                              singletons-are-subsingletons X s) ,
    Ξ£-induction (inhabited-subsingletons-are-singletons X)

  equiv-iff-embedding-and-surjection : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                     β†’  is-equiv f
                                     ⇔ (is-embedding f Γ— is-surjection f)

  equiv-iff-embedding-and-surjection f = (a , b)
   where
    a : is-equiv f β†’ is-embedding f Γ— is-surjection f
    a e = (Ξ» y β†’ singletons-are-subsingletons (fiber f y) (e y)) ,
          (Ξ» y β†’ singletons-are-inhabited     (fiber f y) (e y))

    b : is-embedding f Γ— is-surjection f β†’ is-equiv f
    b (e , s) y = inhabited-subsingletons-are-singletons (fiber f y) (s y) (e y)

  equiv-≑-embedding-and-surjection : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                                   β†’ propext (𝓀 βŠ” π“₯)
                                   β†’  is-equiv f
                                   ≑ (is-embedding f Γ— is-surjection f)

  equiv-≑-embedding-and-surjection f pe =
    pe (being-equiv-is-subsingleton hunapply hunapply f)
       (Γ—-is-subsingleton
         (being-embedding-is-subsingleton hunapply f)
         (being-surjection-is-subsingleton f))
       (lr-implication (equiv-iff-embedding-and-surjection f))
       (rl-implication (equiv-iff-embedding-and-surjection f))

fix : {X : 𝓀 Μ‡ } β†’ (X β†’ X) β†’ 𝓀 Μ‡
fix f = Ξ£ x κž‰ domain f , f x ≑ x

from-fix : {X : 𝓀 Μ‡ } (f : X β†’ X)
         β†’ fix f β†’ X

from-fix f = pr₁

to-fix : {X : 𝓀 Μ‡ } (f : X β†’ X) β†’ wconstant f
       β†’ X β†’ fix f

to-fix f ΞΊ x = f x , ΞΊ (f x) x

fix-is-subsingleton : {X : 𝓀 Μ‡ } (f : X β†’ X)
                    β†’ wconstant f β†’ is-subsingleton (fix f)

fix-is-subsingleton {𝓀} {X} f ΞΊ = Ξ³
 where
  a : (y x : X) β†’ (f x ≑ x) ≃ (f y ≑ x)
  a y x = transport (_≑ x) (ΞΊ x y) , transport-is-equiv (_≑ x) (ΞΊ x y)

  b : (y : X) β†’ fix f ≃ singleton-type' (f y)
  b y = Ξ£-cong (a y)

  c : X β†’ is-singleton (fix f)
  c y = equiv-to-singleton (b y) (singleton-types'-are-singletons X (f y))

  d : fix f β†’ is-singleton (fix f)
  d = c ∘ from-fix f

  Ξ³ : is-subsingleton (fix f)
  Ξ³ = subsingleton-criterion d

choice-function : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
choice-function X = is-inhabited X β†’ X

wconstant-endomap-gives-choice-function : {X : 𝓀 Μ‡ }
                                        β†’ wconstant-endomap X β†’ choice-function X

wconstant-endomap-gives-choice-function {𝓀} {X} (f , ΞΊ) = from-fix f ∘ Ξ³
 where
  Ξ³ : is-inhabited X β†’ fix f
  Ξ³ = inhabited-recursion (fix-is-subsingleton f ΞΊ) (to-fix f ΞΊ)

choice-function-gives-wconstant-endomap : global-dfunext
                                        β†’ {X : 𝓀 Μ‡ }
                                        β†’ choice-function X β†’ wconstant-endomap X

choice-function-gives-wconstant-endomap fe {X} c = f , ΞΊ
 where
  f : X β†’ X
  f = c ∘ inhabited-intro

  ΞΊ : wconstant f
  ΞΊ x y = ap c (inhabitation-is-subsingleton fe X (inhabited-intro x)
                                                  (inhabited-intro y))

module find-hidden-root where

 open basic-arithmetic-and-order public

 μρ : (f : β„• β†’ β„•) β†’ root f β†’ root f
 μρ f r = minimal-root-is-root f (root-gives-minimal-root f r)

 μρ-root : (f : β„• β†’ β„•) β†’ root f β†’ β„•
 μρ-root f r = pr₁ (μρ f r)

 μρ-root-is-root : (f : β„• β†’ β„•) (r : root f) β†’ f (μρ-root f r) ≑ 0
 μρ-root-is-root f r = prβ‚‚ (μρ f r)

 μρ-root-minimal : (f : β„• β†’ β„•) (m : β„•) (p : f m ≑ 0)
                 β†’ (n : β„•) β†’ f n ≑ 0 β†’ μρ-root f (m , p) ≀ n

 μρ-root-minimal f m p n q = not-<-gives-β‰₯ (μρ-root f (m , p)) n Ξ³
  where
   Ο† : Β¬(f n β‰’ 0) β†’ Β¬(n < μρ-root f (m , p))
   Ο† = contrapositive (prβ‚‚(prβ‚‚ (root-gives-minimal-root f (m , p))) n)

   γ : ¬ (n < μρ-root f (m , p))
   Ξ³ = Ο† (dni (f n ≑ 0) q)

 μρ-wconstant : (f : β„• β†’ β„•) β†’ wconstant (μρ f)
 μρ-wconstant f (n , p) (n' , p') = r
  where
   m m' : β„•
   m  = μρ-root f (n , p)
   m' = μρ-root f (n' , p')

   l : m ≀ m'
   l = μρ-root-minimal f n p m' (μρ-root-is-root f (n' , p'))

   l' : m' ≀ m
   l' = μρ-root-minimal f n' p' m (μρ-root-is-root f (n , p))

   q : m ≑ m'
   q = ≀-anti _ _ l l'

   r : μρ f (n , p) ≑ μρ f (n' , p')
   r = to-subtype-≑ (Ξ» _ β†’ β„•-is-set (f _) 0) q

 find-existing-root : (f : β„• β†’ β„•) β†’ is-inhabited (root f) β†’ root f
 find-existing-root f = h ∘ g
   where
    Ξ³ : root f β†’ fix (μρ f)
    γ = to-fix (μρ f) (μρ-wconstant f)

    g : is-inhabited (root f) β†’ fix (μρ f)
    g = inhabited-recursion (fix-is-subsingleton (μρ f) (μρ-wconstant f)) γ

    h : fix (μρ f) β†’ root f
    h = from-fix (μρ f)

 module find-existing-root-example where

  f : β„• β†’ β„•
  f 0 = 1
  f 1 = 1
  f 2 = 0
  f 3 = 1
  f 4 = 0
  f 5 = 1
  f 6 = 1
  f 7 = 0
  f (succ (succ (succ (succ (succ (succ (succ (succ x)))))))) = x

  root-existence : is-inhabited (root f)
  root-existence = inhabited-intro (8 , refl 0)

  r : root f
  r = find-existing-root f root-existence

  x : β„•
  x = pr₁ r

  x-is-root : f x ≑ 0
  x-is-root = prβ‚‚ r

  p : x ≑ 2
  p = refl _

module exit-βˆ₯βˆ₯
        (pt  : subsingleton-truncations-exist)
        (hfe : global-hfunext)
       where

 open basic-truncation-development pt hfe
 open find-hidden-root

 find-βˆ₯βˆ₯-existing-root : (f : β„• β†’ β„•)
                       β†’ (βˆƒ n κž‰ β„• , f n ≑ 0)
                       β†’  Ξ£ n κž‰ β„• , f n ≑ 0

 find-βˆ₯βˆ₯-existing-root f = k
  where
   Ξ³ : root f β†’ fix (μρ f)
   γ = to-fix (μρ f) (μρ-wconstant f)

   g : βˆ₯ root f βˆ₯ β†’ fix (μρ f)
   g = βˆ₯βˆ₯-recursion (fix-is-subsingleton (μρ f) (μρ-wconstant f)) Ξ³

   h : fix (μρ f) β†’ root f
   h = from-fix (μρ f)

   k : βˆ₯ root f βˆ₯ β†’ root f
   k = h ∘ g

 module find-βˆ₯βˆ₯-existing-root-example where

  f : β„• β†’ β„•
  f 0 = 1
  f 1 = 1
  f 2 = 0
  f 3 = 1
  f 4 = 0
  f 5 = 1
  f 6 = 1
  f 7 = 0
  f (succ (succ (succ (succ (succ (succ (succ (succ x)))))))) = x

  root-βˆ₯βˆ₯-existence : βˆ₯ root f βˆ₯
  root-βˆ₯βˆ₯-existence = ∣ 8 , refl 0 ∣

  r : root f
  r = find-βˆ₯βˆ₯-existing-root f root-βˆ₯βˆ₯-existence

  x : β„•
  x = pr₁ r

  x-is-root : f x ≑ 0
  x-is-root = prβ‚‚ r

  NB : find-βˆ₯βˆ₯-existing-root f
     ≑ from-fix (μρ f) ∘ βˆ₯βˆ₯-recursion
                          (fix-is-subsingleton (μρ f) (μρ-wconstant f))
                          (to-fix (μρ f) (μρ-wconstant f))
  NB = refl _

  p : x ≑ 2
  p = ap (pr₁ ∘ from-fix (μρ f))
         (βˆ₯βˆ₯-recursion-computation
            (fix-is-subsingleton (μρ f) (μρ-wconstant f))
            (to-fix (μρ f) (μρ-wconstant f))
            (8 , refl _))

 wconstant-endomap-gives-βˆ₯βˆ₯-choice-function : {X : 𝓀 Μ‡ }
                                            β†’ wconstant-endomap X
                                            β†’ (βˆ₯ X βˆ₯ β†’ X)

 wconstant-endomap-gives-βˆ₯βˆ₯-choice-function {𝓀} {X} (f , ΞΊ) = from-fix f ∘ Ξ³
  where
   Ξ³ : βˆ₯ X βˆ₯ β†’ fix f
   Ξ³ = βˆ₯βˆ₯-recursion (fix-is-subsingleton f ΞΊ) (to-fix f ΞΊ)

 βˆ₯βˆ₯-choice-function-gives-wconstant-endomap : {X : 𝓀 Μ‡ }
                                            β†’ (βˆ₯ X βˆ₯ β†’ X)
                                            β†’ wconstant-endomap X

 βˆ₯βˆ₯-choice-function-gives-wconstant-endomap {𝓀} {X} c = f , ΞΊ
  where
   f : X β†’ X
   f = c ∘ ∣_∣

   ΞΊ : wconstant f
   ΞΊ x y = ap c (βˆ₯βˆ₯-is-subsingleton ∣ x ∣ ∣ y ∣)

 βˆ₯βˆ₯-recursion-set : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ )
                  β†’ is-set Y
                  β†’ (f : X β†’ Y)
                  β†’ wconstant f
                  β†’ βˆ₯ X βˆ₯ β†’ Y

 βˆ₯βˆ₯-recursion-set {𝓀} {π“₯} X Y s f ΞΊ = f'
  where
   ψ : (y y' : Y) β†’  (Ξ£ x κž‰ X , f x ≑ y) β†’ (Ξ£ x' κž‰ X , f x' ≑ y') β†’ y ≑ y'
   ψ y y' (x , r) (x' , r') = y    β‰‘βŸ¨ r ⁻¹   ⟩
                              f x  β‰‘βŸ¨ ΞΊ x x' ⟩
                              f x' β‰‘βŸ¨ r'     ⟩
                              y'   ∎

   Ο† : (y y' : Y) β†’ (βˆƒ x κž‰ X , f x ≑ y) β†’ (βˆƒ x' κž‰ X , f x' ≑ y') β†’ y ≑ y'
   Ο† y y' u u' = βˆ₯βˆ₯-recursion (s y y') (Ξ» - β†’ βˆ₯βˆ₯-recursion (s y y') (ψ y y' -) u') u

   P : 𝓀 βŠ” π“₯ Μ‡
   P = image f

   i : is-subsingleton P
   i (y , u) (y' , u') = to-subtype-≑ (Ξ» _ β†’ βˆƒ-is-subsingleton) (Ο† y y' u u')

   g : βˆ₯ X βˆ₯ β†’ P
   g = βˆ₯βˆ₯-recursion i (corestriction f)

   h : P β†’ Y
   h = restriction f

   f' : βˆ₯ X βˆ₯ β†’ Y
   f' = h ∘ g