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.Injectivity
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.InfProperty
open import TypeTopology.LexicographicCompactness
open import TypeTopology.PropInfTychonoff
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α΅)
β ((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 = 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) β©
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α΅)
β ((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α΅)
(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)

ΞΉπα΅ = ΞΉπ

ΞΉπα΅-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α΅)
(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 = 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.

\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)
(βΌ-not-βΊ u v)
(not-βΊ-βΌ 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}