Merge branch 'master' into literature-idempotents-split

src/category-theory.lagda.md

@@ -33,6 +33,7 @@ open import category-theory.copresheaf-categories public
 open import category-theory.coproducts-in-precategories public
 open import category-theory.cores-categories public
 open import category-theory.cores-precategories public
+open import category-theory.coslice-precategories public
 open import category-theory.dependent-products-of-categories public
 open import category-theory.dependent-products-of-large-categories public
 open import category-theory.dependent-products-of-large-precategories public

src/category-theory/coslice-precategories.lagda.md

@@ -0,0 +1,35 @@
+# Coslice precategories
+
+```agda
+module category-theory.coslice-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.opposite-precategories
+open import category-theory.precategories
+open import category-theory.slice-precategories
+
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The {{#concept "coslice precategory" Agda=Coslice-Precategory}} of a
+[precategory](category-theory.precategories.md) `C` under an object `X` of `C`
+is the category of objects of `C` equipped with a morphism from `X`.
+
+## Definitions
+
+```agda
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2) (X : obj-Precategory C)
+  where
+
+  Coslice-Precategory : Precategory (l1 ⊔ l2) l2
+  Coslice-Precategory =
+    Slice-Precategory (opposite-Precategory C) X
+```

src/elementary-number-theory/inequality-natural-numbers.lagda.md

@@ -7,6 +7,8 @@ module elementary-number-theory.inequality-natural-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.precategories
+
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
@@ -147,6 +149,13 @@ pr1 ℕ-Poset = ℕ-Preorder
 pr2 ℕ-Poset = antisymmetric-leq-ℕ
 ```
 
+### The precategory of natural numbers ordered by inequality
+
+```agda
+ℕ-Precategory : Precategory lzero lzero
+ℕ-Precategory = precategory-Preorder ℕ-Preorder
+```
+
 ### For any two natural numbers we can decide which one is less than the other
 
 ```agda

src/foundation-core/pullbacks.lagda.md

@@ -13,6 +13,7 @@ open import foundation.dependent-pair-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-fibers-of-maps
 open import foundation.identity-types
+open import foundation.morphisms-arrows
 open import foundation.standard-pullbacks
 open import foundation.universe-levels
 
@@ -283,14 +284,30 @@ abstract
 
 ### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the vertical maps
 
+A cone is a pullback if and only if the induced family of maps on fibers between
+the vertical maps is a family of equivalences
+
+```text
+  fiber i a --> fiber g (f a)
+      |               |
+      |               |
+      ∨               ∨
+      C ------------> B
+      |               |
+    i |               | g
+      ∨               ∨
+  a ∈ A ------------> X.
+              f
+```
+
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
   (f : A → X) (g : B → X) (c : cone f g C)
   where
 
   square-tot-map-fiber-vertical-map-cone :
-    gap f g c ∘ map-equiv-total-fiber (pr1 c) ~
+    gap f g c ∘ map-equiv-total-fiber (vertical-map-cone f g c) ~
     tot (λ _ → tot (λ _ → inv)) ∘ tot (map-fiber-vertical-map-cone f g c)
   square-tot-map-fiber-vertical-map-cone
     (.(vertical-map-cone f g c x) , x , refl) =
@@ -332,6 +349,73 @@ module _
         ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq)
 ```
 
+### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the horizontal maps
+
+A cone is a pullback if and only if the induced family of maps on fibers between
+the horizontal maps is a family of equivalences
+
+```text
+                            j
+      fiber j b ----> C --------> B ∋ b
+          |           |           |
+          |           |           | g
+          ∨           ∨           ∨
+    fiber f (g b) --> A --------> X.
+                            f
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
+  (f : A → X) (g : B → X) (c : cone f g C)
+  where
+
+  square-tot-map-fiber-horizontal-map-cone :
+    ( gap g f (swap-cone f g c) ∘
+      map-equiv-total-fiber (horizontal-map-cone f g c)) ~
+    ( tot (λ _ → tot (λ _ → inv)) ∘
+      tot (map-fiber-horizontal-map-cone f g c))
+  square-tot-map-fiber-horizontal-map-cone
+    (.(horizontal-map-cone f g c x) , x , refl) =
+    eq-pair-eq-fiber
+      ( eq-pair-eq-fiber
+        ( ap
+          ( inv)
+          ( inv (right-unit ∙ inv-inv (coherence-square-cone f g c x)))))
+
+  square-tot-map-fiber-horizontal-map-cone' :
+    ( ( λ x →
+        ( horizontal-map-cone f g c x ,
+          vertical-map-cone f g c x ,
+          coherence-square-cone f g c x)) ∘
+      map-equiv-total-fiber (horizontal-map-cone f g c)) ~
+    tot (map-fiber-horizontal-map-cone f g c)
+  square-tot-map-fiber-horizontal-map-cone'
+    (.(horizontal-map-cone f g c x) , x , refl) =
+    eq-pair-eq-fiber
+      ( eq-pair-eq-fiber
+        ( inv (right-unit ∙ inv-inv (coherence-square-cone f g c x))))
+
+  abstract
+    is-fiberwise-equiv-map-fiber-horizontal-map-cone-is-pullback :
+      is-pullback f g c →
+      is-fiberwise-equiv (map-fiber-horizontal-map-cone f g c)
+    is-fiberwise-equiv-map-fiber-horizontal-map-cone-is-pullback pb =
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback g f
+        ( swap-cone f g c)
+        ( is-pullback-swap-cone f g c pb)
+
+  abstract
+    is-pullback-is-fiberwise-equiv-map-fiber-horizontal-map-cone :
+      is-fiberwise-equiv (map-fiber-horizontal-map-cone f g c) →
+      is-pullback f g c
+    is-pullback-is-fiberwise-equiv-map-fiber-horizontal-map-cone is-equiv-fsq =
+      is-pullback-swap-cone' f g c
+        ( is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone g f
+          ( swap-cone f g c)
+          ( is-equiv-fsq))
+```
+
 ### The horizontal pullback pasting property
 
 Given a diagram as follows where the right-hand square is a pullback

src/foundation.lagda.md

@@ -250,6 +250,8 @@ open import foundation.lifts-types public
 open import foundation.limited-principle-of-omniscience public
 open import foundation.locally-small-types public
 open import foundation.logical-equivalences public
+open import foundation.maps-in-global-subuniverses public
+open import foundation.maps-in-subuniverses public
 open import foundation.maybe public
 open import foundation.mere-embeddings public
 open import foundation.mere-equality public
@@ -279,6 +281,7 @@ open import foundation.multivariable-sections public
 open import foundation.negated-equality public
 open import foundation.negation public
 open import foundation.noncontractible-types public
+open import foundation.null-homotopic-maps public
 open import foundation.operations-span-diagrams public
 open import foundation.operations-spans public
 open import foundation.operations-spans-families-of-types public

src/foundation/cartesian-morphisms-arrows.lagda.md

@@ -22,6 +22,7 @@ open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-coproduct-types
 open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-fibers-of-maps
 open import foundation.homotopies-morphisms-arrows
 open import foundation.identity-types
 open import foundation.morphisms-arrows
