Martin Escardo, July 2018

Closure properties of some ordinal constructions.

\begin{code}

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

open import UF.FunExt

module Ordinals.Closure
        (fe : FunExt)
       where

open import CoNaturals.Type
open import InjectiveTypes.Blackboard fe
open import MLTT.AlternativePlus
open import MLTT.Plus-Properties
open import MLTT.Spartan
open import MLTT.Two-Properties
open import Naturals.Binary hiding (_+_ ; L ; R)
open import Notation.CanonicalMap
open import Ordinals.Arithmetic fe
open import Ordinals.InfProperty
open import Ordinals.Injectivity
open import Ordinals.LexicographicCompactness
open import Ordinals.LexicographicOrder
open import Ordinals.ToppedArithmetic fe
open import Ordinals.ToppedType fe
open import Ordinals.Underlying
open import TypeTopology.CompactTypes
open import TypeTopology.ConvergentSequenceHasInf
open import TypeTopology.PropInfTychonoff
open import TypeTopology.SigmaDiscreteAndTotallySeparated
open import TypeTopology.SquashedCantor fe
open import TypeTopology.SquashedSum fe
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.Embeddings
open import UF.Equiv
open import UF.PairFun
open import UF.Retracts
open import UF.Subsingletons

private
 feβ‚€ : funext 𝓀₀ 𝓀₀
 feβ‚€ = fe 𝓀₀ 𝓀₀

\end{code}

Ordinal-indexed sums of topped ordinals are closed under compactness:

\begin{code}

βˆ‘-compactβˆ™ : (Ο„ : Ordα΅€) (Ο… : ⟨ Ο„ ⟩ β†’ Ordα΅€)
           β†’ is-compactβˆ™ ⟨ Ο„ ⟩
           β†’ ((x : ⟨ Ο„ ⟩) β†’ is-compactβˆ™ ⟨ Ο… x ⟩)
           β†’ is-compactβˆ™ ⟨ βˆ‘ Ο„ Ο… ⟩
βˆ‘-compactβˆ™ Ο„ Ο… Ξ΅ Ξ΄ = Ξ£-is-compactβˆ™ Ξ΅ Ξ΄

\end{code}

More compactness closure properties are in the module SquashedSum.

The complication of the following proof in the case for addition is
that the ordinal πŸšα΅’ has underlying set πŸ™+πŸ™ rather than 𝟚, and that
(hence) we defined the ordinal +α΅’ as a sum indexed by πŸ™+πŸ™ rather than
as a co-product. This saved lots of code elsewhere, but adds labour
here (and in some helper lemmas/constructions that we added in other
modules for this purpose). Notice that +' is the sum indexed by 𝟚,
defined in the module MLTT.Spartan. The bulk of the work for the
following construction is performed in the module SquashedCantor.

\begin{code}

+-retract-of-Cantor : (Ο„ : Ordα΅€) (Ο… : Ordα΅€)
                    β†’ retract ⟨ Ο„ ⟩ of Cantor
                    β†’ retract ⟨ Ο… ⟩ of Cantor
                    β†’ retract ⟨ Ο„ +α΅’ Ο…  ⟩ of Cantor
