Skip to content

Preview: depostulate axioms #1380

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 41 commits into
base: master
Choose a base branch
from
Open

Preview: depostulate axioms #1380

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
41 commits
Select commit Hold shift + click to select a range
406d208
depostulate funext in `foundation.function-extensionality`
fredrik-bakke Mar 19, 2025
60a5a24
add funextaxiom dependencies
fredrik-bakke Mar 19, 2025
da48fc2
remove unused funext imports
fredrik-bakke Mar 19, 2025
19929d0
scripts
fredrik-bakke Mar 19, 2025
5cafc70
Revert "depostulate funext in `foundation.function-extensionality`"
fredrik-bakke Mar 20, 2025
ff7f437
Reapply "depostulate funext in `foundation.function-extensionality`"
fredrik-bakke Mar 20, 2025
9cbef82
remove unused imports
fredrik-bakke Mar 20, 2025
70bdce7
factor out `is-contr-Π` and `is-prop-Π`
fredrik-bakke Mar 20, 2025
35ba0ff
fix `multiplication-integers`
fredrik-bakke Mar 20, 2025
80f80bb
move retract precomp/postcomp
fredrik-bakke Mar 20, 2025
217ed4c
`foundation-core.logical-equivalences`
fredrik-bakke Mar 20, 2025
2b54978
`foundation.dependent-products-truncated-types`
fredrik-bakke Mar 20, 2025
c62f26f
move `equiv-Set`
fredrik-bakke Mar 20, 2025
0ed41ca
script
fredrik-bakke Mar 20, 2025
edec29f
import telescope
fredrik-bakke Mar 20, 2025
ef7655b
move raising universe levels unit type
fredrik-bakke Mar 20, 2025
84e9628
`foundation-core.diagonal-maps-of-types`
fredrik-bakke Mar 20, 2025
35ac679
raising universe levels of booleans
fredrik-bakke Mar 20, 2025
d3f695a
`foundation-core.maybe`
fredrik-bakke Mar 20, 2025
cf9ed88
`foundation-core.booleans`
fredrik-bakke Mar 20, 2025
12eaf68
import optimizations reflection
fredrik-bakke Mar 20, 2025
7e89f92
import optimizations reflection
fredrik-bakke Mar 20, 2025
7c34b94
optimize imports `lists.lists`
fredrik-bakke Mar 20, 2025
4588624
imports equality integers
fredrik-bakke Mar 20, 2025
2cfd6ff
imports reflection
fredrik-bakke Mar 20, 2025
1fbc603
imports addition natural numbers
fredrik-bakke Mar 20, 2025
3941908
imports multiplication natural numbers
fredrik-bakke Mar 20, 2025
f402d8e
depostulate funext
fredrik-bakke Mar 20, 2025
63b3fa3
Revert "depostulate funext"
fredrik-bakke Mar 21, 2025
77f4142
fix line length
fredrik-bakke Mar 21, 2025
566e00c
fix dependencies public imports
fredrik-bakke Mar 21, 2025
ee6b0e5
wip unpostulate
fredrik-bakke Mar 21, 2025
1251505
hide scripts
fredrik-bakke Mar 24, 2025
5cd74a3
fix prose
fredrik-bakke Mar 24, 2025
0e6f5f3
repostulate funext
fredrik-bakke Mar 24, 2025
1f40f6f
Merge branch 'master' into unpostulate
fredrik-bakke Mar 24, 2025
49cc93e
fix link concept
fredrik-bakke Mar 24, 2025
29957d0
`foundation-core.raising-universe-levels`
fredrik-bakke Mar 24, 2025
f4f6ce2
restore lemma raising universe levels
fredrik-bakke Mar 24, 2025
fa99f84
preview depostulation
fredrik-bakke Mar 24, 2025
2b2118a
preview depostulation
fredrik-bakke Mar 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
2 changes: 1 addition & 1 deletion scripts/remove_unused_imports.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ def filter_agda_files(f): return utils.is_agda_file(pathlib.Path(f)) and os.path

temp_dir = 'temp'
status = 0
agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching'
agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching -WnoPatternShadowsConstructor'
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why wouldn't we want these warnings?

Also, is the question of including this pragma orthogonal to the purpose of this pull request, or am I missing something?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I thought this pragma promoted the warning to an error. It is orthogonal to this PR, but not to #1373 on which it depends

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(There it caused errors in the file elementary-number-theory.multiplication-integers)


temp_root = os.path.join(root, temp_dir)
shutil.rmtree(temp_root, ignore_errors=True)
Expand Down
328 changes: 168 additions & 160 deletions src/category-theory.lagda.md
View file
Open in desktop

Large diffs are not rendered by default.

26 changes: 17 additions & 9 deletions src/category-theory/adjunctions-large-categories.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,20 +1,28 @@
# Adjunctions between large categories

```agda
module category-theory.adjunctions-large-categories where
open import foundation.truncations-exist
open import foundation-core.univalence
open import foundation.function-extensionality-axiom

module category-theory.adjunctions-large-categories
(funext : function-extensionality)
(univalence : univalence-axiom)
(truncations : truncations-exist)
where
```