@@ -174,6 +175,30 @@ module _
       ( is-pullback-cone-fiber f y)
 ```
 
+### The induced family of equivalences of fibers of cartesian morphisms of arrows
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y) (h : cartesian-hom-arrow f g)
+  where
+
+  equiv-fibers-cartesian-hom-arrow :
+    (b : B) → fiber f b ≃ fiber g (map-codomain-cartesian-hom-arrow f g h b)
+  equiv-fibers-cartesian-hom-arrow b =
+    ( map-fiber-vertical-map-cone
+      ( map-codomain-cartesian-hom-arrow f g h)
+      ( g)
+      ( cone-cartesian-hom-arrow f g h)
+      ( b)) ,
+    ( is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
+      ( map-codomain-cartesian-hom-arrow f g h)
+      ( g)
+      ( cone-cartesian-hom-arrow f g h)
+      ( is-cartesian-cartesian-hom-arrow f g h)
+      ( b))
+```
+
 ### Transposing cartesian morphisms of arrows
 
 The {{#concept "transposition" Disambiguation="cartesian morphism of arrows"}}
@@ -831,7 +856,7 @@ module _
 
 ### Lifting cartesian morphisms along lifts of the codomain
 
-Suppose given a cospan of morphisms of arrows
+Suppose given a cospan diagram of arrows
 
 ```text
     A ------> C <------ B

src/foundation/dependent-sums-pullbacks.lagda.md

@@ -102,7 +102,7 @@ Given a map `f : A → B` with a family of maps over it
 
 ```text
          map-Σ f g
-  Σ A P ----------> Σ B Q
+  Σ A P ---------> Σ B Q
     |                |
     |                |
     ∨                ∨

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

@@ -123,6 +123,24 @@ module _
       ( a)
 ```
 
+### Any cone induces a family of maps between the fibers of the vertical maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
+  (f : A → X) (g : B → X) (c : cone f g C) (b : B)
+  where
+
+  map-fiber-horizontal-map-cone :
+    fiber (horizontal-map-cone f g c) b → fiber f (g b)
+  map-fiber-horizontal-map-cone =
+    map-domain-hom-arrow-fiber
+      ( horizontal-map-cone f g c)
+      ( f)
+      ( hom-arrow-cone' f g c)
+      ( b)
+```
+
 ### For any `f : A → B` and any identification `p : b ＝ b'` in `B`, we obtain a morphism of arrows between the fiber inclusion at `b` to the fiber inclusion at `b'`
 
 ```agda

src/foundation/global-subuniverses.lagda.md

@@ -67,41 +67,25 @@ record global-subuniverse (α : Level → Level) : UUω where
       (l1 l2 : Level) →
       is-closed-under-equiv-subuniverses α subuniverse-global-subuniverse l1 l2
 
-open global-subuniverse public
-
-module _
-  {α : Level → Level} (P : global-subuniverse α)
-  where
-
   is-in-global-subuniverse : {l : Level} → UU l → UU (α l)
   is-in-global-subuniverse {l} X =
-    is-in-subuniverse (subuniverse-global-subuniverse P l) X
+    is-in-subuniverse (subuniverse-global-subuniverse l) X
+
+  is-prop-is-in-global-subuniverse :
+    {l : Level} (X : UU l) → is-prop (is-in-global-subuniverse X)
+  is-prop-is-in-global-subuniverse {l} X =
+    is-prop-type-Prop (subuniverse-global-subuniverse l X)
 
   type-global-subuniverse : (l : Level) → UU (α l ⊔ lsuc l)
   type-global-subuniverse l =
-    type-subuniverse (subuniverse-global-subuniverse P l)
+    type-subuniverse (subuniverse-global-subuniverse l)
 
   inclusion-global-subuniverse :
     {l : Level} → type-global-subuniverse l → UU l
   inclusion-global-subuniverse {l} =
-    inclusion-subuniverse (subuniverse-global-subuniverse P l)
-```
+    inclusion-subuniverse (subuniverse-global-subuniverse l)
 
-### Maps in a subuniverse
-
-We say a map is _in_ a global subuniverse if each of its
-[fibers](foundation-core.fibers-of-maps.md) is.
-
-```agda
-module _
-  {α : Level → Level} (P : global-subuniverse α)
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  where
-
-  is-in-map-global-subuniverse : (A → B) → UU (α (l1 ⊔ l2) ⊔ l2)
-  is-in-map-global-subuniverse f =
-    (y : B) →
-    is-in-subuniverse (subuniverse-global-subuniverse P (l1 ⊔ l2)) (fiber f y)
+open global-subuniverse public
 ```
 
 ### The predicate of essentially being in a subuniverse

src/foundation/homotopy-induction.lagda.md

@@ -88,7 +88,7 @@ module _
     is-torsorial-htpy : is-torsorial (λ g → f ~ g)
     is-torsorial-htpy =
       is-contr-equiv'
-        ( Σ ((x : A) → B x) (Id f))
+        ( Σ ((x : A) → B x) (λ g → f ＝ g))
         ( equiv-tot (λ g → equiv-funext))
         ( is-torsorial-Id f)
 
@@ -109,8 +109,7 @@ abstract
     {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) →
     based-function-extensionality f →
     induction-principle-homotopies f
-  induction-principle-homotopies-based-function-extensionality
-    {A = A} {B} f funext-f =
+  induction-principle-homotopies-based-function-extensionality f funext-f =
     is-identity-system-is-torsorial f
       ( refl-htpy)
       ( is-torsorial-htpy f)
@@ -170,6 +169,10 @@ module _
 
   is-contr-map-ev-refl-htpy : is-contr-map (ev-refl-htpy C)
   is-contr-map-ev-refl-htpy = is-contr-map-is-equiv is-equiv-ev-refl-htpy
+
+  equiv-ev-refl-htpy :
+    ((g : (x : A) → B x) (H : f ~ g) → C g H) ≃ C f refl-htpy
+  equiv-ev-refl-htpy = (ev-refl-htpy C , is-equiv-ev-refl-htpy)
 ```
 
 ## See also