+-retract-of-Cantor Ο„ Ο… Ξ΅ Ξ΄ = retracts-compose d e
 where
  a : retract (Cantor +' Cantor) of (Cantor + Cantor)
  a = +'-retract-of-+

  b : retract (Cantor +' Cantor) of Cantor
  b = retracts-compose +-Cantor-retract a

  c : retract ⟨ Ο„ ⟩ +' ⟨ Ο… ⟩ of (Cantor +' Cantor)
  c = +'-retract Ξ΅ Ξ΄

  d : retract ⟨ Ο„ ⟩ +' ⟨ Ο… ⟩ of Cantor
  d = retracts-compose b c

  e : retract ⟨ Ο„ +α΅’ Ο… ⟩ of (⟨ Ο„ ⟩ +' ⟨ Ο… ⟩)
  e = transport (Ξ» - β†’ retract ⟨ Ο„ +α΅’ Ο… ⟩ of (Ξ£ -)) (dfunext (fe 𝓀₀ 𝓀₁) l) h
   where
    f : 𝟚 β†’ πŸ™ + πŸ™
    f = retraction retract-πŸ™+πŸ™-of-𝟚

    h : retract ⟨ Ο„ +α΅’ Ο… ⟩ of (Ξ£ i κž‰ 𝟚 , ⟨ cases (Ξ» _ β†’ Ο„) (Ξ» _ β†’ Ο…) (f i) ⟩)
    h = Ξ£-reindex-retract f (retraction-has-section retract-πŸ™+πŸ™-of-𝟚)

    l : (i : 𝟚) β†’ ⟨ cases (Ξ» _ β†’ Ο„) (Ξ» _ β†’ Ο…) (f i) ⟩
                = 𝟚-cases ⟨ Ο„ ⟩ ⟨ Ο… ⟩ i
    l β‚€ = refl
    l ₁ = refl

Γ—-retract-of-Cantor : (Ο„ : Ordα΅€) (Ο… : Ordα΅€)
                    β†’ retract ⟨ Ο„ ⟩ of Cantor
                    β†’ retract ⟨ Ο… ⟩ of Cantor
                    β†’ retract ⟨ Ο„ Γ—α΅’ Ο…  ⟩ of Cantor
Γ—-retract-of-Cantor Ο„ Ο… Ξ΅ Ξ΄ =  retracts-compose a b
 where
  a : retract (Cantor Γ— Cantor) of Cantor
  a = pair-seq-retract

  b : retract ⟨ Ο„ ⟩ Γ— ⟨ Ο… ⟩ of (Cantor Γ— Cantor)
  b = Γ—-retract Ξ΅ Ξ΄

\end{code}

More Cantor-retract properties are in the module SquashedCantor.

\begin{code}

Ξ£-retract-of-β„• : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ }
               β†’ retract X of β„•
               β†’ ((x : X) β†’ retract (Y x) of β„•)
               β†’ retract (Ξ£ Y) of β„•
Ξ£-retract-of-β„• {𝓀} {π“₯} {X} {Y} ρ Οƒ = retracts-compose b a
 where
  a : retract (Ξ£ Y) of (β„• Γ— β„•)
  a = Ξ£-retractβ‚‚ ρ Οƒ

  b : retract (β„• Γ— β„•) of β„•
  b = ≃-gives-◁ pairing

Σ₁-β„•-retract : {X : β„• β†’ 𝓀 Μ‡ }
             β†’ ((n : β„•) β†’ retract (X n) of β„•)
             β†’ retract (Σ₁ X) of β„•
Σ₁-β„•-retract {𝓀} {X} ρ = retracts-compose c b
 where
  a : (z : β„• + πŸ™) β†’ retract (X / over) z of ((Ξ» _ β†’ β„•) / over) z
  a = retract-extension X (Ξ» _ β†’ β„•) over ρ

  b : retract (Σ₁ X) of Σ₁ (Ξ» _ β†’ β„•)
  b = Ξ£-retract (X / over) ((Ξ» _ β†’ β„•) / over) a

  c : retract Σ₁ (Ξ» _ β†’ β„•) of β„•
  c = Ξ£-retract-of-β„•
       (≃-gives-◁ β„•-plus-πŸ™)
       (Ξ» (z : β„• + πŸ™) β†’ r z , s z , rs z)
   where
    r : (z : β„• + πŸ™) β†’ β„• β†’ ((Ξ» _ β†’ β„•) / inl) z
    r (inl n) m w = m
    r (inr *) m (k , p) = 𝟘-elim (+disjoint p)
    s : (z : β„• + πŸ™) β†’ ((Ξ» _ β†’ β„•) / inl) z β†’ β„•
    s (inl n) Ο† = Ο† (n , refl)
    s (inr *) Ο† = 0 -- Any natural number will do here.
    rs : (z : β„• + πŸ™) (Ο† : ((Ξ» _ β†’ β„•) / inl) z) β†’ r z (s z Ο†) = Ο†
    rs (inl n) Ο† = dfunext feβ‚€ g
     where
      g : (w : fiber inl (inl n)) β†’ r (inl n) (s (inl n) Ο†) w = Ο† w
      g (n , refl) = refl
    rs (inr *) Ο† = dfunext feβ‚€ g
     where
      g : (w : fiber inl (inr *)) β†’ r (inr *) (s (inr *) Ο†) w = Ο† w
      g (k , p) = 𝟘-elim (+disjoint p)

\end{code}

Preservation of discreteness:

\begin{code}

βˆ‘-is-discrete : (Ο„ : Ordα΅€) (Ο… : ⟨ Ο„ ⟩ β†’ Ordα΅€)
              β†’ is-discrete ⟨ Ο„ ⟩
              β†’ ((x : ⟨ Ο„ ⟩) β†’ is-discrete ⟨ Ο… x ⟩)
              β†’ is-discrete ⟨ βˆ‘ Ο„ Ο… ⟩
βˆ‘-is-discrete Ο„ Ο… Ξ΅ Ξ΄ = Ξ£-is-discrete Ξ΅ Ξ΄

\end{code}

Some maps and their order preservation, used to show that the
embedding of the discrete ordinals into the compact ordinals is order
preserving.

\begin{code}

is-order-preserving  is-order-reflecting  : (Ο„ Ο… : Ordα΅€) β†’ (⟨ Ο„ ⟩ β†’ ⟨ Ο… ⟩) β†’ 𝓀₀ Μ‡

is-order-preserving Ο„ Ο… f = (x y : ⟨ Ο„ ⟩) β†’ x β‰ΊβŸ¨ Ο„ ⟩ y β†’ f x β‰ΊβŸ¨ Ο… ⟩ f y
is-order-reflecting Ο„ Ο… f = (x y : ⟨ Ο„ ⟩) β†’ f x β‰ΊβŸ¨ Ο… ⟩ f y β†’ x β‰ΊβŸ¨ Ο„ ⟩ y

comp-is-order-preserving : (Ο„ Ο… Ο† : Ordα΅€)
                           (f : ⟨ Ο„ ⟩ β†’ ⟨ Ο… ⟩)
                           (g : ⟨ Ο… ⟩ β†’ ⟨ Ο† ⟩)
                         β†’ is-order-preserving Ο„ Ο… f
                         β†’ is-order-preserving Ο… Ο† g
                         β†’ is-order-preserving Ο„ Ο† (g ∘ f)
comp-is-order-preserving Ο„ Ο… Ο† f g p q x y l = q (f x) (f y) (p x y l)

pair-fun-is-order-preserving
 : (Ο„ Ο… : Ordα΅€)
   (A : ⟨ Ο„ ⟩ β†’ Ordα΅€)
   (B : ⟨ Ο… ⟩ β†’ Ordα΅€)
   (f : ⟨ Ο„ ⟩ β†’ ⟨ Ο… ⟩)
   (g : (x : ⟨ Ο„ ⟩) β†’ ⟨ A x ⟩ β†’ ⟨ B (f x) ⟩)
 β†’ is-order-preserving Ο„ Ο… f
 β†’ ((x : ⟨ Ο„ ⟩) β†’ is-order-preserving (A x) (B (f x)) (g x))
 β†’ is-order-preserving (βˆ‘ Ο„ A) (βˆ‘ Ο… B) (pair-fun f g)
pair-fun-is-order-preserving Ο„ Ο… A B f g Ο† Ξ³ (x , a) (y , b) (inl l) =
 inl (Ο† x y l)
pair-fun-is-order-preserving Ο„ Ο… A B f g Ο† Ξ³ (x , a) (x , b) (inr (refl , l)) =
 inr (refl , Ξ³ x a b l)

ΞΉπŸ™α΅’ : ⟨ succβ‚’ Ο‰ ⟩ β†’ ⟨ β„•βˆžα΅’ ⟩
ΞΉπŸ™α΅’ = ΞΉπŸ™

ΞΉπŸ™α΅’-is-order-preserving : is-order-preserving (succβ‚’ Ο‰) β„•βˆžα΅’ ΞΉπŸ™α΅’
ΞΉπŸ™α΅’-is-order-preserving (inl n) (inl m) l = β„•-to-β„•βˆž-order-preserving n m l
ΞΉπŸ™α΅’-is-order-preserving (inl n) (inr *) * = n , (refl , refl)
ΞΉπŸ™α΅’-is-order-preserving (inr *) (inl m) l = 𝟘-elim l
ΞΉπŸ™α΅’-is-order-preserving (inr *) (inr *) l = 𝟘-elim l

open topped-ordinals-injectivity fe

over-ΞΉ-map-is-order-preserving  : (Ο„ : β„• β†’ Ordα΅€) (z : β„• + πŸ™)
                                β†’ is-order-preserving
                                    ((Ο„ β†— (over , over-embedding)) z)
                                    ((Ο„ β†— embedding-β„•-to-β„•βˆž feβ‚€) (ΞΉπŸ™ z))
                                    (over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) z)
