Merge branch 'master' into csbe

Author: fredrik-bakke

.github/workflows/ci.yaml

@@ -34,15 +34,15 @@ jobs:
         agda: ['2.7.0']
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: master
       - name: Setup Agda
         uses: wenkokke/[email protected]
         with:
           agda-version: ${{ matrix.agda }}
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         id: cache-agda-formalization
         name: Restore Agda formalization cache
         with:
@@ -61,13 +61,13 @@ jobs:
           make check
 
       - name: Save Agda build cache
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         with:
           path: master/_build
           key: '${{ steps.cache-agda-formalization.outputs.cache-primary-key }}'
 
       # Install Python and friends for website generation only where needed
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         if: ${{ matrix.os == 'ubuntu-latest' }}
         with:
           python-version: '3.8'
@@ -92,7 +92,7 @@ jobs:
       # keep the same key for a branch and update it on pushes.
       - name: Save pre-website cache
         if: ${{ matrix.os == 'ubuntu-latest' }}
-        uses: actions/cache/save@v3
+        uses: actions/cache/save@v4
         with:
           key: pre-website-${{ github.run_id }}
           path: master/docs
@@ -106,29 +106,29 @@ jobs:
       actions: write
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
         with:
           path: master
 
-      - uses: peaceiris/actions-mdbook@v1
+      - uses: peaceiris/actions-mdbook@v2
         with:
           mdbook-version: '0.4.34'
 
-      - uses: baptiste0928/cargo-install@v2
+      - uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-linkcheck
           version: '0.7.7'
 
       # Install Python and friends for website generation only where needed
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
           cache: 'pip'
 
       - run: python3 -m pip install -r master/scripts/requirements.txt
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         with:
           key: pre-website-${{ github.run_id }}
           path: master/docs
@@ -162,14 +162,14 @@ jobs:
   pre-commit:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
           cache: 'pip'
 
       - run: python3 -m pip install -r scripts/requirements.txt
 
-      - uses: pre-commit/[email protected].0
+      - uses: pre-commit/[email protected].1

.github/workflows/clean-up.yaml

@@ -9,7 +9,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Cleanup
         run: |

.github/workflows/pages.yaml

@@ -32,7 +32,7 @@ jobs:
       id-token: write # to verify the deployment originates from an appropriate source
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: master
           # We need the entire history for contributor information
@@ -43,7 +43,7 @@ jobs:
         with:
           agda-version: ${{ matrix.agda }}
 
-      - uses: actions/cache/restore@v3
+      - uses: actions/cache/restore@v4
         id: cache-agda-formalization
         name: Restore Agda formalization cache
         with:
@@ -56,35 +56,35 @@ jobs:
 
       # Keep versions in sync with the Makefile
       - name: MDBook setup
-        uses: peaceiris/actions-mdbook@v1
+        uses: peaceiris/actions-mdbook@v2
         with:
           mdbook-version: '0.4.34'
 
       - name: Install mdbook-pagetoc
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-pagetoc
           version: '0.1.7'
 
       - name: Install mdbook-katex
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-katex
           version: '0.5.7'
 
       - name: Install mdbook-linkcheck
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-linkcheck
           version: '0.7.7'
 
       - name: Install mdbook-catppuccin
-        uses: baptiste0928/cargo-install@v2
+        uses: baptiste0928/cargo-install@v3
         with:
           crate: mdbook-catppuccin
           version: '1.2.0'
 
-      - uses: actions/setup-python@v4
+      - uses: actions/setup-python@v5
         with:
           python-version: '3.8'
           check-latest: true
@@ -100,21 +100,21 @@ jobs:
           make website
 
       - name: Setup Pages
-        uses: actions/configure-pages@v3
+        uses: actions/configure-pages@v5
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==
           'workflow_dispatch'
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
+        uses: actions/upload-pages-artifact@v3
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==
           'workflow_dispatch'
         with:
           path: master/book/html
 
       - name: Deploy to GitHub Pages
-        uses: actions/deploy-pages@v1
+        uses: actions/deploy-pages@v4
         id: deployment
         if: >-
           github.ref == 'refs/heads/master' || github.event_name ==

.github/workflows/profiling.yaml

@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout our repository
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: repo
 

agda-unimath.agda-lib

@@ -1,3 +1,3 @@
 name: agda-unimath
 include: src
-flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions -WnoWithoutKFlagPrimEraseEquality
+flags: --without-K --exact-split --no-import-sorts --auto-inline --no-require-unique-meta-solutions -WnoWithoutKFlagPrimEraseEquality --no-postfix-projections

src/category-theory/conservative-functors-precategories.lagda.md

@@ -22,8 +22,9 @@ open import foundation.universe-levels
 ## Idea
 
 A [functor](category-theory.functors-precategories.md) `F : C → D` between
-[precategories](category-theory.precategories.md) is **conservative** if every
-morphism that is mapped to an
+[precategories](category-theory.precategories.md) is
+{{#concept "conservative" Disambiguation="functor of set-level precategories" WDID=Q23808682 WD="conservative functor" Agda=is-conservative-functor-Precategory Agda=conservative-functor-Precategory}}
+if every morphism that is mapped to an
 [isomorphism](category-theory.isomorphisms-in-precategories.md) in `D` is an
 isomorphism in `C`.
 

src/category-theory/essentially-surjective-functors-precategories.lagda.md

@@ -22,7 +22,8 @@ open import foundation.universe-levels
 ## Idea
 
 A [functor](category-theory.functors-precategories.md) `F : C → D` between
-[precategories](category-theory.precategories.md) is **essentially surjective**
+[precategories](category-theory.precategories.md) is
+{{#concept "essentially surjective" Disambiguation="functor between set-level precategories" WDID=Q140283 WD="essentially surjective functor" Agda=is-essentially-surjective-functor-Precategory Agda=essentially-surjective-functor-Precategory}}
 if there for every object `y : D`
 [merely exists](foundation.existential-quantification.md) an object `x : C` such
 that `F x ≅ y`.

src/category-theory/pseudomonic-functors-precategories.lagda.md

@@ -43,7 +43,7 @@ Pseudomonic functors present
 is the "right notion" of subcategory with respect to the _principle of
 invariance under equivalences_.
 
-## Definition
+## Definitions
 
 ### The predicate on isomorphisms of being full
 

src/category-theory/split-essentially-surjective-functors-precategories.lagda.md

@@ -7,16 +7,26 @@ module category-theory.split-essentially-surjective-functors-precategories where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.categories
+open import category-theory.cores-precategories
 open import category-theory.essential-fibers-of-functors-precategories
 open import category-theory.essentially-surjective-functors-precategories
+open import category-theory.fully-faithful-functors-precategories
 open import category-theory.functors-precategories
+open import category-theory.isomorphisms-in-categories
 open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
+open import category-theory.pseudomonic-functors-precategories
 
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.equivalences
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.retracts-of-types
+open import foundation.sections
 open import foundation.universe-levels
 ```
 
@@ -25,8 +35,9 @@ open import foundation.universe-levels
 ## Idea
 
 A [functor](category-theory.functors-precategories.md) `F : C → D` between
-[precategories](category-theory.precategories.md) is **split essentially
-surjective** if there is a section of the
+[precategories](category-theory.precategories.md) is
+{{#concept "split essentially surjective" Disambiguation="functor between set-level precategories" Agda=is-split-essentially-surjective-functor-Precategory  Agda=split-essentially-surjective-functor-Precategory}}
+if there is a section of the
 [essential fiber](category-theory.essential-fibers-of-functors-precategories.md)
 over every object of `D`.
 
@@ -166,14 +177,110 @@ module _
       ( is-essentially-surjective-is-split-essentially-surjective-functor-Precategory)
 ```
 
-### Being split essentially surjective is a property of fully faithful functors when the codomain is a category
+### Being split essentially surjective is a property of fully faithful functors when the domain is a category
 
-This remains to be shown. This is Lemma 6.8 of _Univalent Categories and the
-Rezk completion_.
+This is Lemma 6.8 of {{#cite AKS15}}, although we give a different proof.
+
+**Proof.** Let `F : 𝒞 → 𝒟` be a functor of precategories, where `𝒞` is
+univalent. It suffices to assume `F` is fully faithful on the
+[core](category-theory.cores-categories.md) of `𝒞`. Then, to show that
+`is-split-essentially-surjective` is a proposition, i.e., that
+
+```text
+  (d : 𝒟₀) → Σ (x : 𝒞₀), (Fx ≅ d)
+```
+
+is a proposition it is equivalent to show that if it has an element it is
+contractible, so assume `F` is split essentially surjective. Then, it suffices
+to show that for every `d : 𝒟₀`, the type `Σ (x : 𝒞₀), (Fx ≅ d)` is
+contractible. By split essential surjectivity there is an element `y : 𝒞₀` such
+that `Fy ≅ d` and since postcomposing by an isomorphism is an equivalence of
+isomorphism-sets, we have
+
+```text
+  (Fx ≅ d) ≃ (Fx ≅ Fy) ≃ (x ≅ y)
+```
+
+so `(Σ (x : 𝒞₀), (Fx ≅ d)) ≃ (Σ (x : 𝒞₀), (x ≅ y))`, and the latter is
+contractible by univalence.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2) (D : Precategory l3 l4)
+  (F : functor-Precategory C D)
+  (c : is-category-Precategory C)
+  where
+
+  is-proof-irrelevant-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory :
+    ( (x y : obj-Precategory C) →
+      section (preserves-iso-functor-Precategory C D F {x} {y})) →
+    is-proof-irrelevant
+      ( is-split-essentially-surjective-functor-Precategory C D F)
+  is-proof-irrelevant-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory
+    H s =
+    is-contr-Π
+      ( λ d →
+        is-contr-retract-of
+          ( Σ (obj-Category (C , c)) (iso-Category (C , c) (pr1 (s d))))
+          ( retract-tot
+            ( λ x →
+              comp-retract
+                ( retract-section
+                  ( preserves-iso-functor-Precategory C D F)
+                  ( H (pr1 (s d)) x))
+                ( retract-equiv
+                  ( equiv-inv-iso-Precategory D ∘e
+                    equiv-postcomp-hom-iso-Precategory
+                      ( core-precategory-Precategory D)
+                      ( map-equiv
+                        ( compute-iso-core-Precategory D)
+                        ( inv-iso-Precategory D (pr2 (s d))))
+                      ( obj-functor-Precategory C D F x)))))
+          ( is-torsorial-iso-Category (C , c) (pr1 (s d))))
+
+  is-prop-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory :
+    ( (x y : obj-Precategory C) →
+      section (preserves-iso-functor-Precategory C D F {x} {y})) →
+    is-prop
+      ( is-split-essentially-surjective-functor-Precategory C D F)
+  is-prop-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory
+    =
+    is-prop-is-proof-irrelevant ∘
+    is-proof-irrelevant-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory
+
+  is-prop-is-split-essentially-surjective-is-fully-faithful-on-isos-functor-is-category-domain-Precategory :
+    ( (x y : obj-Precategory C) →
+      is-equiv (preserves-iso-functor-Precategory C D F {x} {y})) →
+    is-prop (is-split-essentially-surjective-functor-Precategory C D F)
+  is-prop-is-split-essentially-surjective-is-fully-faithful-on-isos-functor-is-category-domain-Precategory
+    H =
+    is-prop-is-split-essentially-surjective-has-section-on-isos-functor-is-category-domain-Precategory
+      ( λ x y → section-is-equiv (H x y))
+
+  is-prop-is-split-essentially-surjective-is-pseudomonic-functor-is-category-domain-Precategory :
+    is-pseudomonic-functor-Precategory C D F →
+    is-prop (is-split-essentially-surjective-functor-Precategory C D F)
+  is-prop-is-split-essentially-surjective-is-pseudomonic-functor-is-category-domain-Precategory
+    H =
+    is-prop-is-split-essentially-surjective-is-fully-faithful-on-isos-functor-is-category-domain-Precategory
+      ( λ x y →
+        is-equiv-preserves-iso-is-pseudomonic-functor-Precategory C D F H
+          { x}
+          { y})
+
+  is-prop-is-split-essentially-surjective-is-fully-faithful-functor-is-category-domain-Precategory :
+    is-fully-faithful-functor-Precategory C D F →
+    is-prop (is-split-essentially-surjective-functor-Precategory C D F)
+  is-prop-is-split-essentially-surjective-is-fully-faithful-functor-is-category-domain-Precategory
+    H =
+    is-prop-is-split-essentially-surjective-is-pseudomonic-functor-is-category-domain-Precategory
+      ( is-pseudomonic-is-fully-faithful-functor-Precategory C D F H)
+```
 
 ## References
 
-{{#bibliography}} {{#reference AKS15}}
+{{#bibliography}}
 
 ## External links