<details><summary>Imports</summary>

```agda
open import category-theory.adjunctions-large-precategories
open import category-theory.functors-large-categories
open import category-theory.large-categories
open import category-theory.natural-transformations-functors-large-categories

open import foundation.commuting-squares-of-maps
open import foundation.equivalences
open import foundation.identity-types
open import category-theory.adjunctions-large-precategories funext univalence truncations
open import category-theory.functors-large-categories funext univalence truncations
open import category-theory.large-categories funext univalence truncations
open import category-theory.natural-transformations-functors-large-categories funext univalence truncations

open import foundation.commuting-squares-of-maps funext univalence
open import foundation.equivalences funext
open import foundation.identity-types funext
open import foundation.universe-levels
```

Expand Down
22 changes: 15 additions & 7 deletions src/category-theory/adjunctions-large-precategories.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,20 +1,28 @@
# Adjunctions between large precategories

```agda
module category-theory.adjunctions-large-precategories where
open import foundation.truncations-exist
open import foundation-core.univalence
open import foundation.function-extensionality-axiom

module category-theory.adjunctions-large-precategories
(funext : function-extensionality)
(univalence : univalence-axiom)
(truncations : truncations-exist)
where
```

<details><summary>Imports</summary>

```agda
open import category-theory.functors-large-precategories
open import category-theory.large-precategories
open import category-theory.natural-transformations-functors-large-precategories
open import category-theory.functors-large-precategories funext univalence truncations
open import category-theory.large-precategories funext univalence truncations
open import category-theory.natural-transformations-functors-large-precategories funext univalence truncations

open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-maps
open import foundation.equivalences
open import foundation.identity-types
open import foundation.commuting-squares-of-maps funext univalence
open import foundation.equivalences funext
open import foundation.identity-types funext
open import foundation.universe-levels
```

Expand Down
18 changes: 13 additions & 5 deletions src/category-theory/anafunctors-categories.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,18 +1,26 @@
# Anafunctors between categories

```agda
module category-theory.anafunctors-categories where
open import foundation.truncations-exist
open import foundation-core.univalence
open import foundation.function-extensionality-axiom

module category-theory.anafunctors-categories
(funext : function-extensionality)
(univalence : univalence-axiom)
(truncations : truncations-exist)
where
```

<details><summary>Imports</summary>

```agda
open import category-theory.anafunctors-precategories
open import category-theory.categories
open import category-theory.functors-categories
open import category-theory.anafunctors-precategories funext univalence truncations
open import category-theory.categories funext univalence truncations
open import category-theory.functors-categories funext univalence truncations

open import foundation.dependent-pair-types
open import foundation.propositional-truncations
open import foundation.propositional-truncations funext univalence
open import foundation.universe-levels
```

Expand Down
22 changes: 15 additions & 7 deletions src/category-theory/anafunctors-precategories.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,21 +1,29 @@
# Anafunctors between precategories

```agda
module category-theory.anafunctors-precategories where
open import foundation.truncations-exist
open import foundation-core.univalence
open import foundation.function-extensionality-axiom

module category-theory.anafunctors-precategories
(funext : function-extensionality)
(univalence : univalence-axiom)
(truncations : truncations-exist)
where
```

<details><summary>Imports</summary>

```agda
open import category-theory.functors-precategories
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories
open import category-theory.functors-precategories funext univalence truncations
open import category-theory.isomorphisms-in-precategories funext univalence truncations
open import category-theory.precategories funext univalence truncations

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.cartesian-product-types funext univalence
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.identity-types funext
open import foundation.propositional-truncations funext univalence
open import foundation.universe-levels
```

Expand Down
24 changes: 16 additions & 8 deletions src/category-theory/augmented-simplex-category.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,25 +1,33 @@
# The augmented simplex category

```agda
module category-theory.augmented-simplex-category where
open import foundation.truncations-exist
open import foundation-core.univalence
open import foundation.function-extensionality-axiom

module category-theory.augmented-simplex-category
(funext : function-extensionality)
(univalence : univalence-axiom)
(truncations : truncations-exist)
where
```

<details><summary>Imports</summary>

```agda
open import category-theory.composition-operations-on-binary-families-of-sets
open import category-theory.precategories
open import category-theory.composition-operations-on-binary-families-of-sets funext univalence truncations
open import category-theory.precategories funext univalence truncations

open import elementary-number-theory.inequality-standard-finite-types
open import elementary-number-theory.inequality-standard-finite-types funext univalence truncations
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.sets
open import foundation.strictly-involutive-identity-types
open import foundation.identity-types funext
open import foundation.sets funext univalence
open import foundation.strictly-involutive-identity-types funext univalence
open import foundation.universe-levels

open import order-theory.order-preserving-maps-posets
open import order-theory.order-preserving-maps-posets funext univalence truncations
```

</details>
Expand Down
43 changes: 26 additions & 17 deletions src/category-theory/categories.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,30 +1,39 @@
# Categories