over-ΞΉ-map-is-order-preserving Ο„ (inl n) x y ((.n , refl) , l) = (n , refl) , Ξ³
 where
  Ξ³ : over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) (inl n) x (n , refl) β‰ΊβŸ¨ Ο„ n ⟩
      over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) (inl n) y (n , refl)
  Ξ³ = transport₂⁻¹
        (Ξ» a b β†’ a β‰ΊβŸ¨ Ο„ n ⟩ b)
        (over-ΞΉ-map-left (Ξ» n β†’ ⟨ Ο„ n ⟩) n x)
        (over-ΞΉ-map-left (Ξ» n β†’ ⟨ Ο„ n ⟩) n y)
        l
over-ΞΉ-map-is-order-preserving Ο„ (inr *) x y ((n , p) , l) = 𝟘-elim (+disjoint p)

βˆ‘-up : (Ο„ : β„• β†’ Ordα΅€) β†’ ⟨ βˆ‘β‚ Ο„ ⟩ β†’ ⟨ βˆ‘ΒΉ Ο„ ⟩
βˆ‘-up Ο„ = Ξ£-up (Ξ» n β†’ ⟨ Ο„ n ⟩)

βˆ‘-up-is-order-preserving : (Ο„ : β„• β†’ Ordα΅€)
                         β†’ is-order-preserving (βˆ‘β‚ Ο„) (βˆ‘ΒΉ Ο„) (βˆ‘-up Ο„)
βˆ‘-up-is-order-preserving Ο„  = pair-fun-is-order-preserving
                               (succβ‚’ Ο‰)
                               β„•βˆžα΅’
                               (Ο„ β†— (over , over-embedding))
                               (Ο„  β†— embedding-β„•-to-β„•βˆž feβ‚€)
                               ΞΉπŸ™α΅’
                               (over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩))
                               ΞΉπŸ™α΅’-is-order-preserving
                               (over-ΞΉ-map-is-order-preserving Ο„)

βˆ‘β†‘ : (Ο„ Ο… : β„• β†’ Ordα΅€) (f : (n : β„•) β†’ ⟨ Ο„ n ⟩ β†’ ⟨ Ο… n ⟩)
   β†’ ⟨ βˆ‘β‚ Ο„ ⟩ β†’ ⟨ βˆ‘ΒΉ Ο… ⟩
