WIP: A constructive Cantor–Schröder–Bernstein theorem?

references.bib

@@ -248,6 +248,25 @@ @article{EKMS93
   keywords = {axiality,closure operation,Galois connection,interior operation,polarity}
 }
 
+@article{Esc08,
+  author       = {Escardó, Martín},
+  title        = {Exhaustible sets in higher-type computation},
+  journal      = {Logical Methods in Computer Science},
+  volume       = {4},
+  year         = {2008},
+  month        = {8},
+  number       = {3},
+  issue        = {3},
+  publisher    = {Centre pour la Communication Scientifique Directe (CCSD)},
+  pages        = {3:3, 37},
+  issn         = {1860-5974},
+  doi          = {10.2168/LMCS-4(3:3)2008},
+  eprint       = {0808.0441},
+  eprinttype   = {arxiv},
+  eprintclass  = {cs},
+  primaryclass = {cs.LO}
+}
+
 @online{Esc19DefinitionsEquivalence,
   title        = {Definitions of Equivalence Satisfying Judgmental/Strict Groupoid Laws?},
   author       = {Escardó, Martín Hötzel},

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,14 @@
+# Domain theory
+
+```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.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 a directed complete poset
+
+```agda
+module _
+  {l1 l2 : Level} (l3 : Level) (P : Poset l1 l2)
+  where
+
+  is-directed-complete-Poset-Prop : Prop (l1 ⊔ l2 ⊔ lsuc l3)
+  is-directed-complete-Poset-Prop =
+    Π-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-Poset-Prop
+
+  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-Poset-Prop
+
+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)
+
+  leq-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)
+  leq-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