Skip to content

Commit

Permalink
Merge branch 'master' into equality-conaturals
Browse files Browse the repository at this point in the history
  • Loading branch information
fredrik-bakke authored Jan 30, 2025
2 parents 9076754 + 41b9165 commit b47b7ac
Show file tree
Hide file tree
Showing 11 changed files with 265 additions and 37 deletions.
26 changes: 13 additions & 13 deletions .github/workflows/ci.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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'
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
2 changes: 1 addition & 1 deletion .github/workflows/clean-up.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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: |
Expand Down
22 changes: 11 additions & 11 deletions .github/workflows/pages.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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:
Expand All @@ -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
Expand All @@ -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 ==
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/profiling.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ jobs:

steps:
- name: Checkout our repository
uses: actions/checkout@v3
uses: actions/checkout@v4
with:
path: repo

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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`.

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
```

Expand All @@ -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`.

Expand Down Expand Up @@ -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

Expand Down
5 changes: 5 additions & 0 deletions src/foundation-core/retracts-of-types.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,11 @@ module _
section-retract : section map-retraction-retract
pr1 section-retract = inclusion-retract
pr2 section-retract = is-retraction-map-retraction-retract

retract-section :
{l1 l2 : Level} {A : UU l1} {B : UU l2}
(f : A B) section f B retract-of A
retract-section f s = (pr1 s , f , pr2 s)
```

### The type of retracts of a type
Expand Down
Loading

0 comments on commit b47b7ac

Please sign in to comment.