βˆ‘β†‘ Ο„ Ο… = Σ↑ (Ξ» n β†’ ⟨ Ο„ n ⟩) (Ξ» n β†’ ⟨ Ο… n ⟩)

Overα΅’ : (Ο„ Ο… : β„• β†’ Ordα΅€) (f : (n : β„•) β†’ ⟨ Ο„ n ⟩ β†’ ⟨ Ο… n ⟩)
      β†’ (z : β„• + πŸ™) β†’ ⟨ (Ο„ β†— (over , over-embedding)) z ⟩ β†’ ⟨ (Ο… β†— (over , over-embedding)) z ⟩
Overα΅’ Ο„ Ο… = Over (Ξ» n β†’ ⟨ Ο„ n ⟩) (Ξ» n β†’ ⟨ Ο… n ⟩)

Overα΅’-is-order-preserving : (Ο„ Ο… : β„• β†’ Ordα΅€) (f : (n : β„•) β†’ ⟨ Ο„ n ⟩ β†’ ⟨ Ο… n ⟩)
                          β†’ ((n : β„•) β†’ is-order-preserving (Ο„ n) (Ο… n) (f n))
                          β†’ (z : β„• + πŸ™) β†’ is-order-preserving
                                            ((Ο„ β†— (over , over-embedding)) z)
                                            ((Ο… β†— (over , over-embedding)) z)
                                            (Overα΅’ Ο„ Ο… f z)
Overα΅’-is-order-preserving Ο„ Ο… f p (inl n) x y ((.n , refl) , l) =
 (n , refl) , p n _ _ l
Overα΅’-is-order-preserving Ο„ Ο… f p (inr *) x y ((n , q) , l) =
 𝟘-elim (+disjoint q)

βˆ‘β‚-functor : (Ο„ Ο… : β„• β†’ Ordα΅€) (f : (n : β„•) β†’ ⟨ Ο„ n ⟩ β†’ ⟨ Ο… n ⟩)
           β†’ ⟨ βˆ‘β‚ Ο„ ⟩ β†’ ⟨ βˆ‘β‚ Ο… ⟩
βˆ‘β‚-functor Ο„ Ξ½ = Σ₁-functor (Ξ» n β†’ ⟨ Ο„ n ⟩) (Ξ» n β†’ ⟨ Ξ½ n ⟩)

βˆ‘β‚-functor-is-order-preserving
 : (Ο„ Ο… : β„• β†’ Ordα΅€)
   (f : (n : β„•) β†’ ⟨ Ο„ n ⟩ β†’ ⟨ Ο… n ⟩)
 β†’ ((n : β„•) β†’ is-order-preserving (Ο„ n) (Ο… n) (f n))
 β†’ is-order-preserving (βˆ‘β‚ Ο„) (βˆ‘β‚ Ο…) (βˆ‘β‚-functor Ο„ Ο… f)
βˆ‘β‚-functor-is-order-preserving Ο„ Ο… f p =
 pair-fun-is-order-preserving
  (succβ‚’ Ο‰)
  (succβ‚’ Ο‰)
  (Ο„ β†— (over , over-embedding))
  (Ο… β†— (over , over-embedding))
  id
  (Over (Ξ» n β†’ ⟨ Ο„ n ⟩) (Ξ» n β†’ ⟨ Ο… n ⟩) f)
  (Ξ» x y l β†’ l)
  (Overα΅’-is-order-preserving Ο„ Ο… f p)

βˆ‘β†‘-is-order-preserving : (Ο„ Ο… : β„• β†’ Ordα΅€)
                         (f : (n : β„•) β†’ ⟨ Ο„ n ⟩ β†’ ⟨ Ο… n ⟩)
                       β†’ ((n : β„•) β†’ is-order-preserving (Ο„ n) (Ο… n) (f n))
                       β†’ is-order-preserving (βˆ‘β‚ Ο„) (βˆ‘ΒΉ Ο…) (βˆ‘β†‘ Ο„ Ο… f)
βˆ‘β†‘-is-order-preserving Ο„ Ο… f p = comp-is-order-preserving
                                  (βˆ‘β‚ Ο„)
                                  (βˆ‘β‚ Ο… )
                                  (βˆ‘ΒΉ Ο…)
                                  (Σ₁-functor
                                     (Ξ» n β†’ ⟨ Ο„ n ⟩)
                                     (Ξ» n β†’ ⟨ Ο… n ⟩)
                                     f)
                                  (βˆ‘-up Ο…)
                                  (βˆ‘β‚-functor-is-order-preserving Ο„ Ο… f p)
                                  (βˆ‘-up-is-order-preserving Ο…)
\end{code}

And now order reflection.

\begin{code}

comp-is-order-reflecting : (Ο„ Ο… Ο† : Ordα΅€)
                           (f : ⟨ Ο„ ⟩ β†’ ⟨ Ο… ⟩)
                           (g : ⟨ Ο… ⟩ β†’ ⟨ Ο† ⟩)
                         β†’ is-order-reflecting Ο„ Ο… f
                         β†’ is-order-reflecting Ο… Ο† g
                         β†’ is-order-reflecting Ο„ Ο† (g ∘ f)
