Merge branch 'master' into iteration-dependent-functions

references.bib

@@ -44,6 +44,17 @@ @article{AL19
   langid      = {english}
 }
 
+@misc{Awodey22,
+       author = {{Awodey}, Steve},
+        title = "{On Hofmann-Streicher universes}",
+     keywords = {Mathematics - Category Theory, Mathematics - Logic},
+         year = 2022,
+        month = may,
+archivePrefix = {arXiv},
+       eprint = {2205.10917},
+ primaryClass = {math.CT}
+}
+
 @online{BCDE21,
   title  = {Free groups in HoTT/UF in Agda},
   author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escardó, Martín},

scripts/preprocessor_git_metadata.py

@@ -84,12 +84,14 @@ def get_author_element_for_file(filename, include_contributors, contributors):
             'HEAD', '--', filename
         ], capture_output=True, text=True, check=True).stdout.splitlines()
 
-        # Collect authors and sort by number of commits
-        author_names = [
-            author['displayName']
-            for author in sorted_authors_from_raw_shortlog_lines(raw_authors_git_output, contributors)
-        ]
-        attribution_text = f'<p><i>Content created by {format_multiple_authors_attribution(author_names)}.</i></p>'
+        # If all commits to a file are chore commits, then there are no authors
+        if raw_authors_git_output:
+          # Collect authors and sort by number of commits
+          author_names = [
+              author['displayName']
+              for author in sorted_authors_from_raw_shortlog_lines(raw_authors_git_output, contributors)
+          ]
+          attribution_text = f'<p><i>Content created by {format_multiple_authors_attribution(author_names)}.</i></p>'
 
     file_log_output = subprocess.run([
         'git', 'log',

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