Two fixed point theorems (#1227)

Formalizations of the Knaster–Tarski fixed point theorem and Kleene's
fixed point theorem, in addition to the necessary infrastructure.

~Merge after #1225.~

src/category-theory/opposite-large-precategories.lagda.md

@@ -14,6 +14,7 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.large-identity-types
 open import foundation.sets
 open import foundation.strictly-involutive-identity-types
 open import foundation.universe-levels
@@ -141,6 +142,18 @@ module _
 
 ## Properties
 
+### The opposite large precategory construction is a strict involution
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (C : Large-Precategory α β)
+  where
+
+  is-involution-opposite-Large-Precategory :
+    opposite-Large-Precategory (opposite-Large-Precategory C) ＝ω C
+  is-involution-opposite-Large-Precategory = reflω
+```
+
 ### Computing the isomorphism sets of the opposite large precategory
 
 ```agda

src/domain-theory.lagda.md

@@ -0,0 +1,17 @@
+# Domain theory
+
+## Modules in the domain theory namespace
+
+```agda
+module domain-theory where
+
+open import domain-theory.directed-complete-posets public
+open import domain-theory.directed-families-posets public
+open import domain-theory.kleenes-fixed-point-theorem-omega-complete-posets public
+open import domain-theory.kleenes-fixed-point-theorem-posets public
+open import domain-theory.omega-complete-posets public
+open import domain-theory.omega-continuous-maps-omega-complete-posets public
+open import domain-theory.omega-continuous-maps-posets public
+open import domain-theory.reindexing-directed-families-posets public
+open import domain-theory.scott-continuous-maps-posets public
+```

src/domain-theory/directed-complete-posets.lagda.md

@@ -0,0 +1,174 @@
+# Directed complete posets
+
+```agda
+module domain-theory.directed-complete-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import domain-theory.directed-families-posets
+
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.sets
+open import foundation.universe-levels
+
+open import order-theory.least-upper-bounds-posets
+open import order-theory.posets
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "directed complete poset" WD="complete partial order" WDID=Q3082805 Agda=Directed-Complete-Poset}}
+is a [poset](order-theory.posets.md) such that all
+[directed families](domain-theory.directed-families-posets.md) have
+[least upper bounds](order-theory.least-upper-bounds-posets.md).
+
+## Definitions
+
+### The predicate on posets of being directed complete
+
+```agda
+module _
+  {l1 l2 : Level} (l3 : Level) (P : Poset l1 l2)
+  where
+
+  is-directed-complete-prop-Poset : Prop (l1 ⊔ l2 ⊔ lsuc l3)
+  is-directed-complete-prop-Poset =
+    Π-Prop
+      ( directed-family-Poset l3 P)
+      ( λ F →
+        has-least-upper-bound-family-of-elements-prop-Poset P
+          ( family-directed-family-Poset P F))
+
+  is-directed-complete-Poset : UU (l1 ⊔ l2 ⊔ lsuc l3)
+  is-directed-complete-Poset =
+    type-Prop is-directed-complete-prop-Poset
+
+  is-prop-is-directed-complete-Poset : is-prop is-directed-complete-Poset
+  is-prop-is-directed-complete-Poset =
+    is-prop-type-Prop is-directed-complete-prop-Poset
+
+module _
+  {l1 l2 l3 : Level} (P : Poset l1 l2) (H : is-directed-complete-Poset l3 P)
+  where
+
+  sup-is-directed-complete-Poset : directed-family-Poset l3 P → type-Poset P
+  sup-is-directed-complete-Poset F = pr1 (H F)
+
+  is-least-upper-bound-sup-is-directed-complete-Poset :
+    (x : directed-family-Poset l3 P) →
+    is-least-upper-bound-family-of-elements-Poset P
+      ( family-directed-family-Poset P x)
+      ( sup-is-directed-complete-Poset x)
+  is-least-upper-bound-sup-is-directed-complete-Poset F = pr2 (H F)
+```
+
+### Directed complete posets
+
+```agda
+Directed-Complete-Poset :
+  (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
+Directed-Complete-Poset l1 l2 l3 =
+  Σ (Poset l1 l2) (is-directed-complete-Poset l3)
+
+module _
+  {l1 l2 l3 : Level} (A : Directed-Complete-Poset l1 l2 l3)
+  where
+
+  poset-Directed-Complete-Poset : Poset l1 l2
+  poset-Directed-Complete-Poset = pr1 A
+
+  type-Directed-Complete-Poset : UU l1
+  type-Directed-Complete-Poset =
+    type-Poset poset-Directed-Complete-Poset
+
+  leq-prop-Directed-Complete-Poset :
+    (x y : type-Directed-Complete-Poset) → Prop l2
+  leq-prop-Directed-Complete-Poset =
+    leq-prop-Poset poset-Directed-Complete-Poset
+
+  leq-Directed-Complete-Poset :
+    (x y : type-Directed-Complete-Poset) → UU l2
+  leq-Directed-Complete-Poset =
+    leq-Poset poset-Directed-Complete-Poset
+
+  is-prop-leq-Directed-Complete-Poset :
+    (x y : type-Directed-Complete-Poset) →
+    is-prop (leq-Directed-Complete-Poset x y)
+  is-prop-leq-Directed-Complete-Poset =
+    is-prop-leq-Poset poset-Directed-Complete-Poset
+
+  refl-leq-Directed-Complete-Poset :
+    (x : type-Directed-Complete-Poset) →
+    leq-Directed-Complete-Poset x x
+  refl-leq-Directed-Complete-Poset =
+    refl-leq-Poset poset-Directed-Complete-Poset
+
+  antisymmetric-leq-Directed-Complete-Poset :
+    is-antisymmetric leq-Directed-Complete-Poset
+  antisymmetric-leq-Directed-Complete-Poset =
+    antisymmetric-leq-Poset poset-Directed-Complete-Poset
+
+  transitive-leq-Directed-Complete-Poset :
+    is-transitive leq-Directed-Complete-Poset
+  transitive-leq-Directed-Complete-Poset =
+    transitive-leq-Poset poset-Directed-Complete-Poset
+
+  is-set-type-Directed-Complete-Poset :
+    is-set type-Directed-Complete-Poset
+  is-set-type-Directed-Complete-Poset =
+    is-set-type-Poset poset-Directed-Complete-Poset
+
+  set-Directed-Complete-Poset : Set l1
+  set-Directed-Complete-Poset =
+    set-Poset poset-Directed-Complete-Poset
+
+  is-directed-complete-Directed-Complete-Poset :
+    is-directed-complete-Poset l3 poset-Directed-Complete-Poset
+  is-directed-complete-Directed-Complete-Poset = pr2 A
+
+  sup-Directed-Complete-Poset :
+    directed-family-Poset l3 poset-Directed-Complete-Poset →
+    type-Directed-Complete-Poset
+  sup-Directed-Complete-Poset =
+    sup-is-directed-complete-Poset
+      ( poset-Directed-Complete-Poset)
+      ( is-directed-complete-Directed-Complete-Poset)
+
+  is-least-upper-bound-sup-Directed-Complete-Poset :
+    (x : directed-family-Poset l3 poset-Directed-Complete-Poset) →
+    is-least-upper-bound-family-of-elements-Poset
+      ( poset-Directed-Complete-Poset)
+      ( family-directed-family-Poset poset-Directed-Complete-Poset x)
+      ( sup-Directed-Complete-Poset x)
+  is-least-upper-bound-sup-Directed-Complete-Poset =
+    is-least-upper-bound-sup-is-directed-complete-Poset
+      ( poset-Directed-Complete-Poset)
+      ( is-directed-complete-Directed-Complete-Poset)
+
+  is-upper-bound-sup-Directed-Complete-Poset :
+    (x : directed-family-Poset l3 poset-Directed-Complete-Poset)
+    (i : type-directed-family-Poset poset-Directed-Complete-Poset x) →
+    leq-Directed-Complete-Poset
+      ( family-directed-family-Poset poset-Directed-Complete-Poset x i)
+      ( sup-Directed-Complete-Poset x)
+  is-upper-bound-sup-Directed-Complete-Poset x =
+    backward-implication
+      ( is-least-upper-bound-sup-Directed-Complete-Poset
+        ( x)
+        ( sup-Directed-Complete-Poset x))
+      ( refl-leq-Directed-Complete-Poset (sup-Directed-Complete-Poset x))
+```
+
+## External links
+
+- [dcpo](https://ncatlab.org/nlab/show/dcpo) at $n$Lab

src/domain-theory/directed-families-posets.lagda.md

@@ -0,0 +1,156 @@
+# Directed families in posets
+
+```agda
+module domain-theory.directed-families-posets where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.inhabited-types
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.surjective-maps
+open import foundation.universal-quantification
+open import foundation.universe-levels
+
+open import order-theory.order-preserving-maps-posets
+open import order-theory.posets
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "directed family of elements" WD="upward directed set" WDID=Q1513048 Agda=directed-family-Poset}}
+in a [poset](order-theory.posets.md) `P` consists of an
+[inhabited type](foundation.inhabited-types.md) `I` and a map `x : I → P` such
+that for any two elements `i j : I` there
+[exists](foundation.existential-quantification.md) an element `k : I` such that
+both `x i ≤ x k` and `x j ≤ x k` hold.
+
+## Definitions
+
+### The predicate on a family of elements in a poset of being directed
+
+```agda
+is-directed-prop-family-Poset :
+  {l1 l2 l3 : Level} (P : Poset l1 l2) (I : Inhabited-Type l3)
+  (x : type-Inhabited-Type I → type-Poset P) → Prop (l2 ⊔ l3)
+is-directed-prop-family-Poset P I x =
+  ∀'
+    ( type-Inhabited-Type I)
+    ( λ i →
+      ∀'
+        ( type-Inhabited-Type I)
+        ( λ j →
+          ∃ ( type-Inhabited-Type I)
+            ( λ k →
+              leq-prop-Poset P (x i) (x k) ∧ leq-prop-Poset P (x j) (x k))))
+
+is-directed-family-Poset :
+  {l1 l2 l3 : Level} (P : Poset l1 l2) (I : Inhabited-Type l3)
+  (α : type-Inhabited-Type I → type-Poset P) → UU (l2 ⊔ l3)
+is-directed-family-Poset P I x = type-Prop (is-directed-prop-family-Poset P I x)
+```
+
+### The type of directed families of elements in a poset
+
+```agda
+directed-family-Poset :
+  {l1 l2 : Level} (l3 : Level) → Poset l1 l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
+directed-family-Poset l3 P =
+  Σ ( Inhabited-Type l3)
+    ( λ I →
+      Σ ( type-Inhabited-Type I → type-Poset P)
+        ( is-directed-family-Poset P I))
+
+module _
+  {l1 l2 l3 : Level} (P : Poset l1 l2) (x : directed-family-Poset l3 P)
+  where
+
+  inhabited-type-directed-family-Poset : Inhabited-Type l3
+  inhabited-type-directed-family-Poset = pr1 x
+
+  type-directed-family-Poset : UU l3
+  type-directed-family-Poset =
+    type-Inhabited-Type inhabited-type-directed-family-Poset
+
+  is-inhabited-type-directed-family-Poset :
+    is-inhabited type-directed-family-Poset
+  is-inhabited-type-directed-family-Poset =
+    is-inhabited-type-Inhabited-Type inhabited-type-directed-family-Poset
+
+  family-directed-family-Poset : type-directed-family-Poset → type-Poset P
+  family-directed-family-Poset = pr1 (pr2 x)
+
+  is-directed-family-directed-family-Poset :
+    is-directed-family-Poset P
+      ( inhabited-type-directed-family-Poset)
+      ( family-directed-family-Poset)
+  is-directed-family-directed-family-Poset = pr2 (pr2 x)
+```
+
+### The action of order preserving maps on directed families
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  (P : Poset l1 l2) (Q : Poset l3 l4)
+  (f : hom-Poset P Q)
+  (x : directed-family-Poset l5 P)
+  where
+
+  type-directed-family-hom-Poset : UU l5
+  type-directed-family-hom-Poset = type-directed-family-Poset P x
+
+  is-inhabited-type-directed-family-hom-Poset :
+    is-inhabited type-directed-family-hom-Poset
+  is-inhabited-type-directed-family-hom-Poset =
+    is-inhabited-type-directed-family-Poset P x
+
+  inhabited-type-directed-family-hom-Poset : Inhabited-Type l5
+  inhabited-type-directed-family-hom-Poset =
+    type-directed-family-hom-Poset ,
+    is-inhabited-type-directed-family-hom-Poset
+
+  family-directed-family-hom-Poset :
+    type-directed-family-hom-Poset → type-Poset Q
+  family-directed-family-hom-Poset =
+    map-hom-Poset P Q f ∘ family-directed-family-Poset P x
+
+  abstract
+    is-directed-family-directed-family-hom-Poset :
+      is-directed-family-Poset Q
+        inhabited-type-directed-family-hom-Poset
+        family-directed-family-hom-Poset
+    is-directed-family-directed-family-hom-Poset u v =
+      elim-exists
+        ( exists-structure-Prop type-directed-family-hom-Poset _)
+        ( λ z y →
+          intro-exists z
+            ( preserves-order-map-hom-Poset P Q f
+                ( family-directed-family-Poset P x u)
+                ( family-directed-family-Poset P x z)
+                ( pr1 y) ,
+              preserves-order-map-hom-Poset P Q f
+                ( family-directed-family-Poset P x v)
+                ( family-directed-family-Poset P x z)
+                ( pr2 y)))
+        ( is-directed-family-directed-family-Poset P x u v)
+
+  directed-family-hom-Poset : directed-family-Poset l5 Q
+  directed-family-hom-Poset =
+    inhabited-type-directed-family-hom-Poset ,
+    family-directed-family-hom-Poset ,
+    is-directed-family-directed-family-hom-Poset
+```