comp-is-order-reflecting Ο„ Ο… Ο† f g p q x y l = p x y (q (f x) (f y) l)

pair-fun-is-order-reflecting
 : (Ο„ Ο… : Ordα΅€)
   (A : ⟨ Ο„ ⟩ β†’ Ordα΅€)
   (B : ⟨ Ο… ⟩ β†’ Ordα΅€)
   (f : ⟨ Ο„ ⟩ β†’ ⟨ Ο… ⟩)
   (g  : (x : ⟨ Ο„ ⟩) β†’ ⟨ A x ⟩ β†’ ⟨ B (f x) ⟩)
 β†’ is-order-reflecting Ο„ Ο… f
 β†’ is-embedding f
 β†’ ((x : ⟨ Ο„ ⟩) β†’ is-order-reflecting (A x) (B (f x)) (g x))
 β†’ is-order-reflecting (βˆ‘ Ο„ A) (βˆ‘ Ο… B) (pair-fun f g)
pair-fun-is-order-reflecting Ο„ Ο… A B f g Ο† e Ξ³ (x , a) (y , b) (inl l) =
 inl (Ο† x y l)
pair-fun-is-order-reflecting Ο„ Ο… A B f g Ο† e Ξ³ (x , a) (y , b) (inr (r , l)) =
 inr (c r , p)
 where
  e' : is-equiv (ap f)
  e' = embedding-gives-embedding' f e x y

  c : f x = f y β†’ x = y
  c = inverse (ap f) e'

  Ξ· : (q : f x = f y) β†’ ap f (c q) = q
  Ξ· = retract-condition (ap f , equivs-have-sections (ap f) e')

  i : transport (Ξ» - β†’ ⟨ B (f -) ⟩) (c r) (g x a)
    = transport (Ξ» - β†’ ⟨ B - ⟩) (ap f (c r)) (g x a)
  i = transport-ap (Ξ» - β†’ ⟨ B - ⟩) f (c r)

  j : transport (Ξ» - β†’ ⟨ B - ⟩) (ap f (c r)) (g x a) β‰ΊβŸ¨ B (f y) ⟩ (g y b)
  j = transport⁻¹
       (Ξ» - β†’ transport (Ξ» - β†’ ⟨ B - ⟩) - (g x a) β‰ΊβŸ¨ B (f y) ⟩ (g y b))
       (Ξ· r)
       l

  k : transport (Ξ» - β†’ ⟨ B (f -) ⟩) (c r) (g x a) β‰ΊβŸ¨ B (f y) ⟩ (g y b)
  k = transport⁻¹ (Ξ» - β†’ - β‰ΊβŸ¨ B (f y) ⟩ (g y b)) i j

  h : {x y : ⟨ Ο„ ⟩} (s : x = y) {a : ⟨ A x ⟩} {b : ⟨ A y ⟩}
    β†’ transport (Ξ» - β†’ ⟨ B (f -) ⟩) s (g x a) β‰ΊβŸ¨ B (f y) ⟩ (g y b)
    β†’ transport (Ξ» - β†’ ⟨ A - ⟩) s a β‰ΊβŸ¨ A y ⟩ b
  h {x} refl {a} {b} = Ξ³ x a b

  p : transport (Ξ» - β†’ ⟨ A - ⟩) (c r) a β‰ΊβŸ¨ A y ⟩ b
  p = h (c r) k

ΞΉπŸ™α΅’-is-order-reflecting : is-order-reflecting (succβ‚’ Ο‰) β„•βˆžα΅’ ΞΉπŸ™α΅’
ΞΉπŸ™α΅’-is-order-reflecting (inl n) (inl m) l =
 β„•-to-β„•βˆž-order-reflecting n m l
ΞΉπŸ™α΅’-is-order-reflecting (inl n) (inr *) l = *
ΞΉπŸ™α΅’-is-order-reflecting (inr *) (inl m) (n , (p , l)) =
 𝟘-elim (∞-is-not-finite n p)
ΞΉπŸ™α΅’-is-order-reflecting (inr *) (inr *) (n , (p , l)) =
 𝟘-elim (∞-is-not-finite n p)

over-ΞΉ-map-is-order-reflecting  : (Ο„ : β„• β†’ Ordα΅€) (z : β„• + πŸ™)
                                β†’ is-order-reflecting
                                    ((Ο„ β†— (over , over-embedding)) z)
                                    ((Ο„ β†— embedding-β„•-to-β„•βˆž feβ‚€) (ΞΉπŸ™ z))
                                    (over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) z)
