Basic properties of orthogonal maps (#979)

- Coproducts of pullbacks are pullbacks
- Gives some equivalent characterizations of orthogonal maps
- Orthogonal maps are closed under homotopy
- Equivalences are left and right orthogonal to any map
- Right orthogonal maps are closed under
  - Composition
  - Left cancellation
  - Dependent products
  - Postcomp exponentiation
  - Products
  - Base change
- Left orthogonal maps are closed under
  - Composition
  - Right cancellation
  - Dependent sums
  - Coproducts
- Local (dependent) types are closed under
  - equivalent types
  - function homotopy
- A type is `f`-local if and only if its terminal map is
- A type is `f`-local if and only if its terminal map is `f`-orthogonal
- A dependent type is `f`-local if its fibers are `f`-null
- Code formatting and refactoring for pullbacks and miscellaneous.

src/category-theory/split-essentially-surjective-functors-precategories.lagda.md

@@ -151,9 +151,8 @@ module _
   where
 
   is-essentially-surjective-is-split-essentially-surjective-functor-Precategory :
-    (F : functor-Precategory C D)
-    (is-split-ess-surj-F :
-        is-split-essentially-surjective-functor-Precategory C D F) →
+    (F : functor-Precategory C D) →
+    is-split-essentially-surjective-functor-Precategory C D F →
     is-essentially-surjective-functor-Precategory C D F
   is-essentially-surjective-is-split-essentially-surjective-functor-Precategory
     F is-split-ess-surj-F =
@@ -179,7 +178,7 @@ Rezk completion_.
    ([arXiv:1303.0584](https://arxiv.org/abs/1303.0584),
    [DOI:10.1017/S0960129514000486](https://doi.org/10.1017/S0960129514000486))
 
-## External link
+## External links
 
 - [Essential Fibres](https://1lab.dev/Cat.Functor.Properties.html#essential-fibres)
   at 1lab

src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md

@@ -748,8 +748,7 @@ is-in-prime-decomposition-is-nontrivial-prime-divisor-ℕ x H nil D y d p =
           ( 1)
           ( inv (is-decomposition-list-is-prime-decomposition-list-ℕ x nil D))))
 is-in-prime-decomposition-is-nontrivial-prime-divisor-ℕ x H (cons z l) D y d p =
-  ind-coprod
-    ( λ _ → y ∈-list (cons z l))
+  rec-coprod
     ( λ e → tr (λ w → w ∈-list (cons z l)) (inv e) (is-head z l))
     ( λ e →
       is-in-tail
@@ -947,7 +946,7 @@ pr2 (fundamental-theorem-arithmetic-list-ℕ x H) d =
 ```agda
 is-prime-list-concat-list-ℕ :
   (p q : list ℕ) → is-prime-list-ℕ p → is-prime-list-ℕ q →
-  is-prime-list-ℕ (concat-list p q)
+  is-prime-list-ℕ (concat-list p q)
 is-prime-list-concat-list-ℕ nil q Pp Pq = Pq
 is-prime-list-concat-list-ℕ (cons x p) q Pp Pq =
   pr1 Pp , is-prime-list-concat-list-ℕ p q (pr2 Pp) Pq

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

@@ -19,18 +19,33 @@ of `A` and `B`.
 
 ## Definition
 
+### Coproduct types
+
 ```agda
 infixr 10 _+_
 
 data _+_ {l1 l2 : Level} (A : UU l1) (B : UU l2) : UU (l1 ⊔ l2)
   where
   inl : A → A + B
   inr : B → A + B
+```
 
+### The induction principle for coproduct types
+
+```agda
 ind-coprod :
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (C : A + B → UU l3) →
   ((x : A) → C (inl x)) → ((y : B) → C (inr y)) →
   (t : A + B) → C t
 ind-coprod C f g (inl x) = f x
 ind-coprod C f g (inr x) = g x
 ```
+
+### The recursion principle for coproduct types
+
+```agda
+rec-coprod :
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} →
+  (A → C) → (B → C) → (A + B) → C
+rec-coprod {C = C} = ind-coprod (λ _ → C)
+```

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

@@ -15,6 +15,8 @@ open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
+open import foundation-core.retractions
+open import foundation-core.sections
 open import foundation-core.transport-along-identifications
 ```
 
@@ -79,11 +81,13 @@ module _
   eq-Eq-fiber α β = eq-Eq-fiber-uncurry (α , β)
 
   is-section-eq-Eq-fiber :
-    {s t : fiber f b} → Eq-eq-fiber {s} {t} ∘ eq-Eq-fiber-uncurry {s} {t} ~ id
+    {s t : fiber f b} →
+    is-section (Eq-eq-fiber {s} {t}) (eq-Eq-fiber-uncurry {s} {t})
   is-section-eq-Eq-fiber (refl , refl) = refl
 
   is-retraction-eq-Eq-fiber :
-    {s t : fiber f b} → eq-Eq-fiber-uncurry {s} {t} ∘ Eq-eq-fiber {s} {t} ~ id
+    {s t : fiber f b} →
+    is-retraction (Eq-eq-fiber {s} {t}) (eq-Eq-fiber-uncurry {s} {t})
   is-retraction-eq-Eq-fiber refl = refl
 
   abstract
@@ -144,12 +148,12 @@ module _
 
   is-section-eq-Eq-fiber' :
     {s t : fiber' f b} →
-    Eq-eq-fiber' {s} {t} ∘ eq-Eq-fiber-uncurry' {s} {t} ~ id
+    is-section (Eq-eq-fiber' {s} {t}) (eq-Eq-fiber-uncurry' {s} {t})
   is-section-eq-Eq-fiber' {x , refl} (refl , refl) = refl
 
   is-retraction-eq-Eq-fiber' :
     {s t : fiber' f b} →
-    eq-Eq-fiber-uncurry' {s} {t} ∘ Eq-eq-fiber' {s} {t} ~ id
+    is-retraction (Eq-eq-fiber' {s} {t}) (eq-Eq-fiber-uncurry' {s} {t})
   is-retraction-eq-Eq-fiber' {x , refl} refl = refl
 
   abstract
@@ -187,17 +191,19 @@ module _
   where
 
   map-equiv-fiber : fiber f y → fiber' f y
-  pr1 (map-equiv-fiber (x , refl)) = x
-  pr2 (map-equiv-fiber (x , refl)) = refl
+  pr1 (map-equiv-fiber (x , _)) = x
+  pr2 (map-equiv-fiber (x , p)) = inv p
 
   map-inv-equiv-fiber : fiber' f y → fiber f y
-  pr1 (map-inv-equiv-fiber (x , refl)) = x
-  pr2 (map-inv-equiv-fiber (x , refl)) = refl
+  pr1 (map-inv-equiv-fiber (x , _)) = x
+  pr2 (map-inv-equiv-fiber (x , p)) = inv p
 
-  is-section-map-inv-equiv-fiber : map-equiv-fiber ∘ map-inv-equiv-fiber ~ id
+  is-section-map-inv-equiv-fiber :
+    is-section map-equiv-fiber map-inv-equiv-fiber
   is-section-map-inv-equiv-fiber (x , refl) = refl
 
-  is-retraction-map-inv-equiv-fiber : map-inv-equiv-fiber ∘ map-equiv-fiber ~ id
+  is-retraction-map-inv-equiv-fiber :
+    is-retraction map-equiv-fiber map-inv-equiv-fiber
   is-retraction-map-inv-equiv-fiber (x , refl) = refl
 
   is-equiv-map-equiv-fiber : is-equiv map-equiv-fiber
@@ -227,19 +233,21 @@ module _
   pr2 (pr1 (map-inv-fiber-pr1 b)) = b
   pr2 (map-inv-fiber-pr1 b) = refl
 
-  is-section-map-inv-fiber-pr1 : (map-inv-fiber-pr1 ∘ map-fiber-pr1) ~ id
-  is-section-map-inv-fiber-pr1 ((.a , y) , refl) = refl
+  is-section-map-inv-fiber-pr1 :
+    is-section map-fiber-pr1 map-inv-fiber-pr1
+  is-section-map-inv-fiber-pr1 b = refl
 
-  is-retraction-map-inv-fiber-pr1 : (map-fiber-pr1 ∘ map-inv-fiber-pr1) ~ id
-  is-retraction-map-inv-fiber-pr1 b = refl
+  is-retraction-map-inv-fiber-pr1 :
+    is-retraction map-fiber-pr1 map-inv-fiber-pr1
+  is-retraction-map-inv-fiber-pr1 ((.a , y) , refl) = refl
 
   abstract
     is-equiv-map-fiber-pr1 : is-equiv map-fiber-pr1
     is-equiv-map-fiber-pr1 =
       is-equiv-is-invertible
         map-inv-fiber-pr1
-        is-retraction-map-inv-fiber-pr1
         is-section-map-inv-fiber-pr1
+        is-retraction-map-inv-fiber-pr1
 
   equiv-fiber-pr1 : fiber (pr1 {B = B}) a ≃ B a
   pr1 equiv-fiber-pr1 = map-fiber-pr1
@@ -250,8 +258,8 @@ module _
     is-equiv-map-inv-fiber-pr1 =
       is-equiv-is-invertible
         map-fiber-pr1
-        is-section-map-inv-fiber-pr1
         is-retraction-map-inv-fiber-pr1
+        is-section-map-inv-fiber-pr1
 
   inv-equiv-fiber-pr1 : B a ≃ fiber (pr1 {B = B}) a
   pr1 inv-equiv-fiber-pr1 = map-inv-fiber-pr1
@@ -265,10 +273,10 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
   where
 
-  map-equiv-total-fiber : (Σ B (fiber f)) → A
+  map-equiv-total-fiber : Σ B (fiber f) → A
   map-equiv-total-fiber t = pr1 (pr2 t)
 
-  triangle-map-equiv-total-fiber : pr1 ~ (f ∘ map-equiv-total-fiber)
+  triangle-map-equiv-total-fiber : pr1 ~ f ∘ map-equiv-total-fiber
   triangle-map-equiv-total-fiber t = inv (pr2 (pr2 t))
 
   map-inv-equiv-total-fiber : A → Σ B (fiber f)
@@ -277,11 +285,11 @@ module _
   pr2 (pr2 (map-inv-equiv-total-fiber x)) = refl
 
   is-retraction-map-inv-equiv-total-fiber :
-    (map-inv-equiv-total-fiber ∘ map-equiv-total-fiber) ~ id
+    is-retraction map-equiv-total-fiber map-inv-equiv-total-fiber
   is-retraction-map-inv-equiv-total-fiber (.(f x) , x , refl) = refl
 
   is-section-map-inv-equiv-total-fiber :
-    (map-equiv-total-fiber ∘ map-inv-equiv-total-fiber) ~ id
+    is-section map-equiv-total-fiber map-inv-equiv-total-fiber
   is-section-map-inv-equiv-total-fiber x = refl
 
   abstract
@@ -329,11 +337,11 @@ module _
   pr2 (inv-map-compute-fiber-comp t) = ap g (pr2 (pr2 t)) ∙ pr2 (pr1 t)
 
   is-section-inv-map-compute-fiber-comp :
-    (map-compute-fiber-comp ∘ inv-map-compute-fiber-comp) ~ id
+    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-retraction-inv-map-compute-fiber-comp :
-    (inv-map-compute-fiber-comp ∘ map-compute-fiber-comp) ~ id
+    is-retraction map-compute-fiber-comp inv-map-compute-fiber-comp
   is-retraction-inv-map-compute-fiber-comp (a , refl) = refl
 
   abstract

src/foundation-core/functoriality-dependent-function-types.lagda.md

@@ -52,8 +52,7 @@ compute-fiber-map-Π :
   {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
   (f : (i : I) → A i → B i) (h : (i : I) → B i) →
   ((i : I) → fiber (f i) (h i)) ≃ fiber (map-Π f) h
-compute-fiber-map-Π f h =
-  equiv-tot (λ _ → equiv-eq-htpy) ∘e distributive-Π-Σ
+compute-fiber-map-Π f h = equiv-tot (λ _ → equiv-eq-htpy) ∘e distributive-Π-Σ
 
 compute-fiber-map-Π' :
   {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
@@ -109,7 +108,7 @@ module _
   compute-inv-equiv-Π-equiv-family :
     (e : (x : A) → B x ≃ C x) →
     ( map-inv-equiv (equiv-Π-equiv-family e)) ~
-    ( map-equiv (equiv-Π-equiv-family λ x → (inv-equiv (e x))))
+    ( map-equiv (equiv-Π-equiv-family (λ x → inv-equiv (e x))))
   compute-inv-equiv-Π-equiv-family e f =
     is-injective-map-equiv
       ( equiv-Π-equiv-family e)