Sequential limits

src/elementary-number-theory/divisibility-modular-arithmetic.lagda.md

@@ -18,7 +18,7 @@ open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.universe-levels
 
-open import univalent-combinatorics.fibers-of-maps
+open import univalent-combinatorics.fibers-of-maps-finite-types
 ```
 
 </details>

src/elementary-number-theory/squares-modular-arithmetic.lagda.md

@@ -16,7 +16,7 @@ open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.universe-levels
 
-open import univalent-combinatorics.fibers-of-maps
+open import univalent-combinatorics.fibers-of-maps-finite-types
 ```
 
 </details>

src/foundation-core/fibers-of-maps.lagda.md

@@ -23,9 +23,9 @@ open import foundation-core.transport-along-identifications
 
 ## Idea
 
-Given a map `f : A → B` and a point `b : B`, the fiber of `f` at `b` is the
-preimage of `f` at `b`. In other words, it consists of the elements `a : A`
-equipped with an identification `Id (f a) b`.
+Given a map `f : A → B` and an element `b : B`, the **fiber** of `f` at `b` is
+the preimage of `f` at `b`. In other words, it consists of the elements `a : A`
+equipped with an [identification](foundation-core.identity-types.md) `f a ＝ b`.
 
 ## Definition
 
@@ -403,3 +403,10 @@ reduce-Π-fiber :
   (C : B → UU l3) → ((y : B) → fiber f y → C y) ≃ ((x : A) → C (f x))
 reduce-Π-fiber f C = reduce-Π-fiber' f (λ y z → C y)
 ```
+
+## Table of files about fibers of maps
+
+The following table lists files that are about fibers of maps as a general
+concept.
+
+{{#include tables/fibers-of-maps.md}}

src/foundation/equality-fibers-of-maps.lagda.md

@@ -119,6 +119,13 @@ module _
         ( is-equiv-tr (fiber (ap f)) right-unit)
 ```
 
+## Table of files about fibers of maps
+
+The following table lists files that are about fibers of maps as a general
+concept.
+
+{{#include tables/fibers-of-maps.md}}
+
 ## See also
 
 - Equality proofs in dependent pair types are characterized in

src/foundation/fibers-of-maps.lagda.md

@@ -58,3 +58,10 @@ module _
         ( cone-fiber)
         ( is-pullback-cone-fiber)
 ```
+
+## Table of files about fibers of maps
+
+The following table lists files that are about fibers of maps as a general
+concept.
+
+{{#include tables/fibers-of-maps.md}}

src/foundation/functoriality-fibers-of-maps.lagda.md

@@ -114,7 +114,9 @@ module _
             ( ap (ap g) (inv right-unit)))))
 ```
 
-## See also
+## Table of files about fibers of maps
 
-- Equality proofs in the fiber of a map are characterized in
-  [`foundation.equality-fibers-of-maps`](foundation.equality-fibers-of-maps.md).
+The following table lists files that are about fibers of maps as a general
+concept.
+
+{{#include tables/fibers-of-maps.md}}

src/graph-theory/complete-bipartite-graphs.lagda.md

@@ -17,7 +17,7 @@ open import univalent-combinatorics.2-element-types
 open import univalent-combinatorics.cartesian-product-types
 open import univalent-combinatorics.coproduct-types
 open import univalent-combinatorics.dependent-pair-types
-open import univalent-combinatorics.fibers-of-maps
+open import univalent-combinatorics.fibers-of-maps-finite-types
 open import univalent-combinatorics.finite-types
 ```
 

src/univalent-combinatorics.lagda.md

@@ -57,7 +57,7 @@ open import univalent-combinatorics.equivalences public
 open import univalent-combinatorics.equivalences-cubes public
 open import univalent-combinatorics.equivalences-standard-finite-types public
 open import univalent-combinatorics.ferrers-diagrams public
-open import univalent-combinatorics.fibers-of-maps public
+open import univalent-combinatorics.fibers-of-maps-finite-types public
 open import univalent-combinatorics.finite-choice public
 open import univalent-combinatorics.finite-connected-components public
 open import univalent-combinatorics.finite-presentations public

src/univalent-combinatorics/fibers-of-maps.lagda.md → src/univalent-combinatorics/fibers-of-maps-finite-types.lagda.md

@@ -1,7 +1,7 @@
 # Fibers of maps between finite types
 
 ```agda
-module univalent-combinatorics.fibers-of-maps where
+module univalent-combinatorics.fibers-of-maps-finite-types where
 
 open import foundation.fibers-of-maps public
 ```
@@ -144,13 +144,13 @@ equiv-is-finite-domain-is-finite-fiber :
   {l1 l2 : Level} {A : UU l1} →
   (B : 𝔽 l2) (f : A → (type-𝔽 B)) →
   ((b : type-𝔽 B) → is-finite (fiber f b)) ≃ is-finite A
-equiv-is-finite-domain-is-finite-fiber {A = A} B f =
+equiv-is-finite-domain-is-finite-fiber B f =
   equiv-prop
     ( is-prop-Π (λ b → is-prop-is-finite (fiber f b)))
     ( is-prop-is-finite A)
     ( λ P →
       is-finite-equiv
         ( equiv-total-fiber f)
         ( is-finite-Σ (is-finite-type-𝔽 B) P))
-    ( λ P → is-finite-fiber f P ( is-finite-type-𝔽 B))
+    ( λ P → is-finite-fiber f P (is-finite-type-𝔽 B))
 ```

src/univalent-combinatorics/surjective-maps.lagda.md

@@ -27,7 +27,7 @@ open import univalent-combinatorics.counting-decidable-subtypes
 open import univalent-combinatorics.counting-dependent-pair-types
 open import univalent-combinatorics.decidable-dependent-function-types
 open import univalent-combinatorics.embeddings
-open import univalent-combinatorics.fibers-of-maps
+open import univalent-combinatorics.fibers-of-maps-finite-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.standard-finite-types
 ```

src/univalent-combinatorics/type-duality.lagda.md

@@ -26,7 +26,7 @@ open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.type-theoretic-principle-of-choice
 open import foundation.universe-levels
 
-open import univalent-combinatorics.fibers-of-maps
+open import univalent-combinatorics.fibers-of-maps-finite-types
 open import univalent-combinatorics.finite-types
 open import univalent-combinatorics.inhabited-finite-types
 ```

tables/fibers-of-maps.md

@@ -0,0 +1,8 @@
+| Concept                          | File                                                                                                            |
+| -------------------------------- | --------------------------------------------------------------------------------------------------------------- |
+| Equality in the fibers of a map  | [`foundation.equality-fibers-of-maps`](foundation.equality-fibers-of-maps.md)                                   |
+| Fibers of maps (foundation)      | [`foundation.fibers-of-maps`](foundation.fibers-of-maps.md)                                                     |
+| Fibers of maps (foundation-core) | [`foundation-core.fibers-of-maps`](foundation-core.fibers-of-maps.md)                                           |
+| Fibers of maps of finite types   | [`univalent-combinatorics.fibers-of-maps-finite-types`](univalent-combinatorics.fibers-of-maps-finite-types.md) |
+| Fibers of pointed maps           | [`structured-types.fibers-of-pointed-maps`](structured-types.fibers-of-pointed-maps.md)                         |
+| Functoriality of fibers of maps  | [`foundation.functoriality-fibers-of-maps`](foundation.functoriality-fibers-of-maps.md)                         |