over-ΞΉ-map-is-order-reflecting Ο„ (inl n) x y ((m , p) , l) = (n , refl) , q
 where
  x' : ⟨ Ο„ n ⟩
  x' = over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) (inl n) x (n , refl)

  y' : ⟨ Ο„ n ⟩
  y' = over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) (inl n) y (n , refl)

  r : n , refl = m , p
  r = β„•-to-β„•βˆž-is-embedding feβ‚€ (ΞΉ n) (n , refl) (m , p)

  t : ⟨ Ο„ n ⟩ β†’ ⟨ Ο„ m ⟩
  t = transport (Ξ» - β†’ ⟨ Ο„ (pr₁ -) ⟩) r

  tr : {w t : fiber ι (ι n)} (r : w = t)
     β†’ is-order-reflecting
        (Ο„ (pr₁ w))
        (Ο„ (pr₁ t))
        (transport (Ξ» - β†’ ⟨ Ο„ (pr₁ -) ⟩) r)
  tr refl x y l = l

  a : t x' = over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) (inl n) x (m , p)
  a = apd (over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) (inl n) x) r

  b : t y' = over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) (inl n) y (m , p)
  b = apd (over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩) (inl n) y) r

  c : t x' β‰ΊβŸ¨ Ο„ m ⟩ t y'
  c = transport₂⁻¹ (Ξ» a b β†’ a β‰ΊβŸ¨ Ο„ m ⟩ b) a b l

  d : x' β‰ΊβŸ¨ Ο„ n ⟩ y'
  d = tr r _ _ c

  q : x (n , refl) β‰ΊβŸ¨ Ο„ n ⟩ y (n , refl)
  q = transportβ‚‚
       (Ξ» a b β†’ a β‰ΊβŸ¨ Ο„ n ⟩ b)
       (over-ΞΉ-map-left (Ξ» n β†’ ⟨ Ο„ n ⟩) n x)
       (over-ΞΉ-map-left (Ξ» n β†’ ⟨ Ο„ n ⟩) n y)
       d
over-ΞΉ-map-is-order-reflecting Ο„ (inr *) x y ((m , p) , l) =
 𝟘-elim (∞-is-not-finite m (p ⁻¹))

βˆ‘-up-is-order-reflecting : (Ο„ : β„• β†’ Ordα΅€)
                         β†’ is-order-reflecting (βˆ‘β‚ Ο„) (βˆ‘ΒΉ Ο„) (βˆ‘-up Ο„)
βˆ‘-up-is-order-reflecting Ο„  = pair-fun-is-order-reflecting
                               (succβ‚’ Ο‰)
                               β„•βˆžα΅’
                               (Ο„ β†— (over , over-embedding))
                               (Ο„  β†— embedding-β„•-to-β„•βˆž feβ‚€)
                               ΞΉπŸ™α΅’
                               (over-ΞΉ-map (Ξ» n β†’ ⟨ Ο„ n ⟩))
                               ΞΉπŸ™α΅’-is-order-reflecting
                               (ΞΉπŸ™-is-embedding feβ‚€)
                               (over-ΞΉ-map-is-order-reflecting Ο„)

Overα΅’-is-order-reflecting : (Ο„ Ο… : β„• β†’ Ordα΅€)
                            (f : (n : β„•) β†’ ⟨ Ο„ n ⟩ β†’ ⟨ Ο… n ⟩)
                          β†’ ((n : β„•) β†’ is-order-reflecting (Ο„ n) (Ο… n) (f n))
                          β†’ (z : β„• + πŸ™) β†’ is-order-reflecting
                                           ((Ο„ β†— (over , over-embedding)) z)
                                           ((Ο… β†— (over , over-embedding)) z)
                                           (Overα΅’ Ο„ Ο… f z)
Overα΅’-is-order-reflecting Ο„ Ο… f p (inl n) x y ((.n , refl) , l) =
 (n , refl) , p n _ _ l
Overα΅’-is-order-reflecting Ο„ Ο… f p (inr *) x y ((n , q) , l) =
 𝟘-elim (+disjoint q)

βˆ‘β‚-functor-is-order-reflecting
 : (Ο„ Ο… : β„• β†’ Ordα΅€)
   (f : (n : β„•) β†’ ⟨ Ο„ n ⟩ β†’ ⟨ Ο… n ⟩)
 β†’ ((n : β„•) β†’ is-order-reflecting (Ο„ n) (Ο… n) (f n))
 β†’ is-order-reflecting (βˆ‘β‚ Ο„) (βˆ‘β‚ Ο…) (βˆ‘β‚-functor Ο„ Ο… f)
βˆ‘β‚-functor-is-order-reflecting Ο„ Ο… f p =
 pair-fun-is-order-reflecting
  (succβ‚’ Ο‰)
  (succβ‚’ Ο‰)
  (Ο„ β†— (over , over-embedding))
  (Ο… β†— (over , over-embedding))
  id
  (Over (Ξ» n β†’ ⟨ Ο„ n ⟩) (Ξ» n β†’ ⟨ Ο… n ⟩) f)
  (Ξ» x y l β†’ l)
  id-is-embedding
  (Overα΅’-is-order-reflecting Ο„ Ο… f p)

βˆ‘β†‘-is-order-reflecting : (Ο„ Ο… : β„• β†’ Ordα΅€) (f : (n : β„•) β†’ ⟨ Ο„ n ⟩ β†’ ⟨ Ο… n ⟩)
                       β†’ ((n : β„•) β†’ is-order-reflecting (Ο„ n) (Ο… n) (f n))
                       β†’ is-order-reflecting (βˆ‘β‚ Ο„) (βˆ‘ΒΉ Ο…) (βˆ‘β†‘ Ο„ Ο… f)
