Ian Ray 1 September 2023 -- edited 9 April 2024
We formalize Curi's notion of abstract inductive definition (in CZF) within
the context of a sup-lattice L with small basis B (and β : B → L). An abstract
inductive definition is a subset ϕ : B × L → Prop (in the TypeTopology library
the type of propositions is denoted Ω) which can be thought of as a
'inference rule' concluding b from a (in the case ϕ(b,a) holds). An inductive
definition induces a closure condition. For example, a subset S is closed under
ϕ if for all b : B and a : L such that (b , a) ∈ ϕ and ↓ᴮa is 'contained' in
S then b ∈ S. Interestingly, there is an intimate connection between the
least-closed subsets of some inductive definition ϕ and the least fixed point
of a monotone map related to ϕ. Constructing these least-closed subsets in
traditional foundations is somewhat grueling. Fortunately, unlike in the realm
of set theory, inductive constructions are first class citizens in a type
theoretic setting. Using UF + HITs we can construct the least closed subset,
under an inductive definition ϕ, as a special quotient inductive type (QIT).
In this file we will develop this relationship and prove a predicative version
of the least fixed point theorem. This work follows the paper 'On Tarski's
Fixed Point Theorem' by Giovanni Curi:
Giovanni Curi. "On Tarski's fixed point theorem". In: Proc. Amer. Math. Soc
143 (2015), pp. 4439-4455. DOI: http://doi.org/10.1090/proc/12569
For a write up of the present formalization in a type theoretic setting see
https://arxiv.org/abs/2401.00841
The content of the present formalization works towards the following result.
Predicative Least Fixed Point Theorem:
Given a 𝓥-sup-lattice L with a 𝓥-presentation and a monotone
endomap f : L → L. If there exists a bounded abstract inductive definition
ϕ such that f ＝ Γ ϕ, then f has a least fixed point.
\begin{code}
{-# OPTIONS --safe --without-K --exact-split #-}
open import MLTT.Spartan
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Logic
open import UF.Powerset-MultiUniverse
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import UF.Size
open import UF.SmallnessProperties
open import UF.UniverseEmbedding
module OrderedTypes.PredicativeLFP
(pt : propositional-truncations-exist)
(fe : Fun-Ext)
(pe : Prop-Ext)
where
private
fe' : FunExt
fe' 𝓤 𝓥 = fe {𝓤} {𝓥}
open import Locales.Frame pt fe hiding (⟨_⟩ ; join-of)
open import Slice.Family
open import UF.ImageAndSurjection pt
open import OrderedTypes.SupLattice pt fe
open import OrderedTypes.SupLattice-SmallBasis pt fe
open AllCombinators pt fe
open PropositionalTruncation pt
\end{code}
We commence by defining what it means for a monotone endomap to have
a least fixed point.
\begin{code}
module _ {𝓤 𝓣 𝓥 : Universe} (L : Sup-Lattice 𝓤 𝓣 𝓥) where
has-least-fixed-point : (f : ⟨ L ⟩ → ⟨ L ⟩) → 𝓤 ⊔ 𝓣 ̇
has-least-fixed-point f =
Σ p ꞉ ⟨ L ⟩ , (f p ＝ p) × ((a : ⟨ L ⟩) → (f a ＝ a) → (p ≤⟨ L ⟩ a) holds)
has-least-fixed-point-is-prop : (f : ⟨ L ⟩ → ⟨ L ⟩)
→ is-prop (has-least-fixed-point f)
has-least-fixed-point-is-prop f (p₁ , fp₁ , l₁) (p₂ , fp₂ , l₂) =
to-subtype-＝ (λ x → ×-is-prop
(sethood-of L)
(Π-is-prop fe (λ y → Π-is-prop fe
(λ _ → holds-is-prop (x ≤⟨ L ⟩ y)))))
(antisymmetry-of L (l₁ p₂ fp₂) (l₂ p₁ fp₁))
\end{code}
We construct the least closed subset of an inductive definition as a QIT family.
Since QITs (and more generally HITs) are not native in Agda we will instead
assume the existence of such a type as well as its induction principle.
Technically speaking we are going to use record types to package the contents
of this QIT family.
Notice all constructors are 'strictly positive' and the path constructors are
'natural' (see Chapter 6 Section 13 of the HoTT book
https://homotopytypetheory.org/book/).
Notice that the QIT family has two constructors which represent the closure
conditions we wish to impose on subsets. The c-closure condition says:
for any subset contained in the least closed subset, elements in the downset of
its join are in the least closed subset as well. That is, Y is c-closed if
for any U ⊆ Y we have ↓ᴮ (⋁ U) ⊆ Y.
The ϕ-cl constructor says:
if for any a : L and b : B with (b , a) ∈ ϕ and ↓ᴮ a 'contained' in the least
closed subset then b is in the least closed subset. That is, Y is ϕ-closed if
for any a : L and b : B we have (b , a) ∈ ϕ ∧ ↓ᴮ a ⊆ Y ⇒ b ∈ Y.
It is worth noting that we don't encode the downsets as subsets in type
theory (rather they are total spaces) so for that reason we won't encode the
closure conditions exactly as above.
TODO: Add syntax so the closure conditions more closely align with the naive
description given above.
We also derive the initiality of the least closed subset from the postulated
induction principle. Initiality is closely related to the 'least' part of
our least fixed point theorem.
\begin{code}
module _
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
private
_≤_ = order-of L
⋁_ = join-of L
open Joins _≤_
open is-basis h
\end{code}
We give names to the closure conditions.
\begin{code}
c-closure : {𝓦 : Universe} (S : 𝓟 {𝓦} B) → (𝓥 ⁺) ⊔ 𝓦 ̇
c-closure S = (U : 𝓟 {𝓥} B)
→ U ⊆ S
→ (b : B) → b ≤ᴮ (⋁ 【 β , U 】)
→ b ∈ S
_closure : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
→ {𝓦 : Universe} (S : 𝓟 {𝓦} B)
→ 𝓤 ⊔ 𝓥 ⊔ 𝓦 ̇
(ϕ closure) S = (a : ⟨ L ⟩)
→ (b : B)
→ (b , a) ∈ ϕ
→ ((b' : B) → (b' ≤ᴮ a → b' ∈ S))
→ b ∈ S
\end{code}
The following record type should be interpreted as supplying the assumption
that the QIT family exists with the apropriate 'initiality' principle
(initiality is considerably weaker than an induction/recursion principle that
one may expect).
\begin{code}
record inductively-generated-subset-exists (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)): 𝓤ω
where
constructor
inductively-generated-subset
field
Ind : B → 𝓤 ⊔ 𝓥 ⁺ ̇
Ind-trunc : (b : B) → is-prop (Ind b)
private
𝓘 : 𝓟 {𝓤 ⊔ 𝓥 ⁺} B
𝓘 b = (Ind b , Ind-trunc b)
field
c-closed : c-closure 𝓘
ϕ-closed : (ϕ closure) 𝓘
Ind-initial : (P : 𝓟 {𝓦} B)
→ c-closure P
→ (ϕ closure) P
→ 𝓘 ⊆ P
module trunc-ind-def
(ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
(ind-e : inductively-generated-subset-exists ϕ)
where
open inductively-generated-subset-exists ind-e
\end{code}
We will now combine the postulated data above to form the least closed subset
of B under some inductive definition ϕ and restate the closure properties and
initiality in terms of it.
\begin{code}
𝓘nd : 𝓟 {𝓤 ⊔ 𝓥 ⁺} B
𝓘nd b = (Ind b , Ind-trunc b)
𝓘nd-is-c-closed : c-closure 𝓘nd
𝓘nd-is-c-closed = c-closed
𝓘nd-is-ϕ-closed : (ϕ closure) 𝓘nd
𝓘nd-is-ϕ-closed = ϕ-closed
𝓘nd-is-initial : (P : 𝓟 {𝓦} B)
→ c-closure P
→ (ϕ closure) P
→ 𝓘nd ⊆ P
𝓘nd-is-initial = Ind-initial
\end{code}
We now consider a restricted class of inductive definitions which we will call
local. A local inductive definition ϕ is one such that the type
Σ b ꞉ B , (Ǝ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ a)
is small.
We then define an operator parameterized by local inductive definitions
and prove that it is monotone. Finally, we show that any monotone endo map on
a sup-lattice determines a monotone operator and corresponding local
inductive definition.
\begin{code}
module local-inductive-definitions
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
private
_≤_ = order-of L
⋁_ = join-of L
open Joins _≤_
open is-basis h
\end{code}
We now define an auxiliary subset/total space which we will use to define the
upcoming monotone operator. This subset is in some sense a generalized downset
that depends on ϕ.
\begin{code}
_↓_ : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)) → (a : ⟨ L ⟩) → 𝓤 ⊔ 𝓣 ⊔ 𝓥 ̇
ϕ ↓ a = Σ b ꞉ B , (Ǝ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ a) holds) holds
↓-to-base : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)) → (a : ⟨ L ⟩) → ϕ ↓ a → B
↓-to-base ϕ a = pr₁
↓-monotonicity-lemma : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
→ (x y : ⟨ L ⟩)
→ (x ≤ y) holds
→ ϕ ↓ x
→ ϕ ↓ y
↓-monotonicity-lemma ϕ x y o (b , c) = (b , inclusion c)
where
inclusion : (Ǝ a' ꞉ ⟨ L ⟩ , ((b , a') ∈ ϕ) × ((a' ≤ x) holds)) holds
→ (Ǝ a' ꞉ ⟨ L ⟩ , ((b , a') ∈ ϕ) × ((a' ≤ y) holds)) holds
inclusion = ∥∥-functor untrunc-inclusion
where
untrunc-inclusion : Σ a' ꞉ ⟨ L ⟩ , ((b , a') ∈ ϕ) × ((a' ≤ x) holds)
→ Σ a' ꞉ ⟨ L ⟩ , ((b , a') ∈ ϕ) × ((a' ≤ y) holds)
untrunc-inclusion (a' , p , r) = (a' , p , transitivity-of L a' x y r o)
↓-has-sup-implies-monotone : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
→ (x y s s' : ⟨ L ⟩)
→ (x ≤ y) holds
→ (s is-lub-of (ϕ ↓ x , β ∘ ↓-to-base ϕ x)) holds
→ (s' is-lub-of (ϕ ↓ y , β ∘ ↓-to-base ϕ y)) holds
→ (s ≤ s') holds
↓-has-sup-implies-monotone
ϕ x y s s' o (is-upbnd , is-least-upbnd) (is-upbnd' , is-least-upbnd') =
is-least-upbnd (s' , s'-is-upbnd)
where
s'-is-upbnd : (s' is-an-upper-bound-of (ϕ ↓ x , β ∘ ↓-to-base ϕ x)) holds
s'-is-upbnd (b , e) = is-upbnd' (↓-monotonicity-lemma ϕ x y o ((b , e)))
is-local : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)) → 𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ̇
is-local ϕ = (a : ⟨ L ⟩) → (ϕ ↓ a) is 𝓥 small
module _ (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)) (i : is-local ϕ) where
private
S' : (a : ⟨ L ⟩) → 𝓥 ̇
S' a = resized (ϕ ↓ a) (i a)
S'-equiv-↓ : (a : ⟨ L ⟩) → S' a ≃ ϕ ↓ a
S'-equiv-↓ a = resizing-condition (i a)
S'-to-↓ : (a : ⟨ L ⟩) → S' a → ϕ ↓ a
S'-to-↓ a = ⌜ S'-equiv-↓ a ⌝
↓-to-S' : (a : ⟨ L ⟩) → ϕ ↓ a → S' a
↓-to-S' a = ⌜ S'-equiv-↓ a ⌝⁻¹
S'-monotone-ish : (x y : ⟨ L ⟩)
→ (x ≤ y) holds
→ S' x
→ S' y
S'-monotone-ish x y o =
↓-to-S' y ∘ ↓-monotonicity-lemma ϕ x y o ∘ S'-to-↓ x
Γ : ⟨ L ⟩ → ⟨ L ⟩
Γ a = ⋁ (S' a , β ∘ pr₁ ∘ S'-to-↓ a)
\end{code}
We show that Γ is monotone.
\begin{code}
Γ-is-monotone : is-monotone-endomap L Γ
Γ-is-monotone x y o =
↓-has-sup-implies-monotone ϕ x y (Γ x) (Γ y) o Γx-is-lub Γy-is-lub
where
Γx-is-lub : (Γ x is-lub-of (ϕ ↓ x , β ∘ ↓-to-base ϕ x)) holds
Γx-is-lub = sup-of-small-fam-is-lub L (β ∘ ↓-to-base ϕ x) (i x)
Γy-is-lub : (Γ y is-lub-of (ϕ ↓ y , β ∘ ↓-to-base ϕ y)) holds
Γy-is-lub = sup-of-small-fam-is-lub L (β ∘ ↓-to-base ϕ y) (i y)
\end{code}
We now show that every monotone map determines and local inductive definition.
\begin{code}
monotone-map-give-local-ind-def : (f : ⟨ L ⟩ → ⟨ L ⟩)
→ is-monotone-endomap L f
→ Σ ϕ ꞉ 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩) ,
Σ i ꞉ (is-local ϕ) ,
((x : ⟨ L ⟩) → (Γ ϕ i) x ＝ f x)
monotone-map-give-local-ind-def f f-mono = (ϕ , i , H)
where
ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)
ϕ (b , a) =
(Lift 𝓤 (b ≤ᴮ f a) , equiv-to-prop (Lift-≃ 𝓤 (b ≤ᴮ f a)) ≤ᴮ-is-prop-valued)
↓ᴮf-equiv-↓-tot : (a : ⟨ L ⟩) → small-↓ᴮ (f a) ≃ ϕ ↓ a
↓ᴮf-equiv-↓-tot a =
Σ-cong' (λ z → z ≤ᴮ f a)
((λ z → (Ǝ a' ꞉ ⟨ L ⟩ , (z , a') ∈ ϕ × (a' ≤ a) holds) holds))
↓ᴮf-equiv-↓
where
↓ᴮf-equiv-↓ : (z : B)
→ (z ≤ᴮ f a)
≃ (Ǝ a' ꞉ ⟨ L ⟩ , (z , a') ∈ ϕ × (a' ≤ a) holds) holds
↓ᴮf-equiv-↓ z =
⌜ prop-≃-≃-↔ fe ≤ᴮ-is-prop-valued ∥∥-is-prop ⌝⁻¹ (↓ᴮf-to-↓ , ↓-to-↓ᴮf)
where
↓ᴮf-to-↓ : z ≤ᴮ f a
→ (Ǝ a' ꞉ ⟨ L ⟩ , (z , a') ∈ ϕ × (a' ≤ a) holds) holds
↓ᴮf-to-↓ o = ∣ (a , ⌜ ≃-Lift 𝓤 (z ≤ᴮ f a) ⌝ o , reflexivity-of L a) ∣
↓-to-↓ᴮf : (Ǝ a' ꞉ ⟨ L ⟩ , (z , a') ∈ ϕ × (a' ≤ a) holds) holds
→ z ≤ᴮ f a
↓-to-↓ᴮf = ∥∥-rec ≤ᴮ-is-prop-valued ↓-to-↓ᴮf'
where
↓-to-↓ᴮf' : Σ a' ꞉ ⟨ L ⟩ , (z , a') ∈ ϕ × (a' ≤ a) holds → z ≤ᴮ f a
↓-to-↓ᴮf' (a' , o , r) =
≤-to-≤ᴮ (transitivity-of L (β z) (f a') (f a)
(≤ᴮ-to-≤
(⌜ ≃-Lift 𝓤 (z ≤ᴮ f a') ⌝⁻¹ o))
(f-mono a' a r))
i : is-local ϕ
i a = (small-↓ᴮ (f a) , ↓ᴮf-equiv-↓-tot a)
G : (x : ⟨ L ⟩) → (f x is-lub-of (ϕ ↓ x , β ∘ ↓-to-base ϕ x)) holds
G x = (fx-is-upbnd , fx-is-least-upbnd)
where
fx-is-upbnd : (f x is-an-upper-bound-of (ϕ ↓ x , β ∘ ↓-to-base ϕ x)) holds
fx-is-upbnd (b , e) = ↓-to-fx-upbnd e
where
↓-to-fx-upbnd : (Ǝ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ x) holds) holds
→ (β b ≤ f x) holds
↓-to-fx-upbnd = ∥∥-rec (holds-is-prop (β b ≤ f x)) ↓-to-fx-upbnd'
where
↓-to-fx-upbnd' : Σ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ x) holds
→ (β b ≤ f x) holds
↓-to-fx-upbnd' (a' , o , r) =
transitivity-of L (β b) (f a') (f x)
(≤ᴮ-to-≤ (⌜ ≃-Lift 𝓤 (b ≤ᴮ f a') ⌝⁻¹ o))
(f-mono a' x r)
fx-is-least-upbnd : ((u , _) : upper-bound (ϕ ↓ x , β ∘ ↓-to-base ϕ x))
→ (f x ≤ u) holds
fx-is-least-upbnd (u , is-upbnd) =
(is-least-upper-boundᴮ (f x))
(u , λ z → is-upbnd (⌜ ↓ᴮf-equiv-↓-tot x ⌝ z))
H : (x : ⟨ L ⟩) → (Γ ϕ i) x ＝ f x
H x =
reindexing-along-equiv-＝-sup
L (id , id-is-equiv (ϕ ↓ x)) (β ∘ ↓-to-base ϕ x)
((Γ ϕ i) x) (f x) (sup-of-small-fam-is-lub L (β ∘ ↓-to-base ϕ x) (i x))
(G x)
ind-def-from-monotone-map : (f : ⟨ L ⟩ → ⟨ L ⟩)
→ is-monotone-endomap L f
→ 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)
ind-def-from-monotone-map f f-mono =
pr₁ (monotone-map-give-local-ind-def f f-mono)
local-from-monotone-map : (f : ⟨ L ⟩ → ⟨ L ⟩)
→ (f-mono : is-monotone-endomap L f)
→ is-local (ind-def-from-monotone-map f f-mono)
local-from-monotone-map f f-mono =
pr₁ (pr₂ (monotone-map-give-local-ind-def f f-mono))
local-ind-def-is-section-of-Γ : (f : ⟨ L ⟩ → ⟨ L ⟩)
→ (f-mono : is-monotone-endomap L f)
→ (x : ⟨ L ⟩)
→ (Γ (ind-def-from-monotone-map f f-mono)
(local-from-monotone-map f f-mono)) x
＝ f x
local-ind-def-is-section-of-Γ f f-mono =
pr₂ (pr₂ (monotone-map-give-local-ind-def f f-mono))
\end{code}
We now spell out the correspondence between small 'closed' subsets and
deflationary points in our sup-lattice. This will allow us to show that
monotone operators have a least fixed point under certain smallness
assumpions.
\begin{code}
module _
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
private
_≤_ = order-of L
⋁_ = join-of L
open Joins _≤_
open is-basis h
open local-inductive-definitions L β h
module correspondance-from-locally-small-ϕ
(ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
(i : is-local ϕ)
where
\end{code}
Next we give a name to the type of subsets of size 𝓥 (small) that are c-closed
and ϕ-closed (recall, that closure was initially defined for subsets with
respect to an arbitrary universe parameter 𝓣.)
\begin{code}
is-small-closed-subset : (P : 𝓟 {𝓥} B) → 𝓤 ⊔ (𝓥 ⁺) ̇
is-small-closed-subset P = ((U : 𝓟 {𝓥} B)
→ (U ⊆ P)
→ ((b : B)
→ b ≤ᴮ (⋁ 【 β , U 】)
→ b ∈ P))
× ((a : ⟨ L ⟩)
→ (b : B)
→ (b , a) ∈ ϕ
→ ((b' : B) → (b' ≤ᴮ a → b' ∈ P))
→ b ∈ P)
is-small-closed-subset-is-predicate : (P : 𝓟 {𝓥} B)
→ is-prop (is-small-closed-subset P)
is-small-closed-subset-is-predicate P =
×-is-prop (Π₄-is-prop fe (λ _ _ b _ → holds-is-prop (P b)))
(Π₄-is-prop fe (λ _ b _ _ → holds-is-prop (P b)))
small-closed-subsets : 𝓤 ⊔ (𝓥 ⁺) ̇
small-closed-subsets = Σ P ꞉ 𝓟 {𝓥} B , is-small-closed-subset P
subset-of-small-closed-subset : small-closed-subsets → 𝓟 {𝓥} B
subset-of-small-closed-subset (P , c-clsd , ϕ-clsd) = P
c-closed-of-small-closed-subset : (X : small-closed-subsets)
→ ((U : 𝓟 {𝓥} B)
→ U ⊆ subset-of-small-closed-subset X
→ ((b : B)
→ b ≤ᴮ (⋁ 【 β , U 】)
→ b ∈ subset-of-small-closed-subset X))
c-closed-of-small-closed-subset (P , c-clsd , ϕ-clsd) = c-clsd
ϕ-closed-of-small-closed-subset : (X : small-closed-subsets)
→ ((a : ⟨ L ⟩)
→ (b : B)
→ ((b , a) ∈ ϕ)
→ ((b' : B)
→ (b' ≤ᴮ a
→ b' ∈ subset-of-small-closed-subset X))
→ b ∈ subset-of-small-closed-subset X)
ϕ-closed-of-small-closed-subset (P , c-clsd , ϕ-clsd) = ϕ-clsd
is-deflationary : (a : ⟨ L ⟩) → 𝓣 ̇
is-deflationary a = ((Γ ϕ i) a ≤ a) holds
is-deflationary-is-predicate : (a : ⟨ L ⟩) → is-prop (is-deflationary a)
is-deflationary-is-predicate a = holds-is-prop ((Γ ϕ i) a ≤ a)
deflationary-points : 𝓤 ⊔ 𝓣 ̇
deflationary-points = Σ a ꞉ ⟨ L ⟩ , (is-deflationary a)
point-def-points : deflationary-points → ⟨ L ⟩
point-def-points (a , _) = a
is-deflationary-def-points : (X : deflationary-points)
→ is-deflationary (point-def-points X)
is-deflationary-def-points (_ , dp) = dp
small-closed-subsets-to-def-points : small-closed-subsets
→ deflationary-points
small-closed-subsets-to-def-points (P , c-closed , ϕ-closed) =
(sup-of-P , sup-is-def)
where
sup-of-P : ⟨ L ⟩
sup-of-P = ⋁ 【 β , P 】
sup-is-def : is-deflationary sup-of-P
sup-is-def = lub-condition (sup-of-P , is-upper-bound)
where
sup-is-lub :
((Γ ϕ i) sup-of-P is-lub-of (ϕ ↓ sup-of-P , β ∘ ↓-to-base ϕ sup-of-P))
holds
sup-is-lub =
sup-of-small-fam-is-lub L (β ∘ ↓-to-base ϕ sup-of-P) (i sup-of-P)
lub-condition :
((u , _) : upper-bound (ϕ ↓ sup-of-P , β ∘ ↓-to-base ϕ sup-of-P))
→ ((Γ ϕ i) sup-of-P ≤ u) holds
lub-condition = pr₂ sup-is-lub
b-in-P-to-b-below-sup : (b : B) → b ∈ P → (β b ≤ sup-of-P) holds
b-in-P-to-b-below-sup b b-in-P =
(join-is-upper-bound-of L 【 β , P 】) (b , b-in-P)
un-trunc-map : (b : B)
→ Σ a ꞉ ⟨ L ⟩ , (b , a) ∈ ϕ × (a ≤ sup-of-P) holds
→ (β b ≤ sup-of-P) holds
un-trunc-map b (a , p , o) =
b-in-P-to-b-below-sup b (ϕ-closed a b p (ϕ-hypothesis))
where
ϕ-hypothesis : (b' : B) → b' ≤ᴮ a → b' ∈ P
ϕ-hypothesis b' r = c-closed P (λ x → id) b' b'-below-sup-P
where
b'-below-sup-P : b' ≤ᴮ sup-of-P
b'-below-sup-P =
≤-to-≤ᴮ (transitivity-of L (β b') a sup-of-P (≤ᴮ-to-≤ r) o)
is-upper-bound : ((b , e) : ϕ ↓ sup-of-P) → (β b ≤ sup-of-P) holds
is-upper-bound (b , e) =
∥∥-rec (holds-is-prop (β b ≤ sup-of-P)) (un-trunc-map b) e
def-points-to-small-closed-subsets : deflationary-points
→ small-closed-subsets
def-points-to-small-closed-subsets (a , is-def) =
(Q a , c-closed , ϕ-closed)
where
Q : (x : ⟨ L ⟩) → 𝓟 {𝓥} B
Q x b = (b ≤ᴮ x , ≤ᴮ-is-prop-valued)
sup-Q_ : (x : ⟨ L ⟩) → ⟨ L ⟩
sup-Q x = ⋁ 【 β , Q x 】
_is-sup-Q : (x : ⟨ L ⟩) → x ＝ sup-Q x
x is-sup-Q = is-supᴮ' x
c-closed : (U : 𝓟 {𝓥} B)
→ (U ⊆ Q a)
→ ((b : B) → (b ≤ᴮ (⋁ 【 β , U 】)) → b ∈ Q a)
c-closed U C b o =
≤-to-≤ᴮ (transitivity-of L (β b) (⋁ 【 β , U 】) a (≤ᴮ-to-≤ o)
(transport (λ - → ((⋁ 【 β , U 】) ≤ -) holds)
(a is-sup-Q ⁻¹)
(joins-preserve-containment
L β {U} {Q a} C)))
ϕ-closed : (a' : ⟨ L ⟩)
→ (b : B)
→ ((b , a') ∈ ϕ)
→ ((b' : B) → (b' ≤ᴮ a' → b' ∈ Q a)) → b ∈ Q a
ϕ-closed a' b p f = trunc-map b ∣ (a' , p , a'-below-a) ∣
where
Γ-is-sup : ((Γ ϕ i) a is-lub-of (ϕ ↓ a , β ∘ ↓-to-base ϕ a)) holds
Γ-is-sup = sup-of-small-fam-is-lub L (β ∘ ↓-to-base ϕ a) (i a)
Γ-an-upper-bound :
((Γ ϕ i) a is-an-upper-bound-of (ϕ ↓ a , β ∘ ↓-to-base ϕ a)) holds
Γ-an-upper-bound = pr₁ Γ-is-sup
trunc-map : (x : B)
→ (Ǝ a'' ꞉ ⟨ L ⟩ , (x , a'') ∈ ϕ × (a'' ≤ a) holds) holds
→ x ≤ᴮ a
trunc-map x e = ≤-to-≤ᴮ (transitivity-of L (β x) ((Γ ϕ i) a) a
(Γ-an-upper-bound (x , e))
(is-def))
a'-below-a : (a' ≤ a) holds
a'-below-a =
transport (λ - → (- ≤ a) holds) (a' is-sup-Q ⁻¹)
(transport (λ - → ((sup-Q a') ≤ -) holds)
(a is-sup-Q ⁻¹)
(joins-preserve-containment L β {Q a'} {Q a} f))
small-closed-subsets-≃-def-points :
small-closed-subsets ≃ deflationary-points
small-closed-subsets-≃-def-points =
(small-closed-subsets-to-def-points ,
qinvs-are-equivs small-closed-subsets-to-def-points is-qinv)
where
H : def-points-to-small-closed-subsets
∘ small-closed-subsets-to-def-points ∼ id
H (P , c-closed , ϕ-closed) =
to-subtype-＝ is-small-closed-subset-is-predicate P'-is-P
where
sup-P : ⟨ L ⟩
sup-P = point-def-points
(small-closed-subsets-to-def-points
(P , c-closed , ϕ-closed))
P' : 𝓟 {𝓥} B
P' = subset-of-small-closed-subset
(def-points-to-small-closed-subsets
(small-closed-subsets-to-def-points
(P , c-closed , ϕ-closed)))
P'-is-P : P' ＝ P
P'-is-P = dfunext fe P'-htpy-P
where
P'-htpy-P : P' ∼ P
P'-htpy-P x =
to-Ω-＝ fe
(pe ≤ᴮ-is-prop-valued (holds-is-prop (P x)) P'-to-P P-to-P')
where
P'-to-P : x ≤ᴮ sup-P → x ∈ P
P'-to-P = c-closed P (λ _ → id) x
P-to-P' : x ∈ P → x ≤ᴮ sup-P
P-to-P' r =
≤-to-≤ᴮ ((join-is-upper-bound-of L 【 β , P 】) (x , r))
G : small-closed-subsets-to-def-points
∘ def-points-to-small-closed-subsets ∼ id
G (a , is-def) = to-subtype-＝ is-deflationary-is-predicate sup-P-is-a
where
P : 𝓟 {𝓥} B
P = subset-of-small-closed-subset
(def-points-to-small-closed-subsets (a , is-def))
sup-P : ⟨ L ⟩
sup-P = point-def-points
(small-closed-subsets-to-def-points
(def-points-to-small-closed-subsets (a , is-def)))
sup-P-is-a : sup-P ＝ a
sup-P-is-a = is-supᴮ' a ⁻¹
is-qinv : qinv small-closed-subsets-to-def-points
is-qinv = (def-points-to-small-closed-subsets , H , G)
\end{code}
Using the previously displayed correspondance we can show that, under certain
smallness assumptions on the least closed subset 𝓘nd ϕ, the monotone operator
Γ ϕ has a least fixed point.
\begin{code}
module small-𝓘nd-from-exists
(ind-e : inductively-generated-subset-exists L β h ϕ)
where
open inductively-generated-subset-exists ind-e
open trunc-ind-def L β h ϕ ind-e
module smallness-assumption (j : (b : B) → (b ∈ 𝓘nd) is 𝓥 small) where
private
𝓘' : (b : B) → 𝓥 ̇
𝓘' b = (resized (b ∈ 𝓘nd)) (j b)
𝓘'-equiv-𝓘nd : (b : B) → 𝓘' b ≃ b ∈ 𝓘nd
𝓘'-equiv-𝓘nd b = resizing-condition (j b)
𝓘'-to-𝓘nd : (b : B) → 𝓘' b → b ∈ 𝓘nd
𝓘'-to-𝓘nd b = ⌜ 𝓘'-equiv-𝓘nd b ⌝
𝓘nd-to-𝓘' : (b : B) → b ∈ 𝓘nd → 𝓘' b
𝓘nd-to-𝓘' b = ⌜ 𝓘'-equiv-𝓘nd b ⌝⁻¹
𝓘'-is-prop-valued : {b : B} → is-prop (𝓘' b)
𝓘'-is-prop-valued {b} = equiv-to-prop (𝓘'-equiv-𝓘nd b) (Ind-trunc b)
𝓘'-subset : 𝓟 {𝓥} B
𝓘'-subset = λ b → (𝓘' b , 𝓘'-is-prop-valued)
𝓘'-is-c-closed : (U : 𝓟 {𝓥} B)
→ U ⊆ 𝓘'-subset
→ (b : B) → b ≤ᴮ (⋁ 【 β , U 】)
→ b ∈ 𝓘'-subset
𝓘'-is-c-closed U C b o =
𝓘nd-to-𝓘' b (𝓘nd-is-c-closed U (λ x → 𝓘'-to-𝓘nd x ∘ C x) b o)
𝓘'-is-ϕ-closed : (a : ⟨ L ⟩)
→ (b : B)
→ (b , a) ∈ ϕ
→ ((b' : B) → b' ≤ᴮ a → b' ∈ 𝓘'-subset)
→ b ∈ 𝓘'-subset
𝓘'-is-ϕ-closed a b p f =
𝓘nd-to-𝓘' b (𝓘nd-is-ϕ-closed a b p (λ b' → 𝓘'-to-𝓘nd b' ∘ f b'))
total-space-𝓘-is-small : (𝕋 𝓘nd) is 𝓥 small
total-space-𝓘-is-small = (𝕋 𝓘'-subset , Σ-cong λ b → 𝓘'-equiv-𝓘nd b)
e : 𝕋 𝓘'-subset ≃ 𝕋 𝓘nd
e = resizing-condition total-space-𝓘-is-small
sup-𝓘 : ⟨ L ⟩
sup-𝓘 = ⋁ (𝕋 𝓘'-subset , β ∘ 𝕋-to-carrier 𝓘nd ∘ ⌜ e ⌝)
sup-𝓘-is-lub : (sup-𝓘 is-lub-of 【 β , 𝓘nd 】) holds
sup-𝓘-is-lub = sup-of-small-fam-is-lub L (β ∘ 𝕋-to-carrier 𝓘nd)
total-space-𝓘-is-small
sup-𝓘-is-fixed-point : (Γ ϕ i) sup-𝓘 ＝ sup-𝓘
sup-𝓘-is-fixed-point = antisymmetry-of L Γ-sup-below-sup sup-below-Γ-sup
where
Γ-sup-below-sup : ((Γ ϕ i) sup-𝓘 ≤ sup-𝓘) holds
Γ-sup-below-sup = is-deflationary-def-points
(small-closed-subsets-to-def-points
(𝓘'-subset , 𝓘'-is-c-closed , 𝓘'-is-ϕ-closed))
sup-below-Γ-sup : (sup-𝓘 ≤ (Γ ϕ i) sup-𝓘) holds
sup-below-Γ-sup = transport (λ - → (sup-𝓘 ≤ -) holds)
sup-Q-is-Γ-sup sup-𝓘-below-sup-Q
where
Γ-Γ-sup-below-Γ-sup : ((Γ ϕ i) ((Γ ϕ i) sup-𝓘) ≤ (Γ ϕ i) sup-𝓘) holds
Γ-Γ-sup-below-Γ-sup =
Γ-is-monotone ϕ i ((Γ ϕ i) sup-𝓘) sup-𝓘 Γ-sup-below-sup
Q-Γ-sup : 𝓟 {𝓥} B
Q-Γ-sup = subset-of-small-closed-subset
(def-points-to-small-closed-subsets
((Γ ϕ i) sup-𝓘 , Γ-Γ-sup-below-Γ-sup))
Q-is-c-closed : (U : 𝓟 {𝓥} B)
→ (U ⊆ Q-Γ-sup)
→ ((b : B)
→ b ≤ᴮ (⋁ 【 β , U 】)
→ b ∈ Q-Γ-sup)
Q-is-c-closed =
c-closed-of-small-closed-subset
(def-points-to-small-closed-subsets
((Γ ϕ i) sup-𝓘 , Γ-Γ-sup-below-Γ-sup))
Q-is-ϕ-closed : (a' : ⟨ L ⟩)
→ (b : B)
→ ((b , a') ∈ ϕ)
→ ((b' : B)
→ (b' ≤ᴮ a' → b' ∈ Q-Γ-sup))
→ b ∈ Q-Γ-sup
Q-is-ϕ-closed = ϕ-closed-of-small-closed-subset
(def-points-to-small-closed-subsets
((Γ ϕ i) sup-𝓘 , Γ-Γ-sup-below-Γ-sup))
𝓘nd-contained-Q-Γ-sup : 𝓘nd ⊆ Q-Γ-sup
𝓘nd-contained-Q-Γ-sup =
𝓘nd-is-initial Q-Γ-sup Q-is-c-closed Q-is-ϕ-closed
𝓘-is-small-subset-contained-Q-Γ-sup : 𝓘'-subset ⊆ Q-Γ-sup
𝓘-is-small-subset-contained-Q-Γ-sup =
(λ z → 𝓘nd-contained-Q-Γ-sup z ∘ 𝓘'-to-𝓘nd z)
sup-Q : ⟨ L ⟩
sup-Q = ⋁ 【 β , Q-Γ-sup 】
sup-𝓘-below-sup-Q : (sup-𝓘 ≤ sup-Q) holds
sup-𝓘-below-sup-Q =
joins-preserve-containment L β {𝓘'-subset} {Q-Γ-sup}
𝓘-is-small-subset-contained-Q-Γ-sup
sup-Q-is-Γ-sup : sup-Q ＝ (Γ ϕ i) sup-𝓘
sup-Q-is-Γ-sup = is-supᴮ' ((Γ ϕ i) sup-𝓘) ⁻¹
sup-𝓘-is-least-fixed-point : (a : ⟨ L ⟩)
→ (Γ ϕ i) a ＝ a
→ (sup-𝓘 ≤⟨ L ⟩ a) holds
sup-𝓘-is-least-fixed-point a p = transport (λ - → (sup-𝓘 ≤ -) holds)
sup-P-is-a
sup-𝓘-below-sup-P
where
Γa-below-a : ((Γ ϕ i) a ≤ a) holds
Γa-below-a = transport (λ - → ((Γ ϕ i) a ≤ -) holds)
p (reflexivity-of L ((Γ ϕ i) a))
P-a : 𝓟 {𝓥} B
P-a = subset-of-small-closed-subset
(def-points-to-small-closed-subsets (a , Γa-below-a))
P-is-c-closed : (U : 𝓟 {𝓥} B)
→ (U ⊆ P-a)
→ ((b : B)
→ b ≤ᴮ (⋁ 【 β , U 】)
→ b ∈ P-a)
P-is-c-closed = c-closed-of-small-closed-subset
(def-points-to-small-closed-subsets
(a , Γa-below-a))
P-is-ϕ-closed : (a' : ⟨ L ⟩)
→ (b : B)
→ ((b , a') ∈ ϕ)
→ ((b' : B)
→ (b' ≤ᴮ a' → b' ∈ P-a))
→ b ∈ P-a
P-is-ϕ-closed = ϕ-closed-of-small-closed-subset
(def-points-to-small-closed-subsets
(a , Γa-below-a))
𝓘nd-contained-P-a : 𝓘nd ⊆ P-a
𝓘nd-contained-P-a = 𝓘nd-is-initial P-a P-is-c-closed P-is-ϕ-closed
𝓘'-subset-contained-P-a : 𝓘'-subset ⊆ P-a
𝓘'-subset-contained-P-a = λ z → 𝓘nd-contained-P-a z ∘ 𝓘'-to-𝓘nd z
sup-P : ⟨ L ⟩
sup-P = ⋁ 【 β , P-a 】
sup-𝓘-below-sup-P : (sup-𝓘 ≤ sup-P) holds
sup-𝓘-below-sup-P =
joins-preserve-containment L β {𝓘'-subset} {P-a}
𝓘'-subset-contained-P-a
sup-P-is-a : sup-P ＝ a
sup-P-is-a = is-supᴮ' a ⁻¹
Γ-has-least-fixed-point : has-least-fixed-point L (Γ ϕ i)
Γ-has-least-fixed-point =
(sup-𝓘 , sup-𝓘-is-fixed-point , sup-𝓘-is-least-fixed-point)
where
sup-𝓘-below : (a : ⟨ L ⟩) → ((Γ ϕ i) a ＝ a) → (sup-𝓘 ≤ a) holds
sup-𝓘-below a p = transport (λ - → (sup-𝓘 ≤ -) holds)
sup-P-is-a
sup-𝓘-below-sup-P
where
Γa-below-a : ((Γ ϕ i) a ≤ a) holds
Γa-below-a = transport (λ - → ((Γ ϕ i) a ≤ -) holds)
p (reflexivity-of L ((Γ ϕ i) a))
P-a : 𝓟 {𝓥} B
P-a = subset-of-small-closed-subset
(def-points-to-small-closed-subsets (a , Γa-below-a))
P-is-c-closed : (U : 𝓟 {𝓥} B)
→ (U ⊆ P-a)
→ ((b : B)
→ b ≤ᴮ (⋁ 【 β , U 】)
→ b ∈ P-a)
P-is-c-closed = c-closed-of-small-closed-subset
(def-points-to-small-closed-subsets
(a , Γa-below-a))
P-is-ϕ-closed : (a' : ⟨ L ⟩)
→ (b : B)
→ ((b , a') ∈ ϕ)
→ ((b' : B)
→ (b' ≤ᴮ a' → b' ∈ P-a))
→ b ∈ P-a
P-is-ϕ-closed = ϕ-closed-of-small-closed-subset
(def-points-to-small-closed-subsets
(a , Γa-below-a))
𝓘nd-contained-P-a : 𝓘nd ⊆ P-a
𝓘nd-contained-P-a = 𝓘nd-is-initial P-a P-is-c-closed P-is-ϕ-closed
𝓘'-subset-contained-P-a : 𝓘'-subset ⊆ P-a
𝓘'-subset-contained-P-a = λ z → 𝓘nd-contained-P-a z ∘ 𝓘'-to-𝓘nd z
sup-P : ⟨ L ⟩
sup-P = ⋁ 【 β , P-a 】
sup-𝓘-below-sup-P : (sup-𝓘 ≤ sup-P) holds
sup-𝓘-below-sup-P =
joins-preserve-containment L β {𝓘'-subset} {P-a}
𝓘'-subset-contained-P-a
sup-P-is-a : sup-P ＝ a
sup-P-is-a = is-supᴮ' a ⁻¹
\end{code}
The remainder of this formalization is essentially a search for restrictions
we may impose on sup-lattices and inductive definitions to achieve the
neccesary smallness assumptions on 𝓘nd which will guarentee least fixed points.
We now consider a boundedness restricion on inductive definitions and show
that bounded inductive definitions are local.
An inductive definition is bounded if there is a small indexed family of
types that can be substituted for elements a : L in a sense to be made
precise below.
\begin{code}
module bounded-inductive-definitions
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
private
_≤_ = order-of L
⋁_ = join-of L
open Joins _≤_
open local-inductive-definitions L β h
open is-basis h
_is-a-small-cover-of_ : (X : 𝓥 ̇) → (Y : 𝓦 ̇) → 𝓥 ⊔ 𝓦 ̇
X is-a-small-cover-of Y = X ↠ Y
has-a-bound : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)) → 𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ̇
has-a-bound ϕ = Σ I ꞉ 𝓥 ̇ , Σ α ꞉ (I → 𝓥 ̇) ,
((a : ⟨ L ⟩)
→ (b : B)
→ (b , a) ∈ ϕ
→ (Ǝ i ꞉ I , α i is-a-small-cover-of ↓ᴮ L β a) holds)
bound-index : {ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)} → has-a-bound ϕ → 𝓥 ̇
bound-index (I , α , covering) = I
bound-family : {ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)}
→ (bnd : has-a-bound ϕ)
→ (bound-index {ϕ} bnd → 𝓥 ̇)
bound-family (I , α , covering) = α
covering-condition : {ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)}
→ (bnd : has-a-bound ϕ)
→ ((a : ⟨ L ⟩)
→ (b : B)
→ (b , a) ∈ ϕ
→ (Ǝ i ꞉ (bound-index {ϕ} bnd) ,
((bound-family {ϕ} bnd) i is-a-small-cover-of ↓ᴮ L β a))
holds)
covering-condition (I , α , covering) = covering
is-bounded : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)) → 𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ̇
is-bounded ϕ = ((a : ⟨ L ⟩) → (b : B) → ((b , a) ∈ ϕ) is 𝓥 small)
× (has-a-bound ϕ)
bounded-implies-local : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
→ is-bounded ϕ
→ is-local ϕ
bounded-implies-local ϕ (ϕ-small , ϕ-has-bound) a =
smallness-closed-under-≃ S₀-is-small S₀-equiv-↓
where
I : 𝓥 ̇
I = bound-index {ϕ} ϕ-has-bound
α : I → 𝓥 ̇
α = bound-family {ϕ} ϕ-has-bound
cov : (a : ⟨ L ⟩)
→ (b : B)
→ (b , a) ∈ ϕ
→ (Ǝ i ꞉ I , (α i is-a-small-cover-of ↓ᴮ L β a)) holds
cov = covering-condition {ϕ} ϕ-has-bound
S₀ : 𝓤 ⊔ 𝓣 ⊔ 𝓥 ̇
S₀ = Σ b ꞉ B , (Ǝ i ꞉ I , (Σ m ꞉ (α i → ↓ᴮ L β a) ,
(b , ⋁ (α i , ↓ᴮ-inclusion L β a ∘ m)) ∈ ϕ)) holds
S₀-is-small : S₀ is 𝓥 small
S₀-is-small =
Σ-is-small
(B , ≃-refl B)
(λ b → ∥∥-is-small pt
(Σ-is-small (I , ≃-refl I)
(λ i → Σ-is-small
(Π-is-small fe' (α i , ≃-refl (α i))
(λ _ → ↓ᴮ-is-small))
(λ m → ϕ-small (⋁ (α i , ↓ᴮ-inclusion L β a ∘ m)) b))))
S₀-to-↓ : S₀ → ϕ ↓ a
S₀-to-↓ (b , e) = (b , ∥∥-functor u e)
where
u : Σ i ꞉ I , Σ m ꞉ (α i → ↓ᴮ L β a) ,
(b , (⋁ (α i , ↓ᴮ-inclusion L β a ∘ m))) ∈ ϕ
→ Σ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ a) holds
u (i , m , p) =
(⋁ (α i , ↓ᴮ-inclusion L β a ∘ m) , p ,
join-is-least-upper-bound-of L (α i , ↓ᴮ-inclusion L β a ∘ m)
(a , λ z → is-upper-bound-↓ a (m z)))
↓-to-S₀ : ϕ ↓ a → S₀
↓-to-S₀ (b , e) = (b , t e)
where
g : (a' : ⟨ L ⟩)
→ (b , a') ∈ ϕ
→ (a' ≤ a) holds
→ Σ i ꞉ I , (α i is-a-small-cover-of ↓ᴮ L β a')
→ Σ i ꞉ I , (Σ m ꞉ (α i → ↓ᴮ L β a) ,
(b , ⋁ (α i , ↓ᴮ-inclusion L β a ∘ m)) ∈ ϕ)
g a' p o (i , α-covers) = (i , m , in-ϕ)
where
inclusion : (a' : ⟨ L ⟩) → (a' ≤ a) holds → ↓ᴮ L β a' → ↓ᴮ L β a
inclusion a' o (x , r) = (x , transitivity-of L (β x) a' a r o)
m : α i → ↓ᴮ L β a
m = inclusion a' o ∘ ⌞ α-covers ⌟
path : a' ＝ ⋁ (α i , ↓ᴮ-inclusion L β a ∘ m)
path = reindexing-along-surj-＝-sup
L α-covers (β ∘ pr₁)
a' (⋁ (α i , ↓ᴮ-inclusion L β a ∘ m)) (↓-is-sup a')
(join-is-lub-of L (α i , ↓ᴮ-inclusion L β a ∘ m))
in-ϕ : (b , ⋁ (α i , ↓ᴮ-inclusion L β a ∘ m)) ∈ ϕ
in-ϕ = transport (λ z → (b , z) ∈ ϕ) path p
trunc-g : (a' : ⟨ L ⟩)
→ (b , a') ∈ ϕ
→ (a' ≤ a) holds
→ (Ǝ i ꞉ I , (α i is-a-small-cover-of ↓ᴮ L β a')) holds
→ (Ǝ i ꞉ I , (Σ m ꞉ (α i → ↓ᴮ L β a) ,
(b , ⋁ (α i , ↓ᴮ-inclusion L β a ∘ m)) ∈ ϕ)) holds
trunc-g a' p o = ∥∥-functor (g a' p o)
cur-trunc-g : Σ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ a) holds
→ (Ǝ i ꞉ I , Σ m ꞉ (α i → ↓ᴮ L β a)
, (b , ⋁ (α i , ↓ᴮ-inclusion L β a ∘ m)) ∈ ϕ) holds
cur-trunc-g (a' , p , o) = trunc-g a' p o (cov a' b p)
t : (Ǝ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ a) holds) holds
→ (Ǝ i ꞉ I , Σ m ꞉ (α i → ↓ᴮ L β a) ,
(b , ⋁ (α i , ↓ᴮ-inclusion L β a ∘ m)) ∈ ϕ) holds
t = ∥∥-rec ∥∥-is-prop cur-trunc-g
S₀-equiv-↓ : S₀ ≃ ϕ ↓ a
S₀-equiv-↓ = (S₀-to-↓ , qinvs-are-equivs S₀-to-↓ is-qinv)
where
H : ↓-to-S₀ ∘ S₀-to-↓ ∼ id
H (b , e) = to-subtype-＝ (λ _ → ∥∥-is-prop) refl
G : S₀-to-↓ ∘ ↓-to-S₀ ∼ id
G (b , e) = to-subtype-＝ (λ _ → ∥∥-is-prop) refl
is-qinv : qinv S₀-to-↓
is-qinv = (↓-to-S₀ , H , G)
\end{code}
We now consider a presentation restriction on sup-lattices stronger than
having a basis.
A sup-lattice has a small presentation if there is a small indexed family of
subsets that can be substituted for arbitrary subsets in a sense to be made
precise below.
\begin{code}
module small-presentation-of-lattice
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
private
_≤_ = order-of L
⋁_ = join-of L
open Joins _≤_
open PropositionalTruncation pt
open is-basis h
_is-a-small-presentation :
Σ J ꞉ 𝓥 ̇ , (J → 𝓟 {𝓥} B) × 𝓟 {𝓥} (B × 𝓟 {𝓥} B) → (𝓥 ⁺) ̇
(J , Y , R) is-a-small-presentation = (b : B)
→ (X : 𝓟 {𝓥} B)
→ b ≤ᴮ (⋁ 【 β , X 】)
≃ ((Ǝ j ꞉ J , Y j ⊆ X × (b , Y j) ∈ R)
holds)
has-small-presentation : (𝓥 ⁺) ̇
has-small-presentation =
Σ 𝓡 ꞉ Σ J ꞉ 𝓥 ̇ , (J → 𝓟 {𝓥} B) × 𝓟 {𝓥} (B × 𝓟 {𝓥} B)
, 𝓡 is-a-small-presentation
\end{code}
We will now define, in the context of bounded ϕ and small-presentation 𝓡, a
new QIT family that is equivalent to 𝓘nd. Our constructors should be familiar
but notice the bounded and small-presentation assumptions allow us to avoid
large quantification!
\begin{code}
module _
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
private
_≤_ = order-of L
⋁_ = join-of L
open bounded-inductive-definitions L β h
open small-presentation-of-lattice L β h
open is-basis h
module small-QIT-from-bounded-and-small-presentation
(small-pres : has-small-presentation)
(ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
(bnd : is-bounded ϕ)
where
I₁ : 𝓥 ̇
I₁ = pr₁ (pr₁ small-pres)
Y : I₁ → 𝓟 {𝓥} B
Y = pr₁ (pr₂ (pr₁ small-pres))
R : 𝓟 {𝓥} (B × 𝓟 {𝓥} B)
R = pr₂ (pr₂ (pr₁ small-pres))
is-small-pres : (I₁ , Y , R) is-a-small-presentation
is-small-pres = pr₂ small-pres
is-small-pres-forward : (b : B)
→ (X : 𝓟 {𝓥} B)
→ b ≤ᴮ (⋁ 【 β , X 】)
→ ((Ǝ j ꞉ I₁ , Y j ⊆ X × (b , Y j) ∈ R) holds)
is-small-pres-forward b X = ⌜ is-small-pres b X ⌝
is-small-pres-backward : (b : B)
→ (X : 𝓟 {𝓥} B)
→ ((Ǝ j ꞉ I₁ , Y j ⊆ X × (b , Y j) ∈ R) holds)
→ b ≤ᴮ (⋁ 【 β , X 】)
is-small-pres-backward b X = ⌜ is-small-pres b X ⌝⁻¹
ϕ-is-small : (a : ⟨ L ⟩) → (b : B) → ((b , a) ∈ ϕ) is 𝓥 small
ϕ-is-small = pr₁ bnd
small-ϕ : (b : B) → (a : ⟨ L ⟩) → 𝓥 ̇
small-ϕ b a = pr₁ (ϕ-is-small a b)
small-ϕ-equiv-ϕ : (a : ⟨ L ⟩) → (b : B) → small-ϕ b a ≃ (b , a) ∈ ϕ
small-ϕ-equiv-ϕ a b = pr₂ (ϕ-is-small a b)
ϕ-is-small-forward : (a : ⟨ L ⟩) → (b : B) → small-ϕ b a → (b , a) ∈ ϕ
ϕ-is-small-forward a b = ⌜ small-ϕ-equiv-ϕ a b ⌝
ϕ-is-small-backward : (a : ⟨ L ⟩) → (b : B) → (b , a) ∈ ϕ → small-ϕ b a
ϕ-is-small-backward a b = ⌜ small-ϕ-equiv-ϕ a b ⌝⁻¹
I₂ : 𝓥 ̇
I₂ = pr₁ (pr₂ bnd)
α : I₂ → 𝓥 ̇
α = pr₁ (pr₂ (pr₂ bnd))
cover-condition : ((a : ⟨ L ⟩)
→ (b : B)
→ (b , a) ∈ ϕ
→ (Ǝ i ꞉ I₂ , α i is-a-small-cover-of ↓ᴮ L β a) holds)
cover-condition = pr₂ (pr₂ (pr₂ bnd))
\end{code}
The following serves as evidence that the desired QIT family is small (and
atleast has strictly positive point constructors).
\begin{code}
data Small-Ind-Check : B → 𝓥 ̇ where
Small-c-cl' : (i : I₁)
→ ((b : B) → (b ∈ Y i → Small-Ind-Check b))
→ (b : B) → (b , Y i) ∈ R
→ Small-Ind-Check b
Small-ϕ-cl' : (i : I₂)
→ (m : α i → B)
→ (b : B)
→ small-ϕ b (⋁ (α i , β ∘ m))
→ ((b' : B) → (b' ≤ᴮ (⋁ (α i , β ∘ m)) → Small-Ind-Check b'))
→ Small-Ind-Check b
\end{code}
Again, we use records to assert the existence of another QIT family with
apropriate 'intiality' principle. As before we will first introduce some
names for the closure properties.
\begin{code}
Small-c-closure : {𝓦 : Universe} (S : 𝓟 {𝓦} B) → 𝓥 ⊔ 𝓦 ̇
Small-c-closure S = (i : I₁)
→ ((b : B) → (b ∈ Y i → b ∈ S))
→ (b : B) → (b , Y i) ∈ R
→ b ∈ S
Small-ϕ-closure : {𝓦 : Universe} (S : 𝓟 {𝓦} B) → 𝓥 ⊔ 𝓦 ̇
Small-ϕ-closure S = (i : I₂)
→ (m : α i → B)
→ (b : B)
→ small-ϕ b (⋁ (α i , β ∘ m))
→ ((b' : B) → (b' ≤ᴮ (⋁ (α i , β ∘ m)) → b' ∈ S))
→ b ∈ S
record inductively-generated-small-subset-exists : 𝓤ω where
constructor
inductively-generated-small-subset
field
Small-Ind : B → 𝓥 ̇
Small-Ind-trunc : (b : B) → is-prop (Small-Ind b)
private
Small-𝓘 : 𝓟 {𝓥} B
Small-𝓘 b = (Small-Ind b , Small-Ind-trunc b)
field
Small-c-cl : Small-c-closure Small-𝓘
Small-ϕ-cl : Small-ϕ-closure Small-𝓘
Small-Ind-Initial : (P : 𝓟 {𝓦} B)
→ Small-c-closure P
→ Small-ϕ-closure P
→ Small-𝓘 ⊆ P
module small-trunc-ind-def
(ind-e : inductively-generated-small-subset-exists)
where
open inductively-generated-small-subset-exists ind-e
Small-𝓘nd : 𝓟 {𝓥} B
Small-𝓘nd b = (Small-Ind b , Small-Ind-trunc b)
Small-𝓘nd-is-c-cl : Small-c-closure Small-𝓘nd
Small-𝓘nd-is-c-cl = Small-c-cl
Small-𝓘nd-is-ϕ-cl : Small-ϕ-closure Small-𝓘nd
Small-𝓘nd-is-ϕ-cl = Small-ϕ-cl
Small-𝓘nd-Initial : (P : 𝓟 {𝓦} B)
→ Small-c-closure P
→ Small-ϕ-closure P
→ Small-𝓘nd ⊆ P
Small-𝓘nd-Initial = Small-Ind-Initial
\end{code}
We will now show that under the assumptions of small presentation and bounded
ϕ that
b ∈ Small-𝓘nd ≃ b ∈ 𝓘nd.
We make essential use of the initiality of both types here.
This will allow us to satisfy the smallness conditions needed to salvage the
least fixed point theorem.
\begin{code}
module _
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
private
_≤_ = order-of L
⋁_ = join-of L
open bounded-inductive-definitions L β h
open small-presentation-of-lattice L β h
open is-basis h
module 𝓘nd-is-small-from-bounded-and-small-presentation
(small-pres : has-small-presentation)
(ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
(bnd : is-bounded ϕ)
where
open small-QIT-from-bounded-and-small-presentation L β h small-pres ϕ bnd
module 𝓘nd-is-small-QITs-exists
(ind-e : inductively-generated-subset-exists L β h ϕ)
(ind-e' : inductively-generated-small-subset-exists)
where
open trunc-ind-def L β h ϕ ind-e
open small-trunc-ind-def ind-e'
𝓘nd-⊆-Small-𝓘nd : 𝓘nd ⊆ Small-𝓘nd
𝓘nd-⊆-Small-𝓘nd = 𝓘nd-is-initial Small-𝓘nd is-c-cl is-ϕ-cl
where
is-c-cl : (U : 𝓟 {𝓥} B)
→ U ⊆ Small-𝓘nd
→ (b : B)
→ b ≤ᴮ (⋁ 【 β , U 】)
→ b ∈ Small-𝓘nd
is-c-cl U C b o = trunc-u (is-small-pres-forward b U o)
where
u : (Σ j ꞉ I₁ , Y j ⊆ U × (b , Y j) ∈ R)
→ b ∈ Small-𝓘nd
u (j , C' , r) = Small-𝓘nd-is-c-cl j (λ x → λ y → C x (C' x y)) b r
trunc-u : (Ǝ j ꞉ I₁ , Y j ⊆ U × (b , Y j) ∈ R) holds
→ b ∈ Small-𝓘nd
trunc-u = ∥∥-rec (holds-is-prop (Small-𝓘nd b)) u
is-ϕ-cl : (a : ⟨ L ⟩)
→ (b : B)
→ (b , a) ∈ ϕ
→ ((b' : B) → b' ≤ᴮ a → b' ∈ Small-𝓘nd)
→ b ∈ Small-𝓘nd
is-ϕ-cl a b p C = trunc-u (cover-condition a b p)
where
u : Σ i ꞉ I₂ , α i is-a-small-cover-of ↓ᴮ L β a → b ∈ Small-𝓘nd
u (i , s) =
Small-𝓘nd-is-ϕ-cl i (↓ᴮ-to-base L β a ∘ ⌞ s ⌟) b
(ϕ-is-small-backward (⋁ (α i , ↓ᴮ-inclusion L β a ∘ ⌞ s ⌟))
b (transport (λ - → (b , -) ∈ ϕ) (a-＝-⋁-α) p))
(λ b' → C b' ∘ (transport (λ - → b' ≤ᴮ -) (a-＝-⋁-α ⁻¹)))
where
a-＝-⋁-α : a ＝ ⋁ (α i , ↓ᴮ-inclusion L β a ∘ ⌞ s ⌟)
a-＝-⋁-α =
reindexing-along-surj-＝-sup
L s (↓ᴮ-inclusion L β a) a (⋁ (α i , ↓ᴮ-inclusion L β a ∘ ⌞ s ⌟))
(↓-is-sup a) (join-is-lub-of L (α i , ↓ᴮ-inclusion L β a ∘ ⌞ s ⌟))
trunc-u : (Ǝ i ꞉ I₂ , α i is-a-small-cover-of ↓ᴮ L β a) holds
→ b ∈ Small-𝓘nd
trunc-u = ∥∥-rec (holds-is-prop (Small-𝓘nd b)) u
Small-𝓘nd-⊆-𝓘nd : Small-𝓘nd ⊆ 𝓘nd
Small-𝓘nd-⊆-𝓘nd = Small-𝓘nd-Initial 𝓘nd is-small-c-cl is-small-ϕ-cl
where
is-small-c-cl : (i : I₁)
→ Y i ⊆ 𝓘nd
→ (b : B)
→ (b , Y i) ∈ R
→ b ∈ 𝓘nd
is-small-c-cl i C b r =
𝓘nd-is-c-closed (Y i) C b
(is-small-pres-backward b (Y i) ∣ (i , (λ _ → id) , r) ∣)
is-small-ϕ-cl : (i : I₂)
→ (m : α i → B)
→ (b : B)
→ small-ϕ b (⋁ (α i , β ∘ m))
→ ((x : B) → x ≤ᴮ (⋁ (α i , β ∘ m)) → x ∈ 𝓘nd)
→ b ∈ 𝓘nd
is-small-ϕ-cl i m b s C =
𝓘nd-is-ϕ-closed (⋁ (α i , β ∘ m)) b
(ϕ-is-small-forward (⋁ (α i , β ∘ m)) b s) C
𝓘nd-is-small : (b : B) → (b ∈ 𝓘nd) is 𝓥 small
𝓘nd-is-small b = (b ∈ Small-𝓘nd , small-𝓘nd-equiv-𝓘nd)
where
small-𝓘nd-equiv-𝓘nd : b ∈ Small-𝓘nd ≃ b ∈ 𝓘nd
small-𝓘nd-equiv-𝓘nd = logically-equivalent-props-are-equivalent
(holds-is-prop (Small-𝓘nd b))
(holds-is-prop (𝓘nd b))
(Small-𝓘nd-⊆-𝓘nd b)
(𝓘nd-⊆-Small-𝓘nd b)
\end{code}
As a corollary of the above result we get a predicative version of the least
fixed point theorem. Notice that we are assuming our sup-lattice is
small-presented and that we have a bounded ϕ that corresponds to our
monotone map. This is the most general statement that can be made but we are
actively exploring other, cleaner, formulations. In particular see the below
notion of density which makes no mention of a particular inductive definition.
Least fixed point theorem:
Given a 𝓥-sup-lattice L with a 𝓥-presentation and a monotone
endomap f : L → L. If there exists a bounded abstract inductive definition
ϕ such that f ＝ Γ ϕ, then f has a least fixed point.
\begin{code}
module _
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
private
_≤_ = order-of L
⋁_ = join-of L
open local-inductive-definitions L β h
open bounded-inductive-definitions L β h
open small-presentation-of-lattice L β h
open small-QIT-from-bounded-and-small-presentation L β h
module QITs-exists-for-all-ϕ
(ind-e : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
→ inductively-generated-subset-exists L β h ϕ)
(ind'-e : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
→ (bnd : is-bounded ϕ)
→ (small-pres : has-small-presentation)
→ inductively-generated-small-subset-exists small-pres ϕ bnd)
where
\end{code}
We first present the untruncated least fixed point theorem.
\begin{code}
Untruncated-Least-Fixed-Point-Theorem : (small-pres : has-small-presentation)
→ (f : ⟨ L ⟩ → ⟨ L ⟩)
→ (f-mono : is-monotone-endomap L f)
→ Σ ϕ ꞉ 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩) ,
Σ bnd ꞉ is-bounded ϕ , ((x : ⟨ L ⟩)
→ (Γ ϕ (bounded-implies-local ϕ bnd)) x
＝ f x)
→ has-least-fixed-point L f
Untruncated-Least-Fixed-Point-Theorem small-pres f f-mono (ϕ , bnd , H) =
transport (λ g → Σ x ꞉ ⟨ L ⟩ , (g x ＝ x) × ((a : ⟨ L ⟩)
→ (g a ＝ a)
→ (x ≤ a) holds))
path Γ-has-least-fixed-point
where
open correspondance-from-locally-small-ϕ L β h ϕ
(bounded-implies-local ϕ bnd)
open small-𝓘nd-from-exists (ind-e ϕ)
open 𝓘nd-is-small-from-bounded-and-small-presentation L β h small-pres ϕ bnd
open small-QIT-from-bounded-and-small-presentation L β h small-pres ϕ bnd
open 𝓘nd-is-small-QITs-exists (ind-e ϕ) (ind'-e ϕ bnd small-pres)
open smallness-assumption 𝓘nd-is-small
path : Γ ϕ (bounded-implies-local ϕ bnd) ＝ f
path = dfunext fe H
\end{code}
We can now state the (truncated) least fixed point theorem.
\begin{code}
Least-Fixed-Point-Theorem : (small-pres : has-small-presentation)
→ (f : ⟨ L ⟩ → ⟨ L ⟩)
→ (f-mono : is-monotone-endomap L f)
→ (Ǝ ϕ ꞉ 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩) ,
Σ bnd ꞉ is-bounded ϕ ,
((x : ⟨ L ⟩)
→ (Γ ϕ (bounded-implies-local ϕ bnd)) x ＝ f x))
holds
→ has-least-fixed-point L f
Least-Fixed-Point-Theorem small-pres f f-mono =
∥∥-rec (has-least-fixed-point-is-prop L f)
(Untruncated-Least-Fixed-Point-Theorem small-pres f f-mono)
\end{code}
We now explore conditions on monotone endomaps that guarantee they
correspond to some bounded inductive definition. We tentatively call this
notion 'density'.
A monotone map f, on a 𝓥-generated sup-lattice L, is dense if there is a family
γ : I → L, I : 𝓥, such that for all b : B and a : L we have
b ≤ᴮ f a → (Ǝ v ꞉ I , b ≤ᴮ f (γ v) × v ≤ᴮ a)
\begin{code}
module _
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
private
_≤_ = order-of L
⋁_ = join-of L
open local-inductive-definitions L β h
open bounded-inductive-definitions L β h
open is-basis h
density-condition : (f : ⟨ L ⟩ → ⟨ L ⟩)
→ (I : 𝓥 ̇)
→ (γ : I → ⟨ L ⟩)
→ 𝓤 ⊔ 𝓣 ⊔ 𝓥 ̇
density-condition f I γ = (b : B)
→ (a : ⟨ L ⟩)
→ b ≤ᴮ f a
→ (Ǝ i ꞉ I , b ≤ᴮ f (γ i) × (γ i ≤ a) holds) holds
is-dense : (f : ⟨ L ⟩ → ⟨ L ⟩) → 𝓤 ⊔ 𝓣 ⊔ (𝓥 ⁺) ̇
is-dense f = Σ I ꞉ 𝓥 ̇ , Σ γ ꞉ (I → ⟨ L ⟩) , density-condition f I γ
module _ (l-small : ⟨ L ⟩ is-locally 𝓥 small) where
private
_＝ˢ_ : ⟨ L ⟩ → ⟨ L ⟩ → 𝓥 ̇
x ＝ˢ y = resized (x ＝ y) (l-small x y)
＝ˢ-equiv-＝ : {x y : ⟨ L ⟩} → (x ＝ˢ y) ≃ (x ＝ y)
＝ˢ-equiv-＝ {x} {y} = resizing-condition (l-small x y)
＝ˢ-to-＝ : {x y : ⟨ L ⟩} → (x ＝ˢ y) → (x ＝ y)
＝ˢ-to-＝ = ⌜ ＝ˢ-equiv-＝ ⌝
＝-to-＝ˢ : {x y : ⟨ L ⟩} → (x ＝ y) → (x ＝ˢ y)
＝-to-＝ˢ = ⌜ ＝ˢ-equiv-＝ ⌝⁻¹
＝ˢ-refl : {x : ⟨ L ⟩} → x ＝ˢ x
＝ˢ-refl = ＝-to-＝ˢ refl
dense-implies-bounded : (f : ⟨ L ⟩ → ⟨ L ⟩)
→ is-monotone-endomap L f
→ is-dense f
→ Σ ϕ ꞉ 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩) ,
Σ bnd ꞉ is-bounded ϕ ,
((a : ⟨ L ⟩)
→ (Γ ϕ (bounded-implies-local ϕ bnd)) a ＝ f a)
dense-implies-bounded f f-mono (I , γ , f-dense) = (ϕ , bnd , H)
where
ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩)
ϕ (b , a') =
(Lift 𝓤 ((Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds)
, equiv-to-prop (Lift-≃ 𝓤 ((Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds))
(holds-is-prop (Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a')))
bnd : is-bounded ϕ
bnd = (ϕ-small , (I , (λ z → small-↓ᴮ (γ z)) , covering-cond))
where
ϕ-small : (a : ⟨ L ⟩) → (b : B) → (ϕ (b , a) holds) is 𝓥 small
ϕ-small a b = ((Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a) holds
, ≃-Lift 𝓤 ((Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a) holds))
covering-cond : (a : ⟨ L ⟩)
→ (b : B)
→ (b , a) ∈ ϕ
→ (Ǝ i ꞉ I , small-↓ᴮ (γ i) ↠ ↓ᴮ L β a) holds
covering-cond a b = demote-equiv-to-surj ∘ transport-lemma ∘ unlift-ϕ
where
unlift-ϕ : (b , a) ∈ ϕ → (Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a) holds
unlift-ϕ = ⌜ Lift-≃ 𝓤 ((Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a) holds) ⌝
transport-lemma : (Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a) holds
→ (Ǝ i ꞉ I , small-↓ᴮ (γ i) ≃ ↓ᴮ L β a) holds
transport-lemma =
∥∥-rec (holds-is-prop (Ǝ i ꞉ I , small-↓ᴮ (γ i) ≃ ↓ᴮ L β a))
(λ (i , o , eq)
→ ∣ (i , transport (λ z → small-↓ᴮ (γ i) ≃ ↓ᴮ L β z)
(＝ˢ-to-＝ eq)
small-↓ᴮ-≃-↓ᴮ) ∣)
demote-equiv-to-surj : (Ǝ i ꞉ I , small-↓ᴮ (γ i) ≃ ↓ᴮ L β a) holds
→ (Ǝ i ꞉ I , small-↓ᴮ (γ i) ↠ ↓ᴮ L β a) holds
demote-equiv-to-surj =
∥∥-functor (λ (i , f , f-is-equiv)
→ (i , f , equivs-are-surjections f-is-equiv))
H : (a : ⟨ L ⟩) → Γ ϕ (bounded-implies-local ϕ bnd) a ＝ f a
H a = reindexing-along-equiv-＝-sup
L ↓ᴮ-fa-equiv-↓ (β ∘ (↓-to-base ϕ a))
(Γ ϕ (bounded-implies-local ϕ bnd) a) (f a)
(sup-of-small-fam-is-lub L (β ∘ ↓-to-base ϕ a)
(bounded-implies-local ϕ bnd a))
(is-supᴮ (f a))
where
↓ᴮ-fa-equiv-↓ : (small-↓ᴮ (f a)) ≃ (ϕ ↓ a)
↓ᴮ-fa-equiv-↓ = Σ-cong ↓ᴮ-fa-equiv
where
↓ᴮ-fa-equiv : (b : B)
→ b ≤ᴮ f a
≃ (Ǝ a' ꞉ ⟨ L ⟩ ,
Lift 𝓤 ((Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds)
× (a' ≤ a) holds) holds
↓ᴮ-fa-equiv b =
logically-equivalent-props-are-equivalent
≤ᴮ-is-prop-valued
(holds-is-prop (Ǝ a' ꞉ ⟨ L ⟩ ,
Lift 𝓤 ((Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds)
× (a' ≤ a) holds))
(↓ᴮ-fa-to b)
(to-↓ᴮ-fa b)
where
↓ᴮ-fa-to : (b : B)
→ b ≤ᴮ f a
→ (Ǝ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ a) holds) holds
↓ᴮ-fa-to b = ∥∥-functor (g ∘ u) ∘ f-dense b a
where
u : Σ i ꞉ I , b ≤ᴮ f (γ i) × (γ i ≤ a) holds
→ Σ a' ꞉ ⟨ L ⟩ ,
(Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds × (a' ≤ a) holds
u (i , o , r) = (γ i , ∣ (i , o , ＝ˢ-refl) ∣ , r)
g : Σ a' ꞉ ⟨ L ⟩ ,
(Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds × (a' ≤ a) holds
→ Σ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ a) holds
g (a' , e , r) =
(a' ,
⌜ ≃-Lift 𝓤 ((Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds) ⌝ e , r)
to-↓ᴮ-fa : (b : B)
→ (Ǝ a' ꞉ ⟨ L ⟩ ,
(b , a') ∈ ϕ × (a' ≤ a) holds) holds
→ b ≤ᴮ f a
to-↓ᴮ-fa b = ∥∥-rec ≤ᴮ-is-prop-valued u ∘ ∥∥-functor g
where
u' : (a' : ⟨ L ⟩)
→ Σ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a'
→ (a' ≤ a) holds
→ b ≤ᴮ f a
u' a' (i , r , path) o =
≤-to-≤ᴮ (transitivity-of L (β b) (f a') (f a)
(transport (λ z → (β b ≤ z) holds)
(ap f (＝ˢ-to-＝ path))
(≤ᴮ-to-≤ r))
(f-mono a' a o))
trunc-u' : (a' : ⟨ L ⟩)
→ (Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds
→ (a' ≤ a) holds
→ b ≤ᴮ f a
trunc-u' a' =
∥∥-rec (Π-is-prop fe (λ _ → ≤ᴮ-is-prop-valued)) (u' a')
u : Σ a' ꞉ ⟨ L ⟩ ,
(Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds × (a' ≤ a) holds
→ b ≤ᴮ f a
u = uncurry (λ a' → uncurry (trunc-u' a'))
g : Σ a' ꞉ ⟨ L ⟩ , (b , a') ∈ ϕ × (a' ≤ a) holds
→ Σ a' ꞉ ⟨ L ⟩ ,
(Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds × (a' ≤ a) holds
g (a' , e , r) =
(a' ,
⌜ Lift-≃ 𝓤 ((Ǝ i ꞉ I , b ≤ᴮ f (γ i) × γ i ＝ˢ a') holds) ⌝ e , r)
\end{code}
We use the notion of density, along with the reasonable assumption that our
lattice is locally small, to state another version of the least fixed point
theorem.
\begin{code}
module _
{𝓤 𝓣 𝓥 : Universe}
{B : 𝓥 ̇}
(L : Sup-Lattice 𝓤 𝓣 𝓥)
(β : B → ⟨ L ⟩)
(h : is-basis L β)
where
open propositional-truncations-exist pt
open bounded-inductive-definitions L β h
open small-presentation-of-lattice L β h
open small-QIT-from-bounded-and-small-presentation L β h
module QITs-exists-density
(ind-e : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
→ inductively-generated-subset-exists L β h ϕ)
(ind'-e : (ϕ : 𝓟 {𝓤 ⊔ 𝓥} (B × ⟨ L ⟩))
→ (bnd : is-bounded ϕ)
→ (small-pres : has-small-presentation)
→ inductively-generated-small-subset-exists small-pres ϕ bnd)
where
open QITs-exists-for-all-ϕ L β h ind-e ind'-e
Least-Fixed-Point-Theorem-from-Density : has-small-presentation
→ ⟨ L ⟩ is-locally 𝓥 small
→ (f : ⟨ L ⟩ → ⟨ L ⟩)
→ is-monotone-endomap L f
→ is-dense L β h f
→ has-least-fixed-point L f
Least-Fixed-Point-Theorem-from-Density small-pres l-small f f-mono f-dense =
Untruncated-Least-Fixed-Point-Theorem small-pres f f-mono
(dense-implies-bounded L β h l-small f f-mono f-dense)
\end{code}