```agda
module category-theory.categories where
open import foundation.truncations-exist
open import foundation-core.univalence
open import foundation.function-extensionality-axiom

module category-theory.categories
(funext : function-extensionality)
(univalence : univalence-axiom)
(truncations : truncations-exist)
where
```

<details><summary>Imports</summary>

```agda
open import category-theory.composition-operations-on-binary-families-of-sets
open import category-theory.isomorphisms-in-precategories
open import category-theory.nonunital-precategories
open import category-theory.precategories
open import category-theory.preunivalent-categories
open import category-theory.strongly-preunivalent-categories

open import foundation.1-types
open import foundation.cartesian-product-types
open import category-theory.composition-operations-on-binary-families-of-sets funext univalence truncations
open import category-theory.isomorphisms-in-precategories funext univalence truncations
open import category-theory.nonunital-precategories funext univalence truncations
open import category-theory.precategories funext univalence truncations
open import category-theory.preunivalent-categories funext univalence truncations
open import category-theory.strongly-preunivalent-categories funext univalence truncations

open import foundation.1-types funext univalence
open import foundation.cartesian-product-types funext univalence
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.dependent-products-propositions funext
open import foundation.equivalences funext
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.sets
open import foundation.strictly-involutive-identity-types
open import foundation.surjective-maps
open import foundation.identity-types funext
open import foundation.logical-equivalences funext
open import foundation.propositions funext univalence
open import foundation.sets funext univalence
open import foundation.strictly-involutive-identity-types funext univalence
open import foundation.surjective-maps funext univalence truncations
open import foundation.universe-levels
```

Expand Down
40 changes: 24 additions & 16 deletions src/category-theory/category-of-functors-from-small-to-large-categories.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,27 +1,35 @@
# The category of functors and natural transformations from small to large categories

```agda
module category-theory.category-of-functors-from-small-to-large-categories where
open import foundation.truncations-exist
open import foundation-core.univalence
open import foundation.function-extensionality-axiom

module category-theory.category-of-functors-from-small-to-large-categories
(funext : function-extensionality)
(univalence : univalence-axiom)
(truncations : truncations-exist)
where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import category-theory.category-of-functors
open import category-theory.functors-from-small-to-large-categories
open import category-theory.functors-from-small-to-large-precategories
open import category-theory.isomorphisms-in-large-precategories
open import category-theory.isomorphisms-in-precategories
open import category-theory.large-categories
open import category-theory.large-precategories
open import category-theory.natural-isomorphisms-functors-categories
open import category-theory.natural-isomorphisms-functors-precategories
open import category-theory.precategories
open import category-theory.precategory-of-functors-from-small-to-large-precategories

open import foundation.equivalences
open import foundation.identity-types
open import category-theory.categories funext univalence truncations
open import category-theory.category-of-functors funext univalence truncations
open import category-theory.functors-from-small-to-large-categories funext univalence truncations
open import category-theory.functors-from-small-to-large-precategories funext univalence truncations
open import category-theory.isomorphisms-in-large-precategories funext univalence truncations
open import category-theory.isomorphisms-in-precategories funext univalence truncations
open import category-theory.large-categories funext univalence truncations
open import category-theory.large-precategories funext univalence truncations
open import category-theory.natural-isomorphisms-functors-categories funext univalence truncations
open import category-theory.natural-isomorphisms-functors-precategories funext univalence truncations
open import category-theory.precategories funext univalence truncations
open import category-theory.precategory-of-functors-from-small-to-large-precategories funext univalence truncations

open import foundation.equivalences funext
open import foundation.identity-types funext
open import foundation.universe-levels
```

Expand Down
32 changes: 20 additions & 12 deletions src/category-theory/category-of-functors.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,25 +1,33 @@
# The category of functors and natural transformations between two categories

```agda
module category-theory.category-of-functors where
open import foundation.truncations-exist
open import foundation-core.univalence
open import foundation.function-extensionality-axiom

module category-theory.category-of-functors
(funext : function-extensionality)
(univalence : univalence-axiom)
(truncations : truncations-exist)
where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import category-theory.category-of-maps-categories
open import category-theory.functors-categories
open import category-theory.functors-precategories
open import category-theory.isomorphisms-in-categories
open import category-theory.natural-isomorphisms-functors-categories
open import category-theory.natural-isomorphisms-functors-precategories
open import category-theory.precategories
open import category-theory.precategory-of-functors
open import category-theory.categories funext univalence truncations
open import category-theory.category-of-maps-categories funext univalence truncations
open import category-theory.functors-categories funext univalence truncations
open import category-theory.functors-precategories funext univalence truncations
open import category-theory.isomorphisms-in-categories funext univalence truncations
open import category-theory.natural-isomorphisms-functors-categories funext univalence truncations
open import category-theory.natural-isomorphisms-functors-precategories funext univalence truncations
open import category-theory.precategories funext univalence truncations
open import category-theory.precategory-of-functors funext univalence truncations

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.equivalences funext
open import foundation.identity-types funext
open import foundation.universe-levels
```

Expand Down
Loading
Loading