βˆ‘β†‘-is-order-reflecting Ο„ Ο… f p = comp-is-order-reflecting
                                  (βˆ‘β‚ Ο„)
                                  (βˆ‘β‚ Ο… )
                                  (βˆ‘ΒΉ Ο…)
                                  (Σ₁-functor
                                    (Ξ» n β†’ ⟨ Ο„ n ⟩)
                                    (Ξ» n β†’ ⟨ Ο… n ⟩)
                                    f)
                                  (βˆ‘-up Ο…)
                                  (βˆ‘β‚-functor-is-order-reflecting Ο„ Ο… f p)
                                  (βˆ‘-up-is-order-reflecting Ο…)
\end{code}

28 July 2018. Inf property.

\begin{code}

πŸ™α΅’-has-infs-of-complemented-subsets : has-infs-of-complemented-subsets (πŸ™α΅’ {𝓀})
πŸ™α΅’-has-infs-of-complemented-subsets p = ⋆ , f , g , h
 where
  f : (Ξ£ x κž‰ πŸ™ , p x = β‚€) β†’ p ⋆ = β‚€
  f (⋆ , r) = r

  g : (x : πŸ™) β†’ p x = β‚€ β†’ ⋆ β‰ΎβŸ¨ πŸ™α΅’ ⟩ x
  g ⋆ r a = 𝟘-elim a

  h : (x : πŸ™) β†’ is-roots-lower-bound (Ξ» x y β†’ x β‰ΎβŸ¨ πŸ™α΅’ ⟩ y) p x β†’ x β‰ΎβŸ¨ πŸ™α΅’ ⟩ ⋆
  h ⋆ Ο† a = 𝟘-elim a

πŸšα΅’-has-infs-of-complemented-subsets : has-infs-of-complemented-subsets πŸšα΅’
πŸšα΅’-has-infs-of-complemented-subsets p = 𝟚-equality-cases Ο† Ξ³
 where
  _≀_ : πŸ™ + πŸ™ β†’ πŸ™ + πŸ™ β†’ 𝓀₀ Μ‡
  x ≀ y = x β‰ΎβŸ¨ πŸšα΅’ ⟩ y

  Ο† : (r : p (inl ⋆) = β‚€) β†’ Ξ£ x κž‰ πŸ™ + πŸ™ , is-conditional-root _≀_ p x Γ— is-roots-infimum _≀_ p x
  Ο† r = inl ⋆ , f , g , h
   where
    f : (Ξ£ x κž‰ πŸ™ + πŸ™ , p x = β‚€) β†’ p (inl ⋆) = β‚€
    f (inl ⋆ , s) = s
    f (inr ⋆ , s) = r

    g : (x : πŸ™ + πŸ™) β†’ p x = β‚€ β†’ inl ⋆ ≀ x
    g (inl ⋆) s l = 𝟘-elim l
    g (inr ⋆) s l = 𝟘-elim l

    h : (x : πŸ™ + πŸ™) β†’ is-roots-lower-bound _≀_ p x β†’ x ≀ inl ⋆
    h (inl ⋆) Ο† l = 𝟘-elim l
    h (inr ⋆) Ο† ⋆ = Ο† (inl ⋆) r ⋆

  Ξ³ : (r : p (inl ⋆) = ₁)
    β†’ Ξ£ x κž‰ πŸ™ + πŸ™ , is-conditional-root _≀_ p x Γ— is-roots-infimum _≀_ p x
  Ξ³ r = inr ⋆ , f , g , h
   where
    f : (Ξ£ x κž‰ πŸ™ + πŸ™ , p x = β‚€) β†’ p (inr ⋆) = β‚€
    f (inl ⋆ , s) = 𝟘-elim (zero-is-not-one (s ⁻¹ βˆ™ r))
    f (inr ⋆ , s) = s

    g : (x : πŸ™ + πŸ™) β†’ p x = β‚€ β†’ inr ⋆ ≀ x
    g (inl ⋆) s l = 𝟘-elim (zero-is-not-one (s ⁻¹ βˆ™ r))
    g (inr ⋆) s l = 𝟘-elim l

    h : (x : πŸ™ + πŸ™) β†’ is-roots-lower-bound _≀_ p x β†’ x ≀ inr ⋆
    h (inl ⋆) Ο† a = 𝟘-elim a
    h (inr ⋆) Ο† a = 𝟘-elim a

\end{code}

It is not necessary to use propositional extensionality to prove the
following, but it is simpler to do so given that we have already
proved has-infs-of-complemented-subsets for various types using
different, logically equivalent orders.

TODO. This is a bottleneck. The use of propext here propagates to a
number of files which otherwise wouldn't need to assume propext. Maybe
get rid of this at some point, here and in the other files.

\begin{code}

βˆ‘-has-infs-of-complemented-subsets
 : propext 𝓀₀
 β†’ (Ο„ : Ordα΅€) (Ο… : ⟨ Ο„ ⟩ β†’ Ordα΅€)
 β†’ has-infs-of-complemented-subsets Ο„
 β†’ ((x : ⟨ Ο„ ⟩) β†’ has-infs-of-complemented-subsets (Ο… x))
 β†’ has-infs-of-complemented-subsets (βˆ‘ Ο„ Ο…)
