diff --git a/source/Naturals/RootsTruncation.lagda b/source/Naturals/RootsTruncation.lagda index 2efd89615..e9316b765 100644 --- a/source/Naturals/RootsTruncation.lagda +++ b/source/Naturals/RootsTruncation.lagda @@ -290,16 +290,16 @@ extensionlity. private abstract - minimal-pair' : (A : β„• β†’ 𝓀 Μ‡ ) + minimal-pair⁺ : (A : β„• β†’ 𝓀 Μ‡ ) β†’ ((n : β„•) β†’ A n β†’ (k : β„•) β†’ k < n β†’ is-decidable (A k)) β†’ (n : β„•) β†’ A n β†’ Ξ£ (k , aβ‚–) κž‰ Ξ£ A , ((i : β„•) β†’ A i β†’ k ≀ i) - minimal-pair' A Ξ΄ 0 aβ‚€ = (0 , aβ‚€) , (Ξ» i aα΅’ β†’ zero-least i) - minimal-pair' A Ξ΄ (succ n) aβ‚™β‚Šβ‚ = II + minimal-pair⁺ A Ξ΄ 0 aβ‚€ = (0 , aβ‚€) , (Ξ» i aα΅’ β†’ zero-least i) + minimal-pair⁺ A Ξ΄ (succ n) aβ‚™β‚Šβ‚ = II where IH : Ξ£ (j , aβ±Όβ‚Šβ‚) κž‰ Ξ£ (A ∘ succ) , ((i : β„•) β†’ A (succ i) β†’ j ≀ i) - IH = minimal-pair' (A ∘ succ) (Ξ» n aβ‚™β‚Šβ‚ j β†’ Ξ΄ (succ n) aβ‚™β‚Šβ‚ (succ j)) n aβ‚™β‚Šβ‚ + IH = minimal-pair⁺ (A ∘ succ) (Ξ» n aβ‚™β‚Šβ‚ j β†’ Ξ΄ (succ n) aβ‚™β‚Šβ‚ (succ j)) n aβ‚™β‚Šβ‚ I : type-of IH β†’ Ξ£ (k , aβ‚–) κž‰ Ξ£ A , ((i : β„•) β†’ A i β†’ k ≀ i) @@ -320,7 +320,7 @@ module _ (A : β„• β†’ 𝓀 Μ‡ ) where minimal-pair : Ξ£ A β†’ Ξ£ A - minimal-pair (n , aβ‚™) = pr₁ (minimal-pair' A Ξ΄ n aβ‚™) + minimal-pair (n , aβ‚™) = pr₁ (minimal-pair⁺ A Ξ΄ n aβ‚™) minimal-number : Ξ£ A β†’ β„• minimal-number = pr₁ ∘ minimal-pair @@ -329,7 +329,7 @@ module _ (A : β„• β†’ 𝓀 Μ‡ ) minimal-number-requirement = prβ‚‚ ∘ minimal-pair minimality : (Οƒ : Ξ£ A) β†’ (i : β„•) β†’ A i β†’ minimal-number Οƒ ≀ i - minimality (n , aβ‚™) = prβ‚‚ (minimal-pair' A Ξ΄ n aβ‚™) + minimality (n , aβ‚™) = prβ‚‚ (minimal-pair⁺ A Ξ΄ n aβ‚™) minimal-pair-wconstant : is-prop-valued-family A β†’ wconstant minimal-pair minimal-pair-wconstant A-prop-valued Οƒ Οƒ' = diff --git a/source/TypeTopology/DecidabilityOfNonContinuity.lagda b/source/TypeTopology/DecidabilityOfNonContinuity.lagda index b5143ce51..497376543 100644 --- a/source/TypeTopology/DecidabilityOfNonContinuity.lagda +++ b/source/TypeTopology/DecidabilityOfNonContinuity.lagda @@ -142,8 +142,11 @@ function extensionality, and we choose the latter for convenience. \begin{code} +is-modulus-of-continuity : (β„•βˆž β†’ β„•) β†’ β„• β†’ 𝓀₀ Μ‡ +is-modulus-of-continuity f m = (n : β„•) β†’ f (max (ΞΉ m) (ΞΉ n)) ＝ f ∞ + continuous : (β„•βˆž β†’ β„•) β†’ 𝓀₀ Μ‡ -continuous f = Ξ£ m κž‰ β„• , ((n : β„•) β†’ f (max (ΞΉ m) (ΞΉ n)) ＝ f ∞) +continuous f = Ξ£ m κž‰ β„• , is-modulus-of-continuity f m \end{code} @@ -773,8 +776,11 @@ contrapositive, Β¬ WLPO is stronger than Β¬ LPO: \begin{code} +restriction : (β„•βˆž β†’ β„•) β†’ (β„• β†’ β„•) +restriction f = f ∘ ΞΉ + _extends_ : (β„•βˆž β†’ β„•) β†’ (β„• β†’ β„•) β†’ 𝓀₀ Μ‡ -f extends g = f ∘ ΞΉ ∼ g +f extends g = restriction f ∼ g β„•βˆž-extension : (β„• β†’ β„•) β†’ 𝓀₀ Μ‡ β„•βˆž-extension g = Ξ£ f κž‰ (β„•βˆž β†’ β„•) , f extends g @@ -857,7 +863,7 @@ LPO-gives-β„•βˆž-extension lpo g y E k (inl (n , p)) = ap g (β„•-to-β„•βˆž-lc (p ⁻¹)) E k (inr Ξ½) = 𝟘-elim (Ξ½ (k , refl)) - e : f ∘ ΞΉ ∼ g + e : restriction f ∼ g e k = E k (lpo (ΞΉ k)) P : (d : is-decidable (Ξ£ n κž‰ β„• , ∞ ＝ ΞΉ n)) β†’ F ∞ d ＝ y @@ -926,10 +932,8 @@ open import Naturals.Order renaming max-idemp to maxβ„•-idemp ; max-comm to maxβ„•-comm) -is-modulus-of-eventual-constancy - : (β„• β†’ β„•) β†’ β„• β†’ 𝓀₀ Μ‡ -is-modulus-of-eventual-constancy g m - = ((n : β„•) β†’ g (maxβ„• m n) ＝ g m) +is-modulus-of-eventual-constancy : (β„• β†’ β„•) β†’ β„• β†’ 𝓀₀ Μ‡ +is-modulus-of-eventual-constancy g m = ((n : β„•) β†’ g (maxβ„• m n) ＝ g m) being-modulus-of-eventual-constancy-is-prop : (g : β„• β†’ β„•) @@ -939,38 +943,35 @@ being-modulus-of-eventual-constancy-is-prop g m = Ξ -is-prop fe (Ξ» n β†’ β„•-is-set) eventually-constant : (β„• β†’ β„•) β†’ 𝓀₀ Μ‡ -eventually-constant g - = Ξ£ m κž‰ β„• , is-modulus-of-eventual-constancy g m +eventually-constant g = Ξ£ m κž‰ β„• , is-modulus-of-eventual-constancy g m eventual-constancy-data = eventually-constant eventual-constancy-gives-continuous-extension : (g : β„• β†’ β„•) - β†’ eventually-constant g - β†’ Ξ£ (f , _) κž‰ β„•βˆž-extension g , continuous f -eventual-constancy-gives-continuous-extension g - = uncurry (h g) + ((m , _) : eventually-constant g) + β†’ Ξ£ (f , _) κž‰ β„•βˆž-extension g , is-modulus-of-continuity f m +eventual-constancy-gives-continuous-extension g (m , a) + = h g m a where h : (g : β„• β†’ β„•) (m : β„•) β†’ is-modulus-of-eventual-constancy g m - β†’ Ξ£ (f , _) κž‰ β„•βˆž-extension g , continuous f + β†’ Ξ£ (f , _) κž‰ β„•βˆž-extension g , is-modulus-of-continuity f m h g 0 a = ((Ξ» _ β†’ g 0) , (Ξ» n β†’ g 0 ＝⟨ (a n)⁻¹ ⟩ g (maxβ„• 0 n) ＝⟨ refl ⟩ g n ∎)) , - 0 , (Ξ» n β†’ refl) - h g (succ m) a = I IH where - IH : Ξ£ (f , _) κž‰ β„•βˆž-extension (g ∘ succ) , continuous f + IH : Ξ£ (f , _) κž‰ β„•βˆž-extension (g ∘ succ) , is-modulus-of-continuity f m IH = h (g ∘ succ) m (a ∘ succ) - I : (Ξ£ (f , _) κž‰ β„•βˆž-extension (g ∘ succ) , continuous f) - β†’ Ξ£ (f' , _) κž‰ β„•βˆž-extension g , continuous f' - I ((f , e) , (m , m-is-modulus)) = (f' , e') , - (succ m , succ-m-is-modulus) + I : type-of IH + β†’ Ξ£ (f' , _) κž‰ β„•βˆž-extension g , is-modulus-of-continuity f' (succ m) + I ((f , e) , m-is-modulus) + = (f' , e') , succ-m-is-modulus where f' : β„•βˆž β†’ β„• f' = β„•βˆž-cases fe (g 0) f @@ -992,7 +993,7 @@ eventual-constancy-gives-continuous-extension g f (max (ΞΉ m) (ΞΉ n)) ＝⟨ IV ⟩ f ∞ ＝⟨ V ⟩ f' (Succ ∞) ＝⟨ VI ⟩ - f' ∞ ∎ + f' ∞ ∎ where II = ap f' ((max-Succ fe (ΞΉ m) (ΞΉ n))⁻¹) III = β„•βˆž-cases-Succ fe (g 0) f (max (ΞΉ m) (ΞΉ n)) @@ -1000,13 +1001,67 @@ eventual-constancy-gives-continuous-extension g V = (β„•βˆž-cases-Succ fe (g 0) f ∞)⁻¹ VI = ap f' (Succ-∞-is-∞ fe) -continuous-extension-gives-eventual-constancy +\end{code} + +It will be convenient name various projections of the construction above. + +\begin{code} + +evc-extension : (g : β„• β†’ β„•) - ((f , _) : β„•βˆž-extension g) - β†’ continuous f β†’ eventually-constant g -continuous-extension-gives-eventual-constancy g (f , e) (m , m-is-modulus) - = m , (Ξ» n β†’ g (maxβ„• m n) ＝⟨ (e (maxβ„• m n))⁻¹ ⟩ + β†’ β„•βˆž β†’ β„• +evc-extension g c + = pr₁ (pr₁ (eventual-constancy-gives-continuous-extension g c)) + +evc-extension-property + : (g : β„• β†’ β„•) + (c : eventually-constant g) + β†’ (evc-extension g c) extends g +evc-extension-property g c + = prβ‚‚ (pr₁ (eventual-constancy-gives-continuous-extension g c)) + +evc-extension-modulus-of-continuity + : (g : β„• β†’ β„•) + (c@(m , _) : eventually-constant g) + β†’ is-modulus-of-continuity (evc-extension g c) m +evc-extension-modulus-of-continuity g c@(m , _) + = prβ‚‚ (eventual-constancy-gives-continuous-extension g c) + +evc-extension-continuity + : (g : β„• β†’ β„•) + (c : eventually-constant g) + β†’ continuous (evc-extension g c) +evc-extension-continuity g c@(m , _) + = m , evc-extension-modulus-of-continuity g c + +evc-extension-∞ + : (g : β„• β†’ β„•) + (c@(m , _) : eventually-constant g) + β†’ evc-extension g c ∞ ＝ g m +evc-extension-∞ g c@(m , a) + = f ∞ ＝⟨ (evc-extension-modulus-of-continuity g c m)⁻¹ ⟩ + f (max (ΞΉ m) (ΞΉ m)) ＝⟨ ap f (max-idemp fe (ΞΉ m)) ⟩ + f (ΞΉ m) ＝⟨ evc-extension-property g c m ⟩ + g m ∎ + where + f : β„•βˆž β†’ β„• + f = evc-extension g c + +\end{code} + +The converse of the above. + +\begin{code} + +continuous-extension-gives-eventual-constancy' + : (g : β„• β†’ β„•) + ((f , _) : β„•βˆž-extension g) + (m : β„•) + β†’ is-modulus-of-continuity f m + β†’ is-modulus-of-eventual-constancy g m +continuous-extension-gives-eventual-constancy' g (f , e) m m-is-modulus + = (Ξ» n β†’ g (maxβ„• m n) ＝⟨ (e (maxβ„• m n))⁻¹ ⟩ f (ΞΉ (maxβ„• m n)) ＝⟨ ap f (max-fin fe m n) ⟩ f (max (ΞΉ m) (ΞΉ n)) ＝⟨ m-is-modulus n ⟩ f ∞ ＝⟨ (m-is-modulus m)⁻¹ ⟩ @@ -1014,6 +1069,14 @@ continuous-extension-gives-eventual-constancy g (f , e) (m , m-is-modulus) f (ΞΉ m) ＝⟨ e m ⟩ g m ∎) +continuous-extension-gives-eventual-constancy + : (g : β„• β†’ β„•) + ((f , _) : β„•βˆž-extension g) + β†’ continuous f + β†’ eventually-constant g +continuous-extension-gives-eventual-constancy g ext (m , m-is-modulus) + = m , continuous-extension-gives-eventual-constancy' g ext m m-is-modulus + \end{code} Is there a nice necessary and sufficient condition for the @@ -1234,6 +1297,9 @@ constancy data has split support. \end{code} +A more general result is proved below, which doesn't assume that g has +an extension. + The second necessary condition for the explicit existence of an extension is also necessary for the anonymous existence. @@ -1252,6 +1318,32 @@ extension is also necessary for the anonymous existence. \end{code} +The following is immediate, and we need its reformulation given after +it. + +\begin{code} + + open continuity-criteria pt + + is-continuous-extension-gives-is-eventually-constant + : (g : β„• β†’ β„•) + ((f , _) : β„•βˆž-extension g) + β†’ is-continuous f + β†’ is-eventually-constant g + is-continuous-extension-gives-is-eventually-constant g e + = βˆ₯βˆ₯-functor (continuous-extension-gives-eventual-constancy g e) + + restriction-of-continuous-function-is-eventually-constant + : (f : β„•βˆž β†’ β„•) + β†’ is-continuous f + β†’ is-eventually-constant (restriction f) + restriction-of-continuous-function-is-eventually-constant f + = is-continuous-extension-gives-is-eventually-constant + (restriction f) + (f , (Ξ» x β†’ refl)) + +\end{code} + Added 10th September 2024. We should have added this immediate consequence earlier. If all maps β„• β†’ β„• can be extended to β„•βˆž, then WLPO holds. Just consider the identity function, which can't have any @@ -1335,19 +1427,20 @@ Markov's Principle. We leave this as an open problem. Added 18th September 2024. There is another way of looking at the above development, which gives rise to a further question. -We have the restriction map r : (β„•βˆž β†’ β„•) β†’ (β„• β†’ β„•) defined by r f ＝ f ∘ ΞΉ. +We have the restriction map (β„•βˆž β†’ β„•) β†’ (β„• β†’ β„•) defined above +as restriction f ＝ f ∘ ΞΉ. For any map f : X β†’ Y we have that X ≃ Ξ£ y κž‰ Y , Ξ£ x κž‰ X , f x ＝ y ＝ Ξ£ y κž‰ Y , fiber f y. -With X = (β„•βˆž β†’ β„•) and Y = (β„• β†’ β„•) and f = r, the definition of -_extends_, together with the fact that _∼_ coincides with _＝_ under -function extensionality, the above specializes to +With X = (β„•βˆž β†’ β„•) and Y = (β„• β†’ β„•) and f = restriction, the definition +of _extends_, together with the fact that _∼_ coincides with _＝_ +under function extensionality, the above specializes to (β„•βˆž β†’ β„•) ≃ Ξ£ g κž‰ (β„• β†’ β„•) , Ξ£ f κž‰ (β„•βˆž β†’ β„•) , f ∘ ΞΉ ＝ g - ≃ Ξ£ g κž‰ (β„• β†’ β„•) , Ξ£ f κž‰ (β„•βˆž β†’ β„•) , f ∘ ΞΉ ∼ g + ≃ Ξ£ g κž‰ (β„• β†’ β„•) , Ξ£ f κž‰ (β„•βˆž β†’ β„•) , restriction f ∼ g ≃ Ξ£ g κž‰ (β„• β†’ β„•) , Ξ£ f κž‰ (β„•βˆž β†’ β„•) , f extends g ≃ Ξ£ g κž‰ (β„• β†’ β„•) , β„•-extension g @@ -1387,55 +1480,58 @@ induction. \begin{code} - module _ (g : β„• β†’ β„•) (n : β„•) where - - modulus-down - : is-modulus-of-eventual-constancy g (succ n) - β†’ is-decidable (is-modulus-of-eventual-constancy g n) - modulus-down ΞΌ = III - where - I : g (succ n) ＝ g n β†’ is-modulus-of-eventual-constancy g n - I e m = - Cases (order-split n m) - (Ξ» (l : n < m) - β†’ g (maxβ„• n m) ＝⟨ ap g (max-ordβ†’ n m (≀-trans _ _ _ (≀-succ n) l)) ⟩ - g m ＝⟨ ap g ((max-ordβ†’ (succ n) m l)⁻¹) ⟩ - g (maxβ„• (succ n) m) ＝⟨ ΞΌ m ⟩ - g (succ n) ＝⟨ e ⟩ - g n ∎) - (Ξ» (l : m ≀ n) - β†’ g (maxβ„• n m) ＝⟨ ap g (maxβ„•-comm n m) ⟩ - g (maxβ„• m n) ＝⟨ ap g (max-ordβ†’ m n l) ⟩ - g n ∎) - - II : is-modulus-of-eventual-constancy g n β†’ g (succ n) ＝ g n - II a = g (succ n) ＝⟨ ap g ((max-ordβ†’ n (succ n) (≀-succ n))⁻¹) ⟩ - g (maxβ„• n (succ n)) ＝⟨ a (succ n) ⟩ - g n ∎ - - III : is-decidable (is-modulus-of-eventual-constancy g n) - III = map-decidable I II (β„•-is-discrete (g (succ n)) (g n)) - - modulus-up : is-modulus-of-eventual-constancy g n - β†’ is-modulus-of-eventual-constancy g (succ n) - modulus-up ΞΌ m = - g (maxβ„• (succ n) m) ＝⟨ ap g I ⟩ - g (maxβ„• n (maxβ„• (succ n) m)) ＝⟨ ΞΌ (maxβ„• (succ n) m) ⟩ - g n ＝⟨ (ΞΌ (succ n))⁻¹ ⟩ - g (maxβ„• n (succ n)) ＝⟨ ap g (max-ordβ†’ n (succ n) (≀-succ n)) ⟩ - g (succ n) ∎ - where - I : maxβ„• (succ n) m ＝ maxβ„• n (maxβ„• (succ n) m) - I = (max-ordβ†’ n _ - (≀-trans _ _ _ - (≀-succ n) - (max-ord← _ _ - (maxβ„• (succ n) (maxβ„• (succ n) m) ＝⟨ II ⟩ - maxβ„• (maxβ„• (succ n) (succ n)) m ＝⟨ III ⟩ - maxβ„• (succ n) m ∎))))⁻¹ - where - II = (max-assoc (succ n) (succ n) m)⁻¹ - III = ap (Ξ» - β†’ maxβ„• - m) (maxβ„•-idemp (succ n)) + modulus-down + : (g : β„• β†’ β„•) + (n : β„•) + β†’ is-modulus-of-eventual-constancy g (succ n) + β†’ is-decidable (is-modulus-of-eventual-constancy g n) + modulus-down g n ΞΌ = III + where + I : g (succ n) ＝ g n β†’ is-modulus-of-eventual-constancy g n + I e m = + Cases (order-split n m) + (Ξ» (l : n < m) + β†’ g (maxβ„• n m) ＝⟨ ap g (max-ordβ†’ n m (≀-trans _ _ _ (≀-succ n) l)) ⟩ + g m ＝⟨ ap g ((max-ordβ†’ (succ n) m l)⁻¹) ⟩ + g (maxβ„• (succ n) m) ＝⟨ ΞΌ m ⟩ + g (succ n) ＝⟨ e ⟩ + g n ∎) + (Ξ» (l : m ≀ n) + β†’ g (maxβ„• n m) ＝⟨ ap g (maxβ„•-comm n m) ⟩ + g (maxβ„• m n) ＝⟨ ap g (max-ordβ†’ m n l) ⟩ + g n ∎) + + II : is-modulus-of-eventual-constancy g n β†’ g (succ n) ＝ g n + II a = g (succ n) ＝⟨ ap g ((max-ordβ†’ n (succ n) (≀-succ n))⁻¹) ⟩ + g (maxβ„• n (succ n)) ＝⟨ a (succ n) ⟩ + g n ∎ + + III : is-decidable (is-modulus-of-eventual-constancy g n) + III = map-decidable I II (β„•-is-discrete (g (succ n)) (g n)) + + modulus-up + : (g : β„• β†’ β„•) + (n : β„•) + β†’ is-modulus-of-eventual-constancy g n + β†’ is-modulus-of-eventual-constancy g (succ n) + modulus-up g n ΞΌ m = + g (maxβ„• (succ n) m) ＝⟨ ap g I ⟩ + g (maxβ„• n (maxβ„• (succ n) m)) ＝⟨ ΞΌ (maxβ„• (succ n) m) ⟩ + g n ＝⟨ (ΞΌ (succ n))⁻¹ ⟩ + g (maxβ„• n (succ n)) ＝⟨ ap g (max-ordβ†’ n (succ n) (≀-succ n)) ⟩ + g (succ n) ∎ + where + I : maxβ„• (succ n) m ＝ maxβ„• n (maxβ„• (succ n) m) + I = (max-ordβ†’ n _ + (≀-trans _ _ _ + (≀-succ n) + (max-ord← _ _ + (maxβ„• (succ n) (maxβ„• (succ n) m) ＝⟨ II ⟩ + maxβ„• (maxβ„• (succ n) (succ n)) m ＝⟨ III ⟩ + maxβ„• (succ n) m ∎))))⁻¹ + where + II = (max-assoc (succ n) (succ n) m)⁻¹ + III = ap (Ξ» - β†’ maxβ„• - m) (maxβ„•-idemp (succ n)) conditional-decidability-of-being-modulus-of-constancy : (g : β„• β†’ β„•) @@ -1450,14 +1546,85 @@ induction. (modulus-down g) (modulus-up g) - eventual-constancy-data-has-split-support + eventual-constancy-property-gives-eventual-constancy-data : (g : β„• β†’ β„•) β†’ is-eventually-constant g β†’ eventual-constancy-data g - eventual-constancy-data-has-split-support g + eventual-constancy-property-gives-eventual-constancy-data g = exit-truncation⁺ (is-modulus-of-eventual-constancy g) (being-modulus-of-eventual-constancy-is-prop g) (conditional-decidability-of-being-modulus-of-constancy g) + open import UF.Equiv + open continuity-criteria pt + + private + Ο• : (Ξ£ f κž‰ (β„•βˆž β†’ β„•) , is-continuous f) + β†’ (Ξ£ g κž‰ (β„• β†’ β„•), is-eventually-constant g) + Ο• (f , f-cts) = restriction f , + restriction-of-continuous-function-is-eventually-constant f f-cts + + Ξ³ : (Ξ£ g κž‰ (β„• β†’ β„•), is-eventually-constant g) + β†’ (Ξ£ f κž‰ (β„•βˆž β†’ β„•) , is-continuous f) + Ξ³ (g , g-evc) = + evc-extension g (eventual-constancy-property-gives-eventual-constancy-data g g-evc) , + ∣ evc-extension-continuity g (eventual-constancy-property-gives-eventual-constancy-data g g-evc) ∣ + where + c : eventual-constancy-data g + c = eventual-constancy-property-gives-eventual-constancy-data g g-evc + +{- + Ξ³Ο• : Ξ³ ∘ Ο• ∼ id + Ξ³Ο• (f , f-cts) = to-subtype-＝ + (Ξ» _ β†’ βˆƒ-is-prop) + (dfunext fe III) + where + c : eventual-constancy-data (restriction f) + c = eventual-constancy-property-gives-eventual-constancy-data + (restriction f) + (restriction-of-continuous-function-is-eventually-constant f f-cts) + + I : (n : β„•) β†’ evc-extension (restriction f) c (ΞΉ n) ＝ f (ΞΉ n) + I = evc-extension-property (restriction f) c + + m : β„• + m = pr₁ c + +-- To fill the the remaining need to prove a couple of lemmas that are +-- worth having anyway. Next time. + + gap : is-modulus-of-continuity f m + gap = {!!} + + II + = evc-extension (restriction f) c ∞ ＝⟨ evc-extension-∞ (restriction f) c ⟩ + restriction f m ＝⟨ refl ⟩ + f (ΞΉ m) ＝⟨ ap f ((max-idemp fe (ΞΉ m))⁻¹) ⟩ + f (max (ΞΉ m) (ΞΉ m)) ＝⟨ gap m ⟩ + f ∞ ∎ + + III : (x : β„•βˆž) β†’ evc-extension (restriction f) c x ＝ f x + III = β„•βˆž-density fe β„•-is-¬¬-separated I II + + ϕγ : Ο• ∘ Ξ³ ∼ id + ϕγ (g , g-evc) = + to-subtype-＝ + (Ξ» _ β†’ βˆƒ-is-prop) + (dfunext fe + (Ξ» n β†’ evc-extension-property + g + (eventual-constancy-property-gives-eventual-constancy-data g g-evc) + n)) + + Ο•-is-equiv : is-equiv Ο• + Ο•-is-equiv = qinvs-are-equivs Ο• (Ξ³ , Ξ³Ο• , ϕγ) + + characterization-of-type-of-continuous-functions-≃ + : (Ξ£ f κž‰ (β„•βˆž β†’ β„•) , is-continuous f) + ≃ (Ξ£ g κž‰ (β„• β†’ β„•), is-eventually-constant g) + characterization-of-type-of-continuous-functions-≃ + = Ο• , Ο•-is-equiv +-} + \end{code}