Martin Escardo 1st May 2020.

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.Partial-Functions where

open import MGS.More-FunExt-Consequences public

Ξ β‚š : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” (π“₯ ⁺) Μ‡
Ξ β‚š {𝓀} {π“₯} {X} A = Ξ£ R κž‰ ((x : X) β†’ A x β†’ π“₯ Μ‡ )
                       , ((x : X) β†’ is-subsingleton (Ξ£ a κž‰ A x , R x a))

_⇀_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” (π“₯ ⁺) Μ‡
X ⇀ Y = Ξ β‚š (Ξ» (_ : X) β†’ Y)

is-defined : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } β†’ Ξ β‚š A β†’ X β†’ π“₯ Μ‡
is-defined (R , Οƒ) x = Ξ£ a κž‰ _ , R x a

being-defined-is-subsingleton : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f : Ξ β‚š A) (x : X)
                              β†’ is-subsingleton (is-defined f x)

being-defined-is-subsingleton (R , Οƒ) x = Οƒ x

_[_,_] :  {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f : Ξ β‚š A) (x : X) β†’ is-defined f x β†’ A x
(R , s) [ x , (a , r)] = a

_＝ₖ_ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } β†’ Ξ β‚š A β†’ Ξ β‚š A β†’ 𝓀 βŠ” π“₯ Μ‡
f ＝ₖ g = βˆ€ x β†’ (is-defined f x ↔ is-defined g x)
             Γ— ((i : is-defined f x) (j : is-defined g x) β†’ f [ x , i ] ＝ g [ x , j ])

module ΞΌ-operator (fe : dfunext 𝓀₀ 𝓀₀) where

 open basic-arithmetic-and-order

 being-minimal-root-is-subsingleton : (f : β„• β†’ β„•) (m : β„•)
                                    β†’ is-subsingleton (is-minimal-root f m)

 being-minimal-root-is-subsingleton f m = Γ—-is-subsingleton
                                           (β„•-is-set (f m) 0)
                                           (Ξ -is-subsingleton fe
                                              (Ξ» _ β†’ Ξ -is-subsingleton fe
                                              (Ξ» _ β†’ Ξ -is-subsingleton fe
                                              (Ξ» _ β†’ 𝟘-is-subsingleton))))

 minimal-root-is-subsingleton : (f : β„• β†’ β„•)
                              β†’ is-subsingleton (minimal-root f)

 minimal-root-is-subsingleton f (m , p , Ο†) (m' , p' , Ο†') =
   to-subtype-＝
    (being-minimal-root-is-subsingleton f)
    (at-most-one-minimal-root f m m' (p , Ο†) (p' , Ο†'))

 ΞΌ : (β„• β†’ β„•) ⇀ β„•
 ΞΌ = is-minimal-root , minimal-root-is-subsingleton

 ΞΌ-propertyβ‚€ : (f : β„• β†’ β„•) β†’ (Ξ£ n κž‰ β„• , f n ＝ 0) β†’ is-defined ΞΌ f
 ΞΌ-propertyβ‚€ = root-gives-minimal-root

 ΞΌ-property₁ : (f : β„• β†’ β„•) (i : is-defined ΞΌ f)
             β†’ (f (ΞΌ [ f , i ]) ＝ 0)
             Γ— ((n : β„•) β†’ n < ΞΌ [ f , i ] β†’ f n β‰  0)

 ΞΌ-property₁ f = prβ‚‚

is-total : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } β†’ Ξ β‚š A β†’ 𝓀 βŠ” π“₯ Μ‡
is-total f = βˆ€ x β†’ is-defined f x

infix  30 _[_,_]

\end{code}