βˆ‘-has-infs-of-complemented-subsets pe Ο„ Ο… Ξ΅ Ξ΄ = Ξ³
 where
  _≀_ : ⟨ βˆ‘ Ο„ Ο… ⟩ β†’ ⟨ βˆ‘ Ο„ Ο… ⟩ β†’ 𝓀₀ Μ‡
  _≀_ = lex-order (Ξ» x y β†’ x β‰ΎβŸ¨ Ο„ ⟩ y) (Ξ» {x} a b β†’ a β‰ΎβŸ¨ Ο… x ⟩ b)

  ≀-prop-valued : (z t : ⟨ βˆ‘ Ο„ Ο… ⟩) β†’ is-prop (z ≀ t)
  ≀-prop-valued (x , a) (y , b) (p , u) (q , v) =
   to-Σ-=
    (β‰Ύ-prop-valued Ο„ x y p q ,
    dfunext feβ‚€ (Ξ» r β†’ β‰Ύ-prop-valued (Ο… y) _ _ _ _))

  Ο† : has-inf _≀_
  Ο† = Ξ£-has-inf ((Ξ» x y β†’ x β‰ΎβŸ¨ Ο„ ⟩ y)) ((Ξ» {x} a b β†’ a β‰ΎβŸ¨ Ο… x ⟩ b)) Ξ΅ Ξ΄

  open lexicographic-commutation
         (underlying-order Ο„)
         (Ξ» {x} β†’ underlying-order (Ο… x))
         (𝟘 {𝓀₀})
       hiding (_≀_)

  i : (z t : ⟨ βˆ‘ Ο„ Ο… ⟩) β†’ z ≀ t β†’ z β‰ΎβŸ¨ βˆ‘ Ο„ Ο… ⟩ t
  i (x , a) (y , b) = back y x b a

  j : (z t : ⟨ βˆ‘ Ο„ Ο… ⟩) β†’ z β‰ΎβŸ¨ βˆ‘ Ο„ Ο… ⟩ t β†’ z ≀ t
  j (x , a) (y , b) = forth y x b a

  k : (z t : ⟨ βˆ‘ Ο„ Ο… ⟩) β†’ z ≀ t = z β‰ΎβŸ¨ βˆ‘ Ο„ Ο… ⟩ t
  k z t = pe (≀-prop-valued z t) (β‰Ύ-prop-valued (βˆ‘ Ο„ Ο…) z t) (i z t) (j z t)

  l : _≀_ = (Ξ» z t β†’ z β‰ΎβŸ¨ βˆ‘ Ο„ Ο… ⟩ t)
  l = dfunext (fe 𝓀₀ 𝓀₁) (Ξ» z β†’ dfunext (fe 𝓀₀ 𝓀₁) (k z))

  Ξ³ : has-infs-of-complemented-subsets (βˆ‘ Ο„ Ο…)
  Ξ³ = transport has-inf l Ο†

β„•βˆžα΅’-has-infs-of-complemented-subsets : propext 𝓀₀
                                     β†’ has-infs-of-complemented-subsets β„•βˆžα΅’
β„•βˆžα΅’-has-infs-of-complemented-subsets pe = transport has-inf p (β„•βˆž-has-inf feβ‚€)
 where
  p : _β‰Όβ„•βˆž_ = underlying-weak-order β„•βˆžα΅’
  p = dfunext (fe 𝓀₀ 𝓀₁)
       (Ξ» u β†’ dfunext (fe 𝓀₀ 𝓀₁)
                (Ξ» v β†’ pe (β‰Ό-is-prop-valued feβ‚€ u v)
                          (β‰Ύ-prop-valued β„•βˆžα΅’ u v)
                          (β‰Ό-gives-not-β‰Ί u v)
                          (not-β‰Ί-gives-β‰Ό feβ‚€ u v)))


βˆ‘β‚-has-infs-of-complemented-subsets
 : propext 𝓀₀
 β†’ (Ο„ : β„• β†’ Ordα΅€)
 β†’ ((n : β„•) β†’ has-infs-of-complemented-subsets (Ο„ n))
 β†’ has-infs-of-complemented-subsets (βˆ‘ΒΉ Ο„)
βˆ‘β‚-has-infs-of-complemented-subsets pe Ο„ Ξ΅ =
 βˆ‘-has-infs-of-complemented-subsets pe
  β„•βˆžα΅’
  (Ξ» (x : β„•βˆž) β†’ (Ο„ β†— embedding-β„•-to-β„•βˆž feβ‚€) x)
  (β„•βˆžα΅’-has-infs-of-complemented-subsets pe)
  a
 where
  a : (x : ⟨ β„•βˆžα΅’ ⟩) β†’ has-infs-of-complemented-subsets
                       ((Ο„ β†— embedding-β„•-to-β„•βˆž feβ‚€) x)
  a x = prop-inf-tychonoff fe
         (β„•-to-β„•βˆž-is-embedding feβ‚€ x)
         (Ξ» {w} x y β†’ x β‰ΊβŸ¨ Ο„ (pr₁ w) ⟩ y)
         (Ξ» w β†’ Ξ΅ (pr₁ w))

\end{code}