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
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}