Factor out standard pullbacks (#1042)

- Factors `foundation(-core).pullbacks` into a treatment for standard
pullbacks in `foundation(-core).standard-pullbacks`, and cones
satisfying `is-pullback` in `foundation(-core).pullbacks`. This makes
the file about pullbacks much more readable, finally.
- Deletes `foundation.pullback-squares` because it was just a stub, and
led to misuse in some places. After a refactoring of cones, we may want
an additional file about pullback cones.

src/category-theory/terminal-category.lagda.md

@@ -137,7 +137,7 @@ is-category-terminal-Category :
 is-category-terminal-Category x y =
   is-equiv-is-contr
     ( iso-eq-Precategory terminal-Precategory x y)
-    ( is-prop-is-contr is-contr-unit x y)
+    ( is-prop-unit x y)
     ( is-contr-Σ is-contr-unit star
       ( is-proof-irrelevant-is-prop
         ( is-prop-is-iso-Precategory terminal-Precategory star)

src/foundation-core/cartesian-product-types.lagda.md

@@ -13,11 +13,13 @@ open import foundation.universe-levels
 
 </details>
 
-## Definition
+## Definitions
 
 Cartesian products of types are defined as dependent pair types, using a
 constant type family.
 
+### The cartesian product type
+
 ```agda
 product : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
 product A B = Σ A (λ _ → B)
@@ -30,3 +32,21 @@ infixr 15 _×_
 _×_ : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
 _×_ = product
 ```
+
+### The induction principle for the cartesian product type
+
+```agda
+ind-product :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : A × B → UU l3} →
+  ((x : A) (y : B) → C (x , y)) → (t : A × B) → C t
+ind-product = ind-Σ
+```
+
+### The recursion principle for the cartesian product type
+
+```agda
+rec-product :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} →
+  (A → B → C) → (A × B) → C
+rec-product = ind-product
+```

src/foundation-core/contractible-types.lagda.md

@@ -18,6 +18,7 @@ open import foundation.universe-levels
 open import foundation-core.cartesian-product-types
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
+open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.transport-along-identifications
 ```
@@ -105,9 +106,9 @@ module _
 
   abstract
     is-contr-retract-of : A retract-of B → is-contr B → is-contr A
-    pr1 (is-contr-retract-of (pair i (pair r is-retraction)) H) = r (center H)
-    pr2 (is-contr-retract-of (pair i (pair r is-retraction)) H) x =
-      ap r (contraction H (i x)) ∙ (is-retraction x)
+    pr1 (is-contr-retract-of (pair i (pair r is-retraction-r)) H) = r (center H)
+    pr2 (is-contr-retract-of (pair i (pair r is-retraction-r)) H) x =
+      ap r (contraction H (i x)) ∙ (is-retraction-r x)
 ```
 
 ### Contractible types are closed under equivalences
@@ -120,10 +121,8 @@ module _
   abstract
     is-contr-is-equiv :
       (f : A → B) → is-equiv f → is-contr B → is-contr A
-    pr1 (is-contr-is-equiv f H (pair b K)) = map-inv-is-equiv H b
-    pr2 (is-contr-is-equiv f H (pair b K)) x =
-      ( ap (map-inv-is-equiv H) (K (f x))) ∙
-      ( is-retraction-map-inv-is-equiv H x)
+    is-contr-is-equiv f is-equiv-f =
+      is-contr-retract-of B (f , retraction-is-equiv is-equiv-f)
 
   abstract
     is-contr-equiv : (e : A ≃ B) → is-contr B → is-contr A
@@ -186,7 +185,7 @@ module _
         ( A × B)
         ( pair
           ( λ x → pair x (pr2 (center is-contr-AB)))
-          ( pair pr1 (λ x → refl)))
+          ( pair pr1 refl-htpy))
         ( is-contr-AB)
 
 module _
@@ -200,7 +199,7 @@ module _
         ( A × B)
         ( pair
           ( pair (pr1 (center is-contr-AB)))
-          ( pair pr2 (λ x → refl)))
+          ( pair pr2 refl-htpy))
         ( is-contr-AB)
 
 module _

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

@@ -331,46 +331,46 @@ module _
   pr1 (pr2 (map-compute-fiber-comp (a , p))) = a
   pr2 (pr2 (map-compute-fiber-comp (a , p))) = refl
 
-  inv-map-compute-fiber-comp :
+  map-inv-compute-fiber-comp :
     Σ (fiber g x) (λ t → fiber h (pr1 t)) → fiber (g ∘ h) x
-  pr1 (inv-map-compute-fiber-comp t) = pr1 (pr2 t)
-  pr2 (inv-map-compute-fiber-comp t) = ap g (pr2 (pr2 t)) ∙ pr2 (pr1 t)
+  pr1 (map-inv-compute-fiber-comp t) = pr1 (pr2 t)
+  pr2 (map-inv-compute-fiber-comp t) = ap g (pr2 (pr2 t)) ∙ pr2 (pr1 t)
 
-  is-section-inv-map-compute-fiber-comp :
-    is-section map-compute-fiber-comp inv-map-compute-fiber-comp
-  is-section-inv-map-compute-fiber-comp ((.(h a) , refl) , (a , refl)) = refl
+  is-section-map-inv-compute-fiber-comp :
+    is-section map-compute-fiber-comp map-inv-compute-fiber-comp
+  is-section-map-inv-compute-fiber-comp ((.(h a) , refl) , (a , refl)) = refl
 
-  is-retraction-inv-map-compute-fiber-comp :
-    is-retraction map-compute-fiber-comp inv-map-compute-fiber-comp
-  is-retraction-inv-map-compute-fiber-comp (a , refl) = refl
+  is-retraction-map-inv-compute-fiber-comp :
+    is-retraction map-compute-fiber-comp map-inv-compute-fiber-comp
+  is-retraction-map-inv-compute-fiber-comp (a , refl) = refl
 
   abstract
     is-equiv-map-compute-fiber-comp :
       is-equiv map-compute-fiber-comp
     is-equiv-map-compute-fiber-comp =
       is-equiv-is-invertible
-        ( inv-map-compute-fiber-comp)
-        ( is-section-inv-map-compute-fiber-comp)
-        ( is-retraction-inv-map-compute-fiber-comp)
+        ( map-inv-compute-fiber-comp)
+        ( is-section-map-inv-compute-fiber-comp)
+        ( is-retraction-map-inv-compute-fiber-comp)
 
   compute-fiber-comp :
     fiber (g ∘ h) x ≃ Σ (fiber g x) (λ t → fiber h (pr1 t))
   pr1 compute-fiber-comp = map-compute-fiber-comp
   pr2 compute-fiber-comp = is-equiv-map-compute-fiber-comp
 
   abstract
-    is-equiv-inv-map-compute-fiber-comp :
-      is-equiv inv-map-compute-fiber-comp
-    is-equiv-inv-map-compute-fiber-comp =
+    is-equiv-map-inv-compute-fiber-comp :
+      is-equiv map-inv-compute-fiber-comp
+    is-equiv-map-inv-compute-fiber-comp =
         is-equiv-is-invertible
           ( map-compute-fiber-comp)
-          ( is-retraction-inv-map-compute-fiber-comp)
-          ( is-section-inv-map-compute-fiber-comp)
+          ( is-retraction-map-inv-compute-fiber-comp)
+          ( is-section-map-inv-compute-fiber-comp)
 
   inv-compute-fiber-comp :
     Σ (fiber g x) (λ t → fiber h (pr1 t)) ≃ fiber (g ∘ h) x
-  pr1 inv-compute-fiber-comp = inv-map-compute-fiber-comp
-  pr2 inv-compute-fiber-comp = is-equiv-inv-map-compute-fiber-comp
+  pr1 inv-compute-fiber-comp = map-inv-compute-fiber-comp
+  pr2 inv-compute-fiber-comp = is-equiv-map-inv-compute-fiber-comp
 ```
 
 ## Table of files about fibers of maps

src/foundation-core/postcomposition-functions.lagda.md

@@ -9,8 +9,6 @@ module foundation-core.postcomposition-functions where
 ```agda
 open import foundation.postcomposition-dependent-functions
 open import foundation.universe-levels
-
-open import foundation-core.function-types
 ```
 
 </details>